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

  Synopsis    [Finds the first path of a ZDD.]

  Description [Defines an iterator on the paths of a ZDD
  and finds its first path. Returns a generator that contains the
  information necessary to continue the enumeration if successful; NULL
  otherwise.<p>
  A path is represented as an array of literals, which are integers in
  {0, 1, 2}; 0 represents an else arc out of a node, 1 represents a then arc
  out of a node, and 2 stands for the absence of a node.
  The size of the array equals the number of variables in the manager at
  the time Cudd_zddFirstCube is called.<p>
  The paths that end in the empty terminal are not enumerated.]

  SideEffects [The first path is returned as a side effect.]

  SeeAlso     [Cudd_zddForeachPath Cudd_zddNextPath Cudd_GenFree
  Cudd_IsGenEmpty]

******************************************************************************/
Function
Synopsis    [Finds the first path of a ZDD.]

Description [Defines an iterator on the paths of a ZDD
and finds its first path. Returns a generator that contains the
information necessary to continue the enumeration if successful; NULL
otherwise.
A path is represented as an array of literals, which are integers in
{0, 1, 2}; 0 represents an else arc out of a node, 1 represents a then arc
out of a node, and 2 stands for the absence of a node.
The size of the array equals the number of variables in the manager at
the time Cudd_zddFirstCube is called.
The paths that end in the empty terminal are not enumerated.]

SideEffects [The first path is returned as a side effect.]


Function Synopsis [ Finds the first path of a ZDD . ] Description [ Defines an iterator on the paths of a ZDD and finds its first path . Returns a generator that contains the information necessary to continue the enumeration if successful ; NULL otherwise . A path is represented as an array of literals which are integers in { 0 1 2 } ; 0 represents an else arc out of a node 1 represents a then arc out of a node and 2 stands for the absence of a node . The size of the array equals the number of variables in the manager at the time Cudd_zddFirstCube is called . The paths that end in the empty terminal are not enumerated . ] SideEffects [ The first path is returned as a side effect . ]
DdGen *
Cudd_zddFirstPath(
  DdManager * zdd,
  DdNode * f,
  int ** path)
{
    DdGen *gen;
    DdNode *top, *next, *prev;
    int i;
    int nvars;
    if (zdd == NULL || f == NULL) return(NULL);
    gen = ABC_ALLOC(DdGen,1);
    if (gen == NULL) {
        zdd->errorCode = CUDD_MEMORY_OUT;
        return(NULL);
    }
    gen->manager = zdd;
    gen->type = CUDD_GEN_ZDD_PATHS;
    gen->status = CUDD_GEN_EMPTY;
    gen->gen.cubes.cube = NULL;
    gen->gen.cubes.value = DD_ZERO_VAL;
    gen->stack.sp = 0;
    gen->stack.stack = NULL;
    gen->node = NULL;
    nvars = zdd->sizeZ;
    gen->gen.cubes.cube = ABC_ALLOC(int,nvars);
    if (gen->gen.cubes.cube == NULL) {
        zdd->errorCode = CUDD_MEMORY_OUT;
        ABC_FREE(gen);
        return(NULL);
    }
    for (i = 0; i < nvars; i++) gen->gen.cubes.cube[i] = 2;
    gen->stack.stack = ABC_ALLOC(DdNodePtr, nvars+1);
    if (gen->stack.stack == NULL) {
        zdd->errorCode = CUDD_MEMORY_OUT;
        ABC_FREE(gen->gen.cubes.cube);
        ABC_FREE(gen);
        return(NULL);
    }
    for (i = 0; i <= nvars; i++) gen->stack.stack[i] = NULL;
    gen->stack.stack[gen->stack.sp] = f; gen->stack.sp++;
    while (1) {
        top = gen->stack.stack[gen->stack.sp-1];
        if (!cuddIsConstant(Cudd_Regular(top))) {
            gen->gen.cubes.cube[Cudd_Regular(top)->index] = 0;
            next = cuddE(Cudd_Regular(top));
            gen->stack.stack[gen->stack.sp] = Cudd_Not(next); gen->stack.sp++;
        } else if (Cudd_Regular(top) == DD_ZERO(zdd)) {
            while (1) {
                if (gen->stack.sp == 1) {
                    gen->status = CUDD_GEN_EMPTY;
                    gen->stack.sp--;
                    goto done;
                }
                prev = Cudd_Regular(gen->stack.stack[gen->stack.sp-2]);
                next = cuddT(prev);
                if (next != top) { 
                    gen->gen.cubes.cube[prev->index] = 1;
                    gen->stack.stack[gen->stack.sp-1] = next;
                    break;
                }
                gen->gen.cubes.cube[prev->index] = 2;
                gen->stack.sp--;
                top = gen->stack.stack[gen->stack.sp-1];
            }
        } else {
            gen->status = CUDD_GEN_NONEMPTY;
            gen->gen.cubes.value = cuddV(Cudd_Regular(top));
            goto done;
        }
    }
done:
    *path = gen->gen.cubes.cube;
    return(gen);
}
DdGen * Cudd_zddFirstPath ( DdManager * zdd , DdNode * f , int * * path ) { DdGen * gen ; DdNode * top , * next , * prev ; int i ; int nvars ; if ( zdd == NULL || f == NULL ) return ( NULL ) ; gen = ABC_ALLOC ( DdGen , 1 ) ; if ( gen == NULL ) { zdd -> errorCode = CUDD_MEMORY_OUT ; return ( NULL ) ; } gen -> manager = zdd ; gen -> type = CUDD_GEN_ZDD_PATHS ; gen -> status = CUDD_GEN_EMPTY ; gen -> gen . cubes . cube = NULL ; gen -> gen . cubes . value = DD_ZERO_VAL ; gen -> stack . sp = 0 ; gen -> stack . stack = NULL ; gen -> node = NULL ; nvars = zdd -> sizeZ ; gen -> gen . cubes . cube = ABC_ALLOC ( int , nvars ) ; if ( gen -> gen . cubes . cube == NULL ) { zdd -> errorCode = CUDD_MEMORY_OUT ; ABC_FREE ( gen ) ; return ( NULL ) ; } for ( i = 0 ; i < nvars ; i ++ ) gen -> gen . cubes . cube [ i ] = 2 ; gen -> stack . stack = ABC_ALLOC ( DdNodePtr , nvars + 1 ) ; if ( gen -> stack . stack == NULL ) { zdd -> errorCode = CUDD_MEMORY_OUT ; ABC_FREE ( gen -> gen . cubes . cube ) ; ABC_FREE ( gen ) ; return ( NULL ) ; } for ( i = 0 ; i <= nvars ; i ++ ) gen -> stack . stack [ i ] = NULL ; gen -> stack . stack [ gen -> stack . sp ] = f ; gen -> stack . sp ++ ; while ( 1 ) { top = gen -> stack . stack [ gen -> stack . sp - 1 ] ; if ( ! cuddIsConstant ( Cudd_Regular ( top ) ) ) { gen -> gen . cubes . cube [ Cudd_Regular ( top ) -> index ] = 0 ; next = cuddE ( Cudd_Regular ( top ) ) ; gen -> stack . stack [ gen -> stack . sp ] = Cudd_Not ( next ) ; gen -> stack . sp ++ ; } else if ( Cudd_Regular ( top ) == DD_ZERO ( zdd ) ) { while ( 1 ) { if ( gen -> stack . sp == 1 ) { gen -> status = CUDD_GEN_EMPTY ; gen -> stack . sp -- ; goto done ; } prev = Cudd_Regular ( gen -> stack . stack [ gen -> stack . sp - 2 ] ) ; next = cuddT ( prev ) ; if ( next != top ) { gen -> gen . cubes . cube [ prev -> index ] = 1 ; gen -> stack . stack [ gen -> stack . sp - 1 ] = next ; break ; } gen -> gen . cubes . cube [ prev -> index ] = 2 ; gen -> stack . sp -- ; top = gen -> stack . stack [ gen -> stack . sp - 1 ] ; } } else { gen -> status = CUDD_GEN_NONEMPTY ; gen -> gen . cubes . value = cuddV ( Cudd_Regular ( top ) ) ; goto done ; } } done : * path = gen -> gen . cubes . cube ; return ( gen ) ; }
Function
Synopsis    [Finds the first path of a ZDD.]
Function Synopsis [ Finds the first path of a ZDD . ]
/* Sanity Check. */ /* Allocate generator an initialize it. */ /* The maximum stack depth is one plus the number of variables.
    ** because a path may have nodes at all levels, including the
    ** constant level.
    */ /* Find the first path of the ZDD. */ /* Take the else branch first. */ /* Backtrack. */ /* The current node has no predecessor. */ /* follow the then branch next */ /* Pop the stack and try again. */