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

00001 
00064 #include "util.h"
00065 #include "cuddInt.h"
00066 
00067 /*---------------------------------------------------------------------------*/
00068 /* Constant declarations                                                     */
00069 /*---------------------------------------------------------------------------*/
00070 
00071 
00072 /*---------------------------------------------------------------------------*/
00073 /* Stucture declarations                                                     */
00074 /*---------------------------------------------------------------------------*/
00075 
00076 
00077 /*---------------------------------------------------------------------------*/
00078 /* Type declarations                                                         */
00079 /*---------------------------------------------------------------------------*/
00080 
00081 
00082 /*---------------------------------------------------------------------------*/
00083 /* Variable declarations                                                     */
00084 /*---------------------------------------------------------------------------*/
00085 
00086 #ifndef lint
00087 static char rcsid[] DD_UNUSED = "$Id: cuddZddIsop.c,v 1.20 2009/02/19 16:26:12 fabio Exp $";
00088 #endif
00089 
00090 /*---------------------------------------------------------------------------*/
00091 /* Macro declarations                                                        */
00092 /*---------------------------------------------------------------------------*/
00093 
00094 
00097 /*---------------------------------------------------------------------------*/
00098 /* Static function prototypes                                                */
00099 /*---------------------------------------------------------------------------*/
00100 
00101 
00104 /*---------------------------------------------------------------------------*/
00105 /* Definition of exported functions                                          */
00106 /*---------------------------------------------------------------------------*/
00107 
00131 DdNode  *
00132 Cudd_zddIsop(
00133   DdManager * dd,
00134   DdNode * L,
00135   DdNode * U,
00136   DdNode ** zdd_I)
00137 {
00138     DdNode      *res;
00139     int         autoDynZ;
00140 
00141     autoDynZ = dd->autoDynZ;
00142     dd->autoDynZ = 0;
00143 
00144     do {
00145         dd->reordered = 0;
00146         res = cuddZddIsop(dd, L, U, zdd_I);
00147     } while (dd->reordered == 1);
00148     dd->autoDynZ = autoDynZ;
00149     return(res);
00150 
00151 } /* end of Cudd_zddIsop */
00152 
00153 
00169 DdNode  *
00170 Cudd_bddIsop(
00171   DdManager * dd,
00172   DdNode * L,
00173   DdNode * U)
00174 {
00175     DdNode      *res;
00176 
00177     do {
00178         dd->reordered = 0;
00179         res = cuddBddIsop(dd, L, U);
00180     } while (dd->reordered == 1);
00181     return(res);
00182 
00183 } /* end of Cudd_bddIsop */
00184 
00185 
00198 DdNode  *
00199 Cudd_MakeBddFromZddCover(
00200   DdManager * dd,
00201   DdNode * node)
00202 {
00203     DdNode      *res;
00204 
00205     do {
00206         dd->reordered = 0;
00207         res = cuddMakeBddFromZddCover(dd, node);
00208     } while (dd->reordered == 1);
00209     return(res);
00210 } /* end of Cudd_MakeBddFromZddCover */
00211 
00212 
00213 /*---------------------------------------------------------------------------*/
00214 /* Definition of internal functions                                          */
00215 /*---------------------------------------------------------------------------*/
00216 
00217 
00229 DdNode  *
00230 cuddZddIsop(
00231   DdManager * dd,
00232   DdNode * L,
00233   DdNode * U,
00234   DdNode ** zdd_I)
00235 {
00236     DdNode      *one = DD_ONE(dd);
00237     DdNode      *zero = Cudd_Not(one);
00238     DdNode      *zdd_one = DD_ONE(dd);
00239     DdNode      *zdd_zero = DD_ZERO(dd);
00240     int         v, top_l, top_u;
00241     DdNode      *Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud;
00242     DdNode      *Lsuper0, *Usuper0, *Lsuper1, *Usuper1;
00243     DdNode      *Isub0, *Isub1, *Id;
00244     DdNode      *zdd_Isub0, *zdd_Isub1, *zdd_Id;
00245     DdNode      *x;
00246     DdNode      *term0, *term1, *sum;
00247     DdNode      *Lv, *Uv, *Lnv, *Unv;
00248     DdNode      *r, *y, *z;
00249     int         index;
00250     DD_CTFP     cacheOp;
00251 
00252     statLine(dd);
00253     if (L == zero) {
00254         *zdd_I = zdd_zero;
00255         return(zero);
00256     }
00257     if (U == one) {
00258         *zdd_I = zdd_one;
00259         return(one);
00260     }
00261 
00262     if (U == zero || L == one) {
00263         printf("*** ERROR : illegal condition for ISOP (U < L).\n");
00264         exit(1);
00265     }
00266 
00267     /* Check the cache. We store two results for each recursive call.
00268     ** One is the BDD, and the other is the ZDD. Both are needed.
00269     ** Hence we need a double hit in the cache to terminate the
00270     ** recursion. Clearly, collisions may evict only one of the two
00271     ** results. */
00272     cacheOp = (DD_CTFP) cuddZddIsop;
00273     r = cuddCacheLookup2(dd, cuddBddIsop, L, U);
00274     if (r) {
00275         *zdd_I = cuddCacheLookup2Zdd(dd, cacheOp, L, U);
00276         if (*zdd_I)
00277             return(r);
00278         else {
00279             /* The BDD result may have been dead. In that case
00280             ** cuddCacheLookup2 would have called cuddReclaim,
00281             ** whose effects we now have to undo. */
00282             cuddRef(r);
00283             Cudd_RecursiveDeref(dd, r);
00284         }
00285     }
00286 
00287     top_l = dd->perm[Cudd_Regular(L)->index];
00288     top_u = dd->perm[Cudd_Regular(U)->index];
00289     v = ddMin(top_l, top_u);
00290 
00291     /* Compute cofactors. */
00292     if (top_l == v) {
00293         index = Cudd_Regular(L)->index;
00294         Lv = Cudd_T(L);
00295         Lnv = Cudd_E(L);
00296         if (Cudd_IsComplement(L)) {
00297             Lv = Cudd_Not(Lv);
00298             Lnv = Cudd_Not(Lnv);
00299         }
00300     }
00301     else {
00302         index = Cudd_Regular(U)->index;
00303         Lv = Lnv = L;
00304     }
00305 
00306     if (top_u == v) {
00307         Uv = Cudd_T(U);
00308         Unv = Cudd_E(U);
00309         if (Cudd_IsComplement(U)) {
00310             Uv = Cudd_Not(Uv);
00311             Unv = Cudd_Not(Unv);
00312         }
00313     }
00314     else {
00315         Uv = Unv = U;
00316     }
00317 
00318     Lsub0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Uv));
00319     if (Lsub0 == NULL)
00320         return(NULL);
00321     Cudd_Ref(Lsub0);
00322     Usub0 = Unv;
00323     Lsub1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Unv));
00324     if (Lsub1 == NULL) {
00325         Cudd_RecursiveDeref(dd, Lsub0);
00326         return(NULL);
00327     }
00328     Cudd_Ref(Lsub1);
00329     Usub1 = Uv;
00330 
00331     Isub0 = cuddZddIsop(dd, Lsub0, Usub0, &zdd_Isub0);
00332     if (Isub0 == NULL) {
00333         Cudd_RecursiveDeref(dd, Lsub0);
00334         Cudd_RecursiveDeref(dd, Lsub1);
00335         return(NULL);
00336     }
00337     /*
00338     if ((!cuddIsConstant(Cudd_Regular(Isub0))) &&
00339         (Cudd_Regular(Isub0)->index != zdd_Isub0->index / 2 ||
00340         dd->permZ[index * 2] > dd->permZ[zdd_Isub0->index])) {
00341         printf("*** ERROR : illegal permutation in ZDD. ***\n");
00342     }
00343     */
00344     Cudd_Ref(Isub0);
00345     Cudd_Ref(zdd_Isub0);
00346     Isub1 = cuddZddIsop(dd, Lsub1, Usub1, &zdd_Isub1);
00347     if (Isub1 == NULL) {
00348         Cudd_RecursiveDeref(dd, Lsub0);
00349         Cudd_RecursiveDeref(dd, Lsub1);
00350         Cudd_RecursiveDeref(dd, Isub0);
00351         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00352         return(NULL);
00353     }
00354     /*
00355     if ((!cuddIsConstant(Cudd_Regular(Isub1))) &&
00356         (Cudd_Regular(Isub1)->index != zdd_Isub1->index / 2 ||
00357         dd->permZ[index * 2] > dd->permZ[zdd_Isub1->index])) {
00358         printf("*** ERROR : illegal permutation in ZDD. ***\n");
00359     }
00360     */
00361     Cudd_Ref(Isub1);
00362     Cudd_Ref(zdd_Isub1);
00363     Cudd_RecursiveDeref(dd, Lsub0);
00364     Cudd_RecursiveDeref(dd, Lsub1);
00365 
00366     Lsuper0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Isub0));
00367     if (Lsuper0 == NULL) {
00368         Cudd_RecursiveDeref(dd, Isub0);
00369         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00370         Cudd_RecursiveDeref(dd, Isub1);
00371         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
00372         return(NULL);
00373     }
00374     Cudd_Ref(Lsuper0);
00375     Lsuper1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Isub1));
00376     if (Lsuper1 == NULL) {
00377         Cudd_RecursiveDeref(dd, Isub0);
00378         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00379         Cudd_RecursiveDeref(dd, Isub1);
00380         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
00381         Cudd_RecursiveDeref(dd, Lsuper0);
00382         return(NULL);
00383     }
00384     Cudd_Ref(Lsuper1);
00385     Usuper0 = Unv;
00386     Usuper1 = Uv;
00387 
00388     /* Ld = Lsuper0 + Lsuper1 */
00389     Ld = cuddBddAndRecur(dd, Cudd_Not(Lsuper0), Cudd_Not(Lsuper1));
00390     if (Ld == NULL) {
00391         Cudd_RecursiveDeref(dd, Isub0);
00392         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00393         Cudd_RecursiveDeref(dd, Isub1);
00394         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
00395         Cudd_RecursiveDeref(dd, Lsuper0);
00396         Cudd_RecursiveDeref(dd, Lsuper1);
00397         return(NULL);
00398     }
00399     Ld = Cudd_Not(Ld);
00400     Cudd_Ref(Ld);
00401     /* Ud = Usuper0 * Usuper1 */
00402     Ud = cuddBddAndRecur(dd, Usuper0, Usuper1);
00403     if (Ud == NULL) {
00404         Cudd_RecursiveDeref(dd, Isub0);
00405         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00406         Cudd_RecursiveDeref(dd, Isub1);
00407         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
00408         Cudd_RecursiveDeref(dd, Lsuper0);
00409         Cudd_RecursiveDeref(dd, Lsuper1);
00410         Cudd_RecursiveDeref(dd, Ld);
00411         return(NULL);
00412     }
00413     Cudd_Ref(Ud);
00414     Cudd_RecursiveDeref(dd, Lsuper0);
00415     Cudd_RecursiveDeref(dd, Lsuper1);
00416 
00417     Id = cuddZddIsop(dd, Ld, Ud, &zdd_Id);
00418     if (Id == NULL) {
00419         Cudd_RecursiveDeref(dd, Isub0);
00420         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00421         Cudd_RecursiveDeref(dd, Isub1);
00422         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
00423         Cudd_RecursiveDeref(dd, Ld);
00424         Cudd_RecursiveDeref(dd, Ud);
00425         return(NULL);
00426     }
00427     /*
00428     if ((!cuddIsConstant(Cudd_Regular(Id))) &&
00429         (Cudd_Regular(Id)->index != zdd_Id->index / 2 ||
00430         dd->permZ[index * 2] > dd->permZ[zdd_Id->index])) {
00431         printf("*** ERROR : illegal permutation in ZDD. ***\n");
00432     }
00433     */
00434     Cudd_Ref(Id);
00435     Cudd_Ref(zdd_Id);
00436     Cudd_RecursiveDeref(dd, Ld);
00437     Cudd_RecursiveDeref(dd, Ud);
00438 
00439     x = cuddUniqueInter(dd, index, one, zero);
00440     if (x == NULL) {
00441         Cudd_RecursiveDeref(dd, Isub0);
00442         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00443         Cudd_RecursiveDeref(dd, Isub1);
00444         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
00445         Cudd_RecursiveDeref(dd, Id);
00446         Cudd_RecursiveDerefZdd(dd, zdd_Id);
00447         return(NULL);
00448     }
00449     Cudd_Ref(x);
00450     /* term0 = x * Isub0 */
00451     term0 = cuddBddAndRecur(dd, Cudd_Not(x), Isub0);
00452     if (term0 == NULL) {
00453         Cudd_RecursiveDeref(dd, Isub0);
00454         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00455         Cudd_RecursiveDeref(dd, Isub1);
00456         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
00457         Cudd_RecursiveDeref(dd, Id);
00458         Cudd_RecursiveDerefZdd(dd, zdd_Id);
00459         Cudd_RecursiveDeref(dd, x);
00460         return(NULL);
00461     }
00462     Cudd_Ref(term0);
00463     Cudd_RecursiveDeref(dd, Isub0);
00464     /* term1 = x * Isub1 */
00465     term1 = cuddBddAndRecur(dd, x, Isub1);
00466     if (term1 == NULL) {
00467         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00468         Cudd_RecursiveDeref(dd, Isub1);
00469         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
00470         Cudd_RecursiveDeref(dd, Id);
00471         Cudd_RecursiveDerefZdd(dd, zdd_Id);
00472         Cudd_RecursiveDeref(dd, x);
00473         Cudd_RecursiveDeref(dd, term0);
00474         return(NULL);
00475     }
00476     Cudd_Ref(term1);
00477     Cudd_RecursiveDeref(dd, x);
00478     Cudd_RecursiveDeref(dd, Isub1);
00479     /* sum = term0 + term1 */
00480     sum = cuddBddAndRecur(dd, Cudd_Not(term0), Cudd_Not(term1));
00481     if (sum == NULL) {
00482         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00483         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
00484         Cudd_RecursiveDeref(dd, Id);
00485         Cudd_RecursiveDerefZdd(dd, zdd_Id);
00486         Cudd_RecursiveDeref(dd, term0);
00487         Cudd_RecursiveDeref(dd, term1);
00488         return(NULL);
00489     }
00490     sum = Cudd_Not(sum);
00491     Cudd_Ref(sum);
00492     Cudd_RecursiveDeref(dd, term0);
00493     Cudd_RecursiveDeref(dd, term1);
00494     /* r = sum + Id */
00495     r = cuddBddAndRecur(dd, Cudd_Not(sum), Cudd_Not(Id));
00496     r = Cudd_NotCond(r, r != NULL);
00497     if (r == NULL) {
00498         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00499         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
00500         Cudd_RecursiveDeref(dd, Id);
00501         Cudd_RecursiveDerefZdd(dd, zdd_Id);
00502         Cudd_RecursiveDeref(dd, sum);
00503         return(NULL);
00504     }
00505     Cudd_Ref(r);
00506     Cudd_RecursiveDeref(dd, sum);
00507     Cudd_RecursiveDeref(dd, Id);
00508 
00509     if (zdd_Isub0 != zdd_zero) {
00510         z = cuddZddGetNodeIVO(dd, index * 2 + 1, zdd_Isub0, zdd_Id);
00511         if (z == NULL) {
00512             Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00513             Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
00514             Cudd_RecursiveDerefZdd(dd, zdd_Id);
00515             Cudd_RecursiveDeref(dd, r);
00516             return(NULL);
00517         }
00518     }
00519     else {
00520         z = zdd_Id;
00521     }
00522     Cudd_Ref(z);
00523     if (zdd_Isub1 != zdd_zero) {
00524         y = cuddZddGetNodeIVO(dd, index * 2, zdd_Isub1, z);
00525         if (y == NULL) {
00526             Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00527             Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
00528             Cudd_RecursiveDerefZdd(dd, zdd_Id);
00529             Cudd_RecursiveDeref(dd, r);
00530             Cudd_RecursiveDerefZdd(dd, z);
00531             return(NULL);
00532         }
00533     }
00534     else
00535         y = z;
00536     Cudd_Ref(y);
00537 
00538     Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00539     Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
00540     Cudd_RecursiveDerefZdd(dd, zdd_Id);
00541     Cudd_RecursiveDerefZdd(dd, z);
00542 
00543     cuddCacheInsert2(dd, cuddBddIsop, L, U, r);
00544     cuddCacheInsert2(dd, cacheOp, L, U, y);
00545 
00546     Cudd_Deref(r);
00547     Cudd_Deref(y);
00548     *zdd_I = y;
00549     /*
00550     if (Cudd_Regular(r)->index != y->index / 2) {
00551         printf("*** ERROR : mismatch in indices between BDD and ZDD. ***\n");
00552     }
00553     */
00554     return(r);
00555 
00556 } /* end of cuddZddIsop */
00557 
00558 
00570 DdNode  *
00571 cuddBddIsop(
00572   DdManager * dd,
00573   DdNode * L,
00574   DdNode * U)
00575 {
00576     DdNode      *one = DD_ONE(dd);
00577     DdNode      *zero = Cudd_Not(one);
00578     int         v, top_l, top_u;
00579     DdNode      *Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud;
00580     DdNode      *Lsuper0, *Usuper0, *Lsuper1, *Usuper1;
00581     DdNode      *Isub0, *Isub1, *Id;
00582     DdNode      *x;
00583     DdNode      *term0, *term1, *sum;
00584     DdNode      *Lv, *Uv, *Lnv, *Unv;
00585     DdNode      *r;
00586     int         index;
00587 
00588     statLine(dd);
00589     if (L == zero)
00590         return(zero);
00591     if (U == one)
00592         return(one);
00593 
00594     /* Check cache */
00595     r = cuddCacheLookup2(dd, cuddBddIsop, L, U);
00596     if (r)
00597         return(r);
00598 
00599     top_l = dd->perm[Cudd_Regular(L)->index];
00600     top_u = dd->perm[Cudd_Regular(U)->index];
00601     v = ddMin(top_l, top_u);
00602 
00603     /* Compute cofactors */
00604     if (top_l == v) {
00605         index = Cudd_Regular(L)->index;
00606         Lv = Cudd_T(L);
00607         Lnv = Cudd_E(L);
00608         if (Cudd_IsComplement(L)) {
00609             Lv = Cudd_Not(Lv);
00610             Lnv = Cudd_Not(Lnv);
00611         }
00612     }
00613     else {
00614         index = Cudd_Regular(U)->index;
00615         Lv = Lnv = L;
00616     }
00617 
00618     if (top_u == v) {
00619         Uv = Cudd_T(U);
00620         Unv = Cudd_E(U);
00621         if (Cudd_IsComplement(U)) {
00622             Uv = Cudd_Not(Uv);
00623             Unv = Cudd_Not(Unv);
00624         }
00625     }
00626     else {
00627         Uv = Unv = U;
00628     }
00629 
00630     Lsub0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Uv));
00631     if (Lsub0 == NULL)
00632         return(NULL);
00633     Cudd_Ref(Lsub0);
00634     Usub0 = Unv;
00635     Lsub1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Unv));
00636     if (Lsub1 == NULL) {
00637         Cudd_RecursiveDeref(dd, Lsub0);
00638         return(NULL);
00639     }
00640     Cudd_Ref(Lsub1);
00641     Usub1 = Uv;
00642 
00643     Isub0 = cuddBddIsop(dd, Lsub0, Usub0);
00644     if (Isub0 == NULL) {
00645         Cudd_RecursiveDeref(dd, Lsub0);
00646         Cudd_RecursiveDeref(dd, Lsub1);
00647         return(NULL);
00648     }
00649     Cudd_Ref(Isub0);
00650     Isub1 = cuddBddIsop(dd, Lsub1, Usub1);
00651     if (Isub1 == NULL) {
00652         Cudd_RecursiveDeref(dd, Lsub0);
00653         Cudd_RecursiveDeref(dd, Lsub1);
00654         Cudd_RecursiveDeref(dd, Isub0);
00655         return(NULL);
00656     }
00657     Cudd_Ref(Isub1);
00658     Cudd_RecursiveDeref(dd, Lsub0);
00659     Cudd_RecursiveDeref(dd, Lsub1);
00660 
00661     Lsuper0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Isub0));
00662     if (Lsuper0 == NULL) {
00663         Cudd_RecursiveDeref(dd, Isub0);
00664         Cudd_RecursiveDeref(dd, Isub1);
00665         return(NULL);
00666     }
00667     Cudd_Ref(Lsuper0);
00668     Lsuper1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Isub1));
00669     if (Lsuper1 == NULL) {
00670         Cudd_RecursiveDeref(dd, Isub0);
00671         Cudd_RecursiveDeref(dd, Isub1);
00672         Cudd_RecursiveDeref(dd, Lsuper0);
00673         return(NULL);
00674     }
00675     Cudd_Ref(Lsuper1);
00676     Usuper0 = Unv;
00677     Usuper1 = Uv;
00678 
00679     /* Ld = Lsuper0 + Lsuper1 */
00680     Ld = cuddBddAndRecur(dd, Cudd_Not(Lsuper0), Cudd_Not(Lsuper1));
00681     Ld = Cudd_NotCond(Ld, Ld != NULL);
00682     if (Ld == NULL) {
00683         Cudd_RecursiveDeref(dd, Isub0);
00684         Cudd_RecursiveDeref(dd, Isub1);
00685         Cudd_RecursiveDeref(dd, Lsuper0);
00686         Cudd_RecursiveDeref(dd, Lsuper1);
00687         return(NULL);
00688     }
00689     Cudd_Ref(Ld);
00690     Ud = cuddBddAndRecur(dd, Usuper0, Usuper1);
00691     if (Ud == NULL) {
00692         Cudd_RecursiveDeref(dd, Isub0);
00693         Cudd_RecursiveDeref(dd, Isub1);
00694         Cudd_RecursiveDeref(dd, Lsuper0);
00695         Cudd_RecursiveDeref(dd, Lsuper1);
00696         Cudd_RecursiveDeref(dd, Ld);
00697         return(NULL);
00698     }
00699     Cudd_Ref(Ud);
00700     Cudd_RecursiveDeref(dd, Lsuper0);
00701     Cudd_RecursiveDeref(dd, Lsuper1);
00702 
00703     Id = cuddBddIsop(dd, Ld, Ud);
00704     if (Id == NULL) {
00705         Cudd_RecursiveDeref(dd, Isub0);
00706         Cudd_RecursiveDeref(dd, Isub1);
00707         Cudd_RecursiveDeref(dd, Ld);
00708         Cudd_RecursiveDeref(dd, Ud);
00709         return(NULL);
00710     }
00711     Cudd_Ref(Id);
00712     Cudd_RecursiveDeref(dd, Ld);
00713     Cudd_RecursiveDeref(dd, Ud);
00714 
00715     x = cuddUniqueInter(dd, index, one, zero);
00716     if (x == NULL) {
00717         Cudd_RecursiveDeref(dd, Isub0);
00718         Cudd_RecursiveDeref(dd, Isub1);
00719         Cudd_RecursiveDeref(dd, Id);
00720         return(NULL);
00721     }
00722     Cudd_Ref(x);
00723     term0 = cuddBddAndRecur(dd, Cudd_Not(x), Isub0);
00724     if (term0 == NULL) {
00725         Cudd_RecursiveDeref(dd, Isub0);
00726         Cudd_RecursiveDeref(dd, Isub1);
00727         Cudd_RecursiveDeref(dd, Id);
00728         Cudd_RecursiveDeref(dd, x);
00729         return(NULL);
00730     }
00731     Cudd_Ref(term0);
00732     Cudd_RecursiveDeref(dd, Isub0);
00733     term1 = cuddBddAndRecur(dd, x, Isub1);
00734     if (term1 == NULL) {
00735         Cudd_RecursiveDeref(dd, Isub1);
00736         Cudd_RecursiveDeref(dd, Id);
00737         Cudd_RecursiveDeref(dd, x);
00738         Cudd_RecursiveDeref(dd, term0);
00739         return(NULL);
00740     }
00741     Cudd_Ref(term1);
00742     Cudd_RecursiveDeref(dd, x);
00743     Cudd_RecursiveDeref(dd, Isub1);
00744     /* sum = term0 + term1 */
00745     sum = cuddBddAndRecur(dd, Cudd_Not(term0), Cudd_Not(term1));
00746     sum = Cudd_NotCond(sum, sum != NULL);
00747     if (sum == NULL) {
00748         Cudd_RecursiveDeref(dd, Id);
00749         Cudd_RecursiveDeref(dd, term0);
00750         Cudd_RecursiveDeref(dd, term1);
00751         return(NULL);
00752     }
00753     Cudd_Ref(sum);
00754     Cudd_RecursiveDeref(dd, term0);
00755     Cudd_RecursiveDeref(dd, term1);
00756     /* r = sum + Id */
00757     r = cuddBddAndRecur(dd, Cudd_Not(sum), Cudd_Not(Id));
00758     r = Cudd_NotCond(r, r != NULL);
00759     if (r == NULL) {
00760         Cudd_RecursiveDeref(dd, Id);
00761         Cudd_RecursiveDeref(dd, sum);
00762         return(NULL);
00763     }
00764     Cudd_Ref(r);
00765     Cudd_RecursiveDeref(dd, sum);
00766     Cudd_RecursiveDeref(dd, Id);
00767 
00768     cuddCacheInsert2(dd, cuddBddIsop, L, U, r);
00769 
00770     Cudd_Deref(r);
00771     return(r);
00772 
00773 } /* end of cuddBddIsop */
00774 
00775 
00795 DdNode  *
00796 cuddMakeBddFromZddCover(
00797   DdManager * dd,
00798   DdNode * node)
00799 {
00800     DdNode      *neW;
00801     int         v;
00802     DdNode      *f1, *f0, *fd;
00803     DdNode      *b1, *b0, *bd;
00804     DdNode      *T, *E;
00805 
00806     statLine(dd);
00807     if (node == dd->one)
00808         return(dd->one);
00809     if (node == dd->zero)
00810         return(Cudd_Not(dd->one));
00811 
00812     /* Check cache */
00813     neW = cuddCacheLookup1(dd, cuddMakeBddFromZddCover, node);
00814     if (neW)
00815         return(neW);
00816 
00817     v = Cudd_Regular(node)->index;      /* either yi or zi */
00818     if (cuddZddGetCofactors3(dd, node, v, &f1, &f0, &fd)) return(NULL);
00819     Cudd_Ref(f1);
00820     Cudd_Ref(f0);
00821     Cudd_Ref(fd);
00822 
00823     b1 = cuddMakeBddFromZddCover(dd, f1);
00824     if (!b1) {
00825         Cudd_RecursiveDerefZdd(dd, f1);
00826         Cudd_RecursiveDerefZdd(dd, f0);
00827         Cudd_RecursiveDerefZdd(dd, fd);
00828         return(NULL);
00829     }
00830     Cudd_Ref(b1);
00831     b0 = cuddMakeBddFromZddCover(dd, f0);
00832     if (!b0) {
00833         Cudd_RecursiveDerefZdd(dd, f1);
00834         Cudd_RecursiveDerefZdd(dd, f0);
00835         Cudd_RecursiveDerefZdd(dd, fd);
00836         Cudd_RecursiveDeref(dd, b1);
00837         return(NULL);
00838     }
00839     Cudd_Ref(b0);
00840     Cudd_RecursiveDerefZdd(dd, f1);
00841     Cudd_RecursiveDerefZdd(dd, f0);
00842     if (fd != dd->zero) {
00843         bd = cuddMakeBddFromZddCover(dd, fd);
00844         if (!bd) {
00845             Cudd_RecursiveDerefZdd(dd, fd);
00846             Cudd_RecursiveDeref(dd, b1);
00847             Cudd_RecursiveDeref(dd, b0);
00848             return(NULL);
00849         }
00850         Cudd_Ref(bd);
00851         Cudd_RecursiveDerefZdd(dd, fd);
00852 
00853         T = cuddBddAndRecur(dd, Cudd_Not(b1), Cudd_Not(bd));
00854         if (!T) {
00855             Cudd_RecursiveDeref(dd, b1);
00856             Cudd_RecursiveDeref(dd, b0);
00857             Cudd_RecursiveDeref(dd, bd);
00858             return(NULL);
00859         }
00860         T = Cudd_NotCond(T, T != NULL);
00861         Cudd_Ref(T);
00862         Cudd_RecursiveDeref(dd, b1);
00863         E = cuddBddAndRecur(dd, Cudd_Not(b0), Cudd_Not(bd));
00864         if (!E) {
00865             Cudd_RecursiveDeref(dd, b0);
00866             Cudd_RecursiveDeref(dd, bd);
00867             Cudd_RecursiveDeref(dd, T);
00868             return(NULL);
00869         }
00870         E = Cudd_NotCond(E, E != NULL);
00871         Cudd_Ref(E);
00872         Cudd_RecursiveDeref(dd, b0);
00873         Cudd_RecursiveDeref(dd, bd);
00874     }
00875     else {
00876         Cudd_RecursiveDerefZdd(dd, fd);
00877         T = b1;
00878         E = b0;
00879     }
00880 
00881     if (Cudd_IsComplement(T)) {
00882         neW = cuddUniqueInterIVO(dd, v / 2, Cudd_Not(T), Cudd_Not(E));
00883         if (!neW) {
00884             Cudd_RecursiveDeref(dd, T);
00885             Cudd_RecursiveDeref(dd, E);
00886             return(NULL);
00887         }
00888         neW = Cudd_Not(neW);
00889     }
00890     else {
00891         neW = cuddUniqueInterIVO(dd, v / 2, T, E);
00892         if (!neW) {
00893             Cudd_RecursiveDeref(dd, T);
00894             Cudd_RecursiveDeref(dd, E);
00895             return(NULL);
00896         }
00897     }
00898     Cudd_Ref(neW);
00899     Cudd_RecursiveDeref(dd, T);
00900     Cudd_RecursiveDeref(dd, E);
00901 
00902     cuddCacheInsert1(dd, cuddMakeBddFromZddCover, node, neW);
00903     Cudd_Deref(neW);
00904     return(neW);
00905 
00906 } /* end of cuddMakeBddFromZddCover */
00907 
00908 
00909 /*---------------------------------------------------------------------------*/
00910 /* Definition of static functions                                            */
00911 /*---------------------------------------------------------------------------*/