src/cuBdd/cuddZddIsop.c File Reference
#include "util.h"#include "cuddInt.h"
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.20 2009/02/19 16:26:12 fabio 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 170 of file cuddZddIsop.c.
00174 { 00175 DdNode *res; 00176 00177 do { 00178 dd->reordered = 0; 00179 res = cuddBddIsop(dd, L, U); 00180 } while (dd->reordered == 1); 00181 return(res); 00182 00183 } /* end of Cudd_bddIsop */
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 199 of file cuddZddIsop.c.
00202 { 00203 DdNode *res; 00204 00205 do { 00206 dd->reordered = 0; 00207 res = cuddMakeBddFromZddCover(dd, node); 00208 } while (dd->reordered == 1); 00209 return(res); 00210 } /* end of Cudd_MakeBddFromZddCover */
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 132 of file cuddZddIsop.c.
00137 { 00138 DdNode *res; 00139 int autoDynZ; 00140 00141 autoDynZ = dd->autoDynZ; 00142 dd->autoDynZ = 0; 00143 00144 do { 00145 dd->reordered = 0; 00146 res = cuddZddIsop(dd, L, U, zdd_I); 00147 } while (dd->reordered == 1); 00148 dd->autoDynZ = autoDynZ; 00149 return(res); 00150 00151 } /* end of Cudd_zddIsop */
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_bddIsop.]
Description []
SideEffects [None]
SeeAlso [Cudd_bddIsop]
Definition at line 571 of file cuddZddIsop.c.
00575 { 00576 DdNode *one = DD_ONE(dd); 00577 DdNode *zero = Cudd_Not(one); 00578 int v, top_l, top_u; 00579 DdNode *Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud; 00580 DdNode *Lsuper0, *Usuper0, *Lsuper1, *Usuper1; 00581 DdNode *Isub0, *Isub1, *Id; 00582 DdNode *x; 00583 DdNode *term0, *term1, *sum; 00584 DdNode *Lv, *Uv, *Lnv, *Unv; 00585 DdNode *r; 00586 int index; 00587 00588 statLine(dd); 00589 if (L == zero) 00590 return(zero); 00591 if (U == one) 00592 return(one); 00593 00594 /* Check cache */ 00595 r = cuddCacheLookup2(dd, cuddBddIsop, L, U); 00596 if (r) 00597 return(r); 00598 00599 top_l = dd->perm[Cudd_Regular(L)->index]; 00600 top_u = dd->perm[Cudd_Regular(U)->index]; 00601 v = ddMin(top_l, top_u); 00602 00603 /* Compute cofactors */ 00604 if (top_l == v) { 00605 index = Cudd_Regular(L)->index; 00606 Lv = Cudd_T(L); 00607 Lnv = Cudd_E(L); 00608 if (Cudd_IsComplement(L)) { 00609 Lv = Cudd_Not(Lv); 00610 Lnv = Cudd_Not(Lnv); 00611 } 00612 } 00613 else { 00614 index = Cudd_Regular(U)->index; 00615 Lv = Lnv = L; 00616 } 00617 00618 if (top_u == v) { 00619 Uv = Cudd_T(U); 00620 Unv = Cudd_E(U); 00621 if (Cudd_IsComplement(U)) { 00622 Uv = Cudd_Not(Uv); 00623 Unv = Cudd_Not(Unv); 00624 } 00625 } 00626 else { 00627 Uv = Unv = U; 00628 } 00629 00630 Lsub0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Uv)); 00631 if (Lsub0 == NULL) 00632 return(NULL); 00633 Cudd_Ref(Lsub0); 00634 Usub0 = Unv; 00635 Lsub1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Unv)); 00636 if (Lsub1 == NULL) { 00637 Cudd_RecursiveDeref(dd, Lsub0); 00638 return(NULL); 00639 } 00640 Cudd_Ref(Lsub1); 00641 Usub1 = Uv; 00642 00643 Isub0 = cuddBddIsop(dd, Lsub0, Usub0); 00644 if (Isub0 == NULL) { 00645 Cudd_RecursiveDeref(dd, Lsub0); 00646 Cudd_RecursiveDeref(dd, Lsub1); 00647 return(NULL); 00648 } 00649 Cudd_Ref(Isub0); 00650 Isub1 = cuddBddIsop(dd, Lsub1, Usub1); 00651 if (Isub1 == NULL) { 00652 Cudd_RecursiveDeref(dd, Lsub0); 00653 Cudd_RecursiveDeref(dd, Lsub1); 00654 Cudd_RecursiveDeref(dd, Isub0); 00655 return(NULL); 00656 } 00657 Cudd_Ref(Isub1); 00658 Cudd_RecursiveDeref(dd, Lsub0); 00659 Cudd_RecursiveDeref(dd, Lsub1); 00660 00661 Lsuper0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Isub0)); 00662 if (Lsuper0 == NULL) { 00663 Cudd_RecursiveDeref(dd, Isub0); 00664 Cudd_RecursiveDeref(dd, Isub1); 00665 return(NULL); 00666 } 00667 Cudd_Ref(Lsuper0); 00668 Lsuper1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Isub1)); 00669 if (Lsuper1 == NULL) { 00670 Cudd_RecursiveDeref(dd, Isub0); 00671 Cudd_RecursiveDeref(dd, Isub1); 00672 Cudd_RecursiveDeref(dd, Lsuper0); 00673 return(NULL); 00674 } 00675 Cudd_Ref(Lsuper1); 00676 Usuper0 = Unv; 00677 Usuper1 = Uv; 00678 00679 /* Ld = Lsuper0 + Lsuper1 */ 00680 Ld = cuddBddAndRecur(dd, Cudd_Not(Lsuper0), Cudd_Not(Lsuper1)); 00681 Ld = Cudd_NotCond(Ld, Ld != NULL); 00682 if (Ld == NULL) { 00683 Cudd_RecursiveDeref(dd, Isub0); 00684 Cudd_RecursiveDeref(dd, Isub1); 00685 Cudd_RecursiveDeref(dd, Lsuper0); 00686 Cudd_RecursiveDeref(dd, Lsuper1); 00687 return(NULL); 00688 } 00689 Cudd_Ref(Ld); 00690 Ud = cuddBddAndRecur(dd, Usuper0, Usuper1); 00691 if (Ud == NULL) { 00692 Cudd_RecursiveDeref(dd, Isub0); 00693 Cudd_RecursiveDeref(dd, Isub1); 00694 Cudd_RecursiveDeref(dd, Lsuper0); 00695 Cudd_RecursiveDeref(dd, Lsuper1); 00696 Cudd_RecursiveDeref(dd, Ld); 00697 return(NULL); 00698 } 00699 Cudd_Ref(Ud); 00700 Cudd_RecursiveDeref(dd, Lsuper0); 00701 Cudd_RecursiveDeref(dd, Lsuper1); 00702 00703 Id = cuddBddIsop(dd, Ld, Ud); 00704 if (Id == NULL) { 00705 Cudd_RecursiveDeref(dd, Isub0); 00706 Cudd_RecursiveDeref(dd, Isub1); 00707 Cudd_RecursiveDeref(dd, Ld); 00708 Cudd_RecursiveDeref(dd, Ud); 00709 return(NULL); 00710 } 00711 Cudd_Ref(Id); 00712 Cudd_RecursiveDeref(dd, Ld); 00713 Cudd_RecursiveDeref(dd, Ud); 00714 00715 x = cuddUniqueInter(dd, index, one, zero); 00716 if (x == NULL) { 00717 Cudd_RecursiveDeref(dd, Isub0); 00718 Cudd_RecursiveDeref(dd, Isub1); 00719 Cudd_RecursiveDeref(dd, Id); 00720 return(NULL); 00721 } 00722 Cudd_Ref(x); 00723 term0 = cuddBddAndRecur(dd, Cudd_Not(x), Isub0); 00724 if (term0 == NULL) { 00725 Cudd_RecursiveDeref(dd, Isub0); 00726 Cudd_RecursiveDeref(dd, Isub1); 00727 Cudd_RecursiveDeref(dd, Id); 00728 Cudd_RecursiveDeref(dd, x); 00729 return(NULL); 00730 } 00731 Cudd_Ref(term0); 00732 Cudd_RecursiveDeref(dd, Isub0); 00733 term1 = cuddBddAndRecur(dd, x, Isub1); 00734 if (term1 == NULL) { 00735 Cudd_RecursiveDeref(dd, Isub1); 00736 Cudd_RecursiveDeref(dd, Id); 00737 Cudd_RecursiveDeref(dd, x); 00738 Cudd_RecursiveDeref(dd, term0); 00739 return(NULL); 00740 } 00741 Cudd_Ref(term1); 00742 Cudd_RecursiveDeref(dd, x); 00743 Cudd_RecursiveDeref(dd, Isub1); 00744 /* sum = term0 + term1 */ 00745 sum = cuddBddAndRecur(dd, Cudd_Not(term0), Cudd_Not(term1)); 00746 sum = Cudd_NotCond(sum, sum != NULL); 00747 if (sum == NULL) { 00748 Cudd_RecursiveDeref(dd, Id); 00749 Cudd_RecursiveDeref(dd, term0); 00750 Cudd_RecursiveDeref(dd, term1); 00751 return(NULL); 00752 } 00753 Cudd_Ref(sum); 00754 Cudd_RecursiveDeref(dd, term0); 00755 Cudd_RecursiveDeref(dd, term1); 00756 /* r = sum + Id */ 00757 r = cuddBddAndRecur(dd, Cudd_Not(sum), Cudd_Not(Id)); 00758 r = Cudd_NotCond(r, r != NULL); 00759 if (r == NULL) { 00760 Cudd_RecursiveDeref(dd, Id); 00761 Cudd_RecursiveDeref(dd, sum); 00762 return(NULL); 00763 } 00764 Cudd_Ref(r); 00765 Cudd_RecursiveDeref(dd, sum); 00766 Cudd_RecursiveDeref(dd, Id); 00767 00768 cuddCacheInsert2(dd, cuddBddIsop, L, U, r); 00769 00770 Cudd_Deref(r); 00771 return(r); 00772 00773 } /* end of cuddBddIsop */
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 796 of file cuddZddIsop.c.
00799 { 00800 DdNode *neW; 00801 int v; 00802 DdNode *f1, *f0, *fd; 00803 DdNode *b1, *b0, *bd; 00804 DdNode *T, *E; 00805 00806 statLine(dd); 00807 if (node == dd->one) 00808 return(dd->one); 00809 if (node == dd->zero) 00810 return(Cudd_Not(dd->one)); 00811 00812 /* Check cache */ 00813 neW = cuddCacheLookup1(dd, cuddMakeBddFromZddCover, node); 00814 if (neW) 00815 return(neW); 00816 00817 v = Cudd_Regular(node)->index; /* either yi or zi */ 00818 if (cuddZddGetCofactors3(dd, node, v, &f1, &f0, &fd)) return(NULL); 00819 Cudd_Ref(f1); 00820 Cudd_Ref(f0); 00821 Cudd_Ref(fd); 00822 00823 b1 = cuddMakeBddFromZddCover(dd, f1); 00824 if (!b1) { 00825 Cudd_RecursiveDerefZdd(dd, f1); 00826 Cudd_RecursiveDerefZdd(dd, f0); 00827 Cudd_RecursiveDerefZdd(dd, fd); 00828 return(NULL); 00829 } 00830 Cudd_Ref(b1); 00831 b0 = cuddMakeBddFromZddCover(dd, f0); 00832 if (!b0) { 00833 Cudd_RecursiveDerefZdd(dd, f1); 00834 Cudd_RecursiveDerefZdd(dd, f0); 00835 Cudd_RecursiveDerefZdd(dd, fd); 00836 Cudd_RecursiveDeref(dd, b1); 00837 return(NULL); 00838 } 00839 Cudd_Ref(b0); 00840 Cudd_RecursiveDerefZdd(dd, f1); 00841 Cudd_RecursiveDerefZdd(dd, f0); 00842 if (fd != dd->zero) { 00843 bd = cuddMakeBddFromZddCover(dd, fd); 00844 if (!bd) { 00845 Cudd_RecursiveDerefZdd(dd, fd); 00846 Cudd_RecursiveDeref(dd, b1); 00847 Cudd_RecursiveDeref(dd, b0); 00848 return(NULL); 00849 } 00850 Cudd_Ref(bd); 00851 Cudd_RecursiveDerefZdd(dd, fd); 00852 00853 T = cuddBddAndRecur(dd, Cudd_Not(b1), Cudd_Not(bd)); 00854 if (!T) { 00855 Cudd_RecursiveDeref(dd, b1); 00856 Cudd_RecursiveDeref(dd, b0); 00857 Cudd_RecursiveDeref(dd, bd); 00858 return(NULL); 00859 } 00860 T = Cudd_NotCond(T, T != NULL); 00861 Cudd_Ref(T); 00862 Cudd_RecursiveDeref(dd, b1); 00863 E = cuddBddAndRecur(dd, Cudd_Not(b0), Cudd_Not(bd)); 00864 if (!E) { 00865 Cudd_RecursiveDeref(dd, b0); 00866 Cudd_RecursiveDeref(dd, bd); 00867 Cudd_RecursiveDeref(dd, T); 00868 return(NULL); 00869 } 00870 E = Cudd_NotCond(E, E != NULL); 00871 Cudd_Ref(E); 00872 Cudd_RecursiveDeref(dd, b0); 00873 Cudd_RecursiveDeref(dd, bd); 00874 } 00875 else { 00876 Cudd_RecursiveDerefZdd(dd, fd); 00877 T = b1; 00878 E = b0; 00879 } 00880 00881 if (Cudd_IsComplement(T)) { 00882 neW = cuddUniqueInterIVO(dd, v / 2, Cudd_Not(T), Cudd_Not(E)); 00883 if (!neW) { 00884 Cudd_RecursiveDeref(dd, T); 00885 Cudd_RecursiveDeref(dd, E); 00886 return(NULL); 00887 } 00888 neW = Cudd_Not(neW); 00889 } 00890 else { 00891 neW = cuddUniqueInterIVO(dd, v / 2, T, E); 00892 if (!neW) { 00893 Cudd_RecursiveDeref(dd, T); 00894 Cudd_RecursiveDeref(dd, E); 00895 return(NULL); 00896 } 00897 } 00898 Cudd_Ref(neW); 00899 Cudd_RecursiveDeref(dd, T); 00900 Cudd_RecursiveDeref(dd, E); 00901 00902 cuddCacheInsert1(dd, cuddMakeBddFromZddCover, node, neW); 00903 Cudd_Deref(neW); 00904 return(neW); 00905 00906 } /* end of cuddMakeBddFromZddCover */
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddIsop.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddIsop]
Definition at line 230 of file cuddZddIsop.c.
00235 { 00236 DdNode *one = DD_ONE(dd); 00237 DdNode *zero = Cudd_Not(one); 00238 DdNode *zdd_one = DD_ONE(dd); 00239 DdNode *zdd_zero = DD_ZERO(dd); 00240 int v, top_l, top_u; 00241 DdNode *Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud; 00242 DdNode *Lsuper0, *Usuper0, *Lsuper1, *Usuper1; 00243 DdNode *Isub0, *Isub1, *Id; 00244 DdNode *zdd_Isub0, *zdd_Isub1, *zdd_Id; 00245 DdNode *x; 00246 DdNode *term0, *term1, *sum; 00247 DdNode *Lv, *Uv, *Lnv, *Unv; 00248 DdNode *r, *y, *z; 00249 int index; 00250 DD_CTFP cacheOp; 00251 00252 statLine(dd); 00253 if (L == zero) { 00254 *zdd_I = zdd_zero; 00255 return(zero); 00256 } 00257 if (U == one) { 00258 *zdd_I = zdd_one; 00259 return(one); 00260 } 00261 00262 if (U == zero || L == one) { 00263 printf("*** ERROR : illegal condition for ISOP (U < L).\n"); 00264 exit(1); 00265 } 00266 00267 /* Check the cache. We store two results for each recursive call. 00268 ** One is the BDD, and the other is the ZDD. Both are needed. 00269 ** Hence we need a double hit in the cache to terminate the 00270 ** recursion. Clearly, collisions may evict only one of the two 00271 ** results. */ 00272 cacheOp = (DD_CTFP) cuddZddIsop; 00273 r = cuddCacheLookup2(dd, cuddBddIsop, L, U); 00274 if (r) { 00275 *zdd_I = cuddCacheLookup2Zdd(dd, cacheOp, L, U); 00276 if (*zdd_I) 00277 return(r); 00278 else { 00279 /* The BDD result may have been dead. In that case 00280 ** cuddCacheLookup2 would have called cuddReclaim, 00281 ** whose effects we now have to undo. */ 00282 cuddRef(r); 00283 Cudd_RecursiveDeref(dd, r); 00284 } 00285 } 00286 00287 top_l = dd->perm[Cudd_Regular(L)->index]; 00288 top_u = dd->perm[Cudd_Regular(U)->index]; 00289 v = ddMin(top_l, top_u); 00290 00291 /* Compute cofactors. */ 00292 if (top_l == v) { 00293 index = Cudd_Regular(L)->index; 00294 Lv = Cudd_T(L); 00295 Lnv = Cudd_E(L); 00296 if (Cudd_IsComplement(L)) { 00297 Lv = Cudd_Not(Lv); 00298 Lnv = Cudd_Not(Lnv); 00299 } 00300 } 00301 else { 00302 index = Cudd_Regular(U)->index; 00303 Lv = Lnv = L; 00304 } 00305 00306 if (top_u == v) { 00307 Uv = Cudd_T(U); 00308 Unv = Cudd_E(U); 00309 if (Cudd_IsComplement(U)) { 00310 Uv = Cudd_Not(Uv); 00311 Unv = Cudd_Not(Unv); 00312 } 00313 } 00314 else { 00315 Uv = Unv = U; 00316 } 00317 00318 Lsub0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Uv)); 00319 if (Lsub0 == NULL) 00320 return(NULL); 00321 Cudd_Ref(Lsub0); 00322 Usub0 = Unv; 00323 Lsub1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Unv)); 00324 if (Lsub1 == NULL) { 00325 Cudd_RecursiveDeref(dd, Lsub0); 00326 return(NULL); 00327 } 00328 Cudd_Ref(Lsub1); 00329 Usub1 = Uv; 00330 00331 Isub0 = cuddZddIsop(dd, Lsub0, Usub0, &zdd_Isub0); 00332 if (Isub0 == NULL) { 00333 Cudd_RecursiveDeref(dd, Lsub0); 00334 Cudd_RecursiveDeref(dd, Lsub1); 00335 return(NULL); 00336 } 00337 /* 00338 if ((!cuddIsConstant(Cudd_Regular(Isub0))) && 00339 (Cudd_Regular(Isub0)->index != zdd_Isub0->index / 2 || 00340 dd->permZ[index * 2] > dd->permZ[zdd_Isub0->index])) { 00341 printf("*** ERROR : illegal permutation in ZDD. ***\n"); 00342 } 00343 */ 00344 Cudd_Ref(Isub0); 00345 Cudd_Ref(zdd_Isub0); 00346 Isub1 = cuddZddIsop(dd, Lsub1, Usub1, &zdd_Isub1); 00347 if (Isub1 == NULL) { 00348 Cudd_RecursiveDeref(dd, Lsub0); 00349 Cudd_RecursiveDeref(dd, Lsub1); 00350 Cudd_RecursiveDeref(dd, Isub0); 00351 Cudd_RecursiveDerefZdd(dd, zdd_Isub0); 00352 return(NULL); 00353 } 00354 /* 00355 if ((!cuddIsConstant(Cudd_Regular(Isub1))) && 00356 (Cudd_Regular(Isub1)->index != zdd_Isub1->index / 2 || 00357 dd->permZ[index * 2] > dd->permZ[zdd_Isub1->index])) { 00358 printf("*** ERROR : illegal permutation in ZDD. ***\n"); 00359 } 00360 */ 00361 Cudd_Ref(Isub1); 00362 Cudd_Ref(zdd_Isub1); 00363 Cudd_RecursiveDeref(dd, Lsub0); 00364 Cudd_RecursiveDeref(dd, Lsub1); 00365 00366 Lsuper0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Isub0)); 00367 if (Lsuper0 == NULL) { 00368 Cudd_RecursiveDeref(dd, Isub0); 00369 Cudd_RecursiveDerefZdd(dd, zdd_Isub0); 00370 Cudd_RecursiveDeref(dd, Isub1); 00371 Cudd_RecursiveDerefZdd(dd, zdd_Isub1); 00372 return(NULL); 00373 } 00374 Cudd_Ref(Lsuper0); 00375 Lsuper1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Isub1)); 00376 if (Lsuper1 == NULL) { 00377 Cudd_RecursiveDeref(dd, Isub0); 00378 Cudd_RecursiveDerefZdd(dd, zdd_Isub0); 00379 Cudd_RecursiveDeref(dd, Isub1); 00380 Cudd_RecursiveDerefZdd(dd, zdd_Isub1); 00381 Cudd_RecursiveDeref(dd, Lsuper0); 00382 return(NULL); 00383 } 00384 Cudd_Ref(Lsuper1); 00385 Usuper0 = Unv; 00386 Usuper1 = Uv; 00387 00388 /* Ld = Lsuper0 + Lsuper1 */ 00389 Ld = cuddBddAndRecur(dd, Cudd_Not(Lsuper0), Cudd_Not(Lsuper1)); 00390 if (Ld == NULL) { 00391 Cudd_RecursiveDeref(dd, Isub0); 00392 Cudd_RecursiveDerefZdd(dd, zdd_Isub0); 00393 Cudd_RecursiveDeref(dd, Isub1); 00394 Cudd_RecursiveDerefZdd(dd, zdd_Isub1); 00395 Cudd_RecursiveDeref(dd, Lsuper0); 00396 Cudd_RecursiveDeref(dd, Lsuper1); 00397 return(NULL); 00398 } 00399 Ld = Cudd_Not(Ld); 00400 Cudd_Ref(Ld); 00401 /* Ud = Usuper0 * Usuper1 */ 00402 Ud = cuddBddAndRecur(dd, Usuper0, Usuper1); 00403 if (Ud == NULL) { 00404 Cudd_RecursiveDeref(dd, Isub0); 00405 Cudd_RecursiveDerefZdd(dd, zdd_Isub0); 00406 Cudd_RecursiveDeref(dd, Isub1); 00407 Cudd_RecursiveDerefZdd(dd, zdd_Isub1); 00408 Cudd_RecursiveDeref(dd, Lsuper0); 00409 Cudd_RecursiveDeref(dd, Lsuper1); 00410 Cudd_RecursiveDeref(dd, Ld); 00411 return(NULL); 00412 } 00413 Cudd_Ref(Ud); 00414 Cudd_RecursiveDeref(dd, Lsuper0); 00415 Cudd_RecursiveDeref(dd, Lsuper1); 00416 00417 Id = cuddZddIsop(dd, Ld, Ud, &zdd_Id); 00418 if (Id == NULL) { 00419 Cudd_RecursiveDeref(dd, Isub0); 00420 Cudd_RecursiveDerefZdd(dd, zdd_Isub0); 00421 Cudd_RecursiveDeref(dd, Isub1); 00422 Cudd_RecursiveDerefZdd(dd, zdd_Isub1); 00423 Cudd_RecursiveDeref(dd, Ld); 00424 Cudd_RecursiveDeref(dd, Ud); 00425 return(NULL); 00426 } 00427 /* 00428 if ((!cuddIsConstant(Cudd_Regular(Id))) && 00429 (Cudd_Regular(Id)->index != zdd_Id->index / 2 || 00430 dd->permZ[index * 2] > dd->permZ[zdd_Id->index])) { 00431 printf("*** ERROR : illegal permutation in ZDD. ***\n"); 00432 } 00433 */ 00434 Cudd_Ref(Id); 00435 Cudd_Ref(zdd_Id); 00436 Cudd_RecursiveDeref(dd, Ld); 00437 Cudd_RecursiveDeref(dd, Ud); 00438 00439 x = cuddUniqueInter(dd, index, one, zero); 00440 if (x == NULL) { 00441 Cudd_RecursiveDeref(dd, Isub0); 00442 Cudd_RecursiveDerefZdd(dd, zdd_Isub0); 00443 Cudd_RecursiveDeref(dd, Isub1); 00444 Cudd_RecursiveDerefZdd(dd, zdd_Isub1); 00445 Cudd_RecursiveDeref(dd, Id); 00446 Cudd_RecursiveDerefZdd(dd, zdd_Id); 00447 return(NULL); 00448 } 00449 Cudd_Ref(x); 00450 /* term0 = x * Isub0 */ 00451 term0 = cuddBddAndRecur(dd, Cudd_Not(x), Isub0); 00452 if (term0 == NULL) { 00453 Cudd_RecursiveDeref(dd, Isub0); 00454 Cudd_RecursiveDerefZdd(dd, zdd_Isub0); 00455 Cudd_RecursiveDeref(dd, Isub1); 00456 Cudd_RecursiveDerefZdd(dd, zdd_Isub1); 00457 Cudd_RecursiveDeref(dd, Id); 00458 Cudd_RecursiveDerefZdd(dd, zdd_Id); 00459 Cudd_RecursiveDeref(dd, x); 00460 return(NULL); 00461 } 00462 Cudd_Ref(term0); 00463 Cudd_RecursiveDeref(dd, Isub0); 00464 /* term1 = x * Isub1 */ 00465 term1 = cuddBddAndRecur(dd, x, Isub1); 00466 if (term1 == NULL) { 00467 Cudd_RecursiveDerefZdd(dd, zdd_Isub0); 00468 Cudd_RecursiveDeref(dd, Isub1); 00469 Cudd_RecursiveDerefZdd(dd, zdd_Isub1); 00470 Cudd_RecursiveDeref(dd, Id); 00471 Cudd_RecursiveDerefZdd(dd, zdd_Id); 00472 Cudd_RecursiveDeref(dd, x); 00473 Cudd_RecursiveDeref(dd, term0); 00474 return(NULL); 00475 } 00476 Cudd_Ref(term1); 00477 Cudd_RecursiveDeref(dd, x); 00478 Cudd_RecursiveDeref(dd, Isub1); 00479 /* sum = term0 + term1 */ 00480 sum = cuddBddAndRecur(dd, Cudd_Not(term0), Cudd_Not(term1)); 00481 if (sum == NULL) { 00482 Cudd_RecursiveDerefZdd(dd, zdd_Isub0); 00483 Cudd_RecursiveDerefZdd(dd, zdd_Isub1); 00484 Cudd_RecursiveDeref(dd, Id); 00485 Cudd_RecursiveDerefZdd(dd, zdd_Id); 00486 Cudd_RecursiveDeref(dd, term0); 00487 Cudd_RecursiveDeref(dd, term1); 00488 return(NULL); 00489 } 00490 sum = Cudd_Not(sum); 00491 Cudd_Ref(sum); 00492 Cudd_RecursiveDeref(dd, term0); 00493 Cudd_RecursiveDeref(dd, term1); 00494 /* r = sum + Id */ 00495 r = cuddBddAndRecur(dd, Cudd_Not(sum), Cudd_Not(Id)); 00496 r = Cudd_NotCond(r, r != NULL); 00497 if (r == NULL) { 00498 Cudd_RecursiveDerefZdd(dd, zdd_Isub0); 00499 Cudd_RecursiveDerefZdd(dd, zdd_Isub1); 00500 Cudd_RecursiveDeref(dd, Id); 00501 Cudd_RecursiveDerefZdd(dd, zdd_Id); 00502 Cudd_RecursiveDeref(dd, sum); 00503 return(NULL); 00504 } 00505 Cudd_Ref(r); 00506 Cudd_RecursiveDeref(dd, sum); 00507 Cudd_RecursiveDeref(dd, Id); 00508 00509 if (zdd_Isub0 != zdd_zero) { 00510 z = cuddZddGetNodeIVO(dd, index * 2 + 1, zdd_Isub0, zdd_Id); 00511 if (z == NULL) { 00512 Cudd_RecursiveDerefZdd(dd, zdd_Isub0); 00513 Cudd_RecursiveDerefZdd(dd, zdd_Isub1); 00514 Cudd_RecursiveDerefZdd(dd, zdd_Id); 00515 Cudd_RecursiveDeref(dd, r); 00516 return(NULL); 00517 } 00518 } 00519 else { 00520 z = zdd_Id; 00521 } 00522 Cudd_Ref(z); 00523 if (zdd_Isub1 != zdd_zero) { 00524 y = cuddZddGetNodeIVO(dd, index * 2, zdd_Isub1, z); 00525 if (y == NULL) { 00526 Cudd_RecursiveDerefZdd(dd, zdd_Isub0); 00527 Cudd_RecursiveDerefZdd(dd, zdd_Isub1); 00528 Cudd_RecursiveDerefZdd(dd, zdd_Id); 00529 Cudd_RecursiveDeref(dd, r); 00530 Cudd_RecursiveDerefZdd(dd, z); 00531 return(NULL); 00532 } 00533 } 00534 else 00535 y = z; 00536 Cudd_Ref(y); 00537 00538 Cudd_RecursiveDerefZdd(dd, zdd_Isub0); 00539 Cudd_RecursiveDerefZdd(dd, zdd_Isub1); 00540 Cudd_RecursiveDerefZdd(dd, zdd_Id); 00541 Cudd_RecursiveDerefZdd(dd, z); 00542 00543 cuddCacheInsert2(dd, cuddBddIsop, L, U, r); 00544 cuddCacheInsert2(dd, cacheOp, L, U, y); 00545 00546 Cudd_Deref(r); 00547 Cudd_Deref(y); 00548 *zdd_I = y; 00549 /* 00550 if (Cudd_Regular(r)->index != y->index / 2) { 00551 printf("*** ERROR : mismatch in indices between BDD and ZDD. ***\n"); 00552 } 00553 */ 00554 return(r); 00555 00556 } /* end of cuddZddIsop */
Variable Documentation
char rcsid [] DD_UNUSED = "$Id: cuddZddIsop.c,v 1.20 2009/02/19 16:26:12 fabio 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 [Copyright (c) 1995-2004, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
Definition at line 87 of file cuddZddIsop.c.
