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

  Synopsis    [ Labels each node with the shortest distance from the constant.]

  Description [Labels each node with the shortest distance from the constant.
  This is done in a DFS search of the BDD. Each node has an odd
  and even parity distance from the sink (since there exists paths to both
  zero and one) which is less than MAXSHORTINT. At each node these distances
  are updated using the minimum distance of its children from the constant.
  SInce now both the length from the root and child is known, the minimum path
  length(length of the shortest path between the root and the constant that
  this node lies on) of this node can be calculated and used to update the
  pathLengthArray]

  SideEffects [Updates Path Table and path length array]

  SeeAlso     [CreatePathTable CreateTopDist AssessPathLength]

******************************************************************************/
Function
Synopsis    [ Labels each node with the shortest distance from the constant.]

Description [Labels each node with the shortest distance from the constant.
This is done in a DFS search of the BDD. Each node has an odd
and even parity distance from the sink (since there exists paths to both
zero and one) which is less than MAXSHORTINT. At each node these distances
are updated using the minimum distance of its children from the constant.
SInce now both the length from the root and child is known, the minimum path
length(length of the shortest path between the root and the constant that
this node lies on) of this node can be calculated and used to update the
pathLengthArray]

SideEffects [Updates Path Table and path length array]


Function Synopsis [ Labels each node with the shortest distance from the constant . ] Description [ Labels each node with the shortest distance from the constant . This is done in a DFS search of the BDD . Each node has an odd and even parity distance from the sink ( since there exists paths to both zero and one ) which is less than MAXSHORTINT . At each node these distances are updated using the minimum distance of its children from the constant . SInce now both the length from the root and child is known the minimum path length ( length of the shortest path between the root and the constant that this node lies on ) of this node can be calculated and used to update the pathLengthArray ] SideEffects [ Updates Path Table and path length array ]
static int
CreateBotDist(
  DdNode * node ,
  st__table * pathTable ,
  unsigned int * pathLengthArray ,
  FILE *fp )
{
    DdNode *N, *Nv, *Nnv;
    DdNode *realChild;
    DdNode *child, *regChild;
    NodeDist_t *nodeStat, *nodeStatChild;
    unsigned int  oddLen, evenLen, pathLength;
    DdHalfWord botDist;
    int processingDone;
    if (Cudd_IsConstant(node))
        return(1);
    N = Cudd_Regular(node);
    if (! st__lookup(pathTable, (const char *)N, (char **)&nodeStat)) {
        fprintf(fp, "Something wrong, the entry doesn't exist\n");
        return(0);
    }
    if ((nodeStat->oddTopDist != MAXSHORTINT) &&
        (nodeStat->oddBotDist != MAXSHORTINT))
        oddLen = (nodeStat->oddTopDist + nodeStat->oddBotDist);
    else
        oddLen = MAXSHORTINT;
    if (!((nodeStat->evenTopDist == MAXSHORTINT) ||
          (nodeStat->evenBotDist == MAXSHORTINT)))
        evenLen = (nodeStat->evenTopDist +nodeStat->evenBotDist);
    else
        evenLen = MAXSHORTINT;
    pathLength = (oddLen <= evenLen) ? oddLen : evenLen;
    Nv = Cudd_T(N);
    Nnv = Cudd_E(N);
    processingDone = 0;
    while (processingDone != 2) {
        if (!processingDone) {
            child = Nv;
        } else {
            child = Nnv;
        }
        realChild = Cudd_NotCond(child, Cudd_IsComplement(node));
        regChild = Cudd_Regular(child);
        if (Cudd_IsConstant(realChild)) {
            if (Cudd_IsComplement(child))
                nodeStat->oddBotDist = 1;
            else
                nodeStat->evenBotDist = 1;
        } else {
            if (! st__lookup(pathTable, (const char *)regChild, (char **)&nodeStatChild)) {
                fprintf(fp, "Something wrong, node in table should have been created in top dist proc.\n");
                return(0);
            }
            if (nodeStatChild->oddBotDist == MAXSHORTINT) {
                if (nodeStatChild->evenBotDist == MAXSHORTINT) {
                    if (!CreateBotDist(realChild, pathTable, pathLengthArray, fp))
                        return(0);
                } else {
                    fprintf(fp, "Something wrong, both bot nodeStats should be there\n");
                    return(0);
                }
            }
            if (Cudd_IsComplement(child)) {
                if (nodeStatChild->oddBotDist != MAXSHORTINT)
                    botDist = nodeStatChild->oddBotDist + 1;
                else
                    botDist = MAXSHORTINT;
                if (nodeStat->evenBotDist > botDist )
                    nodeStat->evenBotDist = botDist;
                if (nodeStatChild->evenBotDist != MAXSHORTINT)
                    botDist = nodeStatChild->evenBotDist + 1;
                else
                    botDist = MAXSHORTINT;
                if (nodeStat->oddBotDist > botDist)
                    nodeStat->oddBotDist = botDist;
            } else {
                if (nodeStatChild->evenBotDist != MAXSHORTINT)
                    botDist = nodeStatChild->evenBotDist + 1;
                else
                    botDist = MAXSHORTINT;
                if (nodeStat->evenBotDist > botDist)
                    nodeStat->evenBotDist = botDist;
                if (nodeStatChild->oddBotDist != MAXSHORTINT)
                    botDist = nodeStatChild->oddBotDist + 1;
                else
                    botDist = MAXSHORTINT;
                if (nodeStat->oddBotDist > botDist)
                    nodeStat->oddBotDist = botDist;
            }
        } 
        processingDone++;
    } 
    if ((nodeStat->oddTopDist != MAXSHORTINT) &&
        (nodeStat->oddBotDist != MAXSHORTINT))
        oddLen = (nodeStat->oddTopDist + nodeStat->oddBotDist);
    else
        oddLen = MAXSHORTINT;
    if ((nodeStat->evenTopDist != MAXSHORTINT) &&
        (nodeStat->evenBotDist != MAXSHORTINT))
        evenLen = (nodeStat->evenTopDist +nodeStat->evenBotDist);
    else
        evenLen = MAXSHORTINT;
    if (oddLen < pathLength ) {
        if (pathLength != MAXSHORTINT)
            pathLengthArray[pathLength]--;
        if (oddLen != MAXSHORTINT)
            pathLengthArray[oddLen]++;
        pathLength = oddLen;
    }
    if (evenLen < pathLength ) {
        if (pathLength != MAXSHORTINT)
            pathLengthArray[pathLength]--;
        if (evenLen != MAXSHORTINT)
            pathLengthArray[evenLen]++;
    }
    return(1);
}
static int CreateBotDist ( DdNode * node , st__table * pathTable , unsigned int * pathLengthArray , FILE * fp ) { DdNode * N , * Nv , * Nnv ; DdNode * realChild ; DdNode * child , * regChild ; NodeDist_t * nodeStat , * nodeStatChild ; unsigned int oddLen , evenLen , pathLength ; DdHalfWord botDist ; int processingDone ; if ( Cudd_IsConstant ( node ) ) return ( 1 ) ; N = Cudd_Regular ( node ) ; if ( ! st__lookup ( pathTable , ( const char * ) N , ( char * * ) & nodeStat ) ) { fprintf ( fp , " \n " ) ; return ( 0 ) ; } if ( ( nodeStat -> oddTopDist != MAXSHORTINT ) && ( nodeStat -> oddBotDist != MAXSHORTINT ) ) oddLen = ( nodeStat -> oddTopDist + nodeStat -> oddBotDist ) ; else oddLen = MAXSHORTINT ; if ( ! ( ( nodeStat -> evenTopDist == MAXSHORTINT ) || ( nodeStat -> evenBotDist == MAXSHORTINT ) ) ) evenLen = ( nodeStat -> evenTopDist + nodeStat -> evenBotDist ) ; else evenLen = MAXSHORTINT ; pathLength = ( oddLen <= evenLen ) ? oddLen : evenLen ; Nv = Cudd_T ( N ) ; Nnv = Cudd_E ( N ) ; processingDone = 0 ; while ( processingDone != 2 ) { if ( ! processingDone ) { child = Nv ; } else { child = Nnv ; } realChild = Cudd_NotCond ( child , Cudd_IsComplement ( node ) ) ; regChild = Cudd_Regular ( child ) ; if ( Cudd_IsConstant ( realChild ) ) { if ( Cudd_IsComplement ( child ) ) nodeStat -> oddBotDist = 1 ; else nodeStat -> evenBotDist = 1 ; } else { if ( ! st__lookup ( pathTable , ( const char * ) regChild , ( char * * ) & nodeStatChild ) ) { fprintf ( fp , " \n " ) ; return ( 0 ) ; } if ( nodeStatChild -> oddBotDist == MAXSHORTINT ) { if ( nodeStatChild -> evenBotDist == MAXSHORTINT ) { if ( ! CreateBotDist ( realChild , pathTable , pathLengthArray , fp ) ) return ( 0 ) ; } else { fprintf ( fp , " \n " ) ; return ( 0 ) ; } } if ( Cudd_IsComplement ( child ) ) { if ( nodeStatChild -> oddBotDist != MAXSHORTINT ) botDist = nodeStatChild -> oddBotDist + 1 ; else botDist = MAXSHORTINT ; if ( nodeStat -> evenBotDist > botDist ) nodeStat -> evenBotDist = botDist ; if ( nodeStatChild -> evenBotDist != MAXSHORTINT ) botDist = nodeStatChild -> evenBotDist + 1 ; else botDist = MAXSHORTINT ; if ( nodeStat -> oddBotDist > botDist ) nodeStat -> oddBotDist = botDist ; } else { if ( nodeStatChild -> evenBotDist != MAXSHORTINT ) botDist = nodeStatChild -> evenBotDist + 1 ; else botDist = MAXSHORTINT ; if ( nodeStat -> evenBotDist > botDist ) nodeStat -> evenBotDist = botDist ; if ( nodeStatChild -> oddBotDist != MAXSHORTINT ) botDist = nodeStatChild -> oddBotDist + 1 ; else botDist = MAXSHORTINT ; if ( nodeStat -> oddBotDist > botDist ) nodeStat -> oddBotDist = botDist ; } } processingDone ++ ; } if ( ( nodeStat -> oddTopDist != MAXSHORTINT ) && ( nodeStat -> oddBotDist != MAXSHORTINT ) ) oddLen = ( nodeStat -> oddTopDist + nodeStat -> oddBotDist ) ; else oddLen = MAXSHORTINT ; if ( ( nodeStat -> evenTopDist != MAXSHORTINT ) && ( nodeStat -> evenBotDist != MAXSHORTINT ) ) evenLen = ( nodeStat -> evenTopDist + nodeStat -> evenBotDist ) ; else evenLen = MAXSHORTINT ; if ( oddLen < pathLength ) { if ( pathLength != MAXSHORTINT ) pathLengthArray [ pathLength ] -- ; if ( oddLen != MAXSHORTINT ) pathLengthArray [ oddLen ] ++ ; pathLength = oddLen ; } if ( evenLen < pathLength ) { if ( pathLength != MAXSHORTINT ) pathLengthArray [ pathLength ] -- ; if ( evenLen != MAXSHORTINT ) pathLengthArray [ evenLen ] ++ ; } return ( 1 ) ; }
Function
Synopsis    [ Labels each node with the shortest distance from the constant.]
Function Synopsis [ Labels each node with the shortest distance from the constant . ]
/* current node */ /* path table with path lengths */ /* array that stores number of nodes belonging to a particular path length. */ /* where to write messages */ /* each node has one table entry */ /* update as you go down the min dist of each node from
       the root in each (odd and even) parity */ /* compute length of odd parity distances */ /* compute length of even parity distances */ /* assign pathlength to minimum of the two */ /* process each child */ /* Found a minterm; count parity and shortest distance
            ** from the constant.
            */ /* If node not in table, recur. */ /* Update shortest distance from the constant depending on
            **  parity. */ /* If parity on the edge then add 1 to even distance
                ** of child to get odd parity distance and add 1 to
                ** odd distance of child to get even parity
                ** distance. Change distance of current node only if
                ** the calculated distance is less than existing
                ** distance. */ /* If parity on the edge then add 1 to even distance
                ** of child to get even parity distance and add 1 to
                ** odd distance of child to get odd parity distance.
                ** Change distance of current node only if the
                ** calculated distance is lesser than existing
                ** distance. */ /* end of else (if not constant child ) */ /* end of while processing Nv, Nnv */ /* Compute shortest path length on the fly. */ /* Update path length array that has number of nodes of a particular
    ** path length. */