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

00001 
00051 #include        "util_hack.h"
00052 #include        "cuddInt.h"
00053 
00054 /*---------------------------------------------------------------------------*/
00055 /* Constant declarations                                                     */
00056 /*---------------------------------------------------------------------------*/
00057 
00058 
00059 /*---------------------------------------------------------------------------*/
00060 /* Stucture declarations                                                     */
00061 /*---------------------------------------------------------------------------*/
00062 
00063 
00064 /*---------------------------------------------------------------------------*/
00065 /* Type declarations                                                         */
00066 /*---------------------------------------------------------------------------*/
00067 
00068 
00069 /*---------------------------------------------------------------------------*/
00070 /* Variable declarations                                                     */
00071 /*---------------------------------------------------------------------------*/
00072 
00073 #ifndef lint
00074 static char rcsid[] DD_UNUSED = "$Id: cuddZddFuncs.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $";
00075 #endif
00076 
00077 /*---------------------------------------------------------------------------*/
00078 /* Macro declarations                                                        */
00079 /*---------------------------------------------------------------------------*/
00080 
00081 
00084 /*---------------------------------------------------------------------------*/
00085 /* Static function prototypes                                                */
00086 /*---------------------------------------------------------------------------*/
00087 
00088 
00092 /*---------------------------------------------------------------------------*/
00093 /* Definition of exported functions                                          */
00094 /*---------------------------------------------------------------------------*/
00095 
00096 
00113 DdNode  *
00114 Cudd_zddProduct(
00115   DdManager * dd,
00116   DdNode * f,
00117   DdNode * g)
00118 {
00119     DdNode      *res;
00120 
00121     do {
00122         dd->reordered = 0;
00123         res = cuddZddProduct(dd, f, g);
00124     } while (dd->reordered == 1);
00125     return(res);
00126 
00127 } /* end of Cudd_zddProduct */
00128 
00129 
00144 DdNode  *
00145 Cudd_zddUnateProduct(
00146   DdManager * dd,
00147   DdNode * f,
00148   DdNode * g)
00149 {
00150     DdNode      *res;
00151 
00152     do {
00153         dd->reordered = 0;
00154         res = cuddZddUnateProduct(dd, f, g);
00155     } while (dd->reordered == 1);
00156     return(res);
00157 
00158 } /* end of Cudd_zddUnateProduct */
00159 
00160 
00178 DdNode  *
00179 Cudd_zddWeakDiv(
00180   DdManager * dd,
00181   DdNode * f,
00182   DdNode * g)
00183 {
00184     DdNode      *res;
00185 
00186     do {
00187         dd->reordered = 0;
00188         res = cuddZddWeakDiv(dd, f, g);
00189     } while (dd->reordered == 1);
00190     return(res);
00191 
00192 } /* end of Cudd_zddWeakDiv */
00193 
00194 
00209 DdNode  *
00210 Cudd_zddDivide(
00211   DdManager * dd,
00212   DdNode * f,
00213   DdNode * g)
00214 {
00215     DdNode      *res;
00216 
00217     do {
00218         dd->reordered = 0;
00219         res = cuddZddDivide(dd, f, g);
00220     } while (dd->reordered == 1);
00221     return(res);
00222 
00223 } /* end of Cudd_zddDivide */
00224 
00225 
00238 DdNode  *
00239 Cudd_zddWeakDivF(
00240   DdManager * dd,
00241   DdNode * f,
00242   DdNode * g)
00243 {
00244     DdNode      *res;
00245 
00246     do {
00247         dd->reordered = 0;
00248         res = cuddZddWeakDivF(dd, f, g);
00249     } while (dd->reordered == 1);
00250     return(res);
00251 
00252 } /* end of Cudd_zddWeakDivF */
00253 
00254 
00267 DdNode  *
00268 Cudd_zddDivideF(
00269   DdManager * dd,
00270   DdNode * f,
00271   DdNode * g)
00272 {
00273     DdNode      *res;
00274 
00275     do {
00276         dd->reordered = 0;
00277         res = cuddZddDivideF(dd, f, g);
00278     } while (dd->reordered == 1);
00279     return(res);
00280 
00281 } /* end of Cudd_zddDivideF */
00282 
00283 
00300 DdNode  *
00301 Cudd_zddComplement(
00302   DdManager *dd,
00303   DdNode *node)
00304 {
00305     DdNode      *b, *isop, *zdd_I;
00306 
00307     /* Check cache */
00308     zdd_I = cuddCacheLookup1Zdd(dd, cuddZddComplement, node);
00309     if (zdd_I)
00310         return(zdd_I);
00311 
00312     b = Cudd_MakeBddFromZddCover(dd, node);
00313     if (!b)
00314         return(NULL);
00315     Cudd_Ref(b);
00316     isop = Cudd_zddIsop(dd, Cudd_Not(b), Cudd_Not(b), &zdd_I);
00317     if (!isop) {
00318         Cudd_RecursiveDeref(dd, b);
00319         return(NULL);
00320     }
00321     Cudd_Ref(isop);
00322     Cudd_Ref(zdd_I);
00323     Cudd_RecursiveDeref(dd, b);
00324     Cudd_RecursiveDeref(dd, isop);
00325 
00326     cuddCacheInsert1(dd, cuddZddComplement, node, zdd_I);
00327     Cudd_Deref(zdd_I);
00328     return(zdd_I);
00329 } /* end of Cudd_zddComplement */
00330 
00331 
00332 /*---------------------------------------------------------------------------*/
00333 /* Definition of internal functions                                          */
00334 /*---------------------------------------------------------------------------*/
00335 
00336 
00348 DdNode  *
00349 cuddZddProduct(
00350   DdManager * dd,
00351   DdNode * f,
00352   DdNode * g)
00353 {
00354     int         v, top_f, top_g;
00355     DdNode      *tmp, *term1, *term2, *term3;
00356     DdNode      *f0, *f1, *fd, *g0, *g1, *gd;
00357     DdNode      *R0, *R1, *Rd, *N0, *N1;
00358     DdNode      *r;
00359     DdNode      *one = DD_ONE(dd);
00360     DdNode      *zero = DD_ZERO(dd);
00361     int         flag;
00362     int         pv, nv;
00363 
00364     statLine(dd);
00365     if (f == zero || g == zero)
00366         return(zero);
00367     if (f == one)
00368         return(g);
00369     if (g == one)
00370         return(f);
00371 
00372     top_f = dd->permZ[f->index];
00373     top_g = dd->permZ[g->index];
00374 
00375     if (top_f > top_g)
00376         return(cuddZddProduct(dd, g, f));
00377 
00378     /* Check cache */
00379     r = cuddCacheLookup2Zdd(dd, cuddZddProduct, f, g);
00380     if (r)
00381         return(r);
00382 
00383     v = f->index;       /* either yi or zi */
00384     flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);
00385     if (flag == 1)
00386         return(NULL);
00387     Cudd_Ref(f1);
00388     Cudd_Ref(f0);
00389     Cudd_Ref(fd);
00390     flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd);
00391     if (flag == 1) {
00392         Cudd_RecursiveDerefZdd(dd, f1);
00393         Cudd_RecursiveDerefZdd(dd, f0);
00394         Cudd_RecursiveDerefZdd(dd, fd);
00395         return(NULL);
00396     }
00397     Cudd_Ref(g1);
00398     Cudd_Ref(g0);
00399     Cudd_Ref(gd);
00400     pv = cuddZddGetPosVarIndex(dd, v);
00401     nv = cuddZddGetNegVarIndex(dd, v);
00402 
00403     Rd = cuddZddProduct(dd, fd, gd);
00404     if (Rd == NULL) {
00405         Cudd_RecursiveDerefZdd(dd, f1);
00406         Cudd_RecursiveDerefZdd(dd, f0);
00407         Cudd_RecursiveDerefZdd(dd, fd);
00408         Cudd_RecursiveDerefZdd(dd, g1);
00409         Cudd_RecursiveDerefZdd(dd, g0);
00410         Cudd_RecursiveDerefZdd(dd, gd);
00411         return(NULL);
00412     }
00413     Cudd_Ref(Rd);
00414 
00415     term1 = cuddZddProduct(dd, f0, g0);
00416     if (term1 == NULL) {
00417         Cudd_RecursiveDerefZdd(dd, f1);
00418         Cudd_RecursiveDerefZdd(dd, f0);
00419         Cudd_RecursiveDerefZdd(dd, fd);
00420         Cudd_RecursiveDerefZdd(dd, g1);
00421         Cudd_RecursiveDerefZdd(dd, g0);
00422         Cudd_RecursiveDerefZdd(dd, gd);
00423         Cudd_RecursiveDerefZdd(dd, Rd);
00424         return(NULL);
00425     }
00426     Cudd_Ref(term1);
00427     term2 = cuddZddProduct(dd, f0, gd);
00428     if (term2 == NULL) {
00429         Cudd_RecursiveDerefZdd(dd, f1);
00430         Cudd_RecursiveDerefZdd(dd, f0);
00431         Cudd_RecursiveDerefZdd(dd, fd);
00432         Cudd_RecursiveDerefZdd(dd, g1);
00433         Cudd_RecursiveDerefZdd(dd, g0);
00434         Cudd_RecursiveDerefZdd(dd, gd);
00435         Cudd_RecursiveDerefZdd(dd, Rd);
00436         Cudd_RecursiveDerefZdd(dd, term1);
00437         return(NULL);
00438     }
00439     Cudd_Ref(term2);
00440     term3 = cuddZddProduct(dd, fd, g0);
00441     if (term3 == NULL) {
00442         Cudd_RecursiveDerefZdd(dd, f1);
00443         Cudd_RecursiveDerefZdd(dd, f0);
00444         Cudd_RecursiveDerefZdd(dd, fd);
00445         Cudd_RecursiveDerefZdd(dd, g1);
00446         Cudd_RecursiveDerefZdd(dd, g0);
00447         Cudd_RecursiveDerefZdd(dd, gd);
00448         Cudd_RecursiveDerefZdd(dd, Rd);
00449         Cudd_RecursiveDerefZdd(dd, term1);
00450         Cudd_RecursiveDerefZdd(dd, term2);
00451         return(NULL);
00452     }
00453     Cudd_Ref(term3);
00454     Cudd_RecursiveDerefZdd(dd, f0);
00455     Cudd_RecursiveDerefZdd(dd, g0);
00456     tmp = cuddZddUnion(dd, term1, term2);
00457     if (tmp == NULL) {
00458         Cudd_RecursiveDerefZdd(dd, f1);
00459         Cudd_RecursiveDerefZdd(dd, fd);
00460         Cudd_RecursiveDerefZdd(dd, g1);
00461         Cudd_RecursiveDerefZdd(dd, gd);
00462         Cudd_RecursiveDerefZdd(dd, Rd);
00463         Cudd_RecursiveDerefZdd(dd, term1);
00464         Cudd_RecursiveDerefZdd(dd, term2);
00465         Cudd_RecursiveDerefZdd(dd, term3);
00466         return(NULL);
00467     }
00468     Cudd_Ref(tmp);
00469     Cudd_RecursiveDerefZdd(dd, term1);
00470     Cudd_RecursiveDerefZdd(dd, term2);
00471     R0 = cuddZddUnion(dd, tmp, term3);
00472     if (R0 == NULL) {
00473         Cudd_RecursiveDerefZdd(dd, f1);
00474         Cudd_RecursiveDerefZdd(dd, fd);
00475         Cudd_RecursiveDerefZdd(dd, g1);
00476         Cudd_RecursiveDerefZdd(dd, gd);
00477         Cudd_RecursiveDerefZdd(dd, Rd);
00478         Cudd_RecursiveDerefZdd(dd, term3);
00479         Cudd_RecursiveDerefZdd(dd, tmp);
00480         return(NULL);
00481     }
00482     Cudd_Ref(R0);
00483     Cudd_RecursiveDerefZdd(dd, tmp);
00484     Cudd_RecursiveDerefZdd(dd, term3);
00485     N0 = cuddZddGetNode(dd, nv, R0, Rd); /* nv = zi */
00486     if (N0 == NULL) {
00487         Cudd_RecursiveDerefZdd(dd, f1);
00488         Cudd_RecursiveDerefZdd(dd, fd);
00489         Cudd_RecursiveDerefZdd(dd, g1);
00490         Cudd_RecursiveDerefZdd(dd, gd);
00491         Cudd_RecursiveDerefZdd(dd, Rd);
00492         Cudd_RecursiveDerefZdd(dd, R0);
00493         return(NULL);
00494     }
00495     Cudd_Ref(N0);
00496     Cudd_RecursiveDerefZdd(dd, R0);
00497     Cudd_RecursiveDerefZdd(dd, Rd);
00498 
00499     term1 = cuddZddProduct(dd, f1, g1);
00500     if (term1 == NULL) {
00501         Cudd_RecursiveDerefZdd(dd, f1);
00502         Cudd_RecursiveDerefZdd(dd, fd);
00503         Cudd_RecursiveDerefZdd(dd, g1);
00504         Cudd_RecursiveDerefZdd(dd, gd);
00505         Cudd_RecursiveDerefZdd(dd, N0);
00506         return(NULL);
00507     }
00508     Cudd_Ref(term1);
00509     term2 = cuddZddProduct(dd, f1, gd);
00510     if (term2 == NULL) {
00511         Cudd_RecursiveDerefZdd(dd, f1);
00512         Cudd_RecursiveDerefZdd(dd, fd);
00513         Cudd_RecursiveDerefZdd(dd, g1);
00514         Cudd_RecursiveDerefZdd(dd, gd);
00515         Cudd_RecursiveDerefZdd(dd, N0);
00516         Cudd_RecursiveDerefZdd(dd, term1);
00517         return(NULL);
00518     }
00519     Cudd_Ref(term2);
00520     term3 = cuddZddProduct(dd, fd, g1);
00521     if (term3 == NULL) {
00522         Cudd_RecursiveDerefZdd(dd, f1);
00523         Cudd_RecursiveDerefZdd(dd, fd);
00524         Cudd_RecursiveDerefZdd(dd, g1);
00525         Cudd_RecursiveDerefZdd(dd, gd);
00526         Cudd_RecursiveDerefZdd(dd, N0);
00527         Cudd_RecursiveDerefZdd(dd, term1);
00528         Cudd_RecursiveDerefZdd(dd, term2);
00529         return(NULL);
00530     }
00531     Cudd_Ref(term3);
00532     Cudd_RecursiveDerefZdd(dd, f1);
00533     Cudd_RecursiveDerefZdd(dd, g1);
00534     Cudd_RecursiveDerefZdd(dd, fd);
00535     Cudd_RecursiveDerefZdd(dd, gd);
00536     tmp = cuddZddUnion(dd, term1, term2);
00537     if (tmp == NULL) {
00538         Cudd_RecursiveDerefZdd(dd, N0);
00539         Cudd_RecursiveDerefZdd(dd, term1);
00540         Cudd_RecursiveDerefZdd(dd, term2);
00541         Cudd_RecursiveDerefZdd(dd, term3);
00542         return(NULL);
00543     }
00544     Cudd_Ref(tmp);
00545     Cudd_RecursiveDerefZdd(dd, term1);
00546     Cudd_RecursiveDerefZdd(dd, term2);
00547     R1 = cuddZddUnion(dd, tmp, term3);
00548     if (R1 == NULL) {
00549         Cudd_RecursiveDerefZdd(dd, N0);
00550         Cudd_RecursiveDerefZdd(dd, term3);
00551         Cudd_RecursiveDerefZdd(dd, tmp);
00552         return(NULL);
00553     }
00554     Cudd_Ref(R1);
00555     Cudd_RecursiveDerefZdd(dd, tmp);
00556     Cudd_RecursiveDerefZdd(dd, term3);
00557     N1 = cuddZddGetNode(dd, pv, R1, N0); /* pv = yi */
00558     if (N1 == NULL) {
00559         Cudd_RecursiveDerefZdd(dd, N0);
00560         Cudd_RecursiveDerefZdd(dd, R1);
00561         return(NULL);
00562     }
00563     Cudd_Ref(N1);
00564     Cudd_RecursiveDerefZdd(dd, R1);
00565     Cudd_RecursiveDerefZdd(dd, N0);
00566 
00567     cuddCacheInsert2(dd, cuddZddProduct, f, g, N1);
00568     Cudd_Deref(N1);
00569     return(N1);
00570 
00571 } /* end of cuddZddProduct */
00572 
00573 
00585 DdNode  *
00586 cuddZddUnateProduct(
00587   DdManager * dd,
00588   DdNode * f,
00589   DdNode * g)
00590 {
00591     int         v, top_f, top_g;
00592     DdNode      *term1, *term2, *term3, *term4;
00593     DdNode      *sum1, *sum2;
00594     DdNode      *f0, *f1, *g0, *g1;
00595     DdNode      *r;
00596     DdNode      *one = DD_ONE(dd);
00597     DdNode      *zero = DD_ZERO(dd);
00598     int         flag;
00599 
00600     statLine(dd);
00601     if (f == zero || g == zero)
00602         return(zero);
00603     if (f == one)
00604         return(g);
00605     if (g == one)
00606         return(f);
00607 
00608     top_f = dd->permZ[f->index];
00609     top_g = dd->permZ[g->index];
00610 
00611     if (top_f > top_g)
00612         return(cuddZddUnateProduct(dd, g, f));
00613 
00614     /* Check cache */
00615     r = cuddCacheLookup2Zdd(dd, cuddZddUnateProduct, f, g);
00616     if (r)
00617         return(r);
00618 
00619     v = f->index;       /* either yi or zi */
00620     flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0);
00621     if (flag == 1)
00622         return(NULL);
00623     Cudd_Ref(f1);
00624     Cudd_Ref(f0);
00625     flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0);
00626     if (flag == 1) {
00627         Cudd_RecursiveDerefZdd(dd, f1);
00628         Cudd_RecursiveDerefZdd(dd, f0);
00629         return(NULL);
00630     }
00631     Cudd_Ref(g1);
00632     Cudd_Ref(g0);
00633 
00634     term1 = cuddZddUnateProduct(dd, f1, g1);
00635     if (term1 == NULL) {
00636         Cudd_RecursiveDerefZdd(dd, f1);
00637         Cudd_RecursiveDerefZdd(dd, f0);
00638         Cudd_RecursiveDerefZdd(dd, g1);
00639         Cudd_RecursiveDerefZdd(dd, g0);
00640         return(NULL);
00641     }
00642     Cudd_Ref(term1);
00643     term2 = cuddZddUnateProduct(dd, f1, g0);
00644     if (term2 == NULL) {
00645         Cudd_RecursiveDerefZdd(dd, f1);
00646         Cudd_RecursiveDerefZdd(dd, f0);
00647         Cudd_RecursiveDerefZdd(dd, g1);
00648         Cudd_RecursiveDerefZdd(dd, g0);
00649         Cudd_RecursiveDerefZdd(dd, term1);
00650         return(NULL);
00651     }
00652     Cudd_Ref(term2);
00653     term3 = cuddZddUnateProduct(dd, f0, g1);
00654     if (term3 == NULL) {
00655         Cudd_RecursiveDerefZdd(dd, f1);
00656         Cudd_RecursiveDerefZdd(dd, f0);
00657         Cudd_RecursiveDerefZdd(dd, g1);
00658         Cudd_RecursiveDerefZdd(dd, g0);
00659         Cudd_RecursiveDerefZdd(dd, term1);
00660         Cudd_RecursiveDerefZdd(dd, term2);
00661         return(NULL);
00662     }
00663     Cudd_Ref(term3);
00664     term4 = cuddZddUnateProduct(dd, f0, g0);
00665     if (term4 == NULL) {
00666         Cudd_RecursiveDerefZdd(dd, f1);
00667         Cudd_RecursiveDerefZdd(dd, f0);
00668         Cudd_RecursiveDerefZdd(dd, g1);
00669         Cudd_RecursiveDerefZdd(dd, g0);
00670         Cudd_RecursiveDerefZdd(dd, term1);
00671         Cudd_RecursiveDerefZdd(dd, term2);
00672         Cudd_RecursiveDerefZdd(dd, term3);
00673         return(NULL);
00674     }
00675     Cudd_Ref(term4);
00676     Cudd_RecursiveDerefZdd(dd, f1);
00677     Cudd_RecursiveDerefZdd(dd, f0);
00678     Cudd_RecursiveDerefZdd(dd, g1);
00679     Cudd_RecursiveDerefZdd(dd, g0);
00680     sum1 = cuddZddUnion(dd, term1, term2);
00681     if (sum1 == NULL) {
00682         Cudd_RecursiveDerefZdd(dd, term1);
00683         Cudd_RecursiveDerefZdd(dd, term2);
00684         Cudd_RecursiveDerefZdd(dd, term3);
00685         Cudd_RecursiveDerefZdd(dd, term4);
00686         return(NULL);
00687     }
00688     Cudd_Ref(sum1);
00689     Cudd_RecursiveDerefZdd(dd, term1);
00690     Cudd_RecursiveDerefZdd(dd, term2);
00691     sum2 = cuddZddUnion(dd, sum1, term3);
00692     if (sum2 == NULL) {
00693         Cudd_RecursiveDerefZdd(dd, term3);
00694         Cudd_RecursiveDerefZdd(dd, term4);
00695         Cudd_RecursiveDerefZdd(dd, sum1);
00696         return(NULL);
00697     }
00698     Cudd_Ref(sum2);
00699     Cudd_RecursiveDerefZdd(dd, sum1);
00700     Cudd_RecursiveDerefZdd(dd, term3);
00701     r = cuddZddGetNode(dd, v, sum2, term4);
00702     if (r == NULL) {
00703         Cudd_RecursiveDerefZdd(dd, term4);
00704         Cudd_RecursiveDerefZdd(dd, sum2);
00705         return(NULL);
00706     }
00707     Cudd_Ref(r);
00708     Cudd_RecursiveDerefZdd(dd, sum2);
00709     Cudd_RecursiveDerefZdd(dd, term4);
00710 
00711     cuddCacheInsert2(dd, cuddZddUnateProduct, f, g, r);
00712     Cudd_Deref(r);
00713     return(r);
00714 
00715 } /* end of cuddZddUnateProduct */
00716 
00717 
00729 DdNode  *
00730 cuddZddWeakDiv(
00731   DdManager * dd,
00732   DdNode * f,
00733   DdNode * g)
00734 {
00735     int         v;
00736     DdNode      *one = DD_ONE(dd);
00737     DdNode      *zero = DD_ZERO(dd);
00738     DdNode      *f0, *f1, *fd, *g0, *g1, *gd;
00739     DdNode      *q, *tmp;
00740     DdNode      *r;
00741     int         flag;
00742 
00743     statLine(dd);
00744     if (g == one)
00745         return(f);
00746     if (f == zero || f == one)
00747         return(zero);
00748     if (f == g)
00749         return(one);
00750 
00751     /* Check cache. */
00752     r = cuddCacheLookup2Zdd(dd, cuddZddWeakDiv, f, g);
00753     if (r)
00754         return(r);
00755 
00756     v = g->index;
00757 
00758     flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);
00759     if (flag == 1)
00760         return(NULL);
00761     Cudd_Ref(f1);
00762     Cudd_Ref(f0);
00763     Cudd_Ref(fd);
00764     flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd);
00765     if (flag == 1) {
00766         Cudd_RecursiveDerefZdd(dd, f1);
00767         Cudd_RecursiveDerefZdd(dd, f0);
00768         Cudd_RecursiveDerefZdd(dd, fd);
00769         return(NULL);
00770     }
00771     Cudd_Ref(g1);
00772     Cudd_Ref(g0);
00773     Cudd_Ref(gd);
00774 
00775     q = g;
00776 
00777     if (g0 != zero) {
00778         q = cuddZddWeakDiv(dd, f0, g0);
00779         if (q == NULL) {
00780             Cudd_RecursiveDerefZdd(dd, f1);
00781             Cudd_RecursiveDerefZdd(dd, f0);
00782             Cudd_RecursiveDerefZdd(dd, fd);
00783             Cudd_RecursiveDerefZdd(dd, g1);
00784             Cudd_RecursiveDerefZdd(dd, g0);
00785             Cudd_RecursiveDerefZdd(dd, gd);
00786             return(NULL);
00787         }
00788         Cudd_Ref(q);
00789     }
00790     else
00791         Cudd_Ref(q);
00792     Cudd_RecursiveDerefZdd(dd, f0);
00793     Cudd_RecursiveDerefZdd(dd, g0);
00794 
00795     if (q == zero) {
00796         Cudd_RecursiveDerefZdd(dd, f1);
00797         Cudd_RecursiveDerefZdd(dd, g1);
00798         Cudd_RecursiveDerefZdd(dd, fd);
00799         Cudd_RecursiveDerefZdd(dd, gd);
00800         cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, zero);
00801         Cudd_Deref(q);
00802         return(zero);
00803     }
00804 
00805     if (g1 != zero) {
00806         Cudd_RecursiveDerefZdd(dd, q);
00807         tmp = cuddZddWeakDiv(dd, f1, g1);
00808         if (tmp == NULL) {
00809             Cudd_RecursiveDerefZdd(dd, f1);
00810             Cudd_RecursiveDerefZdd(dd, g1);
00811             Cudd_RecursiveDerefZdd(dd, fd);
00812             Cudd_RecursiveDerefZdd(dd, gd);
00813             return(NULL);
00814         }
00815         Cudd_Ref(tmp);
00816         Cudd_RecursiveDerefZdd(dd, f1);
00817         Cudd_RecursiveDerefZdd(dd, g1);
00818         if (q == g)
00819             q = tmp;
00820         else {
00821             q = cuddZddIntersect(dd, q, tmp);
00822             if (q == NULL) {
00823                 Cudd_RecursiveDerefZdd(dd, fd);
00824                 Cudd_RecursiveDerefZdd(dd, gd);
00825                 return(NULL);
00826             }
00827             Cudd_Ref(q);
00828             Cudd_RecursiveDerefZdd(dd, tmp);
00829         }
00830     }
00831     else {
00832         Cudd_RecursiveDerefZdd(dd, f1);
00833         Cudd_RecursiveDerefZdd(dd, g1);
00834     }
00835 
00836     if (q == zero) {
00837         Cudd_RecursiveDerefZdd(dd, fd);
00838         Cudd_RecursiveDerefZdd(dd, gd);
00839         cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, zero);
00840         Cudd_Deref(q);
00841         return(zero);
00842     }
00843 
00844     if (gd != zero) {
00845         Cudd_RecursiveDerefZdd(dd, q);
00846         tmp = cuddZddWeakDiv(dd, fd, gd);
00847         if (tmp == NULL) {
00848             Cudd_RecursiveDerefZdd(dd, fd);
00849             Cudd_RecursiveDerefZdd(dd, gd);
00850             return(NULL);
00851         }
00852         Cudd_Ref(tmp);
00853         Cudd_RecursiveDerefZdd(dd, fd);
00854         Cudd_RecursiveDerefZdd(dd, gd);
00855         if (q == g)
00856             q = tmp;
00857         else {
00858             q = cuddZddIntersect(dd, q, tmp);
00859             if (q == NULL) {
00860                 Cudd_RecursiveDerefZdd(dd, tmp);
00861                 return(NULL);
00862             }
00863             Cudd_Ref(q);
00864             Cudd_RecursiveDerefZdd(dd, tmp);
00865         }
00866     }
00867     else {
00868         Cudd_RecursiveDerefZdd(dd, fd);
00869         Cudd_RecursiveDerefZdd(dd, gd);
00870     }
00871 
00872     cuddCacheInsert2(dd, cuddZddWeakDiv, f, g, q);
00873     Cudd_Deref(q);
00874     return(q);
00875 
00876 } /* end of cuddZddWeakDiv */
00877 
00878 
00890 DdNode  *
00891 cuddZddWeakDivF(
00892   DdManager * dd,
00893   DdNode * f,
00894   DdNode * g)
00895 {
00896     int         v, top_f, top_g, vf, vg;
00897     DdNode      *one = DD_ONE(dd);
00898     DdNode      *zero = DD_ZERO(dd);
00899     DdNode      *f0, *f1, *fd, *g0, *g1, *gd;
00900     DdNode      *q, *tmp;
00901     DdNode      *r;
00902     DdNode      *term1, *term0, *termd;
00903     int         flag;
00904     int         pv, nv;
00905 
00906     statLine(dd);
00907     if (g == one)
00908         return(f);
00909     if (f == zero || f == one)
00910         return(zero);
00911     if (f == g)
00912         return(one);
00913 
00914     /* Check cache. */
00915     r = cuddCacheLookup2Zdd(dd, cuddZddWeakDivF, f, g);
00916     if (r)
00917         return(r);
00918 
00919     top_f = dd->permZ[f->index];
00920     top_g = dd->permZ[g->index];
00921     vf = top_f >> 1;
00922     vg = top_g >> 1;
00923     v = ddMin(top_f, top_g);
00924 
00925     if (v == top_f && vf < vg) {
00926         v = f->index;
00927         flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);
00928         if (flag == 1)
00929             return(NULL);
00930         Cudd_Ref(f1);
00931         Cudd_Ref(f0);
00932         Cudd_Ref(fd);
00933 
00934         pv = cuddZddGetPosVarIndex(dd, v);
00935         nv = cuddZddGetNegVarIndex(dd, v);
00936 
00937         term1 = cuddZddWeakDivF(dd, f1, g);
00938         if (term1 == NULL) {
00939             Cudd_RecursiveDerefZdd(dd, f1);
00940             Cudd_RecursiveDerefZdd(dd, f0);
00941             Cudd_RecursiveDerefZdd(dd, fd);
00942             return(NULL);
00943         }
00944         Cudd_Ref(term1);
00945         Cudd_RecursiveDerefZdd(dd, f1);
00946         term0 = cuddZddWeakDivF(dd, f0, g);
00947         if (term0 == NULL) {
00948             Cudd_RecursiveDerefZdd(dd, f0);
00949             Cudd_RecursiveDerefZdd(dd, fd);
00950             Cudd_RecursiveDerefZdd(dd, term1);
00951             return(NULL);
00952         }
00953         Cudd_Ref(term0);
00954         Cudd_RecursiveDerefZdd(dd, f0);
00955         termd = cuddZddWeakDivF(dd, fd, g);
00956         if (termd == NULL) {
00957             Cudd_RecursiveDerefZdd(dd, fd);
00958             Cudd_RecursiveDerefZdd(dd, term1);
00959             Cudd_RecursiveDerefZdd(dd, term0);
00960             return(NULL);
00961         }
00962         Cudd_Ref(termd);
00963         Cudd_RecursiveDerefZdd(dd, fd);
00964 
00965         tmp = cuddZddGetNode(dd, nv, term0, termd); /* nv = zi */
00966         if (tmp == NULL) {
00967             Cudd_RecursiveDerefZdd(dd, term1);
00968             Cudd_RecursiveDerefZdd(dd, term0);
00969             Cudd_RecursiveDerefZdd(dd, termd);
00970             return(NULL);
00971         }
00972         Cudd_Ref(tmp);
00973         Cudd_RecursiveDerefZdd(dd, term0);
00974         Cudd_RecursiveDerefZdd(dd, termd);
00975         q = cuddZddGetNode(dd, pv, term1, tmp); /* pv = yi */
00976         if (q == NULL) {
00977             Cudd_RecursiveDerefZdd(dd, term1);
00978             Cudd_RecursiveDerefZdd(dd, tmp);
00979             return(NULL);
00980         }
00981         Cudd_Ref(q);
00982         Cudd_RecursiveDerefZdd(dd, term1);
00983         Cudd_RecursiveDerefZdd(dd, tmp);
00984 
00985         cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, q);
00986         Cudd_Deref(q);
00987         return(q);
00988     }
00989 
00990     if (v == top_f)
00991         v = f->index;
00992     else
00993         v = g->index;
00994 
00995     flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);
00996     if (flag == 1)
00997         return(NULL);
00998     Cudd_Ref(f1);
00999     Cudd_Ref(f0);
01000     Cudd_Ref(fd);
01001     flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd);
01002     if (flag == 1) {
01003         Cudd_RecursiveDerefZdd(dd, f1);
01004         Cudd_RecursiveDerefZdd(dd, f0);
01005         Cudd_RecursiveDerefZdd(dd, fd);
01006         return(NULL);
01007     }
01008     Cudd_Ref(g1);
01009     Cudd_Ref(g0);
01010     Cudd_Ref(gd);
01011 
01012     q = g;
01013 
01014     if (g0 != zero) {
01015         q = cuddZddWeakDivF(dd, f0, g0);
01016         if (q == NULL) {
01017             Cudd_RecursiveDerefZdd(dd, f1);
01018             Cudd_RecursiveDerefZdd(dd, f0);
01019             Cudd_RecursiveDerefZdd(dd, fd);
01020             Cudd_RecursiveDerefZdd(dd, g1);
01021             Cudd_RecursiveDerefZdd(dd, g0);
01022             Cudd_RecursiveDerefZdd(dd, gd);
01023             return(NULL);
01024         }
01025         Cudd_Ref(q);
01026     }
01027     else
01028         Cudd_Ref(q);
01029     Cudd_RecursiveDerefZdd(dd, f0);
01030     Cudd_RecursiveDerefZdd(dd, g0);
01031 
01032     if (q == zero) {
01033         Cudd_RecursiveDerefZdd(dd, f1);
01034         Cudd_RecursiveDerefZdd(dd, g1);
01035         Cudd_RecursiveDerefZdd(dd, fd);
01036         Cudd_RecursiveDerefZdd(dd, gd);
01037         cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, zero);
01038         Cudd_Deref(q);
01039         return(zero);
01040     }
01041 
01042     if (g1 != zero) {
01043         Cudd_RecursiveDerefZdd(dd, q);
01044         tmp = cuddZddWeakDivF(dd, f1, g1);
01045         if (tmp == NULL) {
01046             Cudd_RecursiveDerefZdd(dd, f1);
01047             Cudd_RecursiveDerefZdd(dd, g1);
01048             Cudd_RecursiveDerefZdd(dd, fd);
01049             Cudd_RecursiveDerefZdd(dd, gd);
01050             return(NULL);
01051         }
01052         Cudd_Ref(tmp);
01053         Cudd_RecursiveDerefZdd(dd, f1);
01054         Cudd_RecursiveDerefZdd(dd, g1);
01055         if (q == g)
01056             q = tmp;
01057         else {
01058             q = cuddZddIntersect(dd, q, tmp);
01059             if (q == NULL) {
01060                 Cudd_RecursiveDerefZdd(dd, fd);
01061                 Cudd_RecursiveDerefZdd(dd, gd);
01062                 return(NULL);
01063             }
01064             Cudd_Ref(q);
01065             Cudd_RecursiveDerefZdd(dd, tmp);
01066         }
01067     }
01068     else {
01069         Cudd_RecursiveDerefZdd(dd, f1);
01070         Cudd_RecursiveDerefZdd(dd, g1);
01071     }
01072 
01073     if (q == zero) {
01074         Cudd_RecursiveDerefZdd(dd, fd);
01075         Cudd_RecursiveDerefZdd(dd, gd);
01076         cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, zero);
01077         Cudd_Deref(q);
01078         return(zero);
01079     }
01080 
01081     if (gd != zero) {
01082         Cudd_RecursiveDerefZdd(dd, q);
01083         tmp = cuddZddWeakDivF(dd, fd, gd);
01084         if (tmp == NULL) {
01085             Cudd_RecursiveDerefZdd(dd, fd);
01086             Cudd_RecursiveDerefZdd(dd, gd);
01087             return(NULL);
01088         }
01089         Cudd_Ref(tmp);
01090         Cudd_RecursiveDerefZdd(dd, fd);
01091         Cudd_RecursiveDerefZdd(dd, gd);
01092         if (q == g)
01093             q = tmp;
01094         else {
01095             q = cuddZddIntersect(dd, q, tmp);
01096             if (q == NULL) {
01097                 Cudd_RecursiveDerefZdd(dd, tmp);
01098                 return(NULL);
01099             }
01100             Cudd_Ref(q);
01101             Cudd_RecursiveDerefZdd(dd, tmp);
01102         }
01103     }
01104     else {
01105         Cudd_RecursiveDerefZdd(dd, fd);
01106         Cudd_RecursiveDerefZdd(dd, gd);
01107     }
01108 
01109     cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, q);
01110     Cudd_Deref(q);
01111     return(q);
01112 
01113 } /* end of cuddZddWeakDivF */
01114 
01115 
01127 DdNode  *
01128 cuddZddDivide(
01129   DdManager * dd,
01130   DdNode * f,
01131   DdNode * g)
01132 {
01133     int         v;
01134     DdNode      *one = DD_ONE(dd);
01135     DdNode      *zero = DD_ZERO(dd);
01136     DdNode      *f0, *f1, *g0, *g1;
01137     DdNode      *q, *r, *tmp;
01138     int         flag;
01139 
01140     statLine(dd);
01141     if (g == one)
01142         return(f);
01143     if (f == zero || f == one)
01144         return(zero);
01145     if (f == g)
01146         return(one);
01147 
01148     /* Check cache. */
01149     r = cuddCacheLookup2Zdd(dd, cuddZddDivide, f, g);
01150     if (r)
01151         return(r);
01152 
01153     v = g->index;
01154 
01155     flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0);
01156     if (flag == 1)
01157         return(NULL);
01158     Cudd_Ref(f1);
01159     Cudd_Ref(f0);
01160     flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0);    /* g1 != zero */
01161     if (flag == 1) {
01162         Cudd_RecursiveDerefZdd(dd, f1);
01163         Cudd_RecursiveDerefZdd(dd, f0);
01164         return(NULL);
01165     }
01166     Cudd_Ref(g1);
01167     Cudd_Ref(g0);
01168 
01169     r = cuddZddDivide(dd, f1, g1);
01170     if (r == NULL) {
01171         Cudd_RecursiveDerefZdd(dd, f1);
01172         Cudd_RecursiveDerefZdd(dd, f0);
01173         Cudd_RecursiveDerefZdd(dd, g1);
01174         Cudd_RecursiveDerefZdd(dd, g0);
01175         return(NULL);
01176     }
01177     Cudd_Ref(r);
01178 
01179     if (r != zero && g0 != zero) {
01180         tmp = r;
01181         q = cuddZddDivide(dd, f0, g0);
01182         if (q == NULL) {
01183             Cudd_RecursiveDerefZdd(dd, f1);
01184             Cudd_RecursiveDerefZdd(dd, f0);
01185             Cudd_RecursiveDerefZdd(dd, g1);
01186             Cudd_RecursiveDerefZdd(dd, g0);
01187             return(NULL);
01188         }
01189         Cudd_Ref(q);
01190         r = cuddZddIntersect(dd, r, q);
01191         if (r == NULL) {
01192             Cudd_RecursiveDerefZdd(dd, f1);
01193             Cudd_RecursiveDerefZdd(dd, f0);
01194             Cudd_RecursiveDerefZdd(dd, g1);
01195             Cudd_RecursiveDerefZdd(dd, g0);
01196             Cudd_RecursiveDerefZdd(dd, q);
01197             return(NULL);
01198         }
01199         Cudd_Ref(r);
01200         Cudd_RecursiveDerefZdd(dd, q);
01201         Cudd_RecursiveDerefZdd(dd, tmp);
01202     }
01203 
01204     Cudd_RecursiveDerefZdd(dd, f1);
01205     Cudd_RecursiveDerefZdd(dd, f0);
01206     Cudd_RecursiveDerefZdd(dd, g1);
01207     Cudd_RecursiveDerefZdd(dd, g0);
01208     
01209     cuddCacheInsert2(dd, cuddZddDivide, f, g, r);
01210     Cudd_Deref(r);
01211     return(r);
01212 
01213 } /* end of cuddZddDivide */
01214 
01215 
01227 DdNode  *
01228 cuddZddDivideF(
01229   DdManager * dd,
01230   DdNode * f,
01231   DdNode * g)
01232 {
01233     int         v;
01234     DdNode      *one = DD_ONE(dd);
01235     DdNode      *zero = DD_ZERO(dd);
01236     DdNode      *f0, *f1, *g0, *g1;
01237     DdNode      *q, *r, *tmp;
01238     int         flag;
01239 
01240     statLine(dd);
01241     if (g == one)
01242         return(f);
01243     if (f == zero || f == one)
01244         return(zero);
01245     if (f == g)
01246         return(one);
01247 
01248     /* Check cache. */
01249     r = cuddCacheLookup2Zdd(dd, cuddZddDivideF, f, g);
01250     if (r)
01251         return(r);
01252 
01253     v = g->index;
01254 
01255     flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0);
01256     if (flag == 1)
01257         return(NULL);
01258     Cudd_Ref(f1);
01259     Cudd_Ref(f0);
01260     flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0);    /* g1 != zero */
01261     if (flag == 1) {
01262         Cudd_RecursiveDerefZdd(dd, f1);
01263         Cudd_RecursiveDerefZdd(dd, f0);
01264         return(NULL);
01265     }
01266     Cudd_Ref(g1);
01267     Cudd_Ref(g0);
01268 
01269     r = cuddZddDivideF(dd, f1, g1);
01270     if (r == NULL) {
01271         Cudd_RecursiveDerefZdd(dd, f1);
01272         Cudd_RecursiveDerefZdd(dd, f0);
01273         Cudd_RecursiveDerefZdd(dd, g1);
01274         Cudd_RecursiveDerefZdd(dd, g0);
01275         return(NULL);
01276     }
01277     Cudd_Ref(r);
01278 
01279     if (r != zero && g0 != zero) {
01280         tmp = r;
01281         q = cuddZddDivideF(dd, f0, g0);
01282         if (q == NULL) {
01283             Cudd_RecursiveDerefZdd(dd, f1);
01284             Cudd_RecursiveDerefZdd(dd, f0);
01285             Cudd_RecursiveDerefZdd(dd, g1);
01286             Cudd_RecursiveDerefZdd(dd, g0);
01287             return(NULL);
01288         }
01289         Cudd_Ref(q);
01290         r = cuddZddIntersect(dd, r, q);
01291         if (r == NULL) {
01292             Cudd_RecursiveDerefZdd(dd, f1);
01293             Cudd_RecursiveDerefZdd(dd, f0);
01294             Cudd_RecursiveDerefZdd(dd, g1);
01295             Cudd_RecursiveDerefZdd(dd, g0);
01296             Cudd_RecursiveDerefZdd(dd, q);
01297             return(NULL);
01298         }
01299         Cudd_Ref(r);
01300         Cudd_RecursiveDerefZdd(dd, q);
01301         Cudd_RecursiveDerefZdd(dd, tmp);
01302     }
01303 
01304     Cudd_RecursiveDerefZdd(dd, f1);
01305     Cudd_RecursiveDerefZdd(dd, f0);
01306     Cudd_RecursiveDerefZdd(dd, g1);
01307     Cudd_RecursiveDerefZdd(dd, g0);
01308     
01309     cuddCacheInsert2(dd, cuddZddDivideF, f, g, r);
01310     Cudd_Deref(r);
01311     return(r);
01312 
01313 } /* end of cuddZddDivideF */
01314 
01315 
01328 int
01329 cuddZddGetCofactors3(
01330   DdManager * dd,
01331   DdNode * f,
01332   int  v,
01333   DdNode ** f1,
01334   DdNode ** f0,
01335   DdNode ** fd)
01336 {
01337     DdNode      *pc, *nc;
01338     DdNode      *zero = DD_ZERO(dd);
01339     int         top, hv, ht, pv, nv;
01340     int         level;
01341 
01342     top = dd->permZ[f->index];
01343     level = dd->permZ[v];
01344     hv = level >> 1;
01345     ht = top >> 1;
01346 
01347     if (hv < ht) {
01348         *f1 = zero;
01349         *f0 = zero;
01350         *fd = f;
01351     }
01352     else {
01353         pv = cuddZddGetPosVarIndex(dd, v);
01354         nv = cuddZddGetNegVarIndex(dd, v);
01355 
01356         /* not to create intermediate ZDD node */
01357         if (cuddZddGetPosVarLevel(dd, v) < cuddZddGetNegVarLevel(dd, v)) {
01358             pc = cuddZddSubset1(dd, f, pv);
01359             if (pc == NULL)
01360                 return(1);
01361             Cudd_Ref(pc);
01362             nc = cuddZddSubset0(dd, f, pv);
01363             if (nc == NULL) {
01364                 Cudd_RecursiveDerefZdd(dd, pc);
01365                 return(1);
01366             }
01367             Cudd_Ref(nc);
01368 
01369             *f1 = cuddZddSubset0(dd, pc, nv);
01370             if (*f1 == NULL) {
01371                 Cudd_RecursiveDerefZdd(dd, pc);
01372                 Cudd_RecursiveDerefZdd(dd, nc);
01373                 return(1);
01374             }
01375             Cudd_Ref(*f1);
01376             *f0 = cuddZddSubset1(dd, nc, nv);
01377             if (*f0 == NULL) {
01378                 Cudd_RecursiveDerefZdd(dd, pc);
01379                 Cudd_RecursiveDerefZdd(dd, nc);
01380                 Cudd_RecursiveDerefZdd(dd, *f1);
01381                 return(1);
01382             }
01383             Cudd_Ref(*f0);
01384 
01385             *fd = cuddZddSubset0(dd, nc, nv);
01386             if (*fd == NULL) {
01387                 Cudd_RecursiveDerefZdd(dd, pc);
01388                 Cudd_RecursiveDerefZdd(dd, nc);
01389                 Cudd_RecursiveDerefZdd(dd, *f1);
01390                 Cudd_RecursiveDerefZdd(dd, *f0);
01391                 return(1);
01392             }
01393             Cudd_Ref(*fd);
01394         } else {
01395             pc = cuddZddSubset1(dd, f, nv);
01396             if (pc == NULL)
01397                 return(1);
01398             Cudd_Ref(pc);
01399             nc = cuddZddSubset0(dd, f, nv);
01400             if (nc == NULL) {
01401                 Cudd_RecursiveDerefZdd(dd, pc);
01402                 return(1);
01403             }
01404             Cudd_Ref(nc);
01405 
01406             *f0 = cuddZddSubset0(dd, pc, pv);
01407             if (*f0 == NULL) {
01408                 Cudd_RecursiveDerefZdd(dd, pc);
01409                 Cudd_RecursiveDerefZdd(dd, nc);
01410                 return(1);
01411             }
01412             Cudd_Ref(*f0);
01413             *f1 = cuddZddSubset1(dd, nc, pv);
01414             if (*f1 == NULL) {
01415                 Cudd_RecursiveDerefZdd(dd, pc);
01416                 Cudd_RecursiveDerefZdd(dd, nc);
01417                 Cudd_RecursiveDerefZdd(dd, *f1);
01418                 return(1);
01419             }
01420             Cudd_Ref(*f1);
01421 
01422             *fd = cuddZddSubset0(dd, nc, pv);
01423             if (*fd == NULL) {
01424                 Cudd_RecursiveDerefZdd(dd, pc);
01425                 Cudd_RecursiveDerefZdd(dd, nc);
01426                 Cudd_RecursiveDerefZdd(dd, *f1);
01427                 Cudd_RecursiveDerefZdd(dd, *f0);
01428                 return(1);
01429             }
01430             Cudd_Ref(*fd);
01431         }
01432 
01433         Cudd_RecursiveDerefZdd(dd, pc);
01434         Cudd_RecursiveDerefZdd(dd, nc);
01435         Cudd_Deref(*f1);
01436         Cudd_Deref(*f0);
01437         Cudd_Deref(*fd);
01438     }
01439     return(0);
01440 
01441 } /* end of cuddZddGetCofactors3 */
01442 
01443 
01455 int
01456 cuddZddGetCofactors2(
01457   DdManager * dd,
01458   DdNode * f,
01459   int  v,
01460   DdNode ** f1,
01461   DdNode ** f0)
01462 {
01463     *f1 = cuddZddSubset1(dd, f, v);
01464     if (*f1 == NULL)
01465         return(1);
01466     *f0 = cuddZddSubset0(dd, f, v);
01467     if (*f0 == NULL) {
01468         Cudd_RecursiveDerefZdd(dd, *f1);
01469         return(1);
01470     }
01471     return(0);
01472 
01473 } /* end of cuddZddGetCofactors2 */
01474 
01475 
01490 DdNode  *
01491 cuddZddComplement(
01492   DdManager * dd,
01493   DdNode *node)
01494 {
01495     DdNode      *b, *isop, *zdd_I;
01496 
01497     /* Check cache */
01498     zdd_I = cuddCacheLookup1Zdd(dd, cuddZddComplement, node);
01499     if (zdd_I)
01500         return(zdd_I);
01501 
01502     b = cuddMakeBddFromZddCover(dd, node);
01503     if (!b)
01504         return(NULL);
01505     cuddRef(b);
01506     isop = cuddZddIsop(dd, Cudd_Not(b), Cudd_Not(b), &zdd_I);
01507     if (!isop) {
01508         Cudd_RecursiveDeref(dd, b);
01509         return(NULL);
01510     }
01511     cuddRef(isop);
01512     cuddRef(zdd_I);
01513     Cudd_RecursiveDeref(dd, b);
01514     Cudd_RecursiveDeref(dd, isop);
01515 
01516     cuddCacheInsert1(dd, cuddZddComplement, node, zdd_I);
01517     cuddDeref(zdd_I);
01518     return(zdd_I);
01519 } /* end of cuddZddComplement */
01520 
01521 
01533 int
01534 cuddZddGetPosVarIndex(
01535   DdManager * dd,
01536   int index)
01537 {
01538     int pv = (index >> 1) << 1;
01539     return(pv);
01540 } /* end of cuddZddGetPosVarIndex */
01541 
01542 
01554 int
01555 cuddZddGetNegVarIndex(
01556   DdManager * dd,
01557   int index)
01558 {
01559     int nv = index | 0x1;
01560     return(nv);
01561 } /* end of cuddZddGetPosVarIndex */
01562 
01563 
01575 int
01576 cuddZddGetPosVarLevel(
01577   DdManager * dd,
01578   int index)
01579 {
01580     int pv = cuddZddGetPosVarIndex(dd, index);
01581     return(dd->permZ[pv]);
01582 } /* end of cuddZddGetPosVarLevel */
01583 
01584 
01596 int
01597 cuddZddGetNegVarLevel(
01598   DdManager * dd,
01599   int index)
01600 {
01601     int nv = cuddZddGetNegVarIndex(dd, index);
01602     return(dd->permZ[nv]);
01603 } /* end of cuddZddGetNegVarLevel */