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

  Synopsis    [Performs the recursive step of Cudd_bddCharToVect.]

  Description [Performs the recursive step of Cudd_bddCharToVect.
  This function maintains the invariant that f is non-zero.
  Returns the i-th component of the vector if successful; otherwise NULL.]

  SideEffects [None]

  SeeAlso     [Cudd_bddCharToVect]

******************************************************************************/
Function
Synopsis    [Performs the recursive step of Cudd_bddCharToVect.]

Description [Performs the recursive step of Cudd_bddCharToVect.
This function maintains the invariant that f is non-zero.
Returns the i-th component of the vector if successful; otherwise NULL.]




Function Synopsis [ Performs the recursive step of Cudd_bddCharToVect . ] Description [ Performs the recursive step of Cudd_bddCharToVect . This function maintains the invariant that f is non - zero . Returns the i - th component of the vector if successful ; otherwise NULL . ]
static DdNode *
cuddBddCharToVect(
  DdManager * dd,
  DdNode * f,
  DdNode * x)
{
    unsigned int topf;
    unsigned int level;
    int comple;
    DdNode *one, *zero, *res, *F, *fT, *fE, *T, *E;
    statLine(dd);
    res = cuddCacheLookup2(dd, cuddBddCharToVect, f, x);
    if (res != NULL) {
        return(res);
    }
    F = Cudd_Regular(f);
    topf = cuddI(dd,F->index);
    level = dd->perm[x->index];
    if (topf > level) return(x);
    one = DD_ONE(dd);
    zero = Cudd_Not(one);
    comple = F != f;
    fT = Cudd_NotCond(cuddT(F),comple);
    fE = Cudd_NotCond(cuddE(F),comple);
    if (topf == level) {
        if (fT == zero) return(zero);
        if (fE == zero) return(one);
        return(x);
    }
    if (fT == zero) return(cuddBddCharToVect(dd, fE, x));
    if (fE == zero) return(cuddBddCharToVect(dd, fT, x));
    T = cuddBddCharToVect(dd, fT, x);
    if (T == NULL) {
        return(NULL);
    }
    cuddRef(T);
    E = cuddBddCharToVect(dd, fE, x);
    if (E == NULL) {
        Cudd_IterDerefBdd(dd,T);
        return(NULL);
    }
    cuddRef(E);
    res = cuddBddIteRecur(dd, dd->vars[F->index], T, E);
    if (res == NULL) {
        Cudd_IterDerefBdd(dd,T);
        Cudd_IterDerefBdd(dd,E);
        return(NULL);
    }
    cuddDeref(T);
    cuddDeref(E);
    cuddCacheInsert2(dd, cuddBddCharToVect, f, x, res);
    return(res);
}
static DdNode * cuddBddCharToVect ( DdManager * dd , DdNode * f , DdNode * x ) { unsigned int topf ; unsigned int level ; int comple ; DdNode * one , * zero , * res , * F , * fT , * fE , * T , * E ; statLine ( dd ) ; res = cuddCacheLookup2 ( dd , cuddBddCharToVect , f , x ) ; if ( res != NULL ) { return ( res ) ; } F = Cudd_Regular ( f ) ; topf = cuddI ( dd , F -> index ) ; level = dd -> perm [ x -> index ] ; if ( topf > level ) return ( x ) ; one = DD_ONE ( dd ) ; zero = Cudd_Not ( one ) ; comple = F != f ; fT = Cudd_NotCond ( cuddT ( F ) , comple ) ; fE = Cudd_NotCond ( cuddE ( F ) , comple ) ; if ( topf == level ) { if ( fT == zero ) return ( zero ) ; if ( fE == zero ) return ( one ) ; return ( x ) ; } if ( fT == zero ) return ( cuddBddCharToVect ( dd , fE , x ) ) ; if ( fE == zero ) return ( cuddBddCharToVect ( dd , fT , x ) ) ; T = cuddBddCharToVect ( dd , fT , x ) ; if ( T == NULL ) { return ( NULL ) ; } cuddRef ( T ) ; E = cuddBddCharToVect ( dd , fE , x ) ; if ( E == NULL ) { Cudd_IterDerefBdd ( dd , T ) ; return ( NULL ) ; } cuddRef ( E ) ; res = cuddBddIteRecur ( dd , dd -> vars [ F -> index ] , T , E ) ; if ( res == NULL ) { Cudd_IterDerefBdd ( dd , T ) ; Cudd_IterDerefBdd ( dd , E ) ; return ( NULL ) ; } cuddDeref ( T ) ; cuddDeref ( E ) ; cuddCacheInsert2 ( dd , cuddBddCharToVect , f , x , res ) ; return ( res ) ; }
Function
Synopsis    [Performs the recursive step of Cudd_bddCharToVect.]
Function Synopsis [ Performs the recursive step of Cudd_bddCharToVect . ]
/* Check the cache. */ /* Here topf < level. */