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

00001 
00047 #include "util_hack.h"
00048 #include "cuddInt.h"
00049 
00050 
00051 /*---------------------------------------------------------------------------*/
00052 /* Constant declarations                                                     */
00053 /*---------------------------------------------------------------------------*/
00054 
00055 
00056 /*---------------------------------------------------------------------------*/
00057 /* Stucture declarations                                                     */
00058 /*---------------------------------------------------------------------------*/
00059 
00060 
00061 /*---------------------------------------------------------------------------*/
00062 /* Type declarations                                                         */
00063 /*---------------------------------------------------------------------------*/
00064 
00065 
00066 /*---------------------------------------------------------------------------*/
00067 /* Variable declarations                                                     */
00068 /*---------------------------------------------------------------------------*/
00069 
00070 #ifndef lint
00071 static char rcsid[] DD_UNUSED = "$Id: cuddBddIte.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $";
00072 #endif
00073 
00074 /*---------------------------------------------------------------------------*/
00075 /* Macro declarations                                                        */
00076 /*---------------------------------------------------------------------------*/
00077 
00078 
00081 /*---------------------------------------------------------------------------*/
00082 /* Static function prototypes                                                */
00083 /*---------------------------------------------------------------------------*/
00084 
00085 static void bddVarToConst ARGS((DdNode *f, DdNode **gp, DdNode **hp, DdNode *one));
00086 static int bddVarToCanonical ARGS((DdManager *dd, DdNode **fp, DdNode **gp, DdNode **hp, unsigned int *topfp, unsigned int *topgp, unsigned int *tophp));
00087 static int bddVarToCanonicalSimple ARGS((DdManager *dd, DdNode **fp, DdNode **gp, DdNode **hp, unsigned int *topfp, unsigned int *topgp, unsigned int *tophp));
00088 
00092 /*---------------------------------------------------------------------------*/
00093 /* Definition of exported functions                                          */
00094 /*---------------------------------------------------------------------------*/
00095 
00096 
00110 DdNode *
00111 Cudd_bddIte(
00112   DdManager * dd,
00113   DdNode * f,
00114   DdNode * g,
00115   DdNode * h)
00116 {
00117     DdNode *res;
00118 
00119     do {
00120         dd->reordered = 0;
00121         res = cuddBddIteRecur(dd,f,g,h);
00122     } while (dd->reordered == 1);
00123     return(res);
00124 
00125 } /* end of Cudd_bddIte */
00126 
00127 
00141 DdNode *
00142 Cudd_bddIteConstant(
00143   DdManager * dd,
00144   DdNode * f,
00145   DdNode * g,
00146   DdNode * h)
00147 {
00148     DdNode       *r, *Fv, *Fnv, *Gv, *Gnv, *H, *Hv, *Hnv, *t, *e;
00149     DdNode       *one = DD_ONE(dd);
00150     DdNode       *zero = Cudd_Not(one);
00151     int          comple;
00152     unsigned int topf, topg, toph, v;
00153 
00154     statLine(dd);
00155     /* Trivial cases. */
00156     if (f == one)                       /* ITE(1,G,H) => G */
00157         return(g);
00158     
00159     if (f == zero)                      /* ITE(0,G,H) => H */
00160         return(h);
00161     
00162     /* f now not a constant. */
00163     bddVarToConst(f, &g, &h, one);      /* possibly convert g or h */
00164                                         /* to constants */
00165 
00166     if (g == h)                         /* ITE(F,G,G) => G */
00167         return(g);
00168 
00169     if (Cudd_IsConstant(g) && Cudd_IsConstant(h)) 
00170         return(DD_NON_CONSTANT);        /* ITE(F,1,0) or ITE(F,0,1) */
00171                                         /* => DD_NON_CONSTANT */
00172     
00173     if (g == Cudd_Not(h))
00174         return(DD_NON_CONSTANT);        /* ITE(F,G,G') => DD_NON_CONSTANT */
00175                                         /* if F != G and F != G' */
00176     
00177     comple = bddVarToCanonical(dd, &f, &g, &h, &topf, &topg, &toph);
00178 
00179     /* Cache lookup. */
00180     r = cuddConstantLookup(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h);
00181     if (r != NULL) {
00182         return(Cudd_NotCond(r,comple && r != DD_NON_CONSTANT));
00183     }
00184 
00185     v = ddMin(topg, toph);
00186 
00187     /* ITE(F,G,H) = (v,G,H) (non constant) if F = (v,1,0), v < top(G,H). */
00188     if (topf < v && cuddT(f) == one && cuddE(f) == zero) {
00189         return(DD_NON_CONSTANT);
00190     }
00191 
00192     /* Compute cofactors. */
00193     if (topf <= v) {
00194         v = ddMin(topf, v);             /* v = top_var(F,G,H) */
00195         Fv = cuddT(f); Fnv = cuddE(f);
00196     } else {
00197         Fv = Fnv = f;
00198     }
00199 
00200     if (topg == v) {
00201         Gv = cuddT(g); Gnv = cuddE(g);
00202     } else {
00203         Gv = Gnv = g;
00204     }
00205 
00206     if (toph == v) {
00207         H = Cudd_Regular(h);
00208         Hv = cuddT(H); Hnv = cuddE(H);
00209         if (Cudd_IsComplement(h)) {
00210             Hv = Cudd_Not(Hv);
00211             Hnv = Cudd_Not(Hnv);
00212         }
00213     } else {
00214         Hv = Hnv = h;
00215     }
00216 
00217     /* Recursion. */
00218     t = Cudd_bddIteConstant(dd, Fv, Gv, Hv);
00219     if (t == DD_NON_CONSTANT || !Cudd_IsConstant(t)) {
00220         cuddCacheInsert(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT);
00221         return(DD_NON_CONSTANT);
00222     }
00223     e = Cudd_bddIteConstant(dd, Fnv, Gnv, Hnv);
00224     if (e == DD_NON_CONSTANT || !Cudd_IsConstant(e) || t != e) {
00225         cuddCacheInsert(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT);
00226         return(DD_NON_CONSTANT);
00227     }
00228     cuddCacheInsert(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h, t);
00229     return(Cudd_NotCond(t,comple));
00230 
00231 } /* end of Cudd_bddIteConstant */
00232 
00233 
00249 DdNode *
00250 Cudd_bddIntersect(
00251   DdManager * dd /* manager */,
00252   DdNode * f /* first operand */,
00253   DdNode * g /* second operand */)
00254 {
00255     DdNode *res;
00256 
00257     do {
00258         dd->reordered = 0;
00259         res = cuddBddIntersectRecur(dd,f,g);
00260     } while (dd->reordered == 1);
00261 
00262     return(res);
00263 
00264 } /* end of Cudd_bddIntersect */
00265 
00266 
00281 DdNode *
00282 Cudd_bddAnd(
00283   DdManager * dd,
00284   DdNode * f,
00285   DdNode * g)
00286 {
00287     DdNode *res;
00288 
00289     do {
00290         dd->reordered = 0;
00291         res = cuddBddAndRecur(dd,f,g);
00292     } while (dd->reordered == 1);
00293     return(res);
00294 
00295 } /* end of Cudd_bddAnd */
00296 
00297 
00312 DdNode *
00313 Cudd_bddOr(
00314   DdManager * dd,
00315   DdNode * f,
00316   DdNode * g)
00317 {
00318     DdNode *res;
00319 
00320     do {
00321         dd->reordered = 0;
00322         res = cuddBddAndRecur(dd,Cudd_Not(f),Cudd_Not(g));
00323     } while (dd->reordered == 1);
00324     res = Cudd_NotCond(res,res != NULL);
00325     return(res);
00326 
00327 } /* end of Cudd_bddOr */
00328 
00329 
00344 DdNode *
00345 Cudd_bddNand(
00346   DdManager * dd,
00347   DdNode * f,
00348   DdNode * g)
00349 {
00350     DdNode *res;
00351 
00352     do {
00353         dd->reordered = 0;
00354         res = cuddBddAndRecur(dd,f,g);
00355     } while (dd->reordered == 1);
00356     res = Cudd_NotCond(res,res != NULL);
00357     return(res);
00358 
00359 } /* end of Cudd_bddNand */
00360 
00361 
00376 DdNode *
00377 Cudd_bddNor(
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     return(res);
00389 
00390 } /* end of Cudd_bddNor */
00391 
00392 
00407 DdNode *
00408 Cudd_bddXor(
00409   DdManager * dd,
00410   DdNode * f,
00411   DdNode * g)
00412 {
00413     DdNode *res;
00414 
00415     do {
00416         dd->reordered = 0;
00417         res = cuddBddXorRecur(dd,f,g);
00418     } while (dd->reordered == 1);
00419     return(res);
00420 
00421 } /* end of Cudd_bddXor */
00422 
00423 
00438 DdNode *
00439 Cudd_bddXnor(
00440   DdManager * dd,
00441   DdNode * f,
00442   DdNode * g)
00443 {
00444     DdNode *res;
00445 
00446     do {
00447         dd->reordered = 0;
00448         res = cuddBddXorRecur(dd,f,Cudd_Not(g));
00449     } while (dd->reordered == 1);
00450     return(res);
00451 
00452 } /* end of Cudd_bddXnor */
00453 
00454 
00467 int
00468 Cudd_bddLeq(
00469   DdManager * dd,
00470   DdNode * f,
00471   DdNode * g)
00472 {
00473     DdNode *one, *zero, *tmp, *F, *fv, *fvn, *gv, *gvn;
00474     unsigned int topf, topg, res;
00475 
00476     statLine(dd);
00477     /* Terminal cases and normalization. */
00478     if (f == g) return(1);
00479 
00480     if (Cudd_IsComplement(g)) {
00481         /* Special case: if f is regular and g is complemented,
00482         ** f(1,...,1) = 1 > 0 = g(1,...,1).
00483         */
00484         if (!Cudd_IsComplement(f)) return(0);
00485         /* Both are complemented: Swap and complement because
00486         ** f <= g <=> g' <= f' and we want the second argument to be regular.
00487         */
00488         tmp = g;
00489         g = Cudd_Not(f);
00490         f = Cudd_Not(tmp);
00491     } else if (Cudd_IsComplement(f) && g < f) {
00492         tmp = g;
00493         g = Cudd_Not(f);
00494         f = Cudd_Not(tmp);
00495     }
00496 
00497     /* Now g is regular and, if f is not regular, f < g. */
00498     one = DD_ONE(dd);
00499     if (g == one) return(1);    /* no need to test against zero */
00500     if (f == one) return(0);    /* since at this point g != one */
00501     if (Cudd_Not(f) == g) return(0); /* because neither is constant */
00502     zero = Cudd_Not(one);
00503     if (f == zero) return(1);
00504 
00505     /* Here neither f nor g is constant. */
00506 
00507     /* Check cache. */
00508     tmp = cuddCacheLookup2(dd,(DdNode * (*)(DdManager *, DdNode *,
00509                            DdNode *))Cudd_bddLeq,f,g);
00510     if (tmp != NULL) {
00511         return(tmp == one);
00512     }
00513 
00514     /* Compute cofactors. */
00515     F = Cudd_Regular(f);
00516     topf = dd->perm[F->index];
00517     topg = dd->perm[g->index];
00518     if (topf <= topg) {
00519         fv = cuddT(F); fvn = cuddE(F);
00520         if (f != F) {
00521             fv = Cudd_Not(fv);
00522             fvn = Cudd_Not(fvn);
00523         }
00524     } else {
00525         fv = fvn = f;
00526     }
00527     if (topg <= topf) {
00528         gv = cuddT(g); gvn = cuddE(g);
00529     } else {
00530         gv = gvn = g;
00531     }
00532 
00533     /* Recursive calls. Since we want to maximize the probability of
00534     ** the special case f(1,...,1) > g(1,...,1), we consider the negative
00535     ** cofactors first. Indeed, the complementation parity of the positive
00536     ** cofactors is the same as the one of the parent functions.
00537     */
00538     res = Cudd_bddLeq(dd,fvn,gvn) && Cudd_bddLeq(dd,fv,gv);
00539 
00540     /* Store result in cache and return. */
00541     cuddCacheInsert2(dd,(DdNode * (*)(DdManager *, DdNode *, DdNode *))Cudd_bddLeq,f,g,(res ? one : zero));
00542     return(res);
00543 
00544 } /* end of Cudd_bddLeq */
00545 
00546 
00547 /*---------------------------------------------------------------------------*/
00548 /* Definition of internal functions                                          */
00549 /*---------------------------------------------------------------------------*/
00550 
00551 
00565 DdNode *
00566 cuddBddIteRecur(
00567   DdManager * dd,
00568   DdNode * f,
00569   DdNode * g,
00570   DdNode * h)
00571 {
00572     DdNode       *one, *zero, *res;
00573     DdNode       *r, *Fv, *Fnv, *Gv, *Gnv, *H, *Hv, *Hnv, *t, *e;
00574     unsigned int topf, topg, toph, v;
00575     int          index;
00576     int          comple;
00577 
00578     statLine(dd);
00579     /* Terminal cases. */
00580 
00581     /* One variable cases. */
00582     if (f == (one = DD_ONE(dd)))        /* ITE(1,G,H) = G */
00583         return(g);
00584     
00585     if (f == (zero = Cudd_Not(one)))    /* ITE(0,G,H) = H */
00586         return(h);
00587     
00588     /* From now on, f is known not to be a constant. */
00589     if (g == one || f == g) {   /* ITE(F,F,H) = ITE(F,1,H) = F + H */
00590         if (h == zero) {        /* ITE(F,1,0) = F */
00591             return(f);
00592         } else {
00593             res = cuddBddAndRecur(dd,Cudd_Not(f),Cudd_Not(h));
00594             return(Cudd_NotCond(res,res != NULL));
00595         }
00596     } else if (g == zero || f == Cudd_Not(g)) { /* ITE(F,!F,H) = ITE(F,0,H) = !F * H */
00597         if (h == one) {         /* ITE(F,0,1) = !F */
00598             return(Cudd_Not(f));
00599         } else {
00600             res = cuddBddAndRecur(dd,Cudd_Not(f),h);
00601             return(res);
00602         }
00603     }
00604     if (h == zero || f == h) {    /* ITE(F,G,F) = ITE(F,G,0) = F * G */
00605         res = cuddBddAndRecur(dd,f,g);
00606         return(res);
00607     } else if (h == one || f == Cudd_Not(h)) { /* ITE(F,G,!F) = ITE(F,G,1) = !F + G */
00608         res = cuddBddAndRecur(dd,f,Cudd_Not(g));
00609         return(Cudd_NotCond(res,res != NULL));
00610     }
00611 
00612     /* Check remaining one variable case. */
00613     if (g == h) {               /* ITE(F,G,G) = G */
00614         return(g);
00615     } else if (g == Cudd_Not(h)) { /* ITE(F,G,!G) = F <-> G */
00616         res = cuddBddXorRecur(dd,f,h);
00617         return(res);
00618     }
00619     
00620     /* From here, there are no constants. */
00621     comple = bddVarToCanonicalSimple(dd, &f, &g, &h, &topf, &topg, &toph);
00622 
00623     /* f & g are now regular pointers */
00624 
00625     v = ddMin(topg, toph);
00626 
00627     /* A shortcut: ITE(F,G,H) = (v,G,H) if F = (v,1,0), v < top(G,H). */
00628     if (topf < v && cuddT(f) == one && cuddE(f) == zero) {
00629         r = cuddUniqueInter(dd, (int) f->index, g, h);
00630         return(Cudd_NotCond(r,comple && r != NULL));
00631     }
00632 
00633     /* Check cache. */
00634     r = cuddCacheLookup(dd, DD_BDD_ITE_TAG, f, g, h);
00635     if (r != NULL) {
00636         return(Cudd_NotCond(r,comple));
00637     }
00638 
00639     /* Compute cofactors. */
00640     if (topf <= v) {
00641         v = ddMin(topf, v);     /* v = top_var(F,G,H) */
00642         index = f->index;
00643         Fv = cuddT(f); Fnv = cuddE(f);
00644     } else {
00645         Fv = Fnv = f;
00646     }
00647     if (topg == v) {
00648         index = g->index;
00649         Gv = cuddT(g); Gnv = cuddE(g);
00650     } else {
00651         Gv = Gnv = g;
00652     }
00653     if (toph == v) {
00654         H = Cudd_Regular(h);
00655         index = H->index;
00656         Hv = cuddT(H); Hnv = cuddE(H);
00657         if (Cudd_IsComplement(h)) {
00658             Hv = Cudd_Not(Hv);
00659             Hnv = Cudd_Not(Hnv);
00660         }
00661     } else {
00662         Hv = Hnv = h;
00663     }
00664 
00665     /* Recursive step. */
00666     t = cuddBddIteRecur(dd,Fv,Gv,Hv);
00667     if (t == NULL) return(NULL);
00668     cuddRef(t);
00669 
00670     e = cuddBddIteRecur(dd,Fnv,Gnv,Hnv);
00671     if (e == NULL) {
00672         Cudd_IterDerefBdd(dd,t);
00673         return(NULL);
00674     }
00675     cuddRef(e);
00676 
00677     r = (t == e) ? t : cuddUniqueInter(dd,index,t,e);
00678     if (r == NULL) {
00679         Cudd_IterDerefBdd(dd,t);
00680         Cudd_IterDerefBdd(dd,e);
00681         return(NULL);
00682     }
00683     cuddDeref(t);
00684     cuddDeref(e);
00685 
00686     cuddCacheInsert(dd, DD_BDD_ITE_TAG, f, g, h, r);
00687     return(Cudd_NotCond(r,comple));
00688 
00689 } /* end of cuddBddIteRecur */
00690 
00691 
00703 DdNode *
00704 cuddBddIntersectRecur(
00705   DdManager * dd,
00706   DdNode * f,
00707   DdNode * g)
00708 {
00709     DdNode *res;
00710     DdNode *F, *G, *t, *e;
00711     DdNode *fv, *fnv, *gv, *gnv;
00712     DdNode *one, *zero;
00713     unsigned int index, topf, topg;
00714 
00715     statLine(dd);
00716     one = DD_ONE(dd);
00717     zero = Cudd_Not(one);
00718 
00719     /* Terminal cases. */
00720     if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
00721     if (f == g || g == one) return(f);
00722     if (f == one) return(g);
00723 
00724     /* At this point f and g are not constant. */
00725     if (f > g) { DdNode *tmp = f; f = g; g = tmp; }
00726     res = cuddCacheLookup2(dd,Cudd_bddIntersect,f,g);
00727     if (res != NULL) return(res);
00728 
00729     /* Find splitting variable. Here we can skip the use of cuddI,
00730     ** because the operands are known to be non-constant.
00731     */
00732     F = Cudd_Regular(f);
00733     topf = dd->perm[F->index];
00734     G = Cudd_Regular(g);
00735     topg = dd->perm[G->index];
00736 
00737     /* Compute cofactors. */
00738     if (topf <= topg) {
00739         index = F->index;
00740         fv = cuddT(F);
00741         fnv = cuddE(F);
00742         if (Cudd_IsComplement(f)) {
00743             fv = Cudd_Not(fv);
00744             fnv = Cudd_Not(fnv);
00745         }
00746     } else {
00747         index = G->index;
00748         fv = fnv = f;
00749     }
00750 
00751     if (topg <= topf) {
00752         gv = cuddT(G);
00753         gnv = cuddE(G);
00754         if (Cudd_IsComplement(g)) {
00755             gv = Cudd_Not(gv);
00756             gnv = Cudd_Not(gnv);
00757         }
00758     } else {
00759         gv = gnv = g;
00760     }
00761 
00762     /* Compute partial results. */
00763     t = cuddBddIntersectRecur(dd,fv,gv);
00764     if (t == NULL) return(NULL);
00765     cuddRef(t);
00766     if (t != zero) {
00767         e = zero;
00768     } else {
00769         e = cuddBddIntersectRecur(dd,fnv,gnv);
00770         if (e == NULL) {
00771             Cudd_IterDerefBdd(dd, t);
00772             return(NULL);
00773         }
00774     }
00775     cuddRef(e);
00776 
00777     if (t == e) { /* both equal zero */
00778         res = t;
00779     } else if (Cudd_IsComplement(t)) {
00780         res = cuddUniqueInter(dd,(int)index,Cudd_Not(t),Cudd_Not(e));
00781         if (res == NULL) {
00782             Cudd_IterDerefBdd(dd, t);
00783             Cudd_IterDerefBdd(dd, e);
00784             return(NULL);
00785         }
00786         res = Cudd_Not(res);
00787     } else {
00788         res = cuddUniqueInter(dd,(int)index,t,e);
00789         if (res == NULL) {
00790             Cudd_IterDerefBdd(dd, t);
00791             Cudd_IterDerefBdd(dd, e);
00792             return(NULL);
00793         }
00794     }
00795     cuddDeref(e);
00796     cuddDeref(t);
00797 
00798     cuddCacheInsert2(dd,Cudd_bddIntersect,f,g,res);
00799 
00800     return(res);
00801 
00802 } /* end of cuddBddIntersectRecur */
00803 
00804 
00818 DdNode *
00819 cuddBddAndRecur(
00820   DdManager * manager,
00821   DdNode * f,
00822   DdNode * g)
00823 {
00824     DdNode *F, *fv, *fnv, *G, *gv, *gnv;
00825     DdNode *one, *r, *t, *e;
00826     unsigned int topf, topg, index;
00827 
00828     statLine(manager);
00829     one = DD_ONE(manager);
00830 
00831     /* Terminal cases. */
00832     F = Cudd_Regular(f);
00833     G = Cudd_Regular(g);
00834     if (F == G) {
00835         if (f == g) return(f);
00836         else return(Cudd_Not(one));
00837     }
00838     if (F == one) {
00839         if (f == one) return(g);
00840         else return(f);
00841     }
00842     if (G == one) {
00843         if (g == one) return(f);
00844         else return(g);
00845     }
00846 
00847     /* At this point f and g are not constant. */
00848     if (f > g) { /* Try to increase cache efficiency. */
00849         DdNode *tmp = f;
00850         f = g;
00851         g = tmp;
00852         F = Cudd_Regular(f);
00853         G = Cudd_Regular(g);
00854     }
00855 
00856     /* Check cache. */
00857     if (F->ref != 1 || G->ref != 1) {
00858         r = cuddCacheLookup2(manager, Cudd_bddAnd, f, g);
00859         if (r != NULL) return(r);
00860     }
00861 
00862     /* Here we can skip the use of cuddI, because the operands are known
00863     ** to be non-constant.
00864     */
00865     topf = manager->perm[F->index];
00866     topg = manager->perm[G->index];
00867 
00868     /* Compute cofactors. */
00869     if (topf <= topg) {
00870         index = F->index;
00871         fv = cuddT(F);
00872         fnv = cuddE(F);
00873         if (Cudd_IsComplement(f)) {
00874             fv = Cudd_Not(fv);
00875             fnv = Cudd_Not(fnv);
00876         }
00877     } else {
00878         index = G->index;
00879         fv = fnv = f;
00880     }
00881 
00882     if (topg <= topf) {
00883         gv = cuddT(G);
00884         gnv = cuddE(G);
00885         if (Cudd_IsComplement(g)) {
00886             gv = Cudd_Not(gv);
00887             gnv = Cudd_Not(gnv);
00888         }
00889     } else {
00890         gv = gnv = g;
00891     }
00892 
00893     t = cuddBddAndRecur(manager, fv, gv);
00894     if (t == NULL) return(NULL);
00895     cuddRef(t);
00896 
00897     e = cuddBddAndRecur(manager, fnv, gnv);
00898     if (e == NULL) {
00899         Cudd_IterDerefBdd(manager, t);
00900         return(NULL);
00901     }
00902     cuddRef(e);
00903 
00904     if (t == e) {
00905         r = t;
00906     } else {
00907         if (Cudd_IsComplement(t)) {
00908             r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
00909             if (r == NULL) {
00910                 Cudd_IterDerefBdd(manager, t);
00911                 Cudd_IterDerefBdd(manager, e);
00912                 return(NULL);
00913             }
00914             r = Cudd_Not(r);
00915         } else {
00916             r = cuddUniqueInter(manager,(int)index,t,e);
00917             if (r == NULL) {
00918                 Cudd_IterDerefBdd(manager, t);
00919                 Cudd_IterDerefBdd(manager, e);
00920                 return(NULL);
00921             }
00922         }
00923     }
00924     cuddDeref(e);
00925     cuddDeref(t);
00926     if (F->ref != 1 || G->ref != 1)
00927         cuddCacheInsert2(manager, Cudd_bddAnd, f, g, r);
00928     return(r);
00929 
00930 } /* end of cuddBddAndRecur */
00931 
00932 
00946 DdNode *
00947 cuddBddXorRecur(
00948   DdManager * manager,
00949   DdNode * f,
00950   DdNode * g)
00951 {
00952     DdNode *fv, *fnv, *G, *gv, *gnv;
00953     DdNode *one, *zero, *r, *t, *e;
00954     unsigned int topf, topg, index;
00955 
00956     statLine(manager);
00957     one = DD_ONE(manager);
00958     zero = Cudd_Not(one);
00959 
00960     /* Terminal cases. */
00961     if (f == g) return(zero);
00962     if (f == Cudd_Not(g)) return(one);
00963     if (f > g) { /* Try to increase cache efficiency and simplify tests. */
00964         DdNode *tmp = f;
00965         f = g;
00966         g = tmp;
00967     }
00968     if (g == zero) return(f);
00969     if (g == one) return(Cudd_Not(f));
00970     if (Cudd_IsComplement(f)) {
00971         f = Cudd_Not(f);
00972         g = Cudd_Not(g);
00973     }
00974     /* Now the first argument is regular. */
00975     if (f == one) return(Cudd_Not(g));
00976 
00977     /* At this point f and g are not constant. */
00978 
00979     /* Check cache. */
00980     r = cuddCacheLookup2(manager, Cudd_bddXor, f, g);
00981     if (r != NULL) return(r);
00982 
00983     /* Here we can skip the use of cuddI, because the operands are known
00984     ** to be non-constant.
00985     */
00986     topf = manager->perm[f->index];
00987     G = Cudd_Regular(g);
00988     topg = manager->perm[G->index];
00989 
00990     /* Compute cofactors. */
00991     if (topf <= topg) {
00992         index = f->index;
00993         fv = cuddT(f);
00994         fnv = cuddE(f);
00995     } else {
00996         index = G->index;
00997         fv = fnv = f;
00998     }
00999 
01000     if (topg <= topf) {
01001         gv = cuddT(G);
01002         gnv = cuddE(G);
01003         if (Cudd_IsComplement(g)) {
01004             gv = Cudd_Not(gv);
01005             gnv = Cudd_Not(gnv);
01006         }
01007     } else {
01008         gv = gnv = g;
01009     }
01010 
01011     t = cuddBddXorRecur(manager, fv, gv);
01012     if (t == NULL) return(NULL);
01013     cuddRef(t);
01014 
01015     e = cuddBddXorRecur(manager, fnv, gnv);
01016     if (e == NULL) {
01017         Cudd_IterDerefBdd(manager, t);
01018         return(NULL);
01019     }
01020     cuddRef(e);
01021 
01022     if (t == e) {
01023         r = t;
01024     } else {
01025         if (Cudd_IsComplement(t)) {
01026             r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
01027             if (r == NULL) {
01028                 Cudd_IterDerefBdd(manager, t);
01029                 Cudd_IterDerefBdd(manager, e);
01030                 return(NULL);
01031             }
01032             r = Cudd_Not(r);
01033         } else {
01034             r = cuddUniqueInter(manager,(int)index,t,e);
01035             if (r == NULL) {
01036                 Cudd_IterDerefBdd(manager, t);
01037                 Cudd_IterDerefBdd(manager, e);
01038                 return(NULL);
01039             }
01040         }
01041     }
01042     cuddDeref(e);
01043     cuddDeref(t);
01044     cuddCacheInsert2(manager, Cudd_bddXor, f, g, r);
01045     return(r);
01046 
01047 } /* end of cuddBddXorRecur */
01048 
01049 
01050 /*---------------------------------------------------------------------------*/
01051 /* Definition of static functions                                            */
01052 /*---------------------------------------------------------------------------*/
01053 
01054 
01067 static void
01068 bddVarToConst(
01069   DdNode * f,
01070   DdNode ** gp,
01071   DdNode ** hp,
01072   DdNode * one)
01073 {
01074     DdNode *g = *gp;
01075     DdNode *h = *hp;
01076 
01077     if (f == g) {    /* ITE(F,F,H) = ITE(F,1,H) = F + H */
01078         *gp = one;
01079     } else if (f == Cudd_Not(g)) {    /* ITE(F,!F,H) = ITE(F,0,H) = !F * H */
01080         *gp = Cudd_Not(one);
01081     }
01082     if (f == h) {    /* ITE(F,G,F) = ITE(F,G,0) = F * G */
01083         *hp = Cudd_Not(one);
01084     } else if (f == Cudd_Not(h)) {    /* ITE(F,G,!F) = ITE(F,G,1) = !F + G */
01085         *hp = one;
01086     }
01087 
01088 } /* end of bddVarToConst */
01089 
01090 
01102 static int
01103 bddVarToCanonical(
01104   DdManager * dd,
01105   DdNode ** fp,
01106   DdNode ** gp,
01107   DdNode ** hp,
01108   unsigned int * topfp,
01109   unsigned int * topgp,
01110   unsigned int * tophp)
01111 {
01112     register DdNode             *F, *G, *H, *r, *f, *g, *h;
01113     register unsigned int       topf, topg, toph;
01114     DdNode                      *one = dd->one;
01115     int                         comple, change;
01116 
01117     f = *fp;
01118     g = *gp;
01119     h = *hp;
01120     F = Cudd_Regular(f);
01121     G = Cudd_Regular(g);
01122     H = Cudd_Regular(h);
01123     topf = cuddI(dd,F->index);
01124     topg = cuddI(dd,G->index);
01125     toph = cuddI(dd,H->index);
01126 
01127     change = 0;
01128 
01129     if (G == one) {                     /* ITE(F,c,H) */
01130         if ((topf > toph) || (topf == toph && f > h)) {
01131             r = h;
01132             h = f;
01133             f = r;                      /* ITE(F,1,H) = ITE(H,1,F) */
01134             if (g != one) {     /* g == zero */
01135                 f = Cudd_Not(f);                /* ITE(F,0,H) = ITE(!H,0,!F) */
01136                 h = Cudd_Not(h);
01137             }
01138             change = 1;
01139         }
01140     } else if (H == one) {              /* ITE(F,G,c) */
01141         if ((topf > topg) || (topf == topg && f > g)) {
01142             r = g;
01143             g = f;
01144             f = r;                      /* ITE(F,G,0) = ITE(G,F,0) */
01145             if (h == one) {
01146                 f = Cudd_Not(f);                /* ITE(F,G,1) = ITE(!G,!F,1) */
01147                 g = Cudd_Not(g);
01148             }
01149             change = 1;
01150         }
01151     } else if (g == Cudd_Not(h)) {      /* ITE(F,G,!G) = ITE(G,F,!F) */
01152         if ((topf > topg) || (topf == topg && f > g)) {
01153             r = f;
01154             f = g;
01155             g = r;
01156             h = Cudd_Not(r);
01157             change = 1;
01158         }
01159     }
01160     /* adjust pointers so that the first 2 arguments to ITE are regular */
01161     if (Cudd_IsComplement(f) != 0) {    /* ITE(!F,G,H) = ITE(F,H,G) */
01162         f = Cudd_Not(f);
01163         r = g;
01164         g = h;
01165         h = r;
01166         change = 1;
01167     }
01168     comple = 0;
01169     if (Cudd_IsComplement(g) != 0) {    /* ITE(F,!G,H) = !ITE(F,G,!H) */
01170         g = Cudd_Not(g);
01171         h = Cudd_Not(h);
01172         change = 1;
01173         comple = 1;
01174     }
01175     if (change != 0) {
01176         *fp = f;
01177         *gp = g;
01178         *hp = h;
01179     }
01180     *topfp = cuddI(dd,f->index);
01181     *topgp = cuddI(dd,g->index);
01182     *tophp = cuddI(dd,Cudd_Regular(h)->index);
01183 
01184     return(comple);
01185 
01186 } /* end of bddVarToCanonical */
01187 
01188 
01204 static int
01205 bddVarToCanonicalSimple(
01206   DdManager * dd,
01207   DdNode ** fp,
01208   DdNode ** gp,
01209   DdNode ** hp,
01210   unsigned int * topfp,
01211   unsigned int * topgp,
01212   unsigned int * tophp)
01213 {
01214     register DdNode             *r, *f, *g, *h;
01215     int                         comple, change;
01216 
01217     f = *fp;
01218     g = *gp;
01219     h = *hp;
01220 
01221     change = 0;
01222 
01223     /* adjust pointers so that the first 2 arguments to ITE are regular */
01224     if (Cudd_IsComplement(f)) { /* 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)) { /* 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) {
01239         *fp = f;
01240         *gp = g;
01241         *hp = h;
01242     }
01243 
01244     /* Here we can skip the use of cuddI, because the operands are known
01245     ** to be non-constant.
01246     */
01247     *topfp = dd->perm[f->index];
01248     *topgp = dd->perm[g->index];
01249     *tophp = dd->perm[Cudd_Regular(h)->index];
01250 
01251     return(comple);
01252 
01253 } /* end of bddVarToCanonicalSimple */
01254