src/bdd/cudd/cuddAddIte.c File Reference

#include "util_hack.h"
#include "cuddInt.h"
Include dependency graph for cuddAddIte.c:

Go to the source code of this file.

Functions

static void addVarToConst ARGS ((DdNode *f, DdNode **gp, DdNode **hp, DdNode *one, DdNode *zero))
DdNode * Cudd_addIte (DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
DdNode * Cudd_addIteConstant (DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
DdNode * Cudd_addEvalConst (DdManager *dd, DdNode *f, DdNode *g)
DdNode * Cudd_addCmpl (DdManager *dd, DdNode *f)
int Cudd_addLeq (DdManager *dd, DdNode *f, DdNode *g)
DdNode * cuddAddIteRecur (DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
DdNode * cuddAddCmplRecur (DdManager *dd, DdNode *f)
static void addVarToConst (DdNode *f, DdNode **gp, DdNode **hp, DdNode *one, DdNode *zero)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddAddIte.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $"

Function Documentation

static void addVarToConst ( DdNode *  f,
DdNode **  gp,
DdNode **  hp,
DdNode *  one,
DdNode *  zero 
) [static]

Function********************************************************************

Synopsis [Replaces variables with constants if possible (part of canonical form).]

Description []

SideEffects [None]

Definition at line 595 of file cuddAddIte.c.

00601 {
00602     DdNode *g = *gp;
00603     DdNode *h = *hp;
00604 
00605     if (f == g) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */
00606         *gp = one;
00607     }
00608 
00609     if (f == h) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */
00610         *hp = zero;
00611     }
00612 
00613 } /* end of addVarToConst */

static void addVarToConst ARGS ( (DdNode *f, DdNode **gp, DdNode **hp, DdNode *one, DdNode *zero)   )  [static]

AutomaticStart

DdNode* Cudd_addCmpl ( DdManager *  dd,
DdNode *  f 
)

Function********************************************************************

Synopsis [Computes the complement of an ADD a la C language.]

Description [Computes the complement of an ADD a la C language: The complement of 0 is 1 and the complement of everything else is 0. Returns a pointer to the resulting ADD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_addNegate]

Definition at line 316 of file cuddAddIte.c.

00319 {
00320     DdNode *res;
00321 
00322     do {
00323         dd->reordered = 0;
00324         res = cuddAddCmplRecur(dd,f);
00325     } while (dd->reordered == 1);
00326     return(res);
00327 
00328 } /* end of Cudd_addCmpl */

DdNode* Cudd_addEvalConst ( DdManager *  dd,
DdNode *  f,
DdNode *  g 
)

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]

Definition at line 229 of file cuddAddIte.c.

00233 {
00234     DdNode *zero;
00235     DdNode *Fv,*Fnv,*Gv,*Gnv,*r,*t,*e;
00236     unsigned int topf,topg;
00237 
00238 #ifdef DD_DEBUG
00239     assert(!Cudd_IsComplement(f));
00240 #endif
00241 
00242     statLine(dd);
00243     /* Terminal cases. */
00244     if (f == DD_ONE(dd) || cuddIsConstant(g)) {
00245         return(g);
00246     }
00247     if (f == (zero = DD_ZERO(dd))) {
00248         return(dd->background);
00249     }
00250 
00251 #ifdef DD_DEBUG
00252     assert(!cuddIsConstant(f));
00253 #endif
00254     /* From now on, f and g are known not to be constants. */
00255 
00256     topf = cuddI(dd,f->index);
00257     topg = cuddI(dd,g->index);
00258 
00259     /* Check cache. */
00260     r = cuddConstantLookup(dd,DD_ADD_EVAL_CONST_TAG,f,g,g);
00261     if (r != NULL) {
00262         return(r);
00263     }
00264 
00265     /* Compute cofactors. */
00266     if (topf <= topg) {
00267         Fv = cuddT(f); Fnv = cuddE(f);
00268     } else {
00269         Fv = Fnv = f;
00270     }
00271     if (topg <= topf) {
00272         Gv = cuddT(g); Gnv = cuddE(g);
00273     } else {
00274         Gv = Gnv = g;
00275     }
00276     
00277     /* Recursive step. */
00278     if (Fv != zero) {
00279         t = Cudd_addEvalConst(dd,Fv,Gv);
00280         if (t == DD_NON_CONSTANT || !cuddIsConstant(t)) {
00281             cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, DD_NON_CONSTANT);
00282             return(DD_NON_CONSTANT);
00283         }
00284         if (Fnv != zero) {
00285             e = Cudd_addEvalConst(dd,Fnv,Gnv);
00286             if (e == DD_NON_CONSTANT || !cuddIsConstant(e) || t != e) {
00287                 cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, DD_NON_CONSTANT);
00288                 return(DD_NON_CONSTANT);
00289             }
00290         }
00291         cuddCacheInsert2(dd,Cudd_addEvalConst,f,g,t);
00292         return(t);
00293     } else { /* Fnv must be != zero */
00294         e = Cudd_addEvalConst(dd,Fnv,Gnv);
00295         cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, e);
00296         return(e);
00297     }
00298 
00299 } /* end of Cudd_addEvalConst */

DdNode* Cudd_addIte ( DdManager *  dd,
DdNode *  f,
DdNode *  g,
DdNode *  h 
)

AutomaticEnd Function********************************************************************

Synopsis [Implements ITE(f,g,h).]

Description [Implements ITE(f,g,h). This procedure assumes that f is a 0-1 ADD. Returns a pointer to the resulting ADD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_bddIte Cudd_addIteConstant Cudd_addApply]

Definition at line 98 of file cuddAddIte.c.

00103 {
00104     DdNode *res;
00105 
00106     do {
00107         dd->reordered = 0;
00108         res = cuddAddIteRecur(dd,f,g,h);
00109     } while (dd->reordered == 1);
00110     return(res);
00111 
00112 } /* end of Cudd_addIte */

DdNode* Cudd_addIteConstant ( DdManager *  dd,
DdNode *  f,
DdNode *  g,
DdNode *  h 
)

Function********************************************************************

Synopsis [Implements ITEconstant for ADDs.]

Description [Implements ITEconstant for ADDs. 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. No new nodes are created. This function can be used, for instance, to check that g has a constant value (specified by h) whenever f is 1. If the constant value is unknown, then one should use Cudd_addEvalConst.]

SideEffects [None]

SeeAlso [Cudd_addIte Cudd_addEvalConst Cudd_bddIteConstant]

Definition at line 132 of file cuddAddIte.c.

00137 {
00138     DdNode *one,*zero;
00139     DdNode *Fv,*Fnv,*Gv,*Gnv,*Hv,*Hnv,*r,*t,*e;
00140     unsigned int topf,topg,toph,v;
00141 
00142     statLine(dd);
00143     /* Trivial cases. */
00144     if (f == (one = DD_ONE(dd))) {      /* ITE(1,G,H) = G */
00145         return(g);
00146     }
00147     if (f == (zero = DD_ZERO(dd))) {    /* ITE(0,G,H) = H */
00148         return(h);
00149     }
00150 
00151     /* From now on, f is known not to be a constant. */
00152     addVarToConst(f,&g,&h,one,zero);
00153 
00154     /* Check remaining one variable cases. */
00155     if (g == h) {                       /* ITE(F,G,G) = G */
00156         return(g);
00157     }
00158     if (cuddIsConstant(g) && cuddIsConstant(h)) {
00159         return(DD_NON_CONSTANT);
00160     }
00161 
00162     topf = cuddI(dd,f->index);
00163     topg = cuddI(dd,g->index);
00164     toph = cuddI(dd,h->index);
00165     v = ddMin(topg,toph);
00166 
00167     /* ITE(F,G,H) = (x,G,H) (non constant) if F = (x,1,0), x < top(G,H). */
00168     if (topf < v && cuddIsConstant(cuddT(f)) && cuddIsConstant(cuddE(f))) {
00169         return(DD_NON_CONSTANT);
00170     }
00171 
00172     /* Check cache. */
00173     r = cuddConstantLookup(dd,DD_ADD_ITE_CONSTANT_TAG,f,g,h);
00174     if (r != NULL) {
00175         return(r);
00176     }
00177 
00178     /* Compute cofactors. */
00179     if (topf <= v) {
00180         v = ddMin(topf,v);      /* v = top_var(F,G,H) */
00181         Fv = cuddT(f); Fnv = cuddE(f);
00182     } else {
00183         Fv = Fnv = f;
00184     }
00185     if (topg == v) {
00186         Gv = cuddT(g); Gnv = cuddE(g);
00187     } else {
00188         Gv = Gnv = g;
00189     }
00190     if (toph == v) {
00191         Hv = cuddT(h); Hnv = cuddE(h);
00192     } else {
00193         Hv = Hnv = h;
00194     }
00195     
00196     /* Recursive step. */
00197     t = Cudd_addIteConstant(dd,Fv,Gv,Hv);
00198     if (t == DD_NON_CONSTANT || !cuddIsConstant(t)) {
00199         cuddCacheInsert(dd, DD_ADD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT);
00200         return(DD_NON_CONSTANT);
00201     }
00202     e = Cudd_addIteConstant(dd,Fnv,Gnv,Hnv);
00203     if (e == DD_NON_CONSTANT || !cuddIsConstant(e) || t != e) {
00204         cuddCacheInsert(dd, DD_ADD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT);
00205         return(DD_NON_CONSTANT);
00206     }
00207     cuddCacheInsert(dd, DD_ADD_ITE_CONSTANT_TAG, f, g, h, t);
00208     return(t);
00209 
00210 } /* end of Cudd_addIteConstant */

int Cudd_addLeq ( DdManager *  dd,
DdNode *  f,
DdNode *  g 
)

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]

Definition at line 345 of file cuddAddIte.c.

00349 {
00350     DdNode *tmp, *fv, *fvn, *gv, *gvn;
00351     unsigned int topf, topg, res;
00352 
00353     /* Terminal cases. */
00354     if (f == g) return(1);
00355 
00356     statLine(dd);
00357     if (cuddIsConstant(f)) {
00358         if (cuddIsConstant(g)) return(cuddV(f) <= cuddV(g));
00359         if (f == DD_MINUS_INFINITY(dd)) return(1);
00360         if (f == DD_PLUS_INFINITY(dd)) return(0); /* since f != g */
00361     }
00362     if (g == DD_PLUS_INFINITY(dd)) return(1);
00363     if (g == DD_MINUS_INFINITY(dd)) return(0); /* since f != g */
00364 
00365     /* Check cache. */
00366     tmp = cuddCacheLookup2(dd,(DdNode * (*)(DdManager *, DdNode *,
00367                            DdNode *))Cudd_addLeq,f,g);
00368     if (tmp != NULL) {
00369         return(tmp == DD_ONE(dd));
00370     }
00371 
00372     /* Compute cofactors. One of f and g is not constant. */
00373     topf = cuddI(dd,f->index);
00374     topg = cuddI(dd,g->index);
00375     if (topf <= topg) {
00376         fv = cuddT(f); fvn = cuddE(f);
00377     } else {
00378         fv = fvn = f;
00379     }
00380     if (topg <= topf) {
00381         gv = cuddT(g); gvn = cuddE(g);
00382     } else {
00383         gv = gvn = g;
00384     }
00385 
00386     res = Cudd_addLeq(dd,fvn,gvn) && Cudd_addLeq(dd,fv,gv);
00387 
00388     /* Store result in cache and return. */
00389     cuddCacheInsert2(dd,(DdNode * (*)(DdManager *, DdNode *, DdNode *))
00390                      Cudd_addLeq,f,g,Cudd_NotCond(DD_ONE(dd),res==0));
00391     return(res);
00392 
00393 } /* end of Cudd_addLeq */

DdNode* cuddAddCmplRecur ( DdManager *  dd,
DdNode *  f 
)

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_addCmpl.]

Description [Performs the recursive step of Cudd_addCmpl. Returns a pointer to the resulting ADD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_addCmpl]

Definition at line 532 of file cuddAddIte.c.

00535 {
00536     DdNode *one,*zero;
00537     DdNode *r,*Fv,*Fnv,*t,*e;
00538 
00539     statLine(dd);
00540     one = DD_ONE(dd);
00541     zero = DD_ZERO(dd); 
00542 
00543     if (cuddIsConstant(f)) {
00544         if (f == zero) {
00545             return(one);
00546         } else {
00547             return(zero);
00548         }
00549     }
00550     r = cuddCacheLookup1(dd,Cudd_addCmpl,f);
00551     if (r != NULL) {
00552         return(r);
00553     }
00554     Fv = cuddT(f);
00555     Fnv = cuddE(f);
00556     t = cuddAddCmplRecur(dd,Fv);
00557     if (t == NULL) return(NULL);
00558     cuddRef(t);
00559     e = cuddAddCmplRecur(dd,Fnv);
00560     if (e == NULL) {
00561         Cudd_RecursiveDeref(dd,t);
00562         return(NULL);
00563     }
00564     cuddRef(e);
00565     r = (t == e) ? t : cuddUniqueInter(dd,(int)f->index,t,e);
00566     if (r == NULL) {
00567         Cudd_RecursiveDeref(dd, t);
00568         Cudd_RecursiveDeref(dd, e);
00569         return(NULL);
00570     }
00571     cuddDeref(t);
00572     cuddDeref(e);
00573     cuddCacheInsert1(dd,Cudd_addCmpl,f,r);
00574     return(r);
00575 
00576 } /* end of cuddAddCmplRecur */

DdNode* cuddAddIteRecur ( DdManager *  dd,
DdNode *  f,
DdNode *  g,
DdNode *  h 
)

Function********************************************************************

Synopsis [Implements the recursive step of Cudd_addIte(f,g,h).]

Description [Implements the recursive step of Cudd_addIte(f,g,h). Returns a pointer to the resulting ADD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_addIte]

Definition at line 415 of file cuddAddIte.c.

00420 {
00421     DdNode *one,*zero;
00422     DdNode *r,*Fv,*Fnv,*Gv,*Gnv,*Hv,*Hnv,*t,*e;
00423     unsigned int topf,topg,toph,v;
00424     int index;
00425 
00426     statLine(dd);
00427     /* Trivial cases. */
00428 
00429     /* One variable cases. */
00430     if (f == (one = DD_ONE(dd))) {      /* ITE(1,G,H) = G */
00431         return(g);
00432     }
00433     if (f == (zero = DD_ZERO(dd))) {    /* ITE(0,G,H) = H */
00434         return(h);
00435     }
00436 
00437     /* From now on, f is known to not be a constant. */
00438     addVarToConst(f,&g,&h,one,zero);
00439 
00440     /* Check remaining one variable cases. */
00441     if (g == h) {                       /* ITE(F,G,G) = G */
00442         return(g);
00443     }
00444 
00445     if (g == one) {                     /* ITE(F,1,0) = F */
00446         if (h == zero) return(f);
00447     }
00448 
00449     topf = cuddI(dd,f->index);
00450     topg = cuddI(dd,g->index);
00451     toph = cuddI(dd,h->index);
00452     v = ddMin(topg,toph);
00453 
00454     /* A shortcut: ITE(F,G,H) = (x,G,H) if F=(x,1,0), x < top(G,H). */
00455     if (topf < v && cuddT(f) == one && cuddE(f) == zero) {
00456         r = cuddUniqueInter(dd,(int)f->index,g,h);
00457         return(r);
00458     }
00459     if (topf < v && cuddT(f) == zero && cuddE(f) == one) {
00460         r = cuddUniqueInter(dd,(int)f->index,h,g);
00461         return(r);
00462     }
00463 
00464     /* Check cache. */
00465     r = cuddCacheLookup(dd,DD_ADD_ITE_TAG,f,g,h);
00466     if (r != NULL) {
00467         return(r);
00468     }
00469 
00470     /* Compute cofactors. */
00471     if (topf <= v) {
00472         v = ddMin(topf,v);      /* v = top_var(F,G,H) */
00473         index = f->index;
00474         Fv = cuddT(f); Fnv = cuddE(f);
00475     } else {
00476         Fv = Fnv = f;
00477     }
00478     if (topg == v) {
00479         index = g->index;
00480         Gv = cuddT(g); Gnv = cuddE(g);
00481     } else {
00482         Gv = Gnv = g;
00483     }
00484     if (toph == v) {
00485         index = h->index;
00486         Hv = cuddT(h); Hnv = cuddE(h);
00487     } else {
00488         Hv = Hnv = h;
00489     }
00490     
00491     /* Recursive step. */
00492     t = cuddAddIteRecur(dd,Fv,Gv,Hv);
00493     if (t == NULL) return(NULL);
00494     cuddRef(t);
00495 
00496     e = cuddAddIteRecur(dd,Fnv,Gnv,Hnv);
00497     if (e == NULL) {
00498         Cudd_RecursiveDeref(dd,t);
00499         return(NULL);
00500     }
00501     cuddRef(e);
00502 
00503     r = (t == e) ? t : cuddUniqueInter(dd,index,t,e);
00504     if (r == NULL) {
00505         Cudd_RecursiveDeref(dd,t);
00506         Cudd_RecursiveDeref(dd,e);
00507         return(NULL);
00508     }
00509     cuddDeref(t);
00510     cuddDeref(e);
00511 
00512     cuddCacheInsert(dd,DD_ADD_ITE_TAG,f,g,h,r);
00513 
00514     return(r);
00515 
00516 } /* end of cuddAddIteRecur */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddAddIte.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $" [static]

CFile***********************************************************************

FileName [cuddAddIte.c]

PackageName [cudd]

Synopsis [ADD ITE function and satellites.]

Description [External procedures included in this module:

Internal procedures included in this module:

Static procedures included in this module:

]

Author [Fabio Somenzi]

Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]

Definition at line 59 of file cuddAddIte.c.

Generated on Tue Jan 5 12:18:52 2010 for abc70930 by  doxygen 1.6.1