diff options
Diffstat (limited to 'src/bdd/cudd/cuddZddIsop.c')
| -rw-r--r-- | src/bdd/cudd/cuddZddIsop.c | 885 |
1 files changed, 0 insertions, 885 deletions
diff --git a/src/bdd/cudd/cuddZddIsop.c b/src/bdd/cudd/cuddZddIsop.c deleted file mode 100644 index f4b057ea..00000000 --- a/src/bdd/cudd/cuddZddIsop.c +++ /dev/null @@ -1,885 +0,0 @@ -/**CFile*********************************************************************** - - FileName [cuddZddIsop.c] - - PackageName [cudd] - - Synopsis [Functions to find irredundant SOP covers as ZDDs from BDDs.] - - Description [External procedures included in this module: - <ul> - <li> Cudd_bddIsop() - <li> Cudd_zddIsop() - <li> Cudd_MakeBddFromZddCover() - </ul> - Internal procedures included in this module: - <ul> - <li> cuddBddIsop() - <li> cuddZddIsop() - <li> cuddMakeBddFromZddCover() - </ul> - Static procedures included in this module: - <ul> - </ul> - ] - - 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.] - -******************************************************************************/ - -#include "util_hack.h" -#include "cuddInt.h" - -/*---------------------------------------------------------------------------*/ -/* Constant declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Stucture declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Type declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Variable declarations */ -/*---------------------------------------------------------------------------*/ - -#ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddZddIsop.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang Exp $"; -#endif - -/*---------------------------------------------------------------------------*/ -/* Macro declarations */ -/*---------------------------------------------------------------------------*/ - - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - - -/**AutomaticEnd***************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Definition of exported functions */ -/*---------------------------------------------------------------------------*/ - -/**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 <code>i</code> should have indices <code>2i</code> and - <code>2i+1</code>. 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] - -******************************************************************************/ -DdNode * -Cudd_zddIsop( - DdManager * dd, - DdNode * L, - DdNode * U, - DdNode ** zdd_I) -{ - DdNode *res; - int autoDynZ; - - autoDynZ = dd->autoDynZ; - dd->autoDynZ = 0; - - do { - dd->reordered = 0; - res = cuddZddIsop(dd, L, U, zdd_I); - } while (dd->reordered == 1); - dd->autoDynZ = autoDynZ; - return(res); - -} /* end of Cudd_zddIsop */ - - -/**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] - -******************************************************************************/ -DdNode * -Cudd_bddIsop( - DdManager * dd, - DdNode * L, - DdNode * U) -{ - DdNode *res; - - do { - dd->reordered = 0; - res = cuddBddIsop(dd, L, U); - } while (dd->reordered == 1); - return(res); - -} /* 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] - -******************************************************************************/ -DdNode * -Cudd_MakeBddFromZddCover( - DdManager * dd, - DdNode * node) -{ - DdNode *res; - - do { - dd->reordered = 0; - res = cuddMakeBddFromZddCover(dd, node); - } while (dd->reordered == 1); - return(res); -} /* end of Cudd_MakeBddFromZddCover */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of internal functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Cudd_zddIsop.] - - Description [] - - SideEffects [None] - - SeeAlso [Cudd_zddIsop] - -******************************************************************************/ -DdNode * -cuddZddIsop( - DdManager * dd, - DdNode * L, - DdNode * U, - DdNode ** zdd_I) -{ - DdNode *one = DD_ONE(dd); - DdNode *zero = Cudd_Not(one); - DdNode *zdd_one = DD_ONE(dd); - DdNode *zdd_zero = DD_ZERO(dd); - int v, top_l, top_u; - DdNode *Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud; - DdNode *Lsuper0, *Usuper0, *Lsuper1, *Usuper1; - DdNode *Isub0, *Isub1, *Id; - DdNode *zdd_Isub0, *zdd_Isub1, *zdd_Id; - DdNode *x; - DdNode *term0, *term1, *sum; - DdNode *Lv, *Uv, *Lnv, *Unv; - DdNode *r, *y, *z; - int index; - DdNode *(*cacheOp)(DdManager *, DdNode *, DdNode *); - - statLine(dd); - if (L == zero) { - *zdd_I = zdd_zero; - return(zero); - } - if (U == one) { - *zdd_I = zdd_one; - return(one); - } - - if (U == zero || L == one) { - printf("*** ERROR : illegal condition for ISOP (U < L).\n"); - exit(1); - } - - /* Check the cache. We store two results for each recursive call. - ** One is the BDD, and the other is the ZDD. Both are needed. - ** Hence we need a double hit in the cache to terminate the - ** recursion. Clearly, collisions may evict only one of the two - ** results. */ - cacheOp = (DdNode *(*)(DdManager *, DdNode *, DdNode *)) cuddZddIsop; - r = cuddCacheLookup2(dd, cuddBddIsop, L, U); - if (r) { - *zdd_I = cuddCacheLookup2Zdd(dd, cacheOp, L, U); - if (*zdd_I) - return(r); - else { - /* The BDD result may have been dead. In that case - ** cuddCacheLookup2 would have called cuddReclaim, - ** whose effects we now have to undo. */ - cuddRef(r); - Cudd_RecursiveDeref(dd, r); - } - } - - top_l = dd->perm[Cudd_Regular(L)->index]; - top_u = dd->perm[Cudd_Regular(U)->index]; - v = ddMin(top_l, top_u); - - /* Compute cofactors. */ - if (top_l == v) { - index = Cudd_Regular(L)->index; - Lv = Cudd_T(L); - Lnv = Cudd_E(L); - if (Cudd_IsComplement(L)) { - Lv = Cudd_Not(Lv); - Lnv = Cudd_Not(Lnv); - } - } - else { - index = Cudd_Regular(U)->index; - Lv = Lnv = L; - } - - if (top_u == v) { - Uv = Cudd_T(U); - Unv = Cudd_E(U); - if (Cudd_IsComplement(U)) { - Uv = Cudd_Not(Uv); - Unv = Cudd_Not(Unv); - } - } - else { - Uv = Unv = U; - } - - Lsub0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Uv)); - if (Lsub0 == NULL) - return(NULL); - Cudd_Ref(Lsub0); - Usub0 = Unv; - Lsub1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Unv)); - if (Lsub1 == NULL) { - Cudd_RecursiveDeref(dd, Lsub0); - return(NULL); - } - Cudd_Ref(Lsub1); - Usub1 = Uv; - - Isub0 = cuddZddIsop(dd, Lsub0, Usub0, &zdd_Isub0); - if (Isub0 == NULL) { - Cudd_RecursiveDeref(dd, Lsub0); - Cudd_RecursiveDeref(dd, Lsub1); - return(NULL); - } - /* - if ((!cuddIsConstant(Cudd_Regular(Isub0))) && - (Cudd_Regular(Isub0)->index != zdd_Isub0->index / 2 || - dd->permZ[index * 2] > dd->permZ[zdd_Isub0->index])) { - printf("*** ERROR : illegal permutation in ZDD. ***\n"); - } - */ - Cudd_Ref(Isub0); - Cudd_Ref(zdd_Isub0); - Isub1 = cuddZddIsop(dd, Lsub1, Usub1, &zdd_Isub1); - if (Isub1 == NULL) { - Cudd_RecursiveDeref(dd, Lsub0); - Cudd_RecursiveDeref(dd, Lsub1); - Cudd_RecursiveDeref(dd, Isub0); - Cudd_RecursiveDerefZdd(dd, zdd_Isub0); - return(NULL); - } - /* - if ((!cuddIsConstant(Cudd_Regular(Isub1))) && - (Cudd_Regular(Isub1)->index != zdd_Isub1->index / 2 || - dd->permZ[index * 2] > dd->permZ[zdd_Isub1->index])) { - printf("*** ERROR : illegal permutation in ZDD. ***\n"); - } - */ - Cudd_Ref(Isub1); - Cudd_Ref(zdd_Isub1); - Cudd_RecursiveDeref(dd, Lsub0); - Cudd_RecursiveDeref(dd, Lsub1); - - Lsuper0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Isub0)); - if (Lsuper0 == NULL) { - Cudd_RecursiveDeref(dd, Isub0); - Cudd_RecursiveDerefZdd(dd, zdd_Isub0); - Cudd_RecursiveDeref(dd, Isub1); - Cudd_RecursiveDerefZdd(dd, zdd_Isub1); - return(NULL); - } - Cudd_Ref(Lsuper0); - Lsuper1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Isub1)); - if (Lsuper1 == NULL) { - Cudd_RecursiveDeref(dd, Isub0); - Cudd_RecursiveDerefZdd(dd, zdd_Isub0); - Cudd_RecursiveDeref(dd, Isub1); - Cudd_RecursiveDerefZdd(dd, zdd_Isub1); - Cudd_RecursiveDeref(dd, Lsuper0); - return(NULL); - } - Cudd_Ref(Lsuper1); - Usuper0 = Unv; - Usuper1 = Uv; - - /* Ld = Lsuper0 + Lsuper1 */ - Ld = cuddBddAndRecur(dd, Cudd_Not(Lsuper0), Cudd_Not(Lsuper1)); - if (Ld == NULL) { - Cudd_RecursiveDeref(dd, Isub0); - Cudd_RecursiveDerefZdd(dd, zdd_Isub0); - Cudd_RecursiveDeref(dd, Isub1); - Cudd_RecursiveDerefZdd(dd, zdd_Isub1); - Cudd_RecursiveDeref(dd, Lsuper0); - Cudd_RecursiveDeref(dd, Lsuper1); - return(NULL); - } - Ld = Cudd_Not(Ld); - Cudd_Ref(Ld); - /* Ud = Usuper0 * Usuper1 */ - Ud = cuddBddAndRecur(dd, Usuper0, Usuper1); - if (Ud == NULL) { - Cudd_RecursiveDeref(dd, Isub0); - Cudd_RecursiveDerefZdd(dd, zdd_Isub0); - Cudd_RecursiveDeref(dd, Isub1); - Cudd_RecursiveDerefZdd(dd, zdd_Isub1); - Cudd_RecursiveDeref(dd, Lsuper0); - Cudd_RecursiveDeref(dd, Lsuper1); - Cudd_RecursiveDeref(dd, Ld); - return(NULL); - } - Cudd_Ref(Ud); - Cudd_RecursiveDeref(dd, Lsuper0); - Cudd_RecursiveDeref(dd, Lsuper1); - - Id = cuddZddIsop(dd, Ld, Ud, &zdd_Id); - if (Id == NULL) { - Cudd_RecursiveDeref(dd, Isub0); - Cudd_RecursiveDerefZdd(dd, zdd_Isub0); - Cudd_RecursiveDeref(dd, Isub1); - Cudd_RecursiveDerefZdd(dd, zdd_Isub1); - Cudd_RecursiveDeref(dd, Ld); - Cudd_RecursiveDeref(dd, Ud); - return(NULL); - } - /* - if ((!cuddIsConstant(Cudd_Regular(Id))) && - (Cudd_Regular(Id)->index != zdd_Id->index / 2 || - dd->permZ[index * 2] > dd->permZ[zdd_Id->index])) { - printf("*** ERROR : illegal permutation in ZDD. ***\n"); - } - */ - Cudd_Ref(Id); - Cudd_Ref(zdd_Id); - Cudd_RecursiveDeref(dd, Ld); - Cudd_RecursiveDeref(dd, Ud); - - x = cuddUniqueInter(dd, index, one, zero); - if (x == NULL) { - Cudd_RecursiveDeref(dd, Isub0); - Cudd_RecursiveDerefZdd(dd, zdd_Isub0); - Cudd_RecursiveDeref(dd, Isub1); - Cudd_RecursiveDerefZdd(dd, zdd_Isub1); - Cudd_RecursiveDeref(dd, Id); - Cudd_RecursiveDerefZdd(dd, zdd_Id); - return(NULL); - } - Cudd_Ref(x); - /* term0 = x * Isub0 */ - term0 = cuddBddAndRecur(dd, Cudd_Not(x), Isub0); - if (term0 == NULL) { - Cudd_RecursiveDeref(dd, Isub0); - Cudd_RecursiveDerefZdd(dd, zdd_Isub0); - Cudd_RecursiveDeref(dd, Isub1); - Cudd_RecursiveDerefZdd(dd, zdd_Isub1); - Cudd_RecursiveDeref(dd, Id); - Cudd_RecursiveDerefZdd(dd, zdd_Id); - Cudd_RecursiveDeref(dd, x); - return(NULL); - } - Cudd_Ref(term0); - Cudd_RecursiveDeref(dd, Isub0); - /* term1 = x * Isub1 */ - term1 = cuddBddAndRecur(dd, x, Isub1); - if (term1 == NULL) { - Cudd_RecursiveDerefZdd(dd, zdd_Isub0); - Cudd_RecursiveDeref(dd, Isub1); - Cudd_RecursiveDerefZdd(dd, zdd_Isub1); - Cudd_RecursiveDeref(dd, Id); - Cudd_RecursiveDerefZdd(dd, zdd_Id); - Cudd_RecursiveDeref(dd, x); - Cudd_RecursiveDeref(dd, term0); - return(NULL); - } - Cudd_Ref(term1); - Cudd_RecursiveDeref(dd, x); - Cudd_RecursiveDeref(dd, Isub1); - /* sum = term0 + term1 */ - sum = cuddBddAndRecur(dd, Cudd_Not(term0), Cudd_Not(term1)); - if (sum == NULL) { - Cudd_RecursiveDerefZdd(dd, zdd_Isub0); - Cudd_RecursiveDerefZdd(dd, zdd_Isub1); - Cudd_RecursiveDeref(dd, Id); - Cudd_RecursiveDerefZdd(dd, zdd_Id); - Cudd_RecursiveDeref(dd, term0); - Cudd_RecursiveDeref(dd, term1); - return(NULL); - } - sum = Cudd_Not(sum); - Cudd_Ref(sum); - Cudd_RecursiveDeref(dd, term0); - Cudd_RecursiveDeref(dd, term1); - /* r = sum + Id */ - r = cuddBddAndRecur(dd, Cudd_Not(sum), Cudd_Not(Id)); - r = Cudd_NotCond(r, r != NULL); - if (r == NULL) { - Cudd_RecursiveDerefZdd(dd, zdd_Isub0); - Cudd_RecursiveDerefZdd(dd, zdd_Isub1); - Cudd_RecursiveDeref(dd, Id); - Cudd_RecursiveDerefZdd(dd, zdd_Id); - Cudd_RecursiveDeref(dd, sum); - return(NULL); - } - Cudd_Ref(r); - Cudd_RecursiveDeref(dd, sum); - Cudd_RecursiveDeref(dd, Id); - - if (zdd_Isub0 != zdd_zero) { - z = cuddZddGetNodeIVO(dd, index * 2 + 1, zdd_Isub0, zdd_Id); - if (z == NULL) { - Cudd_RecursiveDerefZdd(dd, zdd_Isub0); - Cudd_RecursiveDerefZdd(dd, zdd_Isub1); - Cudd_RecursiveDerefZdd(dd, zdd_Id); - Cudd_RecursiveDeref(dd, r); - return(NULL); - } - } - else { - z = zdd_Id; - } - Cudd_Ref(z); - if (zdd_Isub1 != zdd_zero) { - y = cuddZddGetNodeIVO(dd, index * 2, zdd_Isub1, z); - if (y == NULL) { - Cudd_RecursiveDerefZdd(dd, zdd_Isub0); - Cudd_RecursiveDerefZdd(dd, zdd_Isub1); - Cudd_RecursiveDerefZdd(dd, zdd_Id); - Cudd_RecursiveDeref(dd, r); - Cudd_RecursiveDerefZdd(dd, z); - return(NULL); - } - } - else - y = z; - Cudd_Ref(y); - - Cudd_RecursiveDerefZdd(dd, zdd_Isub0); - Cudd_RecursiveDerefZdd(dd, zdd_Isub1); - Cudd_RecursiveDerefZdd(dd, zdd_Id); - Cudd_RecursiveDerefZdd(dd, z); - - cuddCacheInsert2(dd, cuddBddIsop, L, U, r); - cuddCacheInsert2(dd, cacheOp, L, U, y); - - Cudd_Deref(r); - Cudd_Deref(y); - *zdd_I = y; - /* - if (Cudd_Regular(r)->index != y->index / 2) { - printf("*** ERROR : mismatch in indices between BDD and ZDD. ***\n"); - } - */ - return(r); - -} /* end of cuddZddIsop */ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Cudd_bddIsop.] - - Description [] - - SideEffects [None] - - SeeAlso [Cudd_bddIsop] - -******************************************************************************/ -DdNode * -cuddBddIsop( - DdManager * dd, - DdNode * L, - DdNode * U) -{ - DdNode *one = DD_ONE(dd); - DdNode *zero = Cudd_Not(one); - int v, top_l, top_u; - DdNode *Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud; - DdNode *Lsuper0, *Usuper0, *Lsuper1, *Usuper1; - DdNode *Isub0, *Isub1, *Id; - DdNode *x; - DdNode *term0, *term1, *sum; - DdNode *Lv, *Uv, *Lnv, *Unv; - DdNode *r; - int index; - - statLine(dd); - if (L == zero) - return(zero); - if (U == one) - return(one); - - /* Check cache */ - r = cuddCacheLookup2(dd, cuddBddIsop, L, U); - if (r) - return(r); - - top_l = dd->perm[Cudd_Regular(L)->index]; - top_u = dd->perm[Cudd_Regular(U)->index]; - v = ddMin(top_l, top_u); - - /* Compute cofactors */ - if (top_l == v) { - index = Cudd_Regular(L)->index; - Lv = Cudd_T(L); - Lnv = Cudd_E(L); - if (Cudd_IsComplement(L)) { - Lv = Cudd_Not(Lv); - Lnv = Cudd_Not(Lnv); - } - } - else { - index = Cudd_Regular(U)->index; - Lv = Lnv = L; - } - - if (top_u == v) { - Uv = Cudd_T(U); - Unv = Cudd_E(U); - if (Cudd_IsComplement(U)) { - Uv = Cudd_Not(Uv); - Unv = Cudd_Not(Unv); - } - } - else { - Uv = Unv = U; - } - - Lsub0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Uv)); - if (Lsub0 == NULL) - return(NULL); - Cudd_Ref(Lsub0); - Usub0 = Unv; - Lsub1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Unv)); - if (Lsub1 == NULL) { - Cudd_RecursiveDeref(dd, Lsub0); - return(NULL); - } - Cudd_Ref(Lsub1); - Usub1 = Uv; - - Isub0 = cuddBddIsop(dd, Lsub0, Usub0); - if (Isub0 == NULL) { - Cudd_RecursiveDeref(dd, Lsub0); - Cudd_RecursiveDeref(dd, Lsub1); - return(NULL); - } - Cudd_Ref(Isub0); - Isub1 = cuddBddIsop(dd, Lsub1, Usub1); - if (Isub1 == NULL) { - Cudd_RecursiveDeref(dd, Lsub0); - Cudd_RecursiveDeref(dd, Lsub1); - Cudd_RecursiveDeref(dd, Isub0); - return(NULL); - } - Cudd_Ref(Isub1); - Cudd_RecursiveDeref(dd, Lsub0); - Cudd_RecursiveDeref(dd, Lsub1); - - Lsuper0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Isub0)); - if (Lsuper0 == NULL) { - Cudd_RecursiveDeref(dd, Isub0); - Cudd_RecursiveDeref(dd, Isub1); - return(NULL); - } - Cudd_Ref(Lsuper0); - Lsuper1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Isub1)); - if (Lsuper1 == NULL) { - Cudd_RecursiveDeref(dd, Isub0); - Cudd_RecursiveDeref(dd, Isub1); - Cudd_RecursiveDeref(dd, Lsuper0); - return(NULL); - } - Cudd_Ref(Lsuper1); - Usuper0 = Unv; - Usuper1 = Uv; - - /* Ld = Lsuper0 + Lsuper1 */ - Ld = cuddBddAndRecur(dd, Cudd_Not(Lsuper0), Cudd_Not(Lsuper1)); - Ld = Cudd_NotCond(Ld, Ld != NULL); - if (Ld == NULL) { - Cudd_RecursiveDeref(dd, Isub0); - Cudd_RecursiveDeref(dd, Isub1); - Cudd_RecursiveDeref(dd, Lsuper0); - Cudd_RecursiveDeref(dd, Lsuper1); - return(NULL); - } - Cudd_Ref(Ld); - Ud = cuddBddAndRecur(dd, Usuper0, Usuper1); - if (Ud == NULL) { - Cudd_RecursiveDeref(dd, Isub0); - Cudd_RecursiveDeref(dd, Isub1); - Cudd_RecursiveDeref(dd, Lsuper0); - Cudd_RecursiveDeref(dd, Lsuper1); - Cudd_RecursiveDeref(dd, Ld); - return(NULL); - } - Cudd_Ref(Ud); - Cudd_RecursiveDeref(dd, Lsuper0); - Cudd_RecursiveDeref(dd, Lsuper1); - - Id = cuddBddIsop(dd, Ld, Ud); - if (Id == NULL) { - Cudd_RecursiveDeref(dd, Isub0); - Cudd_RecursiveDeref(dd, Isub1); - Cudd_RecursiveDeref(dd, Ld); - Cudd_RecursiveDeref(dd, Ud); - return(NULL); - } - Cudd_Ref(Id); - Cudd_RecursiveDeref(dd, Ld); - Cudd_RecursiveDeref(dd, Ud); - - x = cuddUniqueInter(dd, index, one, zero); - if (x == NULL) { - Cudd_RecursiveDeref(dd, Isub0); - Cudd_RecursiveDeref(dd, Isub1); - Cudd_RecursiveDeref(dd, Id); - return(NULL); - } - Cudd_Ref(x); - term0 = cuddBddAndRecur(dd, Cudd_Not(x), Isub0); - if (term0 == NULL) { - Cudd_RecursiveDeref(dd, Isub0); - Cudd_RecursiveDeref(dd, Isub1); - Cudd_RecursiveDeref(dd, Id); - Cudd_RecursiveDeref(dd, x); - return(NULL); - } - Cudd_Ref(term0); - Cudd_RecursiveDeref(dd, Isub0); - term1 = cuddBddAndRecur(dd, x, Isub1); - if (term1 == NULL) { - Cudd_RecursiveDeref(dd, Isub1); - Cudd_RecursiveDeref(dd, Id); - Cudd_RecursiveDeref(dd, x); - Cudd_RecursiveDeref(dd, term0); - return(NULL); - } - Cudd_Ref(term1); - Cudd_RecursiveDeref(dd, x); - Cudd_RecursiveDeref(dd, Isub1); - /* sum = term0 + term1 */ - sum = cuddBddAndRecur(dd, Cudd_Not(term0), Cudd_Not(term1)); - sum = Cudd_NotCond(sum, sum != NULL); - if (sum == NULL) { - Cudd_RecursiveDeref(dd, Id); - Cudd_RecursiveDeref(dd, term0); - Cudd_RecursiveDeref(dd, term1); - return(NULL); - } - Cudd_Ref(sum); - Cudd_RecursiveDeref(dd, term0); - Cudd_RecursiveDeref(dd, term1); - /* r = sum + Id */ - r = cuddBddAndRecur(dd, Cudd_Not(sum), Cudd_Not(Id)); - r = Cudd_NotCond(r, r != NULL); - if (r == NULL) { - Cudd_RecursiveDeref(dd, Id); - Cudd_RecursiveDeref(dd, sum); - return(NULL); - } - Cudd_Ref(r); - Cudd_RecursiveDeref(dd, sum); - Cudd_RecursiveDeref(dd, Id); - - cuddCacheInsert2(dd, cuddBddIsop, L, U, r); - - Cudd_Deref(r); - return(r); - -} /* 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] - -******************************************************************************/ -DdNode * -cuddMakeBddFromZddCover( - DdManager * dd, - DdNode * node) -{ - DdNode *neW; - int v; - DdNode *f1, *f0, *fd; - DdNode *b1, *b0, *bd; - DdNode *T, *E; - - statLine(dd); - if (node == dd->one) - return(dd->one); - if (node == dd->zero) - return(Cudd_Not(dd->one)); - - /* Check cache */ - neW = cuddCacheLookup1(dd, cuddMakeBddFromZddCover, node); - if (neW) - return(neW); - - v = Cudd_Regular(node)->index; /* either yi or zi */ - cuddZddGetCofactors3(dd, node, v, &f1, &f0, &fd); - Cudd_Ref(f1); - Cudd_Ref(f0); - Cudd_Ref(fd); - - b1 = cuddMakeBddFromZddCover(dd, f1); - if (!b1) { - Cudd_RecursiveDerefZdd(dd, f1); - Cudd_RecursiveDerefZdd(dd, f0); - Cudd_RecursiveDerefZdd(dd, fd); - return(NULL); - } - Cudd_Ref(b1); - b0 = cuddMakeBddFromZddCover(dd, f0); - if (!b1) { - Cudd_RecursiveDerefZdd(dd, f1); - Cudd_RecursiveDerefZdd(dd, f0); - Cudd_RecursiveDerefZdd(dd, fd); - Cudd_RecursiveDeref(dd, b1); - return(NULL); - } - Cudd_Ref(b0); - Cudd_RecursiveDerefZdd(dd, f1); - Cudd_RecursiveDerefZdd(dd, f0); - if (fd != dd->zero) { - bd = cuddMakeBddFromZddCover(dd, fd); - if (!bd) { - Cudd_RecursiveDerefZdd(dd, fd); - Cudd_RecursiveDeref(dd, b1); - Cudd_RecursiveDeref(dd, b0); - return(NULL); - } - Cudd_Ref(bd); - Cudd_RecursiveDerefZdd(dd, fd); - - T = cuddBddAndRecur(dd, Cudd_Not(b1), Cudd_Not(bd)); - if (!T) { - Cudd_RecursiveDeref(dd, b1); - Cudd_RecursiveDeref(dd, b0); - Cudd_RecursiveDeref(dd, bd); - return(NULL); - } - T = Cudd_NotCond(T, T != NULL); - Cudd_Ref(T); - Cudd_RecursiveDeref(dd, b1); - E = cuddBddAndRecur(dd, Cudd_Not(b0), Cudd_Not(bd)); - if (!E) { - Cudd_RecursiveDeref(dd, b0); - Cudd_RecursiveDeref(dd, bd); - Cudd_RecursiveDeref(dd, T); - return(NULL); - } - E = Cudd_NotCond(E, E != NULL); - Cudd_Ref(E); - Cudd_RecursiveDeref(dd, b0); - Cudd_RecursiveDeref(dd, bd); - } - else { - Cudd_RecursiveDerefZdd(dd, fd); - T = b1; - E = b0; - } - - if (Cudd_IsComplement(T)) { - neW = cuddUniqueInterIVO(dd, v / 2, Cudd_Not(T), Cudd_Not(E)); - if (!neW) { - Cudd_RecursiveDeref(dd, T); - Cudd_RecursiveDeref(dd, E); - return(NULL); - } - neW = Cudd_Not(neW); - } - else { - neW = cuddUniqueInterIVO(dd, v / 2, T, E); - if (!neW) { - Cudd_RecursiveDeref(dd, T); - Cudd_RecursiveDeref(dd, E); - return(NULL); - } - } - Cudd_Ref(neW); - Cudd_RecursiveDeref(dd, T); - Cudd_RecursiveDeref(dd, E); - - cuddCacheInsert1(dd, cuddMakeBddFromZddCover, node, neW); - Cudd_Deref(neW); - return(neW); - -} /* end of cuddMakeBddFromZddCover */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of static functions */ -/*---------------------------------------------------------------------------*/ - |