diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-13 13:42:25 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-13 13:42:25 -0800 |
commit | e7b544f11151f09a4a3fbe39b4a176795a82f677 (patch) | |
tree | a6cbbeb138c9bfe5b2554a5838124ffc3a6c0a5b /src/bdd/cudd/cuddZddSetop.c | |
parent | d99de60e6c88e5f6157b1d5c9b25cfd5d08a1c9a (diff) | |
download | abc-e7b544f11151f09a4a3fbe39b4a176795a82f677.tar.gz abc-e7b544f11151f09a4a3fbe39b4a176795a82f677.tar.bz2 abc-e7b544f11151f09a4a3fbe39b4a176795a82f677.zip |
Upgrade to the latest CUDD 2.4.2.
Diffstat (limited to 'src/bdd/cudd/cuddZddSetop.c')
-rw-r--r-- | src/bdd/cudd/cuddZddSetop.c | 726 |
1 files changed, 379 insertions, 347 deletions
diff --git a/src/bdd/cudd/cuddZddSetop.c b/src/bdd/cudd/cuddZddSetop.c index 566c610b..b4726b63 100644 --- a/src/bdd/cudd/cuddZddSetop.c +++ b/src/bdd/cudd/cuddZddSetop.c @@ -7,51 +7,79 @@ Synopsis [Set operations on ZDDs.] Description [External procedures included in this module: - <ul> - <li> Cudd_zddIte() - <li> Cudd_zddUnion() - <li> Cudd_zddIntersect() - <li> Cudd_zddDiff() - <li> Cudd_zddDiffConst() - <li> Cudd_zddSubset1() - <li> Cudd_zddSubset0() - <li> Cudd_zddChange() - </ul> - Internal procedures included in this module: - <ul> - <li> cuddZddIte() - <li> cuddZddUnion() - <li> cuddZddIntersect() - <li> cuddZddDiff() - <li> cuddZddChangeAux() - <li> cuddZddSubset1() - <li> cuddZddSubset0() - </ul> - Static procedures included in this module: - <ul> - <li> zdd_subset1_aux() - <li> zdd_subset0_aux() - <li> zddVarToConst() - </ul> - ] + <ul> + <li> Cudd_zddIte() + <li> Cudd_zddUnion() + <li> Cudd_zddIntersect() + <li> Cudd_zddDiff() + <li> Cudd_zddDiffConst() + <li> Cudd_zddSubset1() + <li> Cudd_zddSubset0() + <li> Cudd_zddChange() + </ul> + Internal procedures included in this module: + <ul> + <li> cuddZddIte() + <li> cuddZddUnion() + <li> cuddZddIntersect() + <li> cuddZddDiff() + <li> cuddZddChangeAux() + <li> cuddZddSubset1() + <li> cuddZddSubset0() + </ul> + Static procedures included in this module: + <ul> + <li> zdd_subset1_aux() + <li> zdd_subset0_aux() + <li> zddVarToConst() + </ul> + ] SeeAlso [] Author [Hyong-Kyoon Shin, 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.] + 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.] ******************************************************************************/ -#include "util_hack.h" -#include "cuddInt.h" +#include "util_hack.h" +#include "cuddInt.h" ABC_NAMESPACE_IMPL_START + /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ @@ -72,13 +100,16 @@ ABC_NAMESPACE_IMPL_START /*---------------------------------------------------------------------------*/ #ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddZddSetop.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang Exp $"; +static char rcsid[] DD_UNUSED = "$Id: cuddZddSetop.c,v 1.25 2004/08/13 18:04:54 fabio Exp $"; #endif /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ +#ifdef __cplusplus +extern "C" { +#endif /**AutomaticStart*************************************************************/ @@ -86,12 +117,15 @@ static char rcsid[] DD_UNUSED = "$Id: cuddZddSetop.c,v 1.1.1.1 2003/02/24 22:23: /* Static function prototypes */ /*---------------------------------------------------------------------------*/ -static DdNode * zdd_subset1_aux ARGS((DdManager *zdd, DdNode *P, DdNode *zvar)); -static DdNode * zdd_subset0_aux ARGS((DdManager *zdd, DdNode *P, DdNode *zvar)); -static void zddVarToConst ARGS((DdNode *f, DdNode **gp, DdNode **hp, DdNode *base, DdNode *empty)); +static DdNode * zdd_subset1_aux (DdManager *zdd, DdNode *P, DdNode *zvar); +static DdNode * zdd_subset0_aux (DdManager *zdd, DdNode *P, DdNode *zvar); +static void zddVarToConst (DdNode *f, DdNode **gp, DdNode **hp, DdNode *base, DdNode *empty); /**AutomaticEnd***************************************************************/ +#ifdef __cplusplus +} +#endif /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ @@ -120,8 +154,8 @@ Cudd_zddIte( DdNode *res; do { - dd->reordered = 0; - res = cuddZddIte(dd, f, g, h); + dd->reordered = 0; + res = cuddZddIte(dd, f, g, h); } while (dd->reordered == 1); return(res); @@ -149,8 +183,8 @@ Cudd_zddUnion( DdNode *res; do { - dd->reordered = 0; - res = cuddZddUnion(dd, P, Q); + dd->reordered = 0; + res = cuddZddUnion(dd, P, Q); } while (dd->reordered == 1); return(res); @@ -178,8 +212,8 @@ Cudd_zddIntersect( DdNode *res; do { - dd->reordered = 0; - res = cuddZddIntersect(dd, P, Q); + dd->reordered = 0; + res = cuddZddIntersect(dd, P, Q); } while (dd->reordered == 1); return(res); @@ -207,8 +241,8 @@ Cudd_zddDiff( DdNode *res; do { - dd->reordered = 0; - res = cuddZddDiff(dd, P, Q); + dd->reordered = 0; + res = cuddZddDiff(dd, P, Q); } while (dd->reordered == 1); return(res); @@ -234,41 +268,41 @@ Cudd_zddDiffConst( DdNode * P, DdNode * Q) { - int p_top, q_top; - DdNode *empty = DD_ZERO(zdd), *t, *res; - DdManager *table = zdd; + int p_top, q_top; + DdNode *empty = DD_ZERO(zdd), *t, *res; + DdManager *table = zdd; statLine(zdd); if (P == empty) - return(empty); + return(empty); if (Q == empty) - return(P); + return(P); if (P == Q) - return(empty); + return(empty); /* Check cache. The cache is shared by cuddZddDiff(). */ res = cuddCacheLookup2Zdd(table, cuddZddDiff, P, Q); if (res != NULL) - return(res); + return(res); if (cuddIsConstant(P)) - p_top = P->index; + p_top = P->index; else - p_top = zdd->permZ[P->index]; + p_top = zdd->permZ[P->index]; if (cuddIsConstant(Q)) - q_top = Q->index; + q_top = Q->index; else - q_top = zdd->permZ[Q->index]; + q_top = zdd->permZ[Q->index]; if (p_top < q_top) { - res = DD_NON_CONSTANT; + res = DD_NON_CONSTANT; } else if (p_top > q_top) { - res = Cudd_zddDiffConst(zdd, P, cuddE(Q)); + res = Cudd_zddDiffConst(zdd, P, cuddE(Q)); } else { - t = Cudd_zddDiffConst(zdd, cuddT(P), cuddT(Q)); - if (t != empty) - res = DD_NON_CONSTANT; - else - res = Cudd_zddDiffConst(zdd, cuddE(P), cuddE(Q)); + t = Cudd_zddDiffConst(zdd, cuddT(P), cuddT(Q)); + if (t != empty) + res = DD_NON_CONSTANT; + else + res = Cudd_zddDiffConst(zdd, cuddE(P), cuddE(Q)); } cuddCacheInsert2(table, cuddZddDiff, P, Q, res); @@ -298,11 +332,11 @@ Cudd_zddSubset1( DdNode * P, int var) { - DdNode *r; + DdNode *r; do { - dd->reordered = 0; - r = cuddZddSubset1(dd, P, var); + dd->reordered = 0; + r = cuddZddSubset1(dd, P, var); } while (dd->reordered == 1); return(r); @@ -330,11 +364,11 @@ Cudd_zddSubset0( DdNode * P, int var) { - DdNode *r; + DdNode *r; do { - dd->reordered = 0; - r = cuddZddSubset0(dd, P, var); + dd->reordered = 0; + r = cuddZddSubset0(dd, P, var); } while (dd->reordered == 1); return(r); @@ -360,13 +394,13 @@ Cudd_zddChange( DdNode * P, int var) { - DdNode *res; + DdNode *res; if ((unsigned int) var >= CUDD_MAXINDEX - 1) return(NULL); do { - dd->reordered = 0; - res = cuddZddChange(dd, P, var); + dd->reordered = 0; + res = cuddZddChange(dd, P, var); } while (dd->reordered == 1); return(res); @@ -404,8 +438,8 @@ cuddZddIte( statLine(dd); /* Trivial cases. */ /* One variable cases. */ - if (f == (empty = DD_ZERO(dd))) { /* ITE(0,G,H) = H */ - return(h); + if (f == (empty = DD_ZERO(dd))) { /* ITE(0,G,H) = H */ + return(h); } topf = cuddIZ(dd,f->index); topg = cuddIZ(dd,g->index); @@ -414,7 +448,7 @@ cuddZddIte( top = ddMin(topf,v); tautology = (top == CUDD_MAXINDEX) ? DD_ONE(dd) : dd->univ[top]; - if (f == tautology) { /* ITE(1,G,H) = G */ + if (f == tautology) { /* ITE(1,G,H) = G */ return(g); } @@ -422,18 +456,18 @@ cuddZddIte( zddVarToConst(f,&g,&h,tautology,empty); /* Check remaining one variable cases. */ - if (g == h) { /* ITE(F,G,G) = G */ - return(g); + if (g == h) { /* ITE(F,G,G) = G */ + return(g); } - if (g == tautology) { /* ITE(F,1,0) = F */ - if (h == empty) return(f); + if (g == tautology) { /* ITE(F,1,0) = F */ + if (h == empty) return(f); } /* Check cache. */ r = cuddCacheLookupZdd(dd,DD_ZDD_ITE_TAG,f,g,h); if (r != NULL) { - return(r); + return(r); } /* Recompute these because they may have changed in zddVarToConst. */ @@ -442,59 +476,59 @@ cuddZddIte( v = ddMin(topg,toph); if (topf < v) { - r = cuddZddIte(dd,cuddE(f),g,h); - if (r == NULL) return(NULL); + r = cuddZddIte(dd,cuddE(f),g,h); + if (r == NULL) return(NULL); } else if (topf > v) { - if (topg > v) { - Gvn = g; - index = h->index; - } else { - Gvn = cuddE(g); - index = g->index; - } - if (toph > v) { - Hv = empty; Hvn = h; - } else { - Hv = cuddT(h); Hvn = cuddE(h); - } - e = cuddZddIte(dd,f,Gvn,Hvn); - if (e == NULL) return(NULL); - cuddRef(e); - r = cuddZddGetNode(dd,index,Hv,e); - if (r == NULL) { - Cudd_RecursiveDerefZdd(dd,e); - return(NULL); - } - cuddDeref(e); - } else { - index = f->index; - if (topg > v) { - Gv = empty; Gvn = g; + if (topg > v) { + Gvn = g; + index = h->index; + } else { + Gvn = cuddE(g); + index = g->index; + } + if (toph > v) { + Hv = empty; Hvn = h; + } else { + Hv = cuddT(h); Hvn = cuddE(h); + } + e = cuddZddIte(dd,f,Gvn,Hvn); + if (e == NULL) return(NULL); + cuddRef(e); + r = cuddZddGetNode(dd,index,Hv,e); + if (r == NULL) { + Cudd_RecursiveDerefZdd(dd,e); + return(NULL); + } + cuddDeref(e); } else { - Gv = cuddT(g); Gvn = cuddE(g); - } - if (toph > v) { - Hv = empty; Hvn = h; - } else { - Hv = cuddT(h); Hvn = cuddE(h); - } - e = cuddZddIte(dd,cuddE(f),Gvn,Hvn); - if (e == NULL) return(NULL); - cuddRef(e); - t = cuddZddIte(dd,cuddT(f),Gv,Hv); - if (t == NULL) { - Cudd_RecursiveDerefZdd(dd,e); - return(NULL); - } - cuddRef(t); - r = cuddZddGetNode(dd,index,t,e); - if (r == NULL) { - Cudd_RecursiveDerefZdd(dd,e); - Cudd_RecursiveDerefZdd(dd,t); - return(NULL); - } - cuddDeref(t); - cuddDeref(e); + index = f->index; + if (topg > v) { + Gv = empty; Gvn = g; + } else { + Gv = cuddT(g); Gvn = cuddE(g); + } + if (toph > v) { + Hv = empty; Hvn = h; + } else { + Hv = cuddT(h); Hvn = cuddE(h); + } + e = cuddZddIte(dd,cuddE(f),Gvn,Hvn); + if (e == NULL) return(NULL); + cuddRef(e); + t = cuddZddIte(dd,cuddT(f),Gv,Hv); + if (t == NULL) { + Cudd_RecursiveDerefZdd(dd,e); + return(NULL); + } + cuddRef(t); + r = cuddZddGetNode(dd,index,t,e); + if (r == NULL) { + Cudd_RecursiveDerefZdd(dd,e); + Cudd_RecursiveDerefZdd(dd,t); + return(NULL); + } + cuddDeref(t); + cuddDeref(e); } cuddCacheInsert(dd,DD_ZDD_ITE_TAG,f,g,h,r); @@ -521,69 +555,69 @@ cuddZddUnion( DdNode * P, DdNode * Q) { - int p_top, q_top; - DdNode *empty = DD_ZERO(zdd), *t, *e, *res; - DdManager *table = zdd; + int p_top, q_top; + DdNode *empty = DD_ZERO(zdd), *t, *e, *res; + DdManager *table = zdd; statLine(zdd); if (P == empty) - return(Q); + return(Q); if (Q == empty) - return(P); + return(P); if (P == Q) - return(P); + return(P); /* Check cache */ res = cuddCacheLookup2Zdd(table, cuddZddUnion, P, Q); if (res != NULL) - return(res); + return(res); if (cuddIsConstant(P)) - p_top = P->index; + p_top = P->index; else - p_top = zdd->permZ[P->index]; + p_top = zdd->permZ[P->index]; if (cuddIsConstant(Q)) - q_top = Q->index; + q_top = Q->index; else - q_top = zdd->permZ[Q->index]; + q_top = zdd->permZ[Q->index]; if (p_top < q_top) { - e = cuddZddUnion(zdd, cuddE(P), Q); - if (e == NULL) return (NULL); - cuddRef(e); - res = cuddZddGetNode(zdd, P->index, cuddT(P), e); - if (res == NULL) { - Cudd_RecursiveDerefZdd(table, e); - return(NULL); - } - cuddDeref(e); + e = cuddZddUnion(zdd, cuddE(P), Q); + if (e == NULL) return (NULL); + cuddRef(e); + res = cuddZddGetNode(zdd, P->index, cuddT(P), e); + if (res == NULL) { + Cudd_RecursiveDerefZdd(table, e); + return(NULL); + } + cuddDeref(e); } else if (p_top > q_top) { - e = cuddZddUnion(zdd, P, cuddE(Q)); - if (e == NULL) return(NULL); - cuddRef(e); - res = cuddZddGetNode(zdd, Q->index, cuddT(Q), e); - if (res == NULL) { - Cudd_RecursiveDerefZdd(table, e); - return(NULL); - } - cuddDeref(e); + e = cuddZddUnion(zdd, P, cuddE(Q)); + if (e == NULL) return(NULL); + cuddRef(e); + res = cuddZddGetNode(zdd, Q->index, cuddT(Q), e); + if (res == NULL) { + Cudd_RecursiveDerefZdd(table, e); + return(NULL); + } + cuddDeref(e); } else { - t = cuddZddUnion(zdd, cuddT(P), cuddT(Q)); - if (t == NULL) return(NULL); - cuddRef(t); - e = cuddZddUnion(zdd, cuddE(P), cuddE(Q)); - if (e == NULL) { - Cudd_RecursiveDerefZdd(table, t); - return(NULL); - } - cuddRef(e); - res = cuddZddGetNode(zdd, P->index, t, e); - if (res == NULL) { - Cudd_RecursiveDerefZdd(table, t); - Cudd_RecursiveDerefZdd(table, e); - return(NULL); - } - cuddDeref(t); - cuddDeref(e); + t = cuddZddUnion(zdd, cuddT(P), cuddT(Q)); + if (t == NULL) return(NULL); + cuddRef(t); + e = cuddZddUnion(zdd, cuddE(P), cuddE(Q)); + if (e == NULL) { + Cudd_RecursiveDerefZdd(table, t); + return(NULL); + } + cuddRef(e); + res = cuddZddGetNode(zdd, P->index, t, e); + if (res == NULL) { + Cudd_RecursiveDerefZdd(table, t); + Cudd_RecursiveDerefZdd(table, e); + return(NULL); + } + cuddDeref(t); + cuddDeref(e); } cuddCacheInsert2(table, cuddZddUnion, P, Q, res); @@ -610,55 +644,55 @@ cuddZddIntersect( DdNode * P, DdNode * Q) { - int p_top, q_top; - DdNode *empty = DD_ZERO(zdd), *t, *e, *res; - DdManager *table = zdd; + int p_top, q_top; + DdNode *empty = DD_ZERO(zdd), *t, *e, *res; + DdManager *table = zdd; statLine(zdd); if (P == empty) - return(empty); + return(empty); if (Q == empty) - return(empty); + return(empty); if (P == Q) - return(P); + return(P); /* Check cache. */ res = cuddCacheLookup2Zdd(table, cuddZddIntersect, P, Q); if (res != NULL) - return(res); + return(res); if (cuddIsConstant(P)) - p_top = P->index; + p_top = P->index; else - p_top = zdd->permZ[P->index]; + p_top = zdd->permZ[P->index]; if (cuddIsConstant(Q)) - q_top = Q->index; + q_top = Q->index; else - q_top = zdd->permZ[Q->index]; + q_top = zdd->permZ[Q->index]; if (p_top < q_top) { - res = cuddZddIntersect(zdd, cuddE(P), Q); - if (res == NULL) return(NULL); + res = cuddZddIntersect(zdd, cuddE(P), Q); + if (res == NULL) return(NULL); } else if (p_top > q_top) { - res = cuddZddIntersect(zdd, P, cuddE(Q)); - if (res == NULL) return(NULL); + res = cuddZddIntersect(zdd, P, cuddE(Q)); + if (res == NULL) return(NULL); } else { - t = cuddZddIntersect(zdd, cuddT(P), cuddT(Q)); - if (t == NULL) return(NULL); - cuddRef(t); - e = cuddZddIntersect(zdd, cuddE(P), cuddE(Q)); - if (e == NULL) { - Cudd_RecursiveDerefZdd(table, t); - return(NULL); - } - cuddRef(e); - res = cuddZddGetNode(zdd, P->index, t, e); - if (res == NULL) { - Cudd_RecursiveDerefZdd(table, t); - Cudd_RecursiveDerefZdd(table, e); - return(NULL); - } - cuddDeref(t); - cuddDeref(e); + t = cuddZddIntersect(zdd, cuddT(P), cuddT(Q)); + if (t == NULL) return(NULL); + cuddRef(t); + e = cuddZddIntersect(zdd, cuddE(P), cuddE(Q)); + if (e == NULL) { + Cudd_RecursiveDerefZdd(table, t); + return(NULL); + } + cuddRef(e); + res = cuddZddGetNode(zdd, P->index, t, e); + if (res == NULL) { + Cudd_RecursiveDerefZdd(table, t); + Cudd_RecursiveDerefZdd(table, e); + return(NULL); + } + cuddDeref(t); + cuddDeref(e); } cuddCacheInsert2(table, cuddZddIntersect, P, Q, res); @@ -685,62 +719,62 @@ cuddZddDiff( DdNode * P, DdNode * Q) { - int p_top, q_top; - DdNode *empty = DD_ZERO(zdd), *t, *e, *res; - DdManager *table = zdd; + int p_top, q_top; + DdNode *empty = DD_ZERO(zdd), *t, *e, *res; + DdManager *table = zdd; statLine(zdd); if (P == empty) - return(empty); + return(empty); if (Q == empty) - return(P); + return(P); if (P == Q) - return(empty); + return(empty); /* Check cache. The cache is shared by Cudd_zddDiffConst(). */ res = cuddCacheLookup2Zdd(table, cuddZddDiff, P, Q); if (res != NULL && res != DD_NON_CONSTANT) - return(res); + return(res); if (cuddIsConstant(P)) - p_top = P->index; + p_top = P->index; else - p_top = zdd->permZ[P->index]; + p_top = zdd->permZ[P->index]; if (cuddIsConstant(Q)) - q_top = Q->index; + q_top = Q->index; else - q_top = zdd->permZ[Q->index]; + q_top = zdd->permZ[Q->index]; if (p_top < q_top) { - e = cuddZddDiff(zdd, cuddE(P), Q); - if (e == NULL) return(NULL); - cuddRef(e); - res = cuddZddGetNode(zdd, P->index, cuddT(P), e); - if (res == NULL) { - Cudd_RecursiveDerefZdd(table, e); - return(NULL); - } - cuddDeref(e); + e = cuddZddDiff(zdd, cuddE(P), Q); + if (e == NULL) return(NULL); + cuddRef(e); + res = cuddZddGetNode(zdd, P->index, cuddT(P), e); + if (res == NULL) { + Cudd_RecursiveDerefZdd(table, e); + return(NULL); + } + cuddDeref(e); } else if (p_top > q_top) { - res = cuddZddDiff(zdd, P, cuddE(Q)); - if (res == NULL) return(NULL); + res = cuddZddDiff(zdd, P, cuddE(Q)); + if (res == NULL) return(NULL); } else { - t = cuddZddDiff(zdd, cuddT(P), cuddT(Q)); - if (t == NULL) return(NULL); - cuddRef(t); - e = cuddZddDiff(zdd, cuddE(P), cuddE(Q)); - if (e == NULL) { - Cudd_RecursiveDerefZdd(table, t); - return(NULL); - } - cuddRef(e); - res = cuddZddGetNode(zdd, P->index, t, e); - if (res == NULL) { - Cudd_RecursiveDerefZdd(table, t); - Cudd_RecursiveDerefZdd(table, e); - return(NULL); - } - cuddDeref(t); - cuddDeref(e); + t = cuddZddDiff(zdd, cuddT(P), cuddT(Q)); + if (t == NULL) return(NULL); + cuddRef(t); + e = cuddZddDiff(zdd, cuddE(P), cuddE(Q)); + if (e == NULL) { + Cudd_RecursiveDerefZdd(table, t); + return(NULL); + } + cuddRef(e); + res = cuddZddGetNode(zdd, P->index, t, e); + if (res == NULL) { + Cudd_RecursiveDerefZdd(table, t); + Cudd_RecursiveDerefZdd(table, e); + return(NULL); + } + cuddDeref(t); + cuddDeref(e); } cuddCacheInsert2(table, cuddZddDiff, P, Q, res); @@ -767,49 +801,49 @@ cuddZddChangeAux( DdNode * P, DdNode * zvar) { - int top_var, level; - DdNode *res, *t, *e; - DdNode *base = DD_ONE(zdd); - DdNode *empty = DD_ZERO(zdd); + int top_var, level; + DdNode *res, *t, *e; + DdNode *base = DD_ONE(zdd); + DdNode *empty = DD_ZERO(zdd); statLine(zdd); if (P == empty) - return(empty); + return(empty); if (P == base) - return(zvar); + return(zvar); /* Check cache. */ res = cuddCacheLookup2Zdd(zdd, cuddZddChangeAux, P, zvar); if (res != NULL) - return(res); + return(res); top_var = zdd->permZ[P->index]; level = zdd->permZ[zvar->index]; if (top_var > level) { - res = cuddZddGetNode(zdd, zvar->index, P, DD_ZERO(zdd)); - if (res == NULL) return(NULL); + res = cuddZddGetNode(zdd, zvar->index, P, DD_ZERO(zdd)); + if (res == NULL) return(NULL); } else if (top_var == level) { - res = cuddZddGetNode(zdd, zvar->index, cuddE(P), cuddT(P)); - if (res == NULL) return(NULL); + res = cuddZddGetNode(zdd, zvar->index, cuddE(P), cuddT(P)); + if (res == NULL) return(NULL); } else { - t = cuddZddChangeAux(zdd, cuddT(P), zvar); - if (t == NULL) return(NULL); - cuddRef(t); - e = cuddZddChangeAux(zdd, cuddE(P), zvar); - if (e == NULL) { - Cudd_RecursiveDerefZdd(zdd, t); - return(NULL); - } - cuddRef(e); - res = cuddZddGetNode(zdd, P->index, t, e); - if (res == NULL) { - Cudd_RecursiveDerefZdd(zdd, t); - Cudd_RecursiveDerefZdd(zdd, e); - return(NULL); - } - cuddDeref(t); - cuddDeref(e); + t = cuddZddChangeAux(zdd, cuddT(P), zvar); + if (t == NULL) return(NULL); + cuddRef(t); + e = cuddZddChangeAux(zdd, cuddE(P), zvar); + if (e == NULL) { + Cudd_RecursiveDerefZdd(zdd, t); + return(NULL); + } + cuddRef(e); + res = cuddZddGetNode(zdd, P->index, t, e); + if (res == NULL) { + Cudd_RecursiveDerefZdd(zdd, t); + Cudd_RecursiveDerefZdd(zdd, e); + return(NULL); + } + cuddDeref(t); + cuddDeref(e); } cuddCacheInsert2(zdd, cuddZddChangeAux, P, zvar, res); @@ -842,24 +876,24 @@ cuddZddSubset1( DdNode * P, int var) { - DdNode *zvar, *r; - DdNode *base, *empty; + DdNode *zvar, *r; + DdNode *base, *empty; base = DD_ONE(dd); empty = DD_ZERO(dd); zvar = cuddUniqueInterZdd(dd, var, base, empty); if (zvar == NULL) { - return(NULL); + return(NULL); } else { - cuddRef(zvar); - r = zdd_subset1_aux(dd, P, zvar); - if (r == NULL) { + cuddRef(zvar); + r = zdd_subset1_aux(dd, P, zvar); + if (r == NULL) { + Cudd_RecursiveDerefZdd(dd, zvar); + return(NULL); + } + cuddRef(r); Cudd_RecursiveDerefZdd(dd, zvar); - return(NULL); - } - cuddRef(r); - Cudd_RecursiveDerefZdd(dd, zvar); } cuddDeref(r); @@ -891,24 +925,24 @@ cuddZddSubset0( DdNode * P, int var) { - DdNode *zvar, *r; - DdNode *base, *empty; + DdNode *zvar, *r; + DdNode *base, *empty; base = DD_ONE(dd); empty = DD_ZERO(dd); zvar = cuddUniqueInterZdd(dd, var, base, empty); if (zvar == NULL) { - return(NULL); + return(NULL); } else { - cuddRef(zvar); - r = zdd_subset0_aux(dd, P, zvar); - if (r == NULL) { + cuddRef(zvar); + r = zdd_subset0_aux(dd, P, zvar); + if (r == NULL) { + Cudd_RecursiveDerefZdd(dd, zvar); + return(NULL); + } + cuddRef(r); Cudd_RecursiveDerefZdd(dd, zvar); - return(NULL); - } - cuddRef(r); - Cudd_RecursiveDerefZdd(dd, zvar); } cuddDeref(r); @@ -939,7 +973,7 @@ cuddZddChange( DdNode * P, int var) { - DdNode *zvar, *res; + DdNode *zvar, *res; zvar = cuddUniqueInterZdd(dd, var, DD_ONE(dd), DD_ZERO(dd)); if (zvar == NULL) return(NULL); @@ -947,8 +981,8 @@ cuddZddChange( res = cuddZddChangeAux(dd, P, zvar); if (res == NULL) { - Cudd_RecursiveDerefZdd(dd,zvar); - return(NULL); + Cudd_RecursiveDerefZdd(dd,zvar); + return(NULL); } cuddRef(res); Cudd_RecursiveDerefZdd(dd,zvar); @@ -980,23 +1014,22 @@ zdd_subset1_aux( DdNode * P, DdNode * zvar) { - int top_var, level; - DdNode *res, *t, *e; - DdNode *base, *empty; + int top_var, level; + DdNode *res, *t, *e; + DdNode *empty; statLine(zdd); - base = DD_ONE(zdd); empty = DD_ZERO(zdd); /* Check cache. */ res = cuddCacheLookup2Zdd(zdd, zdd_subset1_aux, P, zvar); if (res != NULL) - return(res); + return(res); if (cuddIsConstant(P)) { - res = empty; - cuddCacheInsert2(zdd, zdd_subset1_aux, P, zvar, res); - return(res); + res = empty; + cuddCacheInsert2(zdd, zdd_subset1_aux, P, zvar, res); + return(res); } top_var = zdd->permZ[P->index]; @@ -1005,25 +1038,25 @@ zdd_subset1_aux( if (top_var > level) { res = empty; } else if (top_var == level) { - res = cuddT(P); + res = cuddT(P); } else { t = zdd_subset1_aux(zdd, cuddT(P), zvar); - if (t == NULL) return(NULL); - cuddRef(t); + if (t == NULL) return(NULL); + cuddRef(t); e = zdd_subset1_aux(zdd, cuddE(P), zvar); - if (e == NULL) { - Cudd_RecursiveDerefZdd(zdd, t); - return(NULL); - } - cuddRef(e); + if (e == NULL) { + Cudd_RecursiveDerefZdd(zdd, t); + return(NULL); + } + cuddRef(e); res = cuddZddGetNode(zdd, P->index, t, e); - if (res == NULL) { - Cudd_RecursiveDerefZdd(zdd, t); - Cudd_RecursiveDerefZdd(zdd, e); - return(NULL); - } - cuddDeref(t); - cuddDeref(e); + if (res == NULL) { + Cudd_RecursiveDerefZdd(zdd, t); + Cudd_RecursiveDerefZdd(zdd, e); + return(NULL); + } + cuddDeref(t); + cuddDeref(e); } cuddCacheInsert2(zdd, zdd_subset1_aux, P, zvar, res); @@ -1050,23 +1083,20 @@ zdd_subset0_aux( DdNode * P, DdNode * zvar) { - int top_var, level; - DdNode *res, *t, *e; - DdNode *base, *empty; + int top_var, level; + DdNode *res, *t, *e; statLine(zdd); - base = DD_ONE(zdd); - empty = DD_ZERO(zdd); /* Check cache. */ res = cuddCacheLookup2Zdd(zdd, zdd_subset0_aux, P, zvar); if (res != NULL) - return(res); + return(res); if (cuddIsConstant(P)) { - res = P; - cuddCacheInsert2(zdd, zdd_subset0_aux, P, zvar, res); - return(res); + res = P; + cuddCacheInsert2(zdd, zdd_subset0_aux, P, zvar, res); + return(res); } top_var = zdd->permZ[P->index]; @@ -1080,22 +1110,22 @@ zdd_subset0_aux( } else { t = zdd_subset0_aux(zdd, cuddT(P), zvar); - if (t == NULL) return(NULL); - cuddRef(t); + if (t == NULL) return(NULL); + cuddRef(t); e = zdd_subset0_aux(zdd, cuddE(P), zvar); - if (e == NULL) { - Cudd_RecursiveDerefZdd(zdd, t); - return(NULL); - } - cuddRef(e); + if (e == NULL) { + Cudd_RecursiveDerefZdd(zdd, t); + return(NULL); + } + cuddRef(e); res = cuddZddGetNode(zdd, P->index, t, e); - if (res == NULL) { - Cudd_RecursiveDerefZdd(zdd, t); - Cudd_RecursiveDerefZdd(zdd, e); - return(NULL); - } - cuddDeref(t); - cuddDeref(e); + if (res == NULL) { + Cudd_RecursiveDerefZdd(zdd, t); + Cudd_RecursiveDerefZdd(zdd, e); + return(NULL); + } + cuddDeref(t); + cuddDeref(e); } cuddCacheInsert2(zdd, zdd_subset0_aux, P, zvar, res); @@ -1129,14 +1159,16 @@ zddVarToConst( DdNode *h = *hp; if (f == g) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */ - *gp = base; + *gp = base; } if (f == h) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */ - *hp = empty; + *hp = empty; } } /* end of zddVarToConst */ + ABC_NAMESPACE_IMPL_END + |