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

00001 
00037 #include        "util_hack.h"
00038 #include        "cuddInt.h"
00039 
00040 /*---------------------------------------------------------------------------*/
00041 /* Constant declarations                                                     */
00042 /*---------------------------------------------------------------------------*/
00043 
00044 
00045 /*---------------------------------------------------------------------------*/
00046 /* Stucture declarations                                                     */
00047 /*---------------------------------------------------------------------------*/
00048 
00049 
00050 /*---------------------------------------------------------------------------*/
00051 /* Type declarations                                                         */
00052 /*---------------------------------------------------------------------------*/
00053 
00054 
00055 /*---------------------------------------------------------------------------*/
00056 /* Variable declarations                                                     */
00057 /*---------------------------------------------------------------------------*/
00058 
00059 #ifndef lint
00060 static char rcsid[] DD_UNUSED = "$Id: cuddZddIsop.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang Exp $";
00061 #endif
00062 
00063 /*---------------------------------------------------------------------------*/
00064 /* Macro declarations                                                        */
00065 /*---------------------------------------------------------------------------*/
00066 
00067 
00070 /*---------------------------------------------------------------------------*/
00071 /* Static function prototypes                                                */
00072 /*---------------------------------------------------------------------------*/
00073 
00074 
00077 /*---------------------------------------------------------------------------*/
00078 /* Definition of exported functions                                          */
00079 /*---------------------------------------------------------------------------*/
00080 
00104 DdNode  *
00105 Cudd_zddIsop(
00106   DdManager * dd,
00107   DdNode * L,
00108   DdNode * U,
00109   DdNode ** zdd_I)
00110 {
00111     DdNode      *res;
00112     int         autoDynZ;
00113 
00114     autoDynZ = dd->autoDynZ;
00115     dd->autoDynZ = 0;
00116 
00117     do {
00118         dd->reordered = 0;
00119         res = cuddZddIsop(dd, L, U, zdd_I);
00120     } while (dd->reordered == 1);
00121     dd->autoDynZ = autoDynZ;
00122     return(res);
00123 
00124 } /* end of Cudd_zddIsop */
00125 
00126 
00142 DdNode  *
00143 Cudd_bddIsop(
00144   DdManager * dd,
00145   DdNode * L,
00146   DdNode * U)
00147 {
00148     DdNode      *res;
00149 
00150     do {
00151         dd->reordered = 0;
00152         res = cuddBddIsop(dd, L, U);
00153     } while (dd->reordered == 1);
00154     return(res);
00155 
00156 } /* end of Cudd_bddIsop */
00157 
00158 
00171 DdNode  *
00172 Cudd_MakeBddFromZddCover(
00173   DdManager * dd,
00174   DdNode * node)
00175 {
00176     DdNode      *res;
00177 
00178     do {
00179         dd->reordered = 0;
00180         res = cuddMakeBddFromZddCover(dd, node);
00181     } while (dd->reordered == 1);
00182     return(res);
00183 } /* end of Cudd_MakeBddFromZddCover */
00184 
00185 
00186 /*---------------------------------------------------------------------------*/
00187 /* Definition of internal functions                                          */
00188 /*---------------------------------------------------------------------------*/
00189 
00190 
00202 DdNode  *
00203 cuddZddIsop(
00204   DdManager * dd,
00205   DdNode * L,
00206   DdNode * U,
00207   DdNode ** zdd_I)
00208 {
00209     DdNode      *one = DD_ONE(dd);
00210     DdNode      *zero = Cudd_Not(one);
00211     DdNode      *zdd_one = DD_ONE(dd);
00212     DdNode      *zdd_zero = DD_ZERO(dd);
00213     int         v, top_l, top_u;
00214     DdNode      *Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud;
00215     DdNode      *Lsuper0, *Usuper0, *Lsuper1, *Usuper1;
00216     DdNode      *Isub0, *Isub1, *Id;
00217     DdNode      *zdd_Isub0, *zdd_Isub1, *zdd_Id;
00218     DdNode      *x;
00219     DdNode      *term0, *term1, *sum;
00220     DdNode      *Lv, *Uv, *Lnv, *Unv;
00221     DdNode      *r, *y, *z;
00222     int         index;
00223     DdNode *(*cacheOp)(DdManager *, DdNode *, DdNode *);
00224 
00225     statLine(dd);
00226     if (L == zero) {
00227         *zdd_I = zdd_zero;
00228         return(zero);
00229     }
00230     if (U == one) {
00231         *zdd_I = zdd_one;
00232         return(one);
00233     }
00234 
00235     if (U == zero || L == one) {
00236         printf("*** ERROR : illegal condition for ISOP (U < L).\n");
00237         exit(1);
00238     }
00239 
00240     /* Check the cache. We store two results for each recursive call.
00241     ** One is the BDD, and the other is the ZDD. Both are needed.
00242     ** Hence we need a double hit in the cache to terminate the
00243     ** recursion. Clearly, collisions may evict only one of the two
00244     ** results. */
00245     cacheOp = (DdNode *(*)(DdManager *, DdNode *, DdNode *)) cuddZddIsop;
00246     r = cuddCacheLookup2(dd, cuddBddIsop, L, U);
00247     if (r) {
00248         *zdd_I = cuddCacheLookup2Zdd(dd, cacheOp, L, U);
00249         if (*zdd_I)
00250             return(r);
00251         else {
00252             /* The BDD result may have been dead. In that case
00253             ** cuddCacheLookup2 would have called cuddReclaim,
00254             ** whose effects we now have to undo. */
00255             cuddRef(r);
00256             Cudd_RecursiveDeref(dd, r);
00257         }
00258     }
00259 
00260     top_l = dd->perm[Cudd_Regular(L)->index];
00261     top_u = dd->perm[Cudd_Regular(U)->index];
00262     v = ddMin(top_l, top_u);
00263 
00264     /* Compute cofactors. */
00265     if (top_l == v) {
00266         index = Cudd_Regular(L)->index;
00267         Lv = Cudd_T(L);
00268         Lnv = Cudd_E(L);
00269         if (Cudd_IsComplement(L)) {
00270             Lv = Cudd_Not(Lv);
00271             Lnv = Cudd_Not(Lnv);
00272         }
00273     }
00274     else {
00275         index = Cudd_Regular(U)->index;
00276         Lv = Lnv = L;
00277     }
00278 
00279     if (top_u == v) {
00280         Uv = Cudd_T(U);
00281         Unv = Cudd_E(U);
00282         if (Cudd_IsComplement(U)) {
00283             Uv = Cudd_Not(Uv);
00284             Unv = Cudd_Not(Unv);
00285         }
00286     }
00287     else {
00288         Uv = Unv = U;
00289     }
00290 
00291     Lsub0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Uv));
00292     if (Lsub0 == NULL)
00293         return(NULL);
00294     Cudd_Ref(Lsub0);
00295     Usub0 = Unv;
00296     Lsub1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Unv));
00297     if (Lsub1 == NULL) {
00298         Cudd_RecursiveDeref(dd, Lsub0);
00299         return(NULL);
00300     }
00301     Cudd_Ref(Lsub1);
00302     Usub1 = Uv;
00303 
00304     Isub0 = cuddZddIsop(dd, Lsub0, Usub0, &zdd_Isub0);
00305     if (Isub0 == NULL) {
00306         Cudd_RecursiveDeref(dd, Lsub0);
00307         Cudd_RecursiveDeref(dd, Lsub1);
00308         return(NULL);
00309     }
00310     /*
00311     if ((!cuddIsConstant(Cudd_Regular(Isub0))) &&
00312         (Cudd_Regular(Isub0)->index != zdd_Isub0->index / 2 ||
00313         dd->permZ[index * 2] > dd->permZ[zdd_Isub0->index])) {
00314         printf("*** ERROR : illegal permutation in ZDD. ***\n");
00315     }
00316     */
00317     Cudd_Ref(Isub0);
00318     Cudd_Ref(zdd_Isub0);
00319     Isub1 = cuddZddIsop(dd, Lsub1, Usub1, &zdd_Isub1);
00320     if (Isub1 == NULL) {
00321         Cudd_RecursiveDeref(dd, Lsub0);
00322         Cudd_RecursiveDeref(dd, Lsub1);
00323         Cudd_RecursiveDeref(dd, Isub0);
00324         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00325         return(NULL);
00326     }
00327     /*
00328     if ((!cuddIsConstant(Cudd_Regular(Isub1))) &&
00329         (Cudd_Regular(Isub1)->index != zdd_Isub1->index / 2 ||
00330         dd->permZ[index * 2] > dd->permZ[zdd_Isub1->index])) {
00331         printf("*** ERROR : illegal permutation in ZDD. ***\n");
00332     }
00333     */
00334     Cudd_Ref(Isub1);
00335     Cudd_Ref(zdd_Isub1);
00336     Cudd_RecursiveDeref(dd, Lsub0);
00337     Cudd_RecursiveDeref(dd, Lsub1);
00338 
00339     Lsuper0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Isub0));
00340     if (Lsuper0 == NULL) {
00341         Cudd_RecursiveDeref(dd, Isub0);
00342         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00343         Cudd_RecursiveDeref(dd, Isub1);
00344         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
00345         return(NULL);
00346     }
00347     Cudd_Ref(Lsuper0);
00348     Lsuper1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Isub1));
00349     if (Lsuper1 == NULL) {
00350         Cudd_RecursiveDeref(dd, Isub0);
00351         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00352         Cudd_RecursiveDeref(dd, Isub1);
00353         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
00354         Cudd_RecursiveDeref(dd, Lsuper0);
00355         return(NULL);
00356     }
00357     Cudd_Ref(Lsuper1);
00358     Usuper0 = Unv;
00359     Usuper1 = Uv;
00360 
00361     /* Ld = Lsuper0 + Lsuper1 */
00362     Ld = cuddBddAndRecur(dd, Cudd_Not(Lsuper0), Cudd_Not(Lsuper1));
00363     if (Ld == NULL) {
00364         Cudd_RecursiveDeref(dd, Isub0);
00365         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00366         Cudd_RecursiveDeref(dd, Isub1);
00367         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
00368         Cudd_RecursiveDeref(dd, Lsuper0);
00369         Cudd_RecursiveDeref(dd, Lsuper1);
00370         return(NULL);
00371     }
00372     Ld = Cudd_Not(Ld);
00373     Cudd_Ref(Ld);
00374     /* Ud = Usuper0 * Usuper1 */
00375     Ud = cuddBddAndRecur(dd, Usuper0, Usuper1);
00376     if (Ud == 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         Cudd_RecursiveDeref(dd, Lsuper1);
00383         Cudd_RecursiveDeref(dd, Ld);
00384         return(NULL);
00385     }
00386     Cudd_Ref(Ud);
00387     Cudd_RecursiveDeref(dd, Lsuper0);
00388     Cudd_RecursiveDeref(dd, Lsuper1);
00389 
00390     Id = cuddZddIsop(dd, Ld, Ud, &zdd_Id);
00391     if (Id == NULL) {
00392         Cudd_RecursiveDeref(dd, Isub0);
00393         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00394         Cudd_RecursiveDeref(dd, Isub1);
00395         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
00396         Cudd_RecursiveDeref(dd, Ld);
00397         Cudd_RecursiveDeref(dd, Ud);
00398         return(NULL);
00399     }
00400     /*
00401     if ((!cuddIsConstant(Cudd_Regular(Id))) &&
00402         (Cudd_Regular(Id)->index != zdd_Id->index / 2 ||
00403         dd->permZ[index * 2] > dd->permZ[zdd_Id->index])) {
00404         printf("*** ERROR : illegal permutation in ZDD. ***\n");
00405     }
00406     */
00407     Cudd_Ref(Id);
00408     Cudd_Ref(zdd_Id);
00409     Cudd_RecursiveDeref(dd, Ld);
00410     Cudd_RecursiveDeref(dd, Ud);
00411 
00412     x = cuddUniqueInter(dd, index, one, zero);
00413     if (x == NULL) {
00414         Cudd_RecursiveDeref(dd, Isub0);
00415         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00416         Cudd_RecursiveDeref(dd, Isub1);
00417         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
00418         Cudd_RecursiveDeref(dd, Id);
00419         Cudd_RecursiveDerefZdd(dd, zdd_Id);
00420         return(NULL);
00421     }
00422     Cudd_Ref(x);
00423     /* term0 = x * Isub0 */
00424     term0 = cuddBddAndRecur(dd, Cudd_Not(x), Isub0);
00425     if (term0 == NULL) {
00426         Cudd_RecursiveDeref(dd, Isub0);
00427         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00428         Cudd_RecursiveDeref(dd, Isub1);
00429         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
00430         Cudd_RecursiveDeref(dd, Id);
00431         Cudd_RecursiveDerefZdd(dd, zdd_Id);
00432         Cudd_RecursiveDeref(dd, x);
00433         return(NULL);
00434     }
00435     Cudd_Ref(term0);
00436     Cudd_RecursiveDeref(dd, Isub0);
00437     /* term1 = x * Isub1 */
00438     term1 = cuddBddAndRecur(dd, x, Isub1);
00439     if (term1 == NULL) {
00440         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00441         Cudd_RecursiveDeref(dd, Isub1);
00442         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
00443         Cudd_RecursiveDeref(dd, Id);
00444         Cudd_RecursiveDerefZdd(dd, zdd_Id);
00445         Cudd_RecursiveDeref(dd, x);
00446         Cudd_RecursiveDeref(dd, term0);
00447         return(NULL);
00448     }
00449     Cudd_Ref(term1);
00450     Cudd_RecursiveDeref(dd, x);
00451     Cudd_RecursiveDeref(dd, Isub1);
00452     /* sum = term0 + term1 */
00453     sum = cuddBddAndRecur(dd, Cudd_Not(term0), Cudd_Not(term1));
00454     if (sum == NULL) {
00455         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00456         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
00457         Cudd_RecursiveDeref(dd, Id);
00458         Cudd_RecursiveDerefZdd(dd, zdd_Id);
00459         Cudd_RecursiveDeref(dd, term0);
00460         Cudd_RecursiveDeref(dd, term1);
00461         return(NULL);
00462     }
00463     sum = Cudd_Not(sum);
00464     Cudd_Ref(sum);
00465     Cudd_RecursiveDeref(dd, term0);
00466     Cudd_RecursiveDeref(dd, term1);
00467     /* r = sum + Id */
00468     r = cuddBddAndRecur(dd, Cudd_Not(sum), Cudd_Not(Id));
00469     r = Cudd_NotCond(r, r != NULL);
00470     if (r == NULL) {
00471         Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00472         Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
00473         Cudd_RecursiveDeref(dd, Id);
00474         Cudd_RecursiveDerefZdd(dd, zdd_Id);
00475         Cudd_RecursiveDeref(dd, sum);
00476         return(NULL);
00477     }
00478     Cudd_Ref(r);
00479     Cudd_RecursiveDeref(dd, sum);
00480     Cudd_RecursiveDeref(dd, Id);
00481 
00482     if (zdd_Isub0 != zdd_zero) {
00483         z = cuddZddGetNodeIVO(dd, index * 2 + 1, zdd_Isub0, zdd_Id);
00484         if (z == NULL) {
00485             Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00486             Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
00487             Cudd_RecursiveDerefZdd(dd, zdd_Id);
00488             Cudd_RecursiveDeref(dd, r);
00489             return(NULL);
00490         }
00491     }
00492     else {
00493         z = zdd_Id;
00494     }
00495     Cudd_Ref(z);
00496     if (zdd_Isub1 != zdd_zero) {
00497         y = cuddZddGetNodeIVO(dd, index * 2, zdd_Isub1, z);
00498         if (y == NULL) {
00499             Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00500             Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
00501             Cudd_RecursiveDerefZdd(dd, zdd_Id);
00502             Cudd_RecursiveDeref(dd, r);
00503             Cudd_RecursiveDerefZdd(dd, z);
00504             return(NULL);
00505         }
00506     }
00507     else
00508         y = z;
00509     Cudd_Ref(y);
00510 
00511     Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
00512     Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
00513     Cudd_RecursiveDerefZdd(dd, zdd_Id);
00514     Cudd_RecursiveDerefZdd(dd, z);
00515 
00516     cuddCacheInsert2(dd, cuddBddIsop, L, U, r);
00517     cuddCacheInsert2(dd, cacheOp, L, U, y);
00518 
00519     Cudd_Deref(r);
00520     Cudd_Deref(y);
00521     *zdd_I = y;
00522     /*
00523     if (Cudd_Regular(r)->index != y->index / 2) {
00524         printf("*** ERROR : mismatch in indices between BDD and ZDD. ***\n");
00525     }
00526     */
00527     return(r);
00528 
00529 } /* end of cuddZddIsop */
00530 
00531 
00543 DdNode  *
00544 cuddBddIsop(
00545   DdManager * dd,
00546   DdNode * L,
00547   DdNode * U)
00548 {
00549     DdNode      *one = DD_ONE(dd);
00550     DdNode      *zero = Cudd_Not(one);
00551     int         v, top_l, top_u;
00552     DdNode      *Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud;
00553     DdNode      *Lsuper0, *Usuper0, *Lsuper1, *Usuper1;
00554     DdNode      *Isub0, *Isub1, *Id;
00555     DdNode      *x;
00556     DdNode      *term0, *term1, *sum;
00557     DdNode      *Lv, *Uv, *Lnv, *Unv;
00558     DdNode      *r;
00559     int         index;
00560 
00561     statLine(dd);
00562     if (L == zero)
00563         return(zero);
00564     if (U == one)
00565         return(one);
00566 
00567     /* Check cache */
00568     r = cuddCacheLookup2(dd, cuddBddIsop, L, U);
00569     if (r)
00570         return(r);
00571 
00572     top_l = dd->perm[Cudd_Regular(L)->index];
00573     top_u = dd->perm[Cudd_Regular(U)->index];
00574     v = ddMin(top_l, top_u);
00575 
00576     /* Compute cofactors */
00577     if (top_l == v) {
00578         index = Cudd_Regular(L)->index;
00579         Lv = Cudd_T(L);
00580         Lnv = Cudd_E(L);
00581         if (Cudd_IsComplement(L)) {
00582             Lv = Cudd_Not(Lv);
00583             Lnv = Cudd_Not(Lnv);
00584         }
00585     }
00586     else {
00587         index = Cudd_Regular(U)->index;
00588         Lv = Lnv = L;
00589     }
00590 
00591     if (top_u == v) {
00592         Uv = Cudd_T(U);
00593         Unv = Cudd_E(U);
00594         if (Cudd_IsComplement(U)) {
00595             Uv = Cudd_Not(Uv);
00596             Unv = Cudd_Not(Unv);
00597         }
00598     }
00599     else {
00600         Uv = Unv = U;
00601     }
00602 
00603     Lsub0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Uv));
00604     if (Lsub0 == NULL)
00605         return(NULL);
00606     Cudd_Ref(Lsub0);
00607     Usub0 = Unv;
00608     Lsub1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Unv));
00609     if (Lsub1 == NULL) {
00610         Cudd_RecursiveDeref(dd, Lsub0);
00611         return(NULL);
00612     }
00613     Cudd_Ref(Lsub1);
00614     Usub1 = Uv;
00615 
00616     Isub0 = cuddBddIsop(dd, Lsub0, Usub0);
00617     if (Isub0 == NULL) {
00618         Cudd_RecursiveDeref(dd, Lsub0);
00619         Cudd_RecursiveDeref(dd, Lsub1);
00620         return(NULL);
00621     }
00622     Cudd_Ref(Isub0);
00623     Isub1 = cuddBddIsop(dd, Lsub1, Usub1);
00624     if (Isub1 == NULL) {
00625         Cudd_RecursiveDeref(dd, Lsub0);
00626         Cudd_RecursiveDeref(dd, Lsub1);
00627         Cudd_RecursiveDeref(dd, Isub0);
00628         return(NULL);
00629     }
00630     Cudd_Ref(Isub1);
00631     Cudd_RecursiveDeref(dd, Lsub0);
00632     Cudd_RecursiveDeref(dd, Lsub1);
00633 
00634     Lsuper0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Isub0));
00635     if (Lsuper0 == NULL) {
00636         Cudd_RecursiveDeref(dd, Isub0);
00637         Cudd_RecursiveDeref(dd, Isub1);
00638         return(NULL);
00639     }
00640     Cudd_Ref(Lsuper0);
00641     Lsuper1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Isub1));
00642     if (Lsuper1 == NULL) {
00643         Cudd_RecursiveDeref(dd, Isub0);
00644         Cudd_RecursiveDeref(dd, Isub1);
00645         Cudd_RecursiveDeref(dd, Lsuper0);
00646         return(NULL);
00647     }
00648     Cudd_Ref(Lsuper1);
00649     Usuper0 = Unv;
00650     Usuper1 = Uv;
00651 
00652     /* Ld = Lsuper0 + Lsuper1 */
00653     Ld = cuddBddAndRecur(dd, Cudd_Not(Lsuper0), Cudd_Not(Lsuper1));
00654     Ld = Cudd_NotCond(Ld, Ld != NULL);
00655     if (Ld == NULL) {
00656         Cudd_RecursiveDeref(dd, Isub0);
00657         Cudd_RecursiveDeref(dd, Isub1);
00658         Cudd_RecursiveDeref(dd, Lsuper0);
00659         Cudd_RecursiveDeref(dd, Lsuper1);
00660         return(NULL);
00661     }
00662     Cudd_Ref(Ld);
00663     Ud = cuddBddAndRecur(dd, Usuper0, Usuper1);
00664     if (Ud == NULL) {
00665         Cudd_RecursiveDeref(dd, Isub0);
00666         Cudd_RecursiveDeref(dd, Isub1);
00667         Cudd_RecursiveDeref(dd, Lsuper0);
00668         Cudd_RecursiveDeref(dd, Lsuper1);
00669         Cudd_RecursiveDeref(dd, Ld);
00670         return(NULL);
00671     }
00672     Cudd_Ref(Ud);
00673     Cudd_RecursiveDeref(dd, Lsuper0);
00674     Cudd_RecursiveDeref(dd, Lsuper1);
00675 
00676     Id = cuddBddIsop(dd, Ld, Ud);
00677     if (Id == NULL) {
00678         Cudd_RecursiveDeref(dd, Isub0);
00679         Cudd_RecursiveDeref(dd, Isub1);
00680         Cudd_RecursiveDeref(dd, Ld);
00681         Cudd_RecursiveDeref(dd, Ud);
00682         return(NULL);
00683     }
00684     Cudd_Ref(Id);
00685     Cudd_RecursiveDeref(dd, Ld);
00686     Cudd_RecursiveDeref(dd, Ud);
00687 
00688     x = cuddUniqueInter(dd, index, one, zero);
00689     if (x == NULL) {
00690         Cudd_RecursiveDeref(dd, Isub0);
00691         Cudd_RecursiveDeref(dd, Isub1);
00692         Cudd_RecursiveDeref(dd, Id);
00693         return(NULL);
00694     }
00695     Cudd_Ref(x);
00696     term0 = cuddBddAndRecur(dd, Cudd_Not(x), Isub0);
00697     if (term0 == NULL) {
00698         Cudd_RecursiveDeref(dd, Isub0);
00699         Cudd_RecursiveDeref(dd, Isub1);
00700         Cudd_RecursiveDeref(dd, Id);
00701         Cudd_RecursiveDeref(dd, x);
00702         return(NULL);
00703     }
00704     Cudd_Ref(term0);
00705     Cudd_RecursiveDeref(dd, Isub0);
00706     term1 = cuddBddAndRecur(dd, x, Isub1);
00707     if (term1 == NULL) {
00708         Cudd_RecursiveDeref(dd, Isub1);
00709         Cudd_RecursiveDeref(dd, Id);
00710         Cudd_RecursiveDeref(dd, x);
00711         Cudd_RecursiveDeref(dd, term0);
00712         return(NULL);
00713     }
00714     Cudd_Ref(term1);
00715     Cudd_RecursiveDeref(dd, x);
00716     Cudd_RecursiveDeref(dd, Isub1);
00717     /* sum = term0 + term1 */
00718     sum = cuddBddAndRecur(dd, Cudd_Not(term0), Cudd_Not(term1));
00719     sum = Cudd_NotCond(sum, sum != NULL);
00720     if (sum == NULL) {
00721         Cudd_RecursiveDeref(dd, Id);
00722         Cudd_RecursiveDeref(dd, term0);
00723         Cudd_RecursiveDeref(dd, term1);
00724         return(NULL);
00725     }
00726     Cudd_Ref(sum);
00727     Cudd_RecursiveDeref(dd, term0);
00728     Cudd_RecursiveDeref(dd, term1);
00729     /* r = sum + Id */
00730     r = cuddBddAndRecur(dd, Cudd_Not(sum), Cudd_Not(Id));
00731     r = Cudd_NotCond(r, r != NULL);
00732     if (r == NULL) {
00733         Cudd_RecursiveDeref(dd, Id);
00734         Cudd_RecursiveDeref(dd, sum);
00735         return(NULL);
00736     }
00737     Cudd_Ref(r);
00738     Cudd_RecursiveDeref(dd, sum);
00739     Cudd_RecursiveDeref(dd, Id);
00740 
00741     cuddCacheInsert2(dd, cuddBddIsop, L, U, r);
00742 
00743     Cudd_Deref(r);
00744     return(r);
00745 
00746 } /* end of cuddBddIsop */
00747 
00748 
00768 DdNode  *
00769 cuddMakeBddFromZddCover(
00770   DdManager * dd,
00771   DdNode * node)
00772 {
00773     DdNode      *neW;
00774     int         v;
00775     DdNode      *f1, *f0, *fd;
00776     DdNode      *b1, *b0, *bd;
00777     DdNode      *T, *E;
00778 
00779     statLine(dd);
00780     if (node == dd->one)
00781         return(dd->one);
00782     if (node == dd->zero)
00783         return(Cudd_Not(dd->one));
00784 
00785     /* Check cache */
00786     neW = cuddCacheLookup1(dd, cuddMakeBddFromZddCover, node);
00787     if (neW)
00788         return(neW);
00789 
00790     v = Cudd_Regular(node)->index;      /* either yi or zi */
00791     cuddZddGetCofactors3(dd, node, v, &f1, &f0, &fd);
00792     Cudd_Ref(f1);
00793     Cudd_Ref(f0);
00794     Cudd_Ref(fd);
00795 
00796     b1 = cuddMakeBddFromZddCover(dd, f1);
00797     if (!b1) {
00798         Cudd_RecursiveDerefZdd(dd, f1);
00799         Cudd_RecursiveDerefZdd(dd, f0);
00800         Cudd_RecursiveDerefZdd(dd, fd);
00801         return(NULL);
00802     }
00803     Cudd_Ref(b1);
00804     b0 = cuddMakeBddFromZddCover(dd, f0);
00805     if (!b1) {
00806         Cudd_RecursiveDerefZdd(dd, f1);
00807         Cudd_RecursiveDerefZdd(dd, f0);
00808         Cudd_RecursiveDerefZdd(dd, fd);
00809         Cudd_RecursiveDeref(dd, b1);
00810         return(NULL);
00811     }
00812     Cudd_Ref(b0);
00813     Cudd_RecursiveDerefZdd(dd, f1);
00814     Cudd_RecursiveDerefZdd(dd, f0);
00815     if (fd != dd->zero) {
00816         bd = cuddMakeBddFromZddCover(dd, fd);
00817         if (!bd) {
00818             Cudd_RecursiveDerefZdd(dd, fd);
00819             Cudd_RecursiveDeref(dd, b1);
00820             Cudd_RecursiveDeref(dd, b0);
00821             return(NULL);
00822         }
00823         Cudd_Ref(bd);
00824         Cudd_RecursiveDerefZdd(dd, fd);
00825 
00826         T = cuddBddAndRecur(dd, Cudd_Not(b1), Cudd_Not(bd));
00827         if (!T) {
00828             Cudd_RecursiveDeref(dd, b1);
00829             Cudd_RecursiveDeref(dd, b0);
00830             Cudd_RecursiveDeref(dd, bd);
00831             return(NULL);
00832         }
00833         T = Cudd_NotCond(T, T != NULL);
00834         Cudd_Ref(T);
00835         Cudd_RecursiveDeref(dd, b1);
00836         E = cuddBddAndRecur(dd, Cudd_Not(b0), Cudd_Not(bd));
00837         if (!E) {
00838             Cudd_RecursiveDeref(dd, b0);
00839             Cudd_RecursiveDeref(dd, bd);
00840             Cudd_RecursiveDeref(dd, T);
00841             return(NULL);
00842         }
00843         E = Cudd_NotCond(E, E != NULL);
00844         Cudd_Ref(E);
00845         Cudd_RecursiveDeref(dd, b0);
00846         Cudd_RecursiveDeref(dd, bd);
00847     }
00848     else {
00849         Cudd_RecursiveDerefZdd(dd, fd);
00850         T = b1;
00851         E = b0;
00852     }
00853 
00854     if (Cudd_IsComplement(T)) {
00855         neW = cuddUniqueInterIVO(dd, v / 2, Cudd_Not(T), Cudd_Not(E));
00856         if (!neW) {
00857             Cudd_RecursiveDeref(dd, T);
00858             Cudd_RecursiveDeref(dd, E);
00859             return(NULL);
00860         }
00861         neW = Cudd_Not(neW);
00862     }
00863     else {
00864         neW = cuddUniqueInterIVO(dd, v / 2, T, E);
00865         if (!neW) {
00866             Cudd_RecursiveDeref(dd, T);
00867             Cudd_RecursiveDeref(dd, E);
00868             return(NULL);
00869         }
00870     }
00871     Cudd_Ref(neW);
00872     Cudd_RecursiveDeref(dd, T);
00873     Cudd_RecursiveDeref(dd, E);
00874 
00875     cuddCacheInsert1(dd, cuddMakeBddFromZddCover, node, neW);
00876     Cudd_Deref(neW);
00877     return(neW);
00878 
00879 } /* end of cuddMakeBddFromZddCover */
00880 
00881 
00882 /*---------------------------------------------------------------------------*/
00883 /* Definition of static functions                                            */
00884 /*---------------------------------------------------------------------------*/
00885