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

00001 
00049 #include "util_hack.h"
00050 #include "cuddInt.h"
00051 
00052 
00053 /*---------------------------------------------------------------------------*/
00054 /* Constant declarations                                                     */
00055 /*---------------------------------------------------------------------------*/
00056 
00057 /* Codes for edge markings in Cudd_bddLICompaction.  The codes are defined
00058 ** so that they can be bitwise ORed to implement the code priority scheme.
00059 */
00060 #define DD_LIC_DC 0
00061 #define DD_LIC_1  1
00062 #define DD_LIC_0  2
00063 #define DD_LIC_NL 3
00064 
00065 /*---------------------------------------------------------------------------*/
00066 /* Stucture declarations                                                     */
00067 /*---------------------------------------------------------------------------*/
00068 
00069 
00070 /*---------------------------------------------------------------------------*/
00071 /* Type declarations                                                         */
00072 /*---------------------------------------------------------------------------*/
00073 
00074 /* Key for the cache used in the edge marking phase. */
00075 typedef struct MarkCacheKey {
00076     DdNode *f;
00077     DdNode *c;
00078 } MarkCacheKey;
00079 
00080 /*---------------------------------------------------------------------------*/
00081 /* Variable declarations                                                     */
00082 /*---------------------------------------------------------------------------*/
00083 
00084 #ifndef lint
00085 static char rcsid[] DD_UNUSED = "$Id: cuddGenCof.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $";
00086 #endif
00087 
00088 /*---------------------------------------------------------------------------*/
00089 /* Macro declarations                                                        */
00090 /*---------------------------------------------------------------------------*/
00091 
00092 
00095 /*---------------------------------------------------------------------------*/
00096 /* Static function prototypes                                                */
00097 /*---------------------------------------------------------------------------*/
00098 
00099 static int cuddBddConstrainDecomp ARGS((DdManager *dd, DdNode *f, DdNode **decomp));
00100 static DdNode * cuddBddCharToVect ARGS((DdManager *dd, DdNode *f, DdNode *x));
00101 static int cuddBddLICMarkEdges ARGS((DdManager *dd, DdNode *f, DdNode *c, st_table *table, st_table *cache));
00102 static DdNode * cuddBddLICBuildResult ARGS((DdManager *dd, DdNode *f, st_table *cache, st_table *table));
00103 static int MarkCacheHash ARGS((char *ptr, int modulus));
00104 static int MarkCacheCompare ARGS((const char *ptr1, const char *ptr2));
00105 static enum st_retval MarkCacheCleanUp ARGS((char *key, char *value, char *arg));
00106 static DdNode * cuddBddSqueeze ARGS((DdManager *dd, DdNode *l, DdNode *u));
00107 
00111 /*---------------------------------------------------------------------------*/
00112 /* Definition of exported functions                                          */
00113 /*---------------------------------------------------------------------------*/
00114 
00115 
00140 DdNode *
00141 Cudd_bddConstrain(
00142   DdManager * dd,
00143   DdNode * f,
00144   DdNode * c)
00145 {
00146     DdNode *res;
00147 
00148     do {
00149         dd->reordered = 0;
00150         res = cuddBddConstrainRecur(dd,f,c);
00151     } while (dd->reordered == 1);
00152     return(res);
00153 
00154 } /* end of Cudd_bddConstrain */
00155 
00156 
00172 DdNode *
00173 Cudd_bddRestrict(
00174   DdManager * dd,
00175   DdNode * f,
00176   DdNode * c)
00177 {
00178     DdNode *suppF, *suppC, *commonSupport;
00179     DdNode *cplus, *res;
00180     int retval;
00181     int sizeF, sizeRes;
00182 
00183     /* Check terminal cases here to avoid computing supports in trivial cases.
00184     ** This also allows us notto check later for the case c == 0, in which
00185     ** there is no common support. */
00186     if (c == Cudd_Not(DD_ONE(dd))) return(Cudd_Not(DD_ONE(dd)));
00187     if (Cudd_IsConstant(f)) return(f);
00188     if (f == c) return(DD_ONE(dd));
00189     if (f == Cudd_Not(c)) return(Cudd_Not(DD_ONE(dd)));
00190 
00191     /* Check if supports intersect. */
00192     retval = Cudd_ClassifySupport(dd,f,c,&commonSupport,&suppF,&suppC);
00193     if (retval == 0) {
00194         return(NULL);
00195     }
00196     cuddRef(commonSupport); cuddRef(suppF); cuddRef(suppC);
00197     Cudd_IterDerefBdd(dd,suppF);
00198 
00199     if (commonSupport == DD_ONE(dd)) {
00200         Cudd_IterDerefBdd(dd,commonSupport);
00201         Cudd_IterDerefBdd(dd,suppC);
00202         return(f);
00203     }
00204     Cudd_IterDerefBdd(dd,commonSupport);
00205 
00206     /* Abstract from c the variables that do not appear in f. */
00207     cplus = Cudd_bddExistAbstract(dd, c, suppC);
00208     if (cplus == NULL) {
00209         Cudd_IterDerefBdd(dd,suppC);
00210         return(NULL);
00211     }
00212     cuddRef(cplus);
00213     Cudd_IterDerefBdd(dd,suppC);
00214 
00215     do {
00216         dd->reordered = 0;
00217         res = cuddBddRestrictRecur(dd, f, cplus);
00218     } while (dd->reordered == 1);
00219     if (res == NULL) {
00220         Cudd_IterDerefBdd(dd,cplus);
00221         return(NULL);
00222     }
00223     cuddRef(res);
00224     Cudd_IterDerefBdd(dd,cplus);
00225     /* Make restric safe by returning the smaller of the input and the
00226     ** result. */
00227     sizeF = Cudd_DagSize(f);
00228     sizeRes = Cudd_DagSize(res);
00229     if (sizeF <= sizeRes) {
00230         Cudd_IterDerefBdd(dd, res);
00231         return(f);
00232     } else {
00233         cuddDeref(res);
00234         return(res);
00235     }
00236 
00237 } /* end of Cudd_bddRestrict */
00238 
00239 
00260 DdNode *
00261 Cudd_addConstrain(
00262   DdManager * dd,
00263   DdNode * f,
00264   DdNode * c)
00265 {
00266     DdNode *res;
00267 
00268     do {
00269         dd->reordered = 0;
00270         res = cuddAddConstrainRecur(dd,f,c);
00271     } while (dd->reordered == 1);
00272     return(res);
00273 
00274 } /* end of Cudd_addConstrain */
00275 
00276 
00295 DdNode **
00296 Cudd_bddConstrainDecomp(
00297   DdManager * dd,
00298   DdNode * f)
00299 {
00300     DdNode **decomp;
00301     int res;
00302     int i;
00303 
00304     /* Create an initialize decomposition array. */
00305     decomp = ALLOC(DdNode *,dd->size);
00306     if (decomp == NULL) {
00307         dd->errorCode = CUDD_MEMORY_OUT;
00308         return(NULL);
00309     }
00310     for (i = 0; i < dd->size; i++) {
00311         decomp[i] = NULL;
00312     }
00313     do {
00314         dd->reordered = 0;
00315         /* Clean up the decomposition array in case reordering took place. */
00316         for (i = 0; i < dd->size; i++) {
00317             if (decomp[i] != NULL) {
00318                 Cudd_IterDerefBdd(dd, decomp[i]);
00319                 decomp[i] = NULL;
00320             }
00321         }
00322         res = cuddBddConstrainDecomp(dd,f,decomp);
00323     } while (dd->reordered == 1);
00324     if (res == 0) {
00325         FREE(decomp);
00326         return(NULL);
00327     }
00328     /* Missing components are constant ones. */
00329     for (i = 0; i < dd->size; i++) {
00330         if (decomp[i] == NULL) {
00331             decomp[i] = DD_ONE(dd);
00332             cuddRef(decomp[i]);
00333         }
00334     }
00335     return(decomp);
00336 
00337 } /* end of Cudd_bddConstrainDecomp */
00338 
00339 
00355 DdNode *
00356 Cudd_addRestrict(
00357   DdManager * dd,
00358   DdNode * f,
00359   DdNode * c)
00360 {
00361     DdNode *supp_f, *supp_c;
00362     DdNode *res, *commonSupport;
00363     int intersection;
00364     int sizeF, sizeRes;
00365 
00366     /* Check if supports intersect. */
00367     supp_f = Cudd_Support(dd, f);
00368     if (supp_f == NULL) {
00369         return(NULL);
00370     }
00371     cuddRef(supp_f);
00372     supp_c = Cudd_Support(dd, c);
00373     if (supp_c == NULL) {
00374         Cudd_RecursiveDeref(dd,supp_f);
00375         return(NULL);
00376     }
00377     cuddRef(supp_c);
00378     commonSupport = Cudd_bddLiteralSetIntersection(dd, supp_f, supp_c);
00379     if (commonSupport == NULL) {
00380         Cudd_RecursiveDeref(dd,supp_f);
00381         Cudd_RecursiveDeref(dd,supp_c);
00382         return(NULL);
00383     }
00384     cuddRef(commonSupport);
00385     Cudd_RecursiveDeref(dd,supp_f);
00386     Cudd_RecursiveDeref(dd,supp_c);
00387     intersection = commonSupport != DD_ONE(dd);
00388     Cudd_RecursiveDeref(dd,commonSupport);
00389 
00390     if (intersection) {
00391         do {
00392             dd->reordered = 0;
00393             res = cuddAddRestrictRecur(dd, f, c);
00394         } while (dd->reordered == 1);
00395         sizeF = Cudd_DagSize(f);
00396         sizeRes = Cudd_DagSize(res);
00397         if (sizeF <= sizeRes) {
00398             cuddRef(res);
00399             Cudd_RecursiveDeref(dd, res);
00400             return(f);
00401         } else {
00402             return(res);
00403         }
00404     } else {
00405         return(f);
00406     }
00407 
00408 } /* end of Cudd_addRestrict */
00409 
00410 
00434 DdNode **
00435 Cudd_bddCharToVect(
00436   DdManager * dd,
00437   DdNode * f)
00438 {
00439     int i, j;
00440     DdNode **vect;
00441     DdNode *res = NULL;
00442 
00443     if (f == Cudd_Not(DD_ONE(dd))) return(NULL);
00444 
00445     vect = ALLOC(DdNode *, dd->size);
00446     if (vect == NULL) {
00447         dd->errorCode = CUDD_MEMORY_OUT;
00448         return(NULL);
00449     }
00450 
00451     do {
00452         dd->reordered = 0;
00453         for (i = 0; i < dd->size; i++) {
00454             res = cuddBddCharToVect(dd,f,dd->vars[dd->invperm[i]]);
00455             if (res == NULL) {
00456                 /* Clean up the vector array in case reordering took place. */
00457                 for (j = 0; j < i; j++) {
00458                     Cudd_IterDerefBdd(dd, vect[dd->invperm[j]]);
00459                 }
00460                 break;
00461             }
00462             cuddRef(res);
00463             vect[dd->invperm[i]] = res;
00464         }
00465     } while (dd->reordered == 1);
00466     if (res == NULL) {
00467         FREE(vect);
00468         return(NULL);
00469     }
00470     return(vect);
00471 
00472 } /* end of Cudd_bddCharToVect */
00473 
00474 
00494 DdNode *
00495 Cudd_bddLICompaction(
00496   DdManager * dd /* manager */,
00497   DdNode * f /* function to be minimized */,
00498   DdNode * c /* constraint (care set) */)
00499 {
00500     DdNode *res;
00501 
00502     do {
00503         dd->reordered = 0;
00504         res = cuddBddLICompaction(dd,f,c);
00505     } while (dd->reordered == 1);
00506     return(res);
00507 
00508 } /* end of Cudd_bddLICompaction */
00509 
00510 
00526 DdNode *
00527 Cudd_bddSqueeze(
00528   DdManager * dd /* manager */,
00529   DdNode * l /* lower bound */,
00530   DdNode * u /* upper bound */)
00531 {
00532     DdNode *res;
00533     int sizeRes, sizeL, sizeU;
00534 
00535     do {
00536         dd->reordered = 0;
00537         res = cuddBddSqueeze(dd,l,u);
00538     } while (dd->reordered == 1);
00539     if (res == NULL) return(NULL);
00540     /* We now compare the result with the bounds and return the smallest.
00541     ** We first compare to u, so that in case l == 0 and u == 1, we return
00542     ** 0 as in other minimization algorithms. */
00543     sizeRes = Cudd_DagSize(res);
00544     sizeU = Cudd_DagSize(u);
00545     if (sizeU <= sizeRes) {
00546         cuddRef(res);
00547         Cudd_IterDerefBdd(dd,res);
00548         res = u;
00549         sizeRes = sizeU;
00550     }
00551     sizeL = Cudd_DagSize(l);
00552     if (sizeL <= sizeRes) {
00553         cuddRef(res);
00554         Cudd_IterDerefBdd(dd,res);
00555         res = l;
00556         sizeRes = sizeL;
00557     }
00558     return(res);
00559 
00560 } /* end of Cudd_bddSqueeze */
00561 
00562 
00577 DdNode *
00578 Cudd_bddMinimize(
00579   DdManager * dd,
00580   DdNode * f,
00581   DdNode * c)
00582 {
00583     DdNode *cplus, *res;
00584 
00585     if (c == Cudd_Not(DD_ONE(dd))) return(c);
00586     if (Cudd_IsConstant(f)) return(f);
00587     if (f == c) return(DD_ONE(dd));
00588     if (f == Cudd_Not(c)) return(Cudd_Not(DD_ONE(dd)));
00589 
00590     cplus = Cudd_RemapOverApprox(dd,c,0,0,1.0);
00591     if (cplus == NULL) return(NULL);
00592     cuddRef(cplus);
00593     res = Cudd_bddLICompaction(dd,f,cplus);
00594     if (res == NULL) {
00595         Cudd_IterDerefBdd(dd,cplus);
00596         return(NULL);
00597     }
00598     cuddRef(res);
00599     Cudd_IterDerefBdd(dd,cplus);
00600     cuddDeref(res);
00601     return(res);
00602 
00603 } /* end of Cudd_bddMinimize */
00604 
00605 
00624 DdNode *
00625 Cudd_SubsetCompress(
00626   DdManager * dd /* manager */,
00627   DdNode * f /* BDD whose subset is sought */,
00628   int  nvars /* number of variables in the support of f */,
00629   int  threshold /* maximum number of nodes in the subset */)
00630 {
00631     DdNode *res, *tmp1, *tmp2;
00632 
00633     tmp1 = Cudd_SubsetShortPaths(dd, f, nvars, threshold, 0);
00634     if (tmp1 == NULL) return(NULL);
00635     cuddRef(tmp1);
00636     tmp2 = Cudd_RemapUnderApprox(dd,tmp1,nvars,0,1.0);
00637     if (tmp2 == NULL) {
00638         Cudd_IterDerefBdd(dd,tmp1);
00639         return(NULL);
00640     }
00641     cuddRef(tmp2);
00642     Cudd_IterDerefBdd(dd,tmp1);
00643     res = Cudd_bddSqueeze(dd,tmp2,f);
00644     if (res == NULL) {
00645         Cudd_IterDerefBdd(dd,tmp2);
00646         return(NULL);
00647     }
00648     cuddRef(res);
00649     Cudd_IterDerefBdd(dd,tmp2);
00650     cuddDeref(res);
00651     return(res);
00652 
00653 } /* end of Cudd_SubsetCompress */
00654 
00655 
00674 DdNode *
00675 Cudd_SupersetCompress(
00676   DdManager * dd /* manager */,
00677   DdNode * f /* BDD whose superset is sought */,
00678   int  nvars /* number of variables in the support of f */,
00679   int  threshold /* maximum number of nodes in the superset */)
00680 {
00681     DdNode *subset;
00682 
00683     subset = Cudd_SubsetCompress(dd, Cudd_Not(f),nvars,threshold);
00684 
00685     return(Cudd_NotCond(subset, (subset != NULL)));
00686 
00687 } /* end of Cudd_SupersetCompress */
00688 
00689 
00690 /*---------------------------------------------------------------------------*/
00691 /* Definition of internal functions                                          */
00692 /*---------------------------------------------------------------------------*/
00693 
00694 
00707 DdNode *
00708 cuddBddConstrainRecur(
00709   DdManager * dd,
00710   DdNode * f,
00711   DdNode * c)
00712 {
00713     DdNode       *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r;
00714     DdNode       *one, *zero;
00715     unsigned int topf, topc;
00716     int          index;
00717     int          comple = 0;
00718 
00719     statLine(dd);
00720     one = DD_ONE(dd);
00721     zero = Cudd_Not(one);
00722 
00723     /* Trivial cases. */
00724     if (c == one)               return(f);
00725     if (c == zero)              return(zero);
00726     if (Cudd_IsConstant(f))     return(f);
00727     if (f == c)                 return(one);
00728     if (f == Cudd_Not(c))       return(zero);
00729 
00730     /* Make canonical to increase the utilization of the cache. */
00731     if (Cudd_IsComplement(f)) {
00732         f = Cudd_Not(f);
00733         comple = 1;
00734     }
00735     /* Now f is a regular pointer to a non-constant node; c is also
00736     ** non-constant, but may be complemented.
00737     */
00738 
00739     /* Check the cache. */
00740     r = cuddCacheLookup2(dd, Cudd_bddConstrain, f, c);
00741     if (r != NULL) {
00742         return(Cudd_NotCond(r,comple));
00743     }
00744     
00745     /* Recursive step. */
00746     topf = dd->perm[f->index];
00747     topc = dd->perm[Cudd_Regular(c)->index];
00748     if (topf <= topc) {
00749         index = f->index;
00750         Fv = cuddT(f); Fnv = cuddE(f);
00751     } else {
00752         index = Cudd_Regular(c)->index;
00753         Fv = Fnv = f;
00754     }
00755     if (topc <= topf) {
00756         Cv = cuddT(Cudd_Regular(c)); Cnv = cuddE(Cudd_Regular(c));
00757         if (Cudd_IsComplement(c)) {
00758             Cv = Cudd_Not(Cv);
00759             Cnv = Cudd_Not(Cnv);
00760         }
00761     } else {
00762         Cv = Cnv = c;
00763     }
00764 
00765     if (!Cudd_IsConstant(Cv)) {
00766         t = cuddBddConstrainRecur(dd, Fv, Cv);
00767         if (t == NULL)
00768             return(NULL);
00769     } else if (Cv == one) {
00770         t = Fv;
00771     } else {            /* Cv == zero: return Fnv @ Cnv */
00772         if (Cnv == one) {
00773             r = Fnv;
00774         } else {
00775             r = cuddBddConstrainRecur(dd, Fnv, Cnv);
00776             if (r == NULL)
00777                 return(NULL);
00778         }
00779         return(Cudd_NotCond(r,comple));
00780     }
00781     cuddRef(t);
00782 
00783     if (!Cudd_IsConstant(Cnv)) {
00784         e = cuddBddConstrainRecur(dd, Fnv, Cnv);
00785         if (e == NULL) {
00786             Cudd_IterDerefBdd(dd, t);
00787             return(NULL);
00788         }
00789     } else if (Cnv == one) {
00790         e = Fnv;
00791     } else {            /* Cnv == zero: return Fv @ Cv previously computed */
00792         cuddDeref(t);
00793         return(Cudd_NotCond(t,comple));
00794     }
00795     cuddRef(e);
00796 
00797     if (Cudd_IsComplement(t)) {
00798         t = Cudd_Not(t);
00799         e = Cudd_Not(e);
00800         r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
00801         if (r == NULL) {
00802             Cudd_IterDerefBdd(dd, e);
00803             Cudd_IterDerefBdd(dd, t);
00804             return(NULL);
00805         }
00806         r = Cudd_Not(r);
00807     } else {
00808         r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
00809         if (r == NULL) {
00810             Cudd_IterDerefBdd(dd, e);
00811             Cudd_IterDerefBdd(dd, t);
00812             return(NULL);
00813         }
00814     }
00815     cuddDeref(t);
00816     cuddDeref(e);
00817 
00818     cuddCacheInsert2(dd, Cudd_bddConstrain, f, c, r);
00819     return(Cudd_NotCond(r,comple));
00820 
00821 } /* end of cuddBddConstrainRecur */
00822 
00823 
00836 DdNode *
00837 cuddBddRestrictRecur(
00838   DdManager * dd,
00839   DdNode * f,
00840   DdNode * c)
00841 {
00842     DdNode       *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r, *one, *zero;
00843     unsigned int topf, topc;
00844     int          index;
00845     int          comple = 0;
00846 
00847     statLine(dd);
00848     one = DD_ONE(dd);
00849     zero = Cudd_Not(one);
00850 
00851     /* Trivial cases */
00852     if (c == one)               return(f);
00853     if (c == zero)              return(zero);
00854     if (Cudd_IsConstant(f))     return(f);
00855     if (f == c)                 return(one);
00856     if (f == Cudd_Not(c))       return(zero);
00857 
00858     /* Make canonical to increase the utilization of the cache. */
00859     if (Cudd_IsComplement(f)) {
00860         f = Cudd_Not(f);
00861         comple = 1;
00862     }
00863     /* Now f is a regular pointer to a non-constant node; c is also
00864     ** non-constant, but may be complemented.
00865     */
00866 
00867     /* Check the cache. */
00868     r = cuddCacheLookup2(dd, Cudd_bddRestrict, f, c);
00869     if (r != NULL) {
00870         return(Cudd_NotCond(r,comple));
00871     }
00872 
00873     topf = dd->perm[f->index];
00874     topc = dd->perm[Cudd_Regular(c)->index];
00875 
00876     if (topc < topf) {  /* abstract top variable from c */
00877         DdNode *d, *s1, *s2;
00878 
00879         /* Find complements of cofactors of c. */
00880         if (Cudd_IsComplement(c)) {
00881             s1 = cuddT(Cudd_Regular(c));
00882             s2 = cuddE(Cudd_Regular(c));
00883         } else {
00884             s1 = Cudd_Not(cuddT(c));
00885             s2 = Cudd_Not(cuddE(c));
00886         }
00887         /* Take the OR by applying DeMorgan. */
00888         d = cuddBddAndRecur(dd, s1, s2);
00889         if (d == NULL) return(NULL);
00890         d = Cudd_Not(d);
00891         cuddRef(d);
00892         r = cuddBddRestrictRecur(dd, f, d);
00893         if (r == NULL) {
00894             Cudd_IterDerefBdd(dd, d);
00895             return(NULL);
00896         }
00897         cuddRef(r);
00898         Cudd_IterDerefBdd(dd, d);
00899         cuddCacheInsert2(dd, Cudd_bddRestrict, f, c, r);
00900         cuddDeref(r);
00901         return(Cudd_NotCond(r,comple));
00902     }
00903 
00904     /* Recursive step. Here topf <= topc. */
00905     index = f->index;
00906     Fv = cuddT(f); Fnv = cuddE(f);
00907     if (topc == topf) {
00908         Cv = cuddT(Cudd_Regular(c)); Cnv = cuddE(Cudd_Regular(c));
00909         if (Cudd_IsComplement(c)) {
00910             Cv = Cudd_Not(Cv);
00911             Cnv = Cudd_Not(Cnv);
00912         }
00913     } else {
00914         Cv = Cnv = c;
00915     }
00916 
00917     if (!Cudd_IsConstant(Cv)) {
00918         t = cuddBddRestrictRecur(dd, Fv, Cv);
00919         if (t == NULL) return(NULL);
00920     } else if (Cv == one) {
00921         t = Fv;
00922     } else {            /* Cv == zero: return(Fnv @ Cnv) */
00923         if (Cnv == one) {
00924             r = Fnv;
00925         } else {
00926             r = cuddBddRestrictRecur(dd, Fnv, Cnv);
00927             if (r == NULL) return(NULL);
00928         }
00929         return(Cudd_NotCond(r,comple));
00930     }
00931     cuddRef(t);
00932 
00933     if (!Cudd_IsConstant(Cnv)) {
00934         e = cuddBddRestrictRecur(dd, Fnv, Cnv);
00935         if (e == NULL) {
00936             Cudd_IterDerefBdd(dd, t);
00937             return(NULL);
00938         }
00939     } else if (Cnv == one) {
00940         e = Fnv;
00941     } else {            /* Cnv == zero: return (Fv @ Cv) previously computed */
00942         cuddDeref(t);
00943         return(Cudd_NotCond(t,comple));
00944     }
00945     cuddRef(e);
00946 
00947     if (Cudd_IsComplement(t)) {
00948         t = Cudd_Not(t);
00949         e = Cudd_Not(e);
00950         r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
00951         if (r == NULL) {
00952             Cudd_IterDerefBdd(dd, e);
00953             Cudd_IterDerefBdd(dd, t);
00954             return(NULL);
00955         }
00956         r = Cudd_Not(r);
00957     } else {
00958         r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
00959         if (r == NULL) {
00960             Cudd_IterDerefBdd(dd, e);
00961             Cudd_IterDerefBdd(dd, t);
00962             return(NULL);
00963         }
00964     }
00965     cuddDeref(t);
00966     cuddDeref(e);
00967 
00968     cuddCacheInsert2(dd, Cudd_bddRestrict, f, c, r);
00969     return(Cudd_NotCond(r,comple));
00970 
00971 } /* end of cuddBddRestrictRecur */
00972 
00973 
00986 DdNode *
00987 cuddAddConstrainRecur(
00988   DdManager * dd,
00989   DdNode * f,
00990   DdNode * c)
00991 {
00992     DdNode       *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r;
00993     DdNode       *one, *zero;
00994     unsigned int topf, topc;
00995     int          index;
00996 
00997     statLine(dd);
00998     one = DD_ONE(dd);
00999     zero = DD_ZERO(dd);
01000 
01001     /* Trivial cases. */
01002     if (c == one)               return(f);
01003     if (c == zero)              return(zero);
01004     if (Cudd_IsConstant(f))     return(f);
01005     if (f == c)                 return(one);
01006 
01007     /* Now f and c are non-constant. */
01008 
01009     /* Check the cache. */
01010     r = cuddCacheLookup2(dd, Cudd_addConstrain, f, c);
01011     if (r != NULL) {
01012         return(r);
01013     }
01014     
01015     /* Recursive step. */
01016     topf = dd->perm[f->index];
01017     topc = dd->perm[c->index];
01018     if (topf <= topc) {
01019         index = f->index;
01020         Fv = cuddT(f); Fnv = cuddE(f);
01021     } else {
01022         index = c->index;
01023         Fv = Fnv = f;
01024     }
01025     if (topc <= topf) {
01026         Cv = cuddT(c); Cnv = cuddE(c);
01027     } else {
01028         Cv = Cnv = c;
01029     }
01030 
01031     if (!Cudd_IsConstant(Cv)) {
01032         t = cuddAddConstrainRecur(dd, Fv, Cv);
01033         if (t == NULL)
01034             return(NULL);
01035     } else if (Cv == one) {
01036         t = Fv;
01037     } else {            /* Cv == zero: return Fnv @ Cnv */
01038         if (Cnv == one) {
01039             r = Fnv;
01040         } else {
01041             r = cuddAddConstrainRecur(dd, Fnv, Cnv);
01042             if (r == NULL)
01043                 return(NULL);
01044         }
01045         return(r);
01046     }
01047     cuddRef(t);
01048 
01049     if (!Cudd_IsConstant(Cnv)) {
01050         e = cuddAddConstrainRecur(dd, Fnv, Cnv);
01051         if (e == NULL) {
01052             Cudd_RecursiveDeref(dd, t);
01053             return(NULL);
01054         }
01055     } else if (Cnv == one) {
01056         e = Fnv;
01057     } else {            /* Cnv == zero: return Fv @ Cv previously computed */
01058         cuddDeref(t);
01059         return(t);
01060     }
01061     cuddRef(e);
01062 
01063     r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
01064     if (r == NULL) {
01065         Cudd_RecursiveDeref(dd, e);
01066         Cudd_RecursiveDeref(dd, t);
01067         return(NULL);
01068     }
01069     cuddDeref(t);
01070     cuddDeref(e);
01071 
01072     cuddCacheInsert2(dd, Cudd_addConstrain, f, c, r);
01073     return(r);
01074 
01075 } /* end of cuddAddConstrainRecur */
01076 
01077 
01090 DdNode *
01091 cuddAddRestrictRecur(
01092   DdManager * dd,
01093   DdNode * f,
01094   DdNode * c)
01095 {
01096     DdNode       *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r, *one, *zero;
01097     unsigned int topf, topc;
01098     int          index;
01099 
01100     statLine(dd);
01101     one = DD_ONE(dd);
01102     zero = DD_ZERO(dd);
01103 
01104     /* Trivial cases */
01105     if (c == one)               return(f);
01106     if (c == zero)              return(zero);
01107     if (Cudd_IsConstant(f))     return(f);
01108     if (f == c)                 return(one);
01109 
01110     /* Now f and c are non-constant. */
01111 
01112     /* Check the cache. */
01113     r = cuddCacheLookup2(dd, Cudd_addRestrict, f, c);
01114     if (r != NULL) {
01115         return(r);
01116     }
01117 
01118     topf = dd->perm[f->index];
01119     topc = dd->perm[c->index];
01120 
01121     if (topc < topf) {  /* abstract top variable from c */
01122         DdNode *d, *s1, *s2;
01123 
01124         /* Find cofactors of c. */
01125         s1 = cuddT(c);
01126         s2 = cuddE(c);
01127         /* Take the OR by applying DeMorgan. */
01128         d = cuddAddApplyRecur(dd, Cudd_addOr, s1, s2);
01129         if (d == NULL) return(NULL);
01130         cuddRef(d);
01131         r = cuddAddRestrictRecur(dd, f, d);
01132         if (r == NULL) {
01133             Cudd_RecursiveDeref(dd, d);
01134             return(NULL);
01135         }
01136         cuddRef(r);
01137         Cudd_RecursiveDeref(dd, d);
01138         cuddCacheInsert2(dd, Cudd_addRestrict, f, c, r);
01139         cuddDeref(r);
01140         return(r);
01141     }
01142 
01143     /* Recursive step. Here topf <= topc. */
01144     index = f->index;
01145     Fv = cuddT(f); Fnv = cuddE(f);
01146     if (topc == topf) {
01147         Cv = cuddT(c); Cnv = cuddE(c);
01148     } else {
01149         Cv = Cnv = c;
01150     }
01151 
01152     if (!Cudd_IsConstant(Cv)) {
01153         t = cuddAddRestrictRecur(dd, Fv, Cv);
01154         if (t == NULL) return(NULL);
01155     } else if (Cv == one) {
01156         t = Fv;
01157     } else {            /* Cv == zero: return(Fnv @ Cnv) */
01158         if (Cnv == one) {
01159             r = Fnv;
01160         } else {
01161             r = cuddAddRestrictRecur(dd, Fnv, Cnv);
01162             if (r == NULL) return(NULL);
01163         }
01164         return(r);
01165     }
01166     cuddRef(t);
01167 
01168     if (!Cudd_IsConstant(Cnv)) {
01169         e = cuddAddRestrictRecur(dd, Fnv, Cnv);
01170         if (e == NULL) {
01171             Cudd_RecursiveDeref(dd, t);
01172             return(NULL);
01173         }
01174     } else if (Cnv == one) {
01175         e = Fnv;
01176     } else {            /* Cnv == zero: return (Fv @ Cv) previously computed */
01177         cuddDeref(t);
01178         return(t);
01179     }
01180     cuddRef(e);
01181 
01182     r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
01183     if (r == NULL) {
01184         Cudd_RecursiveDeref(dd, e);
01185         Cudd_RecursiveDeref(dd, t);
01186         return(NULL);
01187     }
01188     cuddDeref(t);
01189     cuddDeref(e);
01190 
01191     cuddCacheInsert2(dd, Cudd_addRestrict, f, c, r);
01192     return(r);
01193 
01194 } /* end of cuddAddRestrictRecur */
01195 
01196 
01197 
01217 DdNode *
01218 cuddBddLICompaction(
01219   DdManager * dd /* manager */,
01220   DdNode * f /* function to be minimized */,
01221   DdNode * c /* constraint (care set) */)
01222 {
01223     st_table *marktable, *markcache, *buildcache;
01224     DdNode *res, *zero;
01225 
01226     zero = Cudd_Not(DD_ONE(dd));
01227     if (c == zero) return(zero);
01228 
01229     /* We need to use local caches for both steps of this operation.
01230     ** The results of the edge marking step are only valid as long as the
01231     ** edge markings themselves are available. However, the edge markings
01232     ** are lost at the end of one invocation of Cudd_bddLICompaction.
01233     ** Hence, the cache entries for the edge marking step must be
01234     ** invalidated at the end of this function.
01235     ** For the result of the building step we argue as follows. The result
01236     ** for a node and a given constrain depends on the BDD in which the node
01237     ** appears. Hence, the same node and constrain may give different results
01238     ** in successive invocations.
01239     */
01240     marktable = st_init_table(st_ptrcmp,st_ptrhash);
01241     if (marktable == NULL) {
01242         return(NULL);
01243     }
01244     markcache = st_init_table(MarkCacheCompare,MarkCacheHash);
01245     if (markcache == NULL) {
01246         st_free_table(marktable);
01247         return(NULL);
01248     }
01249     if (cuddBddLICMarkEdges(dd,f,c,marktable,markcache) == CUDD_OUT_OF_MEM) {
01250         st_foreach(markcache, MarkCacheCleanUp, NULL);
01251         st_free_table(marktable);
01252         st_free_table(markcache);
01253         return(NULL);
01254     }
01255     st_foreach(markcache, MarkCacheCleanUp, NULL);
01256     st_free_table(markcache);
01257     buildcache = st_init_table(st_ptrcmp,st_ptrhash);
01258     if (buildcache == NULL) {
01259         st_free_table(marktable);
01260         return(NULL);
01261     }
01262     res = cuddBddLICBuildResult(dd,f,buildcache,marktable);
01263     st_free_table(buildcache);
01264     st_free_table(marktable);
01265     return(res);
01266 
01267 } /* end of cuddBddLICompaction */
01268 
01269 
01270 /*---------------------------------------------------------------------------*/
01271 /* Definition of static functions                                            */
01272 /*---------------------------------------------------------------------------*/
01273 
01274 
01287 static int
01288 cuddBddConstrainDecomp(
01289   DdManager * dd,
01290   DdNode * f,
01291   DdNode ** decomp)
01292 {
01293     DdNode *F, *fv, *fvn;
01294     DdNode *fAbs;
01295     DdNode *result;
01296     int ok;
01297 
01298     if (Cudd_IsConstant(f)) return(1);
01299     /* Compute complements of cofactors. */
01300     F = Cudd_Regular(f);
01301     fv = cuddT(F);
01302     fvn = cuddE(F);
01303     if (F == f) {
01304         fv = Cudd_Not(fv);
01305         fvn = Cudd_Not(fvn);
01306     }
01307     /* Compute abstraction of top variable. */
01308     fAbs = cuddBddAndRecur(dd, fv, fvn);
01309     if (fAbs == NULL) {
01310         return(0);
01311     }
01312     cuddRef(fAbs);
01313     fAbs = Cudd_Not(fAbs);
01314     /* Recursively find the next abstraction and the components of the
01315     ** decomposition. */
01316     ok = cuddBddConstrainDecomp(dd, fAbs, decomp);
01317     if (ok == 0) {
01318         Cudd_IterDerefBdd(dd,fAbs);
01319         return(0);
01320     }
01321     /* Compute the component of the decomposition corresponding to the
01322     ** top variable and store it in the decomposition array. */
01323     result = cuddBddConstrainRecur(dd, f, fAbs);
01324     if (result == NULL) {
01325         Cudd_IterDerefBdd(dd,fAbs);
01326         return(0);
01327     }
01328     cuddRef(result);
01329     decomp[F->index] = result;
01330     Cudd_IterDerefBdd(dd, fAbs);
01331     return(1);
01332 
01333 } /* end of cuddBddConstrainDecomp */
01334 
01335 
01349 static DdNode *
01350 cuddBddCharToVect(
01351   DdManager * dd,
01352   DdNode * f,
01353   DdNode * x)
01354 {
01355     unsigned int topf;
01356     unsigned int level;
01357     int comple;
01358 
01359     DdNode *one, *zero, *res, *F, *fT, *fE, *T, *E;
01360 
01361     statLine(dd);
01362     /* Check the cache. */
01363     res = cuddCacheLookup2(dd, cuddBddCharToVect, f, x);
01364     if (res != NULL) {
01365         return(res);
01366     }
01367 
01368     F = Cudd_Regular(f);
01369 
01370     topf = cuddI(dd,F->index);
01371     level = dd->perm[x->index];
01372 
01373     if (topf > level) return(x);
01374 
01375     one = DD_ONE(dd);
01376     zero = Cudd_Not(one);
01377 
01378     comple = F != f;
01379     fT = Cudd_NotCond(cuddT(F),comple);
01380     fE = Cudd_NotCond(cuddE(F),comple);
01381 
01382     if (topf == level) {
01383         if (fT == zero) return(zero);
01384         if (fE == zero) return(one);
01385         return(x);
01386     }
01387 
01388     /* Here topf < level. */
01389     if (fT == zero) return(cuddBddCharToVect(dd, fE, x));
01390     if (fE == zero) return(cuddBddCharToVect(dd, fT, x));
01391 
01392     T = cuddBddCharToVect(dd, fT, x);
01393     if (T == NULL) {
01394         return(NULL);
01395     }
01396     cuddRef(T);
01397     E = cuddBddCharToVect(dd, fE, x);
01398     if (E == NULL) {
01399         Cudd_IterDerefBdd(dd,T);
01400         return(NULL);
01401     }
01402     cuddRef(E);
01403     res = cuddBddIteRecur(dd, dd->vars[F->index], T, E);
01404     if (res == NULL) {
01405         Cudd_IterDerefBdd(dd,T);
01406         Cudd_IterDerefBdd(dd,E);
01407         return(NULL);
01408     }
01409     cuddDeref(T);
01410     cuddDeref(E);
01411     cuddCacheInsert2(dd, cuddBddCharToVect, f, x, res);
01412     return(res);
01413 
01414 } /* end of cuddBddCharToVect */
01415 
01416 
01430 static int
01431 cuddBddLICMarkEdges(
01432   DdManager * dd,
01433   DdNode * f,
01434   DdNode * c,
01435   st_table * table,
01436   st_table * cache)
01437 {
01438     DdNode *Fv, *Fnv, *Cv, *Cnv;
01439     DdNode *one, *zero;
01440     unsigned int topf, topc;
01441     int index;
01442     int comple;
01443     int resT, resE, res, retval;
01444     char **slot;
01445     MarkCacheKey *key;
01446 
01447     one = DD_ONE(dd);
01448     zero = Cudd_Not(one);
01449 
01450     /* Terminal cases. */
01451     if (c == zero) return(DD_LIC_DC);
01452     if (f == one)  return(DD_LIC_1);
01453     if (f == zero) return(DD_LIC_0);
01454 
01455     /* Make canonical to increase the utilization of the cache. */
01456     comple = Cudd_IsComplement(f);
01457     f = Cudd_Regular(f);
01458     /* Now f is a regular pointer to a non-constant node; c may be
01459     ** constant, or it may be complemented.
01460     */
01461 
01462     /* Check the cache. */
01463     key = ALLOC(MarkCacheKey, 1);
01464     if (key == NULL) {
01465         dd->errorCode = CUDD_MEMORY_OUT;
01466         return(CUDD_OUT_OF_MEM);
01467     }
01468     key->f = f; key->c = c;
01469     if (st_lookup(cache, (char *)key, (char **)&res)) {
01470         FREE(key);
01471         if (comple) {
01472             if (res == DD_LIC_0) res = DD_LIC_1;
01473             else if (res == DD_LIC_1) res = DD_LIC_0;
01474         }
01475         return(res);
01476     }
01477 
01478     /* Recursive step. */
01479     topf = dd->perm[f->index];
01480     topc = cuddI(dd,Cudd_Regular(c)->index);
01481     if (topf <= topc) {
01482         index = f->index;
01483         Fv = cuddT(f); Fnv = cuddE(f);
01484     } else {
01485         index = Cudd_Regular(c)->index;
01486         Fv = Fnv = f;
01487     }
01488     if (topc <= topf) {
01489         /* We know that c is not constant because f is not. */
01490         Cv = cuddT(Cudd_Regular(c)); Cnv = cuddE(Cudd_Regular(c));
01491         if (Cudd_IsComplement(c)) {
01492             Cv = Cudd_Not(Cv);
01493             Cnv = Cudd_Not(Cnv);
01494         }
01495     } else {
01496         Cv = Cnv = c;
01497     }
01498 
01499     resT = cuddBddLICMarkEdges(dd, Fv, Cv, table, cache);
01500     if (resT == CUDD_OUT_OF_MEM) {
01501         FREE(key);
01502         return(CUDD_OUT_OF_MEM);
01503     }
01504     resE = cuddBddLICMarkEdges(dd, Fnv, Cnv, table, cache);
01505     if (resE == CUDD_OUT_OF_MEM) {
01506         FREE(key);
01507         return(CUDD_OUT_OF_MEM);
01508     }
01509 
01510     /* Update edge markings. */
01511     if (topf <= topc) {
01512         retval = st_find_or_add(table, (char *)f, (char ***)&slot);
01513         if (retval == 0) {
01514             *slot = (char *) (ptrint)((resT << 2) | resE);
01515         } else if (retval == 1) {
01516             *slot = (char *) (ptrint)((int)((ptrint) *slot) | (resT << 2) | resE);
01517         } else {
01518             FREE(key);
01519             return(CUDD_OUT_OF_MEM);
01520         }
01521     }
01522 
01523     /* Cache result. */
01524     res = resT | resE;
01525     if (st_insert(cache, (char *)key, (char *)(ptrint)res) == ST_OUT_OF_MEM) {
01526         FREE(key);
01527         return(CUDD_OUT_OF_MEM);
01528     }
01529 
01530     /* Take into account possible complementation. */
01531     if (comple) {
01532         if (res == DD_LIC_0) res = DD_LIC_1;
01533         else if (res == DD_LIC_1) res = DD_LIC_0;
01534     }
01535     return(res);
01536 
01537 } /* end of cuddBddLICMarkEdges */
01538 
01539 
01552 static DdNode *
01553 cuddBddLICBuildResult(
01554   DdManager * dd,
01555   DdNode * f,
01556   st_table * cache,
01557   st_table * table)
01558 {
01559     DdNode *Fv, *Fnv, *r, *t, *e;
01560     DdNode *one, *zero;
01561     unsigned int topf;
01562     int index;
01563     int comple;
01564     int markT, markE, markings;
01565 
01566     one = DD_ONE(dd);
01567     zero = Cudd_Not(one);
01568 
01569     if (Cudd_IsConstant(f)) return(f);
01570     /* Make canonical to increase the utilization of the cache. */
01571     comple = Cudd_IsComplement(f);
01572     f = Cudd_Regular(f);
01573 
01574     /* Check the cache. */
01575     if (st_lookup(cache, (char *)f, (char **)&r)) {
01576         return(Cudd_NotCond(r,comple));
01577     }
01578 
01579     /* Retrieve the edge markings. */
01580     if (st_lookup(table, (char *)f, (char **)&markings) == 0)
01581         return(NULL);
01582     markT = markings >> 2;
01583     markE = markings & 3;
01584 
01585     topf = dd->perm[f->index];
01586     index = f->index;
01587     Fv = cuddT(f); Fnv = cuddE(f);
01588 
01589     if (markT == DD_LIC_NL) {
01590         t = cuddBddLICBuildResult(dd,Fv,cache,table);
01591         if (t == NULL) {
01592             return(NULL);
01593         }
01594     } else if (markT == DD_LIC_1) {
01595         t = one;
01596     } else {
01597         t = zero;
01598     }
01599     cuddRef(t);
01600     if (markE == DD_LIC_NL) {
01601         e = cuddBddLICBuildResult(dd,Fnv,cache,table);
01602         if (e == NULL) {
01603             Cudd_IterDerefBdd(dd,t);
01604             return(NULL);
01605         }
01606     } else if (markE == DD_LIC_1) {
01607         e = one;
01608     } else {
01609         e = zero;
01610     }
01611     cuddRef(e);
01612 
01613     if (markT == DD_LIC_DC && markE != DD_LIC_DC) {
01614         r = e;
01615     } else if (markT != DD_LIC_DC && markE == DD_LIC_DC) {
01616         r = t;
01617     } else {
01618         if (Cudd_IsComplement(t)) {
01619             t = Cudd_Not(t);
01620             e = Cudd_Not(e);
01621             r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
01622             if (r == NULL) {
01623                 Cudd_IterDerefBdd(dd, e);
01624                 Cudd_IterDerefBdd(dd, t);
01625                 return(NULL);
01626             }
01627             r = Cudd_Not(r);
01628         } else {
01629             r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
01630             if (r == NULL) {
01631                 Cudd_IterDerefBdd(dd, e);
01632                 Cudd_IterDerefBdd(dd, t);
01633                 return(NULL);
01634             }
01635         }
01636     }
01637     cuddDeref(t);
01638     cuddDeref(e);
01639 
01640     if (st_insert(cache, (char *)f, (char *)r) == ST_OUT_OF_MEM) {
01641         cuddRef(r);
01642         Cudd_IterDerefBdd(dd,r);
01643         return(NULL);
01644     }
01645 
01646     return(Cudd_NotCond(r,comple));
01647 
01648 } /* end of cuddBddLICBuildResult */
01649 
01650 
01663 static int
01664 MarkCacheHash(
01665   char * ptr,
01666   int  modulus)
01667 {
01668     int val = 0;
01669     MarkCacheKey *entry;
01670 
01671     entry = (MarkCacheKey *) ptr;
01672 
01673     val = (int) (ptrint) entry->f;
01674     val = val * 997 + (int) (ptrint) entry->c;
01675 
01676     return ((val < 0) ? -val : val) % modulus;
01677 
01678 } /* end of MarkCacheHash */
01679 
01680 
01695 static int
01696 MarkCacheCompare(
01697   const char * ptr1,
01698   const char * ptr2)
01699 {
01700     MarkCacheKey *entry1, *entry2;
01701 
01702     entry1 = (MarkCacheKey *) ptr1;
01703     entry2 = (MarkCacheKey *) ptr2;
01704     
01705     return((entry1->f != entry2->f) || (entry1->c != entry2->c));
01706 
01707 } /* end of MarkCacheCompare */
01708 
01709 
01710 
01724 static enum st_retval
01725 MarkCacheCleanUp(
01726   char * key,
01727   char * value,
01728   char * arg)
01729 {
01730     MarkCacheKey *entry;
01731 
01732     entry = (MarkCacheKey *) key;
01733     FREE(entry);
01734     return ST_CONTINUE;
01735 
01736 } /* end of MarkCacheCleanUp */
01737 
01738 
01755 static DdNode *
01756 cuddBddSqueeze(
01757   DdManager * dd,
01758   DdNode * l,
01759   DdNode * u)
01760 {
01761     DdNode *one, *zero, *r, *lt, *le, *ut, *ue, *t, *e;
01762 #if 0
01763     DdNode *ar;
01764 #endif
01765     int comple = 0;
01766     unsigned int topu, topl;
01767     int index;
01768 
01769     statLine(dd);
01770     if (l == u) {
01771         return(l);
01772     }
01773     one = DD_ONE(dd);
01774     zero = Cudd_Not(one);
01775     /* The only case when l == zero && u == one is at the top level,
01776     ** where returning either one or zero is OK. In all other cases
01777     ** the procedure will detect such a case and will perform
01778     ** remapping. Therefore the order in which we test l and u at this
01779     ** point is immaterial. */
01780     if (l == zero) return(l);
01781     if (u == one)  return(u);
01782 
01783     /* Make canonical to increase the utilization of the cache. */
01784     if (Cudd_IsComplement(u)) {
01785         DdNode *temp;
01786         temp = Cudd_Not(l);
01787         l = Cudd_Not(u);
01788         u = temp;
01789         comple = 1;
01790     }
01791     /* At this point u is regular and non-constant; l is non-constant, but
01792     ** may be complemented. */
01793 
01794     /* Here we could check the relative sizes. */
01795 
01796     /* Check the cache. */
01797     r = cuddCacheLookup2(dd, Cudd_bddSqueeze, l, u);
01798     if (r != NULL) {
01799         return(Cudd_NotCond(r,comple));
01800     }
01801 
01802     /* Recursive step. */
01803     topu = dd->perm[u->index];
01804     topl = dd->perm[Cudd_Regular(l)->index];
01805     if (topu <= topl) {
01806         index = u->index;
01807         ut = cuddT(u); ue = cuddE(u);
01808     } else {
01809         index = Cudd_Regular(l)->index;
01810         ut = ue = u;
01811     }
01812     if (topl <= topu) {
01813         lt = cuddT(Cudd_Regular(l)); le = cuddE(Cudd_Regular(l));
01814         if (Cudd_IsComplement(l)) {
01815             lt = Cudd_Not(lt);
01816             le = Cudd_Not(le);
01817         }
01818     } else {
01819         lt = le = l;
01820     }
01821 
01822     /* If one interval is contained in the other, use the smaller
01823     ** interval. This corresponds to one-sided matching. */
01824     if ((lt == zero || Cudd_bddLeq(dd,lt,le)) &&
01825         (ut == one  || Cudd_bddLeq(dd,ue,ut))) { /* remap */
01826         r = cuddBddSqueeze(dd, le, ue);
01827         if (r == NULL)
01828             return(NULL);
01829         return(Cudd_NotCond(r,comple));
01830     } else if ((le == zero || Cudd_bddLeq(dd,le,lt)) &&
01831                (ue == one  || Cudd_bddLeq(dd,ut,ue))) { /* remap */
01832         r = cuddBddSqueeze(dd, lt, ut);
01833         if (r == NULL)
01834             return(NULL);
01835         return(Cudd_NotCond(r,comple));
01836     } else if ((le == zero || Cudd_bddLeq(dd,le,Cudd_Not(ut))) &&
01837                (ue == one  || Cudd_bddLeq(dd,Cudd_Not(lt),ue))) { /* c-remap */
01838         t = cuddBddSqueeze(dd, lt, ut);
01839         cuddRef(t);
01840         if (Cudd_IsComplement(t)) {
01841             r = cuddUniqueInter(dd, index, Cudd_Not(t), t);
01842             if (r == NULL) {
01843                 Cudd_IterDerefBdd(dd, t);
01844                 return(NULL);
01845             }
01846             r = Cudd_Not(r);
01847         } else {
01848             r = cuddUniqueInter(dd, index, t, Cudd_Not(t));
01849             if (r == NULL) {
01850                 Cudd_IterDerefBdd(dd, t);
01851                 return(NULL);
01852             }
01853         }
01854         cuddDeref(t);
01855         if (r == NULL)
01856             return(NULL);
01857         cuddCacheInsert2(dd, Cudd_bddSqueeze, l, u, r);
01858         return(Cudd_NotCond(r,comple));
01859     } else if ((lt == zero || Cudd_bddLeq(dd,lt,Cudd_Not(ue))) &&
01860                (ut == one  || Cudd_bddLeq(dd,Cudd_Not(le),ut))) { /* c-remap */
01861         e = cuddBddSqueeze(dd, le, ue);
01862         cuddRef(e);
01863         if (Cudd_IsComplement(e)) {
01864             r = cuddUniqueInter(dd, index, Cudd_Not(e), e);
01865             if (r == NULL) {
01866                 Cudd_IterDerefBdd(dd, e);
01867                 return(NULL);
01868             }
01869         } else {
01870             r = cuddUniqueInter(dd, index, e, Cudd_Not(e));
01871             if (r == NULL) {
01872                 Cudd_IterDerefBdd(dd, e);
01873                 return(NULL);
01874             }
01875             r = Cudd_Not(r);
01876         }
01877         cuddDeref(e);
01878         if (r == NULL)
01879             return(NULL);
01880         cuddCacheInsert2(dd, Cudd_bddSqueeze, l, u, r);
01881         return(Cudd_NotCond(r,comple));
01882     }
01883 
01884 #if 0
01885     /* If the two intervals intersect, take a solution from
01886     ** the intersection of the intervals. This guarantees that the
01887     ** splitting variable will not appear in the result.
01888     ** This approach corresponds to two-sided matching, and is very
01889     ** expensive. */
01890     if (Cudd_bddLeq(dd,lt,ue) && Cudd_bddLeq(dd,le,ut)) {
01891         DdNode *au, *al;
01892         au = cuddBddAndRecur(dd,ut,ue);
01893         if (au == NULL)
01894             return(NULL);
01895         cuddRef(au);
01896         al = cuddBddAndRecur(dd,Cudd_Not(lt),Cudd_Not(le));
01897         if (al == NULL) {
01898             Cudd_IterDerefBdd(dd,au);
01899             return(NULL);
01900         }
01901         cuddRef(al);
01902         al = Cudd_Not(al);
01903         ar = cuddBddSqueeze(dd, al, au);
01904         if (ar == NULL) {
01905             Cudd_IterDerefBdd(dd,au);
01906             Cudd_IterDerefBdd(dd,al);
01907             return(NULL);
01908         }
01909         cuddRef(ar);
01910         Cudd_IterDerefBdd(dd,au);
01911         Cudd_IterDerefBdd(dd,al);
01912     } else {
01913         ar = NULL;
01914     }
01915 #endif
01916 
01917     t = cuddBddSqueeze(dd, lt, ut);
01918     if (t == NULL) {
01919         return(NULL);
01920     }
01921     cuddRef(t);
01922     e = cuddBddSqueeze(dd, le, ue);
01923     if (e == NULL) {
01924         Cudd_IterDerefBdd(dd,t);
01925         return(NULL);
01926     }
01927     cuddRef(e);
01928 
01929     if (Cudd_IsComplement(t)) {
01930         t = Cudd_Not(t);
01931         e = Cudd_Not(e);
01932         r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
01933         if (r == NULL) {
01934             Cudd_IterDerefBdd(dd, e);
01935             Cudd_IterDerefBdd(dd, t);
01936             return(NULL);
01937         }
01938         r = Cudd_Not(r);
01939     } else {
01940         r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
01941         if (r == NULL) {
01942             Cudd_IterDerefBdd(dd, e);
01943             Cudd_IterDerefBdd(dd, t);
01944             return(NULL);
01945         }
01946     }
01947     cuddDeref(t);
01948     cuddDeref(e);
01949 
01950 #if 0
01951     /* Check whether there is a result obtained by abstraction and whether
01952     ** it is better than the one obtained by recursion. */
01953     cuddRef(r);
01954     if (ar != NULL) {
01955         if (Cudd_DagSize(ar) <= Cudd_DagSize(r)) {
01956             Cudd_IterDerefBdd(dd, r);
01957             r = ar;
01958         } else {
01959             Cudd_IterDerefBdd(dd, ar);
01960         }
01961     }
01962     cuddDeref(r);
01963 #endif
01964 
01965     cuddCacheInsert2(dd, Cudd_bddSqueeze, l, u, r);
01966     return(Cudd_NotCond(r,comple));
01967 
01968 } /* end of cuddBddSqueeze */