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

00001 
00076 #include "util.h"
00077 #include "cuddInt.h"
00078 
00079 
00080 /*---------------------------------------------------------------------------*/
00081 /* Constant declarations                                                     */
00082 /*---------------------------------------------------------------------------*/
00083 
00084 #define DD_DEBUG 1
00085 
00086 /*---------------------------------------------------------------------------*/
00087 /* Stucture declarations                                                     */
00088 /*---------------------------------------------------------------------------*/
00089 
00090 
00091 /*---------------------------------------------------------------------------*/
00092 /* Type declarations                                                         */
00093 /*---------------------------------------------------------------------------*/
00094 
00095 
00096 /*---------------------------------------------------------------------------*/
00097 /* Variable declarations                                                     */
00098 /*---------------------------------------------------------------------------*/
00099 
00100 #ifndef lint
00101 static char rcsid[] DD_UNUSED = "$Id: cuddPriority.c,v 1.33 2009/02/20 02:14:58 fabio Exp $";
00102 #endif
00103 
00104 /*---------------------------------------------------------------------------*/
00105 /* Macro declarations                                                        */
00106 /*---------------------------------------------------------------------------*/
00107 
00108 
00111 /*---------------------------------------------------------------------------*/
00112 /* Static function prototypes                                                */
00113 /*---------------------------------------------------------------------------*/
00114 static int cuddMinHammingDistRecur (DdNode * f, int *minterm, DdHashTable * table, int upperBound);
00115 static DdNode * separateCube (DdManager *dd, DdNode *f, CUDD_VALUE_TYPE *distance);
00116 static DdNode * createResult (DdManager *dd, unsigned int index, unsigned int phase, DdNode *cube, CUDD_VALUE_TYPE distance);
00117 
00121 /*---------------------------------------------------------------------------*/
00122 /* Definition of exported functions                                          */
00123 /*---------------------------------------------------------------------------*/
00124 
00125 
00170 DdNode *
00171 Cudd_PrioritySelect(
00172   DdManager * dd /* manager */,
00173   DdNode * R /* BDD of the relation */,
00174   DdNode ** x /* array of x variables */,
00175   DdNode ** y /* array of y variables */,
00176   DdNode ** z /* array of z variables (optional: may be NULL) */,
00177   DdNode * Pi /* BDD of the priority function (optional: may be NULL) */,
00178   int  n /* size of x, y, and z */,
00179   DD_PRFP Pifunc /* function used to build Pi if it is NULL */)
00180 {
00181     DdNode *res = NULL;
00182     DdNode *zcube = NULL;
00183     DdNode *Rxz, *Q;
00184     int createdZ = 0;
00185     int createdPi = 0;
00186     int i;
00187 
00188     /* Create z variables if needed. */
00189     if (z == NULL) {
00190         if (Pi != NULL) return(NULL);
00191         z = ALLOC(DdNode *,n);
00192         if (z == NULL) {
00193             dd->errorCode = CUDD_MEMORY_OUT;
00194             return(NULL);
00195         }
00196         createdZ = 1;
00197         for (i = 0; i < n; i++) {
00198             if (dd->size >= (int) CUDD_MAXINDEX - 1) goto endgame;
00199             z[i] = cuddUniqueInter(dd,dd->size,dd->one,Cudd_Not(dd->one));
00200             if (z[i] == NULL) goto endgame;
00201         }
00202     }
00203 
00204     /* Create priority function BDD if needed. */
00205     if (Pi == NULL) {
00206         Pi = Pifunc(dd,n,x,y,z);
00207         if (Pi == NULL) goto endgame;
00208         createdPi = 1;
00209         cuddRef(Pi);
00210     }
00211 
00212     /* Initialize abstraction cube. */
00213     zcube = DD_ONE(dd);
00214     cuddRef(zcube);
00215     for (i = n - 1; i >= 0; i--) {
00216         DdNode *tmpp;
00217         tmpp = Cudd_bddAnd(dd,z[i],zcube);
00218         if (tmpp == NULL) goto endgame;
00219         cuddRef(tmpp);
00220         Cudd_RecursiveDeref(dd,zcube);
00221         zcube = tmpp;
00222     }
00223 
00224     /* Compute subset of (x,y) pairs. */
00225     Rxz = Cudd_bddSwapVariables(dd,R,y,z,n);
00226     if (Rxz == NULL) goto endgame;
00227     cuddRef(Rxz);
00228     Q = Cudd_bddAndAbstract(dd,Rxz,Pi,zcube);
00229     if (Q == NULL) {
00230         Cudd_RecursiveDeref(dd,Rxz);
00231         goto endgame;
00232     }
00233     cuddRef(Q);
00234     Cudd_RecursiveDeref(dd,Rxz);
00235     res = Cudd_bddAnd(dd,R,Cudd_Not(Q));
00236     if (res == NULL) {
00237         Cudd_RecursiveDeref(dd,Q);
00238         goto endgame;
00239     }
00240     cuddRef(res);
00241     Cudd_RecursiveDeref(dd,Q);
00242 
00243 endgame:
00244     if (zcube != NULL) Cudd_RecursiveDeref(dd,zcube);
00245     if (createdZ) {
00246         FREE(z);
00247     }
00248     if (createdPi) {
00249         Cudd_RecursiveDeref(dd,Pi);
00250     }
00251     if (res != NULL) cuddDeref(res);
00252     return(res);
00253 
00254 } /* Cudd_PrioritySelect */
00255 
00256 
00275 DdNode *
00276 Cudd_Xgty(
00277   DdManager * dd /* DD manager */,
00278   int  N /* number of x and y variables */,
00279   DdNode ** z /* array of z variables: unused */,
00280   DdNode ** x /* array of x variables */,
00281   DdNode ** y /* array of y variables */)
00282 {
00283     DdNode *u, *v, *w;
00284     int     i;
00285 
00286     /* Build bottom part of BDD outside loop. */
00287     u = Cudd_bddAnd(dd, x[N-1], Cudd_Not(y[N-1]));
00288     if (u == NULL) return(NULL);
00289     cuddRef(u);
00290 
00291     /* Loop to build the rest of the BDD. */
00292     for (i = N-2; i >= 0; i--) {
00293         v = Cudd_bddAnd(dd, y[i], Cudd_Not(u));
00294         if (v == NULL) {
00295             Cudd_RecursiveDeref(dd, u);
00296             return(NULL);
00297         }
00298         cuddRef(v);
00299         w = Cudd_bddAnd(dd, Cudd_Not(y[i]), u);
00300         if (w == NULL) {
00301             Cudd_RecursiveDeref(dd, u);
00302             Cudd_RecursiveDeref(dd, v);
00303             return(NULL);
00304         }
00305         cuddRef(w);
00306         Cudd_RecursiveDeref(dd, u);
00307         u = Cudd_bddIte(dd, x[i], Cudd_Not(v), w);
00308         if (u == NULL) {
00309             Cudd_RecursiveDeref(dd, v);
00310             Cudd_RecursiveDeref(dd, w);
00311             return(NULL);
00312         }
00313         cuddRef(u);
00314         Cudd_RecursiveDeref(dd, v);
00315         Cudd_RecursiveDeref(dd, w);
00316 
00317     }
00318     cuddDeref(u);
00319     return(u);
00320 
00321 } /* end of Cudd_Xgty */
00322 
00323 
00340 DdNode *
00341 Cudd_Xeqy(
00342   DdManager * dd /* DD manager */,
00343   int  N /* number of x and y variables */,
00344   DdNode ** x /* array of x variables */,
00345   DdNode ** y /* array of y variables */)
00346 {
00347     DdNode *u, *v, *w;
00348     int     i;
00349 
00350     /* Build bottom part of BDD outside loop. */
00351     u = Cudd_bddIte(dd, x[N-1], y[N-1], Cudd_Not(y[N-1]));
00352     if (u == NULL) return(NULL);
00353     cuddRef(u);
00354 
00355     /* Loop to build the rest of the BDD. */
00356     for (i = N-2; i >= 0; i--) {
00357         v = Cudd_bddAnd(dd, y[i], u);
00358         if (v == NULL) {
00359             Cudd_RecursiveDeref(dd, u);
00360             return(NULL);
00361         }
00362         cuddRef(v);
00363         w = Cudd_bddAnd(dd, Cudd_Not(y[i]), u);
00364         if (w == NULL) {
00365             Cudd_RecursiveDeref(dd, u);
00366             Cudd_RecursiveDeref(dd, v);
00367             return(NULL);
00368         }
00369         cuddRef(w);
00370         Cudd_RecursiveDeref(dd, u);
00371         u = Cudd_bddIte(dd, x[i], v, w);
00372         if (u == NULL) {
00373             Cudd_RecursiveDeref(dd, v);
00374             Cudd_RecursiveDeref(dd, w);
00375             return(NULL);
00376         }
00377         cuddRef(u);
00378         Cudd_RecursiveDeref(dd, v);
00379         Cudd_RecursiveDeref(dd, w);
00380     }
00381     cuddDeref(u);
00382     return(u);
00383 
00384 } /* end of Cudd_Xeqy */
00385 
00386 
00403 DdNode *
00404 Cudd_addXeqy(
00405   DdManager * dd /* DD manager */,
00406   int  N /* number of x and y variables */,
00407   DdNode ** x /* array of x variables */,
00408   DdNode ** y /* array of y variables */)
00409 {
00410     DdNode *one, *zero;
00411     DdNode *u, *v, *w;
00412     int     i;
00413 
00414     one = DD_ONE(dd);
00415     zero = DD_ZERO(dd);
00416 
00417     /* Build bottom part of ADD outside loop. */
00418     v = Cudd_addIte(dd, y[N-1], one, zero);
00419     if (v == NULL) return(NULL);
00420     cuddRef(v);
00421     w = Cudd_addIte(dd, y[N-1], zero, one);
00422     if (w == NULL) {
00423         Cudd_RecursiveDeref(dd, v);
00424         return(NULL);
00425     }
00426     cuddRef(w);
00427     u = Cudd_addIte(dd, x[N-1], v, w);
00428     if (u == NULL) {
00429         Cudd_RecursiveDeref(dd, v);
00430         Cudd_RecursiveDeref(dd, w);
00431         return(NULL);
00432     }
00433     cuddRef(u);
00434     Cudd_RecursiveDeref(dd, v);
00435     Cudd_RecursiveDeref(dd, w);
00436 
00437     /* Loop to build the rest of the ADD. */
00438     for (i = N-2; i >= 0; i--) {
00439         v = Cudd_addIte(dd, y[i], u, zero);
00440         if (v == NULL) {
00441             Cudd_RecursiveDeref(dd, u);
00442             return(NULL);
00443         }
00444         cuddRef(v);
00445         w = Cudd_addIte(dd, y[i], zero, u);
00446         if (w == NULL) {
00447             Cudd_RecursiveDeref(dd, u);
00448             Cudd_RecursiveDeref(dd, v);
00449             return(NULL);
00450         }
00451         cuddRef(w);
00452         Cudd_RecursiveDeref(dd, u);
00453         u = Cudd_addIte(dd, x[i], v, w);
00454         if (w == NULL) {
00455             Cudd_RecursiveDeref(dd, v);
00456             Cudd_RecursiveDeref(dd, w);
00457             return(NULL);
00458         }
00459         cuddRef(u);
00460         Cudd_RecursiveDeref(dd, v);
00461         Cudd_RecursiveDeref(dd, w);
00462     }
00463     cuddDeref(u);
00464     return(u);
00465 
00466 } /* end of Cudd_addXeqy */
00467 
00468 
00489 DdNode *
00490 Cudd_Dxygtdxz(
00491   DdManager * dd /* DD manager */,
00492   int  N /* number of x, y, and z variables */,
00493   DdNode ** x /* array of x variables */,
00494   DdNode ** y /* array of y variables */,
00495   DdNode ** z /* array of z variables */)
00496 {
00497     DdNode *one, *zero;
00498     DdNode *z1, *z2, *z3, *z4, *y1_, *y2, *x1;
00499     int     i;
00500 
00501     one = DD_ONE(dd);
00502     zero = Cudd_Not(one);
00503 
00504     /* Build bottom part of BDD outside loop. */
00505     y1_ = Cudd_bddIte(dd, y[N-1], one, Cudd_Not(z[N-1]));
00506     if (y1_ == NULL) return(NULL);
00507     cuddRef(y1_);
00508     y2 = Cudd_bddIte(dd, y[N-1], z[N-1], one);
00509     if (y2 == NULL) {
00510         Cudd_RecursiveDeref(dd, y1_);
00511         return(NULL);
00512     }
00513     cuddRef(y2);
00514     x1 = Cudd_bddIte(dd, x[N-1], y1_, y2);
00515     if (x1 == NULL) {
00516         Cudd_RecursiveDeref(dd, y1_);
00517         Cudd_RecursiveDeref(dd, y2);
00518         return(NULL);
00519     }
00520     cuddRef(x1);
00521     Cudd_RecursiveDeref(dd, y1_);
00522     Cudd_RecursiveDeref(dd, y2);
00523 
00524     /* Loop to build the rest of the BDD. */
00525     for (i = N-2; i >= 0; i--) {
00526         z1 = Cudd_bddIte(dd, z[i], one, Cudd_Not(x1));
00527         if (z1 == NULL) {
00528             Cudd_RecursiveDeref(dd, x1);
00529             return(NULL);
00530         }
00531         cuddRef(z1);
00532         z2 = Cudd_bddIte(dd, z[i], x1, one);
00533         if (z2 == NULL) {
00534             Cudd_RecursiveDeref(dd, x1);
00535             Cudd_RecursiveDeref(dd, z1);
00536             return(NULL);
00537         }
00538         cuddRef(z2);
00539         z3 = Cudd_bddIte(dd, z[i], one, x1);
00540         if (z3 == NULL) {
00541             Cudd_RecursiveDeref(dd, x1);
00542             Cudd_RecursiveDeref(dd, z1);
00543             Cudd_RecursiveDeref(dd, z2);
00544             return(NULL);
00545         }
00546         cuddRef(z3);
00547         z4 = Cudd_bddIte(dd, z[i], x1, zero);
00548         if (z4 == NULL) {
00549             Cudd_RecursiveDeref(dd, x1);
00550             Cudd_RecursiveDeref(dd, z1);
00551             Cudd_RecursiveDeref(dd, z2);
00552             Cudd_RecursiveDeref(dd, z3);
00553             return(NULL);
00554         }
00555         cuddRef(z4);
00556         Cudd_RecursiveDeref(dd, x1);
00557         y1_ = Cudd_bddIte(dd, y[i], z2, Cudd_Not(z1));
00558         if (y1_ == NULL) {
00559             Cudd_RecursiveDeref(dd, z1);
00560             Cudd_RecursiveDeref(dd, z2);
00561             Cudd_RecursiveDeref(dd, z3);
00562             Cudd_RecursiveDeref(dd, z4);
00563             return(NULL);
00564         }
00565         cuddRef(y1_);
00566         y2 = Cudd_bddIte(dd, y[i], z4, z3);
00567         if (y2 == NULL) {
00568             Cudd_RecursiveDeref(dd, z1);
00569             Cudd_RecursiveDeref(dd, z2);
00570             Cudd_RecursiveDeref(dd, z3);
00571             Cudd_RecursiveDeref(dd, z4);
00572             Cudd_RecursiveDeref(dd, y1_);
00573             return(NULL);
00574         }
00575         cuddRef(y2);
00576         Cudd_RecursiveDeref(dd, z1);
00577         Cudd_RecursiveDeref(dd, z2);
00578         Cudd_RecursiveDeref(dd, z3);
00579         Cudd_RecursiveDeref(dd, z4);
00580         x1 = Cudd_bddIte(dd, x[i], y1_, y2);
00581         if (x1 == NULL) {
00582             Cudd_RecursiveDeref(dd, y1_);
00583             Cudd_RecursiveDeref(dd, y2);
00584             return(NULL);
00585         }
00586         cuddRef(x1);
00587         Cudd_RecursiveDeref(dd, y1_);
00588         Cudd_RecursiveDeref(dd, y2);
00589     }
00590     cuddDeref(x1);
00591     return(Cudd_Not(x1));
00592 
00593 } /* end of Cudd_Dxygtdxz */
00594 
00595 
00616 DdNode *
00617 Cudd_Dxygtdyz(
00618   DdManager * dd /* DD manager */,
00619   int  N /* number of x, y, and z variables */,
00620   DdNode ** x /* array of x variables */,
00621   DdNode ** y /* array of y variables */,
00622   DdNode ** z /* array of z variables */)
00623 {
00624     DdNode *one, *zero;
00625     DdNode *z1, *z2, *z3, *z4, *y1_, *y2, *x1;
00626     int     i;
00627 
00628     one = DD_ONE(dd);
00629     zero = Cudd_Not(one);
00630 
00631     /* Build bottom part of BDD outside loop. */
00632     y1_ = Cudd_bddIte(dd, y[N-1], one, z[N-1]);
00633     if (y1_ == NULL) return(NULL);
00634     cuddRef(y1_);
00635     y2 = Cudd_bddIte(dd, y[N-1], z[N-1], zero);
00636     if (y2 == NULL) {
00637         Cudd_RecursiveDeref(dd, y1_);
00638         return(NULL);
00639     }
00640     cuddRef(y2);
00641     x1 = Cudd_bddIte(dd, x[N-1], y1_, Cudd_Not(y2));
00642     if (x1 == NULL) {
00643         Cudd_RecursiveDeref(dd, y1_);
00644         Cudd_RecursiveDeref(dd, y2);
00645         return(NULL);
00646     }
00647     cuddRef(x1);
00648     Cudd_RecursiveDeref(dd, y1_);
00649     Cudd_RecursiveDeref(dd, y2);
00650 
00651     /* Loop to build the rest of the BDD. */
00652     for (i = N-2; i >= 0; i--) {
00653         z1 = Cudd_bddIte(dd, z[i], x1, zero);
00654         if (z1 == NULL) {
00655             Cudd_RecursiveDeref(dd, x1);
00656             return(NULL);
00657         }
00658         cuddRef(z1);
00659         z2 = Cudd_bddIte(dd, z[i], x1, one);
00660         if (z2 == NULL) {
00661             Cudd_RecursiveDeref(dd, x1);
00662             Cudd_RecursiveDeref(dd, z1);
00663             return(NULL);
00664         }
00665         cuddRef(z2);
00666         z3 = Cudd_bddIte(dd, z[i], one, x1);
00667         if (z3 == NULL) {
00668             Cudd_RecursiveDeref(dd, x1);
00669             Cudd_RecursiveDeref(dd, z1);
00670             Cudd_RecursiveDeref(dd, z2);
00671             return(NULL);
00672         }
00673         cuddRef(z3);
00674         z4 = Cudd_bddIte(dd, z[i], one, Cudd_Not(x1));
00675         if (z4 == NULL) {
00676             Cudd_RecursiveDeref(dd, x1);
00677             Cudd_RecursiveDeref(dd, z1);
00678             Cudd_RecursiveDeref(dd, z2);
00679             Cudd_RecursiveDeref(dd, z3);
00680             return(NULL);
00681         }
00682         cuddRef(z4);
00683         Cudd_RecursiveDeref(dd, x1);
00684         y1_ = Cudd_bddIte(dd, y[i], z2, z1);
00685         if (y1_ == NULL) {
00686             Cudd_RecursiveDeref(dd, z1);
00687             Cudd_RecursiveDeref(dd, z2);
00688             Cudd_RecursiveDeref(dd, z3);
00689             Cudd_RecursiveDeref(dd, z4);
00690             return(NULL);
00691         }
00692         cuddRef(y1_);
00693         y2 = Cudd_bddIte(dd, y[i], z4, Cudd_Not(z3));
00694         if (y2 == NULL) {
00695             Cudd_RecursiveDeref(dd, z1);
00696             Cudd_RecursiveDeref(dd, z2);
00697             Cudd_RecursiveDeref(dd, z3);
00698             Cudd_RecursiveDeref(dd, z4);
00699             Cudd_RecursiveDeref(dd, y1_);
00700             return(NULL);
00701         }
00702         cuddRef(y2);
00703         Cudd_RecursiveDeref(dd, z1);
00704         Cudd_RecursiveDeref(dd, z2);
00705         Cudd_RecursiveDeref(dd, z3);
00706         Cudd_RecursiveDeref(dd, z4);
00707         x1 = Cudd_bddIte(dd, x[i], y1_, Cudd_Not(y2));
00708         if (x1 == NULL) {
00709             Cudd_RecursiveDeref(dd, y1_);
00710             Cudd_RecursiveDeref(dd, y2);
00711             return(NULL);
00712         }
00713         cuddRef(x1);
00714         Cudd_RecursiveDeref(dd, y1_);
00715         Cudd_RecursiveDeref(dd, y2);
00716     }
00717     cuddDeref(x1);
00718     return(Cudd_Not(x1));
00719 
00720 } /* end of Cudd_Dxygtdyz */
00721 
00722 
00739 DdNode *
00740 Cudd_Inequality(
00741   DdManager * dd /* DD manager */,
00742   int  N /* number of x and y variables */,
00743   int c /* right-hand side constant */,
00744   DdNode ** x /* array of x variables */,
00745   DdNode ** y /* array of y variables */)
00746 {
00747     /* The nodes at level i represent values of the difference that are
00748     ** multiples of 2^i.  We use variables with names starting with k
00749     ** to denote the multipliers of 2^i in such multiples. */
00750     int kTrue = c;
00751     int kFalse = c - 1;
00752     /* Mask used to compute the ceiling function.  Since we divide by 2^i,
00753     ** we want to know whether the dividend is a multiple of 2^i.  If it is,
00754     ** then ceiling and floor coincide; otherwise, they differ by one. */
00755     int mask = 1;
00756     int i;
00757 
00758     DdNode *f = NULL;           /* the eventual result */
00759     DdNode *one = DD_ONE(dd);
00760     DdNode *zero = Cudd_Not(one);
00761 
00762     /* Two x-labeled nodes are created at most at each iteration.  They are
00763     ** stored, along with their k values, in these variables.  At each level,
00764     ** the old nodes are freed and the new nodes are copied into the old map.
00765     */
00766     DdNode *map[2];
00767     int invalidIndex = 1 << (N-1);
00768     int index[2] = {invalidIndex, invalidIndex};
00769 
00770     /* This should never happen. */
00771     if (N < 0) return(NULL);
00772 
00773     /* If there are no bits, both operands are 0.  The result depends on c. */
00774     if (N == 0) {
00775         if (c >= 0) return(one);
00776         else return(zero);
00777     }
00778 
00779     /* The maximum or the minimum difference comparing to c can generate the terminal case */
00780     if ((1 << N) - 1 < c) return(zero);
00781     else if ((-(1 << N) + 1) >= c) return(one);
00782 
00783     /* Build the result bottom up. */
00784     for (i = 1; i <= N; i++) {
00785         int kTrueLower, kFalseLower;
00786         int leftChild, middleChild, rightChild;
00787         DdNode *g0, *g1, *fplus, *fequal, *fminus;
00788         int j;
00789         DdNode *newMap[2];
00790         int newIndex[2];
00791 
00792         kTrueLower = kTrue;
00793         kFalseLower = kFalse;
00794         /* kTrue = ceiling((c-1)/2^i) + 1 */
00795         kTrue = ((c-1) >> i) + ((c & mask) != 1) + 1;
00796         mask = (mask << 1) | 1;
00797         /* kFalse = floor(c/2^i) - 1 */
00798         kFalse = (c >> i) - 1;
00799         newIndex[0] = invalidIndex;
00800         newIndex[1] = invalidIndex;
00801 
00802         for (j = kFalse + 1; j < kTrue; j++) {
00803             /* Skip if node is not reachable from top of BDD. */
00804             if ((j >= (1 << (N - i))) || (j <= -(1 << (N -i)))) continue;
00805 
00806             /* Find f- */
00807             leftChild = (j << 1) - 1;
00808             if (leftChild >= kTrueLower) {
00809                 fminus = one;
00810             } else if (leftChild <= kFalseLower) {
00811                 fminus = zero;
00812             } else {
00813                 assert(leftChild == index[0] || leftChild == index[1]);
00814                 if (leftChild == index[0]) {
00815                     fminus = map[0];
00816                 } else {
00817                     fminus = map[1];
00818                 }
00819             }
00820 
00821             /* Find f= */
00822             middleChild = j << 1;
00823             if (middleChild >= kTrueLower) {
00824                 fequal = one;
00825             } else if (middleChild <= kFalseLower) {
00826                 fequal = zero;
00827             } else {
00828                 assert(middleChild == index[0] || middleChild == index[1]);
00829                 if (middleChild == index[0]) {
00830                     fequal = map[0];
00831                 } else {
00832                     fequal = map[1];
00833                 }
00834             }
00835 
00836             /* Find f+ */
00837             rightChild = (j << 1) + 1;
00838             if (rightChild >= kTrueLower) {
00839                 fplus = one;
00840             } else if (rightChild <= kFalseLower) {
00841                 fplus = zero;
00842             } else {
00843                 assert(rightChild == index[0] || rightChild == index[1]);
00844                 if (rightChild == index[0]) {
00845                     fplus = map[0];
00846                 } else {
00847                     fplus = map[1];
00848                 }
00849             }
00850 
00851             /* Build new nodes. */
00852             g1 = Cudd_bddIte(dd, y[N - i], fequal, fplus);
00853             if (g1 == NULL) {
00854                 if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]);
00855                 if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]);
00856                 if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]);
00857                 if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]);
00858                 return(NULL);
00859             }
00860             cuddRef(g1);
00861             g0 = Cudd_bddIte(dd, y[N - i], fminus, fequal);
00862             if (g0 == NULL) {
00863                 Cudd_IterDerefBdd(dd, g1);
00864                 if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]);
00865                 if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]);
00866                 if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]);
00867                 if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]);
00868                 return(NULL);
00869             }
00870             cuddRef(g0);
00871             f = Cudd_bddIte(dd, x[N - i], g1, g0);
00872             if (f == NULL) {
00873                 Cudd_IterDerefBdd(dd, g1);
00874                 Cudd_IterDerefBdd(dd, g0);
00875                 if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]);
00876                 if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]);
00877                 if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]);
00878                 if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]);
00879                 return(NULL);
00880             }
00881             cuddRef(f);
00882             Cudd_IterDerefBdd(dd, g1);
00883             Cudd_IterDerefBdd(dd, g0);
00884 
00885             /* Save newly computed node in map. */
00886             assert(newIndex[0] == invalidIndex || newIndex[1] == invalidIndex);
00887             if (newIndex[0] == invalidIndex) {
00888                 newIndex[0] = j;
00889                 newMap[0] = f;
00890             } else {
00891                 newIndex[1] = j;
00892                 newMap[1] = f;
00893             }
00894         }
00895 
00896         /* Copy new map to map. */
00897         if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]);
00898         if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]);
00899         map[0] = newMap[0];
00900         map[1] = newMap[1];
00901         index[0] = newIndex[0];
00902         index[1] = newIndex[1];
00903     }
00904 
00905     cuddDeref(f);
00906     return(f);
00907 
00908 } /* end of Cudd_Inequality */
00909 
00910 
00927 DdNode *
00928 Cudd_Disequality(
00929   DdManager * dd /* DD manager */,
00930   int  N /* number of x and y variables */,
00931   int c /* right-hand side constant */,
00932   DdNode ** x /* array of x variables */,
00933   DdNode ** y /* array of y variables */)
00934 {
00935     /* The nodes at level i represent values of the difference that are
00936     ** multiples of 2^i.  We use variables with names starting with k
00937     ** to denote the multipliers of 2^i in such multiples. */
00938     int kTrueLb = c + 1;
00939     int kTrueUb = c - 1;
00940     int kFalse = c;
00941     /* Mask used to compute the ceiling function.  Since we divide by 2^i,
00942     ** we want to know whether the dividend is a multiple of 2^i.  If it is,
00943     ** then ceiling and floor coincide; otherwise, they differ by one. */
00944     int mask = 1;
00945     int i;
00946 
00947     DdNode *f = NULL;           /* the eventual result */
00948     DdNode *one = DD_ONE(dd);
00949     DdNode *zero = Cudd_Not(one);
00950 
00951     /* Two x-labeled nodes are created at most at each iteration.  They are
00952     ** stored, along with their k values, in these variables.  At each level,
00953     ** the old nodes are freed and the new nodes are copied into the old map.
00954     */
00955     DdNode *map[2];
00956     int invalidIndex = 1 << (N-1);
00957     int index[2] = {invalidIndex, invalidIndex};
00958 
00959     /* This should never happen. */
00960     if (N < 0) return(NULL);
00961 
00962     /* If there are no bits, both operands are 0.  The result depends on c. */
00963     if (N == 0) {
00964         if (c != 0) return(one);
00965         else return(zero);
00966     }
00967 
00968     /* The maximum or the minimum difference comparing to c can generate the terminal case */
00969     if ((1 << N) - 1 < c || (-(1 << N) + 1) > c) return(one);
00970 
00971     /* Build the result bottom up. */
00972     for (i = 1; i <= N; i++) {
00973         int kTrueLbLower, kTrueUbLower;
00974         int leftChild, middleChild, rightChild;
00975         DdNode *g0, *g1, *fplus, *fequal, *fminus;
00976         int j;
00977         DdNode *newMap[2];
00978         int newIndex[2];
00979 
00980         kTrueLbLower = kTrueLb;
00981         kTrueUbLower = kTrueUb;
00982         /* kTrueLb = floor((c-1)/2^i) + 2 */
00983         kTrueLb = ((c-1) >> i) + 2;
00984         /* kTrueUb = ceiling((c+1)/2^i) - 2 */
00985         kTrueUb = ((c+1) >> i) + (((c+2) & mask) != 1) - 2;
00986         mask = (mask << 1) | 1;
00987         newIndex[0] = invalidIndex;
00988         newIndex[1] = invalidIndex;
00989 
00990         for (j = kTrueUb + 1; j < kTrueLb; j++) {
00991             /* Skip if node is not reachable from top of BDD. */
00992             if ((j >= (1 << (N - i))) || (j <= -(1 << (N -i)))) continue;
00993 
00994             /* Find f- */
00995             leftChild = (j << 1) - 1;
00996             if (leftChild >= kTrueLbLower || leftChild <= kTrueUbLower) {
00997                 fminus = one;
00998             } else if (i == 1 && leftChild == kFalse) {
00999                 fminus = zero;
01000             } else {
01001                 assert(leftChild == index[0] || leftChild == index[1]);
01002                 if (leftChild == index[0]) {
01003                     fminus = map[0];
01004                 } else {
01005                     fminus = map[1];
01006                 }
01007             }
01008 
01009             /* Find f= */
01010             middleChild = j << 1;
01011             if (middleChild >= kTrueLbLower || middleChild <= kTrueUbLower) {
01012                 fequal = one;
01013             } else if (i == 1 && middleChild == kFalse) {
01014                 fequal = zero;
01015             } else {
01016                 assert(middleChild == index[0] || middleChild == index[1]);
01017                 if (middleChild == index[0]) {
01018                     fequal = map[0];
01019                 } else {
01020                     fequal = map[1];
01021                 }
01022             }
01023 
01024             /* Find f+ */
01025             rightChild = (j << 1) + 1;
01026             if (rightChild >= kTrueLbLower || rightChild <= kTrueUbLower) {
01027                 fplus = one;
01028             } else if (i == 1 && rightChild == kFalse) {
01029                 fplus = zero;
01030             } else {
01031                 assert(rightChild == index[0] || rightChild == index[1]);
01032                 if (rightChild == index[0]) {
01033                     fplus = map[0];
01034                 } else {
01035                     fplus = map[1];
01036                 }
01037             }
01038 
01039             /* Build new nodes. */
01040             g1 = Cudd_bddIte(dd, y[N - i], fequal, fplus);
01041             if (g1 == NULL) {
01042                 if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]);
01043                 if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]);
01044                 if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]);
01045                 if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]);
01046                 return(NULL);
01047             }
01048             cuddRef(g1);
01049             g0 = Cudd_bddIte(dd, y[N - i], fminus, fequal);
01050             if (g0 == NULL) {
01051                 Cudd_IterDerefBdd(dd, g1);
01052                 if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]);
01053                 if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]);
01054                 if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]);
01055                 if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]);
01056                 return(NULL);
01057             }
01058             cuddRef(g0);
01059             f = Cudd_bddIte(dd, x[N - i], g1, g0);
01060             if (f == NULL) {
01061                 Cudd_IterDerefBdd(dd, g1);
01062                 Cudd_IterDerefBdd(dd, g0);
01063                 if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]);
01064                 if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]);
01065                 if (newIndex[0] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[0]);
01066                 if (newIndex[1] != invalidIndex) Cudd_IterDerefBdd(dd, newMap[1]);
01067                 return(NULL);
01068             }
01069             cuddRef(f);
01070             Cudd_IterDerefBdd(dd, g1);
01071             Cudd_IterDerefBdd(dd, g0);
01072 
01073             /* Save newly computed node in map. */
01074             assert(newIndex[0] == invalidIndex || newIndex[1] == invalidIndex);
01075             if (newIndex[0] == invalidIndex) {
01076                 newIndex[0] = j;
01077                 newMap[0] = f;
01078             } else {
01079                 newIndex[1] = j;
01080                 newMap[1] = f;
01081             }
01082         }
01083 
01084         /* Copy new map to map. */
01085         if (index[0] != invalidIndex) Cudd_IterDerefBdd(dd, map[0]);
01086         if (index[1] != invalidIndex) Cudd_IterDerefBdd(dd, map[1]);
01087         map[0] = newMap[0];
01088         map[1] = newMap[1];
01089         index[0] = newIndex[0];
01090         index[1] = newIndex[1];
01091     }
01092 
01093     cuddDeref(f);
01094     return(f);
01095 
01096 } /* end of Cudd_Disequality */
01097 
01098 
01116 DdNode *
01117 Cudd_bddInterval(
01118   DdManager * dd /* DD manager */,
01119   int  N /* number of x variables */,
01120   DdNode ** x /* array of x variables */,
01121   unsigned int lowerB /* lower bound */,
01122   unsigned int upperB /* upper bound */)
01123 {
01124     DdNode *one, *zero;
01125     DdNode *r, *rl, *ru;
01126     int     i;
01127 
01128     one = DD_ONE(dd);
01129     zero = Cudd_Not(one);
01130 
01131     rl = one;
01132     cuddRef(rl);
01133     ru = one;
01134     cuddRef(ru);
01135 
01136     /* Loop to build the rest of the BDDs. */
01137     for (i = N-1; i >= 0; i--) {
01138         DdNode *vl, *vu;
01139         vl = Cudd_bddIte(dd, x[i],
01140                          lowerB&1 ? rl : one,
01141                          lowerB&1 ? zero : rl);
01142         if (vl == NULL) {
01143             Cudd_IterDerefBdd(dd, rl);
01144             Cudd_IterDerefBdd(dd, ru);
01145             return(NULL);
01146         }
01147         cuddRef(vl);
01148         Cudd_IterDerefBdd(dd, rl);
01149         rl = vl;
01150         lowerB >>= 1;
01151         vu = Cudd_bddIte(dd, x[i],
01152                          upperB&1 ? ru : zero,
01153                          upperB&1 ? one : ru);
01154         if (vu == NULL) {
01155             Cudd_IterDerefBdd(dd, rl);
01156             Cudd_IterDerefBdd(dd, ru);
01157             return(NULL);
01158         }
01159         cuddRef(vu);
01160         Cudd_IterDerefBdd(dd, ru);
01161         ru = vu;
01162         upperB >>= 1;
01163     }
01164 
01165     /* Conjoin the two bounds. */
01166     r = Cudd_bddAnd(dd, rl, ru);
01167     if (r == NULL) {
01168         Cudd_IterDerefBdd(dd, rl);
01169         Cudd_IterDerefBdd(dd, ru);
01170         return(NULL);
01171     }
01172     cuddRef(r);
01173     Cudd_IterDerefBdd(dd, rl);
01174     Cudd_IterDerefBdd(dd, ru);
01175     cuddDeref(r);
01176     return(r);
01177 
01178 } /* end of Cudd_bddInterval */
01179 
01180 
01195 DdNode *
01196 Cudd_CProjection(
01197   DdManager * dd,
01198   DdNode * R,
01199   DdNode * Y)
01200 {
01201     DdNode *res;
01202     DdNode *support;
01203 
01204     if (cuddCheckCube(dd,Y) == 0) {
01205         (void) fprintf(dd->err,
01206         "Error: The third argument of Cudd_CProjection should be a cube\n");
01207         dd->errorCode = CUDD_INVALID_ARG;
01208         return(NULL);
01209     }
01210 
01211     /* Compute the support of Y, which is used by the abstraction step
01212     ** in cuddCProjectionRecur.
01213     */
01214     support = Cudd_Support(dd,Y);
01215     if (support == NULL) return(NULL);
01216     cuddRef(support);
01217 
01218     do {
01219         dd->reordered = 0;
01220         res = cuddCProjectionRecur(dd,R,Y,support);
01221     } while (dd->reordered == 1);
01222 
01223     if (res == NULL) {
01224         Cudd_RecursiveDeref(dd,support);
01225         return(NULL);
01226     }
01227     cuddRef(res);
01228     Cudd_RecursiveDeref(dd,support);
01229     cuddDeref(res);
01230 
01231     return(res);
01232 
01233 } /* end of Cudd_CProjection */
01234 
01235 
01250 DdNode *
01251 Cudd_addHamming(
01252   DdManager * dd,
01253   DdNode ** xVars,
01254   DdNode ** yVars,
01255   int  nVars)
01256 {
01257     DdNode  *result,*tempBdd;
01258     DdNode  *tempAdd,*temp;
01259     int     i;
01260 
01261     result = DD_ZERO(dd);
01262     cuddRef(result);
01263 
01264     for (i = 0; i < nVars; i++) {
01265         tempBdd = Cudd_bddIte(dd,xVars[i],Cudd_Not(yVars[i]),yVars[i]);
01266         if (tempBdd == NULL) {
01267             Cudd_RecursiveDeref(dd,result);
01268             return(NULL);
01269         }
01270         cuddRef(tempBdd);
01271         tempAdd = Cudd_BddToAdd(dd,tempBdd);
01272         if (tempAdd == NULL) {
01273             Cudd_RecursiveDeref(dd,tempBdd);
01274             Cudd_RecursiveDeref(dd,result);
01275             return(NULL);
01276         }
01277         cuddRef(tempAdd);
01278         Cudd_RecursiveDeref(dd,tempBdd);
01279         temp = Cudd_addApply(dd,Cudd_addPlus,tempAdd,result);
01280         if (temp == NULL) {
01281             Cudd_RecursiveDeref(dd,tempAdd);
01282             Cudd_RecursiveDeref(dd,result);
01283             return(NULL);
01284         }
01285         cuddRef(temp);
01286         Cudd_RecursiveDeref(dd,tempAdd);
01287         Cudd_RecursiveDeref(dd,result);
01288         result = temp;
01289     }
01290 
01291     cuddDeref(result);
01292     return(result);
01293 
01294 } /* end of Cudd_addHamming */
01295 
01296 
01313 int
01314 Cudd_MinHammingDist(
01315   DdManager *dd /* DD manager */,
01316   DdNode *f /* function to examine */,
01317   int *minterm /* reference minterm */,
01318   int upperBound /* distance above which an approximate answer is OK */)
01319 {
01320     DdHashTable *table;
01321     CUDD_VALUE_TYPE epsilon;
01322     int res;
01323 
01324     table = cuddHashTableInit(dd,1,2);
01325     if (table == NULL) {
01326         return(CUDD_OUT_OF_MEM);
01327     }
01328     epsilon = Cudd_ReadEpsilon(dd);
01329     Cudd_SetEpsilon(dd,(CUDD_VALUE_TYPE)0.0);
01330     res = cuddMinHammingDistRecur(f,minterm,table,upperBound);
01331     cuddHashTableQuit(table);
01332     Cudd_SetEpsilon(dd,epsilon);
01333 
01334     return(res);
01335 
01336 } /* end of Cudd_MinHammingDist */
01337 
01338 
01354 DdNode *
01355 Cudd_bddClosestCube(
01356   DdManager *dd,
01357   DdNode * f,
01358   DdNode *g,
01359   int *distance)
01360 {
01361     DdNode *res, *acube;
01362     CUDD_VALUE_TYPE rdist;
01363 
01364     /* Compute the cube and distance as a single ADD. */
01365     do {
01366         dd->reordered = 0;
01367         res = cuddBddClosestCube(dd,f,g,CUDD_CONST_INDEX + 1.0);
01368     } while (dd->reordered == 1);
01369     if (res == NULL) return(NULL);
01370     cuddRef(res);
01371 
01372     /* Unpack distance and cube. */
01373     do {
01374         dd->reordered = 0;
01375         acube = separateCube(dd, res, &rdist);
01376     } while (dd->reordered == 1);
01377     if (acube == NULL) {
01378         Cudd_RecursiveDeref(dd, res);
01379         return(NULL);
01380     }
01381     cuddRef(acube);
01382     Cudd_RecursiveDeref(dd, res);
01383 
01384     /* Convert cube from ADD to BDD. */
01385     do {
01386         dd->reordered = 0;
01387         res = cuddAddBddDoPattern(dd, acube);
01388     } while (dd->reordered == 1);
01389     if (res == NULL) {
01390         Cudd_RecursiveDeref(dd, acube);
01391         return(NULL);
01392     }
01393     cuddRef(res);
01394     Cudd_RecursiveDeref(dd, acube);
01395 
01396     *distance = (int) rdist;
01397     cuddDeref(res);
01398     return(res);
01399 
01400 } /* end of Cudd_bddClosestCube */
01401 
01402 
01403 /*---------------------------------------------------------------------------*/
01404 /* Definition of internal functions                                          */
01405 /*---------------------------------------------------------------------------*/
01406 
01407 
01420 DdNode *
01421 cuddCProjectionRecur(
01422   DdManager * dd,
01423   DdNode * R,
01424   DdNode * Y,
01425   DdNode * Ysupp)
01426 {
01427     DdNode *res, *res1, *res2, *resA;
01428     DdNode *r, *y, *RT, *RE, *YT, *YE, *Yrest, *Ra, *Ran, *Gamma, *Alpha;
01429     unsigned int topR, topY, top, index;
01430     DdNode *one = DD_ONE(dd);
01431 
01432     statLine(dd);
01433     if (Y == one) return(R);
01434 
01435 #ifdef DD_DEBUG
01436     assert(!Cudd_IsConstant(Y));
01437 #endif
01438 
01439     if (R == Cudd_Not(one)) return(R);
01440 
01441     res = cuddCacheLookup2(dd, Cudd_CProjection, R, Y);
01442     if (res != NULL) return(res);
01443 
01444     r = Cudd_Regular(R);
01445     topR = cuddI(dd,r->index);
01446     y = Cudd_Regular(Y);
01447     topY = cuddI(dd,y->index);
01448 
01449     top = ddMin(topR, topY);
01450 
01451     /* Compute the cofactors of R */
01452     if (topR == top) {
01453         index = r->index;
01454         RT = cuddT(r);
01455         RE = cuddE(r);
01456         if (r != R) {
01457             RT = Cudd_Not(RT); RE = Cudd_Not(RE);
01458         }
01459     } else {
01460         RT = RE = R;
01461     }
01462 
01463     if (topY > top) {
01464         /* Y does not depend on the current top variable.
01465         ** We just need to compute the results on the two cofactors of R
01466         ** and make them the children of a node labeled r->index.
01467         */
01468         res1 = cuddCProjectionRecur(dd,RT,Y,Ysupp);
01469         if (res1 == NULL) return(NULL);
01470         cuddRef(res1);
01471         res2 = cuddCProjectionRecur(dd,RE,Y,Ysupp);
01472         if (res2 == NULL) {
01473             Cudd_RecursiveDeref(dd,res1);
01474             return(NULL);
01475         }
01476         cuddRef(res2);
01477         res = cuddBddIteRecur(dd, dd->vars[index], res1, res2);
01478         if (res == NULL) {
01479             Cudd_RecursiveDeref(dd,res1);
01480             Cudd_RecursiveDeref(dd,res2);
01481             return(NULL);
01482         }
01483         /* If we have reached this point, res1 and res2 are now
01484         ** incorporated in res. cuddDeref is therefore sufficient.
01485         */
01486         cuddDeref(res1);
01487         cuddDeref(res2);
01488     } else {
01489         /* Compute the cofactors of Y */
01490         index = y->index;
01491         YT = cuddT(y);
01492         YE = cuddE(y);
01493         if (y != Y) {
01494             YT = Cudd_Not(YT); YE = Cudd_Not(YE);
01495         }
01496         if (YT == Cudd_Not(one)) {
01497             Alpha  = Cudd_Not(dd->vars[index]);
01498             Yrest = YE;
01499             Ra = RE;
01500             Ran = RT;
01501         } else {
01502             Alpha = dd->vars[index];
01503             Yrest = YT;
01504             Ra = RT;
01505             Ran = RE;
01506         }
01507         Gamma = cuddBddExistAbstractRecur(dd,Ra,cuddT(Ysupp));
01508         if (Gamma == NULL) return(NULL);
01509         if (Gamma == one) {
01510             res1 = cuddCProjectionRecur(dd,Ra,Yrest,cuddT(Ysupp));
01511             if (res1 == NULL) return(NULL);
01512             cuddRef(res1);
01513             res = cuddBddAndRecur(dd, Alpha, res1);
01514             if (res == NULL) {
01515                 Cudd_RecursiveDeref(dd,res1);
01516                 return(NULL);
01517             }
01518             cuddDeref(res1);
01519         } else if (Gamma == Cudd_Not(one)) {
01520             res1 = cuddCProjectionRecur(dd,Ran,Yrest,cuddT(Ysupp));
01521             if (res1 == NULL) return(NULL);
01522             cuddRef(res1);
01523             res = cuddBddAndRecur(dd, Cudd_Not(Alpha), res1);
01524             if (res == NULL) {
01525                 Cudd_RecursiveDeref(dd,res1);
01526                 return(NULL);
01527             }
01528             cuddDeref(res1);
01529         } else {
01530             cuddRef(Gamma);
01531             resA = cuddCProjectionRecur(dd,Ran,Yrest,cuddT(Ysupp));
01532             if (resA == NULL) {
01533                 Cudd_RecursiveDeref(dd,Gamma);
01534                 return(NULL);
01535             }
01536             cuddRef(resA);
01537             res2 = cuddBddAndRecur(dd, Cudd_Not(Gamma), resA);
01538             if (res2 == NULL) {
01539                 Cudd_RecursiveDeref(dd,Gamma);
01540                 Cudd_RecursiveDeref(dd,resA);
01541                 return(NULL);
01542             }
01543             cuddRef(res2);
01544             Cudd_RecursiveDeref(dd,Gamma);
01545             Cudd_RecursiveDeref(dd,resA);
01546             res1 = cuddCProjectionRecur(dd,Ra,Yrest,cuddT(Ysupp));
01547             if (res1 == NULL) {
01548                 Cudd_RecursiveDeref(dd,res2);
01549                 return(NULL);
01550             }
01551             cuddRef(res1);
01552             res = cuddBddIteRecur(dd, Alpha, res1, res2);
01553             if (res == NULL) {
01554                 Cudd_RecursiveDeref(dd,res1);
01555                 Cudd_RecursiveDeref(dd,res2);
01556                 return(NULL);
01557             }
01558             cuddDeref(res1);
01559             cuddDeref(res2);
01560         }
01561     }
01562 
01563     cuddCacheInsert2(dd,Cudd_CProjection,R,Y,res);
01564 
01565     return(res);
01566 
01567 } /* end of cuddCProjectionRecur */
01568 
01569 
01641 DdNode *
01642 cuddBddClosestCube(
01643   DdManager *dd,
01644   DdNode *f,
01645   DdNode *g,
01646   CUDD_VALUE_TYPE bound)
01647 {
01648     DdNode *res, *F, *G, *ft, *fe, *gt, *ge, *tt, *ee;
01649     DdNode *ctt, *cee, *cte, *cet;
01650     CUDD_VALUE_TYPE minD, dtt, dee, dte, det;
01651     DdNode *one = DD_ONE(dd);
01652     DdNode *lzero = Cudd_Not(one);
01653     DdNode *azero = DD_ZERO(dd);
01654     unsigned int topf, topg, index;
01655 
01656     statLine(dd);
01657     if (bound < (f == Cudd_Not(g))) return(azero);
01658     /* Terminal cases. */
01659     if (g == lzero || f == lzero) return(azero);
01660     if (f == one && g == one) return(one);
01661 
01662     /* Check cache. */
01663     F = Cudd_Regular(f);
01664     G = Cudd_Regular(g);
01665     if (F->ref != 1 || G->ref != 1) {
01666         res = cuddCacheLookup2(dd,(DD_CTFP) Cudd_bddClosestCube, f, g);
01667         if (res != NULL) return(res);
01668     }
01669 
01670     topf = cuddI(dd,F->index);
01671     topg = cuddI(dd,G->index);
01672 
01673     /* Compute cofactors. */
01674     if (topf <= topg) {
01675         index = F->index;
01676         ft = cuddT(F);
01677         fe = cuddE(F);
01678         if (Cudd_IsComplement(f)) {
01679             ft = Cudd_Not(ft);
01680             fe = Cudd_Not(fe);
01681         }
01682     } else {
01683         index = G->index;
01684         ft = fe = f;
01685     }
01686 
01687     if (topg <= topf) {
01688         gt = cuddT(G);
01689         ge = cuddE(G);
01690         if (Cudd_IsComplement(g)) {
01691             gt = Cudd_Not(gt);
01692             ge = Cudd_Not(ge);
01693         }
01694     } else {
01695         gt = ge = g;
01696     }
01697 
01698     tt = cuddBddClosestCube(dd,ft,gt,bound);
01699     if (tt == NULL) return(NULL);
01700     cuddRef(tt);
01701     ctt = separateCube(dd,tt,&dtt);
01702     if (ctt == NULL) {
01703         Cudd_RecursiveDeref(dd, tt);
01704         return(NULL);
01705     }
01706     cuddRef(ctt);
01707     Cudd_RecursiveDeref(dd, tt);
01708     minD = dtt;
01709     bound = ddMin(bound,minD);
01710 
01711     ee = cuddBddClosestCube(dd,fe,ge,bound);
01712     if (ee == NULL) {
01713         Cudd_RecursiveDeref(dd, ctt);
01714         return(NULL);
01715     }
01716     cuddRef(ee);
01717     cee = separateCube(dd,ee,&dee);
01718     if (cee == NULL) {
01719         Cudd_RecursiveDeref(dd, ctt);
01720         Cudd_RecursiveDeref(dd, ee);
01721         return(NULL);
01722     }
01723     cuddRef(cee);
01724     Cudd_RecursiveDeref(dd, ee);
01725     minD = ddMin(dtt, dee);
01726     if (minD <= CUDD_CONST_INDEX) bound = ddMin(bound,minD-1);
01727 
01728     if (minD > 0 && topf == topg) {
01729         DdNode *te = cuddBddClosestCube(dd,ft,ge,bound-1);
01730         if (te == NULL) {
01731             Cudd_RecursiveDeref(dd, ctt);
01732             Cudd_RecursiveDeref(dd, cee);
01733             return(NULL);
01734         }
01735         cuddRef(te);
01736         cte = separateCube(dd,te,&dte);
01737         if (cte == NULL) {
01738             Cudd_RecursiveDeref(dd, ctt);
01739             Cudd_RecursiveDeref(dd, cee);
01740             Cudd_RecursiveDeref(dd, te);
01741             return(NULL);
01742         }
01743         cuddRef(cte);
01744         Cudd_RecursiveDeref(dd, te);
01745         dte += 1.0;
01746         minD = ddMin(minD, dte);
01747     } else {
01748         cte = azero;
01749         cuddRef(cte);
01750         dte = CUDD_CONST_INDEX + 1.0;
01751     }
01752     if (minD <= CUDD_CONST_INDEX) bound = ddMin(bound,minD-1);
01753 
01754     if (minD > 0 && topf == topg) {
01755         DdNode *et = cuddBddClosestCube(dd,fe,gt,bound-1);
01756         if (et == NULL) {
01757             Cudd_RecursiveDeref(dd, ctt);
01758             Cudd_RecursiveDeref(dd, cee);
01759             Cudd_RecursiveDeref(dd, cte);
01760             return(NULL);
01761         }
01762         cuddRef(et);
01763         cet = separateCube(dd,et,&det);
01764         if (cet == NULL) {
01765             Cudd_RecursiveDeref(dd, ctt);
01766             Cudd_RecursiveDeref(dd, cee);
01767             Cudd_RecursiveDeref(dd, cte);
01768             Cudd_RecursiveDeref(dd, et);
01769             return(NULL);
01770         }
01771         cuddRef(cet);
01772         Cudd_RecursiveDeref(dd, et);
01773         det += 1.0;
01774         minD = ddMin(minD, det);
01775     } else {
01776         cet = azero;
01777         cuddRef(cet);
01778         det = CUDD_CONST_INDEX + 1.0;
01779     }
01780 
01781     if (minD == dtt) {
01782         if (dtt == dee && ctt == cee) {
01783             res = createResult(dd,CUDD_CONST_INDEX,1,ctt,dtt);
01784         } else {
01785             res = createResult(dd,index,1,ctt,dtt);
01786         }
01787     } else if (minD == dee) {
01788         res = createResult(dd,index,0,cee,dee);
01789     } else if (minD == dte) {
01790 #ifdef DD_DEBUG
01791         assert(topf == topg);
01792 #endif
01793         res = createResult(dd,index,1,cte,dte);
01794     } else {
01795 #ifdef DD_DEBUG
01796         assert(topf == topg);
01797 #endif
01798         res = createResult(dd,index,0,cet,det);
01799     }
01800     if (res == NULL) {
01801         Cudd_RecursiveDeref(dd, ctt);
01802         Cudd_RecursiveDeref(dd, cee);
01803         Cudd_RecursiveDeref(dd, cte);
01804         Cudd_RecursiveDeref(dd, cet);
01805         return(NULL);
01806     }
01807     cuddRef(res);
01808     Cudd_RecursiveDeref(dd, ctt);
01809     Cudd_RecursiveDeref(dd, cee);
01810     Cudd_RecursiveDeref(dd, cte);
01811     Cudd_RecursiveDeref(dd, cet);
01812 
01813     /* Only cache results that are different from azero to avoid
01814     ** storing results that depend on the value of the bound. */
01815     if ((F->ref != 1 || G->ref != 1) && res != azero)
01816         cuddCacheInsert2(dd,(DD_CTFP) Cudd_bddClosestCube, f, g, res);
01817 
01818     cuddDeref(res);
01819     return(res);
01820 
01821 } /* end of cuddBddClosestCube */
01822 
01823 
01824 /*---------------------------------------------------------------------------*/
01825 /* Definition of static functions                                            */
01826 /*---------------------------------------------------------------------------*/
01827 
01828 
01853 static int
01854 cuddMinHammingDistRecur(
01855   DdNode * f,
01856   int *minterm,
01857   DdHashTable * table,
01858   int upperBound)
01859 {
01860     DdNode      *F, *Ft, *Fe;
01861     double      h, hT, hE;
01862     DdNode      *zero, *res;
01863     DdManager   *dd = table->manager;
01864 
01865     statLine(dd);
01866     if (upperBound == 0) return(0);
01867 
01868     F = Cudd_Regular(f);
01869 
01870     if (cuddIsConstant(F)) {
01871         zero = Cudd_Not(DD_ONE(dd));
01872         if (f == dd->background || f == zero) {
01873             return(upperBound);
01874         } else {
01875             return(0);
01876         }
01877     }
01878     if ((res = cuddHashTableLookup1(table,f)) != NULL) {
01879         h = cuddV(res);
01880         if (res->ref == 0) {
01881             dd->dead++;
01882             dd->constants.dead++;
01883         }
01884         return((int) h);
01885     }
01886 
01887     Ft = cuddT(F); Fe = cuddE(F);
01888     if (Cudd_IsComplement(f)) {
01889         Ft = Cudd_Not(Ft); Fe = Cudd_Not(Fe);
01890     }
01891     if (minterm[F->index] == 0) {
01892         DdNode *temp = Ft;
01893         Ft = Fe; Fe = temp;
01894     }
01895 
01896     hT = cuddMinHammingDistRecur(Ft,minterm,table,upperBound);
01897     if (hT == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
01898     if (hT == 0) {
01899         hE = upperBound;
01900     } else {
01901         hE = cuddMinHammingDistRecur(Fe,minterm,table,upperBound - 1);
01902         if (hE == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
01903     }
01904     h = ddMin(hT, hE + 1);
01905 
01906     if (F->ref != 1) {
01907         ptrint fanout = (ptrint) F->ref;
01908         cuddSatDec(fanout);
01909         res = cuddUniqueConst(dd, (CUDD_VALUE_TYPE) h);
01910         if (!cuddHashTableInsert1(table,f,res,fanout)) {
01911             cuddRef(res); Cudd_RecursiveDeref(dd, res);
01912             return(CUDD_OUT_OF_MEM);
01913         }
01914     }
01915 
01916     return((int) h);
01917 
01918 } /* end of cuddMinHammingDistRecur */
01919 
01920 
01933 static DdNode *
01934 separateCube(
01935   DdManager *dd,
01936   DdNode *f,
01937   CUDD_VALUE_TYPE *distance)
01938 {
01939     DdNode *cube, *t;
01940 
01941     /* One and zero are special cases because the distance is implied. */
01942     if (Cudd_IsConstant(f)) {
01943         *distance = (f == DD_ONE(dd)) ? 0.0 :
01944             (1.0 + (CUDD_VALUE_TYPE) CUDD_CONST_INDEX);
01945         return(f);
01946     }
01947 
01948     /* Find out which branch points to the distance and replace the top
01949     ** node with one pointing to zero instead. */
01950     t = cuddT(f);
01951     if (Cudd_IsConstant(t) && cuddV(t) <= 0) {
01952 #ifdef DD_DEBUG
01953         assert(!Cudd_IsConstant(cuddE(f)) || cuddE(f) == DD_ONE(dd));
01954 #endif
01955         *distance = -cuddV(t);
01956         cube = cuddUniqueInter(dd, f->index, DD_ZERO(dd), cuddE(f));
01957     } else {
01958 #ifdef DD_DEBUG
01959         assert(!Cudd_IsConstant(t) || t == DD_ONE(dd));
01960 #endif
01961         *distance = -cuddV(cuddE(f));
01962         cube = cuddUniqueInter(dd, f->index, t, DD_ZERO(dd));
01963     }
01964 
01965     return(cube);
01966 
01967 } /* end of separateCube */
01968 
01969 
01982 static DdNode *
01983 createResult(
01984   DdManager *dd,
01985   unsigned int index,
01986   unsigned int phase,
01987   DdNode *cube,
01988   CUDD_VALUE_TYPE distance)
01989 {
01990     DdNode *res, *constant;
01991 
01992     /* Special case.  The cube is either one or zero, and we do not
01993     ** add any variables.  Hence, the result is also one or zero,
01994     ** and the distance remains implied by the value of the constant. */
01995     if (index == CUDD_CONST_INDEX && Cudd_IsConstant(cube)) return(cube);
01996 
01997     constant = cuddUniqueConst(dd,-distance);
01998     if (constant == NULL) return(NULL);
01999     cuddRef(constant);
02000 
02001     if (index == CUDD_CONST_INDEX) {
02002         /* Replace the top node. */
02003         if (cuddT(cube) == DD_ZERO(dd)) {
02004             res = cuddUniqueInter(dd,cube->index,constant,cuddE(cube));
02005         } else {
02006             res = cuddUniqueInter(dd,cube->index,cuddT(cube),constant);
02007         }
02008     } else {
02009         /* Add a new top node. */
02010 #ifdef DD_DEBUG
02011         assert(cuddI(dd,index) < cuddI(dd,cube->index));
02012 #endif
02013         if (phase) {
02014             res = cuddUniqueInter(dd,index,cube,constant);
02015         } else {
02016             res = cuddUniqueInter(dd,index,constant,cube);
02017         }
02018     }
02019     if (res == NULL) {
02020         Cudd_RecursiveDeref(dd, constant);
02021         return(NULL);
02022     }
02023     cuddDeref(constant); /* safe because constant is part of res */
02024 
02025     return(res);
02026 
02027 } /* end of createResult */