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

  Synopsis    [Check the tables for the existence of pair and return one
  combination, cache the result.]

  Description [Check the tables for the existence of pair and return
  one combination, cache the result. The assumption is that one of the
  conjuncts is already in the tables.]

  SideEffects [g and h referenced for the cache]

  SeeAlso     [ZeroCase]

******************************************************************************/
Function
Synopsis    [Check the tables for the existence of pair and return one
combination, cache the result.]

Description [Check the tables for the existence of pair and return
one combination, cache the result. The assumption is that one of the
conjuncts is already in the tables.]

SideEffects [g and h referenced for the cache]


Function Synopsis [ Check the tables for the existence of pair and return one combination cache the result . ] Description [ Check the tables for the existence of pair and return one combination cache the result . The assumption is that one of the conjuncts is already in the tables . ] SideEffects [ g and h referenced for the cache ]
static Conjuncts *
CheckTablesCacheAndReturn(
  DdNode * node,
  DdNode * g,
  DdNode * h,
  st__table * ghTable,
  st__table * cacheTable)
{
    int pairValue;
    int value;
    Conjuncts *factors;
    value = 0;
    pairValue = PairInTables(g, h, ghTable);
    assert(pairValue != NONE);
    factors = ABC_ALLOC(Conjuncts, 1);
    if (factors == NULL) return(NULL);
    if ((pairValue == BOTH_H) || (pairValue == H_ST)) {
        if (g != one) {
            value = 0;
            if ( st__lookup_int(ghTable, (char *)Cudd_Regular(g), &value)) {
                value |= 1;
            } else {
                value = 1;
            }
            if ( st__insert(ghTable, (char *)Cudd_Regular(g),
                          (char *)(long)value) == st__OUT_OF_MEM) {
                return(NULL);
            }
        }
        factors->g = g;
        factors->h = h;
    } else  if ((pairValue == BOTH_G) || (pairValue == G_ST)) {
        if (h != one) {
            value = 0;
            if ( st__lookup_int(ghTable, (char *)Cudd_Regular(h), &value)) {
                value |= 2;
            } else {
                value = 2;
            }
            if ( st__insert(ghTable, (char *)Cudd_Regular(h),
                          (char *)(long)value) == st__OUT_OF_MEM) {
                return(NULL);
            }
        }
        factors->g = g;
        factors->h = h;
    } else if (pairValue == H_CR) {
        if (g != one) {
            value = 2;
            if ( st__insert(ghTable, (char *)Cudd_Regular(g),
                          (char *)(long)value) == st__OUT_OF_MEM) {
                return(NULL);
            }
        }
        factors->g = h;
        factors->h = g;
    } else if (pairValue == G_CR) {
        if (h != one) {
            value = 1;
            if ( st__insert(ghTable, (char *)Cudd_Regular(h),
                          (char *)(long)value) == st__OUT_OF_MEM) {
                return(NULL);
            }
        }
        factors->g = h;
        factors->h = g;
    } else if (pairValue == PAIR_CR) {
        factors->g = h;
        factors->h = g;
    } else if (pairValue == PAIR_ST) {
        factors->g = g;
        factors->h = h;
    }
    if ( st__insert(cacheTable, (char *)node, (char *)factors) == st__OUT_OF_MEM) {
        ABC_FREE(factors);
        return(NULL);
    }
    return(factors);
}
static Conjuncts * CheckTablesCacheAndReturn ( DdNode * node , DdNode * g , DdNode * h , st__table * ghTable , st__table * cacheTable ) { int pairValue ; int value ; Conjuncts * factors ; value = 0 ; pairValue = PairInTables ( g , h , ghTable ) ; assert ( pairValue != NONE ) ; factors = ABC_ALLOC ( Conjuncts , 1 ) ; if ( factors == NULL ) return ( NULL ) ; if ( ( pairValue == BOTH_H ) || ( pairValue == H_ST ) ) { if ( g != one ) { value = 0 ; if ( st__lookup_int ( ghTable , ( char * ) Cudd_Regular ( g ) , & value ) ) { value |= 1 ; } else { value = 1 ; } if ( st__insert ( ghTable , ( char * ) Cudd_Regular ( g ) , ( char * ) ( long ) value ) == st__OUT_OF_MEM ) { return ( NULL ) ; } } factors -> g = g ; factors -> h = h ; } else if ( ( pairValue == BOTH_G ) || ( pairValue == G_ST ) ) { if ( h != one ) { value = 0 ; if ( st__lookup_int ( ghTable , ( char * ) Cudd_Regular ( h ) , & value ) ) { value |= 2 ; } else { value = 2 ; } if ( st__insert ( ghTable , ( char * ) Cudd_Regular ( h ) , ( char * ) ( long ) value ) == st__OUT_OF_MEM ) { return ( NULL ) ; } } factors -> g = g ; factors -> h = h ; } else if ( pairValue == H_CR ) { if ( g != one ) { value = 2 ; if ( st__insert ( ghTable , ( char * ) Cudd_Regular ( g ) , ( char * ) ( long ) value ) == st__OUT_OF_MEM ) { return ( NULL ) ; } } factors -> g = h ; factors -> h = g ; } else if ( pairValue == G_CR ) { if ( h != one ) { value = 1 ; if ( st__insert ( ghTable , ( char * ) Cudd_Regular ( h ) , ( char * ) ( long ) value ) == st__OUT_OF_MEM ) { return ( NULL ) ; } } factors -> g = h ; factors -> h = g ; } else if ( pairValue == PAIR_CR ) { factors -> g = h ; factors -> h = g ; } else if ( pairValue == PAIR_ST ) { factors -> g = g ; factors -> h = h ; } if ( st__insert ( cacheTable , ( char * ) node , ( char * ) factors ) == st__OUT_OF_MEM ) { ABC_FREE ( factors ) ; return ( NULL ) ; } return ( factors ) ; }
Function
Synopsis    [Check the tables for the existence of pair and return one
combination, cache the result.]
Function Synopsis [ Check the tables for the existence of pair and return one combination cache the result . ]
/* check tables */ /* if both dont exist in table, we know one exists(either g or h).
     * Therefore store the other and proceed
     */ /* pair exists in table */ /* cache the result for this node */