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

  Synopsis    [Determines whether f is less than or equal to g.]

  Description [Returns 1 if f is less than or equal to g; 0 otherwise.
  No new nodes are created. This procedure works for arbitrary ADDs.
  For 0-1 ADDs Cudd_addEvalConst is more efficient.]

  SideEffects [None]

  SeeAlso     [Cudd_addIteConstant Cudd_addEvalConst Cudd_bddLeq]

******************************************************************************/
Function
Synopsis    [Determines whether f is less than or equal to g.]

Description [Returns 1 if f is less than or equal to g; 0 otherwise.
No new nodes are created. This procedure works for arbitrary ADDs.
For 0-1 ADDs Cudd_addEvalConst is more efficient.]




Function Synopsis [ Determines whether f is less than or equal to g . ] Description [ Returns 1 if f is less than or equal to g ; 0 otherwise . No new nodes are created . This procedure works for arbitrary ADDs . For 0 - 1 ADDs Cudd_addEvalConst is more efficient . ]
int
Cudd_addLeq(
  DdManager * dd,
  DdNode * f,
  DdNode * g)
{
    DdNode *tmp, *fv, *fvn, *gv, *gvn;
    unsigned int topf, topg, res;
    if (f == g) return(1);
    statLine(dd);
    if (cuddIsConstant(f)) {
        if (cuddIsConstant(g)) return(cuddV(f) <= cuddV(g));
        if (f == DD_MINUS_INFINITY(dd)) return(1);
        if (f == DD_PLUS_INFINITY(dd)) return(0); 
    }
    if (g == DD_PLUS_INFINITY(dd)) return(1);
    if (g == DD_MINUS_INFINITY(dd)) return(0); 
    tmp = cuddCacheLookup2(dd,(DD_CTFP)Cudd_addLeq,f,g);
    if (tmp != NULL) {
        return(tmp == DD_ONE(dd));
    }
    topf = cuddI(dd,f->index);
    topg = cuddI(dd,g->index);
    if (topf <= topg) {
        fv = cuddT(f); fvn = cuddE(f);
    } else {
        fv = fvn = f;
    }
    if (topg <= topf) {
        gv = cuddT(g); gvn = cuddE(g);
    } else {
        gv = gvn = g;
    }
    res = Cudd_addLeq(dd,fvn,gvn) && Cudd_addLeq(dd,fv,gv);
    cuddCacheInsert2(dd,(DD_CTFP) Cudd_addLeq,f,g,
                     Cudd_NotCond(DD_ONE(dd),res==0));
    return(res);
}
int Cudd_addLeq ( DdManager * dd , DdNode * f , DdNode * g ) { DdNode * tmp , * fv , * fvn , * gv , * gvn ; unsigned int topf , topg , res ; if ( f == g ) return ( 1 ) ; statLine ( dd ) ; if ( cuddIsConstant ( f ) ) { if ( cuddIsConstant ( g ) ) return ( cuddV ( f ) <= cuddV ( g ) ) ; if ( f == DD_MINUS_INFINITY ( dd ) ) return ( 1 ) ; if ( f == DD_PLUS_INFINITY ( dd ) ) return ( 0 ) ; } if ( g == DD_PLUS_INFINITY ( dd ) ) return ( 1 ) ; if ( g == DD_MINUS_INFINITY ( dd ) ) return ( 0 ) ; tmp = cuddCacheLookup2 ( dd , ( DD_CTFP ) Cudd_addLeq , f , g ) ; if ( tmp != NULL ) { return ( tmp == DD_ONE ( dd ) ) ; } topf = cuddI ( dd , f -> index ) ; topg = cuddI ( dd , g -> index ) ; if ( topf <= topg ) { fv = cuddT ( f ) ; fvn = cuddE ( f ) ; } else { fv = fvn = f ; } if ( topg <= topf ) { gv = cuddT ( g ) ; gvn = cuddE ( g ) ; } else { gv = gvn = g ; } res = Cudd_addLeq ( dd , fvn , gvn ) && Cudd_addLeq ( dd , fv , gv ) ; cuddCacheInsert2 ( dd , ( DD_CTFP ) Cudd_addLeq , f , g , Cudd_NotCond ( DD_ONE ( dd ) , res == 0 ) ) ; return ( res ) ; }
Function
Synopsis    [Determines whether f is less than or equal to g.]
Function Synopsis [ Determines whether f is less than or equal to g . ]
/* Terminal cases. */ /* since f != g */ /* since f != g */ /* Check cache. */ /* Compute cofactors. One of f and g is not constant. */ /* Store result in cache and return. */