diff options
Diffstat (limited to 'src/bdd/cudd/cuddAddAbs.c')
| -rw-r--r-- | src/bdd/cudd/cuddAddAbs.c | 407 |
1 files changed, 212 insertions, 195 deletions
diff --git a/src/bdd/cudd/cuddAddAbs.c b/src/bdd/cudd/cuddAddAbs.c index 40d3222b..f420f99e 100644 --- a/src/bdd/cudd/cuddAddAbs.c +++ b/src/bdd/cudd/cuddAddAbs.c @@ -7,37 +7,65 @@ Synopsis [Quantification functions for ADDs.] Description [External procedures included in this module: - <ul> - <li> Cudd_addExistAbstract() - <li> Cudd_addUnivAbstract() - <li> Cudd_addOrAbstract() - </ul> - Internal procedures included in this module: - <ul> - <li> cuddAddExistAbstractRecur() - <li> cuddAddUnivAbstractRecur() - <li> cuddAddOrAbstractRecur() - </ul> - Static procedures included in this module: - <ul> - <li> addCheckPositiveCube() - </ul>] + <ul> + <li> Cudd_addExistAbstract() + <li> Cudd_addUnivAbstract() + <li> Cudd_addOrAbstract() + </ul> + Internal procedures included in this module: + <ul> + <li> cuddAddExistAbstractRecur() + <li> cuddAddUnivAbstractRecur() + <li> cuddAddOrAbstractRecur() + </ul> + Static procedures included in this module: + <ul> + <li> addCheckPositiveCube() + </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.] ******************************************************************************/ -#include "util_hack.h" -#include "cuddInt.h" +#include "util_hack.h" +#include "cuddInt.h" ABC_NAMESPACE_IMPL_START + /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ @@ -58,10 +86,10 @@ ABC_NAMESPACE_IMPL_START /*---------------------------------------------------------------------------*/ #ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddAddAbs.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $"; +static char rcsid[] DD_UNUSED = "$Id: cuddAddAbs.c,v 1.15 2004/08/13 18:04:45 fabio Exp $"; #endif -static DdNode *two; +static DdNode *two; /*---------------------------------------------------------------------------*/ /* Macro declarations */ @@ -74,7 +102,7 @@ static DdNode *two; /* Static function prototypes */ /*---------------------------------------------------------------------------*/ -static int addCheckPositiveCube ARGS((DdManager *manager, DdNode *cube)); +static int addCheckPositiveCube (DdManager *manager, DdNode *cube); /**AutomaticEnd***************************************************************/ @@ -115,13 +143,13 @@ Cudd_addExistAbstract( } do { - manager->reordered = 0; - res = cuddAddExistAbstractRecur(manager, f, cube); + manager->reordered = 0; + res = cuddAddExistAbstractRecur(manager, f, cube); } while (manager->reordered == 1); if (res == NULL) { - Cudd_RecursiveDeref(manager,two); - return(NULL); + Cudd_RecursiveDeref(manager,two); + return(NULL); } cuddRef(res); Cudd_RecursiveDeref(manager,two); @@ -152,16 +180,16 @@ Cudd_addUnivAbstract( DdNode * f, DdNode * cube) { - DdNode *res; + DdNode *res; if (addCheckPositiveCube(manager, cube) == 0) { - (void) fprintf(manager->err,"Error: Can only abstract cubes"); - return(NULL); + (void) fprintf(manager->err,"Error: Can only abstract cubes"); + return(NULL); } do { - manager->reordered = 0; - res = cuddAddUnivAbstractRecur(manager, f, cube); + manager->reordered = 0; + res = cuddAddUnivAbstractRecur(manager, f, cube); } while (manager->reordered == 1); return(res); @@ -198,8 +226,8 @@ Cudd_addOrAbstract( } do { - manager->reordered = 0; - res = cuddAddOrAbstractRecur(manager, f, cube); + manager->reordered = 0; + res = cuddAddOrAbstractRecur(manager, f, cube); } while (manager->reordered == 1); return(res); @@ -230,38 +258,38 @@ cuddAddExistAbstractRecur( DdNode * f, DdNode * cube) { - DdNode *T, *E, *res, *res1, *res2, *zero; + DdNode *T, *E, *res, *res1, *res2, *zero; statLine(manager); zero = DD_ZERO(manager); - /* Cube is guaranteed to be a cube at this point. */ + /* Cube is guaranteed to be a cube at this point. */ if (f == zero || cuddIsConstant(cube)) { return(f); } /* Abstract a variable that does not appear in f => multiply by 2. */ if (cuddI(manager,f->index) > cuddI(manager,cube->index)) { - res1 = cuddAddExistAbstractRecur(manager, f, cuddT(cube)); - if (res1 == NULL) return(NULL); - cuddRef(res1); - /* Use the "internal" procedure to be alerted in case of - ** dynamic reordering. If dynamic reordering occurs, we - ** have to abort the entire abstraction. - */ - res = cuddAddApplyRecur(manager,Cudd_addTimes,res1,two); - if (res == NULL) { + res1 = cuddAddExistAbstractRecur(manager, f, cuddT(cube)); + if (res1 == NULL) return(NULL); + cuddRef(res1); + /* Use the "internal" procedure to be alerted in case of + ** dynamic reordering. If dynamic reordering occurs, we + ** have to abort the entire abstraction. + */ + res = cuddAddApplyRecur(manager,Cudd_addTimes,res1,two); + if (res == NULL) { + Cudd_RecursiveDeref(manager,res1); + return(NULL); + } + cuddRef(res); Cudd_RecursiveDeref(manager,res1); - return(NULL); - } - cuddRef(res); - Cudd_RecursiveDeref(manager,res1); - cuddDeref(res); + cuddDeref(res); return(res); } if ((res = cuddCacheLookup2(manager, Cudd_addExistAbstract, f, cube)) != NULL) { - return(res); + return(res); } T = cuddT(f); @@ -269,49 +297,49 @@ cuddAddExistAbstractRecur( /* If the two indices are the same, so are their levels. */ if (f->index == cube->index) { - res1 = cuddAddExistAbstractRecur(manager, T, cuddT(cube)); - if (res1 == NULL) return(NULL); + res1 = cuddAddExistAbstractRecur(manager, T, cuddT(cube)); + if (res1 == NULL) return(NULL); cuddRef(res1); - res2 = cuddAddExistAbstractRecur(manager, E, cuddT(cube)); - if (res2 == NULL) { - Cudd_RecursiveDeref(manager,res1); - return(NULL); - } + res2 = cuddAddExistAbstractRecur(manager, E, cuddT(cube)); + if (res2 == NULL) { + Cudd_RecursiveDeref(manager,res1); + return(NULL); + } cuddRef(res2); - res = cuddAddApplyRecur(manager, Cudd_addPlus, res1, res2); - if (res == NULL) { + res = cuddAddApplyRecur(manager, Cudd_addPlus, res1, res2); + if (res == NULL) { + Cudd_RecursiveDeref(manager,res1); + Cudd_RecursiveDeref(manager,res2); + return(NULL); + } + cuddRef(res); Cudd_RecursiveDeref(manager,res1); Cudd_RecursiveDeref(manager,res2); - return(NULL); - } - cuddRef(res); - Cudd_RecursiveDeref(manager,res1); - Cudd_RecursiveDeref(manager,res2); - cuddCacheInsert2(manager, Cudd_addExistAbstract, f, cube, res); - cuddDeref(res); + cuddCacheInsert2(manager, Cudd_addExistAbstract, f, cube, res); + cuddDeref(res); return(res); } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */ - res1 = cuddAddExistAbstractRecur(manager, T, cube); - if (res1 == NULL) return(NULL); + res1 = cuddAddExistAbstractRecur(manager, T, cube); + if (res1 == NULL) return(NULL); cuddRef(res1); - res2 = cuddAddExistAbstractRecur(manager, E, cube); - if (res2 == NULL) { - Cudd_RecursiveDeref(manager,res1); - return(NULL); - } + res2 = cuddAddExistAbstractRecur(manager, E, cube); + if (res2 == NULL) { + Cudd_RecursiveDeref(manager,res1); + return(NULL); + } cuddRef(res2); - res = (res1 == res2) ? res1 : - cuddUniqueInter(manager, (int) f->index, res1, res2); - if (res == NULL) { - Cudd_RecursiveDeref(manager,res1); - Cudd_RecursiveDeref(manager,res2); - return(NULL); - } - cuddDeref(res1); - cuddDeref(res2); - cuddCacheInsert2(manager, Cudd_addExistAbstract, f, cube, res); + res = (res1 == res2) ? res1 : + cuddUniqueInter(manager, (int) f->index, res1, res2); + if (res == NULL) { + Cudd_RecursiveDeref(manager,res1); + Cudd_RecursiveDeref(manager,res2); + return(NULL); + } + cuddDeref(res1); + cuddDeref(res2); + cuddCacheInsert2(manager, Cudd_addExistAbstract, f, cube, res); return(res); - } + } } /* end of cuddAddExistAbstractRecur */ @@ -335,7 +363,7 @@ cuddAddUnivAbstractRecur( DdNode * f, DdNode * cube) { - DdNode *T, *E, *res, *res1, *res2, *one, *zero; + DdNode *T, *E, *res, *res1, *res2, *one, *zero; statLine(manager); one = DD_ONE(manager); @@ -345,31 +373,31 @@ cuddAddUnivAbstractRecur( ** zero and one are the only constatnts c such that c*c=c. */ if (f == zero || f == one || cube == one) { - return(f); + return(f); } /* Abstract a variable that does not appear in f. */ if (cuddI(manager,f->index) > cuddI(manager,cube->index)) { - res1 = cuddAddUnivAbstractRecur(manager, f, cuddT(cube)); - if (res1 == NULL) return(NULL); - cuddRef(res1); - /* Use the "internal" procedure to be alerted in case of - ** dynamic reordering. If dynamic reordering occurs, we - ** have to abort the entire abstraction. - */ - res = cuddAddApplyRecur(manager, Cudd_addTimes, res1, res1); - if (res == NULL) { + res1 = cuddAddUnivAbstractRecur(manager, f, cuddT(cube)); + if (res1 == NULL) return(NULL); + cuddRef(res1); + /* Use the "internal" procedure to be alerted in case of + ** dynamic reordering. If dynamic reordering occurs, we + ** have to abort the entire abstraction. + */ + res = cuddAddApplyRecur(manager, Cudd_addTimes, res1, res1); + if (res == NULL) { + Cudd_RecursiveDeref(manager,res1); + return(NULL); + } + cuddRef(res); Cudd_RecursiveDeref(manager,res1); - return(NULL); - } - cuddRef(res); - Cudd_RecursiveDeref(manager,res1); - cuddDeref(res); - return(res); + cuddDeref(res); + return(res); } if ((res = cuddCacheLookup2(manager, Cudd_addUnivAbstract, f, cube)) != NULL) { - return(res); + return(res); } T = cuddT(f); @@ -377,47 +405,47 @@ cuddAddUnivAbstractRecur( /* If the two indices are the same, so are their levels. */ if (f->index == cube->index) { - res1 = cuddAddUnivAbstractRecur(manager, T, cuddT(cube)); - if (res1 == NULL) return(NULL); + res1 = cuddAddUnivAbstractRecur(manager, T, cuddT(cube)); + if (res1 == NULL) return(NULL); cuddRef(res1); - res2 = cuddAddUnivAbstractRecur(manager, E, cuddT(cube)); - if (res2 == NULL) { - Cudd_RecursiveDeref(manager,res1); - return(NULL); - } + res2 = cuddAddUnivAbstractRecur(manager, E, cuddT(cube)); + if (res2 == NULL) { + Cudd_RecursiveDeref(manager,res1); + return(NULL); + } cuddRef(res2); - res = cuddAddApplyRecur(manager, Cudd_addTimes, res1, res2); - if (res == NULL) { + res = cuddAddApplyRecur(manager, Cudd_addTimes, res1, res2); + if (res == NULL) { + Cudd_RecursiveDeref(manager,res1); + Cudd_RecursiveDeref(manager,res2); + return(NULL); + } + cuddRef(res); Cudd_RecursiveDeref(manager,res1); Cudd_RecursiveDeref(manager,res2); - return(NULL); - } - cuddRef(res); - Cudd_RecursiveDeref(manager,res1); - Cudd_RecursiveDeref(manager,res2); - cuddCacheInsert2(manager, Cudd_addUnivAbstract, f, cube, res); - cuddDeref(res); + cuddCacheInsert2(manager, Cudd_addUnivAbstract, f, cube, res); + cuddDeref(res); return(res); } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */ - res1 = cuddAddUnivAbstractRecur(manager, T, cube); - if (res1 == NULL) return(NULL); + res1 = cuddAddUnivAbstractRecur(manager, T, cube); + if (res1 == NULL) return(NULL); cuddRef(res1); - res2 = cuddAddUnivAbstractRecur(manager, E, cube); - if (res2 == NULL) { - Cudd_RecursiveDeref(manager,res1); - return(NULL); - } + res2 = cuddAddUnivAbstractRecur(manager, E, cube); + if (res2 == NULL) { + Cudd_RecursiveDeref(manager,res1); + return(NULL); + } cuddRef(res2); - res = (res1 == res2) ? res1 : - cuddUniqueInter(manager, (int) f->index, res1, res2); - if (res == NULL) { - Cudd_RecursiveDeref(manager,res1); - Cudd_RecursiveDeref(manager,res2); - return(NULL); - } - cuddDeref(res1); - cuddDeref(res2); - cuddCacheInsert2(manager, Cudd_addUnivAbstract, f, cube, res); + res = (res1 == res2) ? res1 : + cuddUniqueInter(manager, (int) f->index, res1, res2); + if (res == NULL) { + Cudd_RecursiveDeref(manager,res1); + Cudd_RecursiveDeref(manager,res2); + return(NULL); + } + cuddDeref(res1); + cuddDeref(res2); + cuddCacheInsert2(manager, Cudd_addUnivAbstract, f, cube, res); return(res); } @@ -443,38 +471,24 @@ cuddAddOrAbstractRecur( DdNode * f, DdNode * cube) { - DdNode *T, *E, *res, *res1, *res2, *one; + DdNode *T, *E, *res, *res1, *res2, *one; statLine(manager); one = DD_ONE(manager); /* Cube is guaranteed to be a cube at this point. */ if (cuddIsConstant(f) || cube == one) { - return(f); + return(f); } /* Abstract a variable that does not appear in f. */ if (cuddI(manager,f->index) > cuddI(manager,cube->index)) { - res1 = cuddAddOrAbstractRecur(manager, f, cuddT(cube)); - if (res1 == NULL) return(NULL); - cuddRef(res1); - /* Use the "internal" procedure to be alerted in case of - ** dynamic reordering. If dynamic reordering occurs, we - ** have to abort the entire abstraction. - */ - res = cuddAddApplyRecur(manager, Cudd_addOr, res1, res1); - if (res == NULL) { - Cudd_RecursiveDeref(manager,res1); - return(NULL); - } - cuddRef(res); - Cudd_RecursiveDeref(manager,res1); - cuddDeref(res); - return(res); + res = cuddAddOrAbstractRecur(manager, f, cuddT(cube)); + return(res); } if ((res = cuddCacheLookup2(manager, Cudd_addOrAbstract, f, cube)) != NULL) { - return(res); + return(res); } T = cuddT(f); @@ -482,51 +496,51 @@ cuddAddOrAbstractRecur( /* If the two indices are the same, so are their levels. */ if (f->index == cube->index) { - res1 = cuddAddOrAbstractRecur(manager, T, cuddT(cube)); - if (res1 == NULL) return(NULL); + res1 = cuddAddOrAbstractRecur(manager, T, cuddT(cube)); + if (res1 == NULL) return(NULL); cuddRef(res1); - if (res1 != one) { - res2 = cuddAddOrAbstractRecur(manager, E, cuddT(cube)); - if (res2 == NULL) { - Cudd_RecursiveDeref(manager,res1); - return(NULL); - } - cuddRef(res2); - res = cuddAddApplyRecur(manager, Cudd_addOr, res1, res2); - if (res == NULL) { - Cudd_RecursiveDeref(manager,res1); - Cudd_RecursiveDeref(manager,res2); - return(NULL); + if (res1 != one) { + res2 = cuddAddOrAbstractRecur(manager, E, cuddT(cube)); + if (res2 == NULL) { + Cudd_RecursiveDeref(manager,res1); + return(NULL); + } + cuddRef(res2); + res = cuddAddApplyRecur(manager, Cudd_addOr, res1, res2); + if (res == NULL) { + Cudd_RecursiveDeref(manager,res1); + Cudd_RecursiveDeref(manager,res2); + return(NULL); + } + cuddRef(res); + Cudd_RecursiveDeref(manager,res1); + Cudd_RecursiveDeref(manager,res2); + } else { + res = res1; } - cuddRef(res); - Cudd_RecursiveDeref(manager,res1); - Cudd_RecursiveDeref(manager,res2); - } else { - res = res1; - } - cuddCacheInsert2(manager, Cudd_addOrAbstract, f, cube, res); - cuddDeref(res); + cuddCacheInsert2(manager, Cudd_addOrAbstract, f, cube, res); + cuddDeref(res); return(res); } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */ - res1 = cuddAddOrAbstractRecur(manager, T, cube); - if (res1 == NULL) return(NULL); + res1 = cuddAddOrAbstractRecur(manager, T, cube); + if (res1 == NULL) return(NULL); cuddRef(res1); - res2 = cuddAddOrAbstractRecur(manager, E, cube); - if (res2 == NULL) { - Cudd_RecursiveDeref(manager,res1); - return(NULL); - } + res2 = cuddAddOrAbstractRecur(manager, E, cube); + if (res2 == NULL) { + Cudd_RecursiveDeref(manager,res1); + return(NULL); + } cuddRef(res2); - res = (res1 == res2) ? res1 : - cuddUniqueInter(manager, (int) f->index, res1, res2); - if (res == NULL) { - Cudd_RecursiveDeref(manager,res1); - Cudd_RecursiveDeref(manager,res2); - return(NULL); - } - cuddDeref(res1); - cuddDeref(res2); - cuddCacheInsert2(manager, Cudd_addOrAbstract, f, cube, res); + res = (res1 == res2) ? res1 : + cuddUniqueInter(manager, (int) f->index, res1, res2); + if (res == NULL) { + Cudd_RecursiveDeref(manager,res1); + Cudd_RecursiveDeref(manager,res2); + return(NULL); + } + cuddDeref(res1); + cuddDeref(res2); + cuddCacheInsert2(manager, Cudd_addOrAbstract, f, cube, res); return(res); } @@ -567,5 +581,8 @@ addCheckPositiveCube( } /* end of addCheckPositiveCube */ + ABC_NAMESPACE_IMPL_END + + |