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

00001 
00078 #include "util.h"
00079 #include "cuddInt.h"
00080 
00081 /*---------------------------------------------------------------------------*/
00082 /* Constant declarations                                                     */
00083 /*---------------------------------------------------------------------------*/
00084 
00085 
00086 /*---------------------------------------------------------------------------*/
00087 /* Stucture declarations                                                     */
00088 /*---------------------------------------------------------------------------*/
00089 
00090 
00091 /*---------------------------------------------------------------------------*/
00092 /* Type declarations                                                         */
00093 /*---------------------------------------------------------------------------*/
00094 
00095 
00096 /*---------------------------------------------------------------------------*/
00097 /* Variable declarations                                                     */
00098 /*---------------------------------------------------------------------------*/
00099 
00100 #ifndef lint
00101 static char rcsid[] DD_UNUSED = "$Id: cuddZddFuncs.c,v 1.16 2008/04/25 07:39:33 fabio Exp $";
00102 #endif
00103 
00104 /*---------------------------------------------------------------------------*/
00105 /* Macro declarations                                                        */
00106 /*---------------------------------------------------------------------------*/
00107 
00108 
00111 /*---------------------------------------------------------------------------*/
00112 /* Static function prototypes                                                */
00113 /*---------------------------------------------------------------------------*/
00114 
00115 
00119 /*---------------------------------------------------------------------------*/
00120 /* Definition of exported functions                                          */
00121 /*---------------------------------------------------------------------------*/
00122 
00123 
00140 DdNode  *
00141 Cudd_zddProduct(
00142   DdManager * dd,
00143   DdNode * f,
00144   DdNode * g)
00145 {
00146     DdNode      *res;
00147 
00148     do {
00149         dd->reordered = 0;
00150         res = cuddZddProduct(dd, f, g);
00151     } while (dd->reordered == 1);
00152     return(res);
00153 
00154 } /* end of Cudd_zddProduct */
00155 
00156 
00171 DdNode  *
00172 Cudd_zddUnateProduct(
00173   DdManager * dd,
00174   DdNode * f,
00175   DdNode * g)
00176 {
00177     DdNode      *res;
00178 
00179     do {
00180         dd->reordered = 0;
00181         res = cuddZddUnateProduct(dd, f, g);
00182     } while (dd->reordered == 1);
00183     return(res);
00184 
00185 } /* end of Cudd_zddUnateProduct */
00186 
00187 
00205 DdNode  *
00206 Cudd_zddWeakDiv(
00207   DdManager * dd,
00208   DdNode * f,
00209   DdNode * g)
00210 {
00211     DdNode      *res;
00212 
00213     do {
00214         dd->reordered = 0;
00215         res = cuddZddWeakDiv(dd, f, g);
00216     } while (dd->reordered == 1);
00217     return(res);
00218 
00219 } /* end of Cudd_zddWeakDiv */
00220 
00221 
00236 DdNode  *
00237 Cudd_zddDivide(
00238   DdManager * dd,
00239   DdNode * f,
00240   DdNode * g)
00241 {
00242     DdNode      *res;
00243 
00244     do {
00245         dd->reordered = 0;
00246         res = cuddZddDivide(dd, f, g);
00247     } while (dd->reordered == 1);
00248     return(res);
00249 
00250 } /* end of Cudd_zddDivide */
00251 
00252 
00265 DdNode  *
00266 Cudd_zddWeakDivF(
00267   DdManager * dd,
00268   DdNode * f,
00269   DdNode * g)
00270 {
00271     DdNode      *res;
00272 
00273     do {
00274         dd->reordered = 0;
00275         res = cuddZddWeakDivF(dd, f, g);
00276     } while (dd->reordered == 1);
00277     return(res);
00278 
00279 } /* end of Cudd_zddWeakDivF */
00280 
00281 
00294 DdNode  *
00295 Cudd_zddDivideF(
00296   DdManager * dd,
00297   DdNode * f,
00298   DdNode * g)
00299 {
00300     DdNode      *res;
00301 
00302     do {
00303         dd->reordered = 0;
00304         res = cuddZddDivideF(dd, f, g);
00305     } while (dd->reordered == 1);
00306     return(res);
00307 
00308 } /* end of Cudd_zddDivideF */
00309 
00310 
00327 DdNode  *
00328 Cudd_zddComplement(
00329   DdManager *dd,
00330   DdNode *node)
00331 {
00332     DdNode      *b, *isop, *zdd_I;
00333 
00334     /* Check cache */
00335     zdd_I = cuddCacheLookup1Zdd(dd, cuddZddComplement, node);
00336     if (zdd_I)
00337         return(zdd_I);
00338 
00339     b = Cudd_MakeBddFromZddCover(dd, node);
00340     if (!b)
00341         return(NULL);
00342     Cudd_Ref(b);
00343     isop = Cudd_zddIsop(dd, Cudd_Not(b), Cudd_Not(b), &zdd_I);
00344     if (!isop) {
00345         Cudd_RecursiveDeref(dd, b);
00346         return(NULL);
00347     }
00348     Cudd_Ref(isop);
00349     Cudd_Ref(zdd_I);
00350     Cudd_RecursiveDeref(dd, b);
00351     Cudd_RecursiveDeref(dd, isop);
00352 
00353     cuddCacheInsert1(dd, cuddZddComplement, node, zdd_I);
00354     Cudd_Deref(zdd_I);
00355     return(zdd_I);
00356 } /* end of Cudd_zddComplement */
00357 
00358 
00359 /*---------------------------------------------------------------------------*/
00360 /* Definition of internal functions                                          */
00361 /*---------------------------------------------------------------------------*/
00362 
00363 
00375 DdNode  *
00376 cuddZddProduct(
00377   DdManager * dd,
00378   DdNode * f,
00379   DdNode * g)
00380 {
00381     int         v, top_f, top_g;
00382     DdNode      *tmp, *term1, *term2, *term3;
00383     DdNode      *f0, *f1, *fd, *g0, *g1, *gd;
00384     DdNode      *R0, *R1, *Rd, *N0, *N1;
00385     DdNode      *r;
00386     DdNode      *one = DD_ONE(dd);
00387     DdNode      *zero = DD_ZERO(dd);
00388     int         flag;
00389     int         pv, nv;
00390 
00391     statLine(dd);
00392     if (f == zero || g == zero)
00393         return(zero);
00394     if (f == one)
00395         return(g);
00396     if (g == one)
00397         return(f);
00398 
00399     top_f = dd->permZ[f->index];
00400     top_g = dd->permZ[g->index];
00401 
00402     if (top_f > top_g)
00403         return(cuddZddProduct(dd, g, f));
00404 
00405     /* Check cache */
00406     r = cuddCacheLookup2Zdd(dd, cuddZddProduct, f, g);
00407     if (r)
00408         return(r);
00409 
00410     v = f->index;       /* either yi or zi */
00411     flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);
00412     if (flag == 1)
00413         return(NULL);
00414     Cudd_Ref(f1);
00415     Cudd_Ref(f0);
00416     Cudd_Ref(fd);
00417     flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd);
00418     if (flag == 1) {
00419         Cudd_RecursiveDerefZdd(dd, f1);
00420         Cudd_RecursiveDerefZdd(dd, f0);
00421         Cudd_RecursiveDerefZdd(dd, fd);
00422         return(NULL);
00423     }
00424     Cudd_Ref(g1);
00425     Cudd_Ref(g0);
00426     Cudd_Ref(gd);
00427     pv = cuddZddGetPosVarIndex(dd, v);
00428     nv = cuddZddGetNegVarIndex(dd, v);
00429 
00430     Rd = cuddZddProduct(dd, fd, gd);
00431     if (Rd == NULL) {
00432         Cudd_RecursiveDerefZdd(dd, f1);
00433         Cudd_RecursiveDerefZdd(dd, f0);
00434         Cudd_RecursiveDerefZdd(dd, fd);
00435         Cudd_RecursiveDerefZdd(dd, g1);
00436         Cudd_RecursiveDerefZdd(dd, g0);
00437         Cudd_RecursiveDerefZdd(dd, gd);
00438         return(NULL);
00439     }
00440     Cudd_Ref(Rd);
00441 
00442     term1 = cuddZddProduct(dd, f0, g0);
00443     if (term1 == NULL) {
00444         Cudd_RecursiveDerefZdd(dd, f1);
00445         Cudd_RecursiveDerefZdd(dd, f0);
00446         Cudd_RecursiveDerefZdd(dd, fd);
00447         Cudd_RecursiveDerefZdd(dd, g1);
00448         Cudd_RecursiveDerefZdd(dd, g0);
00449         Cudd_RecursiveDerefZdd(dd, gd);
00450         Cudd_RecursiveDerefZdd(dd, Rd);
00451         return(NULL);
00452     }
00453     Cudd_Ref(term1);
00454     term2 = cuddZddProduct(dd, f0, gd);
00455     if (term2 == NULL) {
00456         Cudd_RecursiveDerefZdd(dd, f1);
00457         Cudd_RecursiveDerefZdd(dd, f0);
00458         Cudd_RecursiveDerefZdd(dd, fd);
00459         Cudd_RecursiveDerefZdd(dd, g1);
00460         Cudd_RecursiveDerefZdd(dd, g0);
00461         Cudd_RecursiveDerefZdd(dd, gd);
00462         Cudd_RecursiveDerefZdd(dd, Rd);
00463         Cudd_RecursiveDerefZdd(dd, term1);
00464         return(NULL);
00465     }
00466     Cudd_Ref(term2);
00467     term3 = cuddZddProduct(dd, fd, g0);
00468     if (term3 == NULL) {
00469         Cudd_RecursiveDerefZdd(dd, f1);
00470         Cudd_RecursiveDerefZdd(dd, f0);
00471         Cudd_RecursiveDerefZdd(dd, fd);
00472         Cudd_RecursiveDerefZdd(dd, g1);
00473         Cudd_RecursiveDerefZdd(dd, g0);
00474         Cudd_RecursiveDerefZdd(dd, gd);
00475         Cudd_RecursiveDerefZdd(dd, Rd);
00476         Cudd_RecursiveDerefZdd(dd, term1);
00477         Cudd_RecursiveDerefZdd(dd, term2);
00478         return(NULL);
00479     }
00480     Cudd_Ref(term3);
00481     Cudd_RecursiveDerefZdd(dd, f0);
00482     Cudd_RecursiveDerefZdd(dd, g0);
00483     tmp = cuddZddUnion(dd, term1, term2);
00484     if (tmp == NULL) {
00485         Cudd_RecursiveDerefZdd(dd, f1);
00486         Cudd_RecursiveDerefZdd(dd, fd);
00487         Cudd_RecursiveDerefZdd(dd, g1);
00488         Cudd_RecursiveDerefZdd(dd, gd);
00489         Cudd_RecursiveDerefZdd(dd, Rd);
00490         Cudd_RecursiveDerefZdd(dd, term1);
00491         Cudd_RecursiveDerefZdd(dd, term2);
00492         Cudd_RecursiveDerefZdd(dd, term3);
00493         return(NULL);
00494     }
00495     Cudd_Ref(tmp);
00496     Cudd_RecursiveDerefZdd(dd, term1);
00497     Cudd_RecursiveDerefZdd(dd, term2);
00498     R0 = cuddZddUnion(dd, tmp, term3);
00499     if (R0 == NULL) {
00500         Cudd_RecursiveDerefZdd(dd, f1);
00501         Cudd_RecursiveDerefZdd(dd, fd);
00502         Cudd_RecursiveDerefZdd(dd, g1);
00503         Cudd_RecursiveDerefZdd(dd, gd);
00504         Cudd_RecursiveDerefZdd(dd, Rd);
00505         Cudd_RecursiveDerefZdd(dd, term3);
00506         Cudd_RecursiveDerefZdd(dd, tmp);
00507         return(NULL);
00508     }
00509     Cudd_Ref(R0);
00510     Cudd_RecursiveDerefZdd(dd, tmp);
00511     Cudd_RecursiveDerefZdd(dd, term3);
00512     N0 = cuddZddGetNode(dd, nv, R0, Rd); /* nv = zi */
00513     if (N0 == NULL) {
00514         Cudd_RecursiveDerefZdd(dd, f1);
00515         Cudd_RecursiveDerefZdd(dd, fd);
00516         Cudd_RecursiveDerefZdd(dd, g1);
00517         Cudd_RecursiveDerefZdd(dd, gd);
00518         Cudd_RecursiveDerefZdd(dd, Rd);
00519         Cudd_RecursiveDerefZdd(dd, R0);
00520         return(NULL);
00521     }
00522     Cudd_Ref(N0);
00523     Cudd_RecursiveDerefZdd(dd, R0);
00524     Cudd_RecursiveDerefZdd(dd, Rd);
00525 
00526     term1 = cuddZddProduct(dd, f1, g1);
00527     if (term1 == NULL) {
00528         Cudd_RecursiveDerefZdd(dd, f1);
00529         Cudd_RecursiveDerefZdd(dd, fd);
00530         Cudd_RecursiveDerefZdd(dd, g1);
00531         Cudd_RecursiveDerefZdd(dd, gd);
00532         Cudd_RecursiveDerefZdd(dd, N0);
00533         return(NULL);
00534     }
00535     Cudd_Ref(term1);
00536     term2 = cuddZddProduct(dd, f1, gd);
00537     if (term2 == NULL) {
00538         Cudd_RecursiveDerefZdd(dd, f1);
00539         Cudd_RecursiveDerefZdd(dd, fd);
00540         Cudd_RecursiveDerefZdd(dd, g1);
00541         Cudd_RecursiveDerefZdd(dd, gd);
00542         Cudd_RecursiveDerefZdd(dd, N0);
00543         Cudd_RecursiveDerefZdd(dd, term1);
00544         return(NULL);
00545     }
00546     Cudd_Ref(term2);
00547     term3 = cuddZddProduct(dd, fd, g1);
00548     if (term3 == NULL) {
00549         Cudd_RecursiveDerefZdd(dd, f1);
00550         Cudd_RecursiveDerefZdd(dd, fd);
00551         Cudd_RecursiveDerefZdd(dd, g1);
00552         Cudd_RecursiveDerefZdd(dd, gd);
00553         Cudd_RecursiveDerefZdd(dd, N0);
00554         Cudd_RecursiveDerefZdd(dd, term1);
00555         Cudd_RecursiveDerefZdd(dd, term2);
00556         return(NULL);
00557     }
00558     Cudd_Ref(term3);
00559     Cudd_RecursiveDerefZdd(dd, f1);
00560     Cudd_RecursiveDerefZdd(dd, g1);
00561     Cudd_RecursiveDerefZdd(dd, fd);
00562     Cudd_RecursiveDerefZdd(dd, gd);
00563     tmp = cuddZddUnion(dd, term1, term2);
00564     if (tmp == NULL) {
00565         Cudd_RecursiveDerefZdd(dd, N0);
00566         Cudd_RecursiveDerefZdd(dd, term1);
00567         Cudd_RecursiveDerefZdd(dd, term2);
00568         Cudd_RecursiveDerefZdd(dd, term3);
00569         return(NULL);
00570     }
00571     Cudd_Ref(tmp);
00572     Cudd_RecursiveDerefZdd(dd, term1);
00573     Cudd_RecursiveDerefZdd(dd, term2);
00574     R1 = cuddZddUnion(dd, tmp, term3);
00575     if (R1 == NULL) {
00576         Cudd_RecursiveDerefZdd(dd, N0);
00577         Cudd_RecursiveDerefZdd(dd, term3);
00578         Cudd_RecursiveDerefZdd(dd, tmp);
00579         return(NULL);
00580     }
00581     Cudd_Ref(R1);
00582     Cudd_RecursiveDerefZdd(dd, tmp);
00583     Cudd_RecursiveDerefZdd(dd, term3);
00584     N1 = cuddZddGetNode(dd, pv, R1, N0); /* pv = yi */
00585     if (N1 == NULL) {
00586         Cudd_RecursiveDerefZdd(dd, N0);
00587         Cudd_RecursiveDerefZdd(dd, R1);
00588         return(NULL);
00589     }
00590     Cudd_Ref(N1);
00591     Cudd_RecursiveDerefZdd(dd, R1);
00592     Cudd_RecursiveDerefZdd(dd, N0);
00593 
00594     cuddCacheInsert2(dd, cuddZddProduct, f, g, N1);
00595     Cudd_Deref(N1);
00596     return(N1);
00597 
00598 } /* end of cuddZddProduct */
00599 
00600 
00612 DdNode  *
00613 cuddZddUnateProduct(
00614   DdManager * dd,
00615   DdNode * f,
00616   DdNode * g)
00617 {
00618     int         v, top_f, top_g;
00619     DdNode      *term1, *term2, *term3, *term4;
00620     DdNode      *sum1, *sum2;
00621     DdNode      *f0, *f1, *g0, *g1;
00622     DdNode      *r;
00623     DdNode      *one = DD_ONE(dd);
00624     DdNode      *zero = DD_ZERO(dd);
00625     int         flag;
00626 
00627     statLine(dd);
00628     if (f == zero || g == zero)
00629         return(zero);
00630     if (f == one)
00631         return(g);
00632     if (g == one)
00633         return(f);
00634 
00635     top_f = dd->permZ[f->index];
00636     top_g = dd->permZ[g->index];
00637 
00638     if (top_f > top_g)
00639         return(cuddZddUnateProduct(dd, g, f));
00640 
00641     /* Check cache */
00642     r = cuddCacheLookup2Zdd(dd, cuddZddUnateProduct, f, g);
00643     if (r)
00644         return(r);
00645 
00646     v = f->index;       /* either yi or zi */
00647     flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0);
00648     if (flag == 1)
00649         return(NULL);
00650     Cudd_Ref(f1);
00651     Cudd_Ref(f0);
00652     flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0);
00653     if (flag == 1) {
00654         Cudd_RecursiveDerefZdd(dd, f1);
00655         Cudd_RecursiveDerefZdd(dd, f0);
00656         return(NULL);
00657     }
00658     Cudd_Ref(g1);
00659     Cudd_Ref(g0);
00660 
00661     term1 = cuddZddUnateProduct(dd, f1, g1);
00662     if (term1 == NULL) {
00663         Cudd_RecursiveDerefZdd(dd, f1);
00664         Cudd_RecursiveDerefZdd(dd, f0);
00665         Cudd_RecursiveDerefZdd(dd, g1);
00666         Cudd_RecursiveDerefZdd(dd, g0);
00667         return(NULL);
00668     }
00669     Cudd_Ref(term1);
00670     term2 = cuddZddUnateProduct(dd, f1, g0);
00671     if (term2 == NULL) {
00672         Cudd_RecursiveDerefZdd(dd, f1);
00673         Cudd_RecursiveDerefZdd(dd, f0);
00674         Cudd_RecursiveDerefZdd(dd, g1);
00675         Cudd_RecursiveDerefZdd(dd, g0);
00676         Cudd_RecursiveDerefZdd(dd, term1);
00677         return(NULL);
00678     }
00679     Cudd_Ref(term2);
00680     term3 = cuddZddUnateProduct(dd, f0, g1);
00681     if (term3 == NULL) {
00682         Cudd_RecursiveDerefZdd(dd, f1);
00683         Cudd_RecursiveDerefZdd(dd, f0);
00684         Cudd_RecursiveDerefZdd(dd, g1);
00685         Cudd_RecursiveDerefZdd(dd, g0);
00686         Cudd_RecursiveDerefZdd(dd, term1);
00687         Cudd_RecursiveDerefZdd(dd, term2);
00688         return(NULL);
00689     }
00690     Cudd_Ref(term3);
00691     term4 = cuddZddUnateProduct(dd, f0, g0);
00692     if (term4 == NULL) {
00693         Cudd_RecursiveDerefZdd(dd, f1);
00694         Cudd_RecursiveDerefZdd(dd, f0);
00695         Cudd_RecursiveDerefZdd(dd, g1);
00696         Cudd_RecursiveDerefZdd(dd, g0);
00697         Cudd_RecursiveDerefZdd(dd, term1);
00698         Cudd_RecursiveDerefZdd(dd, term2);
00699         Cudd_RecursiveDerefZdd(dd, term3);
00700         return(NULL);
00701     }
00702     Cudd_Ref(term4);
00703     Cudd_RecursiveDerefZdd(dd, f1);
00704     Cudd_RecursiveDerefZdd(dd, f0);
00705     Cudd_RecursiveDerefZdd(dd, g1);
00706     Cudd_RecursiveDerefZdd(dd, g0);
00707     sum1 = cuddZddUnion(dd, term1, term2);
00708     if (sum1 == NULL) {
00709         Cudd_RecursiveDerefZdd(dd, term1);
00710         Cudd_RecursiveDerefZdd(dd, term2);
00711         Cudd_RecursiveDerefZdd(dd, term3);
00712         Cudd_RecursiveDerefZdd(dd, term4);
00713         return(NULL);
00714     }
00715     Cudd_Ref(sum1);
00716     Cudd_RecursiveDerefZdd(dd, term1);
00717     Cudd_RecursiveDerefZdd(dd, term2);
00718     sum2 = cuddZddUnion(dd, sum1, term3);
00719     if (sum2 == NULL) {
00720         Cudd_RecursiveDerefZdd(dd, term3);
00721         Cudd_RecursiveDerefZdd(dd, term4);
00722         Cudd_RecursiveDerefZdd(dd, sum1);
00723         return(NULL);
00724     }
00725     Cudd_Ref(sum2);
00726     Cudd_RecursiveDerefZdd(dd, sum1);
00727     Cudd_RecursiveDerefZdd(dd, term3);
00728     r = cuddZddGetNode(dd, v, sum2, term4);
00729     if (r == NULL) {
00730         Cudd_RecursiveDerefZdd(dd, term4);
00731         Cudd_RecursiveDerefZdd(dd, sum2);
00732         return(NULL);
00733     }
00734     Cudd_Ref(r);
00735     Cudd_RecursiveDerefZdd(dd, sum2);
00736     Cudd_RecursiveDerefZdd(dd, term4);
00737 
00738     cuddCacheInsert2(dd, cuddZddUnateProduct, f, g, r);
00739     Cudd_Deref(r);
00740     return(r);
00741 
00742 } /* end of cuddZddUnateProduct */
00743 
00744 
00756 DdNode  *
00757 cuddZddWeakDiv(
00758   DdManager * dd,
00759   DdNode * f,
00760   DdNode * g)
00761 {
00762     int         v;
00763     DdNode      *one = DD_ONE(dd);
00764     DdNode      *zero = DD_ZERO(dd);
00765     DdNode      *f0, *f1, *fd, *g0, *g1, *gd;
00766     DdNode      *q, *tmp;
00767     DdNode      *r;
00768     int         flag;
00769 
00770     statLine(dd);
00771     if (g == one)
00772         return(f);
00773     if (f == zero || f == one)
00774         return(zero);
00775     if (f == g)
00776         return(one);
00777 
00778     /* Check cache. */
00779     r = cuddCacheLookup2Zdd(dd, cuddZddWeakDiv, f, g);
00780     if (r)
00781         return(r);
00782 
00783     v = g->index;
00784 
00785     flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);
00786     if (flag == 1)
00787         return(NULL);
00788     Cudd_Ref(f1);
00789     Cudd_Ref(f0);
00790     Cudd_Ref(fd);
00791     flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd);
00792     if (flag == 1) {
00793         Cudd_RecursiveDerefZdd(dd, f1);
00794         Cudd_RecursiveDerefZdd(dd, f0);
00795         Cudd_RecursiveDerefZdd(dd, fd);
00796         return(NULL);
00797     }
00798     Cudd_Ref(g1);
00799     Cudd_Ref(g0);
00800     Cudd_Ref(gd);
00801 
00802     q = g;
00803 
00804     if (g0 != zero) {
00805         q = cuddZddWeakDiv(dd, f0, g0);
00806         if (q == NULL) {
00807             Cudd_RecursiveDerefZdd(dd, f1);
00808             Cudd_RecursiveDerefZdd(dd, f0);
00809             Cudd_RecursiveDerefZdd(dd, fd);
00810             Cudd_RecursiveDerefZdd(dd, g1);
00811             Cudd_RecursiveDerefZdd(dd, g0);
00812             Cudd_RecursiveDerefZdd(dd, gd);
00813             return(NULL);
00814         }
00815         Cudd_Ref(q);
00816     }
00817     else
00818         Cudd_Ref(q);
00819     Cudd_RecursiveDerefZdd(dd, f0);
00820     Cudd_RecursiveDerefZdd(dd, g0);
00821 
00822     if (q == zero) {
00823         Cudd_RecursiveDerefZdd(dd, f1);
00824         Cudd_RecursiveDerefZdd(dd, g1);
00825         Cudd_RecursiveDerefZdd(dd, fd);
00826         Cudd_RecursiveDerefZdd(dd, gd);
00827         cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, zero);
00828         Cudd_Deref(q);
00829         return(zero);
00830     }
00831 
00832     if (g1 != zero) {
00833         Cudd_RecursiveDerefZdd(dd, q);
00834         tmp = cuddZddWeakDiv(dd, f1, g1);
00835         if (tmp == NULL) {
00836             Cudd_RecursiveDerefZdd(dd, f1);
00837             Cudd_RecursiveDerefZdd(dd, g1);
00838             Cudd_RecursiveDerefZdd(dd, fd);
00839             Cudd_RecursiveDerefZdd(dd, gd);
00840             return(NULL);
00841         }
00842         Cudd_Ref(tmp);
00843         Cudd_RecursiveDerefZdd(dd, f1);
00844         Cudd_RecursiveDerefZdd(dd, g1);
00845         if (q == g)
00846             q = tmp;
00847         else {
00848             q = cuddZddIntersect(dd, q, tmp);
00849             if (q == NULL) {
00850                 Cudd_RecursiveDerefZdd(dd, fd);
00851                 Cudd_RecursiveDerefZdd(dd, gd);
00852                 return(NULL);
00853             }
00854             Cudd_Ref(q);
00855             Cudd_RecursiveDerefZdd(dd, tmp);
00856         }
00857     }
00858     else {
00859         Cudd_RecursiveDerefZdd(dd, f1);
00860         Cudd_RecursiveDerefZdd(dd, g1);
00861     }
00862 
00863     if (q == zero) {
00864         Cudd_RecursiveDerefZdd(dd, fd);
00865         Cudd_RecursiveDerefZdd(dd, gd);
00866         cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, zero);
00867         Cudd_Deref(q);
00868         return(zero);
00869     }
00870 
00871     if (gd != zero) {
00872         Cudd_RecursiveDerefZdd(dd, q);
00873         tmp = cuddZddWeakDiv(dd, fd, gd);
00874         if (tmp == NULL) {
00875             Cudd_RecursiveDerefZdd(dd, fd);
00876             Cudd_RecursiveDerefZdd(dd, gd);
00877             return(NULL);
00878         }
00879         Cudd_Ref(tmp);
00880         Cudd_RecursiveDerefZdd(dd, fd);
00881         Cudd_RecursiveDerefZdd(dd, gd);
00882         if (q == g)
00883             q = tmp;
00884         else {
00885             q = cuddZddIntersect(dd, q, tmp);
00886             if (q == NULL) {
00887                 Cudd_RecursiveDerefZdd(dd, tmp);
00888                 return(NULL);
00889             }
00890             Cudd_Ref(q);
00891             Cudd_RecursiveDerefZdd(dd, tmp);
00892         }
00893     }
00894     else {
00895         Cudd_RecursiveDerefZdd(dd, fd);
00896         Cudd_RecursiveDerefZdd(dd, gd);
00897     }
00898 
00899     cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, q);
00900     Cudd_Deref(q);
00901     return(q);
00902 
00903 } /* end of cuddZddWeakDiv */
00904 
00905 
00917 DdNode  *
00918 cuddZddWeakDivF(
00919   DdManager * dd,
00920   DdNode * f,
00921   DdNode * g)
00922 {
00923     int         v, top_f, top_g, vf, vg;
00924     DdNode      *one = DD_ONE(dd);
00925     DdNode      *zero = DD_ZERO(dd);
00926     DdNode      *f0, *f1, *fd, *g0, *g1, *gd;
00927     DdNode      *q, *tmp;
00928     DdNode      *r;
00929     DdNode      *term1, *term0, *termd;
00930     int         flag;
00931     int         pv, nv;
00932 
00933     statLine(dd);
00934     if (g == one)
00935         return(f);
00936     if (f == zero || f == one)
00937         return(zero);
00938     if (f == g)
00939         return(one);
00940 
00941     /* Check cache. */
00942     r = cuddCacheLookup2Zdd(dd, cuddZddWeakDivF, f, g);
00943     if (r)
00944         return(r);
00945 
00946     top_f = dd->permZ[f->index];
00947     top_g = dd->permZ[g->index];
00948     vf = top_f >> 1;
00949     vg = top_g >> 1;
00950     v = ddMin(top_f, top_g);
00951 
00952     if (v == top_f && vf < vg) {
00953         v = f->index;
00954         flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);
00955         if (flag == 1)
00956             return(NULL);
00957         Cudd_Ref(f1);
00958         Cudd_Ref(f0);
00959         Cudd_Ref(fd);
00960 
00961         pv = cuddZddGetPosVarIndex(dd, v);
00962         nv = cuddZddGetNegVarIndex(dd, v);
00963 
00964         term1 = cuddZddWeakDivF(dd, f1, g);
00965         if (term1 == NULL) {
00966             Cudd_RecursiveDerefZdd(dd, f1);
00967             Cudd_RecursiveDerefZdd(dd, f0);
00968             Cudd_RecursiveDerefZdd(dd, fd);
00969             return(NULL);
00970         }
00971         Cudd_Ref(term1);
00972         Cudd_RecursiveDerefZdd(dd, f1);
00973         term0 = cuddZddWeakDivF(dd, f0, g);
00974         if (term0 == NULL) {
00975             Cudd_RecursiveDerefZdd(dd, f0);
00976             Cudd_RecursiveDerefZdd(dd, fd);
00977             Cudd_RecursiveDerefZdd(dd, term1);
00978             return(NULL);
00979         }
00980         Cudd_Ref(term0);
00981         Cudd_RecursiveDerefZdd(dd, f0);
00982         termd = cuddZddWeakDivF(dd, fd, g);
00983         if (termd == NULL) {
00984             Cudd_RecursiveDerefZdd(dd, fd);
00985             Cudd_RecursiveDerefZdd(dd, term1);
00986             Cudd_RecursiveDerefZdd(dd, term0);
00987             return(NULL);
00988         }
00989         Cudd_Ref(termd);
00990         Cudd_RecursiveDerefZdd(dd, fd);
00991 
00992         tmp = cuddZddGetNode(dd, nv, term0, termd); /* nv = zi */
00993         if (tmp == NULL) {
00994             Cudd_RecursiveDerefZdd(dd, term1);
00995             Cudd_RecursiveDerefZdd(dd, term0);
00996             Cudd_RecursiveDerefZdd(dd, termd);
00997             return(NULL);
00998         }
00999         Cudd_Ref(tmp);
01000         Cudd_RecursiveDerefZdd(dd, term0);
01001         Cudd_RecursiveDerefZdd(dd, termd);
01002         q = cuddZddGetNode(dd, pv, term1, tmp); /* pv = yi */
01003         if (q == NULL) {
01004             Cudd_RecursiveDerefZdd(dd, term1);
01005             Cudd_RecursiveDerefZdd(dd, tmp);
01006             return(NULL);
01007         }
01008         Cudd_Ref(q);
01009         Cudd_RecursiveDerefZdd(dd, term1);
01010         Cudd_RecursiveDerefZdd(dd, tmp);
01011 
01012         cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, q);
01013         Cudd_Deref(q);
01014         return(q);
01015     }
01016 
01017     if (v == top_f)
01018         v = f->index;
01019     else
01020         v = g->index;
01021 
01022     flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);
01023     if (flag == 1)
01024         return(NULL);
01025     Cudd_Ref(f1);
01026     Cudd_Ref(f0);
01027     Cudd_Ref(fd);
01028     flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd);
01029     if (flag == 1) {
01030         Cudd_RecursiveDerefZdd(dd, f1);
01031         Cudd_RecursiveDerefZdd(dd, f0);
01032         Cudd_RecursiveDerefZdd(dd, fd);
01033         return(NULL);
01034     }
01035     Cudd_Ref(g1);
01036     Cudd_Ref(g0);
01037     Cudd_Ref(gd);
01038 
01039     q = g;
01040 
01041     if (g0 != zero) {
01042         q = cuddZddWeakDivF(dd, f0, g0);
01043         if (q == NULL) {
01044             Cudd_RecursiveDerefZdd(dd, f1);
01045             Cudd_RecursiveDerefZdd(dd, f0);
01046             Cudd_RecursiveDerefZdd(dd, fd);
01047             Cudd_RecursiveDerefZdd(dd, g1);
01048             Cudd_RecursiveDerefZdd(dd, g0);
01049             Cudd_RecursiveDerefZdd(dd, gd);
01050             return(NULL);
01051         }
01052         Cudd_Ref(q);
01053     }
01054     else
01055         Cudd_Ref(q);
01056     Cudd_RecursiveDerefZdd(dd, f0);
01057     Cudd_RecursiveDerefZdd(dd, g0);
01058 
01059     if (q == zero) {
01060         Cudd_RecursiveDerefZdd(dd, f1);
01061         Cudd_RecursiveDerefZdd(dd, g1);
01062         Cudd_RecursiveDerefZdd(dd, fd);
01063         Cudd_RecursiveDerefZdd(dd, gd);
01064         cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, zero);
01065         Cudd_Deref(q);
01066         return(zero);
01067     }
01068 
01069     if (g1 != zero) {
01070         Cudd_RecursiveDerefZdd(dd, q);
01071         tmp = cuddZddWeakDivF(dd, f1, g1);
01072         if (tmp == NULL) {
01073             Cudd_RecursiveDerefZdd(dd, f1);
01074             Cudd_RecursiveDerefZdd(dd, g1);
01075             Cudd_RecursiveDerefZdd(dd, fd);
01076             Cudd_RecursiveDerefZdd(dd, gd);
01077             return(NULL);
01078         }
01079         Cudd_Ref(tmp);
01080         Cudd_RecursiveDerefZdd(dd, f1);
01081         Cudd_RecursiveDerefZdd(dd, g1);
01082         if (q == g)
01083             q = tmp;
01084         else {
01085             q = cuddZddIntersect(dd, q, tmp);
01086             if (q == NULL) {
01087                 Cudd_RecursiveDerefZdd(dd, fd);
01088                 Cudd_RecursiveDerefZdd(dd, gd);
01089                 return(NULL);
01090             }
01091             Cudd_Ref(q);
01092             Cudd_RecursiveDerefZdd(dd, tmp);
01093         }
01094     }
01095     else {
01096         Cudd_RecursiveDerefZdd(dd, f1);
01097         Cudd_RecursiveDerefZdd(dd, g1);
01098     }
01099 
01100     if (q == zero) {
01101         Cudd_RecursiveDerefZdd(dd, fd);
01102         Cudd_RecursiveDerefZdd(dd, gd);
01103         cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, zero);
01104         Cudd_Deref(q);
01105         return(zero);
01106     }
01107 
01108     if (gd != zero) {
01109         Cudd_RecursiveDerefZdd(dd, q);
01110         tmp = cuddZddWeakDivF(dd, fd, gd);
01111         if (tmp == NULL) {
01112             Cudd_RecursiveDerefZdd(dd, fd);
01113             Cudd_RecursiveDerefZdd(dd, gd);
01114             return(NULL);
01115         }
01116         Cudd_Ref(tmp);
01117         Cudd_RecursiveDerefZdd(dd, fd);
01118         Cudd_RecursiveDerefZdd(dd, gd);
01119         if (q == g)
01120             q = tmp;
01121         else {
01122             q = cuddZddIntersect(dd, q, tmp);
01123             if (q == NULL) {
01124                 Cudd_RecursiveDerefZdd(dd, tmp);
01125                 return(NULL);
01126             }
01127             Cudd_Ref(q);
01128             Cudd_RecursiveDerefZdd(dd, tmp);
01129         }
01130     }
01131     else {
01132         Cudd_RecursiveDerefZdd(dd, fd);
01133         Cudd_RecursiveDerefZdd(dd, gd);
01134     }
01135 
01136     cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, q);
01137     Cudd_Deref(q);
01138     return(q);
01139 
01140 } /* end of cuddZddWeakDivF */
01141 
01142 
01154 DdNode  *
01155 cuddZddDivide(
01156   DdManager * dd,
01157   DdNode * f,
01158   DdNode * g)
01159 {
01160     int         v;
01161     DdNode      *one = DD_ONE(dd);
01162     DdNode      *zero = DD_ZERO(dd);
01163     DdNode      *f0, *f1, *g0, *g1;
01164     DdNode      *q, *r, *tmp;
01165     int         flag;
01166 
01167     statLine(dd);
01168     if (g == one)
01169         return(f);
01170     if (f == zero || f == one)
01171         return(zero);
01172     if (f == g)
01173         return(one);
01174 
01175     /* Check cache. */
01176     r = cuddCacheLookup2Zdd(dd, cuddZddDivide, f, g);
01177     if (r)
01178         return(r);
01179 
01180     v = g->index;
01181 
01182     flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0);
01183     if (flag == 1)
01184         return(NULL);
01185     Cudd_Ref(f1);
01186     Cudd_Ref(f0);
01187     flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0);    /* g1 != zero */
01188     if (flag == 1) {
01189         Cudd_RecursiveDerefZdd(dd, f1);
01190         Cudd_RecursiveDerefZdd(dd, f0);
01191         return(NULL);
01192     }
01193     Cudd_Ref(g1);
01194     Cudd_Ref(g0);
01195 
01196     r = cuddZddDivide(dd, f1, g1);
01197     if (r == NULL) {
01198         Cudd_RecursiveDerefZdd(dd, f1);
01199         Cudd_RecursiveDerefZdd(dd, f0);
01200         Cudd_RecursiveDerefZdd(dd, g1);
01201         Cudd_RecursiveDerefZdd(dd, g0);
01202         return(NULL);
01203     }
01204     Cudd_Ref(r);
01205 
01206     if (r != zero && g0 != zero) {
01207         tmp = r;
01208         q = cuddZddDivide(dd, f0, g0);
01209         if (q == NULL) {
01210             Cudd_RecursiveDerefZdd(dd, f1);
01211             Cudd_RecursiveDerefZdd(dd, f0);
01212             Cudd_RecursiveDerefZdd(dd, g1);
01213             Cudd_RecursiveDerefZdd(dd, g0);
01214             return(NULL);
01215         }
01216         Cudd_Ref(q);
01217         r = cuddZddIntersect(dd, r, q);
01218         if (r == NULL) {
01219             Cudd_RecursiveDerefZdd(dd, f1);
01220             Cudd_RecursiveDerefZdd(dd, f0);
01221             Cudd_RecursiveDerefZdd(dd, g1);
01222             Cudd_RecursiveDerefZdd(dd, g0);
01223             Cudd_RecursiveDerefZdd(dd, q);
01224             return(NULL);
01225         }
01226         Cudd_Ref(r);
01227         Cudd_RecursiveDerefZdd(dd, q);
01228         Cudd_RecursiveDerefZdd(dd, tmp);
01229     }
01230 
01231     Cudd_RecursiveDerefZdd(dd, f1);
01232     Cudd_RecursiveDerefZdd(dd, f0);
01233     Cudd_RecursiveDerefZdd(dd, g1);
01234     Cudd_RecursiveDerefZdd(dd, g0);
01235     
01236     cuddCacheInsert2(dd, cuddZddDivide, f, g, r);
01237     Cudd_Deref(r);
01238     return(r);
01239 
01240 } /* end of cuddZddDivide */
01241 
01242 
01254 DdNode  *
01255 cuddZddDivideF(
01256   DdManager * dd,
01257   DdNode * f,
01258   DdNode * g)
01259 {
01260     int         v;
01261     DdNode      *one = DD_ONE(dd);
01262     DdNode      *zero = DD_ZERO(dd);
01263     DdNode      *f0, *f1, *g0, *g1;
01264     DdNode      *q, *r, *tmp;
01265     int         flag;
01266 
01267     statLine(dd);
01268     if (g == one)
01269         return(f);
01270     if (f == zero || f == one)
01271         return(zero);
01272     if (f == g)
01273         return(one);
01274 
01275     /* Check cache. */
01276     r = cuddCacheLookup2Zdd(dd, cuddZddDivideF, f, g);
01277     if (r)
01278         return(r);
01279 
01280     v = g->index;
01281 
01282     flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0);
01283     if (flag == 1)
01284         return(NULL);
01285     Cudd_Ref(f1);
01286     Cudd_Ref(f0);
01287     flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0);    /* g1 != zero */
01288     if (flag == 1) {
01289         Cudd_RecursiveDerefZdd(dd, f1);
01290         Cudd_RecursiveDerefZdd(dd, f0);
01291         return(NULL);
01292     }
01293     Cudd_Ref(g1);
01294     Cudd_Ref(g0);
01295 
01296     r = cuddZddDivideF(dd, f1, g1);
01297     if (r == NULL) {
01298         Cudd_RecursiveDerefZdd(dd, f1);
01299         Cudd_RecursiveDerefZdd(dd, f0);
01300         Cudd_RecursiveDerefZdd(dd, g1);
01301         Cudd_RecursiveDerefZdd(dd, g0);
01302         return(NULL);
01303     }
01304     Cudd_Ref(r);
01305 
01306     if (r != zero && g0 != zero) {
01307         tmp = r;
01308         q = cuddZddDivideF(dd, f0, g0);
01309         if (q == NULL) {
01310             Cudd_RecursiveDerefZdd(dd, f1);
01311             Cudd_RecursiveDerefZdd(dd, f0);
01312             Cudd_RecursiveDerefZdd(dd, g1);
01313             Cudd_RecursiveDerefZdd(dd, g0);
01314             return(NULL);
01315         }
01316         Cudd_Ref(q);
01317         r = cuddZddIntersect(dd, r, q);
01318         if (r == NULL) {
01319             Cudd_RecursiveDerefZdd(dd, f1);
01320             Cudd_RecursiveDerefZdd(dd, f0);
01321             Cudd_RecursiveDerefZdd(dd, g1);
01322             Cudd_RecursiveDerefZdd(dd, g0);
01323             Cudd_RecursiveDerefZdd(dd, q);
01324             return(NULL);
01325         }
01326         Cudd_Ref(r);
01327         Cudd_RecursiveDerefZdd(dd, q);
01328         Cudd_RecursiveDerefZdd(dd, tmp);
01329     }
01330 
01331     Cudd_RecursiveDerefZdd(dd, f1);
01332     Cudd_RecursiveDerefZdd(dd, f0);
01333     Cudd_RecursiveDerefZdd(dd, g1);
01334     Cudd_RecursiveDerefZdd(dd, g0);
01335     
01336     cuddCacheInsert2(dd, cuddZddDivideF, f, g, r);
01337     Cudd_Deref(r);
01338     return(r);
01339 
01340 } /* end of cuddZddDivideF */
01341 
01342 
01355 int
01356 cuddZddGetCofactors3(
01357   DdManager * dd,
01358   DdNode * f,
01359   int  v,
01360   DdNode ** f1,
01361   DdNode ** f0,
01362   DdNode ** fd)
01363 {
01364     DdNode      *pc, *nc;
01365     DdNode      *zero = DD_ZERO(dd);
01366     int         top, hv, ht, pv, nv;
01367     int         level;
01368 
01369     top = dd->permZ[f->index];
01370     level = dd->permZ[v];
01371     hv = level >> 1;
01372     ht = top >> 1;
01373 
01374     if (hv < ht) {
01375         *f1 = zero;
01376         *f0 = zero;
01377         *fd = f;
01378     }
01379     else {
01380         pv = cuddZddGetPosVarIndex(dd, v);
01381         nv = cuddZddGetNegVarIndex(dd, v);
01382 
01383         /* not to create intermediate ZDD node */
01384         if (cuddZddGetPosVarLevel(dd, v) < cuddZddGetNegVarLevel(dd, v)) {
01385             pc = cuddZddSubset1(dd, f, pv);
01386             if (pc == NULL)
01387                 return(1);
01388             Cudd_Ref(pc);
01389             nc = cuddZddSubset0(dd, f, pv);
01390             if (nc == NULL) {
01391                 Cudd_RecursiveDerefZdd(dd, pc);
01392                 return(1);
01393             }
01394             Cudd_Ref(nc);
01395 
01396             *f1 = cuddZddSubset0(dd, pc, nv);
01397             if (*f1 == NULL) {
01398                 Cudd_RecursiveDerefZdd(dd, pc);
01399                 Cudd_RecursiveDerefZdd(dd, nc);
01400                 return(1);
01401             }
01402             Cudd_Ref(*f1);
01403             *f0 = cuddZddSubset1(dd, nc, nv);
01404             if (*f0 == NULL) {
01405                 Cudd_RecursiveDerefZdd(dd, pc);
01406                 Cudd_RecursiveDerefZdd(dd, nc);
01407                 Cudd_RecursiveDerefZdd(dd, *f1);
01408                 return(1);
01409             }
01410             Cudd_Ref(*f0);
01411 
01412             *fd = cuddZddSubset0(dd, nc, nv);
01413             if (*fd == NULL) {
01414                 Cudd_RecursiveDerefZdd(dd, pc);
01415                 Cudd_RecursiveDerefZdd(dd, nc);
01416                 Cudd_RecursiveDerefZdd(dd, *f1);
01417                 Cudd_RecursiveDerefZdd(dd, *f0);
01418                 return(1);
01419             }
01420             Cudd_Ref(*fd);
01421         } else {
01422             pc = cuddZddSubset1(dd, f, nv);
01423             if (pc == NULL)
01424                 return(1);
01425             Cudd_Ref(pc);
01426             nc = cuddZddSubset0(dd, f, nv);
01427             if (nc == NULL) {
01428                 Cudd_RecursiveDerefZdd(dd, pc);
01429                 return(1);
01430             }
01431             Cudd_Ref(nc);
01432 
01433             *f0 = cuddZddSubset0(dd, pc, pv);
01434             if (*f0 == NULL) {
01435                 Cudd_RecursiveDerefZdd(dd, pc);
01436                 Cudd_RecursiveDerefZdd(dd, nc);
01437                 return(1);
01438             }
01439             Cudd_Ref(*f0);
01440             *f1 = cuddZddSubset1(dd, nc, pv);
01441             if (*f1 == NULL) {
01442                 Cudd_RecursiveDerefZdd(dd, pc);
01443                 Cudd_RecursiveDerefZdd(dd, nc);
01444                 Cudd_RecursiveDerefZdd(dd, *f0);
01445                 return(1);
01446             }
01447             Cudd_Ref(*f1);
01448 
01449             *fd = cuddZddSubset0(dd, nc, pv);
01450             if (*fd == NULL) {
01451                 Cudd_RecursiveDerefZdd(dd, pc);
01452                 Cudd_RecursiveDerefZdd(dd, nc);
01453                 Cudd_RecursiveDerefZdd(dd, *f1);
01454                 Cudd_RecursiveDerefZdd(dd, *f0);
01455                 return(1);
01456             }
01457             Cudd_Ref(*fd);
01458         }
01459 
01460         Cudd_RecursiveDerefZdd(dd, pc);
01461         Cudd_RecursiveDerefZdd(dd, nc);
01462         Cudd_Deref(*f1);
01463         Cudd_Deref(*f0);
01464         Cudd_Deref(*fd);
01465     }
01466     return(0);
01467 
01468 } /* end of cuddZddGetCofactors3 */
01469 
01470 
01482 int
01483 cuddZddGetCofactors2(
01484   DdManager * dd,
01485   DdNode * f,
01486   int  v,
01487   DdNode ** f1,
01488   DdNode ** f0)
01489 {
01490     *f1 = cuddZddSubset1(dd, f, v);
01491     if (*f1 == NULL)
01492         return(1);
01493     *f0 = cuddZddSubset0(dd, f, v);
01494     if (*f0 == NULL) {
01495         Cudd_RecursiveDerefZdd(dd, *f1);
01496         return(1);
01497     }
01498     return(0);
01499 
01500 } /* end of cuddZddGetCofactors2 */
01501 
01502 
01517 DdNode  *
01518 cuddZddComplement(
01519   DdManager * dd,
01520   DdNode *node)
01521 {
01522     DdNode      *b, *isop, *zdd_I;
01523 
01524     /* Check cache */
01525     zdd_I = cuddCacheLookup1Zdd(dd, cuddZddComplement, node);
01526     if (zdd_I)
01527         return(zdd_I);
01528 
01529     b = cuddMakeBddFromZddCover(dd, node);
01530     if (!b)
01531         return(NULL);
01532     cuddRef(b);
01533     isop = cuddZddIsop(dd, Cudd_Not(b), Cudd_Not(b), &zdd_I);
01534     if (!isop) {
01535         Cudd_RecursiveDeref(dd, b);
01536         return(NULL);
01537     }
01538     cuddRef(isop);
01539     cuddRef(zdd_I);
01540     Cudd_RecursiveDeref(dd, b);
01541     Cudd_RecursiveDeref(dd, isop);
01542 
01543     cuddCacheInsert1(dd, cuddZddComplement, node, zdd_I);
01544     cuddDeref(zdd_I);
01545     return(zdd_I);
01546 } /* end of cuddZddComplement */
01547 
01548 
01560 int
01561 cuddZddGetPosVarIndex(
01562   DdManager * dd,
01563   int index)
01564 {
01565     int pv = (index >> 1) << 1;
01566     return(pv);
01567 } /* end of cuddZddGetPosVarIndex */
01568 
01569 
01581 int
01582 cuddZddGetNegVarIndex(
01583   DdManager * dd,
01584   int index)
01585 {
01586     int nv = index | 0x1;
01587     return(nv);
01588 } /* end of cuddZddGetPosVarIndex */
01589 
01590 
01602 int
01603 cuddZddGetPosVarLevel(
01604   DdManager * dd,
01605   int index)
01606 {
01607     int pv = cuddZddGetPosVarIndex(dd, index);
01608     return(dd->permZ[pv]);
01609 } /* end of cuddZddGetPosVarLevel */
01610 
01611 
01623 int
01624 cuddZddGetNegVarLevel(
01625   DdManager * dd,
01626   int index)
01627 {
01628     int nv = cuddZddGetNegVarIndex(dd, index);
01629     return(dd->permZ[nv]);
01630 } /* end of cuddZddGetNegVarLevel */