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

00001 
00075 #include "util.h"
00076 #include "cuddInt.h"
00077 
00078 
00079 /*---------------------------------------------------------------------------*/
00080 /* Constant declarations                                                     */
00081 /*---------------------------------------------------------------------------*/
00082 
00083 
00084 /*---------------------------------------------------------------------------*/
00085 /* Stucture declarations                                                     */
00086 /*---------------------------------------------------------------------------*/
00087 
00088 
00089 /*---------------------------------------------------------------------------*/
00090 /* Type declarations                                                         */
00091 /*---------------------------------------------------------------------------*/
00092 
00093 
00094 /*---------------------------------------------------------------------------*/
00095 /* Variable declarations                                                     */
00096 /*---------------------------------------------------------------------------*/
00097 
00098 #ifndef lint
00099 static char rcsid[] DD_UNUSED = "$Id: cuddBddIte.c,v 1.24 2004/08/13 18:04:46 fabio Exp $";
00100 #endif
00101 
00102 /*---------------------------------------------------------------------------*/
00103 /* Macro declarations                                                        */
00104 /*---------------------------------------------------------------------------*/
00105 
00106 
00109 /*---------------------------------------------------------------------------*/
00110 /* Static function prototypes                                                */
00111 /*---------------------------------------------------------------------------*/
00112 
00113 static void bddVarToConst (DdNode *f, DdNode **gp, DdNode **hp, DdNode *one);
00114 static int bddVarToCanonical (DdManager *dd, DdNode **fp, DdNode **gp, DdNode **hp, unsigned int *topfp, unsigned int *topgp, unsigned int *tophp);
00115 static int bddVarToCanonicalSimple (DdManager *dd, DdNode **fp, DdNode **gp, DdNode **hp, unsigned int *topfp, unsigned int *topgp, unsigned int *tophp);
00116 
00120 /*---------------------------------------------------------------------------*/
00121 /* Definition of exported functions                                          */
00122 /*---------------------------------------------------------------------------*/
00123 
00124 
00138 DdNode *
00139 Cudd_bddIte(
00140   DdManager * dd,
00141   DdNode * f,
00142   DdNode * g,
00143   DdNode * h)
00144 {
00145     DdNode *res;
00146 
00147     do {
00148         dd->reordered = 0;
00149         res = cuddBddIteRecur(dd,f,g,h);
00150     } while (dd->reordered == 1);
00151     return(res);
00152 
00153 } /* end of Cudd_bddIte */
00154 
00155 
00169 DdNode *
00170 Cudd_bddIteConstant(
00171   DdManager * dd,
00172   DdNode * f,
00173   DdNode * g,
00174   DdNode * h)
00175 {
00176     DdNode       *r, *Fv, *Fnv, *Gv, *Gnv, *H, *Hv, *Hnv, *t, *e;
00177     DdNode       *one = DD_ONE(dd);
00178     DdNode       *zero = Cudd_Not(one);
00179     int          comple;
00180     unsigned int topf, topg, toph, v;
00181 
00182     statLine(dd);
00183     /* Trivial cases. */
00184     if (f == one)                       /* ITE(1,G,H) => G */
00185         return(g);
00186     
00187     if (f == zero)                      /* ITE(0,G,H) => H */
00188         return(h);
00189     
00190     /* f now not a constant. */
00191     bddVarToConst(f, &g, &h, one);      /* possibly convert g or h */
00192                                         /* to constants */
00193 
00194     if (g == h)                         /* ITE(F,G,G) => G */
00195         return(g);
00196 
00197     if (Cudd_IsConstant(g) && Cudd_IsConstant(h)) 
00198         return(DD_NON_CONSTANT);        /* ITE(F,1,0) or ITE(F,0,1) */
00199                                         /* => DD_NON_CONSTANT */
00200     
00201     if (g == Cudd_Not(h))
00202         return(DD_NON_CONSTANT);        /* ITE(F,G,G') => DD_NON_CONSTANT */
00203                                         /* if F != G and F != G' */
00204     
00205     comple = bddVarToCanonical(dd, &f, &g, &h, &topf, &topg, &toph);
00206 
00207     /* Cache lookup. */
00208     r = cuddConstantLookup(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h);
00209     if (r != NULL) {
00210         return(Cudd_NotCond(r,comple && r != DD_NON_CONSTANT));
00211     }
00212 
00213     v = ddMin(topg, toph);
00214 
00215     /* ITE(F,G,H) = (v,G,H) (non constant) if F = (v,1,0), v < top(G,H). */
00216     if (topf < v && cuddT(f) == one && cuddE(f) == zero) {
00217         return(DD_NON_CONSTANT);
00218     }
00219 
00220     /* Compute cofactors. */
00221     if (topf <= v) {
00222         v = ddMin(topf, v);             /* v = top_var(F,G,H) */
00223         Fv = cuddT(f); Fnv = cuddE(f);
00224     } else {
00225         Fv = Fnv = f;
00226     }
00227 
00228     if (topg == v) {
00229         Gv = cuddT(g); Gnv = cuddE(g);
00230     } else {
00231         Gv = Gnv = g;
00232     }
00233 
00234     if (toph == v) {
00235         H = Cudd_Regular(h);
00236         Hv = cuddT(H); Hnv = cuddE(H);
00237         if (Cudd_IsComplement(h)) {
00238             Hv = Cudd_Not(Hv);
00239             Hnv = Cudd_Not(Hnv);
00240         }
00241     } else {
00242         Hv = Hnv = h;
00243     }
00244 
00245     /* Recursion. */
00246     t = Cudd_bddIteConstant(dd, Fv, Gv, Hv);
00247     if (t == DD_NON_CONSTANT || !Cudd_IsConstant(t)) {
00248         cuddCacheInsert(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT);
00249         return(DD_NON_CONSTANT);
00250     }
00251     e = Cudd_bddIteConstant(dd, Fnv, Gnv, Hnv);
00252     if (e == DD_NON_CONSTANT || !Cudd_IsConstant(e) || t != e) {
00253         cuddCacheInsert(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT);
00254         return(DD_NON_CONSTANT);
00255     }
00256     cuddCacheInsert(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h, t);
00257     return(Cudd_NotCond(t,comple));
00258 
00259 } /* end of Cudd_bddIteConstant */
00260 
00261 
00277 DdNode *
00278 Cudd_bddIntersect(
00279   DdManager * dd /* manager */,
00280   DdNode * f /* first operand */,
00281   DdNode * g /* second operand */)
00282 {
00283     DdNode *res;
00284 
00285     do {
00286         dd->reordered = 0;
00287         res = cuddBddIntersectRecur(dd,f,g);
00288     } while (dd->reordered == 1);
00289 
00290     return(res);
00291 
00292 } /* end of Cudd_bddIntersect */
00293 
00294 
00309 DdNode *
00310 Cudd_bddAnd(
00311   DdManager * dd,
00312   DdNode * f,
00313   DdNode * g)
00314 {
00315     DdNode *res;
00316 
00317     do {
00318         dd->reordered = 0;
00319         res = cuddBddAndRecur(dd,f,g);
00320     } while (dd->reordered == 1);
00321     return(res);
00322 
00323 } /* end of Cudd_bddAnd */
00324 
00325 
00341 DdNode *
00342 Cudd_bddAndLimit(
00343   DdManager * dd,
00344   DdNode * f,
00345   DdNode * g,
00346   unsigned int limit)
00347 {
00348     DdNode *res;
00349     unsigned int saveLimit = dd->maxLive;
00350 
00351     dd->maxLive = (dd->keys - dd->dead) + (dd->keysZ - dd->deadZ) + limit;
00352     do {
00353         dd->reordered = 0;
00354         res = cuddBddAndRecur(dd,f,g);
00355     } while (dd->reordered == 1);
00356     dd->maxLive = saveLimit;
00357     return(res);
00358 
00359 } /* end of Cudd_bddAndLimit */
00360 
00361 
00376 DdNode *
00377 Cudd_bddOr(
00378   DdManager * dd,
00379   DdNode * f,
00380   DdNode * g)
00381 {
00382     DdNode *res;
00383 
00384     do {
00385         dd->reordered = 0;
00386         res = cuddBddAndRecur(dd,Cudd_Not(f),Cudd_Not(g));
00387     } while (dd->reordered == 1);
00388     res = Cudd_NotCond(res,res != NULL);
00389     return(res);
00390 
00391 } /* end of Cudd_bddOr */
00392 
00393 
00408 DdNode *
00409 Cudd_bddNand(
00410   DdManager * dd,
00411   DdNode * f,
00412   DdNode * g)
00413 {
00414     DdNode *res;
00415 
00416     do {
00417         dd->reordered = 0;
00418         res = cuddBddAndRecur(dd,f,g);
00419     } while (dd->reordered == 1);
00420     res = Cudd_NotCond(res,res != NULL);
00421     return(res);
00422 
00423 } /* end of Cudd_bddNand */
00424 
00425 
00440 DdNode *
00441 Cudd_bddNor(
00442   DdManager * dd,
00443   DdNode * f,
00444   DdNode * g)
00445 {
00446     DdNode *res;
00447 
00448     do {
00449         dd->reordered = 0;
00450         res = cuddBddAndRecur(dd,Cudd_Not(f),Cudd_Not(g));
00451     } while (dd->reordered == 1);
00452     return(res);
00453 
00454 } /* end of Cudd_bddNor */
00455 
00456 
00471 DdNode *
00472 Cudd_bddXor(
00473   DdManager * dd,
00474   DdNode * f,
00475   DdNode * g)
00476 {
00477     DdNode *res;
00478 
00479     do {
00480         dd->reordered = 0;
00481         res = cuddBddXorRecur(dd,f,g);
00482     } while (dd->reordered == 1);
00483     return(res);
00484 
00485 } /* end of Cudd_bddXor */
00486 
00487 
00502 DdNode *
00503 Cudd_bddXnor(
00504   DdManager * dd,
00505   DdNode * f,
00506   DdNode * g)
00507 {
00508     DdNode *res;
00509 
00510     do {
00511         dd->reordered = 0;
00512         res = cuddBddXorRecur(dd,f,Cudd_Not(g));
00513     } while (dd->reordered == 1);
00514     return(res);
00515 
00516 } /* end of Cudd_bddXnor */
00517 
00518 
00531 int
00532 Cudd_bddLeq(
00533   DdManager * dd,
00534   DdNode * f,
00535   DdNode * g)
00536 {
00537     DdNode *one, *zero, *tmp, *F, *fv, *fvn, *gv, *gvn;
00538     unsigned int topf, topg, res;
00539 
00540     statLine(dd);
00541     /* Terminal cases and normalization. */
00542     if (f == g) return(1);
00543 
00544     if (Cudd_IsComplement(g)) {
00545         /* Special case: if f is regular and g is complemented,
00546         ** f(1,...,1) = 1 > 0 = g(1,...,1).
00547         */
00548         if (!Cudd_IsComplement(f)) return(0);
00549         /* Both are complemented: Swap and complement because
00550         ** f <= g <=> g' <= f' and we want the second argument to be regular.
00551         */
00552         tmp = g;
00553         g = Cudd_Not(f);
00554         f = Cudd_Not(tmp);
00555     } else if (Cudd_IsComplement(f) && g < f) {
00556         tmp = g;
00557         g = Cudd_Not(f);
00558         f = Cudd_Not(tmp);
00559     }
00560 
00561     /* Now g is regular and, if f is not regular, f < g. */
00562     one = DD_ONE(dd);
00563     if (g == one) return(1);    /* no need to test against zero */
00564     if (f == one) return(0);    /* since at this point g != one */
00565     if (Cudd_Not(f) == g) return(0); /* because neither is constant */
00566     zero = Cudd_Not(one);
00567     if (f == zero) return(1);
00568 
00569     /* Here neither f nor g is constant. */
00570 
00571     /* Check cache. */
00572     tmp = cuddCacheLookup2(dd,(DD_CTFP)Cudd_bddLeq,f,g);
00573     if (tmp != NULL) {
00574         return(tmp == one);
00575     }
00576 
00577     /* Compute cofactors. */
00578     F = Cudd_Regular(f);
00579     topf = dd->perm[F->index];
00580     topg = dd->perm[g->index];
00581     if (topf <= topg) {
00582         fv = cuddT(F); fvn = cuddE(F);
00583         if (f != F) {
00584             fv = Cudd_Not(fv);
00585             fvn = Cudd_Not(fvn);
00586         }
00587     } else {
00588         fv = fvn = f;
00589     }
00590     if (topg <= topf) {
00591         gv = cuddT(g); gvn = cuddE(g);
00592     } else {
00593         gv = gvn = g;
00594     }
00595 
00596     /* Recursive calls. Since we want to maximize the probability of
00597     ** the special case f(1,...,1) > g(1,...,1), we consider the negative
00598     ** cofactors first. Indeed, the complementation parity of the positive
00599     ** cofactors is the same as the one of the parent functions.
00600     */
00601     res = Cudd_bddLeq(dd,fvn,gvn) && Cudd_bddLeq(dd,fv,gv);
00602 
00603     /* Store result in cache and return. */
00604     cuddCacheInsert2(dd,(DD_CTFP)Cudd_bddLeq,f,g,(res ? one : zero));
00605     return(res);
00606 
00607 } /* end of Cudd_bddLeq */
00608 
00609 
00610 /*---------------------------------------------------------------------------*/
00611 /* Definition of internal functions                                          */
00612 /*---------------------------------------------------------------------------*/
00613 
00614 
00628 DdNode *
00629 cuddBddIteRecur(
00630   DdManager * dd,
00631   DdNode * f,
00632   DdNode * g,
00633   DdNode * h)
00634 {
00635     DdNode       *one, *zero, *res;
00636     DdNode       *r, *Fv, *Fnv, *Gv, *Gnv, *H, *Hv, *Hnv, *t, *e;
00637     unsigned int topf, topg, toph, v;
00638     int          index;
00639     int          comple;
00640 
00641     statLine(dd);
00642     /* Terminal cases. */
00643 
00644     /* One variable cases. */
00645     if (f == (one = DD_ONE(dd)))        /* ITE(1,G,H) = G */
00646         return(g);
00647     
00648     if (f == (zero = Cudd_Not(one)))    /* ITE(0,G,H) = H */
00649         return(h);
00650     
00651     /* From now on, f is known not to be a constant. */
00652     if (g == one || f == g) {   /* ITE(F,F,H) = ITE(F,1,H) = F + H */
00653         if (h == zero) {        /* ITE(F,1,0) = F */
00654             return(f);
00655         } else {
00656             res = cuddBddAndRecur(dd,Cudd_Not(f),Cudd_Not(h));
00657             return(Cudd_NotCond(res,res != NULL));
00658         }
00659     } else if (g == zero || f == Cudd_Not(g)) { /* ITE(F,!F,H) = ITE(F,0,H) = !F * H */
00660         if (h == one) {         /* ITE(F,0,1) = !F */
00661             return(Cudd_Not(f));
00662         } else {
00663             res = cuddBddAndRecur(dd,Cudd_Not(f),h);
00664             return(res);
00665         }
00666     }
00667     if (h == zero || f == h) {    /* ITE(F,G,F) = ITE(F,G,0) = F * G */
00668         res = cuddBddAndRecur(dd,f,g);
00669         return(res);
00670     } else if (h == one || f == Cudd_Not(h)) { /* ITE(F,G,!F) = ITE(F,G,1) = !F + G */
00671         res = cuddBddAndRecur(dd,f,Cudd_Not(g));
00672         return(Cudd_NotCond(res,res != NULL));
00673     }
00674 
00675     /* Check remaining one variable case. */
00676     if (g == h) {               /* ITE(F,G,G) = G */
00677         return(g);
00678     } else if (g == Cudd_Not(h)) { /* ITE(F,G,!G) = F <-> G */
00679         res = cuddBddXorRecur(dd,f,h);
00680         return(res);
00681     }
00682     
00683     /* From here, there are no constants. */
00684     comple = bddVarToCanonicalSimple(dd, &f, &g, &h, &topf, &topg, &toph);
00685 
00686     /* f & g are now regular pointers */
00687 
00688     v = ddMin(topg, toph);
00689 
00690     /* A shortcut: ITE(F,G,H) = (v,G,H) if F = (v,1,0), v < top(G,H). */
00691     if (topf < v && cuddT(f) == one && cuddE(f) == zero) {
00692         r = cuddUniqueInter(dd, (int) f->index, g, h);
00693         return(Cudd_NotCond(r,comple && r != NULL));
00694     }
00695 
00696     /* Check cache. */
00697     r = cuddCacheLookup(dd, DD_BDD_ITE_TAG, f, g, h);
00698     if (r != NULL) {
00699         return(Cudd_NotCond(r,comple));
00700     }
00701 
00702     /* Compute cofactors. */
00703     if (topf <= v) {
00704         v = ddMin(topf, v);     /* v = top_var(F,G,H) */
00705         index = f->index;
00706         Fv = cuddT(f); Fnv = cuddE(f);
00707     } else {
00708         Fv = Fnv = f;
00709     }
00710     if (topg == v) {
00711         index = g->index;
00712         Gv = cuddT(g); Gnv = cuddE(g);
00713     } else {
00714         Gv = Gnv = g;
00715     }
00716     if (toph == v) {
00717         H = Cudd_Regular(h);
00718         index = H->index;
00719         Hv = cuddT(H); Hnv = cuddE(H);
00720         if (Cudd_IsComplement(h)) {
00721             Hv = Cudd_Not(Hv);
00722             Hnv = Cudd_Not(Hnv);
00723         }
00724     } else {
00725         Hv = Hnv = h;
00726     }
00727 
00728     /* Recursive step. */
00729     t = cuddBddIteRecur(dd,Fv,Gv,Hv);
00730     if (t == NULL) return(NULL);
00731     cuddRef(t);
00732 
00733     e = cuddBddIteRecur(dd,Fnv,Gnv,Hnv);
00734     if (e == NULL) {
00735         Cudd_IterDerefBdd(dd,t);
00736         return(NULL);
00737     }
00738     cuddRef(e);
00739 
00740     r = (t == e) ? t : cuddUniqueInter(dd,index,t,e);
00741     if (r == NULL) {
00742         Cudd_IterDerefBdd(dd,t);
00743         Cudd_IterDerefBdd(dd,e);
00744         return(NULL);
00745     }
00746     cuddDeref(t);
00747     cuddDeref(e);
00748 
00749     cuddCacheInsert(dd, DD_BDD_ITE_TAG, f, g, h, r);
00750     return(Cudd_NotCond(r,comple));
00751 
00752 } /* end of cuddBddIteRecur */
00753 
00754 
00766 DdNode *
00767 cuddBddIntersectRecur(
00768   DdManager * dd,
00769   DdNode * f,
00770   DdNode * g)
00771 {
00772     DdNode *res;
00773     DdNode *F, *G, *t, *e;
00774     DdNode *fv, *fnv, *gv, *gnv;
00775     DdNode *one, *zero;
00776     unsigned int index, topf, topg;
00777 
00778     statLine(dd);
00779     one = DD_ONE(dd);
00780     zero = Cudd_Not(one);
00781 
00782     /* Terminal cases. */
00783     if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
00784     if (f == g || g == one) return(f);
00785     if (f == one) return(g);
00786 
00787     /* At this point f and g are not constant. */
00788     if (f > g) { DdNode *tmp = f; f = g; g = tmp; }
00789     res = cuddCacheLookup2(dd,Cudd_bddIntersect,f,g);
00790     if (res != NULL) return(res);
00791 
00792     /* Find splitting variable. Here we can skip the use of cuddI,
00793     ** because the operands are known to be non-constant.
00794     */
00795     F = Cudd_Regular(f);
00796     topf = dd->perm[F->index];
00797     G = Cudd_Regular(g);
00798     topg = dd->perm[G->index];
00799 
00800     /* Compute cofactors. */
00801     if (topf <= topg) {
00802         index = F->index;
00803         fv = cuddT(F);
00804         fnv = cuddE(F);
00805         if (Cudd_IsComplement(f)) {
00806             fv = Cudd_Not(fv);
00807             fnv = Cudd_Not(fnv);
00808         }
00809     } else {
00810         index = G->index;
00811         fv = fnv = f;
00812     }
00813 
00814     if (topg <= topf) {
00815         gv = cuddT(G);
00816         gnv = cuddE(G);
00817         if (Cudd_IsComplement(g)) {
00818             gv = Cudd_Not(gv);
00819             gnv = Cudd_Not(gnv);
00820         }
00821     } else {
00822         gv = gnv = g;
00823     }
00824 
00825     /* Compute partial results. */
00826     t = cuddBddIntersectRecur(dd,fv,gv);
00827     if (t == NULL) return(NULL);
00828     cuddRef(t);
00829     if (t != zero) {
00830         e = zero;
00831     } else {
00832         e = cuddBddIntersectRecur(dd,fnv,gnv);
00833         if (e == NULL) {
00834             Cudd_IterDerefBdd(dd, t);
00835             return(NULL);
00836         }
00837     }
00838     cuddRef(e);
00839 
00840     if (t == e) { /* both equal zero */
00841         res = t;
00842     } else if (Cudd_IsComplement(t)) {
00843         res = cuddUniqueInter(dd,(int)index,Cudd_Not(t),Cudd_Not(e));
00844         if (res == NULL) {
00845             Cudd_IterDerefBdd(dd, t);
00846             Cudd_IterDerefBdd(dd, e);
00847             return(NULL);
00848         }
00849         res = Cudd_Not(res);
00850     } else {
00851         res = cuddUniqueInter(dd,(int)index,t,e);
00852         if (res == NULL) {
00853             Cudd_IterDerefBdd(dd, t);
00854             Cudd_IterDerefBdd(dd, e);
00855             return(NULL);
00856         }
00857     }
00858     cuddDeref(e);
00859     cuddDeref(t);
00860 
00861     cuddCacheInsert2(dd,Cudd_bddIntersect,f,g,res);
00862 
00863     return(res);
00864 
00865 } /* end of cuddBddIntersectRecur */
00866 
00867 
00881 DdNode *
00882 cuddBddAndRecur(
00883   DdManager * manager,
00884   DdNode * f,
00885   DdNode * g)
00886 {
00887     DdNode *F, *fv, *fnv, *G, *gv, *gnv;
00888     DdNode *one, *r, *t, *e;
00889     unsigned int topf, topg, index;
00890 
00891     statLine(manager);
00892     one = DD_ONE(manager);
00893 
00894     /* Terminal cases. */
00895     F = Cudd_Regular(f);
00896     G = Cudd_Regular(g);
00897     if (F == G) {
00898         if (f == g) return(f);
00899         else return(Cudd_Not(one));
00900     }
00901     if (F == one) {
00902         if (f == one) return(g);
00903         else return(f);
00904     }
00905     if (G == one) {
00906         if (g == one) return(f);
00907         else return(g);
00908     }
00909 
00910     /* At this point f and g are not constant. */
00911     if (f > g) { /* Try to increase cache efficiency. */
00912         DdNode *tmp = f;
00913         f = g;
00914         g = tmp;
00915         F = Cudd_Regular(f);
00916         G = Cudd_Regular(g);
00917     }
00918 
00919     /* Check cache. */
00920     if (F->ref != 1 || G->ref != 1) {
00921         r = cuddCacheLookup2(manager, Cudd_bddAnd, f, g);
00922         if (r != NULL) return(r);
00923     }
00924 
00925     /* Here we can skip the use of cuddI, because the operands are known
00926     ** to be non-constant.
00927     */
00928     topf = manager->perm[F->index];
00929     topg = manager->perm[G->index];
00930 
00931     /* Compute cofactors. */
00932     if (topf <= topg) {
00933         index = F->index;
00934         fv = cuddT(F);
00935         fnv = cuddE(F);
00936         if (Cudd_IsComplement(f)) {
00937             fv = Cudd_Not(fv);
00938             fnv = Cudd_Not(fnv);
00939         }
00940     } else {
00941         index = G->index;
00942         fv = fnv = f;
00943     }
00944 
00945     if (topg <= topf) {
00946         gv = cuddT(G);
00947         gnv = cuddE(G);
00948         if (Cudd_IsComplement(g)) {
00949             gv = Cudd_Not(gv);
00950             gnv = Cudd_Not(gnv);
00951         }
00952     } else {
00953         gv = gnv = g;
00954     }
00955 
00956     t = cuddBddAndRecur(manager, fv, gv);
00957     if (t == NULL) return(NULL);
00958     cuddRef(t);
00959 
00960     e = cuddBddAndRecur(manager, fnv, gnv);
00961     if (e == NULL) {
00962         Cudd_IterDerefBdd(manager, t);
00963         return(NULL);
00964     }
00965     cuddRef(e);
00966 
00967     if (t == e) {
00968         r = t;
00969     } else {
00970         if (Cudd_IsComplement(t)) {
00971             r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
00972             if (r == NULL) {
00973                 Cudd_IterDerefBdd(manager, t);
00974                 Cudd_IterDerefBdd(manager, e);
00975                 return(NULL);
00976             }
00977             r = Cudd_Not(r);
00978         } else {
00979             r = cuddUniqueInter(manager,(int)index,t,e);
00980             if (r == NULL) {
00981                 Cudd_IterDerefBdd(manager, t);
00982                 Cudd_IterDerefBdd(manager, e);
00983                 return(NULL);
00984             }
00985         }
00986     }
00987     cuddDeref(e);
00988     cuddDeref(t);
00989     if (F->ref != 1 || G->ref != 1)
00990         cuddCacheInsert2(manager, Cudd_bddAnd, f, g, r);
00991     return(r);
00992 
00993 } /* end of cuddBddAndRecur */
00994 
00995 
01009 DdNode *
01010 cuddBddXorRecur(
01011   DdManager * manager,
01012   DdNode * f,
01013   DdNode * g)
01014 {
01015     DdNode *fv, *fnv, *G, *gv, *gnv;
01016     DdNode *one, *zero, *r, *t, *e;
01017     unsigned int topf, topg, index;
01018 
01019     statLine(manager);
01020     one = DD_ONE(manager);
01021     zero = Cudd_Not(one);
01022 
01023     /* Terminal cases. */
01024     if (f == g) return(zero);
01025     if (f == Cudd_Not(g)) return(one);
01026     if (f > g) { /* Try to increase cache efficiency and simplify tests. */
01027         DdNode *tmp = f;
01028         f = g;
01029         g = tmp;
01030     }
01031     if (g == zero) return(f);
01032     if (g == one) return(Cudd_Not(f));
01033     if (Cudd_IsComplement(f)) {
01034         f = Cudd_Not(f);
01035         g = Cudd_Not(g);
01036     }
01037     /* Now the first argument is regular. */
01038     if (f == one) return(Cudd_Not(g));
01039 
01040     /* At this point f and g are not constant. */
01041 
01042     /* Check cache. */
01043     r = cuddCacheLookup2(manager, Cudd_bddXor, f, g);
01044     if (r != NULL) return(r);
01045 
01046     /* Here we can skip the use of cuddI, because the operands are known
01047     ** to be non-constant.
01048     */
01049     topf = manager->perm[f->index];
01050     G = Cudd_Regular(g);
01051     topg = manager->perm[G->index];
01052 
01053     /* Compute cofactors. */
01054     if (topf <= topg) {
01055         index = f->index;
01056         fv = cuddT(f);
01057         fnv = cuddE(f);
01058     } else {
01059         index = G->index;
01060         fv = fnv = f;
01061     }
01062 
01063     if (topg <= topf) {
01064         gv = cuddT(G);
01065         gnv = cuddE(G);
01066         if (Cudd_IsComplement(g)) {
01067             gv = Cudd_Not(gv);
01068             gnv = Cudd_Not(gnv);
01069         }
01070     } else {
01071         gv = gnv = g;
01072     }
01073 
01074     t = cuddBddXorRecur(manager, fv, gv);
01075     if (t == NULL) return(NULL);
01076     cuddRef(t);
01077 
01078     e = cuddBddXorRecur(manager, fnv, gnv);
01079     if (e == NULL) {
01080         Cudd_IterDerefBdd(manager, t);
01081         return(NULL);
01082     }
01083     cuddRef(e);
01084 
01085     if (t == e) {
01086         r = t;
01087     } else {
01088         if (Cudd_IsComplement(t)) {
01089             r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
01090             if (r == NULL) {
01091                 Cudd_IterDerefBdd(manager, t);
01092                 Cudd_IterDerefBdd(manager, e);
01093                 return(NULL);
01094             }
01095             r = Cudd_Not(r);
01096         } else {
01097             r = cuddUniqueInter(manager,(int)index,t,e);
01098             if (r == NULL) {
01099                 Cudd_IterDerefBdd(manager, t);
01100                 Cudd_IterDerefBdd(manager, e);
01101                 return(NULL);
01102             }
01103         }
01104     }
01105     cuddDeref(e);
01106     cuddDeref(t);
01107     cuddCacheInsert2(manager, Cudd_bddXor, f, g, r);
01108     return(r);
01109 
01110 } /* end of cuddBddXorRecur */
01111 
01112 
01113 /*---------------------------------------------------------------------------*/
01114 /* Definition of static functions                                            */
01115 /*---------------------------------------------------------------------------*/
01116 
01117 
01130 static void
01131 bddVarToConst(
01132   DdNode * f,
01133   DdNode ** gp,
01134   DdNode ** hp,
01135   DdNode * one)
01136 {
01137     DdNode *g = *gp;
01138     DdNode *h = *hp;
01139 
01140     if (f == g) {    /* ITE(F,F,H) = ITE(F,1,H) = F + H */
01141         *gp = one;
01142     } else if (f == Cudd_Not(g)) {    /* ITE(F,!F,H) = ITE(F,0,H) = !F * H */
01143         *gp = Cudd_Not(one);
01144     }
01145     if (f == h) {    /* ITE(F,G,F) = ITE(F,G,0) = F * G */
01146         *hp = Cudd_Not(one);
01147     } else if (f == Cudd_Not(h)) {    /* ITE(F,G,!F) = ITE(F,G,1) = !F + G */
01148         *hp = one;
01149     }
01150 
01151 } /* end of bddVarToConst */
01152 
01153 
01165 static int
01166 bddVarToCanonical(
01167   DdManager * dd,
01168   DdNode ** fp,
01169   DdNode ** gp,
01170   DdNode ** hp,
01171   unsigned int * topfp,
01172   unsigned int * topgp,
01173   unsigned int * tophp)
01174 {
01175     register DdNode             *F, *G, *H, *r, *f, *g, *h;
01176     register unsigned int       topf, topg, toph;
01177     DdNode                      *one = dd->one;
01178     int                         comple, change;
01179 
01180     f = *fp;
01181     g = *gp;
01182     h = *hp;
01183     F = Cudd_Regular(f);
01184     G = Cudd_Regular(g);
01185     H = Cudd_Regular(h);
01186     topf = cuddI(dd,F->index);
01187     topg = cuddI(dd,G->index);
01188     toph = cuddI(dd,H->index);
01189 
01190     change = 0;
01191 
01192     if (G == one) {                     /* ITE(F,c,H) */
01193         if ((topf > toph) || (topf == toph && f > h)) {
01194             r = h;
01195             h = f;
01196             f = r;                      /* ITE(F,1,H) = ITE(H,1,F) */
01197             if (g != one) {     /* g == zero */
01198                 f = Cudd_Not(f);                /* ITE(F,0,H) = ITE(!H,0,!F) */
01199                 h = Cudd_Not(h);
01200             }
01201             change = 1;
01202         }
01203     } else if (H == one) {              /* ITE(F,G,c) */
01204         if ((topf > topg) || (topf == topg && f > g)) {
01205             r = g;
01206             g = f;
01207             f = r;                      /* ITE(F,G,0) = ITE(G,F,0) */
01208             if (h == one) {
01209                 f = Cudd_Not(f);                /* ITE(F,G,1) = ITE(!G,!F,1) */
01210                 g = Cudd_Not(g);
01211             }
01212             change = 1;
01213         }
01214     } else if (g == Cudd_Not(h)) {      /* ITE(F,G,!G) = ITE(G,F,!F) */
01215         if ((topf > topg) || (topf == topg && f > g)) {
01216             r = f;
01217             f = g;
01218             g = r;
01219             h = Cudd_Not(r);
01220             change = 1;
01221         }
01222     }
01223     /* adjust pointers so that the first 2 arguments to ITE are regular */
01224     if (Cudd_IsComplement(f) != 0) {    /* ITE(!F,G,H) = ITE(F,H,G) */
01225         f = Cudd_Not(f);
01226         r = g;
01227         g = h;
01228         h = r;
01229         change = 1;
01230     }
01231     comple = 0;
01232     if (Cudd_IsComplement(g) != 0) {    /* ITE(F,!G,H) = !ITE(F,G,!H) */
01233         g = Cudd_Not(g);
01234         h = Cudd_Not(h);
01235         change = 1;
01236         comple = 1;
01237     }
01238     if (change != 0) {
01239         *fp = f;
01240         *gp = g;
01241         *hp = h;
01242     }
01243     *topfp = cuddI(dd,f->index);
01244     *topgp = cuddI(dd,g->index);
01245     *tophp = cuddI(dd,Cudd_Regular(h)->index);
01246 
01247     return(comple);
01248 
01249 } /* end of bddVarToCanonical */
01250 
01251 
01267 static int
01268 bddVarToCanonicalSimple(
01269   DdManager * dd,
01270   DdNode ** fp,
01271   DdNode ** gp,
01272   DdNode ** hp,
01273   unsigned int * topfp,
01274   unsigned int * topgp,
01275   unsigned int * tophp)
01276 {
01277     register DdNode             *r, *f, *g, *h;
01278     int                         comple, change;
01279 
01280     f = *fp;
01281     g = *gp;
01282     h = *hp;
01283 
01284     change = 0;
01285 
01286     /* adjust pointers so that the first 2 arguments to ITE are regular */
01287     if (Cudd_IsComplement(f)) { /* ITE(!F,G,H) = ITE(F,H,G) */
01288         f = Cudd_Not(f);
01289         r = g;
01290         g = h;
01291         h = r;
01292         change = 1;
01293     }
01294     comple = 0;
01295     if (Cudd_IsComplement(g)) { /* ITE(F,!G,H) = !ITE(F,G,!H) */
01296         g = Cudd_Not(g);
01297         h = Cudd_Not(h);
01298         change = 1;
01299         comple = 1;
01300     }
01301     if (change) {
01302         *fp = f;
01303         *gp = g;
01304         *hp = h;
01305     }
01306 
01307     /* Here we can skip the use of cuddI, because the operands are known
01308     ** to be non-constant.
01309     */
01310     *topfp = dd->perm[f->index];
01311     *topgp = dd->perm[g->index];
01312     *tophp = dd->perm[Cudd_Regular(h)->index];
01313 
01314     return(comple);
01315 
01316 } /* end of bddVarToCanonicalSimple */
01317