diff options
Diffstat (limited to 'src/bdd/cudd/cuddBddAbs.c')
| -rw-r--r-- | src/bdd/cudd/cuddBddAbs.c | 379 |
1 files changed, 204 insertions, 175 deletions
diff --git a/src/bdd/cudd/cuddBddAbs.c b/src/bdd/cudd/cuddBddAbs.c index 80d24ca4..a3892af1 100644 --- a/src/bdd/cudd/cuddBddAbs.c +++ b/src/bdd/cudd/cuddBddAbs.c @@ -7,31 +7,58 @@ Synopsis [Quantification functions for BDDs.] Description [External procedures included in this module: - <ul> - <li> Cudd_bddExistAbstract() - <li> Cudd_bddXorExistAbstract() - <li> Cudd_bddUnivAbstract() - <li> Cudd_bddBooleanDiff() - <li> Cudd_bddVarIsDependent() - </ul> - Internal procedures included in this module: - <ul> - <li> cuddBddExistAbstractRecur() - <li> cuddBddXorExistAbstractRecur() - <li> cuddBddBooleanDiffRecur() - </ul> - Static procedures included in this module: - <ul> - <li> bddCheckPositiveCube() - </ul> - ] + <ul> + <li> Cudd_bddExistAbstract() + <li> Cudd_bddXorExistAbstract() + <li> Cudd_bddUnivAbstract() + <li> Cudd_bddBooleanDiff() + <li> Cudd_bddVarIsDependent() + </ul> + Internal procedures included in this module: + <ul> + <li> cuddBddExistAbstractRecur() + <li> cuddBddXorExistAbstractRecur() + <li> cuddBddBooleanDiffRecur() + </ul> + Static procedures included in this module: + <ul> + <li> bddCheckPositiveCube() + </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.] ******************************************************************************/ @@ -42,6 +69,7 @@ ABC_NAMESPACE_IMPL_START + /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ @@ -62,7 +90,7 @@ ABC_NAMESPACE_IMPL_START /*---------------------------------------------------------------------------*/ #ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddBddAbs.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $"; +static char rcsid[] DD_UNUSED = "$Id: cuddBddAbs.c,v 1.26 2004/08/13 18:04:46 fabio Exp $"; #endif /*---------------------------------------------------------------------------*/ @@ -76,7 +104,7 @@ static char rcsid[] DD_UNUSED = "$Id: cuddBddAbs.c,v 1.1.1.1 2003/02/24 22:23:51 /* Static function prototypes */ /*---------------------------------------------------------------------------*/ -static int bddCheckPositiveCube ARGS((DdManager *manager, DdNode *cube)); +static int bddCheckPositiveCube (DdManager *manager, DdNode *cube); /**AutomaticEnd***************************************************************/ @@ -108,14 +136,14 @@ Cudd_bddExistAbstract( if (bddCheckPositiveCube(manager, cube) == 0) { (void) fprintf(manager->err, - "Error: Can only abstract positive cubes\n"); - manager->errorCode = CUDD_INVALID_ARG; + "Error: Can only abstract positive cubes\n"); + manager->errorCode = CUDD_INVALID_ARG; return(NULL); } do { - manager->reordered = 0; - res = cuddBddExistAbstractRecur(manager, f, cube); + manager->reordered = 0; + res = cuddBddExistAbstractRecur(manager, f, cube); } while (manager->reordered == 1); return(res); @@ -148,14 +176,14 @@ Cudd_bddXorExistAbstract( if (bddCheckPositiveCube(manager, cube) == 0) { (void) fprintf(manager->err, - "Error: Can only abstract positive cubes\n"); - manager->errorCode = CUDD_INVALID_ARG; + "Error: Can only abstract positive cubes\n"); + manager->errorCode = CUDD_INVALID_ARG; return(NULL); } do { - manager->reordered = 0; - res = cuddBddXorExistAbstractRecur(manager, f, g, cube); + manager->reordered = 0; + res = cuddBddXorExistAbstractRecur(manager, f, g, cube); } while (manager->reordered == 1); return(res); @@ -181,18 +209,18 @@ Cudd_bddUnivAbstract( DdNode * f, DdNode * cube) { - DdNode *res; + DdNode *res; if (bddCheckPositiveCube(manager, cube) == 0) { - (void) fprintf(manager->err, - "Error: Can only abstract positive cubes\n"); - manager->errorCode = CUDD_INVALID_ARG; - return(NULL); + (void) fprintf(manager->err, + "Error: Can only abstract positive cubes\n"); + manager->errorCode = CUDD_INVALID_ARG; + return(NULL); } do { - manager->reordered = 0; - res = cuddBddExistAbstractRecur(manager, Cudd_Not(f), cube); + manager->reordered = 0; + res = cuddBddExistAbstractRecur(manager, Cudd_Not(f), cube); } while (manager->reordered == 1); if (res != NULL) res = Cudd_Not(res); @@ -229,8 +257,8 @@ Cudd_bddBooleanDiff( var = manager->vars[x]; do { - manager->reordered = 0; - res = cuddBddBooleanDiffRecur(manager, Cudd_Regular(f), var); + manager->reordered = 0; + res = cuddBddBooleanDiffRecur(manager, Cudd_Regular(f), var); } while (manager->reordered == 1); return(res); @@ -254,13 +282,13 @@ Cudd_bddBooleanDiff( ******************************************************************************/ int Cudd_bddVarIsDependent( - DdManager *dd, /* manager */ - DdNode *f, /* function */ - DdNode *var /* variable */) + DdManager *dd, /* manager */ + DdNode *f, /* function */ + DdNode *var /* variable */) { DdNode *F, *res, *zero, *ft, *fe; unsigned topf, level; - DdNode *(*cacheOp)(DdManager *, DdNode *, DdNode *); + DD_CTFP cacheOp; int retval; zero = Cudd_Not(DD_ONE(dd)); @@ -274,14 +302,13 @@ Cudd_bddVarIsDependent( /* Check terminal case. If topf > index of var, f does not depend on var. ** Therefore, var is not dependent in f. */ if (topf > level) { - return(0); + return(0); } - cacheOp = - (DdNode *(*)(DdManager *, DdNode *, DdNode *)) Cudd_bddVarIsDependent; + cacheOp = (DD_CTFP) Cudd_bddVarIsDependent; res = cuddCacheLookup2(dd,cacheOp,f,var); if (res != NULL) { - return(res != zero); + return(res != zero); } /* Compute cofactors. */ @@ -289,10 +316,10 @@ Cudd_bddVarIsDependent( fe = Cudd_NotCond(cuddE(F), f != F); if (topf == level) { - retval = Cudd_bddLeq(dd,ft,Cudd_Not(fe)); + retval = Cudd_bddLeq(dd,ft,Cudd_Not(fe)); } else { - retval = Cudd_bddVarIsDependent(dd,ft,var) && - Cudd_bddVarIsDependent(dd,fe,var); + retval = Cudd_bddVarIsDependent(dd,ft,var) && + Cudd_bddVarIsDependent(dd,fe,var); } cuddCacheInsert2(dd,cacheOp,f,var,Cudd_NotCond(zero,retval)); @@ -327,13 +354,13 @@ cuddBddExistAbstractRecur( DdNode * f, DdNode * cube) { - DdNode *F, *T, *E, *res, *res1, *res2, *one; + DdNode *F, *T, *E, *res, *res1, *res2, *one; statLine(manager); one = DD_ONE(manager); F = Cudd_Regular(f); - /* Cube is guaranteed to be a cube at this point. */ + /* Cube is guaranteed to be a cube at this point. */ if (cube == one || F == one) { return(f); } @@ -341,78 +368,78 @@ cuddBddExistAbstractRecur( /* Abstract a variable that does not appear in f. */ while (manager->perm[F->index] > manager->perm[cube->index]) { - cube = cuddT(cube); - if (cube == one) return(f); + cube = cuddT(cube); + if (cube == one) return(f); } /* Check the cache. */ if (F->ref != 1 && (res = cuddCacheLookup2(manager, Cudd_bddExistAbstract, f, cube)) != NULL) { - return(res); + return(res); } /* Compute the cofactors of f. */ T = cuddT(F); E = cuddE(F); if (f != F) { - T = Cudd_Not(T); E = Cudd_Not(E); + T = Cudd_Not(T); E = Cudd_Not(E); } /* If the two indices are the same, so are their levels. */ if (F->index == cube->index) { - if (T == one || E == one || T == Cudd_Not(E)) { - return(one); - } - res1 = cuddBddExistAbstractRecur(manager, T, cuddT(cube)); - if (res1 == NULL) return(NULL); - if (res1 == one) { - if (F->ref != 1) - cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, one); - return(one); - } + if (T == one || E == one || T == Cudd_Not(E)) { + return(one); + } + res1 = cuddBddExistAbstractRecur(manager, T, cuddT(cube)); + if (res1 == NULL) return(NULL); + if (res1 == one) { + if (F->ref != 1) + cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, one); + return(one); + } cuddRef(res1); - res2 = cuddBddExistAbstractRecur(manager, E, cuddT(cube)); - if (res2 == NULL) { - Cudd_IterDerefBdd(manager,res1); - return(NULL); - } + res2 = cuddBddExistAbstractRecur(manager, E, cuddT(cube)); + if (res2 == NULL) { + Cudd_IterDerefBdd(manager,res1); + return(NULL); + } cuddRef(res2); - res = cuddBddAndRecur(manager, Cudd_Not(res1), Cudd_Not(res2)); - if (res == NULL) { + res = cuddBddAndRecur(manager, Cudd_Not(res1), Cudd_Not(res2)); + if (res == NULL) { + Cudd_IterDerefBdd(manager, res1); + Cudd_IterDerefBdd(manager, res2); + return(NULL); + } + res = Cudd_Not(res); + cuddRef(res); Cudd_IterDerefBdd(manager, res1); Cudd_IterDerefBdd(manager, res2); - return(NULL); - } - res = Cudd_Not(res); - cuddRef(res); - Cudd_IterDerefBdd(manager, res1); - Cudd_IterDerefBdd(manager, res2); - if (F->ref != 1) - cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, res); - cuddDeref(res); + if (F->ref != 1) + cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, res); + cuddDeref(res); return(res); } else { /* if (cuddI(manager,F->index) < cuddI(manager,cube->index)) */ - res1 = cuddBddExistAbstractRecur(manager, T, cube); - if (res1 == NULL) return(NULL); + res1 = cuddBddExistAbstractRecur(manager, T, cube); + if (res1 == NULL) return(NULL); cuddRef(res1); - res2 = cuddBddExistAbstractRecur(manager, E, cube); - if (res2 == NULL) { - Cudd_IterDerefBdd(manager, res1); - return(NULL); - } + res2 = cuddBddExistAbstractRecur(manager, E, cube); + if (res2 == NULL) { + Cudd_IterDerefBdd(manager, res1); + return(NULL); + } cuddRef(res2); - /* ITE takes care of possible complementation of res1 and of the + /* ITE takes care of possible complementation of res1 and of the ** case in which res1 == res2. */ - res = cuddBddIteRecur(manager, manager->vars[F->index], res1, res2); - if (res == NULL) { - Cudd_IterDerefBdd(manager, res1); - Cudd_IterDerefBdd(manager, res2); - return(NULL); - } - cuddDeref(res1); - cuddDeref(res2); - if (F->ref != 1) - cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, res); + res = cuddBddIteRecur(manager, manager->vars[F->index], res1, res2); + if (res == NULL) { + Cudd_IterDerefBdd(manager, res1); + Cudd_IterDerefBdd(manager, res2); + return(NULL); + } + cuddDeref(res1); + cuddDeref(res2); + if (F->ref != 1) + cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, res); return(res); - } + } } /* end of cuddBddExistAbstractRecur */ @@ -448,39 +475,39 @@ cuddBddXorExistAbstractRecur( /* Terminal cases. */ if (f == g) { - return(zero); + return(zero); } if (f == Cudd_Not(g)) { - return(one); + return(one); } if (cube == one) { - return(cuddBddXorRecur(manager, f, g)); + return(cuddBddXorRecur(manager, f, g)); } if (f == one) { - return(cuddBddExistAbstractRecur(manager, Cudd_Not(g), cube)); + return(cuddBddExistAbstractRecur(manager, Cudd_Not(g), cube)); } if (g == one) { - return(cuddBddExistAbstractRecur(manager, Cudd_Not(f), cube)); + return(cuddBddExistAbstractRecur(manager, Cudd_Not(f), cube)); } if (f == zero) { - return(cuddBddExistAbstractRecur(manager, g, cube)); + return(cuddBddExistAbstractRecur(manager, g, cube)); } if (g == zero) { - return(cuddBddExistAbstractRecur(manager, f, cube)); + return(cuddBddExistAbstractRecur(manager, f, cube)); } /* At this point f, g, and cube are not constant. */ if (f > g) { /* Try to increase cache efficiency. */ - DdNode *tmp = f; - f = g; - g = tmp; + DdNode *tmp = f; + f = g; + g = tmp; } /* Check cache. */ r = cuddCacheLookup(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube); if (r != NULL) { - return(r); + return(r); } /* Here we can skip the use of cuddI, because the operands are known @@ -494,38 +521,38 @@ cuddBddXorExistAbstractRecur( topcube = manager->perm[cube->index]; if (topcube < top) { - return(cuddBddXorExistAbstractRecur(manager, f, g, cuddT(cube))); + return(cuddBddXorExistAbstractRecur(manager, f, g, cuddT(cube))); } /* Now, topcube >= top. */ if (topf == top) { - index = F->index; - fv = cuddT(F); - fnv = cuddE(F); - if (Cudd_IsComplement(f)) { - fv = Cudd_Not(fv); - fnv = Cudd_Not(fnv); - } + index = F->index; + fv = cuddT(F); + fnv = cuddE(F); + if (Cudd_IsComplement(f)) { + fv = Cudd_Not(fv); + fnv = Cudd_Not(fnv); + } } else { - index = G->index; - fv = fnv = f; + index = G->index; + fv = fnv = f; } if (topg == top) { - gv = cuddT(G); - gnv = cuddE(G); - if (Cudd_IsComplement(g)) { - gv = Cudd_Not(gv); - gnv = Cudd_Not(gnv); - } + gv = cuddT(G); + gnv = cuddE(G); + if (Cudd_IsComplement(g)) { + gv = Cudd_Not(gv); + gnv = Cudd_Not(gnv); + } } else { - gv = gnv = g; + gv = gnv = g; } if (topcube == top) { - Cube = cuddT(cube); + Cube = cuddT(cube); } else { - Cube = cube; + Cube = cube; } t = cuddBddXorExistAbstractRecur(manager, fv, gv, Cube); @@ -535,53 +562,53 @@ cuddBddXorExistAbstractRecur( ** the else branch if t is 1. */ if (t == one && topcube == top) { - cuddCacheInsert(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube, one); - return(one); + cuddCacheInsert(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube, one); + return(one); } cuddRef(t); e = cuddBddXorExistAbstractRecur(manager, fnv, gnv, Cube); if (e == NULL) { - Cudd_IterDerefBdd(manager, t); - return(NULL); - } - cuddRef(e); - - if (topcube == top) { /* abstract */ - r = cuddBddAndRecur(manager, Cudd_Not(t), Cudd_Not(e)); - if (r == NULL) { Cudd_IterDerefBdd(manager, t); - Cudd_IterDerefBdd(manager, e); return(NULL); } - r = Cudd_Not(r); - cuddRef(r); - Cudd_IterDerefBdd(manager, t); - Cudd_IterDerefBdd(manager, e); - cuddDeref(r); - } else if (t == e) { - r = t; - cuddDeref(t); - cuddDeref(e); - } else { - if (Cudd_IsComplement(t)) { - r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e)); + cuddRef(e); + + if (topcube == top) { /* abstract */ + r = cuddBddAndRecur(manager, Cudd_Not(t), Cudd_Not(e)); if (r == NULL) { - Cudd_IterDerefBdd(manager, t); - Cudd_IterDerefBdd(manager, e); - return(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) { + cuddRef(r); Cudd_IterDerefBdd(manager, t); Cudd_IterDerefBdd(manager, e); - return(NULL); + cuddDeref(r); + } else if (t == e) { + r = t; + cuddDeref(t); + cuddDeref(e); + } 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); + cuddDeref(e); + cuddDeref(t); } cuddCacheInsert(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube, r); return (r); @@ -613,15 +640,15 @@ cuddBddBooleanDiffRecur( statLine(manager); if (cuddI(manager,f->index) > manager->perm[var->index]) { - /* f does not depend on var. */ - return(Cudd_Not(DD_ONE(manager))); + /* f does not depend on var. */ + return(Cudd_Not(DD_ONE(manager))); } /* From now on, f is non-constant. */ /* If the two indices are the same, so are their levels. */ if (f->index == var->index) { - res = cuddBddXorRecur(manager, cuddT(f), cuddE(f)); + res = cuddBddXorRecur(manager, cuddT(f), cuddE(f)); return(res); } @@ -630,7 +657,7 @@ cuddBddBooleanDiffRecur( /* Check the cache. */ res = cuddCacheLookup2(manager, cuddBddBooleanDiffRecur, f, var); if (res != NULL) { - return(res); + return(res); } /* Compute the cofactors of f. */ @@ -641,17 +668,17 @@ cuddBddBooleanDiffRecur( cuddRef(res1); res2 = cuddBddBooleanDiffRecur(manager, Cudd_Regular(E), var); if (res2 == NULL) { - Cudd_IterDerefBdd(manager, res1); - return(NULL); + Cudd_IterDerefBdd(manager, res1); + return(NULL); } cuddRef(res2); /* ITE takes care of possible complementation of res1 and of the ** case in which res1 == res2. */ res = cuddBddIteRecur(manager, manager->vars[f->index], res1, res2); if (res == NULL) { - Cudd_IterDerefBdd(manager, res1); - Cudd_IterDerefBdd(manager, res2); - return(NULL); + Cudd_IterDerefBdd(manager, res1); + Cudd_IterDerefBdd(manager, res2); + return(NULL); } cuddDeref(res1); cuddDeref(res2); @@ -690,5 +717,7 @@ bddCheckPositiveCube( } /* end of bddCheckPositiveCube */ + ABC_NAMESPACE_IMPL_END + |