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

  Synopsis    [Checks whether a variable is dependent on others in a
  function.]

  Description [Checks whether a variable is dependent on others in a
  function.  Returns 1 if the variable is dependent; 0 otherwise. No
  new nodes are created.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
Function
Synopsis    [Checks whether a variable is dependent on others in a
function.]

Description [Checks whether a variable is dependent on others in a
function.  Returns 1 if the variable is dependent; 0 otherwise. No
new nodes are created.]




Function Synopsis [ Checks whether a variable is dependent on others in a function . ] Description [ Checks whether a variable is dependent on others in a function . Returns 1 if the variable is dependent ; 0 otherwise . No new nodes are created . ]
int
Cudd_bddVarIsDependent(
  DdManager *dd,                
  DdNode *f,                    
  DdNode *var                   )
{
    DdNode *F, *res, *zero, *ft, *fe;
    unsigned topf, level;
    DD_CTFP cacheOp;
    int retval;
    zero = Cudd_Not(DD_ONE(dd));
    if (Cudd_IsConstant(f)) return(f == zero);
    F = Cudd_Regular(f);
    topf = (unsigned) dd->perm[F->index];
    level = (unsigned) dd->perm[var->index];
    if (topf > level) {
        return(0);
    }
    cacheOp = (DD_CTFP) Cudd_bddVarIsDependent;
    res = cuddCacheLookup2(dd,cacheOp,f,var);
    if (res != NULL) {
        return(res != zero);
    }
    ft = Cudd_NotCond(cuddT(F), f != F);
    fe = Cudd_NotCond(cuddE(F), f != F);
    if (topf == level) {
        retval = Cudd_bddLeq(dd,ft,Cudd_Not(fe));
    } else {
        retval = Cudd_bddVarIsDependent(dd,ft,var) &&
            Cudd_bddVarIsDependent(dd,fe,var);
    }
    cuddCacheInsert2(dd,cacheOp,f,var,Cudd_NotCond(zero,retval));
    return(retval);
}
int Cudd_bddVarIsDependent ( DdManager * dd , DdNode * f , DdNode * var ) { DdNode * F , * res , * zero , * ft , * fe ; unsigned topf , level ; DD_CTFP cacheOp ; int retval ; zero = Cudd_Not ( DD_ONE ( dd ) ) ; if ( Cudd_IsConstant ( f ) ) return ( f == zero ) ; F = Cudd_Regular ( f ) ; topf = ( unsigned ) dd -> perm [ F -> index ] ; level = ( unsigned ) dd -> perm [ var -> index ] ; if ( topf > level ) { return ( 0 ) ; } cacheOp = ( DD_CTFP ) Cudd_bddVarIsDependent ; res = cuddCacheLookup2 ( dd , cacheOp , f , var ) ; if ( res != NULL ) { return ( res != zero ) ; } ft = Cudd_NotCond ( cuddT ( F ) , f != F ) ; fe = Cudd_NotCond ( cuddE ( F ) , f != F ) ; if ( topf == level ) { retval = Cudd_bddLeq ( dd , ft , Cudd_Not ( fe ) ) ; } else { retval = Cudd_bddVarIsDependent ( dd , ft , var ) && Cudd_bddVarIsDependent ( dd , fe , var ) ; } cuddCacheInsert2 ( dd , cacheOp , f , var , Cudd_NotCond ( zero , retval ) ) ; return ( retval ) ; }
Function
Synopsis    [Checks whether a variable is dependent on others in a
function.]
Function Synopsis [ Checks whether a variable is dependent on others in a function . ]
/* manager */ /* function */ /* variable */ /* From now on f is not constant. */ /* Check terminal case. If topf > index of var, f does not depend on var.
    ** Therefore, var is not dependent in f. */ /* Compute cofactors. */