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

  Synopsis    [Checks whether ADD g is constant whenever ADD f is 1.]

  Description [Checks whether ADD g is constant whenever ADD f is 1.  f
  must be a 0-1 ADD.  Returns a pointer to the resulting ADD (which may
  or may not be constant) or DD_NON_CONSTANT. If f is identically 0,
  the check is assumed to be successful, and the background value is
  returned. No new nodes are created.]

  SideEffects [None]

  SeeAlso     [Cudd_addIteConstant Cudd_addLeq]

******************************************************************************/
Function
Synopsis    [Checks whether ADD g is constant whenever ADD f is 1.]

Description [Checks whether ADD g is constant whenever ADD f is 1.  f
must be a 0-1 ADD.  Returns a pointer to the resulting ADD (which may
or may not be constant) or DD_NON_CONSTANT. If f is identically 0,
the check is assumed to be successful, and the background value is
returned. No new nodes are created.]




Function Synopsis [ Checks whether ADD g is constant whenever ADD f is 1 . ] Description [ Checks whether ADD g is constant whenever ADD f is 1 . f must be a 0 - 1 ADD . Returns a pointer to the resulting ADD ( which may or may not be constant ) or DD_NON_CONSTANT . If f is identically 0 the check is assumed to be successful and the background value is returned . No new nodes are created . ]
DdNode *
Cudd_addEvalConst(
  DdManager * dd,
  DdNode * f,
  DdNode * g)
{
    DdNode *zero;
    DdNode *Fv,*Fnv,*Gv,*Gnv,*r,*t,*e;
    unsigned int topf,topg;
#ifdef DD_DEBUG
    assert(!Cudd_IsComplement(f));
#endif
    statLine(dd);
    if (f == DD_ONE(dd) || cuddIsConstant(g)) {
        return(g);
    }
    if (f == (zero = DD_ZERO(dd))) {
        return(dd->background);
    }
#ifdef DD_DEBUG
    assert(!cuddIsConstant(f));
#endif
    topf = cuddI(dd,f->index);
    topg = cuddI(dd,g->index);
    r = cuddConstantLookup(dd,DD_ADD_EVAL_CONST_TAG,f,g,g);
    if (r != NULL) {
        return(r);
    }
    if (topf <= topg) {
        Fv = cuddT(f); Fnv = cuddE(f);
    } else {
        Fv = Fnv = f;
    }
    if (topg <= topf) {
        Gv = cuddT(g); Gnv = cuddE(g);
    } else {
        Gv = Gnv = g;
    }
    if (Fv != zero) {
        t = Cudd_addEvalConst(dd,Fv,Gv);
        if (t == DD_NON_CONSTANT || !cuddIsConstant(t)) {
            cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, DD_NON_CONSTANT);
            return(DD_NON_CONSTANT);
        }
        if (Fnv != zero) {
            e = Cudd_addEvalConst(dd,Fnv,Gnv);
            if (e == DD_NON_CONSTANT || !cuddIsConstant(e) || t != e) {
                cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, DD_NON_CONSTANT);
                return(DD_NON_CONSTANT);
            }
        }
        cuddCacheInsert2(dd,Cudd_addEvalConst,f,g,t);
        return(t);
    } else { 
        e = Cudd_addEvalConst(dd,Fnv,Gnv);
        cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, e);
        return(e);
    }
}
DdNode * Cudd_addEvalConst ( DdManager * dd , DdNode * f , DdNode * g ) { DdNode * zero ; DdNode * Fv , * Fnv , * Gv , * Gnv , * r , * t , * e ; unsigned int topf , topg ; #ifdef DD_DEBUG assert ( ! Cudd_IsComplement ( f ) ) ; #endif statLine ( dd ) ; if ( f == DD_ONE ( dd ) || cuddIsConstant ( g ) ) { return ( g ) ; } if ( f == ( zero = DD_ZERO ( dd ) ) ) { return ( dd -> background ) ; } #ifdef DD_DEBUG assert ( ! cuddIsConstant ( f ) ) ; #endif topf = cuddI ( dd , f -> index ) ; topg = cuddI ( dd , g -> index ) ; r = cuddConstantLookup ( dd , DD_ADD_EVAL_CONST_TAG , f , g , g ) ; if ( r != NULL ) { return ( r ) ; } if ( topf <= topg ) { Fv = cuddT ( f ) ; Fnv = cuddE ( f ) ; } else { Fv = Fnv = f ; } if ( topg <= topf ) { Gv = cuddT ( g ) ; Gnv = cuddE ( g ) ; } else { Gv = Gnv = g ; } if ( Fv != zero ) { t = Cudd_addEvalConst ( dd , Fv , Gv ) ; if ( t == DD_NON_CONSTANT || ! cuddIsConstant ( t ) ) { cuddCacheInsert2 ( dd , Cudd_addEvalConst , f , g , DD_NON_CONSTANT ) ; return ( DD_NON_CONSTANT ) ; } if ( Fnv != zero ) { e = Cudd_addEvalConst ( dd , Fnv , Gnv ) ; if ( e == DD_NON_CONSTANT || ! cuddIsConstant ( e ) || t != e ) { cuddCacheInsert2 ( dd , Cudd_addEvalConst , f , g , DD_NON_CONSTANT ) ; return ( DD_NON_CONSTANT ) ; } } cuddCacheInsert2 ( dd , Cudd_addEvalConst , f , g , t ) ; return ( t ) ; } else { e = Cudd_addEvalConst ( dd , Fnv , Gnv ) ; cuddCacheInsert2 ( dd , Cudd_addEvalConst , f , g , e ) ; return ( e ) ; } }
Function
Synopsis    [Checks whether ADD g is constant whenever ADD f is 1.]
Function Synopsis [ Checks whether ADD g is constant whenever ADD f is 1 . ]
/* Terminal cases. */ /* From now on, f and g are known not to be constants. */ /* Check cache. */ /* Compute cofactors. */ /* Recursive step. */ /* Fnv must be != zero */