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

00001 
00046 #include "util_hack.h"
00047 #include "cuddInt.h"
00048 
00049 
00050 /*---------------------------------------------------------------------------*/
00051 /* Constant declarations                                                     */
00052 /*---------------------------------------------------------------------------*/
00053 
00054 
00055 /*---------------------------------------------------------------------------*/
00056 /* Stucture declarations                                                     */
00057 /*---------------------------------------------------------------------------*/
00058 
00059 
00060 /*---------------------------------------------------------------------------*/
00061 /* Type declarations                                                         */
00062 /*---------------------------------------------------------------------------*/
00063 
00064 
00065 /*---------------------------------------------------------------------------*/
00066 /* Variable declarations                                                     */
00067 /*---------------------------------------------------------------------------*/
00068 
00069 #ifndef lint
00070 static char rcsid[] DD_UNUSED = "$Id: cuddPriority.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $";
00071 #endif
00072 
00073 /*---------------------------------------------------------------------------*/
00074 /* Macro declarations                                                        */
00075 /*---------------------------------------------------------------------------*/
00076 
00077 
00080 /*---------------------------------------------------------------------------*/
00081 /* Static function prototypes                                                */
00082 /*---------------------------------------------------------------------------*/
00083 static int cuddMinHammingDistRecur ARGS((DdNode * f, int *minterm, DdHashTable * table, int upperBound));
00084 static DdNode * separateCube ARGS((DdManager *dd, DdNode *f, CUDD_VALUE_TYPE *distance));
00085 static DdNode * createResult ARGS((DdManager *dd, unsigned int index, unsigned int phase, DdNode *cube, CUDD_VALUE_TYPE distance));
00086 
00090 /*---------------------------------------------------------------------------*/
00091 /* Definition of exported functions                                          */
00092 /*---------------------------------------------------------------------------*/
00093 
00094 
00139 DdNode *
00140 Cudd_PrioritySelect(
00141   DdManager * dd /* manager */,
00142   DdNode * R /* BDD of the relation */,
00143   DdNode ** x /* array of x variables */,
00144   DdNode ** y /* array of y variables */,
00145   DdNode ** z /* array of z variables (optional: may be NULL) */,
00146   DdNode * Pi /* BDD of the priority function (optional: may be NULL) */,
00147   int  n /* size of x, y, and z */,
00148   DdNode * (*Pifunc)(DdManager *, int, DdNode **, DdNode **, DdNode **) /* function used to build Pi if it is NULL */)
00149 {
00150     DdNode *res = NULL;
00151     DdNode *zcube = NULL;
00152     DdNode *Rxz, *Q;
00153     int createdZ = 0;
00154     int createdPi = 0;
00155     int i;
00156 
00157     /* Create z variables if needed. */
00158     if (z == NULL) {
00159         if (Pi != NULL) return(NULL);
00160         z = ALLOC(DdNode *,n);
00161         if (z == NULL) {
00162             dd->errorCode = CUDD_MEMORY_OUT;
00163             return(NULL);
00164         }
00165         createdZ = 1;
00166         for (i = 0; i < n; i++) {
00167             if (dd->size >= (int) CUDD_MAXINDEX - 1) goto endgame;
00168             z[i] = cuddUniqueInter(dd,dd->size,dd->one,Cudd_Not(dd->one));
00169             if (z[i] == NULL) goto endgame;
00170         }
00171     }
00172 
00173     /* Create priority function BDD if needed. */
00174     if (Pi == NULL) {
00175         Pi = Pifunc(dd,n,x,y,z);
00176         if (Pi == NULL) goto endgame;
00177         createdPi = 1;
00178         cuddRef(Pi);
00179     }
00180 
00181     /* Initialize abstraction cube. */
00182     zcube = DD_ONE(dd);
00183     cuddRef(zcube);
00184     for (i = n - 1; i >= 0; i--) {
00185         DdNode *tmpp;
00186         tmpp = Cudd_bddAnd(dd,z[i],zcube);
00187         if (tmpp == NULL) goto endgame;
00188         cuddRef(tmpp);
00189         Cudd_RecursiveDeref(dd,zcube);
00190         zcube = tmpp;
00191     }
00192 
00193     /* Compute subset of (x,y) pairs. */
00194     Rxz = Cudd_bddSwapVariables(dd,R,y,z,n);
00195     if (Rxz == NULL) goto endgame;
00196     cuddRef(Rxz);
00197     Q = Cudd_bddAndAbstract(dd,Rxz,Pi,zcube);
00198     if (Q == NULL) {
00199         Cudd_RecursiveDeref(dd,Rxz);
00200         goto endgame;
00201     }
00202     cuddRef(Q);
00203     Cudd_RecursiveDeref(dd,Rxz);
00204     res = Cudd_bddAnd(dd,R,Cudd_Not(Q));
00205     if (res == NULL) {
00206         Cudd_RecursiveDeref(dd,Q);
00207         goto endgame;
00208     }
00209     cuddRef(res);
00210     Cudd_RecursiveDeref(dd,Q);
00211 
00212 endgame:
00213     if (zcube != NULL) Cudd_RecursiveDeref(dd,zcube);
00214     if (createdZ) {
00215         FREE(z);
00216     }
00217     if (createdPi) {
00218         Cudd_RecursiveDeref(dd,Pi);
00219     }
00220     if (res != NULL) cuddDeref(res);
00221     return(res);
00222 
00223 } /* Cudd_PrioritySelect */
00224 
00225 
00244 DdNode *
00245 Cudd_Xgty(
00246   DdManager * dd /* DD manager */,
00247   int  N /* number of x and y variables */,
00248   DdNode ** z /* array of z variables: unused */,
00249   DdNode ** x /* array of x variables */,
00250   DdNode ** y /* array of y variables */)
00251 {
00252     DdNode *u, *v, *w;
00253     int     i;
00254 
00255     /* Build bottom part of BDD outside loop. */
00256     u = Cudd_bddAnd(dd, x[N-1], Cudd_Not(y[N-1]));
00257     if (u == NULL) return(NULL);
00258     cuddRef(u);
00259 
00260     /* Loop to build the rest of the BDD. */
00261     for (i = N-2; i >= 0; i--) {
00262         v = Cudd_bddAnd(dd, y[i], Cudd_Not(u));
00263         if (v == NULL) {
00264             Cudd_RecursiveDeref(dd, u);
00265             return(NULL);
00266         }
00267         cuddRef(v);
00268         w = Cudd_bddAnd(dd, Cudd_Not(y[i]), u);
00269         if (w == NULL) {
00270             Cudd_RecursiveDeref(dd, u);
00271             Cudd_RecursiveDeref(dd, v);
00272             return(NULL);
00273         }
00274         cuddRef(w);
00275         Cudd_RecursiveDeref(dd, u);
00276         u = Cudd_bddIte(dd, x[i], Cudd_Not(v), w);
00277         if (u == NULL) {
00278             Cudd_RecursiveDeref(dd, v);
00279             Cudd_RecursiveDeref(dd, w);
00280             return(NULL);
00281         }
00282         cuddRef(u);
00283         Cudd_RecursiveDeref(dd, v);
00284         Cudd_RecursiveDeref(dd, w);
00285 
00286     }
00287     cuddDeref(u);
00288     return(u);
00289 
00290 } /* end of Cudd_Xgty */
00291 
00292 
00309 DdNode *
00310 Cudd_Xeqy(
00311   DdManager * dd /* DD manager */,
00312   int  N /* number of x and y variables */,
00313   DdNode ** x /* array of x variables */,
00314   DdNode ** y /* array of y variables */)
00315 {
00316     DdNode *u, *v, *w;
00317     int     i;
00318 
00319     /* Build bottom part of BDD outside loop. */
00320     u = Cudd_bddIte(dd, x[N-1], y[N-1], Cudd_Not(y[N-1]));
00321     if (u == NULL) return(NULL);
00322     cuddRef(u);
00323 
00324     /* Loop to build the rest of the BDD. */
00325     for (i = N-2; i >= 0; i--) {
00326         v = Cudd_bddAnd(dd, y[i], u);
00327         if (v == NULL) {
00328             Cudd_RecursiveDeref(dd, u);
00329             return(NULL);
00330         }
00331         cuddRef(v);
00332         w = Cudd_bddAnd(dd, Cudd_Not(y[i]), u);
00333         if (w == NULL) {
00334             Cudd_RecursiveDeref(dd, u);
00335             Cudd_RecursiveDeref(dd, v);
00336             return(NULL);
00337         }
00338         cuddRef(w);
00339         Cudd_RecursiveDeref(dd, u);
00340         u = Cudd_bddIte(dd, x[i], v, w);
00341         if (u == NULL) {
00342             Cudd_RecursiveDeref(dd, v);
00343             Cudd_RecursiveDeref(dd, w);
00344             return(NULL);
00345         }
00346         cuddRef(u);
00347         Cudd_RecursiveDeref(dd, v);
00348         Cudd_RecursiveDeref(dd, w);
00349     }
00350     cuddDeref(u);
00351     return(u);
00352 
00353 } /* end of Cudd_Xeqy */
00354 
00355 
00372 DdNode *
00373 Cudd_addXeqy(
00374   DdManager * dd /* DD manager */,
00375   int  N /* number of x and y variables */,
00376   DdNode ** x /* array of x variables */,
00377   DdNode ** y /* array of y variables */)
00378 {
00379     DdNode *one, *zero;
00380     DdNode *u, *v, *w;
00381     int     i;
00382 
00383     one = DD_ONE(dd);
00384     zero = DD_ZERO(dd);
00385 
00386     /* Build bottom part of ADD outside loop. */
00387     v = Cudd_addIte(dd, y[N-1], one, zero);
00388     if (v == NULL) return(NULL);
00389     cuddRef(v);
00390     w = Cudd_addIte(dd, y[N-1], zero, one);
00391     if (w == NULL) {
00392         Cudd_RecursiveDeref(dd, v);
00393         return(NULL);
00394     }
00395     cuddRef(w);
00396     u = Cudd_addIte(dd, x[N-1], v, w);
00397     if (w == NULL) {
00398         Cudd_RecursiveDeref(dd, v);
00399         Cudd_RecursiveDeref(dd, w);
00400         return(NULL);
00401     }
00402     cuddRef(u);
00403     Cudd_RecursiveDeref(dd, v);
00404     Cudd_RecursiveDeref(dd, w);
00405 
00406     /* Loop to build the rest of the ADD. */
00407     for (i = N-2; i >= 0; i--) {
00408         v = Cudd_addIte(dd, y[i], u, zero);
00409         if (v == NULL) {
00410             Cudd_RecursiveDeref(dd, u);
00411             return(NULL);
00412         }
00413         cuddRef(v);
00414         w = Cudd_addIte(dd, y[i], zero, u);
00415         if (w == NULL) {
00416             Cudd_RecursiveDeref(dd, u);
00417             Cudd_RecursiveDeref(dd, v);
00418             return(NULL);
00419         }
00420         cuddRef(w);
00421         Cudd_RecursiveDeref(dd, u);
00422         u = Cudd_addIte(dd, x[i], v, w);
00423         if (w == NULL) {
00424             Cudd_RecursiveDeref(dd, v);
00425             Cudd_RecursiveDeref(dd, w);
00426             return(NULL);
00427         }
00428         cuddRef(u);
00429         Cudd_RecursiveDeref(dd, v);
00430         Cudd_RecursiveDeref(dd, w);
00431     }
00432     cuddDeref(u);
00433     return(u);
00434 
00435 } /* end of Cudd_addXeqy */
00436 
00437 
00458 DdNode *
00459 Cudd_Dxygtdxz(
00460   DdManager * dd /* DD manager */,
00461   int  N /* number of x, y, and z variables */,
00462   DdNode ** x /* array of x variables */,
00463   DdNode ** y /* array of y variables */,
00464   DdNode ** z /* array of z variables */)
00465 {
00466     DdNode *one, *zero;
00467     DdNode *z1, *z2, *z3, *z4, *y1_, *y2, *x1;
00468     int     i;
00469 
00470     one = DD_ONE(dd);
00471     zero = Cudd_Not(one);
00472 
00473     /* Build bottom part of BDD outside loop. */
00474     y1_ = Cudd_bddIte(dd, y[N-1], one, Cudd_Not(z[N-1]));
00475     if (y1_ == NULL) return(NULL);
00476     cuddRef(y1_);
00477     y2 = Cudd_bddIte(dd, y[N-1], z[N-1], one);
00478     if (y2 == NULL) {
00479         Cudd_RecursiveDeref(dd, y1_);
00480         return(NULL);
00481     }
00482     cuddRef(y2);
00483     x1 = Cudd_bddIte(dd, x[N-1], y1_, y2);
00484     if (x1 == NULL) {
00485         Cudd_RecursiveDeref(dd, y1_);
00486         Cudd_RecursiveDeref(dd, y2);
00487         return(NULL);
00488     }
00489     cuddRef(x1);
00490     Cudd_RecursiveDeref(dd, y1_);
00491     Cudd_RecursiveDeref(dd, y2);
00492 
00493     /* Loop to build the rest of the BDD. */
00494     for (i = N-2; i >= 0; i--) {
00495         z1 = Cudd_bddIte(dd, z[i], one, Cudd_Not(x1));
00496         if (z1 == NULL) {
00497             Cudd_RecursiveDeref(dd, x1);
00498             return(NULL);
00499         }
00500         cuddRef(z1);
00501         z2 = Cudd_bddIte(dd, z[i], x1, one);
00502         if (z2 == NULL) {
00503             Cudd_RecursiveDeref(dd, x1);
00504             Cudd_RecursiveDeref(dd, z1);
00505             return(NULL);
00506         }
00507         cuddRef(z2);
00508         z3 = Cudd_bddIte(dd, z[i], one, x1);
00509         if (z3 == NULL) {
00510             Cudd_RecursiveDeref(dd, x1);
00511             Cudd_RecursiveDeref(dd, z1);
00512             Cudd_RecursiveDeref(dd, z2);
00513             return(NULL);
00514         }
00515         cuddRef(z3);
00516         z4 = Cudd_bddIte(dd, z[i], x1, zero);
00517         if (z4 == NULL) {
00518             Cudd_RecursiveDeref(dd, x1);
00519             Cudd_RecursiveDeref(dd, z1);
00520             Cudd_RecursiveDeref(dd, z2);
00521             Cudd_RecursiveDeref(dd, z3);
00522             return(NULL);
00523         }
00524         cuddRef(z4);
00525         Cudd_RecursiveDeref(dd, x1);
00526         y1_ = Cudd_bddIte(dd, y[i], z2, Cudd_Not(z1));
00527         if (y1_ == NULL) {
00528             Cudd_RecursiveDeref(dd, z1);
00529             Cudd_RecursiveDeref(dd, z2);
00530             Cudd_RecursiveDeref(dd, z3);
00531             Cudd_RecursiveDeref(dd, z4);
00532             return(NULL);
00533         }
00534         cuddRef(y1_);
00535         y2 = Cudd_bddIte(dd, y[i], z4, z3);
00536         if (y2 == NULL) {
00537             Cudd_RecursiveDeref(dd, z1);
00538             Cudd_RecursiveDeref(dd, z2);
00539             Cudd_RecursiveDeref(dd, z3);
00540             Cudd_RecursiveDeref(dd, z4);
00541             Cudd_RecursiveDeref(dd, y1_);
00542             return(NULL);
00543         }
00544         cuddRef(y2);
00545         Cudd_RecursiveDeref(dd, z1);
00546         Cudd_RecursiveDeref(dd, z2);
00547         Cudd_RecursiveDeref(dd, z3);
00548         Cudd_RecursiveDeref(dd, z4);
00549         x1 = Cudd_bddIte(dd, x[i], y1_, y2);
00550         if (x1 == NULL) {
00551             Cudd_RecursiveDeref(dd, y1_);
00552             Cudd_RecursiveDeref(dd, y2);
00553             return(NULL);
00554         }
00555         cuddRef(x1);
00556         Cudd_RecursiveDeref(dd, y1_);
00557         Cudd_RecursiveDeref(dd, y2);
00558     }
00559     cuddDeref(x1);
00560     return(Cudd_Not(x1));
00561 
00562 } /* end of Cudd_Dxygtdxz */
00563 
00564 
00585 DdNode *
00586 Cudd_Dxygtdyz(
00587   DdManager * dd /* DD manager */,
00588   int  N /* number of x, y, and z variables */,
00589   DdNode ** x /* array of x variables */,
00590   DdNode ** y /* array of y variables */,
00591   DdNode ** z /* array of z variables */)
00592 {
00593     DdNode *one, *zero;
00594     DdNode *z1, *z2, *z3, *z4, *y1_, *y2, *x1;
00595     int     i;
00596 
00597     one = DD_ONE(dd);
00598     zero = Cudd_Not(one);
00599 
00600     /* Build bottom part of BDD outside loop. */
00601     y1_ = Cudd_bddIte(dd, y[N-1], one, z[N-1]);
00602     if (y1_ == NULL) return(NULL);
00603     cuddRef(y1_);
00604     y2 = Cudd_bddIte(dd, y[N-1], z[N-1], zero);
00605     if (y2 == NULL) {
00606         Cudd_RecursiveDeref(dd, y1_);
00607         return(NULL);
00608     }
00609     cuddRef(y2);
00610     x1 = Cudd_bddIte(dd, x[N-1], y1_, Cudd_Not(y2));
00611     if (x1 == NULL) {
00612         Cudd_RecursiveDeref(dd, y1_);
00613         Cudd_RecursiveDeref(dd, y2);
00614         return(NULL);
00615     }
00616     cuddRef(x1);
00617     Cudd_RecursiveDeref(dd, y1_);
00618     Cudd_RecursiveDeref(dd, y2);
00619 
00620     /* Loop to build the rest of the BDD. */
00621     for (i = N-2; i >= 0; i--) {
00622         z1 = Cudd_bddIte(dd, z[i], x1, zero);
00623         if (z1 == NULL) {
00624             Cudd_RecursiveDeref(dd, x1);
00625             return(NULL);
00626         }
00627         cuddRef(z1);
00628         z2 = Cudd_bddIte(dd, z[i], x1, one);
00629         if (z2 == NULL) {
00630             Cudd_RecursiveDeref(dd, x1);
00631             Cudd_RecursiveDeref(dd, z1);
00632             return(NULL);
00633         }
00634         cuddRef(z2);
00635         z3 = Cudd_bddIte(dd, z[i], one, x1);
00636         if (z3 == NULL) {
00637             Cudd_RecursiveDeref(dd, x1);
00638             Cudd_RecursiveDeref(dd, z1);
00639             Cudd_RecursiveDeref(dd, z2);
00640             return(NULL);
00641         }
00642         cuddRef(z3);
00643         z4 = Cudd_bddIte(dd, z[i], one, Cudd_Not(x1));
00644         if (z4 == NULL) {
00645             Cudd_RecursiveDeref(dd, x1);
00646             Cudd_RecursiveDeref(dd, z1);
00647             Cudd_RecursiveDeref(dd, z2);
00648             Cudd_RecursiveDeref(dd, z3);
00649             return(NULL);
00650         }
00651         cuddRef(z4);
00652         Cudd_RecursiveDeref(dd, x1);
00653         y1_ = Cudd_bddIte(dd, y[i], z2, z1);
00654         if (y1_ == NULL) {
00655             Cudd_RecursiveDeref(dd, z1);
00656             Cudd_RecursiveDeref(dd, z2);
00657             Cudd_RecursiveDeref(dd, z3);
00658             Cudd_RecursiveDeref(dd, z4);
00659             return(NULL);
00660         }
00661         cuddRef(y1_);
00662         y2 = Cudd_bddIte(dd, y[i], z4, Cudd_Not(z3));
00663         if (y2 == NULL) {
00664             Cudd_RecursiveDeref(dd, z1);
00665             Cudd_RecursiveDeref(dd, z2);
00666             Cudd_RecursiveDeref(dd, z3);
00667             Cudd_RecursiveDeref(dd, z4);
00668             Cudd_RecursiveDeref(dd, y1_);
00669             return(NULL);
00670         }
00671         cuddRef(y2);
00672         Cudd_RecursiveDeref(dd, z1);
00673         Cudd_RecursiveDeref(dd, z2);
00674         Cudd_RecursiveDeref(dd, z3);
00675         Cudd_RecursiveDeref(dd, z4);
00676         x1 = Cudd_bddIte(dd, x[i], y1_, Cudd_Not(y2));
00677         if (x1 == NULL) {
00678             Cudd_RecursiveDeref(dd, y1_);
00679             Cudd_RecursiveDeref(dd, y2);
00680             return(NULL);
00681         }
00682         cuddRef(x1);
00683         Cudd_RecursiveDeref(dd, y1_);
00684         Cudd_RecursiveDeref(dd, y2);
00685     }
00686     cuddDeref(x1);
00687     return(Cudd_Not(x1));
00688 
00689 } /* end of Cudd_Dxygtdyz */
00690 
00691 
00706 DdNode *
00707 Cudd_CProjection(
00708   DdManager * dd,
00709   DdNode * R,
00710   DdNode * Y)
00711 {
00712     DdNode *res;
00713     DdNode *support;
00714 
00715     if (cuddCheckCube(dd,Y) == 0) {
00716         (void) fprintf(dd->err,
00717         "Error: The third argument of Cudd_CProjection should be a cube\n");
00718         dd->errorCode = CUDD_INVALID_ARG;
00719         return(NULL);
00720     }
00721 
00722     /* Compute the support of Y, which is used by the abstraction step
00723     ** in cuddCProjectionRecur.
00724     */
00725     support = Cudd_Support(dd,Y);
00726     if (support == NULL) return(NULL);
00727     cuddRef(support);
00728 
00729     do {
00730         dd->reordered = 0;
00731         res = cuddCProjectionRecur(dd,R,Y,support);
00732     } while (dd->reordered == 1);
00733 
00734     if (res == NULL) {
00735         Cudd_RecursiveDeref(dd,support);
00736         return(NULL);
00737     }
00738     cuddRef(res);
00739     Cudd_RecursiveDeref(dd,support);
00740     cuddDeref(res);
00741 
00742     return(res);
00743 
00744 } /* end of Cudd_CProjection */
00745 
00746 
00761 DdNode *
00762 Cudd_addHamming(
00763   DdManager * dd,
00764   DdNode ** xVars,
00765   DdNode ** yVars,
00766   int  nVars)
00767 {
00768     DdNode  *result,*tempBdd;
00769     DdNode  *tempAdd,*temp;
00770     int     i;
00771 
00772     result = DD_ZERO(dd);
00773     cuddRef(result);
00774 
00775     for (i = 0; i < nVars; i++) {
00776         tempBdd = Cudd_bddIte(dd,xVars[i],Cudd_Not(yVars[i]),yVars[i]);
00777         if (tempBdd == NULL) {
00778             Cudd_RecursiveDeref(dd,result);
00779             return(NULL);
00780         }
00781         cuddRef(tempBdd);
00782         tempAdd = Cudd_BddToAdd(dd,tempBdd);
00783         if (tempAdd == NULL) {
00784             Cudd_RecursiveDeref(dd,tempBdd);
00785             Cudd_RecursiveDeref(dd,result);
00786             return(NULL);
00787         }
00788         cuddRef(tempAdd);
00789         Cudd_RecursiveDeref(dd,tempBdd);
00790         temp = Cudd_addApply(dd,Cudd_addPlus,tempAdd,result);
00791         if (temp == NULL) {
00792             Cudd_RecursiveDeref(dd,tempAdd);
00793             Cudd_RecursiveDeref(dd,result);
00794             return(NULL);
00795         }
00796         cuddRef(temp);
00797         Cudd_RecursiveDeref(dd,tempAdd);
00798         Cudd_RecursiveDeref(dd,result);
00799         result = temp;
00800     }
00801 
00802     cuddDeref(result);
00803     return(result);
00804 
00805 } /* end of Cudd_addHamming */
00806 
00807 
00824 int
00825 Cudd_MinHammingDist(
00826   DdManager *dd /* DD manager */,
00827   DdNode *f /* function to examine */,
00828   int *minterm /* reference minterm */,
00829   int upperBound /* distance above which an approximate answer is OK */)
00830 {
00831     DdHashTable *table;
00832     CUDD_VALUE_TYPE epsilon;
00833     int res;
00834 
00835     table = cuddHashTableInit(dd,1,2);
00836     if (table == NULL) {
00837         return(CUDD_OUT_OF_MEM);
00838     }
00839     epsilon = Cudd_ReadEpsilon(dd);
00840     Cudd_SetEpsilon(dd,(CUDD_VALUE_TYPE)0.0);
00841     res = cuddMinHammingDistRecur(f,minterm,table,upperBound);
00842     cuddHashTableQuit(table);
00843     Cudd_SetEpsilon(dd,epsilon);
00844 
00845     return(res);
00846     
00847 } /* end of Cudd_MinHammingDist */
00848 
00849 
00865 DdNode *
00866 Cudd_bddClosestCube(
00867   DdManager *dd,
00868   DdNode * f,
00869   DdNode *g,
00870   int *distance)
00871 {
00872     DdNode *res, *acube;
00873     CUDD_VALUE_TYPE rdist;
00874 
00875     /* Compute the cube and distance as a single ADD. */
00876     do {
00877         dd->reordered = 0;
00878         res = cuddBddClosestCube(dd,f,g,CUDD_CONST_INDEX + 1.0);
00879     } while (dd->reordered == 1);
00880     if (res == NULL) return(NULL);
00881     cuddRef(res);
00882 
00883     /* Unpack distance and cube. */
00884     do {
00885         dd->reordered = 0;
00886         acube = separateCube(dd, res, &rdist);
00887     } while (dd->reordered == 1);
00888     if (acube == NULL) {
00889         Cudd_RecursiveDeref(dd, res);
00890         return(NULL);
00891     }
00892     cuddRef(acube);
00893     Cudd_RecursiveDeref(dd, res);
00894 
00895     /* Convert cube from ADD to BDD. */
00896     do {
00897         dd->reordered = 0;
00898         res = cuddAddBddDoPattern(dd, acube);
00899     } while (dd->reordered == 1);
00900     if (res == NULL) {
00901         Cudd_RecursiveDeref(dd, acube);
00902         return(NULL);
00903     }
00904     cuddRef(res);
00905     Cudd_RecursiveDeref(dd, acube);
00906 
00907     *distance = (int) rdist;
00908     cuddDeref(res);
00909     return(res);
00910 
00911 } /* end of Cudd_bddClosestCube */
00912 
00913 
00914 /*---------------------------------------------------------------------------*/
00915 /* Definition of internal functions                                          */
00916 /*---------------------------------------------------------------------------*/
00917 
00918 
00931 DdNode *
00932 cuddCProjectionRecur(
00933   DdManager * dd,
00934   DdNode * R,
00935   DdNode * Y,
00936   DdNode * Ysupp)
00937 {
00938     DdNode *res, *res1, *res2, *resA;
00939     DdNode *r, *y, *RT, *RE, *YT, *YE, *Yrest, *Ra, *Ran, *Gamma, *Alpha;
00940     unsigned int topR, topY, top, index;
00941     DdNode *one = DD_ONE(dd);
00942 
00943     statLine(dd);
00944     if (Y == one) return(R);
00945 
00946 #ifdef DD_DEBUG
00947     assert(!Cudd_IsConstant(Y));
00948 #endif
00949 
00950     if (R == Cudd_Not(one)) return(R);
00951 
00952     res = cuddCacheLookup2(dd, Cudd_CProjection, R, Y);
00953     if (res != NULL) return(res);
00954 
00955     r = Cudd_Regular(R);
00956     topR = cuddI(dd,r->index);
00957     y = Cudd_Regular(Y);
00958     topY = cuddI(dd,y->index);
00959 
00960     top = ddMin(topR, topY);
00961 
00962     /* Compute the cofactors of R */
00963     if (topR == top) {
00964         index = r->index;
00965         RT = cuddT(r);
00966         RE = cuddE(r);
00967         if (r != R) {
00968             RT = Cudd_Not(RT); RE = Cudd_Not(RE);
00969         }
00970     } else {
00971         RT = RE = R;
00972     }
00973 
00974     if (topY > top) {
00975         /* Y does not depend on the current top variable.
00976         ** We just need to compute the results on the two cofactors of R
00977         ** and make them the children of a node labeled r->index.
00978         */
00979         res1 = cuddCProjectionRecur(dd,RT,Y,Ysupp);
00980         if (res1 == NULL) return(NULL);
00981         cuddRef(res1);
00982         res2 = cuddCProjectionRecur(dd,RE,Y,Ysupp);
00983         if (res2 == NULL) {
00984             Cudd_RecursiveDeref(dd,res1);
00985             return(NULL);
00986         }
00987         cuddRef(res2);
00988         res = cuddBddIteRecur(dd, dd->vars[index], res1, res2);
00989         if (res == NULL) {
00990             Cudd_RecursiveDeref(dd,res1);
00991             Cudd_RecursiveDeref(dd,res2);
00992             return(NULL);
00993         }
00994         /* If we have reached this point, res1 and res2 are now
00995         ** incorporated in res. cuddDeref is therefore sufficient.
00996         */
00997         cuddDeref(res1);
00998         cuddDeref(res2);
00999     } else {
01000         /* Compute the cofactors of Y */
01001         index = y->index;
01002         YT = cuddT(y);
01003         YE = cuddE(y);
01004         if (y != Y) {
01005             YT = Cudd_Not(YT); YE = Cudd_Not(YE);
01006         }
01007         if (YT == Cudd_Not(one)) {
01008             Alpha  = Cudd_Not(dd->vars[index]);
01009             Yrest = YE;
01010             Ra = RE;
01011             Ran = RT;
01012         } else {
01013             Alpha = dd->vars[index];
01014             Yrest = YT;
01015             Ra = RT;
01016             Ran = RE;
01017         }
01018         Gamma = cuddBddExistAbstractRecur(dd,Ra,cuddT(Ysupp));
01019         if (Gamma == NULL) return(NULL);
01020         if (Gamma == one) {
01021             res1 = cuddCProjectionRecur(dd,Ra,Yrest,cuddT(Ysupp));
01022             if (res1 == NULL) return(NULL);
01023             cuddRef(res1);
01024             res = cuddBddAndRecur(dd, Alpha, res1);
01025             if (res == NULL) {
01026                 Cudd_RecursiveDeref(dd,res1);
01027                 return(NULL);
01028             }
01029             cuddDeref(res1);
01030         } else if (Gamma == Cudd_Not(one)) {
01031             res1 = cuddCProjectionRecur(dd,Ran,Yrest,cuddT(Ysupp));
01032             if (res1 == NULL) return(NULL);
01033             cuddRef(res1);
01034             res = cuddBddAndRecur(dd, Cudd_Not(Alpha), res1);
01035             if (res == NULL) {
01036                 Cudd_RecursiveDeref(dd,res1);
01037                 return(NULL);
01038             }
01039             cuddDeref(res1);
01040         } else {
01041             cuddRef(Gamma);
01042             resA = cuddCProjectionRecur(dd,Ran,Yrest,cuddT(Ysupp));
01043             if (resA == NULL) {
01044                 Cudd_RecursiveDeref(dd,Gamma);
01045                 return(NULL);
01046             }
01047             cuddRef(resA);
01048             res2 = cuddBddAndRecur(dd, Cudd_Not(Gamma), resA);
01049             if (res2 == NULL) {
01050                 Cudd_RecursiveDeref(dd,Gamma);
01051                 Cudd_RecursiveDeref(dd,resA);
01052                 return(NULL);
01053             }
01054             cuddRef(res2);
01055             Cudd_RecursiveDeref(dd,Gamma);
01056             Cudd_RecursiveDeref(dd,resA);
01057             res1 = cuddCProjectionRecur(dd,Ra,Yrest,cuddT(Ysupp));
01058             if (res1 == NULL) {
01059                 Cudd_RecursiveDeref(dd,res2);
01060                 return(NULL);
01061             }
01062             cuddRef(res1);
01063             res = cuddBddIteRecur(dd, Alpha, res1, res2);
01064             if (res == NULL) {
01065                 Cudd_RecursiveDeref(dd,res1);
01066                 Cudd_RecursiveDeref(dd,res2);
01067                 return(NULL);
01068             }
01069             cuddDeref(res1);
01070             cuddDeref(res2);
01071         }
01072     }
01073 
01074     cuddCacheInsert2(dd,Cudd_CProjection,R,Y,res);
01075 
01076     return(res);
01077 
01078 } /* end of cuddCProjectionRecur */
01079 
01080 
01102 DdNode *
01103 cuddBddClosestCube(
01104   DdManager *dd,
01105   DdNode *f,
01106   DdNode *g,
01107   CUDD_VALUE_TYPE bound)
01108 {
01109     DdNode *res, *F, *G, *ft, *fe, *gt, *ge, *tt, *ee;
01110     DdNode *ctt, *cee, *cte, *cet;
01111     CUDD_VALUE_TYPE minD, dtt, dee, dte, det;
01112     DdNode *one = DD_ONE(dd);
01113     DdNode *lzero = Cudd_Not(one);
01114     DdNode *azero = DD_ZERO(dd);
01115     unsigned int topf, topg, index;
01116 
01117     statLine(dd);
01118     if (bound < (f == Cudd_Not(g))) return(azero);
01119     /* Terminal cases. */
01120     if (g == lzero || f == lzero) return(azero);
01121     if (f == one && g == one) return(one);
01122 
01123     /* Check cache. */
01124     F = Cudd_Regular(f);
01125     G = Cudd_Regular(g);
01126     if (F->ref != 1 || G->ref != 1) {
01127         res = cuddCacheLookup2(dd,(DdNode * (*)(DdManager *, DdNode *,
01128                                DdNode *)) Cudd_bddClosestCube, f, g);
01129         if (res != NULL) return(res);
01130     }
01131 
01132     topf = cuddI(dd,F->index);
01133     topg = cuddI(dd,G->index);
01134 
01135     /* Compute cofactors. */
01136     if (topf <= topg) {
01137         index = F->index;
01138         ft = cuddT(F);
01139         fe = cuddE(F);
01140         if (Cudd_IsComplement(f)) {
01141             ft = Cudd_Not(ft);
01142             fe = Cudd_Not(fe);
01143         }
01144     } else {
01145         index = G->index;
01146         ft = fe = f;
01147     }
01148 
01149     if (topg <= topf) {
01150         gt = cuddT(G);
01151         ge = cuddE(G);
01152         if (Cudd_IsComplement(g)) {
01153             gt = Cudd_Not(gt);
01154             ge = Cudd_Not(ge);
01155         }
01156     } else {
01157         gt = ge = g;
01158     }
01159 
01160     tt = cuddBddClosestCube(dd,ft,gt,bound);
01161     if (tt == NULL) return(NULL);
01162     cuddRef(tt);
01163     ctt = separateCube(dd,tt,&dtt);
01164     if (ctt == NULL) {
01165         Cudd_RecursiveDeref(dd, tt);
01166         return(NULL);
01167     }
01168     cuddRef(ctt);
01169     Cudd_RecursiveDeref(dd, tt);
01170     minD = dtt;
01171     bound = ddMin(bound,minD);
01172 
01173     ee = cuddBddClosestCube(dd,fe,ge,bound);
01174     if (ee == NULL) {
01175         Cudd_RecursiveDeref(dd, ctt);
01176         return(NULL);
01177     }
01178     cuddRef(ee);
01179     cee = separateCube(dd,ee,&dee);
01180     if (cee == NULL) {
01181         Cudd_RecursiveDeref(dd, ctt);
01182         Cudd_RecursiveDeref(dd, ee);
01183         return(NULL);
01184     }
01185     cuddRef(cee);
01186     Cudd_RecursiveDeref(dd, ee);
01187     minD = ddMin(dtt, dee);
01188     bound = ddMin(bound,minD-1);
01189 
01190     if (minD > 0 && topf == topg) {
01191         DdNode *te = cuddBddClosestCube(dd,ft,ge,bound-1);
01192         if (te == NULL) {
01193             Cudd_RecursiveDeref(dd, ctt);
01194             Cudd_RecursiveDeref(dd, cee);
01195             return(NULL);
01196         }
01197         cuddRef(te);
01198         cte = separateCube(dd,te,&dte);
01199         if (cte == NULL) {
01200             Cudd_RecursiveDeref(dd, ctt);
01201             Cudd_RecursiveDeref(dd, cee);
01202             Cudd_RecursiveDeref(dd, te);
01203             return(NULL);
01204         }
01205         cuddRef(cte);
01206         Cudd_RecursiveDeref(dd, te);
01207         dte += 1.0;
01208         minD = ddMin(minD, dte);
01209     } else {
01210         cte = azero;
01211         cuddRef(cte);
01212         dte = CUDD_CONST_INDEX + 1.0;
01213     }
01214     bound = ddMin(bound,minD-1);
01215 
01216     if (minD > 0 && topf == topg) {
01217         DdNode *et = cuddBddClosestCube(dd,fe,gt,bound-1);
01218         if (et == NULL) {
01219             Cudd_RecursiveDeref(dd, ctt);
01220             Cudd_RecursiveDeref(dd, cee);
01221             Cudd_RecursiveDeref(dd, cte);
01222             return(NULL);
01223         }
01224         cuddRef(et);
01225         cet = separateCube(dd,et,&det);
01226         if (cet == NULL) {
01227             Cudd_RecursiveDeref(dd, ctt);
01228             Cudd_RecursiveDeref(dd, cee);
01229             Cudd_RecursiveDeref(dd, cte);
01230             Cudd_RecursiveDeref(dd, et);
01231             return(NULL);
01232         }
01233         cuddRef(cet);
01234         Cudd_RecursiveDeref(dd, et);
01235         det += 1.0;
01236         minD = ddMin(minD, det);
01237     } else {
01238         cet = azero;
01239         cuddRef(cet);
01240         det = CUDD_CONST_INDEX + 1.0;
01241     }
01242 
01243     if (minD == dtt) {
01244         if (dtt == dee && ctt == cee) {
01245             res = createResult(dd,CUDD_CONST_INDEX,1,ctt,dtt);
01246         } else {
01247             res = createResult(dd,index,1,ctt,dtt);
01248         }
01249     } else if (minD == dee) {
01250         res = createResult(dd,index,0,cee,dee);
01251     } else if (minD == dte) {
01252         res = createResult(dd,index,(topf <= topg),cte,dte);
01253     } else {
01254         res = createResult(dd,index,(topf > topg),cet,det);
01255     }
01256     cuddRef(res);
01257     Cudd_RecursiveDeref(dd, ctt);
01258     Cudd_RecursiveDeref(dd, cee);
01259     Cudd_RecursiveDeref(dd, cte);
01260     Cudd_RecursiveDeref(dd, cet);
01261 
01262     if (F->ref != 1 || G->ref != 1)
01263         cuddCacheInsert2(dd,(DdNode * (*)(DdManager *, DdNode *,
01264                          DdNode *)) Cudd_bddClosestCube, f, g, res);
01265 
01266     cuddDeref(res);
01267     return(res);
01268 
01269 } /* end of cuddBddClosestCube */
01270 
01271 
01272 /*---------------------------------------------------------------------------*/
01273 /* Definition of static functions                                            */
01274 /*---------------------------------------------------------------------------*/
01275 
01276 
01301 static int
01302 cuddMinHammingDistRecur(
01303   DdNode * f,
01304   int *minterm,
01305   DdHashTable * table,
01306   int upperBound)
01307 {
01308     DdNode      *F, *Ft, *Fe;
01309     double      h, hT, hE;
01310     DdNode      *zero, *res;
01311     DdManager   *dd = table->manager;
01312 
01313     statLine(dd);
01314     if (upperBound == 0) return(0);
01315 
01316     F = Cudd_Regular(f);
01317 
01318     if (cuddIsConstant(F)) {
01319         zero = Cudd_Not(DD_ONE(dd));
01320         if (f == dd->background || f == zero) {
01321             return(upperBound);
01322         } else {
01323             return(0);
01324         }
01325     }
01326     if ((res = cuddHashTableLookup1(table,f)) != NULL) {
01327         h = cuddV(res);
01328         if (res->ref == 0) {
01329             dd->dead++;
01330             dd->constants.dead++;
01331         }
01332         return((int) h);
01333     }
01334 
01335     Ft = cuddT(F); Fe = cuddE(F);
01336     if (Cudd_IsComplement(f)) {
01337         Ft = Cudd_Not(Ft); Fe = Cudd_Not(Fe);
01338     }
01339     if (minterm[F->index] == 0) {
01340         DdNode *temp = Ft;
01341         Ft = Fe; Fe = temp;
01342     }
01343 
01344     hT = cuddMinHammingDistRecur(Ft,minterm,table,upperBound);
01345     if (hT == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
01346     if (hT == 0) {
01347         hE = upperBound;
01348     } else {
01349         hE = cuddMinHammingDistRecur(Fe,minterm,table,upperBound - 1);
01350         if (hE == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
01351     }
01352     h = ddMin(hT, hE + 1);
01353 
01354     if (F->ref != 1) {
01355         ptrint fanout = (ptrint) F->ref;
01356         cuddSatDec(fanout);
01357         res = cuddUniqueConst(dd, (CUDD_VALUE_TYPE) h);
01358         if (!cuddHashTableInsert1(table,f,res,fanout)) {
01359             cuddRef(res); Cudd_RecursiveDeref(dd, res);
01360             return(CUDD_OUT_OF_MEM);
01361         }
01362     }
01363 
01364     return((int) h);
01365 
01366 } /* end of cuddMinHammingDistRecur */
01367 
01368 
01381 static DdNode *
01382 separateCube(
01383   DdManager *dd,
01384   DdNode *f,
01385   CUDD_VALUE_TYPE *distance)
01386 {
01387     DdNode *cube, *t;
01388 
01389     /* One and zero are special cases because the distance is implied. */
01390     if (Cudd_IsConstant(f)) {
01391         *distance = (f == DD_ONE(dd)) ? 0.0 :
01392             (1.0 + (CUDD_VALUE_TYPE) CUDD_CONST_INDEX);
01393         return(f);
01394     }
01395 
01396     /* Find out which branch points to the distance and replace the top
01397     ** node with one pointing to zero instead. */
01398     t = cuddT(f);
01399     if (Cudd_IsConstant(t) && cuddV(t) <= 0) {
01400 #ifdef DD_DEBUG
01401         assert(!Cudd_IsConstant(cuddE(f)) || cuddE(f) == DD_ONE(dd));
01402 #endif
01403         *distance = -cuddV(t);
01404         cube = cuddUniqueInter(dd, f->index, DD_ZERO(dd), cuddE(f));
01405     } else {
01406 #ifdef DD_DEBUG
01407         assert(!Cudd_IsConstant(t) || t == DD_ONE(dd));
01408 #endif
01409         *distance = -cuddV(cuddE(f));
01410         cube = cuddUniqueInter(dd, f->index, t, DD_ZERO(dd));
01411     }
01412 
01413     return(cube);
01414 
01415 } /* end of separateCube */
01416 
01417 
01430 static DdNode *
01431 createResult(
01432   DdManager *dd,
01433   unsigned int index,
01434   unsigned int phase,
01435   DdNode *cube,
01436   CUDD_VALUE_TYPE distance)
01437 {
01438     DdNode *res, *constant;
01439 
01440     /* Special case.  The cube is either one or zero, and we do not
01441     ** add any variables.  Hence, the result is also one or zero,
01442     ** and the distance remains implied by teh value of the constant. */
01443     if (index == CUDD_CONST_INDEX && Cudd_IsConstant(cube)) return(cube);
01444 
01445     constant = cuddUniqueConst(dd,-distance);
01446     if (constant == NULL) return(NULL);
01447     cuddRef(constant);
01448 
01449     if (index == CUDD_CONST_INDEX) {
01450         /* Replace the top node. */
01451         if (cuddT(cube) == DD_ZERO(dd)) {
01452             res = cuddUniqueInter(dd,cube->index,constant,cuddE(cube));
01453         } else {
01454             res = cuddUniqueInter(dd,cube->index,cuddT(cube),constant);
01455         }
01456     } else {
01457         /* Add a new top node. */
01458 #ifdef DD_DEBUG
01459         assert(cuddI(dd,index) < cuddI(dd,cube->index));
01460 #endif
01461         if (phase) {
01462             res = cuddUniqueInter(dd,index,cube,constant);
01463         } else {
01464             res = cuddUniqueInter(dd,index,constant,cube);
01465         }
01466     }
01467     if (res == NULL) {
01468         Cudd_RecursiveDeref(dd, constant);
01469         return(NULL);
01470     }
01471     cuddDeref(constant); /* safe because constant is part of res */
01472 
01473     return(res);
01474 
01475 } /* end of createResult */