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

00001 
00076 #include "util.h"
00077 #include "cuddInt.h"
00078 
00079 /*---------------------------------------------------------------------------*/
00080 /* Constant declarations                                                     */
00081 /*---------------------------------------------------------------------------*/
00082 
00083 
00084 /*---------------------------------------------------------------------------*/
00085 /* Stucture declarations                                                     */
00086 /*---------------------------------------------------------------------------*/
00087 
00088 
00089 /*---------------------------------------------------------------------------*/
00090 /* Type declarations                                                         */
00091 /*---------------------------------------------------------------------------*/
00092 
00093 
00094 /*---------------------------------------------------------------------------*/
00095 /* Variable declarations                                                     */
00096 /*---------------------------------------------------------------------------*/
00097 
00098 #ifndef lint
00099 static char rcsid[] DD_UNUSED = "$Id: cuddZddSetop.c,v 1.25 2004/08/13 18:04:54 fabio Exp $";
00100 #endif
00101 
00102 /*---------------------------------------------------------------------------*/
00103 /* Macro declarations                                                        */
00104 /*---------------------------------------------------------------------------*/
00105 
00106 #ifdef __cplusplus
00107 extern "C" {
00108 #endif
00109 
00112 /*---------------------------------------------------------------------------*/
00113 /* Static function prototypes                                                */
00114 /*---------------------------------------------------------------------------*/
00115 
00116 static DdNode * zdd_subset1_aux (DdManager *zdd, DdNode *P, DdNode *zvar);
00117 static DdNode * zdd_subset0_aux (DdManager *zdd, DdNode *P, DdNode *zvar);
00118 static void zddVarToConst (DdNode *f, DdNode **gp, DdNode **hp, DdNode *base, DdNode *empty);
00119 
00122 #ifdef __cplusplus
00123 }
00124 #endif
00125 
00126 /*---------------------------------------------------------------------------*/
00127 /* Definition of exported functions                                          */
00128 /*---------------------------------------------------------------------------*/
00129 
00130 
00143 DdNode *
00144 Cudd_zddIte(
00145   DdManager * dd,
00146   DdNode * f,
00147   DdNode * g,
00148   DdNode * h)
00149 {
00150     DdNode *res;
00151 
00152     do {
00153         dd->reordered = 0;
00154         res = cuddZddIte(dd, f, g, h);
00155     } while (dd->reordered == 1);
00156     return(res);
00157 
00158 } /* end of Cudd_zddIte */
00159 
00160 
00173 DdNode *
00174 Cudd_zddUnion(
00175   DdManager * dd,
00176   DdNode * P,
00177   DdNode * Q)
00178 {
00179     DdNode *res;
00180 
00181     do {
00182         dd->reordered = 0;
00183         res = cuddZddUnion(dd, P, Q);
00184     } while (dd->reordered == 1);
00185     return(res);
00186 
00187 } /* end of Cudd_zddUnion */
00188 
00189 
00202 DdNode *
00203 Cudd_zddIntersect(
00204   DdManager * dd,
00205   DdNode * P,
00206   DdNode * Q)
00207 {
00208     DdNode *res;
00209 
00210     do {
00211         dd->reordered = 0;
00212         res = cuddZddIntersect(dd, P, Q);
00213     } while (dd->reordered == 1);
00214     return(res);
00215 
00216 } /* end of Cudd_zddIntersect */
00217 
00218 
00231 DdNode *
00232 Cudd_zddDiff(
00233   DdManager * dd,
00234   DdNode * P,
00235   DdNode * Q)
00236 {
00237     DdNode *res;
00238 
00239     do {
00240         dd->reordered = 0;
00241         res = cuddZddDiff(dd, P, Q);
00242     } while (dd->reordered == 1);
00243     return(res);
00244 
00245 } /* end of Cudd_zddDiff */
00246 
00247 
00261 DdNode *
00262 Cudd_zddDiffConst(
00263   DdManager * zdd,
00264   DdNode * P,
00265   DdNode * Q)
00266 {
00267     int         p_top, q_top;
00268     DdNode      *empty = DD_ZERO(zdd), *t, *res;
00269     DdManager   *table = zdd;
00270 
00271     statLine(zdd);
00272     if (P == empty)
00273         return(empty);
00274     if (Q == empty)
00275         return(P);
00276     if (P == Q)
00277         return(empty);
00278 
00279     /* Check cache.  The cache is shared by cuddZddDiff(). */
00280     res = cuddCacheLookup2Zdd(table, cuddZddDiff, P, Q);
00281     if (res != NULL)
00282         return(res);
00283 
00284     if (cuddIsConstant(P))
00285         p_top = P->index;
00286     else
00287         p_top = zdd->permZ[P->index];
00288     if (cuddIsConstant(Q))
00289         q_top = Q->index;
00290     else
00291         q_top = zdd->permZ[Q->index];
00292     if (p_top < q_top) {
00293         res = DD_NON_CONSTANT;
00294     } else if (p_top > q_top) {
00295         res = Cudd_zddDiffConst(zdd, P, cuddE(Q));
00296     } else {
00297         t = Cudd_zddDiffConst(zdd, cuddT(P), cuddT(Q));
00298         if (t != empty)
00299             res = DD_NON_CONSTANT;
00300         else
00301             res = Cudd_zddDiffConst(zdd, cuddE(P), cuddE(Q));
00302     }
00303 
00304     cuddCacheInsert2(table, cuddZddDiff, P, Q, res);
00305 
00306     return(res);
00307 
00308 } /* end of Cudd_zddDiffConst */
00309 
00310 
00325 DdNode *
00326 Cudd_zddSubset1(
00327   DdManager * dd,
00328   DdNode * P,
00329   int  var)
00330 {
00331     DdNode      *r;
00332 
00333     do {
00334         dd->reordered = 0;
00335         r = cuddZddSubset1(dd, P, var);
00336     } while (dd->reordered == 1);
00337 
00338     return(r);
00339 
00340 } /* end of Cudd_zddSubset1 */
00341 
00342 
00357 DdNode *
00358 Cudd_zddSubset0(
00359   DdManager * dd,
00360   DdNode * P,
00361   int  var)
00362 {
00363     DdNode      *r;
00364 
00365     do {
00366         dd->reordered = 0;
00367         r = cuddZddSubset0(dd, P, var);
00368     } while (dd->reordered == 1);
00369 
00370     return(r);
00371 
00372 } /* end of Cudd_zddSubset0 */
00373 
00374 
00387 DdNode *
00388 Cudd_zddChange(
00389   DdManager * dd,
00390   DdNode * P,
00391   int  var)
00392 {
00393     DdNode      *res;
00394 
00395     if ((unsigned int) var >= CUDD_MAXINDEX - 1) return(NULL);
00396     
00397     do {
00398         dd->reordered = 0;
00399         res = cuddZddChange(dd, P, var);
00400     } while (dd->reordered == 1);
00401     return(res);
00402 
00403 } /* end of Cudd_zddChange */
00404 
00405 
00406 /*---------------------------------------------------------------------------*/
00407 /* Definition of internal functions                                          */
00408 /*---------------------------------------------------------------------------*/
00409 
00410 
00422 DdNode *
00423 cuddZddIte(
00424   DdManager * dd,
00425   DdNode * f,
00426   DdNode * g,
00427   DdNode * h)
00428 {
00429     DdNode *tautology, *empty;
00430     DdNode *r,*Gv,*Gvn,*Hv,*Hvn,*t,*e;
00431     unsigned int topf,topg,toph,v,top;
00432     int index;
00433 
00434     statLine(dd);
00435     /* Trivial cases. */
00436     /* One variable cases. */
00437     if (f == (empty = DD_ZERO(dd))) {   /* ITE(0,G,H) = H */
00438         return(h);
00439     }
00440     topf = cuddIZ(dd,f->index);
00441     topg = cuddIZ(dd,g->index);
00442     toph = cuddIZ(dd,h->index);
00443     v = ddMin(topg,toph);
00444     top  = ddMin(topf,v);
00445 
00446     tautology = (top == CUDD_MAXINDEX) ? DD_ONE(dd) : dd->univ[top];
00447     if (f == tautology) {                       /* ITE(1,G,H) = G */
00448         return(g);
00449     }
00450 
00451     /* From now on, f is known to not be a constant. */
00452     zddVarToConst(f,&g,&h,tautology,empty);
00453 
00454     /* Check remaining one variable cases. */
00455     if (g == h) {                       /* ITE(F,G,G) = G */
00456         return(g);
00457     }
00458 
00459     if (g == tautology) {                       /* ITE(F,1,0) = F */
00460         if (h == empty) return(f);
00461     }
00462 
00463     /* Check cache. */
00464     r = cuddCacheLookupZdd(dd,DD_ZDD_ITE_TAG,f,g,h);
00465     if (r != NULL) {
00466         return(r);
00467     }
00468 
00469     /* Recompute these because they may have changed in zddVarToConst. */
00470     topg = cuddIZ(dd,g->index);
00471     toph = cuddIZ(dd,h->index);
00472     v = ddMin(topg,toph);
00473 
00474     if (topf < v) {
00475         r = cuddZddIte(dd,cuddE(f),g,h);
00476         if (r == NULL) return(NULL);
00477     } else if (topf > v) {
00478         if (topg > v) {
00479             Gvn = g;
00480             index = h->index;
00481         } else {
00482             Gvn = cuddE(g);
00483             index = g->index;
00484         }
00485         if (toph > v) {
00486             Hv = empty; Hvn = h;
00487         } else {
00488             Hv = cuddT(h); Hvn = cuddE(h);
00489         }
00490         e = cuddZddIte(dd,f,Gvn,Hvn);
00491         if (e == NULL) return(NULL);
00492         cuddRef(e);
00493         r = cuddZddGetNode(dd,index,Hv,e);
00494         if (r == NULL) {
00495             Cudd_RecursiveDerefZdd(dd,e);
00496             return(NULL);
00497         }
00498         cuddDeref(e);
00499     } else {
00500         index = f->index;
00501         if (topg > v) {
00502             Gv = empty; Gvn = g;
00503         } else {
00504             Gv = cuddT(g); Gvn = cuddE(g);
00505         }
00506         if (toph > v) {
00507             Hv = empty; Hvn = h;
00508         } else {
00509             Hv = cuddT(h); Hvn = cuddE(h);
00510         }
00511         e = cuddZddIte(dd,cuddE(f),Gvn,Hvn);
00512         if (e == NULL) return(NULL);
00513         cuddRef(e);
00514         t = cuddZddIte(dd,cuddT(f),Gv,Hv);
00515         if (t == NULL) {
00516             Cudd_RecursiveDerefZdd(dd,e);
00517             return(NULL);
00518         }
00519         cuddRef(t);
00520         r = cuddZddGetNode(dd,index,t,e);
00521         if (r == NULL) {
00522             Cudd_RecursiveDerefZdd(dd,e);
00523             Cudd_RecursiveDerefZdd(dd,t);
00524             return(NULL);
00525         }
00526         cuddDeref(t);
00527         cuddDeref(e);
00528     }
00529 
00530     cuddCacheInsert(dd,DD_ZDD_ITE_TAG,f,g,h,r);
00531 
00532     return(r);
00533 
00534 } /* end of cuddZddIte */
00535 
00536 
00548 DdNode *
00549 cuddZddUnion(
00550   DdManager * zdd,
00551   DdNode * P,
00552   DdNode * Q)
00553 {
00554     int         p_top, q_top;
00555     DdNode      *empty = DD_ZERO(zdd), *t, *e, *res;
00556     DdManager   *table = zdd;
00557 
00558     statLine(zdd);
00559     if (P == empty)
00560         return(Q);
00561     if (Q == empty)
00562         return(P);
00563     if (P == Q)
00564         return(P);
00565 
00566     /* Check cache */
00567     res = cuddCacheLookup2Zdd(table, cuddZddUnion, P, Q);
00568     if (res != NULL)
00569         return(res);
00570 
00571     if (cuddIsConstant(P))
00572         p_top = P->index;
00573     else
00574         p_top = zdd->permZ[P->index];
00575     if (cuddIsConstant(Q))
00576         q_top = Q->index;
00577     else
00578         q_top = zdd->permZ[Q->index];
00579     if (p_top < q_top) {
00580         e = cuddZddUnion(zdd, cuddE(P), Q);
00581         if (e == NULL) return (NULL);
00582         cuddRef(e);
00583         res = cuddZddGetNode(zdd, P->index, cuddT(P), e);
00584         if (res == NULL) {
00585             Cudd_RecursiveDerefZdd(table, e);
00586             return(NULL);
00587         }
00588         cuddDeref(e);
00589     } else if (p_top > q_top) {
00590         e = cuddZddUnion(zdd, P, cuddE(Q));
00591         if (e == NULL) return(NULL);
00592         cuddRef(e);
00593         res = cuddZddGetNode(zdd, Q->index, cuddT(Q), e);
00594         if (res == NULL) {
00595             Cudd_RecursiveDerefZdd(table, e);
00596             return(NULL);
00597         }
00598         cuddDeref(e);
00599     } else {
00600         t = cuddZddUnion(zdd, cuddT(P), cuddT(Q));
00601         if (t == NULL) return(NULL);
00602         cuddRef(t);
00603         e = cuddZddUnion(zdd, cuddE(P), cuddE(Q));
00604         if (e == NULL) {
00605             Cudd_RecursiveDerefZdd(table, t);
00606             return(NULL);
00607         }
00608         cuddRef(e);
00609         res = cuddZddGetNode(zdd, P->index, t, e);
00610         if (res == NULL) {
00611             Cudd_RecursiveDerefZdd(table, t);
00612             Cudd_RecursiveDerefZdd(table, e);
00613             return(NULL);
00614         }
00615         cuddDeref(t);
00616         cuddDeref(e);
00617     }
00618 
00619     cuddCacheInsert2(table, cuddZddUnion, P, Q, res);
00620 
00621     return(res);
00622 
00623 } /* end of cuddZddUnion */
00624 
00625 
00637 DdNode *
00638 cuddZddIntersect(
00639   DdManager * zdd,
00640   DdNode * P,
00641   DdNode * Q)
00642 {
00643     int         p_top, q_top;
00644     DdNode      *empty = DD_ZERO(zdd), *t, *e, *res;
00645     DdManager   *table = zdd;
00646 
00647     statLine(zdd);
00648     if (P == empty)
00649         return(empty);
00650     if (Q == empty)
00651         return(empty);
00652     if (P == Q)
00653         return(P);
00654 
00655     /* Check cache. */
00656     res = cuddCacheLookup2Zdd(table, cuddZddIntersect, P, Q);
00657     if (res != NULL)
00658         return(res);
00659 
00660     if (cuddIsConstant(P))
00661         p_top = P->index;
00662     else
00663         p_top = zdd->permZ[P->index];
00664     if (cuddIsConstant(Q))
00665         q_top = Q->index;
00666     else
00667         q_top = zdd->permZ[Q->index];
00668     if (p_top < q_top) {
00669         res = cuddZddIntersect(zdd, cuddE(P), Q);
00670         if (res == NULL) return(NULL);
00671     } else if (p_top > q_top) {
00672         res = cuddZddIntersect(zdd, P, cuddE(Q));
00673         if (res == NULL) return(NULL);
00674     } else {
00675         t = cuddZddIntersect(zdd, cuddT(P), cuddT(Q));
00676         if (t == NULL) return(NULL);
00677         cuddRef(t);
00678         e = cuddZddIntersect(zdd, cuddE(P), cuddE(Q));
00679         if (e == NULL) {
00680             Cudd_RecursiveDerefZdd(table, t);
00681             return(NULL);
00682         }
00683         cuddRef(e);
00684         res = cuddZddGetNode(zdd, P->index, t, e);
00685         if (res == NULL) {
00686             Cudd_RecursiveDerefZdd(table, t);
00687             Cudd_RecursiveDerefZdd(table, e);
00688             return(NULL);
00689         }
00690         cuddDeref(t);
00691         cuddDeref(e);
00692     }
00693 
00694     cuddCacheInsert2(table, cuddZddIntersect, P, Q, res);
00695 
00696     return(res);
00697 
00698 } /* end of cuddZddIntersect */
00699 
00700 
00712 DdNode *
00713 cuddZddDiff(
00714   DdManager * zdd,
00715   DdNode * P,
00716   DdNode * Q)
00717 {
00718     int         p_top, q_top;
00719     DdNode      *empty = DD_ZERO(zdd), *t, *e, *res;
00720     DdManager   *table = zdd;
00721 
00722     statLine(zdd);
00723     if (P == empty)
00724         return(empty);
00725     if (Q == empty)
00726         return(P);
00727     if (P == Q)
00728         return(empty);
00729 
00730     /* Check cache.  The cache is shared by Cudd_zddDiffConst(). */
00731     res = cuddCacheLookup2Zdd(table, cuddZddDiff, P, Q);
00732     if (res != NULL && res != DD_NON_CONSTANT)
00733         return(res);
00734 
00735     if (cuddIsConstant(P))
00736         p_top = P->index;
00737     else
00738         p_top = zdd->permZ[P->index];
00739     if (cuddIsConstant(Q))
00740         q_top = Q->index;
00741     else
00742         q_top = zdd->permZ[Q->index];
00743     if (p_top < q_top) {
00744         e = cuddZddDiff(zdd, cuddE(P), Q);
00745         if (e == NULL) return(NULL);
00746         cuddRef(e);
00747         res = cuddZddGetNode(zdd, P->index, cuddT(P), e);
00748         if (res == NULL) {
00749             Cudd_RecursiveDerefZdd(table, e);
00750             return(NULL);
00751         }
00752         cuddDeref(e);
00753     } else if (p_top > q_top) {
00754         res = cuddZddDiff(zdd, P, cuddE(Q));
00755         if (res == NULL) return(NULL);
00756     } else {
00757         t = cuddZddDiff(zdd, cuddT(P), cuddT(Q));
00758         if (t == NULL) return(NULL);
00759         cuddRef(t);
00760         e = cuddZddDiff(zdd, cuddE(P), cuddE(Q));
00761         if (e == NULL) {
00762             Cudd_RecursiveDerefZdd(table, t);
00763             return(NULL);
00764         }
00765         cuddRef(e);
00766         res = cuddZddGetNode(zdd, P->index, t, e);
00767         if (res == NULL) {
00768             Cudd_RecursiveDerefZdd(table, t);
00769             Cudd_RecursiveDerefZdd(table, e);
00770             return(NULL);
00771         }
00772         cuddDeref(t);
00773         cuddDeref(e);
00774     }
00775 
00776     cuddCacheInsert2(table, cuddZddDiff, P, Q, res);
00777 
00778     return(res);
00779 
00780 } /* end of cuddZddDiff */
00781 
00782 
00794 DdNode *
00795 cuddZddChangeAux(
00796   DdManager * zdd,
00797   DdNode * P,
00798   DdNode * zvar)
00799 {
00800     int         top_var, level;
00801     DdNode      *res, *t, *e;
00802     DdNode      *base = DD_ONE(zdd);
00803     DdNode      *empty = DD_ZERO(zdd);
00804 
00805     statLine(zdd);
00806     if (P == empty)
00807         return(empty);
00808     if (P == base)
00809         return(zvar);
00810 
00811     /* Check cache. */
00812     res = cuddCacheLookup2Zdd(zdd, cuddZddChangeAux, P, zvar);
00813     if (res != NULL)
00814         return(res);
00815 
00816     top_var = zdd->permZ[P->index];
00817     level = zdd->permZ[zvar->index];
00818 
00819     if (top_var > level) {
00820         res = cuddZddGetNode(zdd, zvar->index, P, DD_ZERO(zdd));
00821         if (res == NULL) return(NULL);
00822     } else if (top_var == level) {
00823         res = cuddZddGetNode(zdd, zvar->index, cuddE(P), cuddT(P));
00824         if (res == NULL) return(NULL);
00825     } else {
00826         t = cuddZddChangeAux(zdd, cuddT(P), zvar);
00827         if (t == NULL) return(NULL);
00828         cuddRef(t);
00829         e = cuddZddChangeAux(zdd, cuddE(P), zvar);
00830         if (e == NULL) {
00831             Cudd_RecursiveDerefZdd(zdd, t);
00832             return(NULL);
00833         }
00834         cuddRef(e);
00835         res = cuddZddGetNode(zdd, P->index, t, e);
00836         if (res == NULL) {
00837             Cudd_RecursiveDerefZdd(zdd, t);
00838             Cudd_RecursiveDerefZdd(zdd, e);
00839             return(NULL);
00840         }
00841         cuddDeref(t);
00842         cuddDeref(e);
00843     }
00844 
00845     cuddCacheInsert2(zdd, cuddZddChangeAux, P, zvar, res);
00846 
00847     return(res);
00848 
00849 } /* end of cuddZddChangeAux */
00850 
00851 
00869 DdNode *
00870 cuddZddSubset1(
00871   DdManager * dd,
00872   DdNode * P,
00873   int  var)
00874 {
00875     DdNode      *zvar, *r;
00876     DdNode      *base, *empty;
00877 
00878     base = DD_ONE(dd);
00879     empty = DD_ZERO(dd);
00880 
00881     zvar = cuddUniqueInterZdd(dd, var, base, empty);
00882     if (zvar == NULL) {
00883         return(NULL);
00884     } else {
00885         cuddRef(zvar);
00886         r = zdd_subset1_aux(dd, P, zvar);
00887         if (r == NULL) {
00888             Cudd_RecursiveDerefZdd(dd, zvar);
00889             return(NULL);
00890         }
00891         cuddRef(r);
00892         Cudd_RecursiveDerefZdd(dd, zvar);
00893     }
00894 
00895     cuddDeref(r);
00896     return(r);
00897 
00898 } /* end of cuddZddSubset1 */
00899 
00900 
00918 DdNode *
00919 cuddZddSubset0(
00920   DdManager * dd,
00921   DdNode * P,
00922   int  var)
00923 {
00924     DdNode      *zvar, *r;
00925     DdNode      *base, *empty;
00926 
00927     base = DD_ONE(dd);
00928     empty = DD_ZERO(dd);
00929 
00930     zvar = cuddUniqueInterZdd(dd, var, base, empty);
00931     if (zvar == NULL) {
00932         return(NULL);
00933     } else {
00934         cuddRef(zvar);
00935         r = zdd_subset0_aux(dd, P, zvar);
00936         if (r == NULL) {
00937             Cudd_RecursiveDerefZdd(dd, zvar);
00938             return(NULL);
00939         }
00940         cuddRef(r);
00941         Cudd_RecursiveDerefZdd(dd, zvar);
00942     }
00943 
00944     cuddDeref(r);
00945     return(r);
00946 
00947 } /* end of cuddZddSubset0 */
00948 
00949 
00966 DdNode *
00967 cuddZddChange(
00968   DdManager * dd,
00969   DdNode * P,
00970   int  var)
00971 {
00972     DdNode      *zvar, *res;
00973 
00974     zvar = cuddUniqueInterZdd(dd, var, DD_ONE(dd), DD_ZERO(dd));
00975     if (zvar == NULL) return(NULL);
00976     cuddRef(zvar);
00977 
00978     res = cuddZddChangeAux(dd, P, zvar);
00979     if (res == NULL) {
00980         Cudd_RecursiveDerefZdd(dd,zvar);
00981         return(NULL);
00982     }
00983     cuddRef(res);
00984     Cudd_RecursiveDerefZdd(dd,zvar);
00985     cuddDeref(res);
00986     return(res);
00987 
00988 } /* end of cuddZddChange */
00989 
00990 
00991 /*---------------------------------------------------------------------------*/
00992 /* Definition of static functions                                            */
00993 /*---------------------------------------------------------------------------*/
00994 
00995 
01007 static DdNode *
01008 zdd_subset1_aux(
01009   DdManager * zdd,
01010   DdNode * P,
01011   DdNode * zvar)
01012 {
01013     int         top_var, level;
01014     DdNode      *res, *t, *e;
01015     DdNode      *empty;
01016 
01017     statLine(zdd);
01018     empty = DD_ZERO(zdd);
01019 
01020     /* Check cache. */
01021     res = cuddCacheLookup2Zdd(zdd, zdd_subset1_aux, P, zvar);
01022     if (res != NULL)
01023         return(res);
01024 
01025     if (cuddIsConstant(P)) {
01026         res = empty;
01027         cuddCacheInsert2(zdd, zdd_subset1_aux, P, zvar, res);
01028         return(res);
01029     }
01030 
01031     top_var = zdd->permZ[P->index];
01032     level = zdd->permZ[zvar->index];
01033 
01034     if (top_var > level) {
01035         res = empty;
01036     } else if (top_var == level) {
01037         res = cuddT(P);
01038     } else {
01039         t = zdd_subset1_aux(zdd, cuddT(P), zvar);
01040         if (t == NULL) return(NULL);
01041         cuddRef(t);
01042         e = zdd_subset1_aux(zdd, cuddE(P), zvar);
01043         if (e == NULL) {
01044             Cudd_RecursiveDerefZdd(zdd, t);
01045             return(NULL);
01046         }
01047         cuddRef(e);
01048         res = cuddZddGetNode(zdd, P->index, t, e);
01049         if (res == NULL) {
01050             Cudd_RecursiveDerefZdd(zdd, t);
01051             Cudd_RecursiveDerefZdd(zdd, e);
01052             return(NULL);
01053         }
01054         cuddDeref(t);
01055         cuddDeref(e);
01056     }
01057 
01058     cuddCacheInsert2(zdd, zdd_subset1_aux, P, zvar, res);
01059 
01060     return(res);
01061 
01062 } /* end of zdd_subset1_aux */
01063 
01064 
01076 static DdNode *
01077 zdd_subset0_aux(
01078   DdManager * zdd,
01079   DdNode * P,
01080   DdNode * zvar)
01081 {
01082     int         top_var, level;
01083     DdNode      *res, *t, *e;
01084 
01085     statLine(zdd);
01086 
01087     /* Check cache. */
01088     res = cuddCacheLookup2Zdd(zdd, zdd_subset0_aux, P, zvar);
01089     if (res != NULL)
01090         return(res);
01091 
01092     if (cuddIsConstant(P)) {
01093         res = P;
01094         cuddCacheInsert2(zdd, zdd_subset0_aux, P, zvar, res);
01095         return(res);
01096     }
01097 
01098     top_var = zdd->permZ[P->index];
01099     level = zdd->permZ[zvar->index];
01100 
01101     if (top_var > level) {
01102         res = P;
01103     }
01104     else if (top_var == level) {
01105         res = cuddE(P);
01106     }
01107     else {
01108         t = zdd_subset0_aux(zdd, cuddT(P), zvar);
01109         if (t == NULL) return(NULL);
01110         cuddRef(t);
01111         e = zdd_subset0_aux(zdd, cuddE(P), zvar);
01112         if (e == NULL) {
01113             Cudd_RecursiveDerefZdd(zdd, t);
01114             return(NULL);
01115         }
01116         cuddRef(e);
01117         res = cuddZddGetNode(zdd, P->index, t, e);
01118         if (res == NULL) {
01119             Cudd_RecursiveDerefZdd(zdd, t);
01120             Cudd_RecursiveDerefZdd(zdd, e);
01121             return(NULL);
01122         }
01123         cuddDeref(t);
01124         cuddDeref(e);
01125     }
01126 
01127     cuddCacheInsert2(zdd, zdd_subset0_aux, P, zvar, res);
01128 
01129     return(res);
01130 
01131 } /* end of zdd_subset0_aux */
01132 
01133 
01146 static void
01147 zddVarToConst(
01148   DdNode * f,
01149   DdNode ** gp,
01150   DdNode ** hp,
01151   DdNode * base,
01152   DdNode * empty)
01153 {
01154     DdNode *g = *gp;
01155     DdNode *h = *hp;
01156 
01157     if (f == g) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */
01158         *gp = base;
01159     }
01160 
01161     if (f == h) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */
01162         *hp = empty;
01163     }
01164 
01165 } /* end of zddVarToConst */
01166