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

00001 
00078 #include "util.h"
00079 #include "cuddInt.h"
00080 
00081 
00082 /*---------------------------------------------------------------------------*/
00083 /* Constant declarations                                                     */
00084 /*---------------------------------------------------------------------------*/
00085 
00086 /* Codes for edge markings in Cudd_bddLICompaction.  The codes are defined
00087 ** so that they can be bitwise ORed to implement the code priority scheme.
00088 */
00089 #define DD_LIC_DC 0
00090 #define DD_LIC_1  1
00091 #define DD_LIC_0  2
00092 #define DD_LIC_NL 3
00093 
00094 /*---------------------------------------------------------------------------*/
00095 /* Stucture declarations                                                     */
00096 /*---------------------------------------------------------------------------*/
00097 
00098 
00099 /*---------------------------------------------------------------------------*/
00100 /* Type declarations                                                         */
00101 /*---------------------------------------------------------------------------*/
00102 
00103 /* Key for the cache used in the edge marking phase. */
00104 typedef struct MarkCacheKey {
00105     DdNode *f;
00106     DdNode *c;
00107 } MarkCacheKey;
00108 
00109 /*---------------------------------------------------------------------------*/
00110 /* Variable declarations                                                     */
00111 /*---------------------------------------------------------------------------*/
00112 
00113 #ifndef lint
00114 static char rcsid[] DD_UNUSED = "$Id: cuddGenCof.c,v 1.38 2005/05/14 17:27:11 fabio Exp $";
00115 #endif
00116 
00117 /*---------------------------------------------------------------------------*/
00118 /* Macro declarations                                                        */
00119 /*---------------------------------------------------------------------------*/
00120 
00121 #ifdef __cplusplus
00122 extern "C" {
00123 #endif
00124 
00127 /*---------------------------------------------------------------------------*/
00128 /* Static function prototypes                                                */
00129 /*---------------------------------------------------------------------------*/
00130 
00131 static int cuddBddConstrainDecomp (DdManager *dd, DdNode *f, DdNode **decomp);
00132 static DdNode * cuddBddCharToVect (DdManager *dd, DdNode *f, DdNode *x);
00133 static int cuddBddLICMarkEdges (DdManager *dd, DdNode *f, DdNode *c, st_table *table, st_table *cache);
00134 static DdNode * cuddBddLICBuildResult (DdManager *dd, DdNode *f, st_table *cache, st_table *table);
00135 static int MarkCacheHash (char *ptr, int modulus);
00136 static int MarkCacheCompare (const char *ptr1, const char *ptr2);
00137 static enum st_retval MarkCacheCleanUp (char *key, char *value, char *arg);
00138 static DdNode * cuddBddSqueeze (DdManager *dd, DdNode *l, DdNode *u);
00139 
00142 #ifdef __cplusplus
00143 }
00144 #endif
00145 
00146 /*---------------------------------------------------------------------------*/
00147 /* Definition of exported functions                                          */
00148 /*---------------------------------------------------------------------------*/
00149 
00150 
00175 DdNode *
00176 Cudd_bddConstrain(
00177   DdManager * dd,
00178   DdNode * f,
00179   DdNode * c)
00180 {
00181     DdNode *res;
00182 
00183     do {
00184         dd->reordered = 0;
00185         res = cuddBddConstrainRecur(dd,f,c);
00186     } while (dd->reordered == 1);
00187     return(res);
00188 
00189 } /* end of Cudd_bddConstrain */
00190 
00191 
00207 DdNode *
00208 Cudd_bddRestrict(
00209   DdManager * dd,
00210   DdNode * f,
00211   DdNode * c)
00212 {
00213     DdNode *suppF, *suppC, *commonSupport;
00214     DdNode *cplus, *res;
00215     int retval;
00216     int sizeF, sizeRes;
00217 
00218     /* Check terminal cases here to avoid computing supports in trivial cases.
00219     ** This also allows us notto check later for the case c == 0, in which
00220     ** there is no common support. */
00221     if (c == Cudd_Not(DD_ONE(dd))) return(Cudd_Not(DD_ONE(dd)));
00222     if (Cudd_IsConstant(f)) return(f);
00223     if (f == c) return(DD_ONE(dd));
00224     if (f == Cudd_Not(c)) return(Cudd_Not(DD_ONE(dd)));
00225 
00226     /* Check if supports intersect. */
00227     retval = Cudd_ClassifySupport(dd,f,c,&commonSupport,&suppF,&suppC);
00228     if (retval == 0) {
00229         return(NULL);
00230     }
00231     cuddRef(commonSupport); cuddRef(suppF); cuddRef(suppC);
00232     Cudd_IterDerefBdd(dd,suppF);
00233 
00234     if (commonSupport == DD_ONE(dd)) {
00235         Cudd_IterDerefBdd(dd,commonSupport);
00236         Cudd_IterDerefBdd(dd,suppC);
00237         return(f);
00238     }
00239     Cudd_IterDerefBdd(dd,commonSupport);
00240 
00241     /* Abstract from c the variables that do not appear in f. */
00242     cplus = Cudd_bddExistAbstract(dd, c, suppC);
00243     if (cplus == NULL) {
00244         Cudd_IterDerefBdd(dd,suppC);
00245         return(NULL);
00246     }
00247     cuddRef(cplus);
00248     Cudd_IterDerefBdd(dd,suppC);
00249 
00250     do {
00251         dd->reordered = 0;
00252         res = cuddBddRestrictRecur(dd, f, cplus);
00253     } while (dd->reordered == 1);
00254     if (res == NULL) {
00255         Cudd_IterDerefBdd(dd,cplus);
00256         return(NULL);
00257     }
00258     cuddRef(res);
00259     Cudd_IterDerefBdd(dd,cplus);
00260     /* Make restric safe by returning the smaller of the input and the
00261     ** result. */
00262     sizeF = Cudd_DagSize(f);
00263     sizeRes = Cudd_DagSize(res);
00264     if (sizeF <= sizeRes) {
00265         Cudd_IterDerefBdd(dd, res);
00266         return(f);
00267     } else {
00268         cuddDeref(res);
00269         return(res);
00270     }
00271 
00272 } /* end of Cudd_bddRestrict */
00273 
00274 
00294 DdNode *
00295 Cudd_bddNPAnd(
00296   DdManager * dd,
00297   DdNode * f,
00298   DdNode * g)
00299 {
00300     DdNode *res;
00301 
00302     do {
00303         dd->reordered = 0;
00304         res = cuddBddNPAndRecur(dd,f,g);
00305     } while (dd->reordered == 1);
00306     return(res);
00307 
00308 } /* end of Cudd_bddNPAnd */
00309 
00310 
00331 DdNode *
00332 Cudd_addConstrain(
00333   DdManager * dd,
00334   DdNode * f,
00335   DdNode * c)
00336 {
00337     DdNode *res;
00338 
00339     do {
00340         dd->reordered = 0;
00341         res = cuddAddConstrainRecur(dd,f,c);
00342     } while (dd->reordered == 1);
00343     return(res);
00344 
00345 } /* end of Cudd_addConstrain */
00346 
00347 
00366 DdNode **
00367 Cudd_bddConstrainDecomp(
00368   DdManager * dd,
00369   DdNode * f)
00370 {
00371     DdNode **decomp;
00372     int res;
00373     int i;
00374 
00375     /* Create an initialize decomposition array. */
00376     decomp = ALLOC(DdNode *,dd->size);
00377     if (decomp == NULL) {
00378         dd->errorCode = CUDD_MEMORY_OUT;
00379         return(NULL);
00380     }
00381     for (i = 0; i < dd->size; i++) {
00382         decomp[i] = NULL;
00383     }
00384     do {
00385         dd->reordered = 0;
00386         /* Clean up the decomposition array in case reordering took place. */
00387         for (i = 0; i < dd->size; i++) {
00388             if (decomp[i] != NULL) {
00389                 Cudd_IterDerefBdd(dd, decomp[i]);
00390                 decomp[i] = NULL;
00391             }
00392         }
00393         res = cuddBddConstrainDecomp(dd,f,decomp);
00394     } while (dd->reordered == 1);
00395     if (res == 0) {
00396         FREE(decomp);
00397         return(NULL);
00398     }
00399     /* Missing components are constant ones. */
00400     for (i = 0; i < dd->size; i++) {
00401         if (decomp[i] == NULL) {
00402             decomp[i] = DD_ONE(dd);
00403             cuddRef(decomp[i]);
00404         }
00405     }
00406     return(decomp);
00407 
00408 } /* end of Cudd_bddConstrainDecomp */
00409 
00410 
00426 DdNode *
00427 Cudd_addRestrict(
00428   DdManager * dd,
00429   DdNode * f,
00430   DdNode * c)
00431 {
00432     DdNode *supp_f, *supp_c;
00433     DdNode *res, *commonSupport;
00434     int intersection;
00435     int sizeF, sizeRes;
00436 
00437     /* Check if supports intersect. */
00438     supp_f = Cudd_Support(dd, f);
00439     if (supp_f == NULL) {
00440         return(NULL);
00441     }
00442     cuddRef(supp_f);
00443     supp_c = Cudd_Support(dd, c);
00444     if (supp_c == NULL) {
00445         Cudd_RecursiveDeref(dd,supp_f);
00446         return(NULL);
00447     }
00448     cuddRef(supp_c);
00449     commonSupport = Cudd_bddLiteralSetIntersection(dd, supp_f, supp_c);
00450     if (commonSupport == NULL) {
00451         Cudd_RecursiveDeref(dd,supp_f);
00452         Cudd_RecursiveDeref(dd,supp_c);
00453         return(NULL);
00454     }
00455     cuddRef(commonSupport);
00456     Cudd_RecursiveDeref(dd,supp_f);
00457     Cudd_RecursiveDeref(dd,supp_c);
00458     intersection = commonSupport != DD_ONE(dd);
00459     Cudd_RecursiveDeref(dd,commonSupport);
00460 
00461     if (intersection) {
00462         do {
00463             dd->reordered = 0;
00464             res = cuddAddRestrictRecur(dd, f, c);
00465         } while (dd->reordered == 1);
00466         sizeF = Cudd_DagSize(f);
00467         sizeRes = Cudd_DagSize(res);
00468         if (sizeF <= sizeRes) {
00469             cuddRef(res);
00470             Cudd_RecursiveDeref(dd, res);
00471             return(f);
00472         } else {
00473             return(res);
00474         }
00475     } else {
00476         return(f);
00477     }
00478 
00479 } /* end of Cudd_addRestrict */
00480 
00481 
00505 DdNode **
00506 Cudd_bddCharToVect(
00507   DdManager * dd,
00508   DdNode * f)
00509 {
00510     int i, j;
00511     DdNode **vect;
00512     DdNode *res = NULL;
00513 
00514     if (f == Cudd_Not(DD_ONE(dd))) return(NULL);
00515 
00516     vect = ALLOC(DdNode *, dd->size);
00517     if (vect == NULL) {
00518         dd->errorCode = CUDD_MEMORY_OUT;
00519         return(NULL);
00520     }
00521 
00522     do {
00523         dd->reordered = 0;
00524         for (i = 0; i < dd->size; i++) {
00525             res = cuddBddCharToVect(dd,f,dd->vars[dd->invperm[i]]);
00526             if (res == NULL) {
00527                 /* Clean up the vector array in case reordering took place. */
00528                 for (j = 0; j < i; j++) {
00529                     Cudd_IterDerefBdd(dd, vect[dd->invperm[j]]);
00530                 }
00531                 break;
00532             }
00533             cuddRef(res);
00534             vect[dd->invperm[i]] = res;
00535         }
00536     } while (dd->reordered == 1);
00537     if (res == NULL) {
00538         FREE(vect);
00539         return(NULL);
00540     }
00541     return(vect);
00542 
00543 } /* end of Cudd_bddCharToVect */
00544 
00545 
00565 DdNode *
00566 Cudd_bddLICompaction(
00567   DdManager * dd /* manager */,
00568   DdNode * f /* function to be minimized */,
00569   DdNode * c /* constraint (care set) */)
00570 {
00571     DdNode *res;
00572 
00573     do {
00574         dd->reordered = 0;
00575         res = cuddBddLICompaction(dd,f,c);
00576     } while (dd->reordered == 1);
00577     return(res);
00578 
00579 } /* end of Cudd_bddLICompaction */
00580 
00581 
00597 DdNode *
00598 Cudd_bddSqueeze(
00599   DdManager * dd /* manager */,
00600   DdNode * l /* lower bound */,
00601   DdNode * u /* upper bound */)
00602 {
00603     DdNode *res;
00604     int sizeRes, sizeL, sizeU;
00605 
00606     do {
00607         dd->reordered = 0;
00608         res = cuddBddSqueeze(dd,l,u);
00609     } while (dd->reordered == 1);
00610     if (res == NULL) return(NULL);
00611     /* We now compare the result with the bounds and return the smallest.
00612     ** We first compare to u, so that in case l == 0 and u == 1, we return
00613     ** 0 as in other minimization algorithms. */
00614     sizeRes = Cudd_DagSize(res);
00615     sizeU = Cudd_DagSize(u);
00616     if (sizeU <= sizeRes) {
00617         cuddRef(res);
00618         Cudd_IterDerefBdd(dd,res);
00619         res = u;
00620         sizeRes = sizeU;
00621     }
00622     sizeL = Cudd_DagSize(l);
00623     if (sizeL <= sizeRes) {
00624         cuddRef(res);
00625         Cudd_IterDerefBdd(dd,res);
00626         res = l;
00627         sizeRes = sizeL;
00628     }
00629     return(res);
00630 
00631 } /* end of Cudd_bddSqueeze */
00632 
00633 
00648 DdNode *
00649 Cudd_bddMinimize(
00650   DdManager * dd,
00651   DdNode * f,
00652   DdNode * c)
00653 {
00654     DdNode *cplus, *res;
00655 
00656     if (c == Cudd_Not(DD_ONE(dd))) return(c);
00657     if (Cudd_IsConstant(f)) return(f);
00658     if (f == c) return(DD_ONE(dd));
00659     if (f == Cudd_Not(c)) return(Cudd_Not(DD_ONE(dd)));
00660 
00661     cplus = Cudd_RemapOverApprox(dd,c,0,0,1.0);
00662     if (cplus == NULL) return(NULL);
00663     cuddRef(cplus);
00664     res = Cudd_bddLICompaction(dd,f,cplus);
00665     if (res == NULL) {
00666         Cudd_IterDerefBdd(dd,cplus);
00667         return(NULL);
00668     }
00669     cuddRef(res);
00670     Cudd_IterDerefBdd(dd,cplus);
00671     cuddDeref(res);
00672     return(res);
00673 
00674 } /* end of Cudd_bddMinimize */
00675 
00676 
00695 DdNode *
00696 Cudd_SubsetCompress(
00697   DdManager * dd /* manager */,
00698   DdNode * f /* BDD whose subset is sought */,
00699   int  nvars /* number of variables in the support of f */,
00700   int  threshold /* maximum number of nodes in the subset */)
00701 {
00702     DdNode *res, *tmp1, *tmp2;
00703 
00704     tmp1 = Cudd_SubsetShortPaths(dd, f, nvars, threshold, 0);
00705     if (tmp1 == NULL) return(NULL);
00706     cuddRef(tmp1);
00707     tmp2 = Cudd_RemapUnderApprox(dd,tmp1,nvars,0,1.0);
00708     if (tmp2 == NULL) {
00709         Cudd_IterDerefBdd(dd,tmp1);
00710         return(NULL);
00711     }
00712     cuddRef(tmp2);
00713     Cudd_IterDerefBdd(dd,tmp1);
00714     res = Cudd_bddSqueeze(dd,tmp2,f);
00715     if (res == NULL) {
00716         Cudd_IterDerefBdd(dd,tmp2);
00717         return(NULL);
00718     }
00719     cuddRef(res);
00720     Cudd_IterDerefBdd(dd,tmp2);
00721     cuddDeref(res);
00722     return(res);
00723 
00724 } /* end of Cudd_SubsetCompress */
00725 
00726 
00745 DdNode *
00746 Cudd_SupersetCompress(
00747   DdManager * dd /* manager */,
00748   DdNode * f /* BDD whose superset is sought */,
00749   int  nvars /* number of variables in the support of f */,
00750   int  threshold /* maximum number of nodes in the superset */)
00751 {
00752     DdNode *subset;
00753 
00754     subset = Cudd_SubsetCompress(dd, Cudd_Not(f),nvars,threshold);
00755 
00756     return(Cudd_NotCond(subset, (subset != NULL)));
00757 
00758 } /* end of Cudd_SupersetCompress */
00759 
00760 
00761 /*---------------------------------------------------------------------------*/
00762 /* Definition of internal functions                                          */
00763 /*---------------------------------------------------------------------------*/
00764 
00765 
00778 DdNode *
00779 cuddBddConstrainRecur(
00780   DdManager * dd,
00781   DdNode * f,
00782   DdNode * c)
00783 {
00784     DdNode       *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r;
00785     DdNode       *one, *zero;
00786     unsigned int topf, topc;
00787     int          index;
00788     int          comple = 0;
00789 
00790     statLine(dd);
00791     one = DD_ONE(dd);
00792     zero = Cudd_Not(one);
00793 
00794     /* Trivial cases. */
00795     if (c == one)               return(f);
00796     if (c == zero)              return(zero);
00797     if (Cudd_IsConstant(f))     return(f);
00798     if (f == c)                 return(one);
00799     if (f == Cudd_Not(c))       return(zero);
00800 
00801     /* Make canonical to increase the utilization of the cache. */
00802     if (Cudd_IsComplement(f)) {
00803         f = Cudd_Not(f);
00804         comple = 1;
00805     }
00806     /* Now f is a regular pointer to a non-constant node; c is also
00807     ** non-constant, but may be complemented.
00808     */
00809 
00810     /* Check the cache. */
00811     r = cuddCacheLookup2(dd, Cudd_bddConstrain, f, c);
00812     if (r != NULL) {
00813         return(Cudd_NotCond(r,comple));
00814     }
00815     
00816     /* Recursive step. */
00817     topf = dd->perm[f->index];
00818     topc = dd->perm[Cudd_Regular(c)->index];
00819     if (topf <= topc) {
00820         index = f->index;
00821         Fv = cuddT(f); Fnv = cuddE(f);
00822     } else {
00823         index = Cudd_Regular(c)->index;
00824         Fv = Fnv = f;
00825     }
00826     if (topc <= topf) {
00827         Cv = cuddT(Cudd_Regular(c)); Cnv = cuddE(Cudd_Regular(c));
00828         if (Cudd_IsComplement(c)) {
00829             Cv = Cudd_Not(Cv);
00830             Cnv = Cudd_Not(Cnv);
00831         }
00832     } else {
00833         Cv = Cnv = c;
00834     }
00835 
00836     if (!Cudd_IsConstant(Cv)) {
00837         t = cuddBddConstrainRecur(dd, Fv, Cv);
00838         if (t == NULL)
00839             return(NULL);
00840     } else if (Cv == one) {
00841         t = Fv;
00842     } else {            /* Cv == zero: return Fnv @ Cnv */
00843         if (Cnv == one) {
00844             r = Fnv;
00845         } else {
00846             r = cuddBddConstrainRecur(dd, Fnv, Cnv);
00847             if (r == NULL)
00848                 return(NULL);
00849         }
00850         return(Cudd_NotCond(r,comple));
00851     }
00852     cuddRef(t);
00853 
00854     if (!Cudd_IsConstant(Cnv)) {
00855         e = cuddBddConstrainRecur(dd, Fnv, Cnv);
00856         if (e == NULL) {
00857             Cudd_IterDerefBdd(dd, t);
00858             return(NULL);
00859         }
00860     } else if (Cnv == one) {
00861         e = Fnv;
00862     } else {            /* Cnv == zero: return Fv @ Cv previously computed */
00863         cuddDeref(t);
00864         return(Cudd_NotCond(t,comple));
00865     }
00866     cuddRef(e);
00867 
00868     if (Cudd_IsComplement(t)) {
00869         t = Cudd_Not(t);
00870         e = Cudd_Not(e);
00871         r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
00872         if (r == NULL) {
00873             Cudd_IterDerefBdd(dd, e);
00874             Cudd_IterDerefBdd(dd, t);
00875             return(NULL);
00876         }
00877         r = Cudd_Not(r);
00878     } else {
00879         r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
00880         if (r == NULL) {
00881             Cudd_IterDerefBdd(dd, e);
00882             Cudd_IterDerefBdd(dd, t);
00883             return(NULL);
00884         }
00885     }
00886     cuddDeref(t);
00887     cuddDeref(e);
00888 
00889     cuddCacheInsert2(dd, Cudd_bddConstrain, f, c, r);
00890     return(Cudd_NotCond(r,comple));
00891 
00892 } /* end of cuddBddConstrainRecur */
00893 
00894 
00907 DdNode *
00908 cuddBddRestrictRecur(
00909   DdManager * dd,
00910   DdNode * f,
00911   DdNode * c)
00912 {
00913     DdNode       *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r, *one, *zero;
00914     unsigned int topf, topc;
00915     int          index;
00916     int          comple = 0;
00917 
00918     statLine(dd);
00919     one = DD_ONE(dd);
00920     zero = Cudd_Not(one);
00921 
00922     /* Trivial cases */
00923     if (c == one)               return(f);
00924     if (c == zero)              return(zero);
00925     if (Cudd_IsConstant(f))     return(f);
00926     if (f == c)                 return(one);
00927     if (f == Cudd_Not(c))       return(zero);
00928 
00929     /* Make canonical to increase the utilization of the cache. */
00930     if (Cudd_IsComplement(f)) {
00931         f = Cudd_Not(f);
00932         comple = 1;
00933     }
00934     /* Now f is a regular pointer to a non-constant node; c is also
00935     ** non-constant, but may be complemented.
00936     */
00937 
00938     /* Check the cache. */
00939     r = cuddCacheLookup2(dd, Cudd_bddRestrict, f, c);
00940     if (r != NULL) {
00941         return(Cudd_NotCond(r,comple));
00942     }
00943 
00944     topf = dd->perm[f->index];
00945     topc = dd->perm[Cudd_Regular(c)->index];
00946 
00947     if (topc < topf) {  /* abstract top variable from c */
00948         DdNode *d, *s1, *s2;
00949 
00950         /* Find complements of cofactors of c. */
00951         if (Cudd_IsComplement(c)) {
00952             s1 = cuddT(Cudd_Regular(c));
00953             s2 = cuddE(Cudd_Regular(c));
00954         } else {
00955             s1 = Cudd_Not(cuddT(c));
00956             s2 = Cudd_Not(cuddE(c));
00957         }
00958         /* Take the OR by applying DeMorgan. */
00959         d = cuddBddAndRecur(dd, s1, s2);
00960         if (d == NULL) return(NULL);
00961         d = Cudd_Not(d);
00962         cuddRef(d);
00963         r = cuddBddRestrictRecur(dd, f, d);
00964         if (r == NULL) {
00965             Cudd_IterDerefBdd(dd, d);
00966             return(NULL);
00967         }
00968         cuddRef(r);
00969         Cudd_IterDerefBdd(dd, d);
00970         cuddCacheInsert2(dd, Cudd_bddRestrict, f, c, r);
00971         cuddDeref(r);
00972         return(Cudd_NotCond(r,comple));
00973     }
00974 
00975     /* Recursive step. Here topf <= topc. */
00976     index = f->index;
00977     Fv = cuddT(f); Fnv = cuddE(f);
00978     if (topc == topf) {
00979         Cv = cuddT(Cudd_Regular(c)); Cnv = cuddE(Cudd_Regular(c));
00980         if (Cudd_IsComplement(c)) {
00981             Cv = Cudd_Not(Cv);
00982             Cnv = Cudd_Not(Cnv);
00983         }
00984     } else {
00985         Cv = Cnv = c;
00986     }
00987 
00988     if (!Cudd_IsConstant(Cv)) {
00989         t = cuddBddRestrictRecur(dd, Fv, Cv);
00990         if (t == NULL) return(NULL);
00991     } else if (Cv == one) {
00992         t = Fv;
00993     } else {            /* Cv == zero: return(Fnv @ Cnv) */
00994         if (Cnv == one) {
00995             r = Fnv;
00996         } else {
00997             r = cuddBddRestrictRecur(dd, Fnv, Cnv);
00998             if (r == NULL) return(NULL);
00999         }
01000         return(Cudd_NotCond(r,comple));
01001     }
01002     cuddRef(t);
01003 
01004     if (!Cudd_IsConstant(Cnv)) {
01005         e = cuddBddRestrictRecur(dd, Fnv, Cnv);
01006         if (e == NULL) {
01007             Cudd_IterDerefBdd(dd, t);
01008             return(NULL);
01009         }
01010     } else if (Cnv == one) {
01011         e = Fnv;
01012     } else {            /* Cnv == zero: return (Fv @ Cv) previously computed */
01013         cuddDeref(t);
01014         return(Cudd_NotCond(t,comple));
01015     }
01016     cuddRef(e);
01017 
01018     if (Cudd_IsComplement(t)) {
01019         t = Cudd_Not(t);
01020         e = Cudd_Not(e);
01021         r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
01022         if (r == NULL) {
01023             Cudd_IterDerefBdd(dd, e);
01024             Cudd_IterDerefBdd(dd, t);
01025             return(NULL);
01026         }
01027         r = Cudd_Not(r);
01028     } else {
01029         r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
01030         if (r == NULL) {
01031             Cudd_IterDerefBdd(dd, e);
01032             Cudd_IterDerefBdd(dd, t);
01033             return(NULL);
01034         }
01035     }
01036     cuddDeref(t);
01037     cuddDeref(e);
01038 
01039     cuddCacheInsert2(dd, Cudd_bddRestrict, f, c, r);
01040     return(Cudd_NotCond(r,comple));
01041 
01042 } /* end of cuddBddRestrictRecur */
01043 
01044 
01057 DdNode *
01058 cuddBddNPAndRecur(
01059   DdManager * manager,
01060   DdNode * f,
01061   DdNode * g)
01062 {
01063     DdNode *F, *ft, *fe, *G, *gt, *ge;
01064     DdNode *one, *r, *t, *e;
01065     unsigned int topf, topg, index;
01066 
01067     statLine(manager);
01068     one = DD_ONE(manager);
01069 
01070     /* Terminal cases. */
01071     F = Cudd_Regular(f);
01072     G = Cudd_Regular(g);
01073     if (F == G) {
01074         if (f == g) return(one);
01075         else return(Cudd_Not(one));
01076     }
01077     if (G == one) {
01078         if (g == one) return(f);
01079         else return(g);
01080     }
01081     if (F == one) {
01082         return(f);
01083     }
01084 
01085     /* At this point f and g are not constant. */
01086     /* Check cache. */
01087     if (F->ref != 1 || G->ref != 1) {
01088         r = cuddCacheLookup2(manager, Cudd_bddNPAnd, f, g);
01089         if (r != NULL) return(r);
01090     }
01091 
01092     /* Here we can skip the use of cuddI, because the operands are known
01093     ** to be non-constant.
01094     */
01095     topf = manager->perm[F->index];
01096     topg = manager->perm[G->index];
01097 
01098     if (topg < topf) {  /* abstract top variable from g */
01099         DdNode *d;
01100 
01101         /* Find complements of cofactors of g. */
01102         if (Cudd_IsComplement(g)) {
01103             gt = cuddT(G);
01104             ge = cuddE(G);
01105         } else {
01106             gt = Cudd_Not(cuddT(g));
01107             ge = Cudd_Not(cuddE(g));
01108         }
01109         /* Take the OR by applying DeMorgan. */
01110         d = cuddBddAndRecur(manager, gt, ge);
01111         if (d == NULL) return(NULL);
01112         d = Cudd_Not(d);
01113         cuddRef(d);
01114         r = cuddBddNPAndRecur(manager, f, d);
01115         if (r == NULL) {
01116             Cudd_IterDerefBdd(manager, d);
01117             return(NULL);
01118         }
01119         cuddRef(r);
01120         Cudd_IterDerefBdd(manager, d);
01121         cuddCacheInsert2(manager, Cudd_bddNPAnd, f, g, r);
01122         cuddDeref(r);
01123         return(r);
01124     }
01125 
01126     /* Compute cofactors. */
01127     index = F->index;
01128     ft = cuddT(F);
01129     fe = cuddE(F);
01130     if (Cudd_IsComplement(f)) {
01131       ft = Cudd_Not(ft);
01132       fe = Cudd_Not(fe);
01133     }
01134 
01135     if (topg == topf) {
01136         gt = cuddT(G);
01137         ge = cuddE(G);
01138         if (Cudd_IsComplement(g)) {
01139             gt = Cudd_Not(gt);
01140             ge = Cudd_Not(ge);
01141         }
01142     } else {
01143         gt = ge = g;
01144     }
01145 
01146     t = cuddBddAndRecur(manager, ft, gt);
01147     if (t == NULL) return(NULL);
01148     cuddRef(t);
01149 
01150     e = cuddBddAndRecur(manager, fe, ge);
01151     if (e == NULL) {
01152         Cudd_IterDerefBdd(manager, t);
01153         return(NULL);
01154     }
01155     cuddRef(e);
01156 
01157     if (t == e) {
01158         r = t;
01159     } else {
01160         if (Cudd_IsComplement(t)) {
01161             r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
01162             if (r == NULL) {
01163                 Cudd_IterDerefBdd(manager, t);
01164                 Cudd_IterDerefBdd(manager, e);
01165                 return(NULL);
01166             }
01167             r = Cudd_Not(r);
01168         } else {
01169             r = cuddUniqueInter(manager,(int)index,t,e);
01170             if (r == NULL) {
01171                 Cudd_IterDerefBdd(manager, t);
01172                 Cudd_IterDerefBdd(manager, e);
01173                 return(NULL);
01174             }
01175         }
01176     }
01177     cuddDeref(e);
01178     cuddDeref(t);
01179     if (F->ref != 1 || G->ref != 1)
01180         cuddCacheInsert2(manager, Cudd_bddNPAnd, f, g, r);
01181     return(r);
01182 
01183 } /* end of cuddBddNPAndRecur */
01184 
01185 
01198 DdNode *
01199 cuddAddConstrainRecur(
01200   DdManager * dd,
01201   DdNode * f,
01202   DdNode * c)
01203 {
01204     DdNode       *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r;
01205     DdNode       *one, *zero;
01206     unsigned int topf, topc;
01207     int          index;
01208 
01209     statLine(dd);
01210     one = DD_ONE(dd);
01211     zero = DD_ZERO(dd);
01212 
01213     /* Trivial cases. */
01214     if (c == one)               return(f);
01215     if (c == zero)              return(zero);
01216     if (Cudd_IsConstant(f))     return(f);
01217     if (f == c)                 return(one);
01218 
01219     /* Now f and c are non-constant. */
01220 
01221     /* Check the cache. */
01222     r = cuddCacheLookup2(dd, Cudd_addConstrain, f, c);
01223     if (r != NULL) {
01224         return(r);
01225     }
01226     
01227     /* Recursive step. */
01228     topf = dd->perm[f->index];
01229     topc = dd->perm[c->index];
01230     if (topf <= topc) {
01231         index = f->index;
01232         Fv = cuddT(f); Fnv = cuddE(f);
01233     } else {
01234         index = c->index;
01235         Fv = Fnv = f;
01236     }
01237     if (topc <= topf) {
01238         Cv = cuddT(c); Cnv = cuddE(c);
01239     } else {
01240         Cv = Cnv = c;
01241     }
01242 
01243     if (!Cudd_IsConstant(Cv)) {
01244         t = cuddAddConstrainRecur(dd, Fv, Cv);
01245         if (t == NULL)
01246             return(NULL);
01247     } else if (Cv == one) {
01248         t = Fv;
01249     } else {            /* Cv == zero: return Fnv @ Cnv */
01250         if (Cnv == one) {
01251             r = Fnv;
01252         } else {
01253             r = cuddAddConstrainRecur(dd, Fnv, Cnv);
01254             if (r == NULL)
01255                 return(NULL);
01256         }
01257         return(r);
01258     }
01259     cuddRef(t);
01260 
01261     if (!Cudd_IsConstant(Cnv)) {
01262         e = cuddAddConstrainRecur(dd, Fnv, Cnv);
01263         if (e == NULL) {
01264             Cudd_RecursiveDeref(dd, t);
01265             return(NULL);
01266         }
01267     } else if (Cnv == one) {
01268         e = Fnv;
01269     } else {            /* Cnv == zero: return Fv @ Cv previously computed */
01270         cuddDeref(t);
01271         return(t);
01272     }
01273     cuddRef(e);
01274 
01275     r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
01276     if (r == NULL) {
01277         Cudd_RecursiveDeref(dd, e);
01278         Cudd_RecursiveDeref(dd, t);
01279         return(NULL);
01280     }
01281     cuddDeref(t);
01282     cuddDeref(e);
01283 
01284     cuddCacheInsert2(dd, Cudd_addConstrain, f, c, r);
01285     return(r);
01286 
01287 } /* end of cuddAddConstrainRecur */
01288 
01289 
01302 DdNode *
01303 cuddAddRestrictRecur(
01304   DdManager * dd,
01305   DdNode * f,
01306   DdNode * c)
01307 {
01308     DdNode       *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r, *one, *zero;
01309     unsigned int topf, topc;
01310     int          index;
01311 
01312     statLine(dd);
01313     one = DD_ONE(dd);
01314     zero = DD_ZERO(dd);
01315 
01316     /* Trivial cases */
01317     if (c == one)               return(f);
01318     if (c == zero)              return(zero);
01319     if (Cudd_IsConstant(f))     return(f);
01320     if (f == c)                 return(one);
01321 
01322     /* Now f and c are non-constant. */
01323 
01324     /* Check the cache. */
01325     r = cuddCacheLookup2(dd, Cudd_addRestrict, f, c);
01326     if (r != NULL) {
01327         return(r);
01328     }
01329 
01330     topf = dd->perm[f->index];
01331     topc = dd->perm[c->index];
01332 
01333     if (topc < topf) {  /* abstract top variable from c */
01334         DdNode *d, *s1, *s2;
01335 
01336         /* Find cofactors of c. */
01337         s1 = cuddT(c);
01338         s2 = cuddE(c);
01339         /* Take the OR by applying DeMorgan. */
01340         d = cuddAddApplyRecur(dd, Cudd_addOr, s1, s2);
01341         if (d == NULL) return(NULL);
01342         cuddRef(d);
01343         r = cuddAddRestrictRecur(dd, f, d);
01344         if (r == NULL) {
01345             Cudd_RecursiveDeref(dd, d);
01346             return(NULL);
01347         }
01348         cuddRef(r);
01349         Cudd_RecursiveDeref(dd, d);
01350         cuddCacheInsert2(dd, Cudd_addRestrict, f, c, r);
01351         cuddDeref(r);
01352         return(r);
01353     }
01354 
01355     /* Recursive step. Here topf <= topc. */
01356     index = f->index;
01357     Fv = cuddT(f); Fnv = cuddE(f);
01358     if (topc == topf) {
01359         Cv = cuddT(c); Cnv = cuddE(c);
01360     } else {
01361         Cv = Cnv = c;
01362     }
01363 
01364     if (!Cudd_IsConstant(Cv)) {
01365         t = cuddAddRestrictRecur(dd, Fv, Cv);
01366         if (t == NULL) return(NULL);
01367     } else if (Cv == one) {
01368         t = Fv;
01369     } else {            /* Cv == zero: return(Fnv @ Cnv) */
01370         if (Cnv == one) {
01371             r = Fnv;
01372         } else {
01373             r = cuddAddRestrictRecur(dd, Fnv, Cnv);
01374             if (r == NULL) return(NULL);
01375         }
01376         return(r);
01377     }
01378     cuddRef(t);
01379 
01380     if (!Cudd_IsConstant(Cnv)) {
01381         e = cuddAddRestrictRecur(dd, Fnv, Cnv);
01382         if (e == NULL) {
01383             Cudd_RecursiveDeref(dd, t);
01384             return(NULL);
01385         }
01386     } else if (Cnv == one) {
01387         e = Fnv;
01388     } else {            /* Cnv == zero: return (Fv @ Cv) previously computed */
01389         cuddDeref(t);
01390         return(t);
01391     }
01392     cuddRef(e);
01393 
01394     r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
01395     if (r == NULL) {
01396         Cudd_RecursiveDeref(dd, e);
01397         Cudd_RecursiveDeref(dd, t);
01398         return(NULL);
01399     }
01400     cuddDeref(t);
01401     cuddDeref(e);
01402 
01403     cuddCacheInsert2(dd, Cudd_addRestrict, f, c, r);
01404     return(r);
01405 
01406 } /* end of cuddAddRestrictRecur */
01407 
01408 
01409 
01429 DdNode *
01430 cuddBddLICompaction(
01431   DdManager * dd /* manager */,
01432   DdNode * f /* function to be minimized */,
01433   DdNode * c /* constraint (care set) */)
01434 {
01435     st_table *marktable, *markcache, *buildcache;
01436     DdNode *res, *zero;
01437 
01438     zero = Cudd_Not(DD_ONE(dd));
01439     if (c == zero) return(zero);
01440 
01441     /* We need to use local caches for both steps of this operation.
01442     ** The results of the edge marking step are only valid as long as the
01443     ** edge markings themselves are available. However, the edge markings
01444     ** are lost at the end of one invocation of Cudd_bddLICompaction.
01445     ** Hence, the cache entries for the edge marking step must be
01446     ** invalidated at the end of this function.
01447     ** For the result of the building step we argue as follows. The result
01448     ** for a node and a given constrain depends on the BDD in which the node
01449     ** appears. Hence, the same node and constrain may give different results
01450     ** in successive invocations.
01451     */
01452     marktable = st_init_table(st_ptrcmp,st_ptrhash);
01453     if (marktable == NULL) {
01454         return(NULL);
01455     }
01456     markcache = st_init_table(MarkCacheCompare,MarkCacheHash);
01457     if (markcache == NULL) {
01458         st_free_table(marktable);
01459         return(NULL);
01460     }
01461     if (cuddBddLICMarkEdges(dd,f,c,marktable,markcache) == CUDD_OUT_OF_MEM) {
01462         st_foreach(markcache, MarkCacheCleanUp, NULL);
01463         st_free_table(marktable);
01464         st_free_table(markcache);
01465         return(NULL);
01466     }
01467     st_foreach(markcache, MarkCacheCleanUp, NULL);
01468     st_free_table(markcache);
01469     buildcache = st_init_table(st_ptrcmp,st_ptrhash);
01470     if (buildcache == NULL) {
01471         st_free_table(marktable);
01472         return(NULL);
01473     }
01474     res = cuddBddLICBuildResult(dd,f,buildcache,marktable);
01475     st_free_table(buildcache);
01476     st_free_table(marktable);
01477     return(res);
01478 
01479 } /* end of cuddBddLICompaction */
01480 
01481 
01482 /*---------------------------------------------------------------------------*/
01483 /* Definition of static functions                                            */
01484 /*---------------------------------------------------------------------------*/
01485 
01486 
01499 static int
01500 cuddBddConstrainDecomp(
01501   DdManager * dd,
01502   DdNode * f,
01503   DdNode ** decomp)
01504 {
01505     DdNode *F, *fv, *fvn;
01506     DdNode *fAbs;
01507     DdNode *result;
01508     int ok;
01509 
01510     if (Cudd_IsConstant(f)) return(1);
01511     /* Compute complements of cofactors. */
01512     F = Cudd_Regular(f);
01513     fv = cuddT(F);
01514     fvn = cuddE(F);
01515     if (F == f) {
01516         fv = Cudd_Not(fv);
01517         fvn = Cudd_Not(fvn);
01518     }
01519     /* Compute abstraction of top variable. */
01520     fAbs = cuddBddAndRecur(dd, fv, fvn);
01521     if (fAbs == NULL) {
01522         return(0);
01523     }
01524     cuddRef(fAbs);
01525     fAbs = Cudd_Not(fAbs);
01526     /* Recursively find the next abstraction and the components of the
01527     ** decomposition. */
01528     ok = cuddBddConstrainDecomp(dd, fAbs, decomp);
01529     if (ok == 0) {
01530         Cudd_IterDerefBdd(dd,fAbs);
01531         return(0);
01532     }
01533     /* Compute the component of the decomposition corresponding to the
01534     ** top variable and store it in the decomposition array. */
01535     result = cuddBddConstrainRecur(dd, f, fAbs);
01536     if (result == NULL) {
01537         Cudd_IterDerefBdd(dd,fAbs);
01538         return(0);
01539     }
01540     cuddRef(result);
01541     decomp[F->index] = result;
01542     Cudd_IterDerefBdd(dd, fAbs);
01543     return(1);
01544 
01545 } /* end of cuddBddConstrainDecomp */
01546 
01547 
01561 static DdNode *
01562 cuddBddCharToVect(
01563   DdManager * dd,
01564   DdNode * f,
01565   DdNode * x)
01566 {
01567     unsigned int topf;
01568     unsigned int level;
01569     int comple;
01570 
01571     DdNode *one, *zero, *res, *F, *fT, *fE, *T, *E;
01572 
01573     statLine(dd);
01574     /* Check the cache. */
01575     res = cuddCacheLookup2(dd, cuddBddCharToVect, f, x);
01576     if (res != NULL) {
01577         return(res);
01578     }
01579 
01580     F = Cudd_Regular(f);
01581 
01582     topf = cuddI(dd,F->index);
01583     level = dd->perm[x->index];
01584 
01585     if (topf > level) return(x);
01586 
01587     one = DD_ONE(dd);
01588     zero = Cudd_Not(one);
01589 
01590     comple = F != f;
01591     fT = Cudd_NotCond(cuddT(F),comple);
01592     fE = Cudd_NotCond(cuddE(F),comple);
01593 
01594     if (topf == level) {
01595         if (fT == zero) return(zero);
01596         if (fE == zero) return(one);
01597         return(x);
01598     }
01599 
01600     /* Here topf < level. */
01601     if (fT == zero) return(cuddBddCharToVect(dd, fE, x));
01602     if (fE == zero) return(cuddBddCharToVect(dd, fT, x));
01603 
01604     T = cuddBddCharToVect(dd, fT, x);
01605     if (T == NULL) {
01606         return(NULL);
01607     }
01608     cuddRef(T);
01609     E = cuddBddCharToVect(dd, fE, x);
01610     if (E == NULL) {
01611         Cudd_IterDerefBdd(dd,T);
01612         return(NULL);
01613     }
01614     cuddRef(E);
01615     res = cuddBddIteRecur(dd, dd->vars[F->index], T, E);
01616     if (res == NULL) {
01617         Cudd_IterDerefBdd(dd,T);
01618         Cudd_IterDerefBdd(dd,E);
01619         return(NULL);
01620     }
01621     cuddDeref(T);
01622     cuddDeref(E);
01623     cuddCacheInsert2(dd, cuddBddCharToVect, f, x, res);
01624     return(res);
01625 
01626 } /* end of cuddBddCharToVect */
01627 
01628 
01642 static int
01643 cuddBddLICMarkEdges(
01644   DdManager * dd,
01645   DdNode * f,
01646   DdNode * c,
01647   st_table * table,
01648   st_table * cache)
01649 {
01650     DdNode *Fv, *Fnv, *Cv, *Cnv;
01651     DdNode *one, *zero;
01652     unsigned int topf, topc;
01653     int comple;
01654     int resT, resE, res, retval;
01655     char **slot;
01656     MarkCacheKey *key;
01657 
01658     one = DD_ONE(dd);
01659     zero = Cudd_Not(one);
01660 
01661     /* Terminal cases. */
01662     if (c == zero) return(DD_LIC_DC);
01663     if (f == one)  return(DD_LIC_1);
01664     if (f == zero) return(DD_LIC_0);
01665 
01666     /* Make canonical to increase the utilization of the cache. */
01667     comple = Cudd_IsComplement(f);
01668     f = Cudd_Regular(f);
01669     /* Now f is a regular pointer to a non-constant node; c may be
01670     ** constant, or it may be complemented.
01671     */
01672 
01673     /* Check the cache. */
01674     key = ALLOC(MarkCacheKey, 1);
01675     if (key == NULL) {
01676         dd->errorCode = CUDD_MEMORY_OUT;
01677         return(CUDD_OUT_OF_MEM);
01678     }
01679     key->f = f; key->c = c;
01680     if (st_lookup_int(cache, (char *)key, &res)) {
01681         FREE(key);
01682         if (comple) {
01683             if (res == DD_LIC_0) res = DD_LIC_1;
01684             else if (res == DD_LIC_1) res = DD_LIC_0;
01685         }
01686         return(res);
01687     }
01688 
01689     /* Recursive step. */
01690     topf = dd->perm[f->index];
01691     topc = cuddI(dd,Cudd_Regular(c)->index);
01692     if (topf <= topc) {
01693         Fv = cuddT(f); Fnv = cuddE(f);
01694     } else {
01695         Fv = Fnv = f;
01696     }
01697     if (topc <= topf) {
01698         /* We know that c is not constant because f is not. */
01699         Cv = cuddT(Cudd_Regular(c)); Cnv = cuddE(Cudd_Regular(c));
01700         if (Cudd_IsComplement(c)) {
01701             Cv = Cudd_Not(Cv);
01702             Cnv = Cudd_Not(Cnv);
01703         }
01704     } else {
01705         Cv = Cnv = c;
01706     }
01707 
01708     resT = cuddBddLICMarkEdges(dd, Fv, Cv, table, cache);
01709     if (resT == CUDD_OUT_OF_MEM) {
01710         FREE(key);
01711         return(CUDD_OUT_OF_MEM);
01712     }
01713     resE = cuddBddLICMarkEdges(dd, Fnv, Cnv, table, cache);
01714     if (resE == CUDD_OUT_OF_MEM) {
01715         FREE(key);
01716         return(CUDD_OUT_OF_MEM);
01717     }
01718 
01719     /* Update edge markings. */
01720     if (topf <= topc) {
01721         retval = st_find_or_add(table, (char *)f, (char ***)&slot);
01722         if (retval == 0) {
01723             *slot = (char *) (ptrint)((resT << 2) | resE);
01724         } else if (retval == 1) {
01725             *slot = (char *) (ptrint)((int)((ptrint) *slot) | (resT << 2) | resE);
01726         } else {
01727             FREE(key);
01728             return(CUDD_OUT_OF_MEM);
01729         }
01730     }
01731 
01732     /* Cache result. */
01733     res = resT | resE;
01734     if (st_insert(cache, (char *)key, (char *)(ptrint)res) == ST_OUT_OF_MEM) {
01735         FREE(key);
01736         return(CUDD_OUT_OF_MEM);
01737     }
01738 
01739     /* Take into account possible complementation. */
01740     if (comple) {
01741         if (res == DD_LIC_0) res = DD_LIC_1;
01742         else if (res == DD_LIC_1) res = DD_LIC_0;
01743     }
01744     return(res);
01745 
01746 } /* end of cuddBddLICMarkEdges */
01747 
01748 
01761 static DdNode *
01762 cuddBddLICBuildResult(
01763   DdManager * dd,
01764   DdNode * f,
01765   st_table * cache,
01766   st_table * table)
01767 {
01768     DdNode *Fv, *Fnv, *r, *t, *e;
01769     DdNode *one, *zero;
01770     int index;
01771     int comple;
01772     int markT, markE, markings;
01773 
01774     one = DD_ONE(dd);
01775     zero = Cudd_Not(one);
01776 
01777     if (Cudd_IsConstant(f)) return(f);
01778     /* Make canonical to increase the utilization of the cache. */
01779     comple = Cudd_IsComplement(f);
01780     f = Cudd_Regular(f);
01781 
01782     /* Check the cache. */
01783     if (st_lookup(cache, f, &r)) {
01784         return(Cudd_NotCond(r,comple));
01785     }
01786 
01787     /* Retrieve the edge markings. */
01788     if (st_lookup_int(table, (char *)f, &markings) == 0)
01789         return(NULL);
01790     markT = markings >> 2;
01791     markE = markings & 3;
01792 
01793     index = f->index;
01794     Fv = cuddT(f); Fnv = cuddE(f);
01795 
01796     if (markT == DD_LIC_NL) {
01797         t = cuddBddLICBuildResult(dd,Fv,cache,table);
01798         if (t == NULL) {
01799             return(NULL);
01800         }
01801     } else if (markT == DD_LIC_1) {
01802         t = one;
01803     } else {
01804         t = zero;
01805     }
01806     cuddRef(t);
01807     if (markE == DD_LIC_NL) {
01808         e = cuddBddLICBuildResult(dd,Fnv,cache,table);
01809         if (e == NULL) {
01810             Cudd_IterDerefBdd(dd,t);
01811             return(NULL);
01812         }
01813     } else if (markE == DD_LIC_1) {
01814         e = one;
01815     } else {
01816         e = zero;
01817     }
01818     cuddRef(e);
01819 
01820     if (markT == DD_LIC_DC && markE != DD_LIC_DC) {
01821         r = e;
01822     } else if (markT != DD_LIC_DC && markE == DD_LIC_DC) {
01823         r = t;
01824     } else {
01825         if (Cudd_IsComplement(t)) {
01826             t = Cudd_Not(t);
01827             e = Cudd_Not(e);
01828             r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
01829             if (r == NULL) {
01830                 Cudd_IterDerefBdd(dd, e);
01831                 Cudd_IterDerefBdd(dd, t);
01832                 return(NULL);
01833             }
01834             r = Cudd_Not(r);
01835         } else {
01836             r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
01837             if (r == NULL) {
01838                 Cudd_IterDerefBdd(dd, e);
01839                 Cudd_IterDerefBdd(dd, t);
01840                 return(NULL);
01841             }
01842         }
01843     }
01844     cuddDeref(t);
01845     cuddDeref(e);
01846 
01847     if (st_insert(cache, (char *)f, (char *)r) == ST_OUT_OF_MEM) {
01848         cuddRef(r);
01849         Cudd_IterDerefBdd(dd,r);
01850         return(NULL);
01851     }
01852 
01853     return(Cudd_NotCond(r,comple));
01854 
01855 } /* end of cuddBddLICBuildResult */
01856 
01857 
01870 static int
01871 MarkCacheHash(
01872   char * ptr,
01873   int  modulus)
01874 {
01875     int val = 0;
01876     MarkCacheKey *entry;
01877 
01878     entry = (MarkCacheKey *) ptr;
01879 
01880     val = (int) (ptrint) entry->f;
01881     val = val * 997 + (int) (ptrint) entry->c;
01882 
01883     return ((val < 0) ? -val : val) % modulus;
01884 
01885 } /* end of MarkCacheHash */
01886 
01887 
01902 static int
01903 MarkCacheCompare(
01904   const char * ptr1,
01905   const char * ptr2)
01906 {
01907     MarkCacheKey *entry1, *entry2;
01908 
01909     entry1 = (MarkCacheKey *) ptr1;
01910     entry2 = (MarkCacheKey *) ptr2;
01911     
01912     return((entry1->f != entry2->f) || (entry1->c != entry2->c));
01913 
01914 } /* end of MarkCacheCompare */
01915 
01916 
01917 
01931 static enum st_retval
01932 MarkCacheCleanUp(
01933   char * key,
01934   char * value,
01935   char * arg)
01936 {
01937     MarkCacheKey *entry;
01938 
01939     entry = (MarkCacheKey *) key;
01940     FREE(entry);
01941     return ST_CONTINUE;
01942 
01943 } /* end of MarkCacheCleanUp */
01944 
01945 
01962 static DdNode *
01963 cuddBddSqueeze(
01964   DdManager * dd,
01965   DdNode * l,
01966   DdNode * u)
01967 {
01968     DdNode *one, *zero, *r, *lt, *le, *ut, *ue, *t, *e;
01969 #if 0
01970     DdNode *ar;
01971 #endif
01972     int comple = 0;
01973     unsigned int topu, topl;
01974     int index;
01975 
01976     statLine(dd);
01977     if (l == u) {
01978         return(l);
01979     }
01980     one = DD_ONE(dd);
01981     zero = Cudd_Not(one);
01982     /* The only case when l == zero && u == one is at the top level,
01983     ** where returning either one or zero is OK. In all other cases
01984     ** the procedure will detect such a case and will perform
01985     ** remapping. Therefore the order in which we test l and u at this
01986     ** point is immaterial. */
01987     if (l == zero) return(l);
01988     if (u == one)  return(u);
01989 
01990     /* Make canonical to increase the utilization of the cache. */
01991     if (Cudd_IsComplement(u)) {
01992         DdNode *temp;
01993         temp = Cudd_Not(l);
01994         l = Cudd_Not(u);
01995         u = temp;
01996         comple = 1;
01997     }
01998     /* At this point u is regular and non-constant; l is non-constant, but
01999     ** may be complemented. */
02000 
02001     /* Here we could check the relative sizes. */
02002 
02003     /* Check the cache. */
02004     r = cuddCacheLookup2(dd, Cudd_bddSqueeze, l, u);
02005     if (r != NULL) {
02006         return(Cudd_NotCond(r,comple));
02007     }
02008 
02009     /* Recursive step. */
02010     topu = dd->perm[u->index];
02011     topl = dd->perm[Cudd_Regular(l)->index];
02012     if (topu <= topl) {
02013         index = u->index;
02014         ut = cuddT(u); ue = cuddE(u);
02015     } else {
02016         index = Cudd_Regular(l)->index;
02017         ut = ue = u;
02018     }
02019     if (topl <= topu) {
02020         lt = cuddT(Cudd_Regular(l)); le = cuddE(Cudd_Regular(l));
02021         if (Cudd_IsComplement(l)) {
02022             lt = Cudd_Not(lt);
02023             le = Cudd_Not(le);
02024         }
02025     } else {
02026         lt = le = l;
02027     }
02028 
02029     /* If one interval is contained in the other, use the smaller
02030     ** interval. This corresponds to one-sided matching. */
02031     if ((lt == zero || Cudd_bddLeq(dd,lt,le)) &&
02032         (ut == one  || Cudd_bddLeq(dd,ue,ut))) { /* remap */
02033         r = cuddBddSqueeze(dd, le, ue);
02034         if (r == NULL)
02035             return(NULL);
02036         return(Cudd_NotCond(r,comple));
02037     } else if ((le == zero || Cudd_bddLeq(dd,le,lt)) &&
02038                (ue == one  || Cudd_bddLeq(dd,ut,ue))) { /* remap */
02039         r = cuddBddSqueeze(dd, lt, ut);
02040         if (r == NULL)
02041             return(NULL);
02042         return(Cudd_NotCond(r,comple));
02043     } else if ((le == zero || Cudd_bddLeq(dd,le,Cudd_Not(ut))) &&
02044                (ue == one  || Cudd_bddLeq(dd,Cudd_Not(lt),ue))) { /* c-remap */
02045         t = cuddBddSqueeze(dd, lt, ut);
02046         cuddRef(t);
02047         if (Cudd_IsComplement(t)) {
02048             r = cuddUniqueInter(dd, index, Cudd_Not(t), t);
02049             if (r == NULL) {
02050                 Cudd_IterDerefBdd(dd, t);
02051                 return(NULL);
02052             }
02053             r = Cudd_Not(r);
02054         } else {
02055             r = cuddUniqueInter(dd, index, t, Cudd_Not(t));
02056             if (r == NULL) {
02057                 Cudd_IterDerefBdd(dd, t);
02058                 return(NULL);
02059             }
02060         }
02061         cuddDeref(t);
02062         if (r == NULL)
02063             return(NULL);
02064         cuddCacheInsert2(dd, Cudd_bddSqueeze, l, u, r);
02065         return(Cudd_NotCond(r,comple));
02066     } else if ((lt == zero || Cudd_bddLeq(dd,lt,Cudd_Not(ue))) &&
02067                (ut == one  || Cudd_bddLeq(dd,Cudd_Not(le),ut))) { /* c-remap */
02068         e = cuddBddSqueeze(dd, le, ue);
02069         cuddRef(e);
02070         if (Cudd_IsComplement(e)) {
02071             r = cuddUniqueInter(dd, index, Cudd_Not(e), e);
02072             if (r == NULL) {
02073                 Cudd_IterDerefBdd(dd, e);
02074                 return(NULL);
02075             }
02076         } else {
02077             r = cuddUniqueInter(dd, index, e, Cudd_Not(e));
02078             if (r == NULL) {
02079                 Cudd_IterDerefBdd(dd, e);
02080                 return(NULL);
02081             }
02082             r = Cudd_Not(r);
02083         }
02084         cuddDeref(e);
02085         if (r == NULL)
02086             return(NULL);
02087         cuddCacheInsert2(dd, Cudd_bddSqueeze, l, u, r);
02088         return(Cudd_NotCond(r,comple));
02089     }
02090 
02091 #if 0
02092     /* If the two intervals intersect, take a solution from
02093     ** the intersection of the intervals. This guarantees that the
02094     ** splitting variable will not appear in the result.
02095     ** This approach corresponds to two-sided matching, and is very
02096     ** expensive. */
02097     if (Cudd_bddLeq(dd,lt,ue) && Cudd_bddLeq(dd,le,ut)) {
02098         DdNode *au, *al;
02099         au = cuddBddAndRecur(dd,ut,ue);
02100         if (au == NULL)
02101             return(NULL);
02102         cuddRef(au);
02103         al = cuddBddAndRecur(dd,Cudd_Not(lt),Cudd_Not(le));
02104         if (al == NULL) {
02105             Cudd_IterDerefBdd(dd,au);
02106             return(NULL);
02107         }
02108         cuddRef(al);
02109         al = Cudd_Not(al);
02110         ar = cuddBddSqueeze(dd, al, au);
02111         if (ar == NULL) {
02112             Cudd_IterDerefBdd(dd,au);
02113             Cudd_IterDerefBdd(dd,al);
02114             return(NULL);
02115         }
02116         cuddRef(ar);
02117         Cudd_IterDerefBdd(dd,au);
02118         Cudd_IterDerefBdd(dd,al);
02119     } else {
02120         ar = NULL;
02121     }
02122 #endif
02123 
02124     t = cuddBddSqueeze(dd, lt, ut);
02125     if (t == NULL) {
02126         return(NULL);
02127     }
02128     cuddRef(t);
02129     e = cuddBddSqueeze(dd, le, ue);
02130     if (e == NULL) {
02131         Cudd_IterDerefBdd(dd,t);
02132         return(NULL);
02133     }
02134     cuddRef(e);
02135 
02136     if (Cudd_IsComplement(t)) {
02137         t = Cudd_Not(t);
02138         e = Cudd_Not(e);
02139         r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
02140         if (r == NULL) {
02141             Cudd_IterDerefBdd(dd, e);
02142             Cudd_IterDerefBdd(dd, t);
02143             return(NULL);
02144         }
02145         r = Cudd_Not(r);
02146     } else {
02147         r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
02148         if (r == NULL) {
02149             Cudd_IterDerefBdd(dd, e);
02150             Cudd_IterDerefBdd(dd, t);
02151             return(NULL);
02152         }
02153     }
02154     cuddDeref(t);
02155     cuddDeref(e);
02156 
02157 #if 0
02158     /* Check whether there is a result obtained by abstraction and whether
02159     ** it is better than the one obtained by recursion. */
02160     cuddRef(r);
02161     if (ar != NULL) {
02162         if (Cudd_DagSize(ar) <= Cudd_DagSize(r)) {
02163             Cudd_IterDerefBdd(dd, r);
02164             r = ar;
02165         } else {
02166             Cudd_IterDerefBdd(dd, ar);
02167         }
02168     }
02169     cuddDeref(r);
02170 #endif
02171 
02172     cuddCacheInsert2(dd, Cudd_bddSqueeze, l, u, r);
02173     return(Cudd_NotCond(r,comple));
02174 
02175 } /* end of cuddBddSqueeze */