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

  Synopsis    [Recursively counts the number of nodes under the dag.
  Also counts the number of nodes under the lighter child of
  this node.]

  Description [Recursively counts the number of nodes under the dag.
  Also counts the number of nodes under the lighter child of
  this node. . Note that the same dag may be the lighter child of two
  different nodes and have different counts. As with the minterm counts,
  the node counts are stored in pages to be space efficient and the
  address for these node counts are stored in an st__table associated
  to each node. ]

  SideEffects [Updates the node data table with node counts]

  SeeAlso     [SubsetCountNodes]

******************************************************************************/
Function
Synopsis    [Recursively counts the number of nodes under the dag.
Also counts the number of nodes under the lighter child of
this node.]

Description [Recursively counts the number of nodes under the dag.
Also counts the number of nodes under the lighter child of
this node.

SideEffects [Updates the node data table with node counts]


Function Synopsis [ Recursively counts the number of nodes under the dag . Also counts the number of nodes under the lighter child of this node . ] Description [ Recursively counts the number of nodes under the dag . Also counts the number of nodes under the lighter child of this node . SideEffects [ Updates the node data table with node counts ]
static int
SubsetCountNodesAux(
  DdNode * node ,
  st__table * table ,
  double  max )
{
    int tval, eval, i;
    DdNode *N, *Nv, *Nnv;
    double minNv, minNnv;
    NodeData_t *dummyN, *dummyNv, *dummyNnv, *dummyNBar;
    int *pmin, *pminBar, *val;
    if ((node == NULL) || Cudd_IsConstant(node))
        return(0);
    if ( st__lookup(table, (const char *)node, (char **)&dummyN) == 1) {
        val = dummyN->nodesPointer;
        if (val != NULL)
            return(0);
    } else {
        return(0);
    }
    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 (Nv == zero) {
            minNv = 0.0;
        } else {
            minNv = max;
        }
    } else {
        if ( st__lookup(table, (const char *)Nv, (char **)&dummyNv) == 1)
            minNv = *(dummyNv->mintermPointer);
        else {
            return(0);
        }
    }
    if (Cudd_IsConstant(Nnv)) {
        if (Nnv == zero) {
            minNnv = 0.0;
        } else {
            minNnv = max;
        }
    } else {
        if ( st__lookup(table, (const char *)Nnv, (char **)&dummyNnv) == 1) {
            minNnv = *(dummyNnv->mintermPointer);
        }
        else {
            return(0);
        }
    }
    if (minNv >= minNnv) {
        tval = SubsetCountNodesAux(Nv, table, max);
        if (memOut) return(0);
        eval = SubsetCountNodesAux(Nnv, table, max);
        if (memOut) return(0);
        if (pageIndex == pageSize) ResizeCountNodePages();
        if (memOut) {
            for (i = 0; i <= page; i++) ABC_FREE(mintermPages[i]);
            ABC_FREE(mintermPages);
            for (i = 0; i <= nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
            ABC_FREE(nodeDataPages);
            st__free_table(table);
            return(0);
        }
        pmin = currentLightNodePage + pageIndex;
        *pmin = eval; 
        dummyN->lightChildNodesPointer = pmin;
    } else {
        eval = SubsetCountNodesAux(Nnv, table, max);
        if (memOut) return(0);
        tval = SubsetCountNodesAux(Nv, table, max);
        if (memOut) return(0);
        if (pageIndex == pageSize) ResizeCountNodePages();
        if (memOut) {
            for (i = 0; i <= page; i++) ABC_FREE(mintermPages[i]);
            ABC_FREE(mintermPages);
            for (i = 0; i <= nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
            ABC_FREE(nodeDataPages);
            st__free_table(table);
            return(0);
        }
        pmin = currentLightNodePage + pageIndex;
        *pmin = tval; 
        dummyN->lightChildNodesPointer = pmin;
    }
    pmin = currentNodePage + pageIndex;
    *pmin = tval + eval + 1;
    dummyN->nodesPointer = pmin;
    pageIndex++;
    if ( st__lookup(table, (const char *)Cudd_Not(node), (char **)&dummyNBar) == 1)  {
        if (pageIndex == pageSize) ResizeCountNodePages();
        if (memOut) {
            for (i = 0; i < page; i++) ABC_FREE(mintermPages[i]);
            ABC_FREE(mintermPages);
            for (i = 0; i < nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
            ABC_FREE(nodeDataPages);
            st__free_table(table);
            return(0);
        }
        pminBar = currentLightNodePage + pageIndex;
        *pminBar = 0;
        dummyNBar->lightChildNodesPointer = pminBar;
        if (pageIndex == pageSize) ResizeCountNodePages();
        if (memOut) {
            for (i = 0; i < page; i++) ABC_FREE(mintermPages[i]);
            ABC_FREE(mintermPages);
            for (i = 0; i < nodeDataPage; i++) ABC_FREE(nodeDataPages[i]);
            ABC_FREE(nodeDataPages);
            st__free_table(table);
            return(0);
        }
        pminBar = currentNodePage + pageIndex;
        *pminBar = 0;
        dummyNBar->nodesPointer = pminBar ; 
        pageIndex++;
    }
    return(*pmin);
}
static int SubsetCountNodesAux ( DdNode * node , st__table * table , double max ) { int tval , eval , i ; DdNode * N , * Nv , * Nnv ; double minNv , minNnv ; NodeData_t * dummyN , * dummyNv , * dummyNnv , * dummyNBar ; int * pmin , * pminBar , * val ; if ( ( node == NULL ) || Cudd_IsConstant ( node ) ) return ( 0 ) ; if ( st__lookup ( table , ( const char * ) node , ( char * * ) & dummyN ) == 1 ) { val = dummyN -> nodesPointer ; if ( val != NULL ) return ( 0 ) ; } else { return ( 0 ) ; } 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 ( Nv == zero ) { minNv = 0.0 ; } else { minNv = max ; } } else { if ( st__lookup ( table , ( const char * ) Nv , ( char * * ) & dummyNv ) == 1 ) minNv = * ( dummyNv -> mintermPointer ) ; else { return ( 0 ) ; } } if ( Cudd_IsConstant ( Nnv ) ) { if ( Nnv == zero ) { minNnv = 0.0 ; } else { minNnv = max ; } } else { if ( st__lookup ( table , ( const char * ) Nnv , ( char * * ) & dummyNnv ) == 1 ) { minNnv = * ( dummyNnv -> mintermPointer ) ; } else { return ( 0 ) ; } } if ( minNv >= minNnv ) { tval = SubsetCountNodesAux ( Nv , table , max ) ; if ( memOut ) return ( 0 ) ; eval = SubsetCountNodesAux ( Nnv , table , max ) ; if ( memOut ) return ( 0 ) ; if ( pageIndex == pageSize ) ResizeCountNodePages ( ) ; if ( memOut ) { for ( i = 0 ; i <= page ; i ++ ) ABC_FREE ( mintermPages [ i ] ) ; ABC_FREE ( mintermPages ) ; for ( i = 0 ; i <= nodeDataPage ; i ++ ) ABC_FREE ( nodeDataPages [ i ] ) ; ABC_FREE ( nodeDataPages ) ; st__free_table ( table ) ; return ( 0 ) ; } pmin = currentLightNodePage + pageIndex ; * pmin = eval ; dummyN -> lightChildNodesPointer = pmin ; } else { eval = SubsetCountNodesAux ( Nnv , table , max ) ; if ( memOut ) return ( 0 ) ; tval = SubsetCountNodesAux ( Nv , table , max ) ; if ( memOut ) return ( 0 ) ; if ( pageIndex == pageSize ) ResizeCountNodePages ( ) ; if ( memOut ) { for ( i = 0 ; i <= page ; i ++ ) ABC_FREE ( mintermPages [ i ] ) ; ABC_FREE ( mintermPages ) ; for ( i = 0 ; i <= nodeDataPage ; i ++ ) ABC_FREE ( nodeDataPages [ i ] ) ; ABC_FREE ( nodeDataPages ) ; st__free_table ( table ) ; return ( 0 ) ; } pmin = currentLightNodePage + pageIndex ; * pmin = tval ; dummyN -> lightChildNodesPointer = pmin ; } pmin = currentNodePage + pageIndex ; * pmin = tval + eval + 1 ; dummyN -> nodesPointer = pmin ; pageIndex ++ ; if ( st__lookup ( table , ( const char * ) Cudd_Not ( node ) , ( char * * ) & dummyNBar ) == 1 ) { if ( pageIndex == pageSize ) ResizeCountNodePages ( ) ; if ( memOut ) { for ( i = 0 ; i < page ; i ++ ) ABC_FREE ( mintermPages [ i ] ) ; ABC_FREE ( mintermPages ) ; for ( i = 0 ; i < nodeDataPage ; i ++ ) ABC_FREE ( nodeDataPages [ i ] ) ; ABC_FREE ( nodeDataPages ) ; st__free_table ( table ) ; return ( 0 ) ; } pminBar = currentLightNodePage + pageIndex ; * pminBar = 0 ; dummyNBar -> lightChildNodesPointer = pminBar ; if ( pageIndex == pageSize ) ResizeCountNodePages ( ) ; if ( memOut ) { for ( i = 0 ; i < page ; i ++ ) ABC_FREE ( mintermPages [ i ] ) ; ABC_FREE ( mintermPages ) ; for ( i = 0 ; i < nodeDataPage ; i ++ ) ABC_FREE ( nodeDataPages [ i ] ) ; ABC_FREE ( nodeDataPages ) ; st__free_table ( table ) ; return ( 0 ) ; } pminBar = currentNodePage + pageIndex ; * pminBar = 0 ; dummyNBar -> nodesPointer = pminBar ; pageIndex ++ ; } return ( * pmin ) ; }
Function
Synopsis    [Recursively counts the number of nodes under the dag.
Function Synopsis [ Recursively counts the number of nodes under the dag .
/* current node */ /* table to update node count, also serves as visited table. */ /* maximum number of variables */ /* if this node has been processed do nothing */ /* find the minterm counts for the THEN and ELSE branches */ /* recur based on which has larger minterm, */ /* store the node count of the lighter child. */ /* Here the ELSE child is lighter */ /* store the node count of the lighter child. */ /* Here the THEN child is lighter */ /* updating the page index for node count storage. */ /* pageIndex is parallel page index for count_nodes and count_lightNodes */ /* if this node has been reached first, it belongs to a heavier
       branch. Its complement will be reached later on a lighter branch.
       Hence the complement has zero node count. */ /* The lighter child has less nodes than the parent.
         * So if parent 0 then lighter child zero
         */ /* maybe should point to zero */