glu-2.2: src/cuBdd/cuddAddIte.c Source File

00001 
00063 #include "util.h"
00064 #include "cuddInt.h"
00065 
00066 /*---------------------------------------------------------------------------*/
00067 /* Constant declarations                                                     */
00068 /*---------------------------------------------------------------------------*/
00069 
00070 
00071 /*---------------------------------------------------------------------------*/
00072 /* Stucture declarations                                                     */
00073 /*---------------------------------------------------------------------------*/
00074 
00075 
00076 /*---------------------------------------------------------------------------*/
00077 /* Type declarations                                                         */
00078 /*---------------------------------------------------------------------------*/
00079 
00080 
00081 /*---------------------------------------------------------------------------*/
00082 /* Variable declarations                                                     */
00083 /*---------------------------------------------------------------------------*/
00084 
00085 #ifndef lint
00086 static char rcsid[] DD_UNUSED = "$Id: cuddAddIte.c,v 1.15 2004/08/13 18:04:45 fabio Exp $";
00087 #endif
00088 
00089 
00090 /*---------------------------------------------------------------------------*/
00091 /* Macro declarations                                                        */
00092 /*---------------------------------------------------------------------------*/
00093 
00094 
00097 /*---------------------------------------------------------------------------*/
00098 /* Static function prototypes                                                */
00099 /*---------------------------------------------------------------------------*/
00100 
00101 static void addVarToConst (DdNode *f, DdNode **gp, DdNode **hp, DdNode *one, DdNode *zero);
00102 
00106 /*---------------------------------------------------------------------------*/
00107 /* Definition of exported functions                                          */
00108 /*---------------------------------------------------------------------------*/
00109 
00110 
00124 DdNode *
00125 Cudd_addIte(
00126   DdManager * dd,
00127   DdNode * f,
00128   DdNode * g,
00129   DdNode * h)
00130 {
00131     DdNode *res;
00132 
00133     do {
00134         dd->reordered = 0;
00135         res = cuddAddIteRecur(dd,f,g,h);
00136     } while (dd->reordered == 1);
00137     return(res);
00138 
00139 } /* end of Cudd_addIte */
00140 
00141 
00158 DdNode *
00159 Cudd_addIteConstant(
00160   DdManager * dd,
00161   DdNode * f,
00162   DdNode * g,
00163   DdNode * h)
00164 {
00165     DdNode *one,*zero;
00166     DdNode *Fv,*Fnv,*Gv,*Gnv,*Hv,*Hnv,*r,*t,*e;
00167     unsigned int topf,topg,toph,v;
00168 
00169     statLine(dd);
00170     /* Trivial cases. */
00171     if (f == (one = DD_ONE(dd))) {      /* ITE(1,G,H) = G */
00172         return(g);
00173     }
00174     if (f == (zero = DD_ZERO(dd))) {    /* ITE(0,G,H) = H */
00175         return(h);
00176     }
00177 
00178     /* From now on, f is known not to be a constant. */
00179     addVarToConst(f,&g,&h,one,zero);
00180 
00181     /* Check remaining one variable cases. */
00182     if (g == h) {                       /* ITE(F,G,G) = G */
00183         return(g);
00184     }
00185     if (cuddIsConstant(g) && cuddIsConstant(h)) {
00186         return(DD_NON_CONSTANT);
00187     }
00188 
00189     topf = cuddI(dd,f->index);
00190     topg = cuddI(dd,g->index);
00191     toph = cuddI(dd,h->index);
00192     v = ddMin(topg,toph);
00193 
00194     /* ITE(F,G,H) = (x,G,H) (non constant) if F = (x,1,0), x < top(G,H). */
00195     if (topf < v && cuddIsConstant(cuddT(f)) && cuddIsConstant(cuddE(f))) {
00196         return(DD_NON_CONSTANT);
00197     }
00198 
00199     /* Check cache. */
00200     r = cuddConstantLookup(dd,DD_ADD_ITE_CONSTANT_TAG,f,g,h);
00201     if (r != NULL) {
00202         return(r);
00203     }
00204 
00205     /* Compute cofactors. */
00206     if (topf <= v) {
00207         v = ddMin(topf,v);      /* v = top_var(F,G,H) */
00208         Fv = cuddT(f); Fnv = cuddE(f);
00209     } else {
00210         Fv = Fnv = f;
00211     }
00212     if (topg == v) {
00213         Gv = cuddT(g); Gnv = cuddE(g);
00214     } else {
00215         Gv = Gnv = g;
00216     }
00217     if (toph == v) {
00218         Hv = cuddT(h); Hnv = cuddE(h);
00219     } else {
00220         Hv = Hnv = h;
00221     }
00222     
00223     /* Recursive step. */
00224     t = Cudd_addIteConstant(dd,Fv,Gv,Hv);
00225     if (t == DD_NON_CONSTANT || !cuddIsConstant(t)) {
00226         cuddCacheInsert(dd, DD_ADD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT);
00227         return(DD_NON_CONSTANT);
00228     }
00229     e = Cudd_addIteConstant(dd,Fnv,Gnv,Hnv);
00230     if (e == DD_NON_CONSTANT || !cuddIsConstant(e) || t != e) {
00231         cuddCacheInsert(dd, DD_ADD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT);
00232         return(DD_NON_CONSTANT);
00233     }
00234     cuddCacheInsert(dd, DD_ADD_ITE_CONSTANT_TAG, f, g, h, t);
00235     return(t);
00236 
00237 } /* end of Cudd_addIteConstant */
00238 
00239 
00255 DdNode *
00256 Cudd_addEvalConst(
00257   DdManager * dd,
00258   DdNode * f,
00259   DdNode * g)
00260 {
00261     DdNode *zero;
00262     DdNode *Fv,*Fnv,*Gv,*Gnv,*r,*t,*e;
00263     unsigned int topf,topg;
00264 
00265 #ifdef DD_DEBUG
00266     assert(!Cudd_IsComplement(f));
00267 #endif
00268 
00269     statLine(dd);
00270     /* Terminal cases. */
00271     if (f == DD_ONE(dd) || cuddIsConstant(g)) {
00272         return(g);
00273     }
00274     if (f == (zero = DD_ZERO(dd))) {
00275         return(dd->background);
00276     }
00277 
00278 #ifdef DD_DEBUG
00279     assert(!cuddIsConstant(f));
00280 #endif
00281     /* From now on, f and g are known not to be constants. */
00282 
00283     topf = cuddI(dd,f->index);
00284     topg = cuddI(dd,g->index);
00285 
00286     /* Check cache. */
00287     r = cuddConstantLookup(dd,DD_ADD_EVAL_CONST_TAG,f,g,g);
00288     if (r != NULL) {
00289         return(r);
00290     }
00291 
00292     /* Compute cofactors. */
00293     if (topf <= topg) {
00294         Fv = cuddT(f); Fnv = cuddE(f);
00295     } else {
00296         Fv = Fnv = f;
00297     }
00298     if (topg <= topf) {
00299         Gv = cuddT(g); Gnv = cuddE(g);
00300     } else {
00301         Gv = Gnv = g;
00302     }
00303     
00304     /* Recursive step. */
00305     if (Fv != zero) {
00306         t = Cudd_addEvalConst(dd,Fv,Gv);
00307         if (t == DD_NON_CONSTANT || !cuddIsConstant(t)) {
00308             cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, DD_NON_CONSTANT);
00309             return(DD_NON_CONSTANT);
00310         }
00311         if (Fnv != zero) {
00312             e = Cudd_addEvalConst(dd,Fnv,Gnv);
00313             if (e == DD_NON_CONSTANT || !cuddIsConstant(e) || t != e) {
00314                 cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, DD_NON_CONSTANT);
00315                 return(DD_NON_CONSTANT);
00316             }
00317         }
00318         cuddCacheInsert2(dd,Cudd_addEvalConst,f,g,t);
00319         return(t);
00320     } else { /* Fnv must be != zero */
00321         e = Cudd_addEvalConst(dd,Fnv,Gnv);
00322         cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, e);
00323         return(e);
00324     }
00325 
00326 } /* end of Cudd_addEvalConst */
00327 
00328 
00342 DdNode *
00343 Cudd_addCmpl(
00344   DdManager * dd,
00345   DdNode * f)
00346 {
00347     DdNode *res;
00348 
00349     do {
00350         dd->reordered = 0;
00351         res = cuddAddCmplRecur(dd,f);
00352     } while (dd->reordered == 1);
00353     return(res);
00354 
00355 } /* end of Cudd_addCmpl */
00356 
00357 
00371 int
00372 Cudd_addLeq(
00373   DdManager * dd,
00374   DdNode * f,
00375   DdNode * g)
00376 {
00377     DdNode *tmp, *fv, *fvn, *gv, *gvn;
00378     unsigned int topf, topg, res;
00379 
00380     /* Terminal cases. */
00381     if (f == g) return(1);
00382 
00383     statLine(dd);
00384     if (cuddIsConstant(f)) {
00385         if (cuddIsConstant(g)) return(cuddV(f) <= cuddV(g));
00386         if (f == DD_MINUS_INFINITY(dd)) return(1);
00387         if (f == DD_PLUS_INFINITY(dd)) return(0); /* since f != g */
00388     }
00389     if (g == DD_PLUS_INFINITY(dd)) return(1);
00390     if (g == DD_MINUS_INFINITY(dd)) return(0); /* since f != g */
00391 
00392     /* Check cache. */
00393     tmp = cuddCacheLookup2(dd,(DD_CTFP)Cudd_addLeq,f,g);
00394     if (tmp != NULL) {
00395         return(tmp == DD_ONE(dd));
00396     }
00397 
00398     /* Compute cofactors. One of f and g is not constant. */
00399     topf = cuddI(dd,f->index);
00400     topg = cuddI(dd,g->index);
00401     if (topf <= topg) {
00402         fv = cuddT(f); fvn = cuddE(f);
00403     } else {
00404         fv = fvn = f;
00405     }
00406     if (topg <= topf) {
00407         gv = cuddT(g); gvn = cuddE(g);
00408     } else {
00409         gv = gvn = g;
00410     }
00411 
00412     res = Cudd_addLeq(dd,fvn,gvn) && Cudd_addLeq(dd,fv,gv);
00413 
00414     /* Store result in cache and return. */
00415     cuddCacheInsert2(dd,(DD_CTFP) Cudd_addLeq,f,g,
00416                      Cudd_NotCond(DD_ONE(dd),res==0));
00417     return(res);
00418 
00419 } /* end of Cudd_addLeq */
00420 
00421 
00422 /*---------------------------------------------------------------------------*/
00423 /* Definition of internal functions                                          */
00424 /*---------------------------------------------------------------------------*/
00425 
00426 
00440 DdNode *
00441 cuddAddIteRecur(
00442   DdManager * dd,
00443   DdNode * f,
00444   DdNode * g,
00445   DdNode * h)
00446 {
00447     DdNode *one,*zero;
00448     DdNode *r,*Fv,*Fnv,*Gv,*Gnv,*Hv,*Hnv,*t,*e;
00449     unsigned int topf,topg,toph,v;
00450     int index;
00451 
00452     statLine(dd);
00453     /* Trivial cases. */
00454 
00455     /* One variable cases. */
00456     if (f == (one = DD_ONE(dd))) {      /* ITE(1,G,H) = G */
00457         return(g);
00458     }
00459     if (f == (zero = DD_ZERO(dd))) {    /* ITE(0,G,H) = H */
00460         return(h);
00461     }
00462 
00463     /* From now on, f is known to not be a constant. */
00464     addVarToConst(f,&g,&h,one,zero);
00465 
00466     /* Check remaining one variable cases. */
00467     if (g == h) {                       /* ITE(F,G,G) = G */
00468         return(g);
00469     }
00470 
00471     if (g == one) {                     /* ITE(F,1,0) = F */
00472         if (h == zero) return(f);
00473     }
00474 
00475     topf = cuddI(dd,f->index);
00476     topg = cuddI(dd,g->index);
00477     toph = cuddI(dd,h->index);
00478     v = ddMin(topg,toph);
00479 
00480     /* A shortcut: ITE(F,G,H) = (x,G,H) if F=(x,1,0), x < top(G,H). */
00481     if (topf < v && cuddT(f) == one && cuddE(f) == zero) {
00482         r = cuddUniqueInter(dd,(int)f->index,g,h);
00483         return(r);
00484     }
00485     if (topf < v && cuddT(f) == zero && cuddE(f) == one) {
00486         r = cuddUniqueInter(dd,(int)f->index,h,g);
00487         return(r);
00488     }
00489 
00490     /* Check cache. */
00491     r = cuddCacheLookup(dd,DD_ADD_ITE_TAG,f,g,h);
00492     if (r != NULL) {
00493         return(r);
00494     }
00495 
00496     /* Compute cofactors. */
00497     if (topf <= v) {
00498         v = ddMin(topf,v);      /* v = top_var(F,G,H) */
00499         index = f->index;
00500         Fv = cuddT(f); Fnv = cuddE(f);
00501     } else {
00502         Fv = Fnv = f;
00503     }
00504     if (topg == v) {
00505         index = g->index;
00506         Gv = cuddT(g); Gnv = cuddE(g);
00507     } else {
00508         Gv = Gnv = g;
00509     }
00510     if (toph == v) {
00511         index = h->index;
00512         Hv = cuddT(h); Hnv = cuddE(h);
00513     } else {
00514         Hv = Hnv = h;
00515     }
00516     
00517     /* Recursive step. */
00518     t = cuddAddIteRecur(dd,Fv,Gv,Hv);
00519     if (t == NULL) return(NULL);
00520     cuddRef(t);
00521 
00522     e = cuddAddIteRecur(dd,Fnv,Gnv,Hnv);
00523     if (e == NULL) {
00524         Cudd_RecursiveDeref(dd,t);
00525         return(NULL);
00526     }
00527     cuddRef(e);
00528 
00529     r = (t == e) ? t : cuddUniqueInter(dd,index,t,e);
00530     if (r == NULL) {
00531         Cudd_RecursiveDeref(dd,t);
00532         Cudd_RecursiveDeref(dd,e);
00533         return(NULL);
00534     }
00535     cuddDeref(t);
00536     cuddDeref(e);
00537 
00538     cuddCacheInsert(dd,DD_ADD_ITE_TAG,f,g,h,r);
00539 
00540     return(r);
00541 
00542 } /* end of cuddAddIteRecur */
00543 
00544 
00557 DdNode *
00558 cuddAddCmplRecur(
00559   DdManager * dd,
00560   DdNode * f)
00561 {
00562     DdNode *one,*zero;
00563     DdNode *r,*Fv,*Fnv,*t,*e;
00564 
00565     statLine(dd);
00566     one = DD_ONE(dd);
00567     zero = DD_ZERO(dd); 
00568 
00569     if (cuddIsConstant(f)) {
00570         if (f == zero) {
00571             return(one);
00572         } else {
00573             return(zero);
00574         }
00575     }
00576     r = cuddCacheLookup1(dd,Cudd_addCmpl,f);
00577     if (r != NULL) {
00578         return(r);
00579     }
00580     Fv = cuddT(f);
00581     Fnv = cuddE(f);
00582     t = cuddAddCmplRecur(dd,Fv);
00583     if (t == NULL) return(NULL);
00584     cuddRef(t);
00585     e = cuddAddCmplRecur(dd,Fnv);
00586     if (e == NULL) {
00587         Cudd_RecursiveDeref(dd,t);
00588         return(NULL);
00589     }
00590     cuddRef(e);
00591     r = (t == e) ? t : cuddUniqueInter(dd,(int)f->index,t,e);
00592     if (r == NULL) {
00593         Cudd_RecursiveDeref(dd, t);
00594         Cudd_RecursiveDeref(dd, e);
00595         return(NULL);
00596     }
00597     cuddDeref(t);
00598     cuddDeref(e);
00599     cuddCacheInsert1(dd,Cudd_addCmpl,f,r);
00600     return(r);
00601 
00602 } /* end of cuddAddCmplRecur */
00603 
00604 
00605 /*---------------------------------------------------------------------------*/
00606 /* Definition of static functions                                            */
00607 /*---------------------------------------------------------------------------*/
00608 
00609 
00620 static void
00621 addVarToConst(
00622   DdNode * f,
00623   DdNode ** gp,
00624   DdNode ** hp,
00625   DdNode * one,
00626   DdNode * zero)
00627 {
00628     DdNode *g = *gp;
00629     DdNode *h = *hp;
00630 
00631     if (f == g) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */
00632         *gp = one;
00633     }
00634 
00635     if (f == h) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */
00636         *hp = zero;
00637     }
00638 
00639 } /* end of addVarToConst */