diff options
Diffstat (limited to 'src/bdd/cudd/cuddAndAbs.c')
-rw-r--r-- | src/bdd/cudd/cuddAndAbs.c | 271 |
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 + |