diff options
Diffstat (limited to 'src/bdd/cudd/cuddGenCof.c')
| -rw-r--r-- | src/bdd/cudd/cuddGenCof.c | 1366 |
1 files changed, 788 insertions, 578 deletions
diff --git a/src/bdd/cudd/cuddGenCof.c b/src/bdd/cudd/cuddGenCof.c index 93e15da0..35c380c0 100644 --- a/src/bdd/cudd/cuddGenCof.c +++ b/src/bdd/cudd/cuddGenCof.c @@ -7,42 +7,71 @@ Synopsis [Generalized cofactors for BDDs and ADDs.] Description [External procedures included in this module: - <ul> - <li> Cudd_bddConstrain() - <li> Cudd_bddRestrict() - <li> Cudd_addConstrain() - <li> Cudd_bddConstrainDecomp() - <li> Cudd_addRestrict() - <li> Cudd_bddCharToVect() - <li> Cudd_bddLICompaction() - <li> Cudd_bddSqueeze() - <li> Cudd_SubsetCompress() - <li> Cudd_SupersetCompress() - </ul> - Internal procedures included in this module: - <ul> - <li> cuddBddConstrainRecur() - <li> cuddBddRestrictRecur() - <li> cuddAddConstrainRecur() - <li> cuddAddRestrictRecur() - <li> cuddBddLICompaction() - </ul> - Static procedures included in this module: - <ul> - <li> cuddBddConstrainDecomp() - <li> cuddBddCharToVect() - <li> cuddBddLICMarkEdges() - <li> cuddBddLICBuildResult() - <li> cuddBddSqueeze() - </ul> - ] + <ul> + <li> Cudd_bddConstrain() + <li> Cudd_bddRestrict() + <li> Cudd_bddNPAnd() + <li> Cudd_addConstrain() + <li> Cudd_bddConstrainDecomp() + <li> Cudd_addRestrict() + <li> Cudd_bddCharToVect() + <li> Cudd_bddLICompaction() + <li> Cudd_bddSqueeze() + <li> Cudd_SubsetCompress() + <li> Cudd_SupersetCompress() + </ul> + Internal procedures included in this module: + <ul> + <li> cuddBddConstrainRecur() + <li> cuddBddRestrictRecur() + <li> cuddBddNPAndRecur() + <li> cuddAddConstrainRecur() + <li> cuddAddRestrictRecur() + <li> cuddBddLICompaction() + </ul> + Static procedures included in this module: + <ul> + <li> cuddBddConstrainDecomp() + <li> cuddBddCharToVect() + <li> cuddBddLICMarkEdges() + <li> cuddBddLICBuildResult() + <li> cuddBddSqueeze() + </ul> + ] Author [Fabio Somenzi] - 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.] ******************************************************************************/ @@ -53,6 +82,7 @@ ABC_NAMESPACE_IMPL_START + /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ @@ -85,13 +115,16 @@ typedef struct MarkCacheKey { /*---------------------------------------------------------------------------*/ #ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddGenCof.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $"; +static char rcsid[] DD_UNUSED = "$Id: cuddGenCof.c,v 1.38 2005/05/14 17:27:11 fabio Exp $"; #endif /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ +#ifdef __cplusplus +extern "C" { +#endif /**AutomaticStart*************************************************************/ @@ -99,17 +132,20 @@ static char rcsid[] DD_UNUSED = "$Id: cuddGenCof.c,v 1.1.1.1 2003/02/24 22:23:52 /* Static function prototypes */ /*---------------------------------------------------------------------------*/ -static int cuddBddConstrainDecomp ARGS((DdManager *dd, DdNode *f, DdNode **decomp)); -static DdNode * cuddBddCharToVect ARGS((DdManager *dd, DdNode *f, DdNode *x)); -static int cuddBddLICMarkEdges ARGS((DdManager *dd, DdNode *f, DdNode *c, st_table *table, st_table *cache)); -static DdNode * cuddBddLICBuildResult ARGS((DdManager *dd, DdNode *f, st_table *cache, st_table *table)); -static int MarkCacheHash ARGS((const char *ptr, int modulus)); -static int MarkCacheCompare ARGS((const char *ptr1, const char *ptr2)); -static enum st_retval MarkCacheCleanUp ARGS((char *key, char *value, char *arg)); -static DdNode * cuddBddSqueeze ARGS((DdManager *dd, DdNode *l, DdNode *u)); +static int cuddBddConstrainDecomp (DdManager *dd, DdNode *f, DdNode **decomp); +static DdNode * cuddBddCharToVect (DdManager *dd, DdNode *f, DdNode *x); +static int cuddBddLICMarkEdges (DdManager *dd, DdNode *f, DdNode *c, st_table *table, st_table *cache); +static DdNode * cuddBddLICBuildResult (DdManager *dd, DdNode *f, st_table *cache, st_table *table); +static int MarkCacheHash (const char *ptr, int modulus); +static int MarkCacheCompare (const char *ptr1, const char *ptr2); +static enum st_retval MarkCacheCleanUp (char *key, char *value, char *arg); +static DdNode * cuddBddSqueeze (DdManager *dd, DdNode *l, DdNode *u); /**AutomaticEnd***************************************************************/ +#ifdef __cplusplus +} +#endif /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ @@ -149,8 +185,8 @@ Cudd_bddConstrain( DdNode *res; do { - dd->reordered = 0; - res = cuddBddConstrainRecur(dd,f,c); + dd->reordered = 0; + res = cuddBddConstrainRecur(dd,f,c); } while (dd->reordered == 1); return(res); @@ -194,34 +230,34 @@ Cudd_bddRestrict( /* Check if supports intersect. */ retval = Cudd_ClassifySupport(dd,f,c,&commonSupport,&suppF,&suppC); if (retval == 0) { - return(NULL); + return(NULL); } cuddRef(commonSupport); cuddRef(suppF); cuddRef(suppC); Cudd_IterDerefBdd(dd,suppF); if (commonSupport == DD_ONE(dd)) { - Cudd_IterDerefBdd(dd,commonSupport); - Cudd_IterDerefBdd(dd,suppC); - return(f); + Cudd_IterDerefBdd(dd,commonSupport); + Cudd_IterDerefBdd(dd,suppC); + return(f); } Cudd_IterDerefBdd(dd,commonSupport); /* Abstract from c the variables that do not appear in f. */ cplus = Cudd_bddExistAbstract(dd, c, suppC); if (cplus == NULL) { - Cudd_IterDerefBdd(dd,suppC); - return(NULL); + Cudd_IterDerefBdd(dd,suppC); + return(NULL); } cuddRef(cplus); Cudd_IterDerefBdd(dd,suppC); do { - dd->reordered = 0; - res = cuddBddRestrictRecur(dd, f, cplus); + dd->reordered = 0; + res = cuddBddRestrictRecur(dd, f, cplus); } while (dd->reordered == 1); if (res == NULL) { - Cudd_IterDerefBdd(dd,cplus); - return(NULL); + Cudd_IterDerefBdd(dd,cplus); + return(NULL); } cuddRef(res); Cudd_IterDerefBdd(dd,cplus); @@ -230,11 +266,11 @@ Cudd_bddRestrict( sizeF = Cudd_DagSize(f); sizeRes = Cudd_DagSize(res); if (sizeF <= sizeRes) { - Cudd_IterDerefBdd(dd, res); - return(f); + Cudd_IterDerefBdd(dd, res); + return(f); } else { - cuddDeref(res); - return(res); + cuddDeref(res); + return(res); } } /* end of Cudd_bddRestrict */ @@ -242,6 +278,42 @@ Cudd_bddRestrict( /**Function******************************************************************** + Synopsis [Computes f non-polluting-and g.] + + Description [Computes f non-polluting-and g. The non-polluting AND + of f and g is a hybrid of AND and Restrict. From Restrict, this + operation takes the idea of existentially quantifying the top + variable of the second operand if it does not appear in the first. + Therefore, the variables that appear in the result also appear in f. + For the rest, the function behaves like AND. Since the two operands + play different roles, non-polluting AND is not commutative. + + Returns a pointer to the result if successful; NULL otherwise.] + + SideEffects [None] + + SeeAlso [Cudd_bddConstrain Cudd_bddRestrict] + +******************************************************************************/ +DdNode * +Cudd_bddNPAnd( + DdManager * dd, + DdNode * f, + DdNode * g) +{ + DdNode *res; + + do { + dd->reordered = 0; + res = cuddBddNPAndRecur(dd,f,g); + } while (dd->reordered == 1); + return(res); + +} /* end of Cudd_bddNPAnd */ + + +/**Function******************************************************************** + Synopsis [Computes f constrain c for ADDs.] Description [Computes f constrain c (f @ c), for f an ADD and c a 0-1 @@ -269,8 +341,8 @@ Cudd_addConstrain( DdNode *res; do { - dd->reordered = 0; - res = cuddAddConstrainRecur(dd,f,c); + dd->reordered = 0; + res = cuddAddConstrainRecur(dd,f,c); } while (dd->reordered == 1); return(res); @@ -307,33 +379,33 @@ Cudd_bddConstrainDecomp( /* Create an initialize decomposition array. */ decomp = ABC_ALLOC(DdNode *,dd->size); if (decomp == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(NULL); + dd->errorCode = CUDD_MEMORY_OUT; + return(NULL); } for (i = 0; i < dd->size; i++) { - decomp[i] = NULL; + decomp[i] = NULL; } do { - dd->reordered = 0; - /* Clean up the decomposition array in case reordering took place. */ - for (i = 0; i < dd->size; i++) { - if (decomp[i] != NULL) { - Cudd_IterDerefBdd(dd, decomp[i]); - decomp[i] = NULL; + dd->reordered = 0; + /* Clean up the decomposition array in case reordering took place. */ + for (i = 0; i < dd->size; i++) { + if (decomp[i] != NULL) { + Cudd_IterDerefBdd(dd, decomp[i]); + decomp[i] = NULL; + } } - } - res = cuddBddConstrainDecomp(dd,f,decomp); + res = cuddBddConstrainDecomp(dd,f,decomp); } while (dd->reordered == 1); if (res == 0) { - ABC_FREE(decomp); - return(NULL); + ABC_FREE(decomp); + return(NULL); } /* Missing components are constant ones. */ for (i = 0; i < dd->size; i++) { - if (decomp[i] == NULL) { - decomp[i] = DD_ONE(dd); - cuddRef(decomp[i]); - } + if (decomp[i] == NULL) { + decomp[i] = DD_ONE(dd); + cuddRef(decomp[i]); + } } return(decomp); @@ -369,20 +441,20 @@ Cudd_addRestrict( /* Check if supports intersect. */ supp_f = Cudd_Support(dd, f); if (supp_f == NULL) { - return(NULL); + return(NULL); } cuddRef(supp_f); supp_c = Cudd_Support(dd, c); if (supp_c == NULL) { - Cudd_RecursiveDeref(dd,supp_f); - return(NULL); + Cudd_RecursiveDeref(dd,supp_f); + return(NULL); } cuddRef(supp_c); commonSupport = Cudd_bddLiteralSetIntersection(dd, supp_f, supp_c); if (commonSupport == NULL) { - Cudd_RecursiveDeref(dd,supp_f); - Cudd_RecursiveDeref(dd,supp_c); - return(NULL); + Cudd_RecursiveDeref(dd,supp_f); + Cudd_RecursiveDeref(dd,supp_c); + return(NULL); } cuddRef(commonSupport); Cudd_RecursiveDeref(dd,supp_f); @@ -391,21 +463,21 @@ Cudd_addRestrict( Cudd_RecursiveDeref(dd,commonSupport); if (intersection) { - do { - dd->reordered = 0; - res = cuddAddRestrictRecur(dd, f, c); - } while (dd->reordered == 1); - sizeF = Cudd_DagSize(f); - sizeRes = Cudd_DagSize(res); - if (sizeF <= sizeRes) { - cuddRef(res); - Cudd_RecursiveDeref(dd, res); - return(f); - } else { - return(res); - } + do { + dd->reordered = 0; + res = cuddAddRestrictRecur(dd, f, c); + } while (dd->reordered == 1); + sizeF = Cudd_DagSize(f); + sizeRes = Cudd_DagSize(res); + if (sizeF <= sizeRes) { + cuddRef(res); + Cudd_RecursiveDeref(dd, res); + return(f); + } else { + return(res); + } } else { - return(f); + return(f); } } /* end of Cudd_addRestrict */ @@ -427,7 +499,7 @@ Cudd_addRestrict( otherwise. The size of the array equals the number of variables in the manager. The components of the solution have their reference counts already incremented (unlike the results of most other functions in - the package.] + the package).] SideEffects [None] @@ -447,28 +519,28 @@ Cudd_bddCharToVect( vect = ABC_ALLOC(DdNode *, dd->size); if (vect == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(NULL); + dd->errorCode = CUDD_MEMORY_OUT; + return(NULL); } do { - dd->reordered = 0; - for (i = 0; i < dd->size; i++) { - res = cuddBddCharToVect(dd,f,dd->vars[dd->invperm[i]]); - if (res == NULL) { - /* Clean up the vector array in case reordering took place. */ - for (j = 0; j < i; j++) { - Cudd_IterDerefBdd(dd, vect[dd->invperm[j]]); - } - break; + dd->reordered = 0; + for (i = 0; i < dd->size; i++) { + res = cuddBddCharToVect(dd,f,dd->vars[dd->invperm[i]]); + if (res == NULL) { + /* Clean up the vector array in case reordering took place. */ + for (j = 0; j < i; j++) { + Cudd_IterDerefBdd(dd, vect[dd->invperm[j]]); + } + break; + } + cuddRef(res); + vect[dd->invperm[i]] = res; } - cuddRef(res); - vect[dd->invperm[i]] = res; - } } while (dd->reordered == 1); if (res == NULL) { - ABC_FREE(vect); - return(NULL); + ABC_FREE(vect); + return(NULL); } return(vect); @@ -503,8 +575,8 @@ Cudd_bddLICompaction( DdNode *res; do { - dd->reordered = 0; - res = cuddBddLICompaction(dd,f,c); + dd->reordered = 0; + res = cuddBddLICompaction(dd,f,c); } while (dd->reordered == 1); return(res); @@ -536,8 +608,8 @@ Cudd_bddSqueeze( int sizeRes, sizeL, sizeU; do { - dd->reordered = 0; - res = cuddBddSqueeze(dd,l,u); + dd->reordered = 0; + res = cuddBddSqueeze(dd,l,u); } while (dd->reordered == 1); if (res == NULL) return(NULL); /* We now compare the result with the bounds and return the smallest. @@ -546,17 +618,17 @@ Cudd_bddSqueeze( sizeRes = Cudd_DagSize(res); sizeU = Cudd_DagSize(u); if (sizeU <= sizeRes) { - cuddRef(res); - Cudd_IterDerefBdd(dd,res); - res = u; - sizeRes = sizeU; + cuddRef(res); + Cudd_IterDerefBdd(dd,res); + res = u; + sizeRes = sizeU; } sizeL = Cudd_DagSize(l); if (sizeL <= sizeRes) { - cuddRef(res); - Cudd_IterDerefBdd(dd,res); - res = l; - sizeRes = sizeL; + cuddRef(res); + Cudd_IterDerefBdd(dd,res); + res = l; + sizeRes = sizeL; } return(res); @@ -595,8 +667,8 @@ Cudd_bddMinimize( cuddRef(cplus); res = Cudd_bddLICompaction(dd,f,cplus); if (res == NULL) { - Cudd_IterDerefBdd(dd,cplus); - return(NULL); + Cudd_IterDerefBdd(dd,cplus); + return(NULL); } cuddRef(res); Cudd_IterDerefBdd(dd,cplus); @@ -638,15 +710,15 @@ Cudd_SubsetCompress( cuddRef(tmp1); tmp2 = Cudd_RemapUnderApprox(dd,tmp1,nvars,0,1.0); if (tmp2 == NULL) { - Cudd_IterDerefBdd(dd,tmp1); - return(NULL); + Cudd_IterDerefBdd(dd,tmp1); + return(NULL); } cuddRef(tmp2); Cudd_IterDerefBdd(dd,tmp1); res = Cudd_bddSqueeze(dd,tmp2,f); if (res == NULL) { - Cudd_IterDerefBdd(dd,tmp2); - return(NULL); + Cudd_IterDerefBdd(dd,tmp2); + return(NULL); } cuddRef(res); Cudd_IterDerefBdd(dd,tmp2); @@ -714,9 +786,9 @@ cuddBddConstrainRecur( DdNode * c) { DdNode *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r; - DdNode *one, *zero; + DdNode *one, *zero; unsigned int topf, topc; - int index; + int index; int comple = 0; statLine(dd); @@ -724,16 +796,16 @@ cuddBddConstrainRecur( zero = Cudd_Not(one); /* Trivial cases. */ - if (c == one) return(f); - if (c == zero) return(zero); - if (Cudd_IsConstant(f)) return(f); - if (f == c) return(one); - if (f == Cudd_Not(c)) return(zero); + if (c == one) return(f); + if (c == zero) return(zero); + if (Cudd_IsConstant(f)) return(f); + if (f == c) return(one); + if (f == Cudd_Not(c)) return(zero); /* Make canonical to increase the utilization of the cache. */ if (Cudd_IsComplement(f)) { - f = Cudd_Not(f); - comple = 1; + f = Cudd_Not(f); + comple = 1; } /* Now f is a regular pointer to a non-constant node; c is also ** non-constant, but may be complemented. @@ -742,78 +814,78 @@ cuddBddConstrainRecur( /* Check the cache. */ r = cuddCacheLookup2(dd, Cudd_bddConstrain, f, c); if (r != NULL) { - return(Cudd_NotCond(r,comple)); + return(Cudd_NotCond(r,comple)); } /* Recursive step. */ topf = dd->perm[f->index]; topc = dd->perm[Cudd_Regular(c)->index]; if (topf <= topc) { - index = f->index; - Fv = cuddT(f); Fnv = cuddE(f); + index = f->index; + Fv = cuddT(f); Fnv = cuddE(f); } else { - index = Cudd_Regular(c)->index; - Fv = Fnv = f; + index = Cudd_Regular(c)->index; + Fv = Fnv = f; } if (topc <= topf) { - Cv = cuddT(Cudd_Regular(c)); Cnv = cuddE(Cudd_Regular(c)); - if (Cudd_IsComplement(c)) { - Cv = Cudd_Not(Cv); - Cnv = Cudd_Not(Cnv); - } + Cv = cuddT(Cudd_Regular(c)); Cnv = cuddE(Cudd_Regular(c)); + if (Cudd_IsComplement(c)) { + Cv = Cudd_Not(Cv); + Cnv = Cudd_Not(Cnv); + } } else { - Cv = Cnv = c; + Cv = Cnv = c; } if (!Cudd_IsConstant(Cv)) { - t = cuddBddConstrainRecur(dd, Fv, Cv); - if (t == NULL) - return(NULL); + t = cuddBddConstrainRecur(dd, Fv, Cv); + if (t == NULL) + return(NULL); } else if (Cv == one) { - t = Fv; - } else { /* Cv == zero: return Fnv @ Cnv */ - if (Cnv == one) { - r = Fnv; - } else { - r = cuddBddConstrainRecur(dd, Fnv, Cnv); - if (r == NULL) - return(NULL); - } - return(Cudd_NotCond(r,comple)); + t = Fv; + } else { /* Cv == zero: return Fnv @ Cnv */ + if (Cnv == one) { + r = Fnv; + } else { + r = cuddBddConstrainRecur(dd, Fnv, Cnv); + if (r == NULL) + return(NULL); + } + return(Cudd_NotCond(r,comple)); } cuddRef(t); if (!Cudd_IsConstant(Cnv)) { - e = cuddBddConstrainRecur(dd, Fnv, Cnv); - if (e == NULL) { - Cudd_IterDerefBdd(dd, t); - return(NULL); - } + e = cuddBddConstrainRecur(dd, Fnv, Cnv); + if (e == NULL) { + Cudd_IterDerefBdd(dd, t); + return(NULL); + } } else if (Cnv == one) { - e = Fnv; - } else { /* Cnv == zero: return Fv @ Cv previously computed */ - cuddDeref(t); - return(Cudd_NotCond(t,comple)); + e = Fnv; + } else { /* Cnv == zero: return Fv @ Cv previously computed */ + cuddDeref(t); + return(Cudd_NotCond(t,comple)); } cuddRef(e); if (Cudd_IsComplement(t)) { - t = Cudd_Not(t); - e = Cudd_Not(e); - r = (t == e) ? t : cuddUniqueInter(dd, index, t, e); - if (r == NULL) { - Cudd_IterDerefBdd(dd, e); - Cudd_IterDerefBdd(dd, t); - return(NULL); - } - r = Cudd_Not(r); + t = Cudd_Not(t); + e = Cudd_Not(e); + r = (t == e) ? t : cuddUniqueInter(dd, index, t, e); + if (r == NULL) { + Cudd_IterDerefBdd(dd, e); + Cudd_IterDerefBdd(dd, t); + return(NULL); + } + r = Cudd_Not(r); } else { - r = (t == e) ? t : cuddUniqueInter(dd, index, t, e); - if (r == NULL) { - Cudd_IterDerefBdd(dd, e); - Cudd_IterDerefBdd(dd, t); - return(NULL); - } + r = (t == e) ? t : cuddUniqueInter(dd, index, t, e); + if (r == NULL) { + Cudd_IterDerefBdd(dd, e); + Cudd_IterDerefBdd(dd, t); + return(NULL); + } } cuddDeref(t); cuddDeref(e); @@ -842,26 +914,26 @@ cuddBddRestrictRecur( DdNode * f, DdNode * c) { - DdNode *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r, *one, *zero; + DdNode *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r, *one, *zero; unsigned int topf, topc; - int index; - int comple = 0; + int index; + int comple = 0; statLine(dd); one = DD_ONE(dd); zero = Cudd_Not(one); /* Trivial cases */ - if (c == one) return(f); - if (c == zero) return(zero); - if (Cudd_IsConstant(f)) return(f); - if (f == c) return(one); - if (f == Cudd_Not(c)) return(zero); + if (c == one) return(f); + if (c == zero) return(zero); + if (Cudd_IsConstant(f)) return(f); + if (f == c) return(one); + if (f == Cudd_Not(c)) return(zero); /* Make canonical to increase the utilization of the cache. */ if (Cudd_IsComplement(f)) { - f = Cudd_Not(f); - comple = 1; + f = Cudd_Not(f); + comple = 1; } /* Now f is a regular pointer to a non-constant node; c is also ** non-constant, but may be complemented. @@ -870,100 +942,100 @@ cuddBddRestrictRecur( /* Check the cache. */ r = cuddCacheLookup2(dd, Cudd_bddRestrict, f, c); if (r != NULL) { - return(Cudd_NotCond(r,comple)); + return(Cudd_NotCond(r,comple)); } topf = dd->perm[f->index]; topc = dd->perm[Cudd_Regular(c)->index]; - if (topc < topf) { /* abstract top variable from c */ - DdNode *d, *s1, *s2; + if (topc < topf) { /* abstract top variable from c */ + DdNode *d, *s1, *s2; - /* Find complements of cofactors of c. */ - if (Cudd_IsComplement(c)) { - s1 = cuddT(Cudd_Regular(c)); - s2 = cuddE(Cudd_Regular(c)); - } else { - s1 = Cudd_Not(cuddT(c)); - s2 = Cudd_Not(cuddE(c)); - } - /* Take the OR by applying DeMorgan. */ - d = cuddBddAndRecur(dd, s1, s2); - if (d == NULL) return(NULL); - d = Cudd_Not(d); - cuddRef(d); - r = cuddBddRestrictRecur(dd, f, d); - if (r == NULL) { + /* Find complements of cofactors of c. */ + if (Cudd_IsComplement(c)) { + s1 = cuddT(Cudd_Regular(c)); + s2 = cuddE(Cudd_Regular(c)); + } else { + s1 = Cudd_Not(cuddT(c)); + s2 = Cudd_Not(cuddE(c)); + } + /* Take the OR by applying DeMorgan. */ + d = cuddBddAndRecur(dd, s1, s2); + if (d == NULL) return(NULL); + d = Cudd_Not(d); + cuddRef(d); + r = cuddBddRestrictRecur(dd, f, d); + if (r == NULL) { + Cudd_IterDerefBdd(dd, d); + return(NULL); + } + cuddRef(r); Cudd_IterDerefBdd(dd, d); - return(NULL); - } - cuddRef(r); - Cudd_IterDerefBdd(dd, d); - cuddCacheInsert2(dd, Cudd_bddRestrict, f, c, r); - cuddDeref(r); - return(Cudd_NotCond(r,comple)); + cuddCacheInsert2(dd, Cudd_bddRestrict, f, c, r); + cuddDeref(r); + return(Cudd_NotCond(r,comple)); } /* Recursive step. Here topf <= topc. */ index = f->index; Fv = cuddT(f); Fnv = cuddE(f); if (topc == topf) { - Cv = cuddT(Cudd_Regular(c)); Cnv = cuddE(Cudd_Regular(c)); - if (Cudd_IsComplement(c)) { - Cv = Cudd_Not(Cv); - Cnv = Cudd_Not(Cnv); - } + Cv = cuddT(Cudd_Regular(c)); Cnv = cuddE(Cudd_Regular(c)); + if (Cudd_IsComplement(c)) { + Cv = Cudd_Not(Cv); + Cnv = Cudd_Not(Cnv); + } } else { - Cv = Cnv = c; + Cv = Cnv = c; } if (!Cudd_IsConstant(Cv)) { - t = cuddBddRestrictRecur(dd, Fv, Cv); - if (t == NULL) return(NULL); + t = cuddBddRestrictRecur(dd, Fv, Cv); + if (t == NULL) return(NULL); } else if (Cv == one) { - t = Fv; - } else { /* Cv == zero: return(Fnv @ Cnv) */ - if (Cnv == one) { - r = Fnv; - } else { - r = cuddBddRestrictRecur(dd, Fnv, Cnv); - if (r == NULL) return(NULL); - } - return(Cudd_NotCond(r,comple)); + t = Fv; + } else { /* Cv == zero: return(Fnv @ Cnv) */ + if (Cnv == one) { + r = Fnv; + } else { + r = cuddBddRestrictRecur(dd, Fnv, Cnv); + if (r == NULL) return(NULL); + } + return(Cudd_NotCond(r,comple)); } cuddRef(t); if (!Cudd_IsConstant(Cnv)) { - e = cuddBddRestrictRecur(dd, Fnv, Cnv); - if (e == NULL) { - Cudd_IterDerefBdd(dd, t); - return(NULL); - } + e = cuddBddRestrictRecur(dd, Fnv, Cnv); + if (e == NULL) { + Cudd_IterDerefBdd(dd, t); + return(NULL); + } } else if (Cnv == one) { - e = Fnv; - } else { /* Cnv == zero: return (Fv @ Cv) previously computed */ - cuddDeref(t); - return(Cudd_NotCond(t,comple)); + e = Fnv; + } else { /* Cnv == zero: return (Fv @ Cv) previously computed */ + cuddDeref(t); + return(Cudd_NotCond(t,comple)); } cuddRef(e); if (Cudd_IsComplement(t)) { - t = Cudd_Not(t); - e = Cudd_Not(e); - r = (t == e) ? t : cuddUniqueInter(dd, index, t, e); - if (r == NULL) { - Cudd_IterDerefBdd(dd, e); - Cudd_IterDerefBdd(dd, t); - return(NULL); - } - r = Cudd_Not(r); + t = Cudd_Not(t); + e = Cudd_Not(e); + r = (t == e) ? t : cuddUniqueInter(dd, index, t, e); + if (r == NULL) { + Cudd_IterDerefBdd(dd, e); + Cudd_IterDerefBdd(dd, t); + return(NULL); + } + r = Cudd_Not(r); } else { - r = (t == e) ? t : cuddUniqueInter(dd, index, t, e); - if (r == NULL) { - Cudd_IterDerefBdd(dd, e); - Cudd_IterDerefBdd(dd, t); - return(NULL); - } + r = (t == e) ? t : cuddUniqueInter(dd, index, t, e); + if (r == NULL) { + Cudd_IterDerefBdd(dd, e); + Cudd_IterDerefBdd(dd, t); + return(NULL); + } } cuddDeref(t); cuddDeref(e); @@ -976,6 +1048,147 @@ cuddBddRestrictRecur( /**Function******************************************************************** + Synopsis [Implements the recursive step of Cudd_bddAnd.] + + Description [Implements the recursive step of Cudd_bddNPAnd. + Returns a pointer to the result is successful; NULL otherwise.] + + SideEffects [None] + + SeeAlso [Cudd_bddNPAnd] + +******************************************************************************/ +DdNode * +cuddBddNPAndRecur( + DdManager * manager, + DdNode * f, + DdNode * g) +{ + DdNode *F, *ft, *fe, *G, *gt, *ge; + DdNode *one, *r, *t, *e; + unsigned int topf, topg, index; + + statLine(manager); + one = DD_ONE(manager); + + /* Terminal cases. */ + F = Cudd_Regular(f); + G = Cudd_Regular(g); + if (F == G) { + if (f == g) return(one); + else return(Cudd_Not(one)); + } + if (G == one) { + if (g == one) return(f); + else return(g); + } + if (F == one) { + return(f); + } + + /* At this point f and g are not constant. */ + /* Check cache. */ + if (F->ref != 1 || G->ref != 1) { + r = cuddCacheLookup2(manager, Cudd_bddNPAnd, f, g); + if (r != NULL) return(r); + } + + /* Here we can skip the use of cuddI, because the operands are known + ** to be non-constant. + */ + topf = manager->perm[F->index]; + topg = manager->perm[G->index]; + + if (topg < topf) { /* abstract top variable from g */ + DdNode *d; + + /* Find complements of cofactors of g. */ + if (Cudd_IsComplement(g)) { + gt = cuddT(G); + ge = cuddE(G); + } else { + gt = Cudd_Not(cuddT(g)); + ge = Cudd_Not(cuddE(g)); + } + /* Take the OR by applying DeMorgan. */ + d = cuddBddAndRecur(manager, gt, ge); + if (d == NULL) return(NULL); + d = Cudd_Not(d); + cuddRef(d); + r = cuddBddNPAndRecur(manager, f, d); + if (r == NULL) { + Cudd_IterDerefBdd(manager, d); + return(NULL); + } + cuddRef(r); + Cudd_IterDerefBdd(manager, d); + cuddCacheInsert2(manager, Cudd_bddNPAnd, f, g, r); + cuddDeref(r); + return(r); + } + + /* Compute cofactors. */ + index = F->index; + ft = cuddT(F); + fe = cuddE(F); + if (Cudd_IsComplement(f)) { + ft = Cudd_Not(ft); + fe = Cudd_Not(fe); + } + + if (topg == topf) { + gt = cuddT(G); + ge = cuddE(G); + if (Cudd_IsComplement(g)) { + gt = Cudd_Not(gt); + ge = Cudd_Not(ge); + } + } else { + gt = ge = g; + } + + t = cuddBddAndRecur(manager, ft, gt); + if (t == NULL) return(NULL); + cuddRef(t); + + e = cuddBddAndRecur(manager, fe, ge); + if (e == NULL) { + Cudd_IterDerefBdd(manager, t); + return(NULL); + } + cuddRef(e); + + if (t == e) { + r = t; + } else { + if (Cudd_IsComplement(t)) { + r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e)); + if (r == NULL) { + Cudd_IterDerefBdd(manager, t); + Cudd_IterDerefBdd(manager, e); + return(NULL); + } + r = Cudd_Not(r); + } else { + r = cuddUniqueInter(manager,(int)index,t,e); + if (r == NULL) { + Cudd_IterDerefBdd(manager, t); + Cudd_IterDerefBdd(manager, e); + return(NULL); + } + } + } + cuddDeref(e); + cuddDeref(t); + if (F->ref != 1 || G->ref != 1) + cuddCacheInsert2(manager, Cudd_bddNPAnd, f, g, r); + return(r); + +} /* end of cuddBddNPAndRecur */ + + +/**Function******************************************************************** + Synopsis [Performs the recursive step of Cudd_addConstrain.] Description [Performs the recursive step of Cudd_addConstrain. @@ -993,81 +1206,81 @@ cuddAddConstrainRecur( DdNode * c) { DdNode *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r; - DdNode *one, *zero; + DdNode *one, *zero; unsigned int topf, topc; - int index; + int index; statLine(dd); one = DD_ONE(dd); zero = DD_ZERO(dd); /* Trivial cases. */ - if (c == one) return(f); - if (c == zero) return(zero); - if (Cudd_IsConstant(f)) return(f); - if (f == c) return(one); + if (c == one) return(f); + if (c == zero) return(zero); + if (Cudd_IsConstant(f)) return(f); + if (f == c) return(one); /* Now f and c are non-constant. */ /* Check the cache. */ r = cuddCacheLookup2(dd, Cudd_addConstrain, f, c); if (r != NULL) { - return(r); + return(r); } /* Recursive step. */ topf = dd->perm[f->index]; topc = dd->perm[c->index]; if (topf <= topc) { - index = f->index; - Fv = cuddT(f); Fnv = cuddE(f); + index = f->index; + Fv = cuddT(f); Fnv = cuddE(f); } else { - index = c->index; - Fv = Fnv = f; + index = c->index; + Fv = Fnv = f; } if (topc <= topf) { - Cv = cuddT(c); Cnv = cuddE(c); + Cv = cuddT(c); Cnv = cuddE(c); } else { - Cv = Cnv = c; + Cv = Cnv = c; } if (!Cudd_IsConstant(Cv)) { - t = cuddAddConstrainRecur(dd, Fv, Cv); - if (t == NULL) - return(NULL); + t = cuddAddConstrainRecur(dd, Fv, Cv); + if (t == NULL) + return(NULL); } else if (Cv == one) { - t = Fv; - } else { /* Cv == zero: return Fnv @ Cnv */ - if (Cnv == one) { - r = Fnv; - } else { - r = cuddAddConstrainRecur(dd, Fnv, Cnv); - if (r == NULL) - return(NULL); - } - return(r); + t = Fv; + } else { /* Cv == zero: return Fnv @ Cnv */ + if (Cnv == one) { + r = Fnv; + } else { + r = cuddAddConstrainRecur(dd, Fnv, Cnv); + if (r == NULL) + return(NULL); + } + return(r); } cuddRef(t); if (!Cudd_IsConstant(Cnv)) { - e = cuddAddConstrainRecur(dd, Fnv, Cnv); - if (e == NULL) { - Cudd_RecursiveDeref(dd, t); - return(NULL); - } + e = cuddAddConstrainRecur(dd, Fnv, Cnv); + if (e == NULL) { + Cudd_RecursiveDeref(dd, t); + return(NULL); + } } else if (Cnv == one) { - e = Fnv; - } else { /* Cnv == zero: return Fv @ Cv previously computed */ - cuddDeref(t); - return(t); + e = Fnv; + } else { /* Cnv == zero: return Fv @ Cv previously computed */ + cuddDeref(t); + return(t); } cuddRef(e); r = (t == e) ? t : cuddUniqueInter(dd, index, t, e); if (r == NULL) { - Cudd_RecursiveDeref(dd, e); - Cudd_RecursiveDeref(dd, t); - return(NULL); + Cudd_RecursiveDeref(dd, e); + Cudd_RecursiveDeref(dd, t); + return(NULL); } cuddDeref(t); cuddDeref(e); @@ -1096,97 +1309,97 @@ cuddAddRestrictRecur( DdNode * f, DdNode * c) { - DdNode *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r, *one, *zero; + DdNode *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r, *one, *zero; unsigned int topf, topc; - int index; + int index; statLine(dd); one = DD_ONE(dd); zero = DD_ZERO(dd); /* Trivial cases */ - if (c == one) return(f); - if (c == zero) return(zero); - if (Cudd_IsConstant(f)) return(f); - if (f == c) return(one); + if (c == one) return(f); + if (c == zero) return(zero); + if (Cudd_IsConstant(f)) return(f); + if (f == c) return(one); /* Now f and c are non-constant. */ /* Check the cache. */ r = cuddCacheLookup2(dd, Cudd_addRestrict, f, c); if (r != NULL) { - return(r); + return(r); } topf = dd->perm[f->index]; topc = dd->perm[c->index]; - if (topc < topf) { /* abstract top variable from c */ - DdNode *d, *s1, *s2; - - /* Find cofactors of c. */ - s1 = cuddT(c); - s2 = cuddE(c); - /* Take the OR by applying DeMorgan. */ - d = cuddAddApplyRecur(dd, Cudd_addOr, s1, s2); - if (d == NULL) return(NULL); - cuddRef(d); - r = cuddAddRestrictRecur(dd, f, d); - if (r == NULL) { + if (topc < topf) { /* abstract top variable from c */ + DdNode *d, *s1, *s2; + + /* Find cofactors of c. */ + s1 = cuddT(c); + s2 = cuddE(c); + /* Take the OR by applying DeMorgan. */ + d = cuddAddApplyRecur(dd, Cudd_addOr, s1, s2); + if (d == NULL) return(NULL); + cuddRef(d); + r = cuddAddRestrictRecur(dd, f, d); + if (r == NULL) { + Cudd_RecursiveDeref(dd, d); + return(NULL); + } + cuddRef(r); Cudd_RecursiveDeref(dd, d); - return(NULL); - } - cuddRef(r); - Cudd_RecursiveDeref(dd, d); - cuddCacheInsert2(dd, Cudd_addRestrict, f, c, r); - cuddDeref(r); - return(r); + cuddCacheInsert2(dd, Cudd_addRestrict, f, c, r); + cuddDeref(r); + return(r); } /* Recursive step. Here topf <= topc. */ index = f->index; Fv = cuddT(f); Fnv = cuddE(f); if (topc == topf) { - Cv = cuddT(c); Cnv = cuddE(c); + Cv = cuddT(c); Cnv = cuddE(c); } else { - Cv = Cnv = c; + Cv = Cnv = c; } if (!Cudd_IsConstant(Cv)) { - t = cuddAddRestrictRecur(dd, Fv, Cv); - if (t == NULL) return(NULL); + t = cuddAddRestrictRecur(dd, Fv, Cv); + if (t == NULL) return(NULL); } else if (Cv == one) { - t = Fv; - } else { /* Cv == zero: return(Fnv @ Cnv) */ - if (Cnv == one) { - r = Fnv; - } else { - r = cuddAddRestrictRecur(dd, Fnv, Cnv); - if (r == NULL) return(NULL); - } - return(r); + t = Fv; + } else { /* Cv == zero: return(Fnv @ Cnv) */ + if (Cnv == one) { + r = Fnv; + } else { + r = cuddAddRestrictRecur(dd, Fnv, Cnv); + if (r == NULL) return(NULL); + } + return(r); } cuddRef(t); if (!Cudd_IsConstant(Cnv)) { - e = cuddAddRestrictRecur(dd, Fnv, Cnv); - if (e == NULL) { - Cudd_RecursiveDeref(dd, t); - return(NULL); - } + e = cuddAddRestrictRecur(dd, Fnv, Cnv); + if (e == NULL) { + Cudd_RecursiveDeref(dd, t); + return(NULL); + } } else if (Cnv == one) { - e = Fnv; - } else { /* Cnv == zero: return (Fv @ Cv) previously computed */ - cuddDeref(t); - return(t); + e = Fnv; + } else { /* Cnv == zero: return (Fv @ Cv) previously computed */ + cuddDeref(t); + return(t); } cuddRef(e); r = (t == e) ? t : cuddUniqueInter(dd, index, t, e); if (r == NULL) { - Cudd_RecursiveDeref(dd, e); - Cudd_RecursiveDeref(dd, t); - return(NULL); + Cudd_RecursiveDeref(dd, e); + Cudd_RecursiveDeref(dd, t); + return(NULL); } cuddDeref(t); cuddDeref(e); @@ -1240,27 +1453,27 @@ cuddBddLICompaction( ** appears. Hence, the same node and constrain may give different results ** in successive invocations. */ - marktable = st_init_table(st_ptrcmp, st_ptrhash);; + marktable = st_init_table(st_ptrcmp,st_ptrhash); if (marktable == NULL) { - return(NULL); + return(NULL); } markcache = st_init_table(MarkCacheCompare,MarkCacheHash); if (markcache == NULL) { - st_free_table(marktable); - return(NULL); + st_free_table(marktable); + return(NULL); } if (cuddBddLICMarkEdges(dd,f,c,marktable,markcache) == CUDD_OUT_OF_MEM) { - st_foreach(markcache, (ST_PFSR)MarkCacheCleanUp, NULL); - st_free_table(marktable); - st_free_table(markcache); - return(NULL); + st_foreach(markcache, MarkCacheCleanUp, NULL); + st_free_table(marktable); + st_free_table(markcache); + return(NULL); } - st_foreach(markcache, (ST_PFSR)MarkCacheCleanUp, NULL); + st_foreach(markcache, MarkCacheCleanUp, NULL); st_free_table(markcache); - buildcache = st_init_table(st_ptrcmp, st_ptrhash);; + buildcache = st_init_table(st_ptrcmp,st_ptrhash); if (buildcache == NULL) { - st_free_table(marktable); - return(NULL); + st_free_table(marktable); + return(NULL); } res = cuddBddLICBuildResult(dd,f,buildcache,marktable); st_free_table(buildcache); @@ -1304,13 +1517,13 @@ cuddBddConstrainDecomp( fv = cuddT(F); fvn = cuddE(F); if (F == f) { - fv = Cudd_Not(fv); - fvn = Cudd_Not(fvn); + fv = Cudd_Not(fv); + fvn = Cudd_Not(fvn); } /* Compute abstraction of top variable. */ fAbs = cuddBddAndRecur(dd, fv, fvn); if (fAbs == NULL) { - return(0); + return(0); } cuddRef(fAbs); fAbs = Cudd_Not(fAbs); @@ -1318,15 +1531,15 @@ cuddBddConstrainDecomp( ** decomposition. */ ok = cuddBddConstrainDecomp(dd, fAbs, decomp); if (ok == 0) { - Cudd_IterDerefBdd(dd,fAbs); - return(0); + Cudd_IterDerefBdd(dd,fAbs); + return(0); } /* Compute the component of the decomposition corresponding to the ** top variable and store it in the decomposition array. */ result = cuddBddConstrainRecur(dd, f, fAbs); if (result == NULL) { - Cudd_IterDerefBdd(dd,fAbs); - return(0); + Cudd_IterDerefBdd(dd,fAbs); + return(0); } cuddRef(result); decomp[F->index] = result; @@ -1365,7 +1578,7 @@ cuddBddCharToVect( /* Check the cache. */ res = cuddCacheLookup2(dd, cuddBddCharToVect, f, x); if (res != NULL) { - return(res); + return(res); } F = Cudd_Regular(f); @@ -1383,9 +1596,9 @@ cuddBddCharToVect( fE = Cudd_NotCond(cuddE(F),comple); if (topf == level) { - if (fT == zero) return(zero); - if (fE == zero) return(one); - return(x); + if (fT == zero) return(zero); + if (fE == zero) return(one); + return(x); } /* Here topf < level. */ @@ -1394,20 +1607,20 @@ cuddBddCharToVect( T = cuddBddCharToVect(dd, fT, x); if (T == NULL) { - return(NULL); + return(NULL); } cuddRef(T); E = cuddBddCharToVect(dd, fE, x); if (E == NULL) { - Cudd_IterDerefBdd(dd,T); - return(NULL); + Cudd_IterDerefBdd(dd,T); + return(NULL); } cuddRef(E); res = cuddBddIteRecur(dd, dd->vars[F->index], T, E); if (res == NULL) { - Cudd_IterDerefBdd(dd,T); - Cudd_IterDerefBdd(dd,E); - return(NULL); + Cudd_IterDerefBdd(dd,T); + Cudd_IterDerefBdd(dd,E); + return(NULL); } cuddDeref(T); cuddDeref(E); @@ -1441,7 +1654,6 @@ cuddBddLICMarkEdges( DdNode *Fv, *Fnv, *Cv, *Cnv; DdNode *one, *zero; unsigned int topf, topc; - int index; int comple; int resT, resE, res, retval; char **slot; @@ -1465,75 +1677,73 @@ cuddBddLICMarkEdges( /* Check the cache. */ key = ABC_ALLOC(MarkCacheKey, 1); if (key == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(CUDD_OUT_OF_MEM); + dd->errorCode = CUDD_MEMORY_OUT; + return(CUDD_OUT_OF_MEM); } key->f = f; key->c = c; - if (st_lookup(cache, (char *)key, (char **)&res)) { - ABC_FREE(key); - if (comple) { - if (res == DD_LIC_0) res = DD_LIC_1; - else if (res == DD_LIC_1) res = DD_LIC_0; - } - return(res); + if (st_lookup_int(cache, (char *)key, &res)) { + ABC_FREE(key); + if (comple) { + if (res == DD_LIC_0) res = DD_LIC_1; + else if (res == DD_LIC_1) res = DD_LIC_0; + } + return(res); } /* Recursive step. */ topf = dd->perm[f->index]; topc = cuddI(dd,Cudd_Regular(c)->index); if (topf <= topc) { - index = f->index; - Fv = cuddT(f); Fnv = cuddE(f); + Fv = cuddT(f); Fnv = cuddE(f); } else { - index = Cudd_Regular(c)->index; - Fv = Fnv = f; + Fv = Fnv = f; } if (topc <= topf) { - /* We know that c is not constant because f is not. */ - Cv = cuddT(Cudd_Regular(c)); Cnv = cuddE(Cudd_Regular(c)); - if (Cudd_IsComplement(c)) { - Cv = Cudd_Not(Cv); - Cnv = Cudd_Not(Cnv); - } + /* We know that c is not constant because f is not. */ + Cv = cuddT(Cudd_Regular(c)); Cnv = cuddE(Cudd_Regular(c)); + if (Cudd_IsComplement(c)) { + Cv = Cudd_Not(Cv); + Cnv = Cudd_Not(Cnv); + } } else { - Cv = Cnv = c; + Cv = Cnv = c; } resT = cuddBddLICMarkEdges(dd, Fv, Cv, table, cache); if (resT == CUDD_OUT_OF_MEM) { - ABC_FREE(key); - return(CUDD_OUT_OF_MEM); + ABC_FREE(key); + return(CUDD_OUT_OF_MEM); } resE = cuddBddLICMarkEdges(dd, Fnv, Cnv, table, cache); if (resE == CUDD_OUT_OF_MEM) { - ABC_FREE(key); - return(CUDD_OUT_OF_MEM); + ABC_FREE(key); + return(CUDD_OUT_OF_MEM); } /* Update edge markings. */ if (topf <= topc) { - retval = st_find_or_add(table, (char *)f, (char ***)&slot); - if (retval == 0) { - *slot = (char *) (ptrint)((resT << 2) | resE); - } else if (retval == 1) { - *slot = (char *) (ptrint)((int)((ptrint) *slot) | (resT << 2) | resE); - } else { - ABC_FREE(key); - return(CUDD_OUT_OF_MEM); - } + retval = st_find_or_add(table, (char *)f, (char ***)&slot); + if (retval == 0) { + *slot = (char *) (ptrint)((resT << 2) | resE); + } else if (retval == 1) { + *slot = (char *) (ptrint)((int)((ptrint) *slot) | (resT << 2) | resE); + } else { + ABC_FREE(key); + return(CUDD_OUT_OF_MEM); + } } /* Cache result. */ res = resT | resE; if (st_insert(cache, (char *)key, (char *)(ptrint)res) == ST_OUT_OF_MEM) { - ABC_FREE(key); - return(CUDD_OUT_OF_MEM); + ABC_FREE(key); + return(CUDD_OUT_OF_MEM); } /* Take into account possible complementation. */ if (comple) { - if (res == DD_LIC_0) res = DD_LIC_1; - else if (res == DD_LIC_1) res = DD_LIC_0; + if (res == DD_LIC_0) res = DD_LIC_1; + else if (res == DD_LIC_1) res = DD_LIC_0; } return(res); @@ -1561,8 +1771,7 @@ cuddBddLICBuildResult( { DdNode *Fv, *Fnv, *r, *t, *e; DdNode *one, *zero; - unsigned int topf; - int index; + int index; int comple; int markT, markE, markings; @@ -1575,75 +1784,74 @@ cuddBddLICBuildResult( f = Cudd_Regular(f); /* Check the cache. */ - if (st_lookup(cache, (char *)f, (char **)&r)) { - return(Cudd_NotCond(r,comple)); + if (st_lookup(cache, (const char *)f, (char **)&r)) { + return(Cudd_NotCond(r,comple)); } /* Retrieve the edge markings. */ - if (st_lookup(table, (char *)f, (char **)&markings) == 0) - return(NULL); + if (st_lookup_int(table, (char *)f, &markings) == 0) + return(NULL); markT = markings >> 2; markE = markings & 3; - topf = dd->perm[f->index]; index = f->index; Fv = cuddT(f); Fnv = cuddE(f); if (markT == DD_LIC_NL) { - t = cuddBddLICBuildResult(dd,Fv,cache,table); - if (t == NULL) { - return(NULL); - } + t = cuddBddLICBuildResult(dd,Fv,cache,table); + if (t == NULL) { + return(NULL); + } } else if (markT == DD_LIC_1) { - t = one; + t = one; } else { - t = zero; + t = zero; } cuddRef(t); if (markE == DD_LIC_NL) { - e = cuddBddLICBuildResult(dd,Fnv,cache,table); - if (e == NULL) { - Cudd_IterDerefBdd(dd,t); - return(NULL); - } + e = cuddBddLICBuildResult(dd,Fnv,cache,table); + if (e == NULL) { + Cudd_IterDerefBdd(dd,t); + return(NULL); + } } else if (markE == DD_LIC_1) { - e = one; + e = one; } else { - e = zero; + e = zero; } cuddRef(e); if (markT == DD_LIC_DC && markE != DD_LIC_DC) { - r = e; + r = e; } else if (markT != DD_LIC_DC && markE == DD_LIC_DC) { - r = t; - } else { - if (Cudd_IsComplement(t)) { - t = Cudd_Not(t); - e = Cudd_Not(e); - r = (t == e) ? t : cuddUniqueInter(dd, index, t, e); - if (r == NULL) { - Cudd_IterDerefBdd(dd, e); - Cudd_IterDerefBdd(dd, t); - return(NULL); - } - r = Cudd_Not(r); + r = t; } else { - r = (t == e) ? t : cuddUniqueInter(dd, index, t, e); - if (r == NULL) { - Cudd_IterDerefBdd(dd, e); - Cudd_IterDerefBdd(dd, t); - return(NULL); + if (Cudd_IsComplement(t)) { + t = Cudd_Not(t); + e = Cudd_Not(e); + r = (t == e) ? t : cuddUniqueInter(dd, index, t, e); + if (r == NULL) { + Cudd_IterDerefBdd(dd, e); + Cudd_IterDerefBdd(dd, t); + return(NULL); + } + r = Cudd_Not(r); + } else { + r = (t == e) ? t : cuddUniqueInter(dd, index, t, e); + if (r == NULL) { + Cudd_IterDerefBdd(dd, e); + Cudd_IterDerefBdd(dd, t); + return(NULL); + } } } - } cuddDeref(t); cuddDeref(e); if (st_insert(cache, (char *)f, (char *)r) == ST_OUT_OF_MEM) { - cuddRef(r); - Cudd_IterDerefBdd(dd,r); - return(NULL); + cuddRef(r); + Cudd_IterDerefBdd(dd,r); + return(NULL); } return(Cudd_NotCond(r,comple)); @@ -1669,9 +1877,9 @@ MarkCacheHash( int modulus) { int val = 0; - const MarkCacheKey *entry; + MarkCacheKey *entry; - entry = (const MarkCacheKey *) ptr; + entry = (MarkCacheKey *) ptr; val = (int) (ptrint) entry->f; val = val * 997 + (int) (ptrint) entry->c; @@ -1771,7 +1979,7 @@ cuddBddSqueeze( statLine(dd); if (l == u) { - return(l); + return(l); } one = DD_ONE(dd); zero = Cudd_Not(one); @@ -1785,11 +1993,11 @@ cuddBddSqueeze( /* Make canonical to increase the utilization of the cache. */ if (Cudd_IsComplement(u)) { - DdNode *temp; - temp = Cudd_Not(l); - l = Cudd_Not(u); - u = temp; - comple = 1; + DdNode *temp; + temp = Cudd_Not(l); + l = Cudd_Not(u); + u = temp; + comple = 1; } /* At this point u is regular and non-constant; l is non-constant, but ** may be complemented. */ @@ -1799,89 +2007,89 @@ cuddBddSqueeze( /* Check the cache. */ r = cuddCacheLookup2(dd, Cudd_bddSqueeze, l, u); if (r != NULL) { - return(Cudd_NotCond(r,comple)); + return(Cudd_NotCond(r,comple)); } /* Recursive step. */ topu = dd->perm[u->index]; topl = dd->perm[Cudd_Regular(l)->index]; if (topu <= topl) { - index = u->index; - ut = cuddT(u); ue = cuddE(u); + index = u->index; + ut = cuddT(u); ue = cuddE(u); } else { - index = Cudd_Regular(l)->index; - ut = ue = u; + index = Cudd_Regular(l)->index; + ut = ue = u; } if (topl <= topu) { - lt = cuddT(Cudd_Regular(l)); le = cuddE(Cudd_Regular(l)); - if (Cudd_IsComplement(l)) { - lt = Cudd_Not(lt); - le = Cudd_Not(le); - } + lt = cuddT(Cudd_Regular(l)); le = cuddE(Cudd_Regular(l)); + if (Cudd_IsComplement(l)) { + lt = Cudd_Not(lt); + le = Cudd_Not(le); + } } else { - lt = le = l; + lt = le = l; } /* If one interval is contained in the other, use the smaller ** interval. This corresponds to one-sided matching. */ if ((lt == zero || Cudd_bddLeq(dd,lt,le)) && - (ut == one || Cudd_bddLeq(dd,ue,ut))) { /* remap */ - r = cuddBddSqueeze(dd, le, ue); - if (r == NULL) - return(NULL); - return(Cudd_NotCond(r,comple)); + (ut == one || Cudd_bddLeq(dd,ue,ut))) { /* remap */ + r = cuddBddSqueeze(dd, le, ue); + if (r == NULL) + return(NULL); + return(Cudd_NotCond(r,comple)); } else if ((le == zero || Cudd_bddLeq(dd,le,lt)) && - (ue == one || Cudd_bddLeq(dd,ut,ue))) { /* remap */ - r = cuddBddSqueeze(dd, lt, ut); - if (r == NULL) - return(NULL); - return(Cudd_NotCond(r,comple)); + (ue == one || Cudd_bddLeq(dd,ut,ue))) { /* remap */ + r = cuddBddSqueeze(dd, lt, ut); + if (r == NULL) + return(NULL); + return(Cudd_NotCond(r,comple)); } else if ((le == zero || Cudd_bddLeq(dd,le,Cudd_Not(ut))) && - (ue == one || Cudd_bddLeq(dd,Cudd_Not(lt),ue))) { /* c-remap */ - t = cuddBddSqueeze(dd, lt, ut); - cuddRef(t); - if (Cudd_IsComplement(t)) { - r = cuddUniqueInter(dd, index, Cudd_Not(t), t); - if (r == NULL) { - Cudd_IterDerefBdd(dd, t); - return(NULL); - } - r = Cudd_Not(r); - } else { - r = cuddUniqueInter(dd, index, t, Cudd_Not(t)); - if (r == NULL) { - Cudd_IterDerefBdd(dd, t); - return(NULL); + (ue == one || Cudd_bddLeq(dd,Cudd_Not(lt),ue))) { /* c-remap */ + t = cuddBddSqueeze(dd, lt, ut); + cuddRef(t); + if (Cudd_IsComplement(t)) { + r = cuddUniqueInter(dd, index, Cudd_Not(t), t); + if (r == NULL) { + Cudd_IterDerefBdd(dd, t); + return(NULL); + } + r = Cudd_Not(r); + } else { + r = cuddUniqueInter(dd, index, t, Cudd_Not(t)); + if (r == NULL) { + Cudd_IterDerefBdd(dd, t); + return(NULL); + } } - } - cuddDeref(t); - if (r == NULL) - return(NULL); - cuddCacheInsert2(dd, Cudd_bddSqueeze, l, u, r); - return(Cudd_NotCond(r,comple)); + cuddDeref(t); + if (r == NULL) + return(NULL); + cuddCacheInsert2(dd, Cudd_bddSqueeze, l, u, r); + return(Cudd_NotCond(r,comple)); } else if ((lt == zero || Cudd_bddLeq(dd,lt,Cudd_Not(ue))) && - (ut == one || Cudd_bddLeq(dd,Cudd_Not(le),ut))) { /* c-remap */ - e = cuddBddSqueeze(dd, le, ue); - cuddRef(e); - if (Cudd_IsComplement(e)) { - r = cuddUniqueInter(dd, index, Cudd_Not(e), e); - if (r == NULL) { - Cudd_IterDerefBdd(dd, e); - return(NULL); + (ut == one || Cudd_bddLeq(dd,Cudd_Not(le),ut))) { /* c-remap */ + e = cuddBddSqueeze(dd, le, ue); + cuddRef(e); + if (Cudd_IsComplement(e)) { + r = cuddUniqueInter(dd, index, Cudd_Not(e), e); + if (r == NULL) { + Cudd_IterDerefBdd(dd, e); + return(NULL); + } + } else { + r = cuddUniqueInter(dd, index, e, Cudd_Not(e)); + if (r == NULL) { + Cudd_IterDerefBdd(dd, e); + return(NULL); + } + r = Cudd_Not(r); } - } else { - r = cuddUniqueInter(dd, index, e, Cudd_Not(e)); - if (r == NULL) { - Cudd_IterDerefBdd(dd, e); - return(NULL); - } - r = Cudd_Not(r); - } - cuddDeref(e); - if (r == NULL) - return(NULL); - cuddCacheInsert2(dd, Cudd_bddSqueeze, l, u, r); - return(Cudd_NotCond(r,comple)); + cuddDeref(e); + if (r == NULL) + return(NULL); + cuddCacheInsert2(dd, Cudd_bddSqueeze, l, u, r); + return(Cudd_NotCond(r,comple)); } #if 0 @@ -1891,61 +2099,61 @@ cuddBddSqueeze( ** This approach corresponds to two-sided matching, and is very ** expensive. */ if (Cudd_bddLeq(dd,lt,ue) && Cudd_bddLeq(dd,le,ut)) { - DdNode *au, *al; - au = cuddBddAndRecur(dd,ut,ue); - if (au == NULL) - return(NULL); - cuddRef(au); - al = cuddBddAndRecur(dd,Cudd_Not(lt),Cudd_Not(le)); - if (al == NULL) { - Cudd_IterDerefBdd(dd,au); - return(NULL); - } - cuddRef(al); - al = Cudd_Not(al); - ar = cuddBddSqueeze(dd, al, au); - if (ar == NULL) { + DdNode *au, *al; + au = cuddBddAndRecur(dd,ut,ue); + if (au == NULL) + return(NULL); + cuddRef(au); + al = cuddBddAndRecur(dd,Cudd_Not(lt),Cudd_Not(le)); + if (al == NULL) { + Cudd_IterDerefBdd(dd,au); + return(NULL); + } + cuddRef(al); + al = Cudd_Not(al); + ar = cuddBddSqueeze(dd, al, au); + if (ar == NULL) { + Cudd_IterDerefBdd(dd,au); + Cudd_IterDerefBdd(dd,al); + return(NULL); + } + cuddRef(ar); Cudd_IterDerefBdd(dd,au); Cudd_IterDerefBdd(dd,al); - return(NULL); - } - cuddRef(ar); - Cudd_IterDerefBdd(dd,au); - Cudd_IterDerefBdd(dd,al); } else { - ar = NULL; + ar = NULL; } #endif t = cuddBddSqueeze(dd, lt, ut); if (t == NULL) { - return(NULL); + return(NULL); } cuddRef(t); e = cuddBddSqueeze(dd, le, ue); if (e == NULL) { - Cudd_IterDerefBdd(dd,t); - return(NULL); + Cudd_IterDerefBdd(dd,t); + return(NULL); } cuddRef(e); if (Cudd_IsComplement(t)) { - t = Cudd_Not(t); - e = Cudd_Not(e); - r = (t == e) ? t : cuddUniqueInter(dd, index, t, e); - if (r == NULL) { - Cudd_IterDerefBdd(dd, e); - Cudd_IterDerefBdd(dd, t); - return(NULL); - } - r = Cudd_Not(r); + t = Cudd_Not(t); + e = Cudd_Not(e); + r = (t == e) ? t : cuddUniqueInter(dd, index, t, e); + if (r == NULL) { + Cudd_IterDerefBdd(dd, e); + Cudd_IterDerefBdd(dd, t); + return(NULL); + } + r = Cudd_Not(r); } else { - r = (t == e) ? t : cuddUniqueInter(dd, index, t, e); - if (r == NULL) { - Cudd_IterDerefBdd(dd, e); - Cudd_IterDerefBdd(dd, t); - return(NULL); - } + r = (t == e) ? t : cuddUniqueInter(dd, index, t, e); + if (r == NULL) { + Cudd_IterDerefBdd(dd, e); + Cudd_IterDerefBdd(dd, t); + return(NULL); + } } cuddDeref(t); cuddDeref(e); @@ -1955,12 +2163,12 @@ cuddBddSqueeze( ** it is better than the one obtained by recursion. */ cuddRef(r); if (ar != NULL) { - if (Cudd_DagSize(ar) <= Cudd_DagSize(r)) { - Cudd_IterDerefBdd(dd, r); - r = ar; - } else { - Cudd_IterDerefBdd(dd, ar); - } + if (Cudd_DagSize(ar) <= Cudd_DagSize(r)) { + Cudd_IterDerefBdd(dd, r); + r = ar; + } else { + Cudd_IterDerefBdd(dd, ar); + } } cuddDeref(r); #endif @@ -1969,5 +2177,7 @@ cuddBddSqueeze( return(Cudd_NotCond(r,comple)); } /* end of cuddBddSqueeze */ + + ABC_NAMESPACE_IMPL_END |