diff options
Diffstat (limited to 'src/bdd/cudd/cuddAddAbs.c')
| -rw-r--r-- | src/bdd/cudd/cuddAddAbs.c | 566 |
1 files changed, 0 insertions, 566 deletions
diff --git a/src/bdd/cudd/cuddAddAbs.c b/src/bdd/cudd/cuddAddAbs.c deleted file mode 100644 index b256ad0f..00000000 --- a/src/bdd/cudd/cuddAddAbs.c +++ /dev/null @@ -1,566 +0,0 @@ -/**CFile*********************************************************************** - - FileName [cuddAddAbs.c] - - PackageName [cudd] - - 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>] - - 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.] - -******************************************************************************/ - -#include "util_hack.h" -#include "cuddInt.h" - -/*---------------------------------------------------------------------------*/ -/* Constant declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Stucture declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Type declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Variable declarations */ -/*---------------------------------------------------------------------------*/ - -#ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddAddAbs.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $"; -#endif - -static DdNode *two; - -/*---------------------------------------------------------------------------*/ -/* Macro declarations */ -/*---------------------------------------------------------------------------*/ - - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - -static int addCheckPositiveCube ARGS((DdManager *manager, DdNode *cube)); - -/**AutomaticEnd***************************************************************/ - - -/*---------------------------------------------------------------------------*/ -/* Definition of exported functions */ -/*---------------------------------------------------------------------------*/ - -/**Function******************************************************************** - - Synopsis [Existentially Abstracts all the variables in cube from f.] - - Description [Abstracts all the variables in cube from f by summing - over all possible values taken by the variables. Returns the - abstracted ADD.] - - SideEffects [None] - - SeeAlso [Cudd_addUnivAbstract Cudd_bddExistAbstract - Cudd_addOrAbstract] - -******************************************************************************/ -DdNode * -Cudd_addExistAbstract( - DdManager * manager, - DdNode * f, - DdNode * cube) -{ - DdNode *res; - - two = cuddUniqueConst(manager,(CUDD_VALUE_TYPE) 2); - if (two == NULL) return(NULL); - cuddRef(two); - - if (addCheckPositiveCube(manager, cube) == 0) { - (void) fprintf(manager->err,"Error: Can only abstract cubes"); - return(NULL); - } - - do { - manager->reordered = 0; - res = cuddAddExistAbstractRecur(manager, f, cube); - } while (manager->reordered == 1); - - if (res == NULL) { - Cudd_RecursiveDeref(manager,two); - return(NULL); - } - cuddRef(res); - Cudd_RecursiveDeref(manager,two); - cuddDeref(res); - - return(res); - -} /* end of Cudd_addExistAbstract */ - - -/**Function******************************************************************** - - Synopsis [Universally Abstracts all the variables in cube from f.] - - Description [Abstracts all the variables in cube from f by taking - the product over all possible values taken by the variable. Returns - the abstracted ADD if successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_addExistAbstract Cudd_bddUnivAbstract - Cudd_addOrAbstract] - -******************************************************************************/ -DdNode * -Cudd_addUnivAbstract( - DdManager * manager, - DdNode * f, - DdNode * cube) -{ - DdNode *res; - - if (addCheckPositiveCube(manager, cube) == 0) { - (void) fprintf(manager->err,"Error: Can only abstract cubes"); - return(NULL); - } - - do { - manager->reordered = 0; - res = cuddAddUnivAbstractRecur(manager, f, cube); - } while (manager->reordered == 1); - - return(res); - -} /* end of Cudd_addUnivAbstract */ - - -/**Function******************************************************************** - - Synopsis [Disjunctively abstracts all the variables in cube from the - 0-1 ADD f.] - - Description [Abstracts all the variables in cube from the 0-1 ADD f - by taking the disjunction over all possible values taken by the - variables. Returns the abstracted ADD if successful; NULL - otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_addUnivAbstract Cudd_addExistAbstract] - -******************************************************************************/ -DdNode * -Cudd_addOrAbstract( - DdManager * manager, - DdNode * f, - DdNode * cube) -{ - DdNode *res; - - if (addCheckPositiveCube(manager, cube) == 0) { - (void) fprintf(manager->err,"Error: Can only abstract cubes"); - return(NULL); - } - - do { - manager->reordered = 0; - res = cuddAddOrAbstractRecur(manager, f, cube); - } while (manager->reordered == 1); - return(res); - -} /* end of Cudd_addOrAbstract */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of internal functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Cudd_addExistAbstract.] - - Description [Performs the recursive step of Cudd_addExistAbstract. - Returns the ADD obtained by abstracting the variables of cube from f, - if successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -DdNode * -cuddAddExistAbstractRecur( - DdManager * manager, - DdNode * f, - DdNode * cube) -{ - DdNode *T, *E, *res, *res1, *res2, *zero; - - statLine(manager); - zero = DD_ZERO(manager); - - /* 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) { - Cudd_RecursiveDeref(manager,res1); - return(NULL); - } - cuddRef(res); - Cudd_RecursiveDeref(manager,res1); - cuddDeref(res); - return(res); - } - - if ((res = cuddCacheLookup2(manager, Cudd_addExistAbstract, f, cube)) != NULL) { - return(res); - } - - T = cuddT(f); - E = cuddE(f); - - /* 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); - cuddRef(res1); - 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) { - 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); - return(res); - } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */ - 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); - } - 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); - return(res); - } - -} /* end of cuddAddExistAbstractRecur */ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Cudd_addUnivAbstract.] - - Description [Performs the recursive step of Cudd_addUnivAbstract. - Returns the ADD obtained by abstracting the variables of cube from f, - if successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -DdNode * -cuddAddUnivAbstractRecur( - DdManager * manager, - DdNode * f, - DdNode * cube) -{ - DdNode *T, *E, *res, *res1, *res2, *one, *zero; - - statLine(manager); - one = DD_ONE(manager); - zero = DD_ZERO(manager); - - /* Cube is guaranteed to be a cube at this point. - ** zero and one are the only constatnts c such that c*c=c. - */ - if (f == zero || f == one || cube == one) { - 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) { - Cudd_RecursiveDeref(manager,res1); - return(NULL); - } - cuddRef(res); - Cudd_RecursiveDeref(manager,res1); - cuddDeref(res); - return(res); - } - - if ((res = cuddCacheLookup2(manager, Cudd_addUnivAbstract, f, cube)) != NULL) { - return(res); - } - - T = cuddT(f); - E = cuddE(f); - - /* 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); - cuddRef(res1); - 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) { - 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); - return(res); - } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */ - 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); - } - 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); - return(res); - } - -} /* end of cuddAddUnivAbstractRecur */ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Cudd_addOrAbstract.] - - Description [Performs the recursive step of Cudd_addOrAbstract. - Returns the ADD obtained by abstracting the variables of cube from f, - if successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -DdNode * -cuddAddOrAbstractRecur( - DdManager * manager, - DdNode * f, - DdNode * cube) -{ - 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); - } - - /* 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); - } - - if ((res = cuddCacheLookup2(manager, Cudd_addOrAbstract, f, cube)) != NULL) { - return(res); - } - - T = cuddT(f); - E = cuddE(f); - - /* 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); - 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); - } - cuddRef(res); - Cudd_RecursiveDeref(manager,res1); - Cudd_RecursiveDeref(manager,res2); - } else { - res = res1; - } - 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); - cuddRef(res1); - 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); - return(res); - } - -} /* end of cuddAddOrAbstractRecur */ - - - -/*---------------------------------------------------------------------------*/ -/* Definition of static functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Checks whether cube is an ADD representing the product - of positive literals.] - - Description [Checks whether cube is an ADD representing the product of - positive literals. Returns 1 in case of success; 0 otherwise.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -static int -addCheckPositiveCube( - DdManager * manager, - DdNode * cube) -{ - if (Cudd_IsComplement(cube)) return(0); - if (cube == DD_ONE(manager)) return(1); - if (cuddIsConstant(cube)) return(0); - if (cuddE(cube) == DD_ZERO(manager)) { - return(addCheckPositiveCube(manager, cuddT(cube))); - } - return(0); - -} /* end of addCheckPositiveCube */ - |