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

  Synopsis    [Implements the recursive step of Cudd_FindEssential.]

  Description [Implements the recursive step of Cudd_FindEssential.
  Returns a pointer to the cube BDD if successful; NULL otherwise.]

  SideEffects [None]

******************************************************************************/
Function
Synopsis    [Implements the recursive step of Cudd_FindEssential.]

Description [Implements the recursive step of Cudd_FindEssential.
Returns a pointer to the cube BDD if successful; NULL otherwise.]


Function Synopsis [ Implements the recursive step of Cudd_FindEssential . ] Description [ Implements the recursive step of Cudd_FindEssential . Returns a pointer to the cube BDD if successful ; NULL otherwise . ]
static DdNode *
ddFindEssentialRecur(
  DdManager * dd,
  DdNode * f)
{
    DdNode      *T, *E, *F;
    DdNode      *essT, *essE, *res;
    int         index;
    DdNode      *one, *lzero, *azero;
    one = DD_ONE(dd);
    F = Cudd_Regular(f);
    if (cuddIsConstant(F)) return(one);
    res = cuddCacheLookup1(dd,Cudd_FindEssential,f);
    if (res != NULL) {
        return(res);
    }
    lzero = Cudd_Not(one);
    azero = DD_ZERO(dd);
    T = cuddT(F);
    E = cuddE(F);
    if (Cudd_IsComplement(f)) {
        T = Cudd_Not(T); E = Cudd_Not(E);
    }
    index = F->index;
    if (Cudd_IsConstant(T) && T != lzero && T != azero) {
        if (E == lzero || E == azero) {
            res = dd->vars[index];
        } else {
            res = one;
        }
    } else if (T == lzero || T == azero) {
        if (Cudd_IsConstant(E)) { 
            res = Cudd_Not(dd->vars[index]);
        } else { 
            essE = ddFindEssentialRecur(dd,E);
            if (essE == NULL) {
                return(NULL);
            }
            cuddRef(essE);
            res = cuddUniqueInter(dd,index,one,Cudd_Not(essE));
            if (res == NULL) {
                Cudd_RecursiveDeref(dd,essE);
                return(NULL);
            }
            res = Cudd_Not(res);
            cuddDeref(essE);
        }
    } else { 
        if (E == lzero || E == azero) {
            essT = ddFindEssentialRecur(dd,T);
            if (essT == NULL) {
                return(NULL);
            }
            cuddRef(essT);
            res = cuddBddAndRecur(dd,dd->vars[index],essT);
            if (res == NULL) {
                Cudd_RecursiveDeref(dd,essT);
                return(NULL);
            }
            cuddDeref(essT);
        } else if (!Cudd_IsConstant(E)) {
            essT = ddFindEssentialRecur(dd,T);
            if (essT == NULL) {
                return(NULL);
            }
            if (essT == one) {
                res = one;
            } else {
                cuddRef(essT);
                essE = ddFindEssentialRecur(dd,E);
                if (essE == NULL) {
                    Cudd_RecursiveDeref(dd,essT);
                    return(NULL);
                }
                cuddRef(essE);
                res = cuddBddLiteralSetIntersectionRecur(dd,essT,essE);
                if (res == NULL) {
                    Cudd_RecursiveDeref(dd,essT);
                    Cudd_RecursiveDeref(dd,essE);
                    return(NULL);
                }
                cuddRef(res);
                Cudd_RecursiveDeref(dd,essT);
                Cudd_RecursiveDeref(dd,essE);
                cuddDeref(res);
            }
        } else {        
            res = one;
        }
    }
    cuddCacheInsert1(dd,Cudd_FindEssential, f, res);
    return(res);
}
static DdNode * ddFindEssentialRecur ( DdManager * dd , DdNode * f ) { DdNode * T , * E , * F ; DdNode * essT , * essE , * res ; int index ; DdNode * one , * lzero , * azero ; one = DD_ONE ( dd ) ; F = Cudd_Regular ( f ) ; if ( cuddIsConstant ( F ) ) return ( one ) ; res = cuddCacheLookup1 ( dd , Cudd_FindEssential , f ) ; if ( res != NULL ) { return ( res ) ; } lzero = Cudd_Not ( one ) ; azero = DD_ZERO ( dd ) ; T = cuddT ( F ) ; E = cuddE ( F ) ; if ( Cudd_IsComplement ( f ) ) { T = Cudd_Not ( T ) ; E = Cudd_Not ( E ) ; } index = F -> index ; if ( Cudd_IsConstant ( T ) && T != lzero && T != azero ) { if ( E == lzero || E == azero ) { res = dd -> vars [ index ] ; } else { res = one ; } } else if ( T == lzero || T == azero ) { if ( Cudd_IsConstant ( E ) ) { res = Cudd_Not ( dd -> vars [ index ] ) ; } else { essE = ddFindEssentialRecur ( dd , E ) ; if ( essE == NULL ) { return ( NULL ) ; } cuddRef ( essE ) ; res = cuddUniqueInter ( dd , index , one , Cudd_Not ( essE ) ) ; if ( res == NULL ) { Cudd_RecursiveDeref ( dd , essE ) ; return ( NULL ) ; } res = Cudd_Not ( res ) ; cuddDeref ( essE ) ; } } else { if ( E == lzero || E == azero ) { essT = ddFindEssentialRecur ( dd , T ) ; if ( essT == NULL ) { return ( NULL ) ; } cuddRef ( essT ) ; res = cuddBddAndRecur ( dd , dd -> vars [ index ] , essT ) ; if ( res == NULL ) { Cudd_RecursiveDeref ( dd , essT ) ; return ( NULL ) ; } cuddDeref ( essT ) ; } else if ( ! Cudd_IsConstant ( E ) ) { essT = ddFindEssentialRecur ( dd , T ) ; if ( essT == NULL ) { return ( NULL ) ; } if ( essT == one ) { res = one ; } else { cuddRef ( essT ) ; essE = ddFindEssentialRecur ( dd , E ) ; if ( essE == NULL ) { Cudd_RecursiveDeref ( dd , essT ) ; return ( NULL ) ; } cuddRef ( essE ) ; res = cuddBddLiteralSetIntersectionRecur ( dd , essT , essE ) ; if ( res == NULL ) { Cudd_RecursiveDeref ( dd , essT ) ; Cudd_RecursiveDeref ( dd , essE ) ; return ( NULL ) ; } cuddRef ( res ) ; Cudd_RecursiveDeref ( dd , essT ) ; Cudd_RecursiveDeref ( dd , essE ) ; cuddDeref ( res ) ; } } else { res = one ; } } cuddCacheInsert1 ( dd , Cudd_FindEssential , f , res ) ; return ( res ) ; }
Function
Synopsis    [Implements the recursive step of Cudd_FindEssential.]
Function Synopsis [ Implements the recursive step of Cudd_FindEssential . ]
/* If f is constant the set of essential variables is empty. */ /* Find cofactors: here f is non-constant. */ /* if E is zero, index is essential, otherwise there are no
        ** essentials, because index is not essential and no other variable
        ** can be, since setting index = 1 makes the function constant and
        ** different from 0.
        */ /* E cannot be zero here */ /* E == non-constant */ /* find essentials in the else branch */ /* add index to the set with negative phase */ /* T == non-const */ /* find essentials in the then branch */ /* add index to the set with positive phase */ /* use And because essT may be complemented */ /* if E is a non-zero constant there are no essentials
            ** because T is non-constant.
            */ /* res = intersection(essT, essE) */ /* E is a non-zero constant */