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

  Synopsis    [Generates the next path of a ZDD.]

  Description [Generates the next path of a ZDD onset,
  using generator gen. Returns 0 if the enumeration is completed; 1
  otherwise.]

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

  SeeAlso     [Cudd_zddForeachPath Cudd_zddFirstPath Cudd_GenFree
  Cudd_IsGenEmpty]

******************************************************************************/
Function
Synopsis    [Generates the next path of a ZDD.]

Description [Generates the next path of a ZDD onset,
using generator gen. Returns 0 if the enumeration is completed; 1
otherwise.]

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


Function Synopsis [ Generates the next path of a ZDD . ] Description [ Generates the next path of a ZDD onset using generator gen . Returns 0 if the enumeration is completed ; 1 otherwise . ] SideEffects [ The path is returned as a side effect . The generator is modified . ]
int
Cudd_zddNextPath(
  DdGen * gen,
  int ** path)
{
    DdNode *top, *next, *prev;
    DdManager *zdd = gen->manager;
    while (1) {
        if (gen->stack.sp == 1) {
            gen->status = CUDD_GEN_EMPTY;
            gen->stack.sp--;
            goto done;
        }
        top = gen->stack.stack[gen->stack.sp-1];
        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--;
    }
    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:
    if (gen->status == CUDD_GEN_EMPTY) return(0);
    *path = gen->gen.cubes.cube;
    return(1);
}
int Cudd_zddNextPath ( DdGen * gen , int * * path ) { DdNode * top , * next , * prev ; DdManager * zdd = gen -> manager ; while ( 1 ) { if ( gen -> stack . sp == 1 ) { gen -> status = CUDD_GEN_EMPTY ; gen -> stack . sp -- ; goto done ; } top = gen -> stack . stack [ gen -> stack . sp - 1 ] ; 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 -- ; } 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 : if ( gen -> status == CUDD_GEN_EMPTY ) return ( 0 ) ; * path = gen -> gen . cubes . cube ; return ( 1 ) ; }
Function
Synopsis    [Generates the next path of a ZDD.]
Function Synopsis [ Generates the next path of a ZDD . ]
/* Backtrack from previously reached terminal node. */ /* The current node has no predecessor. */ /* follow the then branch next */ /* Pop the stack and try again. */ /* Take the else branch first. */ /* Backtrack. */ /* The current node has no predecessor. */ /* follow the then branch next */ /* Pop the stack and try again. */