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

  Synopsis    [The main procedure that returns a subset by choosing the heavier
  branch in the BDD.]

  Description [Here a subset BDD is built by throwing away one of the
  children. Starting at root, annotate each node with the number of
  minterms (in terms of the total number of variables specified -
  numVars), number of nodes taken by the DAG rooted at this node and
  number of additional nodes taken by the child that has the lesser
  minterms. The child with the lower number of minterms is thrown away
  and a dyanmic count of the nodes of the subset is kept. Once the
  threshold is reached the subset is returned to the calling
  procedure.]

  SideEffects [None]

  SeeAlso     [Cudd_SubsetHeavyBranch]

******************************************************************************/
Function
Synopsis    [The main procedure that returns a subset by choosing the heavier
branch in the BDD.]

Description [Here a subset BDD is built by throwing away one of the
children. Starting at root, annotate each node with the number of
minterms (in terms of the total number of variables specified
numVars), number of nodes taken by the DAG rooted at this node and
number of additional nodes taken by the child that has the lesser
minterms. The child with the lower number of minterms is thrown away
and a dyanmic count of the nodes of the subset is kept. Once the
threshold is reached the subset is returned to the calling
procedure.]




Function Synopsis [ The main procedure that returns a subset by choosing the heavier branch in the BDD . ] Description [ Here a subset BDD is built by throwing away one of the children . Starting at root annotate each node with the number of minterms ( in terms of the total number of variables specified numVars ) number of nodes taken by the DAG rooted at this node and number of additional nodes taken by the child that has the lesser minterms . The child with the lower number of minterms is thrown away and a dyanmic count of the nodes of the subset is kept . Once the threshold is reached the subset is returned to the calling procedure . ]
DdNode *
cuddSubsetHeavyBranch(
  DdManager * dd ,
  DdNode * f ,
  int  numVars ,
  int  threshold )
{
    int i, *size;
    st__table *visitedTable;
    int numNodes;
    NodeData_t *currNodeQual;
    DdNode *subset;
    st__table *storeTable, *approxTable;
    char *key, *value;
    st__generator *stGen;
    if (f == NULL) {
        fprintf(dd->err, "Cannot subset, nil object\n");
        dd->errorCode = CUDD_INVALID_ARG;
        return(NULL);
    }
    one  = Cudd_ReadOne(dd);
    zero = Cudd_Not(one);
    if (numVars == 0) {
        numVars = DBL_MAX_EXP - 1;
    }
    if (Cudd_IsConstant(f)) {
        return(f);
    }
    max = pow(2.0, (double)numVars);
    visitedTable = SubsetCountMinterm(f, numVars);
    if ((visitedTable == NULL) || memOut) {
        (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
        dd->errorCode = CUDD_MEMORY_OUT;
        return(0);
    }
    numNodes = SubsetCountNodes(f, visitedTable, numVars);
    if (memOut) {
        (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
        dd->errorCode = CUDD_MEMORY_OUT;
        return(0);
    }
    if ( st__lookup(visitedTable, (const char *)f, (char **)&currNodeQual) == 0) {
        fprintf(dd->err,
                "Something is wrong, ought to be node quality table\n");
        dd->errorCode = CUDD_INTERNAL_ERROR;
    }
    size = ABC_ALLOC(int, 1);
    if (size == NULL) {
        dd->errorCode = CUDD_MEMORY_OUT;
        return(NULL);
    }
    *size = numNodes;
#ifdef DEBUG
    num_calls = 0;
#endif
    storeTable = st__init_table( st__ptrcmp, st__ptrhash);
    cuddRef(one);
    if ( st__insert(storeTable, (char *)Cudd_ReadOne(dd), NIL(char)) ==
        st__OUT_OF_MEM) {
        fprintf(dd->out, "Something wrong, st__table insert failed\n");
    }
    approxTable = st__init_table( st__ptrcmp, st__ptrhash);
    subset = (DdNode *)BuildSubsetBdd(dd, f, size, visitedTable, threshold,
                                      storeTable, approxTable);
    if (subset != NULL) {
        cuddRef(subset);
    }
    stGen = st__init_gen(approxTable);
    if (stGen == NULL) {
        st__free_table(approxTable);
        return(NULL);
    }
    while( st__gen(stGen, (const char **)&key, (char **)&value)) {
        Cudd_RecursiveDeref(dd, (DdNode *)value);
    }
    st__free_gen(stGen); stGen = NULL;
    st__free_table(approxTable);
    stGen = st__init_gen(storeTable);
    if (stGen == NULL) {
        st__free_table(storeTable);
        return(NULL);
    }
    while( st__gen(stGen, (const char **)&key, (char **)&value)) {
        Cudd_RecursiveDeref(dd, (DdNode *)key);
    }
    st__free_gen(stGen); stGen = NULL;
    st__free_table(storeTable);
    for (i = 0; i <= page; i++) {
        ABC_FREE(mintermPages[i]);
    }
    ABC_FREE(mintermPages);
    for (i = 0; i <= page; i++) {
        ABC_FREE(nodePages[i]);
    }
    ABC_FREE(nodePages);
    for (i = 0; i <= page; i++) {
        ABC_FREE(lightNodePages[i]);
    }
    ABC_FREE(lightNodePages);
    for (i = 0; i <= nodeDataPage; i++) {
        ABC_FREE(nodeDataPages[i]);
    }
    ABC_FREE(nodeDataPages);
    st__free_table(visitedTable);
    ABC_FREE(size);
#if 0
    (void) Cudd_DebugCheck(dd);
    (void) Cudd_CheckKeys(dd);
#endif
    if (subset != NULL) {
#ifdef DD_DEBUG
      if (!Cudd_bddLeq(dd, subset, f)) {
            fprintf(dd->err, "Wrong subset\n");
            dd->errorCode = CUDD_INTERNAL_ERROR;
            return(NULL);
      }
#endif
        cuddDeref(subset);
        return(subset);
    } else {
        return(NULL);
    }
}
DdNode * cuddSubsetHeavyBranch ( DdManager * dd , DdNode * f , int numVars , int threshold ) { int i , * size ; st__table * visitedTable ; int numNodes ; NodeData_t * currNodeQual ; DdNode * subset ; st__table * storeTable , * approxTable ; char * key , * value ; st__generator * stGen ; if ( f == NULL ) { fprintf ( dd -> err , " \n " ) ; dd -> errorCode = CUDD_INVALID_ARG ; return ( NULL ) ; } one = Cudd_ReadOne ( dd ) ; zero = Cudd_Not ( one ) ; if ( numVars == 0 ) { numVars = DBL_MAX_EXP - 1 ; } if ( Cudd_IsConstant ( f ) ) { return ( f ) ; } max = pow ( 2.0 , ( double ) numVars ) ; visitedTable = SubsetCountMinterm ( f , numVars ) ; if ( ( visitedTable == NULL ) || memOut ) { ( void ) fprintf ( dd -> err , " \n " ) ; dd -> errorCode = CUDD_MEMORY_OUT ; return ( 0 ) ; } numNodes = SubsetCountNodes ( f , visitedTable , numVars ) ; if ( memOut ) { ( void ) fprintf ( dd -> err , " \n " ) ; dd -> errorCode = CUDD_MEMORY_OUT ; return ( 0 ) ; } if ( st__lookup ( visitedTable , ( const char * ) f , ( char * * ) & currNodeQual ) == 0 ) { fprintf ( dd -> err , " \n " ) ; dd -> errorCode = CUDD_INTERNAL_ERROR ; } size = ABC_ALLOC ( int , 1 ) ; if ( size == NULL ) { dd -> errorCode = CUDD_MEMORY_OUT ; return ( NULL ) ; } * size = numNodes ; #ifdef DEBUG num_calls = 0 ; #endif storeTable = st__init_table ( st__ptrcmp , st__ptrhash ) ; cuddRef ( one ) ; if ( st__insert ( storeTable , ( char * ) Cudd_ReadOne ( dd ) , NIL ( char ) ) == st__OUT_OF_MEM ) { fprintf ( dd -> out , " \n " ) ; } approxTable = st__init_table ( st__ptrcmp , st__ptrhash ) ; subset = ( DdNode * ) BuildSubsetBdd ( dd , f , size , visitedTable , threshold , storeTable , approxTable ) ; if ( subset != NULL ) { cuddRef ( subset ) ; } stGen = st__init_gen ( approxTable ) ; if ( stGen == NULL ) { st__free_table ( approxTable ) ; return ( NULL ) ; } while ( st__gen ( stGen , ( const char * * ) & key , ( char * * ) & value ) ) { Cudd_RecursiveDeref ( dd , ( DdNode * ) value ) ; } st__free_gen ( stGen ) ; stGen = NULL ; st__free_table ( approxTable ) ; stGen = st__init_gen ( storeTable ) ; if ( stGen == NULL ) { st__free_table ( storeTable ) ; return ( NULL ) ; } while ( st__gen ( stGen , ( const char * * ) & key , ( char * * ) & value ) ) { Cudd_RecursiveDeref ( dd , ( DdNode * ) key ) ; } st__free_gen ( stGen ) ; stGen = NULL ; st__free_table ( storeTable ) ; for ( i = 0 ; i <= page ; i ++ ) { ABC_FREE ( mintermPages [ i ] ) ; } ABC_FREE ( mintermPages ) ; for ( i = 0 ; i <= page ; i ++ ) { ABC_FREE ( nodePages [ i ] ) ; } ABC_FREE ( nodePages ) ; for ( i = 0 ; i <= page ; i ++ ) { ABC_FREE ( lightNodePages [ i ] ) ; } ABC_FREE ( lightNodePages ) ; for ( i = 0 ; i <= nodeDataPage ; i ++ ) { ABC_FREE ( nodeDataPages [ i ] ) ; } ABC_FREE ( nodeDataPages ) ; st__free_table ( visitedTable ) ; ABC_FREE ( size ) ; #if 0 ( void ) Cudd_DebugCheck ( dd ) ; ( void ) Cudd_CheckKeys ( dd ) ; #endif if ( subset != NULL ) { #ifdef DD_DEBUG if ( ! Cudd_bddLeq ( dd , subset , f ) ) { fprintf ( dd -> err , " \n " ) ; dd -> errorCode = CUDD_INTERNAL_ERROR ; return ( NULL ) ; } #endif cuddDeref ( subset ) ; return ( subset ) ; } else { return ( NULL ) ; } }
Function
Synopsis    [The main procedure that returns a subset by choosing the heavier
branch in the BDD.]
Function Synopsis [ The main procedure that returns a subset by choosing the heavier branch in the BDD . ]
/* DD manager */ /* current DD */ /* maximum number of variables */ /* threshold size for the subset */ /* If user does not know numVars value, set it to the maximum
     * exponent that the pow function can take. The -1 is due to the
     * discrepancy in the value that pow takes and the value that
     * log gives.
     */ /* set default value */ /* Create visited table where structures for node data are allocated and
       stored in a st__table */ /* table to store nodes being created. */ /* insert the constant */ /* table to store approximations of nodes */