abc70930: src/bdd/cudd/cuddAddIte.c Source File

00001 
00036 #include "util_hack.h"
00037 #include "cuddInt.h"
00038 
00039 /*---------------------------------------------------------------------------*/
00040 /* Constant declarations                                                     */
00041 /*---------------------------------------------------------------------------*/
00042 
00043 
00044 /*---------------------------------------------------------------------------*/
00045 /* Stucture declarations                                                     */
00046 /*---------------------------------------------------------------------------*/
00047 
00048 
00049 /*---------------------------------------------------------------------------*/
00050 /* Type declarations                                                         */
00051 /*---------------------------------------------------------------------------*/
00052 
00053 
00054 /*---------------------------------------------------------------------------*/
00055 /* Variable declarations                                                     */
00056 /*---------------------------------------------------------------------------*/
00057 
00058 #ifndef lint
00059 static char rcsid[] DD_UNUSED = "$Id: cuddAddIte.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $";
00060 #endif
00061 
00062 
00063 /*---------------------------------------------------------------------------*/
00064 /* Macro declarations                                                        */
00065 /*---------------------------------------------------------------------------*/
00066 
00067 
00070 /*---------------------------------------------------------------------------*/
00071 /* Static function prototypes                                                */
00072 /*---------------------------------------------------------------------------*/
00073 
00074 static void addVarToConst ARGS((DdNode *f, DdNode **gp, DdNode **hp, DdNode *one, DdNode *zero));
00075 
00079 /*---------------------------------------------------------------------------*/
00080 /* Definition of exported functions                                          */
00081 /*---------------------------------------------------------------------------*/
00082 
00083 
00097 DdNode *
00098 Cudd_addIte(
00099   DdManager * dd,
00100   DdNode * f,
00101   DdNode * g,
00102   DdNode * h)
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 */
00113 
00114 
00131 DdNode *
00132 Cudd_addIteConstant(
00133   DdManager * dd,
00134   DdNode * f,
00135   DdNode * g,
00136   DdNode * h)
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 */
00211 
00212 
00228 DdNode *
00229 Cudd_addEvalConst(
00230   DdManager * dd,
00231   DdNode * f,
00232   DdNode * g)
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 */
00300 
00301 
00315 DdNode *
00316 Cudd_addCmpl(
00317   DdManager * dd,
00318   DdNode * f)
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 */
00329 
00330 
00344 int
00345 Cudd_addLeq(
00346   DdManager * dd,
00347   DdNode * f,
00348   DdNode * g)
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 */
00394 
00395 
00396 /*---------------------------------------------------------------------------*/
00397 /* Definition of internal functions                                          */
00398 /*---------------------------------------------------------------------------*/
00399 
00400 
00414 DdNode *
00415 cuddAddIteRecur(
00416   DdManager * dd,
00417   DdNode * f,
00418   DdNode * g,
00419   DdNode * h)
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 */
00517 
00518 
00531 DdNode *
00532 cuddAddCmplRecur(
00533   DdManager * dd,
00534   DdNode * f)
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 */
00577 
00578 
00579 /*---------------------------------------------------------------------------*/
00580 /* Definition of static functions                                            */
00581 /*---------------------------------------------------------------------------*/
00582 
00583 
00594 static void
00595 addVarToConst(
00596   DdNode * f,
00597   DdNode ** gp,
00598   DdNode ** hp,
00599   DdNode * one,
00600   DdNode * zero)
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 */