summaryrefslogtreecommitdiffstats
path: root/src/bdd/cudd/cuddAndAbs.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/bdd/cudd/cuddAndAbs.c')
-rw-r--r--src/bdd/cudd/cuddAndAbs.c271
1 files changed, 151 insertions, 120 deletions
diff --git a/src/bdd/cudd/cuddAndAbs.c b/src/bdd/cudd/cuddAndAbs.c
index 10b057ac..39695918 100644
--- a/src/bdd/cudd/cuddAndAbs.c
+++ b/src/bdd/cudd/cuddAndAbs.c
@@ -7,20 +7,48 @@
Synopsis [Combined AND and existential abstraction for BDDs]
Description [External procedures included in this module:
- <ul>
- <li> Cudd_bddAndAbstract()
- </ul>
- Internal procedures included in this module:
- <ul>
- <li> cuddBddAndAbstractRecur()
- </ul>]
+ <ul>
+ <li> Cudd_bddAndAbstract()
+ <li> Cudd_bddAndAbstractLimit()
+ </ul>
+ Internal procedures included in this module:
+ <ul>
+ <li> cuddBddAndAbstractRecur()
+ </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.]
******************************************************************************/
@@ -31,6 +59,7 @@ ABC_NAMESPACE_IMPL_START
+
/*---------------------------------------------------------------------------*/
/* Constant declarations */
/*---------------------------------------------------------------------------*/
@@ -51,7 +80,7 @@ ABC_NAMESPACE_IMPL_START
/*---------------------------------------------------------------------------*/
#ifndef lint
-static char rcsid[] DD_UNUSED = "$Id: cuddAndAbs.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $";
+static char rcsid[] DD_UNUSED = "$Id: cuddAndAbs.c,v 1.19 2004/08/13 18:04:46 fabio Exp $";
#endif
@@ -101,8 +130,8 @@ Cudd_bddAndAbstract(
DdNode *res;
do {
- manager->reordered = 0;
- res = cuddBddAndAbstractRecur(manager, f, g, cube);
+ manager->reordered = 0;
+ res = cuddBddAndAbstractRecur(manager, f, g, cube);
} while (manager->reordered == 1);
return(res);
@@ -135,10 +164,11 @@ Cudd_bddAndAbstractLimit(
{
DdNode *res;
unsigned int saveLimit = manager->maxLive;
+
+ manager->maxLive = (manager->keys - manager->dead) +
+ (manager->keysZ - manager->deadZ) + limit;
do {
manager->reordered = 0;
- manager->maxLive = (manager->keys - manager->dead) +
- (manager->keysZ - manager->deadZ) + limit;
res = cuddBddAndAbstractRecur(manager, f, g, cube);
} while (manager->reordered == 1);
manager->maxLive = saveLimit;
@@ -147,7 +177,6 @@ Cudd_bddAndAbstractLimit(
} /* end of Cudd_bddAndAbstractLimit */
-
/*---------------------------------------------------------------------------*/
/* Definition of internal functions */
/*---------------------------------------------------------------------------*/
@@ -184,23 +213,23 @@ cuddBddAndAbstractRecur(
/* Terminal cases. */
if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
- if (f == one && g == one) return(one);
+ if (f == one && g == one) return(one);
if (cube == one) {
- return(cuddBddAndRecur(manager, f, g));
+ return(cuddBddAndRecur(manager, f, g));
}
if (f == one || f == g) {
- return(cuddBddExistAbstractRecur(manager, g, cube));
+ return(cuddBddExistAbstractRecur(manager, g, cube));
}
if (g == one) {
- 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;
}
/* Here we can skip the use of cuddI, because the operands are known
@@ -214,129 +243,129 @@ cuddBddAndAbstractRecur(
topcube = manager->perm[cube->index];
while (topcube < top) {
- cube = cuddT(cube);
- if (cube == one) {
- return(cuddBddAndRecur(manager, f, g));
- }
- topcube = manager->perm[cube->index];
+ cube = cuddT(cube);
+ if (cube == one) {
+ return(cuddBddAndRecur(manager, f, g));
+ }
+ topcube = manager->perm[cube->index];
}
/* Now, topcube >= top. */
/* Check cache. */
if (F->ref != 1 || G->ref != 1) {
- r = cuddCacheLookup(manager, DD_BDD_AND_ABSTRACT_TAG, f, g, cube);
- if (r != NULL) {
- return(r);
- }
+ r = cuddCacheLookup(manager, DD_BDD_AND_ABSTRACT_TAG, f, g, cube);
+ if (r != NULL) {
+ return(r);
+ }
}
if (topf == top) {
- index = F->index;
- ft = cuddT(F);
- fe = cuddE(F);
- if (Cudd_IsComplement(f)) {
- ft = Cudd_Not(ft);
- fe = Cudd_Not(fe);
- }
+ index = F->index;
+ ft = cuddT(F);
+ fe = cuddE(F);
+ if (Cudd_IsComplement(f)) {
+ ft = Cudd_Not(ft);
+ fe = Cudd_Not(fe);
+ }
} else {
- index = G->index;
- ft = fe = f;
+ index = G->index;
+ ft = fe = f;
}
if (topg == top) {
- gt = cuddT(G);
- ge = cuddE(G);
- if (Cudd_IsComplement(g)) {
- gt = Cudd_Not(gt);
- ge = Cudd_Not(ge);
- }
+ gt = cuddT(G);
+ ge = cuddE(G);
+ if (Cudd_IsComplement(g)) {
+ gt = Cudd_Not(gt);
+ ge = Cudd_Not(ge);
+ }
} else {
- gt = ge = g;
+ gt = ge = g;
}
- if (topcube == top) { /* quantify */
- DdNode *Cube = cuddT(cube);
- t = cuddBddAndAbstractRecur(manager, ft, gt, Cube);
- if (t == NULL) return(NULL);
- /* Special case: 1 OR anything = 1. Hence, no need to compute
- ** the else branch if t is 1. Likewise t + t * anything == t.
- ** Notice that t == fe implies that fe does not depend on the
- ** variables in Cube. Likewise for t == ge.
- */
- if (t == one || t == fe || t == ge) {
- if (F->ref != 1 || G->ref != 1)
- cuddCacheInsert(manager, DD_BDD_AND_ABSTRACT_TAG,
- f, g, cube, t);
- return(t);
- }
- cuddRef(t);
- /* Special case: t + !t * anything == t + anything. */
- if (t == Cudd_Not(fe)) {
- e = cuddBddExistAbstractRecur(manager, ge, Cube);
- } else if (t == Cudd_Not(ge)) {
- e = cuddBddExistAbstractRecur(manager, fe, Cube);
- } else {
- e = cuddBddAndAbstractRecur(manager, fe, ge, Cube);
- }
- if (e == NULL) {
- Cudd_IterDerefBdd(manager, t);
- return(NULL);
- }
- if (t == e) {
- r = t;
- cuddDeref(t);
- } else {
- cuddRef(e);
- r = cuddBddAndRecur(manager, Cudd_Not(t), Cudd_Not(e));
- if (r == NULL) {
- Cudd_IterDerefBdd(manager, t);
- Cudd_IterDerefBdd(manager, e);
- return(NULL);
+ if (topcube == top) { /* quantify */
+ DdNode *Cube = cuddT(cube);
+ t = cuddBddAndAbstractRecur(manager, ft, gt, Cube);
+ if (t == NULL) return(NULL);
+ /* Special case: 1 OR anything = 1. Hence, no need to compute
+ ** the else branch if t is 1. Likewise t + t * anything == t.
+ ** Notice that t == fe implies that fe does not depend on the
+ ** variables in Cube. Likewise for t == ge.
+ */
+ if (t == one || t == fe || t == ge) {
+ if (F->ref != 1 || G->ref != 1)
+ cuddCacheInsert(manager, DD_BDD_AND_ABSTRACT_TAG,
+ f, g, cube, t);
+ return(t);
}
- r = Cudd_Not(r);
- cuddRef(r);
- Cudd_DelayedDerefBdd(manager, t);
- Cudd_DelayedDerefBdd(manager, e);
- cuddDeref(r);
- }
- } else {
- t = cuddBddAndAbstractRecur(manager, ft, gt, cube);
- if (t == NULL) return(NULL);
- cuddRef(t);
- e = cuddBddAndAbstractRecur(manager, fe, ge, cube);
- if (e == NULL) {
- Cudd_IterDerefBdd(manager, t);
- return(NULL);
- }
- if (t == e) {
- r = t;
- cuddDeref(t);
- } else {
- cuddRef(e);
- if (Cudd_IsComplement(t)) {
- r = cuddUniqueInter(manager, (int) index,
- Cudd_Not(t), Cudd_Not(e));
- if (r == NULL) {
+ cuddRef(t);
+ /* Special case: t + !t * anything == t + anything. */
+ if (t == Cudd_Not(fe)) {
+ e = cuddBddExistAbstractRecur(manager, ge, Cube);
+ } else if (t == Cudd_Not(ge)) {
+ e = cuddBddExistAbstractRecur(manager, fe, Cube);
+ } else {
+ e = cuddBddAndAbstractRecur(manager, fe, ge, Cube);
+ }
+ if (e == NULL) {
Cudd_IterDerefBdd(manager, t);
- Cudd_IterDerefBdd(manager, e);
return(NULL);
}
- r = Cudd_Not(r);
+ if (t == e) {
+ r = t;
+ cuddDeref(t);
} else {
- r = cuddUniqueInter(manager,(int)index,t,e);
- if (r == NULL) {
+ cuddRef(e);
+ 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_DelayedDerefBdd(manager, t);
+ Cudd_DelayedDerefBdd(manager, e);
+ cuddDeref(r);
+ }
+ } else {
+ t = cuddBddAndAbstractRecur(manager, ft, gt, cube);
+ if (t == NULL) return(NULL);
+ cuddRef(t);
+ e = cuddBddAndAbstractRecur(manager, fe, ge, cube);
+ if (e == NULL) {
Cudd_IterDerefBdd(manager, t);
- Cudd_IterDerefBdd(manager, e);
return(NULL);
}
+ if (t == e) {
+ r = t;
+ cuddDeref(t);
+ } else {
+ cuddRef(e);
+ 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);
- }
}
if (F->ref != 1 || G->ref != 1)
- cuddCacheInsert(manager, DD_BDD_AND_ABSTRACT_TAG, f, g, cube, r);
+ cuddCacheInsert(manager, DD_BDD_AND_ABSTRACT_TAG, f, g, cube, r);
return (r);
} /* end of cuddBddAndAbstractRecur */
@@ -346,5 +375,7 @@ cuddBddAndAbstractRecur(
/* Definition of static functions */
/*---------------------------------------------------------------------------*/
+
ABC_NAMESPACE_IMPL_END
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-18 07:45:14 +0000