abc/src/bdd/cudd/cuddGenCof.c
/**Function********************************************************************

  Synopsis    [Performs the edge marking step of Cudd_bddLICompaction.]

  Description [Performs the edge marking step of Cudd_bddLICompaction.
  Returns the LUB of the markings of the two outgoing edges of <code>f</code>
  if successful; otherwise CUDD_OUT_OF_MEM.]

  SideEffects [None]

  SeeAlso     [Cudd_bddLICompaction cuddBddLICBuildResult]

******************************************************************************/
Function
Synopsis    [Performs the edge marking step of Cudd_bddLICompaction.]

Description [Performs the edge marking step of Cudd_bddLICompaction.
Returns the LUB of the markings of the two outgoing edges of f
if successful; otherwise CUDD_OUT_OF_MEM.]




Function Synopsis [ Performs the edge marking step of Cudd_bddLICompaction . ] Description [ Performs the edge marking step of Cudd_bddLICompaction . Returns the LUB of the markings of the two outgoing edges of f if successful ; otherwise CUDD_OUT_OF_MEM . ]
static int
cuddBddLICMarkEdges(
  DdManager * dd,
  DdNode * f,
  DdNode * c,
  st__table * table,
  st__table * cache)
{
    DdNode *Fv, *Fnv, *Cv, *Cnv;
    DdNode *one, *zero;
    unsigned int topf, topc;
    int comple;
    int resT, resE, res, retval;
    char **slot;
    MarkCacheKey *key;
    one = DD_ONE(dd);
    zero = Cudd_Not(one);
    if (c == zero) return(DD_LIC_DC);
    if (f == one)  return(DD_LIC_1);
    if (f == zero) return(DD_LIC_0);
    comple = Cudd_IsComplement(f);
    f = Cudd_Regular(f);
    key = ABC_ALLOC(MarkCacheKey, 1);
    if (key == NULL) {
        dd->errorCode = CUDD_MEMORY_OUT;
        return(CUDD_OUT_OF_MEM);
    }
    key->f = f; key->c = c;
    if ( st__lookup_int(cache, (char *)key, &res)) {
        ABC_FREE(key);
        if (comple) {
            if (res == DD_LIC_0) res = DD_LIC_1;
            else if (res == DD_LIC_1) res = DD_LIC_0;
        }
        return(res);
    }
    topf = dd->perm[f->index];
    topc = cuddI(dd,Cudd_Regular(c)->index);
    if (topf <= topc) {
        Fv = cuddT(f); Fnv = cuddE(f);
    } else {
        Fv = Fnv = f;
    }
    if (topc <= topf) {
        Cv = cuddT(Cudd_Regular(c)); Cnv = cuddE(Cudd_Regular(c));
        if (Cudd_IsComplement(c)) {
            Cv = Cudd_Not(Cv);
            Cnv = Cudd_Not(Cnv);
        }
    } else {
        Cv = Cnv = c;
    }
    resT = cuddBddLICMarkEdges(dd, Fv, Cv, table, cache);
    if (resT == CUDD_OUT_OF_MEM) {
        ABC_FREE(key);
        return(CUDD_OUT_OF_MEM);
    }
    resE = cuddBddLICMarkEdges(dd, Fnv, Cnv, table, cache);
    if (resE == CUDD_OUT_OF_MEM) {
        ABC_FREE(key);
        return(CUDD_OUT_OF_MEM);
    }
    if (topf <= topc) {
        retval = st__find_or_add(table, (char *)f, (char ***)&slot);
        if (retval == 0) {
            *slot = (char *) (ptrint)((resT << 2) | resE);
        } else if (retval == 1) {
            *slot = (char *) (ptrint)((int)((ptrint) *slot) | (resT << 2) | resE);
        } else {
            ABC_FREE(key);
            return(CUDD_OUT_OF_MEM);
        }
    }
    res = resT | resE;
    if ( st__insert(cache, (char *)key, (char *)(ptrint)res) == st__OUT_OF_MEM) {
        ABC_FREE(key);
        return(CUDD_OUT_OF_MEM);
    }
    if (comple) {
        if (res == DD_LIC_0) res = DD_LIC_1;
        else if (res == DD_LIC_1) res = DD_LIC_0;
    }
    return(res);
}
static int cuddBddLICMarkEdges ( DdManager * dd , DdNode * f , DdNode * c , st__table * table , st__table * cache ) { DdNode * Fv , * Fnv , * Cv , * Cnv ; DdNode * one , * zero ; unsigned int topf , topc ; int comple ; int resT , resE , res , retval ; char * * slot ; MarkCacheKey * key ; one = DD_ONE ( dd ) ; zero = Cudd_Not ( one ) ; if ( c == zero ) return ( DD_LIC_DC ) ; if ( f == one ) return ( DD_LIC_1 ) ; if ( f == zero ) return ( DD_LIC_0 ) ; comple = Cudd_IsComplement ( f ) ; f = Cudd_Regular ( f ) ; key = ABC_ALLOC ( MarkCacheKey , 1 ) ; if ( key == NULL ) { dd -> errorCode = CUDD_MEMORY_OUT ; return ( CUDD_OUT_OF_MEM ) ; } key -> f = f ; key -> c = c ; if ( st__lookup_int ( cache , ( char * ) key , & res ) ) { ABC_FREE ( key ) ; if ( comple ) { if ( res == DD_LIC_0 ) res = DD_LIC_1 ; else if ( res == DD_LIC_1 ) res = DD_LIC_0 ; } return ( res ) ; } topf = dd -> perm [ f -> index ] ; topc = cuddI ( dd , Cudd_Regular ( c ) -> index ) ; if ( topf <= topc ) { Fv = cuddT ( f ) ; Fnv = cuddE ( f ) ; } else { Fv = Fnv = f ; } if ( topc <= topf ) { Cv = cuddT ( Cudd_Regular ( c ) ) ; Cnv = cuddE ( Cudd_Regular ( c ) ) ; if ( Cudd_IsComplement ( c ) ) { Cv = Cudd_Not ( Cv ) ; Cnv = Cudd_Not ( Cnv ) ; } } else { Cv = Cnv = c ; } resT = cuddBddLICMarkEdges ( dd , Fv , Cv , table , cache ) ; if ( resT == CUDD_OUT_OF_MEM ) { ABC_FREE ( key ) ; return ( CUDD_OUT_OF_MEM ) ; } resE = cuddBddLICMarkEdges ( dd , Fnv , Cnv , table , cache ) ; if ( resE == CUDD_OUT_OF_MEM ) { ABC_FREE ( key ) ; return ( CUDD_OUT_OF_MEM ) ; } if ( topf <= topc ) { retval = st__find_or_add ( table , ( char * ) f , ( char * * * ) & slot ) ; if ( retval == 0 ) { * slot = ( char * ) ( ptrint ) ( ( resT << 2 ) | resE ) ; } else if ( retval == 1 ) { * slot = ( char * ) ( ptrint ) ( ( int ) ( ( ptrint ) * slot ) | ( resT << 2 ) | resE ) ; } else { ABC_FREE ( key ) ; return ( CUDD_OUT_OF_MEM ) ; } } res = resT | resE ; if ( st__insert ( cache , ( char * ) key , ( char * ) ( ptrint ) res ) == st__OUT_OF_MEM ) { ABC_FREE ( key ) ; return ( CUDD_OUT_OF_MEM ) ; } if ( comple ) { if ( res == DD_LIC_0 ) res = DD_LIC_1 ; else if ( res == DD_LIC_1 ) res = DD_LIC_0 ; } return ( res ) ; }
Function
Synopsis    [Performs the edge marking step of Cudd_bddLICompaction.]
Function Synopsis [ Performs the edge marking step of Cudd_bddLICompaction . ]
/* Terminal cases. */ /* Make canonical to increase the utilization of the cache. */ /* Now f is a regular pointer to a non-constant node; c may be
    ** constant, or it may be complemented.
    */ /* Check the cache. */ /* Recursive step. */ /* We know that c is not constant because f is not. */ /* Update edge markings. */ /* Cache result. */ /* Take into account possible complementation. */