src/bdd/cudd/cuddZddIsop.c File Reference
#include "util_hack.h"#include "cuddInt.h"
Include dependency graph for cuddZddIsop.c:
Go to the source code of this file.
Functions | |
| DdNode * | Cudd_zddIsop (DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I) |
| DdNode * | Cudd_bddIsop (DdManager *dd, DdNode *L, DdNode *U) |
| DdNode * | Cudd_MakeBddFromZddCover (DdManager *dd, DdNode *node) |
| DdNode * | cuddZddIsop (DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I) |
| DdNode * | cuddBddIsop (DdManager *dd, DdNode *L, DdNode *U) |
| DdNode * | cuddMakeBddFromZddCover (DdManager *dd, DdNode *node) |
Variables | |
| static char rcsid[] | DD_UNUSED = "$Id: cuddZddIsop.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang Exp $" |
Function Documentation
Function********************************************************************
Synopsis [Computes a BDD in the interval between L and U with a simple sum-of-produuct cover.]
Description [Computes a BDD in the interval between L and U with a simple sum-of-produuct cover. This procedure is similar to Cudd_zddIsop, but it does not return the ZDD for the cover. Returns a pointer to the BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_zddIsop]
Definition at line 143 of file cuddZddIsop.c.
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 */
Function********************************************************************
Synopsis [Converts a ZDD cover to a BDD graph.]
Description [Converts a ZDD cover to a BDD graph. If successful, it returns a BDD node, otherwise it returns NULL.]
SideEffects []
SeeAlso [cuddMakeBddFromZddCover]
Definition at line 172 of file cuddZddIsop.c.
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 */
AutomaticStart AutomaticEnd Function********************************************************************
Synopsis [Computes an ISOP in ZDD form from BDDs.]
Description [Computes an irredundant sum of products (ISOP) in ZDD form from BDDs. The two BDDs L and U represent the lower bound and the upper bound, respectively, of the function. The ISOP uses two ZDD variables for each BDD variable: One for the positive literal, and one for the negative literal. These two variables should be adjacent in the ZDD order. The two ZDD variables corresponding to BDD variable i should have indices 2i and 2i+1. The result of this procedure depends on the variable order. If successful, Cudd_zddIsop returns the BDD for the function chosen from the interval. The ZDD representing the irredundant cover is returned as a side effect in zdd_I. In case of failure, NULL is returned.]
SideEffects [zdd_I holds the pointer to the ZDD for the ISOP on successful return.]
SeeAlso [Cudd_bddIsop Cudd_zddVarsFromBddVars]
Definition at line 105 of file cuddZddIsop.c.
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 */
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_bddIsop.]
Description []
SideEffects [None]
SeeAlso [Cudd_bddIsop]
Definition at line 544 of file cuddZddIsop.c.
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 */
Function********************************************************************
Synopsis [Converts a ZDD cover to a BDD graph.]
Description [Converts a ZDD cover to a BDD graph. If successful, it returns a BDD node, otherwise it returns NULL. It is a recursive algorithm as the following. First computes 3 cofactors of a ZDD cover; f1, f0 and fd. Second, compute BDDs(b1, b0 and bd) of f1, f0 and fd. Third, compute T=b1+bd and E=b0+bd. Fourth, compute ITE(v,T,E) where v is the variable which has the index of the top node of the ZDD cover. In this case, since the index of v can be larger than either one of T or one of E, cuddUniqueInterIVO is called, here IVO stands for independent variable ordering.]
SideEffects []
SeeAlso [Cudd_MakeBddFromZddCover]
Definition at line 769 of file cuddZddIsop.c.
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 */
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddIsop.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddIsop]
Definition at line 203 of file cuddZddIsop.c.
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 */
Variable Documentation
char rcsid [] DD_UNUSED = "$Id: cuddZddIsop.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang Exp $" [static] |
CFile***********************************************************************
FileName [cuddZddIsop.c]
PackageName [cudd]
Synopsis [Functions to find irredundant SOP covers as ZDDs from BDDs.]
Description [External procedures included in this module:
Internal procedures included in this module:
Static procedures included in this module:
SeeAlso []
Author [In-Ho Moon]
Copyright [ This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]
Definition at line 60 of file cuddZddIsop.c.
