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

  Synopsis    [Builds the subset BDD using the heavy branch method.]

  Description [The procedure carries out the building of the subset BDD
  starting at the root. Using the three different counts labelling each node,
  the procedure chooses the heavier branch starting from the root and keeps
  track of the number of nodes it discards at each step, thus keeping count
  of the size of the subset BDD dynamically. Once the threshold is satisfied,
  the procedure then calls ITE to build the BDD.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
Function
Synopsis    [Builds the subset BDD using the heavy branch method.]

Description [The procedure carries out the building of the subset BDD
starting at the root. Using the three different counts labelling each node,
the procedure chooses the heavier branch starting from the root and keeps
track of the number of nodes it discards at each step, thus keeping count
of the size of the subset BDD dynamically. Once the threshold is satisfied,
the procedure then calls ITE to build the BDD.]




Function Synopsis [ Builds the subset BDD using the heavy branch method . ] Description [ The procedure carries out the building of the subset BDD starting at the root . Using the three different counts labelling each node the procedure chooses the heavier branch starting from the root and keeps track of the number of nodes it discards at each step thus keeping count of the size of the subset BDD dynamically . Once the threshold is satisfied the procedure then calls ITE to build the BDD . ]
static DdNode *
BuildSubsetBdd(
  DdManager * dd ,
  DdNode * node ,
  int * size ,
  st__table * visitedTable ,
  int  threshold,
  st__table * storeTable,
  st__table * approxTable)
{
    DdNode *Nv, *Nnv, *N, *topv, *neW;
    double minNv, minNnv;
    NodeData_t *currNodeQual;
    NodeData_t *currNodeQualT;
    NodeData_t *currNodeQualE;
    DdNode *ThenBranch, *ElseBranch;
    unsigned int topid;
    char *dummy;
#ifdef DEBUG
    num_calls++;
#endif
    if ((*size) <= threshold) {
      StoreNodes(storeTable, dd, node);
      return(node);
    }
    if (Cudd_IsConstant(node))
        return(node);
    if (! st__lookup(visitedTable, (const char *)node, (char **)&currNodeQual)) {
        fprintf(dd->err,
                "Something is wrong, ought to be in node quality table\n");
    }
    N = Cudd_Regular(node);
    Nv = Cudd_T(N);
    Nnv = Cudd_E(N);
    Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
    Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
    if (!Cudd_IsConstant(Nv)) {
        if (! st__lookup(visitedTable, (const char *)Nv, (char **)&currNodeQualT)) {
                fprintf(dd->out,"Something wrong, couldnt find nodes in node quality table\n");
                dd->errorCode = CUDD_INTERNAL_ERROR;
                return(NULL);
            }
        else {
            minNv = *(((NodeData_t *)currNodeQualT)->mintermPointer);
        }
    } else {
        if (Nv == zero) {
            minNv = 0;
        } else  {
            minNv = max;
        }
    }
    if (!Cudd_IsConstant(Nnv)) {
        if (! st__lookup(visitedTable, (const char *)Nnv, (char **)&currNodeQualE)) {
            fprintf(dd->out,"Something wrong, couldnt find nodes in node quality table\n");
            dd->errorCode = CUDD_INTERNAL_ERROR;
            return(NULL);
        } else {
            minNnv = *(((NodeData_t *)currNodeQualE)->mintermPointer);
        }
    } else {
        if (Nnv == zero) {
            minNnv = 0;
        } else {
            minNnv = max;
        }
    }
    *size = (*(size)) - (int)*(currNodeQual->lightChildNodesPointer);
    if (minNv >= minNnv) { 
        ThenBranch = (DdNode *)BuildSubsetBdd(dd, Nv, size,
              visitedTable, threshold, storeTable, approxTable);
        if (ThenBranch == NULL) {
            return(NULL);
        }
        cuddRef(ThenBranch);
        if ( st__lookup(storeTable, (char *)Cudd_Regular(Nnv), &dummy)) {
          ElseBranch = Nnv;
          cuddRef(ElseBranch);
        } else {
          if ( st__lookup(approxTable, (char *)Nnv, &dummy)) {
            ElseBranch = (DdNode *)dummy;
            cuddRef(ElseBranch);
          } else {
            ElseBranch = zero;
            cuddRef(ElseBranch);
          }
        }
    }
    else {
        ElseBranch = (DdNode *)BuildSubsetBdd(dd, Nnv, size,
                      visitedTable, threshold, storeTable, approxTable);
        if (ElseBranch == NULL) {
            return(NULL);
        }
        cuddRef(ElseBranch);
        if ( st__lookup(storeTable, (char *)Cudd_Regular(Nv), &dummy)) {
          ThenBranch = Nv;
          cuddRef(ThenBranch);
        } else {
          if ( st__lookup(approxTable, (char *)Nv, &dummy)) {
            ThenBranch = (DdNode *)dummy;
            cuddRef(ThenBranch);
          } else {
            ThenBranch = zero;
            cuddRef(ThenBranch);
          }
        }
    }
    topid = Cudd_NodeReadIndex(N);
    topv = Cudd_ReadVars(dd, topid);
    cuddRef(topv);
    neW =  cuddBddIteRecur(dd, topv, ThenBranch, ElseBranch);
    if (neW != NULL) {
      cuddRef(neW);
    }
    Cudd_RecursiveDeref(dd, topv);
    Cudd_RecursiveDeref(dd, ThenBranch);
    Cudd_RecursiveDeref(dd, ElseBranch);
    if (neW == NULL)
        return(NULL);
    else {
        if (! st__lookup(storeTable, (char *)Cudd_Regular(neW), &dummy)) {
          cuddRef(neW);
          if (! st__insert(storeTable, (char *)Cudd_Regular(neW), NIL(char)))
              return (NULL);
        }
        if (N !=  Cudd_Regular(neW)) {
            if ( st__lookup(approxTable, (char *)node, &dummy)) {
                fprintf(dd->err, "This node should not be in the approximated table\n");
            } else {
                cuddRef(neW);
                if (! st__insert(approxTable, (char *)node, (char *)neW))
                    return(NULL);
            }
        }
        cuddDeref(neW);
        return(neW);
    }
}
static DdNode * BuildSubsetBdd ( DdManager * dd , DdNode * node , int * size , st__table * visitedTable , int threshold , st__table * storeTable , st__table * approxTable ) { DdNode * Nv , * Nnv , * N , * topv , * neW ; double minNv , minNnv ; NodeData_t * currNodeQual ; NodeData_t * currNodeQualT ; NodeData_t * currNodeQualE ; DdNode * ThenBranch , * ElseBranch ; unsigned int topid ; char * dummy ; #ifdef DEBUG num_calls ++ ; #endif if ( ( * size ) <= threshold ) { StoreNodes ( storeTable , dd , node ) ; return ( node ) ; } if ( Cudd_IsConstant ( node ) ) return ( node ) ; if ( ! st__lookup ( visitedTable , ( const char * ) node , ( char * * ) & currNodeQual ) ) { fprintf ( dd -> err , " \n " ) ; } N = Cudd_Regular ( node ) ; Nv = Cudd_T ( N ) ; Nnv = Cudd_E ( N ) ; Nv = Cudd_NotCond ( Nv , Cudd_IsComplement ( node ) ) ; Nnv = Cudd_NotCond ( Nnv , Cudd_IsComplement ( node ) ) ; if ( ! Cudd_IsConstant ( Nv ) ) { if ( ! st__lookup ( visitedTable , ( const char * ) Nv , ( char * * ) & currNodeQualT ) ) { fprintf ( dd -> out , " \n " ) ; dd -> errorCode = CUDD_INTERNAL_ERROR ; return ( NULL ) ; } else { minNv = * ( ( ( NodeData_t * ) currNodeQualT ) -> mintermPointer ) ; } } else { if ( Nv == zero ) { minNv = 0 ; } else { minNv = max ; } } if ( ! Cudd_IsConstant ( Nnv ) ) { if ( ! st__lookup ( visitedTable , ( const char * ) Nnv , ( char * * ) & currNodeQualE ) ) { fprintf ( dd -> out , " \n " ) ; dd -> errorCode = CUDD_INTERNAL_ERROR ; return ( NULL ) ; } else { minNnv = * ( ( ( NodeData_t * ) currNodeQualE ) -> mintermPointer ) ; } } else { if ( Nnv == zero ) { minNnv = 0 ; } else { minNnv = max ; } } * size = ( * ( size ) ) - ( int ) * ( currNodeQual -> lightChildNodesPointer ) ; if ( minNv >= minNnv ) { ThenBranch = ( DdNode * ) BuildSubsetBdd ( dd , Nv , size , visitedTable , threshold , storeTable , approxTable ) ; if ( ThenBranch == NULL ) { return ( NULL ) ; } cuddRef ( ThenBranch ) ; if ( st__lookup ( storeTable , ( char * ) Cudd_Regular ( Nnv ) , & dummy ) ) { ElseBranch = Nnv ; cuddRef ( ElseBranch ) ; } else { if ( st__lookup ( approxTable , ( char * ) Nnv , & dummy ) ) { ElseBranch = ( DdNode * ) dummy ; cuddRef ( ElseBranch ) ; } else { ElseBranch = zero ; cuddRef ( ElseBranch ) ; } } } else { ElseBranch = ( DdNode * ) BuildSubsetBdd ( dd , Nnv , size , visitedTable , threshold , storeTable , approxTable ) ; if ( ElseBranch == NULL ) { return ( NULL ) ; } cuddRef ( ElseBranch ) ; if ( st__lookup ( storeTable , ( char * ) Cudd_Regular ( Nv ) , & dummy ) ) { ThenBranch = Nv ; cuddRef ( ThenBranch ) ; } else { if ( st__lookup ( approxTable , ( char * ) Nv , & dummy ) ) { ThenBranch = ( DdNode * ) dummy ; cuddRef ( ThenBranch ) ; } else { ThenBranch = zero ; cuddRef ( ThenBranch ) ; } } } topid = Cudd_NodeReadIndex ( N ) ; topv = Cudd_ReadVars ( dd , topid ) ; cuddRef ( topv ) ; neW = cuddBddIteRecur ( dd , topv , ThenBranch , ElseBranch ) ; if ( neW != NULL ) { cuddRef ( neW ) ; } Cudd_RecursiveDeref ( dd , topv ) ; Cudd_RecursiveDeref ( dd , ThenBranch ) ; Cudd_RecursiveDeref ( dd , ElseBranch ) ; if ( neW == NULL ) return ( NULL ) ; else { if ( ! st__lookup ( storeTable , ( char * ) Cudd_Regular ( neW ) , & dummy ) ) { cuddRef ( neW ) ; if ( ! st__insert ( storeTable , ( char * ) Cudd_Regular ( neW ) , NIL ( char ) ) ) return ( NULL ) ; } if ( N != Cudd_Regular ( neW ) ) { if ( st__lookup ( approxTable , ( char * ) node , & dummy ) ) { fprintf ( dd -> err , " \n " ) ; } else { cuddRef ( neW ) ; if ( ! st__insert ( approxTable , ( char * ) node , ( char * ) neW ) ) return ( NULL ) ; } } cuddDeref ( neW ) ; return ( neW ) ; } }
Function
Synopsis    [Builds the subset BDD using the heavy branch method.]
Function Synopsis [ Builds the subset BDD using the heavy branch method . ]
/* DD manager */ /* current node */ /* current size of the subset */ /* visited table storing all node data */ /*If the size of the subset is below the threshold, dont do
      anything. */ /* store nodes below this, so we can recombine if possible */ /* Look up minterm count for this node. */ /* Get children. */ /* complement if necessary */ /* find out minterms and nodes contributed by then child */ /* find out minterms and nodes contributed by else child */ /* keep track of size of subset by subtracting the number of
     * differential nodes contributed by lighter child
     */ /*SubsetCountNodesAux procedure takes
                             the Then branch in case of a tie */ /* recur with the Then branch */ /* The Else branch is either a node that already exists in the
         * subset, or one whose approximation has been computed, or
         * Zero.
         */ /* recur with the Else branch */ /* The Then branch is either a node that already exists in the
         * subset, or one whose approximation has been computed, or
         * Zero.
         */ /* construct the Bdd with the top variable and the two children */ /* store this node in the store table */ /* store the approximation for this node */