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

00001 
00049 #include    "util_hack.h"
00050 #include    "cuddInt.h"
00051 
00052 /*---------------------------------------------------------------------------*/
00053 /* Constant declarations                                                     */
00054 /*---------------------------------------------------------------------------*/
00055 
00056 
00057 /*---------------------------------------------------------------------------*/
00058 /* Stucture declarations                                                     */
00059 /*---------------------------------------------------------------------------*/
00060 
00061 
00062 /*---------------------------------------------------------------------------*/
00063 /* Type declarations                                                         */
00064 /*---------------------------------------------------------------------------*/
00065 
00066 
00067 /*---------------------------------------------------------------------------*/
00068 /* Variable declarations                                                     */
00069 /*---------------------------------------------------------------------------*/
00070 
00071 #ifndef lint
00072 static char rcsid[] DD_UNUSED = "$Id: cuddZddSetop.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang Exp $";
00073 #endif
00074 
00075 /*---------------------------------------------------------------------------*/
00076 /* Macro declarations                                                        */
00077 /*---------------------------------------------------------------------------*/
00078 
00079 
00082 /*---------------------------------------------------------------------------*/
00083 /* Static function prototypes                                                */
00084 /*---------------------------------------------------------------------------*/
00085 
00086 static DdNode * zdd_subset1_aux ARGS((DdManager *zdd, DdNode *P, DdNode *zvar));
00087 static DdNode * zdd_subset0_aux ARGS((DdManager *zdd, DdNode *P, DdNode *zvar));
00088 static void zddVarToConst ARGS((DdNode *f, DdNode **gp, DdNode **hp, DdNode *base, DdNode *empty));
00089 
00093 /*---------------------------------------------------------------------------*/
00094 /* Definition of exported functions                                          */
00095 /*---------------------------------------------------------------------------*/
00096 
00097 
00110 DdNode *
00111 Cudd_zddIte(
00112   DdManager * dd,
00113   DdNode * f,
00114   DdNode * g,
00115   DdNode * h)
00116 {
00117     DdNode *res;
00118 
00119     do {
00120         dd->reordered = 0;
00121         res = cuddZddIte(dd, f, g, h);
00122     } while (dd->reordered == 1);
00123     return(res);
00124 
00125 } /* end of Cudd_zddIte */
00126 
00127 
00140 DdNode *
00141 Cudd_zddUnion(
00142   DdManager * dd,
00143   DdNode * P,
00144   DdNode * Q)
00145 {
00146     DdNode *res;
00147 
00148     do {
00149         dd->reordered = 0;
00150         res = cuddZddUnion(dd, P, Q);
00151     } while (dd->reordered == 1);
00152     return(res);
00153 
00154 } /* end of Cudd_zddUnion */
00155 
00156 
00169 DdNode *
00170 Cudd_zddIntersect(
00171   DdManager * dd,
00172   DdNode * P,
00173   DdNode * Q)
00174 {
00175     DdNode *res;
00176 
00177     do {
00178         dd->reordered = 0;
00179         res = cuddZddIntersect(dd, P, Q);
00180     } while (dd->reordered == 1);
00181     return(res);
00182 
00183 } /* end of Cudd_zddIntersect */
00184 
00185 
00198 DdNode *
00199 Cudd_zddDiff(
00200   DdManager * dd,
00201   DdNode * P,
00202   DdNode * Q)
00203 {
00204     DdNode *res;
00205 
00206     do {
00207         dd->reordered = 0;
00208         res = cuddZddDiff(dd, P, Q);
00209     } while (dd->reordered == 1);
00210     return(res);
00211 
00212 } /* end of Cudd_zddDiff */
00213 
00214 
00228 DdNode *
00229 Cudd_zddDiffConst(
00230   DdManager * zdd,
00231   DdNode * P,
00232   DdNode * Q)
00233 {
00234     int         p_top, q_top;
00235     DdNode      *empty = DD_ZERO(zdd), *t, *res;
00236     DdManager   *table = zdd;
00237 
00238     statLine(zdd);
00239     if (P == empty)
00240         return(empty);
00241     if (Q == empty)
00242         return(P);
00243     if (P == Q)
00244         return(empty);
00245 
00246     /* Check cache.  The cache is shared by cuddZddDiff(). */
00247     res = cuddCacheLookup2Zdd(table, cuddZddDiff, P, Q);
00248     if (res != NULL)
00249         return(res);
00250 
00251     if (cuddIsConstant(P))
00252         p_top = P->index;
00253     else
00254         p_top = zdd->permZ[P->index];
00255     if (cuddIsConstant(Q))
00256         q_top = Q->index;
00257     else
00258         q_top = zdd->permZ[Q->index];
00259     if (p_top < q_top) {
00260         res = DD_NON_CONSTANT;
00261     } else if (p_top > q_top) {
00262         res = Cudd_zddDiffConst(zdd, P, cuddE(Q));
00263     } else {
00264         t = Cudd_zddDiffConst(zdd, cuddT(P), cuddT(Q));
00265         if (t != empty)
00266             res = DD_NON_CONSTANT;
00267         else
00268             res = Cudd_zddDiffConst(zdd, cuddE(P), cuddE(Q));
00269     }
00270 
00271     cuddCacheInsert2(table, cuddZddDiff, P, Q, res);
00272 
00273     return(res);
00274 
00275 } /* end of Cudd_zddDiffConst */
00276 
00277 
00292 DdNode *
00293 Cudd_zddSubset1(
00294   DdManager * dd,
00295   DdNode * P,
00296   int  var)
00297 {
00298     DdNode      *r;
00299 
00300     do {
00301         dd->reordered = 0;
00302         r = cuddZddSubset1(dd, P, var);
00303     } while (dd->reordered == 1);
00304 
00305     return(r);
00306 
00307 } /* end of Cudd_zddSubset1 */
00308 
00309 
00324 DdNode *
00325 Cudd_zddSubset0(
00326   DdManager * dd,
00327   DdNode * P,
00328   int  var)
00329 {
00330     DdNode      *r;
00331 
00332     do {
00333         dd->reordered = 0;
00334         r = cuddZddSubset0(dd, P, var);
00335     } while (dd->reordered == 1);
00336 
00337     return(r);
00338 
00339 } /* end of Cudd_zddSubset0 */
00340 
00341 
00354 DdNode *
00355 Cudd_zddChange(
00356   DdManager * dd,
00357   DdNode * P,
00358   int  var)
00359 {
00360     DdNode      *res;
00361 
00362     if ((unsigned int) var >= CUDD_MAXINDEX - 1) return(NULL);
00363     
00364     do {
00365         dd->reordered = 0;
00366         res = cuddZddChange(dd, P, var);
00367     } while (dd->reordered == 1);
00368     return(res);
00369 
00370 } /* end of Cudd_zddChange */
00371 
00372 
00373 /*---------------------------------------------------------------------------*/
00374 /* Definition of internal functions                                          */
00375 /*---------------------------------------------------------------------------*/
00376 
00377 
00389 DdNode *
00390 cuddZddIte(
00391   DdManager * dd,
00392   DdNode * f,
00393   DdNode * g,
00394   DdNode * h)
00395 {
00396     DdNode *tautology, *empty;
00397     DdNode *r,*Gv,*Gvn,*Hv,*Hvn,*t,*e;
00398     unsigned int topf,topg,toph,v,top;
00399     int index;
00400 
00401     statLine(dd);
00402     /* Trivial cases. */
00403     /* One variable cases. */
00404     if (f == (empty = DD_ZERO(dd))) {   /* ITE(0,G,H) = H */
00405         return(h);
00406     }
00407     topf = cuddIZ(dd,f->index);
00408     topg = cuddIZ(dd,g->index);
00409     toph = cuddIZ(dd,h->index);
00410     v = ddMin(topg,toph);
00411     top  = ddMin(topf,v);
00412 
00413     tautology = (top == CUDD_MAXINDEX) ? DD_ONE(dd) : dd->univ[top];
00414     if (f == tautology) {                       /* ITE(1,G,H) = G */
00415         return(g);
00416     }
00417 
00418     /* From now on, f is known to not be a constant. */
00419     zddVarToConst(f,&g,&h,tautology,empty);
00420 
00421     /* Check remaining one variable cases. */
00422     if (g == h) {                       /* ITE(F,G,G) = G */
00423         return(g);
00424     }
00425 
00426     if (g == tautology) {                       /* ITE(F,1,0) = F */
00427         if (h == empty) return(f);
00428     }
00429 
00430     /* Check cache. */
00431     r = cuddCacheLookupZdd(dd,DD_ZDD_ITE_TAG,f,g,h);
00432     if (r != NULL) {
00433         return(r);
00434     }
00435 
00436     /* Recompute these because they may have changed in zddVarToConst. */
00437     topg = cuddIZ(dd,g->index);
00438     toph = cuddIZ(dd,h->index);
00439     v = ddMin(topg,toph);
00440 
00441     if (topf < v) {
00442         r = cuddZddIte(dd,cuddE(f),g,h);
00443         if (r == NULL) return(NULL);
00444     } else if (topf > v) {
00445         if (topg > v) {
00446             Gvn = g;
00447             index = h->index;
00448         } else {
00449             Gvn = cuddE(g);
00450             index = g->index;
00451         }
00452         if (toph > v) {
00453             Hv = empty; Hvn = h;
00454         } else {
00455             Hv = cuddT(h); Hvn = cuddE(h);
00456         }
00457         e = cuddZddIte(dd,f,Gvn,Hvn);
00458         if (e == NULL) return(NULL);
00459         cuddRef(e);
00460         r = cuddZddGetNode(dd,index,Hv,e);
00461         if (r == NULL) {
00462             Cudd_RecursiveDerefZdd(dd,e);
00463             return(NULL);
00464         }
00465         cuddDeref(e);
00466     } else {
00467         index = f->index;
00468         if (topg > v) {
00469             Gv = empty; Gvn = g;
00470         } else {
00471             Gv = cuddT(g); Gvn = cuddE(g);
00472         }
00473         if (toph > v) {
00474             Hv = empty; Hvn = h;
00475         } else {
00476             Hv = cuddT(h); Hvn = cuddE(h);
00477         }
00478         e = cuddZddIte(dd,cuddE(f),Gvn,Hvn);
00479         if (e == NULL) return(NULL);
00480         cuddRef(e);
00481         t = cuddZddIte(dd,cuddT(f),Gv,Hv);
00482         if (t == NULL) {
00483             Cudd_RecursiveDerefZdd(dd,e);
00484             return(NULL);
00485         }
00486         cuddRef(t);
00487         r = cuddZddGetNode(dd,index,t,e);
00488         if (r == NULL) {
00489             Cudd_RecursiveDerefZdd(dd,e);
00490             Cudd_RecursiveDerefZdd(dd,t);
00491             return(NULL);
00492         }
00493         cuddDeref(t);
00494         cuddDeref(e);
00495     }
00496 
00497     cuddCacheInsert(dd,DD_ZDD_ITE_TAG,f,g,h,r);
00498 
00499     return(r);
00500 
00501 } /* end of cuddZddIte */
00502 
00503 
00515 DdNode *
00516 cuddZddUnion(
00517   DdManager * zdd,
00518   DdNode * P,
00519   DdNode * Q)
00520 {
00521     int         p_top, q_top;
00522     DdNode      *empty = DD_ZERO(zdd), *t, *e, *res;
00523     DdManager   *table = zdd;
00524 
00525     statLine(zdd);
00526     if (P == empty)
00527         return(Q);
00528     if (Q == empty)
00529         return(P);
00530     if (P == Q)
00531         return(P);
00532 
00533     /* Check cache */
00534     res = cuddCacheLookup2Zdd(table, cuddZddUnion, P, Q);
00535     if (res != NULL)
00536         return(res);
00537 
00538     if (cuddIsConstant(P))
00539         p_top = P->index;
00540     else
00541         p_top = zdd->permZ[P->index];
00542     if (cuddIsConstant(Q))
00543         q_top = Q->index;
00544     else
00545         q_top = zdd->permZ[Q->index];
00546     if (p_top < q_top) {
00547         e = cuddZddUnion(zdd, cuddE(P), Q);
00548         if (e == NULL) return (NULL);
00549         cuddRef(e);
00550         res = cuddZddGetNode(zdd, P->index, cuddT(P), e);
00551         if (res == NULL) {
00552             Cudd_RecursiveDerefZdd(table, e);
00553             return(NULL);
00554         }
00555         cuddDeref(e);
00556     } else if (p_top > q_top) {
00557         e = cuddZddUnion(zdd, P, cuddE(Q));
00558         if (e == NULL) return(NULL);
00559         cuddRef(e);
00560         res = cuddZddGetNode(zdd, Q->index, cuddT(Q), e);
00561         if (res == NULL) {
00562             Cudd_RecursiveDerefZdd(table, e);
00563             return(NULL);
00564         }
00565         cuddDeref(e);
00566     } else {
00567         t = cuddZddUnion(zdd, cuddT(P), cuddT(Q));
00568         if (t == NULL) return(NULL);
00569         cuddRef(t);
00570         e = cuddZddUnion(zdd, cuddE(P), cuddE(Q));
00571         if (e == NULL) {
00572             Cudd_RecursiveDerefZdd(table, t);
00573             return(NULL);
00574         }
00575         cuddRef(e);
00576         res = cuddZddGetNode(zdd, P->index, t, e);
00577         if (res == NULL) {
00578             Cudd_RecursiveDerefZdd(table, t);
00579             Cudd_RecursiveDerefZdd(table, e);
00580             return(NULL);
00581         }
00582         cuddDeref(t);
00583         cuddDeref(e);
00584     }
00585 
00586     cuddCacheInsert2(table, cuddZddUnion, P, Q, res);
00587 
00588     return(res);
00589 
00590 } /* end of cuddZddUnion */
00591 
00592 
00604 DdNode *
00605 cuddZddIntersect(
00606   DdManager * zdd,
00607   DdNode * P,
00608   DdNode * Q)
00609 {
00610     int         p_top, q_top;
00611     DdNode      *empty = DD_ZERO(zdd), *t, *e, *res;
00612     DdManager   *table = zdd;
00613 
00614     statLine(zdd);
00615     if (P == empty)
00616         return(empty);
00617     if (Q == empty)
00618         return(empty);
00619     if (P == Q)
00620         return(P);
00621 
00622     /* Check cache. */
00623     res = cuddCacheLookup2Zdd(table, cuddZddIntersect, P, Q);
00624     if (res != NULL)
00625         return(res);
00626 
00627     if (cuddIsConstant(P))
00628         p_top = P->index;
00629     else
00630         p_top = zdd->permZ[P->index];
00631     if (cuddIsConstant(Q))
00632         q_top = Q->index;
00633     else
00634         q_top = zdd->permZ[Q->index];
00635     if (p_top < q_top) {
00636         res = cuddZddIntersect(zdd, cuddE(P), Q);
00637         if (res == NULL) return(NULL);
00638     } else if (p_top > q_top) {
00639         res = cuddZddIntersect(zdd, P, cuddE(Q));
00640         if (res == NULL) return(NULL);
00641     } else {
00642         t = cuddZddIntersect(zdd, cuddT(P), cuddT(Q));
00643         if (t == NULL) return(NULL);
00644         cuddRef(t);
00645         e = cuddZddIntersect(zdd, cuddE(P), cuddE(Q));
00646         if (e == NULL) {
00647             Cudd_RecursiveDerefZdd(table, t);
00648             return(NULL);
00649         }
00650         cuddRef(e);
00651         res = cuddZddGetNode(zdd, P->index, t, e);
00652         if (res == NULL) {
00653             Cudd_RecursiveDerefZdd(table, t);
00654             Cudd_RecursiveDerefZdd(table, e);
00655             return(NULL);
00656         }
00657         cuddDeref(t);
00658         cuddDeref(e);
00659     }
00660 
00661     cuddCacheInsert2(table, cuddZddIntersect, P, Q, res);
00662 
00663     return(res);
00664 
00665 } /* end of cuddZddIntersect */
00666 
00667 
00679 DdNode *
00680 cuddZddDiff(
00681   DdManager * zdd,
00682   DdNode * P,
00683   DdNode * Q)
00684 {
00685     int         p_top, q_top;
00686     DdNode      *empty = DD_ZERO(zdd), *t, *e, *res;
00687     DdManager   *table = zdd;
00688 
00689     statLine(zdd);
00690     if (P == empty)
00691         return(empty);
00692     if (Q == empty)
00693         return(P);
00694     if (P == Q)
00695         return(empty);
00696 
00697     /* Check cache.  The cache is shared by Cudd_zddDiffConst(). */
00698     res = cuddCacheLookup2Zdd(table, cuddZddDiff, P, Q);
00699     if (res != NULL && res != DD_NON_CONSTANT)
00700         return(res);
00701 
00702     if (cuddIsConstant(P))
00703         p_top = P->index;
00704     else
00705         p_top = zdd->permZ[P->index];
00706     if (cuddIsConstant(Q))
00707         q_top = Q->index;
00708     else
00709         q_top = zdd->permZ[Q->index];
00710     if (p_top < q_top) {
00711         e = cuddZddDiff(zdd, cuddE(P), Q);
00712         if (e == NULL) return(NULL);
00713         cuddRef(e);
00714         res = cuddZddGetNode(zdd, P->index, cuddT(P), e);
00715         if (res == NULL) {
00716             Cudd_RecursiveDerefZdd(table, e);
00717             return(NULL);
00718         }
00719         cuddDeref(e);
00720     } else if (p_top > q_top) {
00721         res = cuddZddDiff(zdd, P, cuddE(Q));
00722         if (res == NULL) return(NULL);
00723     } else {
00724         t = cuddZddDiff(zdd, cuddT(P), cuddT(Q));
00725         if (t == NULL) return(NULL);
00726         cuddRef(t);
00727         e = cuddZddDiff(zdd, cuddE(P), cuddE(Q));
00728         if (e == NULL) {
00729             Cudd_RecursiveDerefZdd(table, t);
00730             return(NULL);
00731         }
00732         cuddRef(e);
00733         res = cuddZddGetNode(zdd, P->index, t, e);
00734         if (res == NULL) {
00735             Cudd_RecursiveDerefZdd(table, t);
00736             Cudd_RecursiveDerefZdd(table, e);
00737             return(NULL);
00738         }
00739         cuddDeref(t);
00740         cuddDeref(e);
00741     }
00742 
00743     cuddCacheInsert2(table, cuddZddDiff, P, Q, res);
00744 
00745     return(res);
00746 
00747 } /* end of cuddZddDiff */
00748 
00749 
00761 DdNode *
00762 cuddZddChangeAux(
00763   DdManager * zdd,
00764   DdNode * P,
00765   DdNode * zvar)
00766 {
00767     int         top_var, level;
00768     DdNode      *res, *t, *e;
00769     DdNode      *base = DD_ONE(zdd);
00770     DdNode      *empty = DD_ZERO(zdd);
00771 
00772     statLine(zdd);
00773     if (P == empty)
00774         return(empty);
00775     if (P == base)
00776         return(zvar);
00777 
00778     /* Check cache. */
00779     res = cuddCacheLookup2Zdd(zdd, cuddZddChangeAux, P, zvar);
00780     if (res != NULL)
00781         return(res);
00782 
00783     top_var = zdd->permZ[P->index];
00784     level = zdd->permZ[zvar->index];
00785 
00786     if (top_var > level) {
00787         res = cuddZddGetNode(zdd, zvar->index, P, DD_ZERO(zdd));
00788         if (res == NULL) return(NULL);
00789     } else if (top_var == level) {
00790         res = cuddZddGetNode(zdd, zvar->index, cuddE(P), cuddT(P));
00791         if (res == NULL) return(NULL);
00792     } else {
00793         t = cuddZddChangeAux(zdd, cuddT(P), zvar);
00794         if (t == NULL) return(NULL);
00795         cuddRef(t);
00796         e = cuddZddChangeAux(zdd, cuddE(P), zvar);
00797         if (e == NULL) {
00798             Cudd_RecursiveDerefZdd(zdd, t);
00799             return(NULL);
00800         }
00801         cuddRef(e);
00802         res = cuddZddGetNode(zdd, P->index, t, e);
00803         if (res == NULL) {
00804             Cudd_RecursiveDerefZdd(zdd, t);
00805             Cudd_RecursiveDerefZdd(zdd, e);
00806             return(NULL);
00807         }
00808         cuddDeref(t);
00809         cuddDeref(e);
00810     }
00811 
00812     cuddCacheInsert2(zdd, cuddZddChangeAux, P, zvar, res);
00813 
00814     return(res);
00815 
00816 } /* end of cuddZddChangeAux */
00817 
00818 
00836 DdNode *
00837 cuddZddSubset1(
00838   DdManager * dd,
00839   DdNode * P,
00840   int  var)
00841 {
00842     DdNode      *zvar, *r;
00843     DdNode      *base, *empty;
00844 
00845     base = DD_ONE(dd);
00846     empty = DD_ZERO(dd);
00847 
00848     zvar = cuddUniqueInterZdd(dd, var, base, empty);
00849     if (zvar == NULL) {
00850         return(NULL);
00851     } else {
00852         cuddRef(zvar);
00853         r = zdd_subset1_aux(dd, P, zvar);
00854         if (r == NULL) {
00855             Cudd_RecursiveDerefZdd(dd, zvar);
00856             return(NULL);
00857         }
00858         cuddRef(r);
00859         Cudd_RecursiveDerefZdd(dd, zvar);
00860     }
00861 
00862     cuddDeref(r);
00863     return(r);
00864 
00865 } /* end of cuddZddSubset1 */
00866 
00867 
00885 DdNode *
00886 cuddZddSubset0(
00887   DdManager * dd,
00888   DdNode * P,
00889   int  var)
00890 {
00891     DdNode      *zvar, *r;
00892     DdNode      *base, *empty;
00893 
00894     base = DD_ONE(dd);
00895     empty = DD_ZERO(dd);
00896 
00897     zvar = cuddUniqueInterZdd(dd, var, base, empty);
00898     if (zvar == NULL) {
00899         return(NULL);
00900     } else {
00901         cuddRef(zvar);
00902         r = zdd_subset0_aux(dd, P, zvar);
00903         if (r == NULL) {
00904             Cudd_RecursiveDerefZdd(dd, zvar);
00905             return(NULL);
00906         }
00907         cuddRef(r);
00908         Cudd_RecursiveDerefZdd(dd, zvar);
00909     }
00910 
00911     cuddDeref(r);
00912     return(r);
00913 
00914 } /* end of cuddZddSubset0 */
00915 
00916 
00933 DdNode *
00934 cuddZddChange(
00935   DdManager * dd,
00936   DdNode * P,
00937   int  var)
00938 {
00939     DdNode      *zvar, *res;
00940 
00941     zvar = cuddUniqueInterZdd(dd, var, DD_ONE(dd), DD_ZERO(dd));
00942     if (zvar == NULL) return(NULL);
00943     cuddRef(zvar);
00944 
00945     res = cuddZddChangeAux(dd, P, zvar);
00946     if (res == NULL) {
00947         Cudd_RecursiveDerefZdd(dd,zvar);
00948         return(NULL);
00949     }
00950     cuddRef(res);
00951     Cudd_RecursiveDerefZdd(dd,zvar);
00952     cuddDeref(res);
00953     return(res);
00954 
00955 } /* end of cuddZddChange */
00956 
00957 
00958 /*---------------------------------------------------------------------------*/
00959 /* Definition of static functions                                            */
00960 /*---------------------------------------------------------------------------*/
00961 
00962 
00974 static DdNode *
00975 zdd_subset1_aux(
00976   DdManager * zdd,
00977   DdNode * P,
00978   DdNode * zvar)
00979 {
00980     int         top_var, level;
00981     DdNode      *res, *t, *e;
00982     DdNode      *base, *empty;
00983 
00984     statLine(zdd);
00985     base = DD_ONE(zdd);
00986     empty = DD_ZERO(zdd);
00987 
00988     /* Check cache. */
00989     res = cuddCacheLookup2Zdd(zdd, zdd_subset1_aux, P, zvar);
00990     if (res != NULL)
00991         return(res);
00992 
00993     if (cuddIsConstant(P)) {
00994         res = empty;
00995         cuddCacheInsert2(zdd, zdd_subset1_aux, P, zvar, res);
00996         return(res);
00997     }
00998 
00999     top_var = zdd->permZ[P->index];
01000     level = zdd->permZ[zvar->index];
01001 
01002     if (top_var > level) {
01003         res = empty;
01004     } else if (top_var == level) {
01005         res = cuddT(P);
01006     } else {
01007         t = zdd_subset1_aux(zdd, cuddT(P), zvar);
01008         if (t == NULL) return(NULL);
01009         cuddRef(t);
01010         e = zdd_subset1_aux(zdd, cuddE(P), zvar);
01011         if (e == NULL) {
01012             Cudd_RecursiveDerefZdd(zdd, t);
01013             return(NULL);
01014         }
01015         cuddRef(e);
01016         res = cuddZddGetNode(zdd, P->index, t, e);
01017         if (res == NULL) {
01018             Cudd_RecursiveDerefZdd(zdd, t);
01019             Cudd_RecursiveDerefZdd(zdd, e);
01020             return(NULL);
01021         }
01022         cuddDeref(t);
01023         cuddDeref(e);
01024     }
01025 
01026     cuddCacheInsert2(zdd, zdd_subset1_aux, P, zvar, res);
01027 
01028     return(res);
01029 
01030 } /* end of zdd_subset1_aux */
01031 
01032 
01044 static DdNode *
01045 zdd_subset0_aux(
01046   DdManager * zdd,
01047   DdNode * P,
01048   DdNode * zvar)
01049 {
01050     int         top_var, level;
01051     DdNode      *res, *t, *e;
01052     DdNode      *base, *empty;
01053 
01054     statLine(zdd);
01055     base = DD_ONE(zdd);
01056     empty = DD_ZERO(zdd);
01057 
01058     /* Check cache. */
01059     res = cuddCacheLookup2Zdd(zdd, zdd_subset0_aux, P, zvar);
01060     if (res != NULL)
01061         return(res);
01062 
01063     if (cuddIsConstant(P)) {
01064         res = P;
01065         cuddCacheInsert2(zdd, zdd_subset0_aux, P, zvar, res);
01066         return(res);
01067     }
01068 
01069     top_var = zdd->permZ[P->index];
01070     level = zdd->permZ[zvar->index];
01071 
01072     if (top_var > level) {
01073         res = P;
01074     }
01075     else if (top_var == level) {
01076         res = cuddE(P);
01077     }
01078     else {
01079         t = zdd_subset0_aux(zdd, cuddT(P), zvar);
01080         if (t == NULL) return(NULL);
01081         cuddRef(t);
01082         e = zdd_subset0_aux(zdd, cuddE(P), zvar);
01083         if (e == NULL) {
01084             Cudd_RecursiveDerefZdd(zdd, t);
01085             return(NULL);
01086         }
01087         cuddRef(e);
01088         res = cuddZddGetNode(zdd, P->index, t, e);
01089         if (res == NULL) {
01090             Cudd_RecursiveDerefZdd(zdd, t);
01091             Cudd_RecursiveDerefZdd(zdd, e);
01092             return(NULL);
01093         }
01094         cuddDeref(t);
01095         cuddDeref(e);
01096     }
01097 
01098     cuddCacheInsert2(zdd, zdd_subset0_aux, P, zvar, res);
01099 
01100     return(res);
01101 
01102 } /* end of zdd_subset0_aux */
01103 
01104 
01117 static void
01118 zddVarToConst(
01119   DdNode * f,
01120   DdNode ** gp,
01121   DdNode ** hp,
01122   DdNode * base,
01123   DdNode * empty)
01124 {
01125     DdNode *g = *gp;
01126     DdNode *h = *hp;
01127 
01128     if (f == g) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */
01129         *gp = base;
01130     }
01131 
01132     if (f == h) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */
01133         *hp = empty;
01134     }
01135 
01136 } /* end of zddVarToConst */
01137