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

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

  Description [Check the tables for the existence of pair and return
  one combination, store in cache. The pair that has more pointers to
  it is picked. An approximation of the number of local pointers is
  made by taking the reference count of the pairs sent. ]

  SideEffects []

  SeeAlso     [ZeroCase BuildConjuncts]

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

Description [Check the tables for the existence of pair and return
one combination, store in cache. The pair that has more pointers to
it is picked. An approximation of the number of local pointers is
made by taking the reference count of the pairs sent.




Function Synopsis [ Check the tables for the existence of pair and return one combination store in cache . ] Description [ Check the tables for the existence of pair and return one combination store in cache . The pair that has more pointers to it is picked . An approximation of the number of local pointers is made by taking the reference count of the pairs sent .
static Conjuncts *
PickOnePair(
  DdNode * node,
  DdNode * g1,
  DdNode * h1,
  DdNode * g2,
  DdNode * h2,
  st__table * ghTable,
  st__table * cacheTable)
{
    int value;
    Conjuncts *factors;
    int oneRef, twoRef;
    factors = ABC_ALLOC(Conjuncts, 1);
    if (factors == NULL) return(NULL);
    if (h2 == one) {
        twoRef = (Cudd_Regular(g2))->ref;
    } else if (g2 == one) {
        twoRef = (Cudd_Regular(h2))->ref;
    } else {
        twoRef = ((Cudd_Regular(g2))->ref + (Cudd_Regular(h2))->ref)/2;
    }
    if (h1 == one) {
        oneRef  = (Cudd_Regular(g1))->ref;
    } else if (g1 == one) {
        oneRef  = (Cudd_Regular(h1))->ref;
    } else {
        oneRef = ((Cudd_Regular(g1))->ref + (Cudd_Regular(h1))->ref)/2;
    }
    if (oneRef >= twoRef) {
        factors->g = g1;
        factors->h = h1;
    } else {
        factors->g = g2;
        factors->h = h2;
    }
    if (factors->g != one) {
        value = 0;
        if ( st__lookup_int(ghTable, (char *)Cudd_Regular(factors->g), &value)) {
            if (value == 2) {
                value |= 1;
                if ( st__insert(ghTable, (char *)Cudd_Regular(factors->g),
                              (char *)(long)value) == st__OUT_OF_MEM) {
                    ABC_FREE(factors);
                    return(NULL);
                }
            }
        } else {
            value = 1;
            if ( st__insert(ghTable, (char *)Cudd_Regular(factors->g),
                          (char *)(long)value) == st__OUT_OF_MEM) {
                ABC_FREE(factors);
                return(NULL);
            }
        }
    }
    if (factors->h != one) {
        value = 0;
        if ( st__lookup_int(ghTable, (char *)Cudd_Regular(factors->h), &value)) {
            if (value == 1) {
                value |= 2;
                if ( st__insert(ghTable, (char *)Cudd_Regular(factors->h),
                              (char *)(long)value) == st__OUT_OF_MEM) {
                    ABC_FREE(factors);
                    return(NULL);
                }
            }       
        } else {
            value = 2;
            if ( st__insert(ghTable, (char *)Cudd_Regular(factors->h),
                          (char *)(long)value) == st__OUT_OF_MEM) {
                ABC_FREE(factors);
                return(NULL);
            }
        }
    }
    if ( st__insert(cacheTable, (char *)node, (char *)factors) ==
            st__OUT_OF_MEM) {
        ABC_FREE(factors);
        return(NULL);
    }
    return(factors);
}
static Conjuncts * PickOnePair ( DdNode * node , DdNode * g1 , DdNode * h1 , DdNode * g2 , DdNode * h2 , st__table * ghTable , st__table * cacheTable ) { int value ; Conjuncts * factors ; int oneRef , twoRef ; factors = ABC_ALLOC ( Conjuncts , 1 ) ; if ( factors == NULL ) return ( NULL ) ; if ( h2 == one ) { twoRef = ( Cudd_Regular ( g2 ) ) -> ref ; } else if ( g2 == one ) { twoRef = ( Cudd_Regular ( h2 ) ) -> ref ; } else { twoRef = ( ( Cudd_Regular ( g2 ) ) -> ref + ( Cudd_Regular ( h2 ) ) -> ref ) / 2 ; } if ( h1 == one ) { oneRef = ( Cudd_Regular ( g1 ) ) -> ref ; } else if ( g1 == one ) { oneRef = ( Cudd_Regular ( h1 ) ) -> ref ; } else { oneRef = ( ( Cudd_Regular ( g1 ) ) -> ref + ( Cudd_Regular ( h1 ) ) -> ref ) / 2 ; } if ( oneRef >= twoRef ) { factors -> g = g1 ; factors -> h = h1 ; } else { factors -> g = g2 ; factors -> h = h2 ; } if ( factors -> g != one ) { value = 0 ; if ( st__lookup_int ( ghTable , ( char * ) Cudd_Regular ( factors -> g ) , & value ) ) { if ( value == 2 ) { value |= 1 ; if ( st__insert ( ghTable , ( char * ) Cudd_Regular ( factors -> g ) , ( char * ) ( long ) value ) == st__OUT_OF_MEM ) { ABC_FREE ( factors ) ; return ( NULL ) ; } } } else { value = 1 ; if ( st__insert ( ghTable , ( char * ) Cudd_Regular ( factors -> g ) , ( char * ) ( long ) value ) == st__OUT_OF_MEM ) { ABC_FREE ( factors ) ; return ( NULL ) ; } } } if ( factors -> h != one ) { value = 0 ; if ( st__lookup_int ( ghTable , ( char * ) Cudd_Regular ( factors -> h ) , & value ) ) { if ( value == 1 ) { value |= 2 ; if ( st__insert ( ghTable , ( char * ) Cudd_Regular ( factors -> h ) , ( char * ) ( long ) value ) == st__OUT_OF_MEM ) { ABC_FREE ( factors ) ; return ( NULL ) ; } } } else { value = 2 ; if ( st__insert ( ghTable , ( char * ) Cudd_Regular ( factors -> h ) , ( char * ) ( long ) value ) == st__OUT_OF_MEM ) { ABC_FREE ( factors ) ; return ( NULL ) ; } } } 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, store in cache.]
Function Synopsis [ Check the tables for the existence of pair and return one combination store in cache . ]
/* count the number of pointers to pair 2 */ /* count the number of pointers to pair 1 */ /* pick the pair with higher reference count */ /*
     * Store computed factors in respective tables to encourage
     * recombination.
     */ /* insert g in htable */ /* insert h in htable */ /* Store factors in cache table for later use. */