diff options
Diffstat (limited to 'src/bdd/cudd/cuddBddAbs.c')
| -rw-r--r-- | src/bdd/cudd/cuddBddAbs.c | 689 |
1 files changed, 0 insertions, 689 deletions
diff --git a/src/bdd/cudd/cuddBddAbs.c b/src/bdd/cudd/cuddBddAbs.c deleted file mode 100644 index 9552464e..00000000 --- a/src/bdd/cudd/cuddBddAbs.c +++ /dev/null @@ -1,689 +0,0 @@ -/**CFile*********************************************************************** - - FileName [cuddBddAbs.c] - - PackageName [cudd] - - 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> - ] - - 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: cuddBddAbs.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $"; -#endif - -/*---------------------------------------------------------------------------*/ -/* Macro declarations */ -/*---------------------------------------------------------------------------*/ - - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - -static int bddCheckPositiveCube ARGS((DdManager *manager, DdNode *cube)); - -/**AutomaticEnd***************************************************************/ - - -/*---------------------------------------------------------------------------*/ -/* Definition of exported functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Existentially abstracts all the variables in cube from f.] - - Description [Existentially abstracts all the variables in cube from f. - Returns the abstracted BDD if successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_bddUnivAbstract Cudd_addExistAbstract] - -******************************************************************************/ -DdNode * -Cudd_bddExistAbstract( - DdManager * manager, - DdNode * f, - DdNode * cube) -{ - 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); - } - - do { - manager->reordered = 0; - res = cuddBddExistAbstractRecur(manager, f, cube); - } while (manager->reordered == 1); - - return(res); - -} /* end of Cudd_bddExistAbstract */ - - -/**Function******************************************************************** - - Synopsis [Takes the exclusive OR of two BDDs and simultaneously abstracts the - variables in cube.] - - Description [Takes the exclusive OR of two BDDs and simultaneously abstracts - the variables in cube. The variables are existentially abstracted. Returns a - pointer to the result is successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_bddUnivAbstract Cudd_bddExistAbstract Cudd_bddAndAbstract] - -******************************************************************************/ -DdNode * -Cudd_bddXorExistAbstract( - DdManager * manager, - DdNode * f, - DdNode * g, - DdNode * cube) -{ - 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); - } - - do { - manager->reordered = 0; - res = cuddBddXorExistAbstractRecur(manager, f, g, cube); - } while (manager->reordered == 1); - - return(res); - -} /* end of Cudd_bddXorExistAbstract */ - - -/**Function******************************************************************** - - Synopsis [Universally abstracts all the variables in cube from f.] - - Description [Universally abstracts all the variables in cube from f. - Returns the abstracted BDD if successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_bddExistAbstract Cudd_addUnivAbstract] - -******************************************************************************/ -DdNode * -Cudd_bddUnivAbstract( - DdManager * manager, - DdNode * f, - DdNode * cube) -{ - 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); - } - - do { - manager->reordered = 0; - res = cuddBddExistAbstractRecur(manager, Cudd_Not(f), cube); - } while (manager->reordered == 1); - if (res != NULL) res = Cudd_Not(res); - - return(res); - -} /* end of Cudd_bddUnivAbstract */ - - -/**Function******************************************************************** - - Synopsis [Computes the boolean difference of f with respect to x.] - - Description [Computes the boolean difference of f with respect to the - variable with index x. Returns the BDD of the boolean difference if - successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -DdNode * -Cudd_bddBooleanDiff( - DdManager * manager, - DdNode * f, - int x) -{ - DdNode *res, *var; - - /* If the variable is not currently in the manager, f cannot - ** depend on it. - */ - if (x >= manager->size) return(Cudd_Not(DD_ONE(manager))); - var = manager->vars[x]; - - do { - manager->reordered = 0; - res = cuddBddBooleanDiffRecur(manager, Cudd_Regular(f), var); - } while (manager->reordered == 1); - - return(res); - -} /* end of Cudd_bddBooleanDiff */ - - -/**Function******************************************************************** - - Synopsis [Checks whether a variable is dependent on others in a - function.] - - Description [Checks whether a variable is dependent on others in a - function. Returns 1 if the variable is dependent; 0 otherwise. No - new nodes are created.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -int -Cudd_bddVarIsDependent( - DdManager *dd, /* manager */ - DdNode *f, /* function */ - DdNode *var /* variable */) -{ - DdNode *F, *res, *zero, *ft, *fe; - unsigned topf, level; - DdNode *(*cacheOp)(DdManager *, DdNode *, DdNode *); - int retval; - - zero = Cudd_Not(DD_ONE(dd)); - if (Cudd_IsConstant(f)) return(f == zero); - - /* From now on f is not constant. */ - F = Cudd_Regular(f); - topf = (unsigned) dd->perm[F->index]; - level = (unsigned) dd->perm[var->index]; - - /* 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); - } - - cacheOp = - (DdNode *(*)(DdManager *, DdNode *, DdNode *)) Cudd_bddVarIsDependent; - res = cuddCacheLookup2(dd,cacheOp,f,var); - if (res != NULL) { - return(res != zero); - } - - /* Compute cofactors. */ - ft = Cudd_NotCond(cuddT(F), f != F); - fe = Cudd_NotCond(cuddE(F), f != F); - - if (topf == level) { - retval = Cudd_bddLeq(dd,ft,Cudd_Not(fe)); - } else { - retval = Cudd_bddVarIsDependent(dd,ft,var) && - Cudd_bddVarIsDependent(dd,fe,var); - } - - cuddCacheInsert2(dd,cacheOp,f,var,Cudd_NotCond(zero,retval)); - - return(retval); - -} /* Cudd_bddVarIsDependent */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of internal functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive steps of Cudd_bddExistAbstract.] - - Description [Performs the recursive steps of Cudd_bddExistAbstract. - Returns the BDD obtained by abstracting the variables - of cube from f if successful; NULL otherwise. It is also used by - Cudd_bddUnivAbstract.] - - SideEffects [None] - - SeeAlso [Cudd_bddExistAbstract Cudd_bddUnivAbstract] - -******************************************************************************/ -DdNode * -cuddBddExistAbstractRecur( - DdManager * manager, - DdNode * f, - DdNode * cube) -{ - 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. */ - if (cube == one || F == one) { - return(f); - } - /* From now on, f and cube are non-constant. */ - - /* 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); - } - - /* Check the cache. */ - if (F->ref != 1 && (res = cuddCacheLookup2(manager, Cudd_bddExistAbstract, f, cube)) != NULL) { - return(res); - } - - /* Compute the cofactors of f. */ - T = cuddT(F); E = cuddE(F); - if (f != F) { - 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); - } - cuddRef(res1); - 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) { - 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); - return(res); - } else { /* if (cuddI(manager,F->index) < cuddI(manager,cube->index)) */ - 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); - } - 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); - } - cuddDeref(res1); - cuddDeref(res2); - if (F->ref != 1) - cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, res); - return(res); - } - -} /* end of cuddBddExistAbstractRecur */ - - -/**Function******************************************************************** - - Synopsis [Takes the exclusive OR of two BDDs and simultaneously abstracts the - variables in cube.] - - Description [Takes the exclusive OR of two BDDs and simultaneously abstracts - the variables in cube. The variables are existentially abstracted. Returns a - pointer to the result is successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_bddAndAbstract] - -******************************************************************************/ -DdNode * -cuddBddXorExistAbstractRecur( - DdManager * manager, - DdNode * f, - DdNode * g, - DdNode * cube) -{ - DdNode *F, *fv, *fnv, *G, *gv, *gnv; - DdNode *one, *zero, *r, *t, *e, *Cube; - unsigned int topf, topg, topcube, top, index; - - statLine(manager); - one = DD_ONE(manager); - zero = Cudd_Not(one); - - /* Terminal cases. */ - if (f == g) { - return(zero); - } - if (f == Cudd_Not(g)) { - return(one); - } - if (cube == one) { - return(cuddBddXorRecur(manager, f, g)); - } - if (f == one) { - return(cuddBddExistAbstractRecur(manager, Cudd_Not(g), cube)); - } - if (g == one) { - return(cuddBddExistAbstractRecur(manager, Cudd_Not(f), cube)); - } - if (f == zero) { - return(cuddBddExistAbstractRecur(manager, g, cube)); - } - if (g == zero) { - 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; - } - - /* Check cache. */ - r = cuddCacheLookup(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube); - if (r != NULL) { - return(r); - } - - /* Here we can skip the use of cuddI, because the operands are known - ** to be non-constant. - */ - F = Cudd_Regular(f); - topf = manager->perm[F->index]; - G = Cudd_Regular(g); - topg = manager->perm[G->index]; - top = ddMin(topf, topg); - topcube = manager->perm[cube->index]; - - if (topcube < top) { - 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); - } - } else { - 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); - } - } else { - gv = gnv = g; - } - - if (topcube == top) { - Cube = cuddT(cube); - } else { - Cube = cube; - } - - t = cuddBddXorExistAbstractRecur(manager, fv, gv, Cube); - if (t == NULL) return(NULL); - - /* Special case: 1 OR anything = 1. Hence, no need to compute - ** 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); - } - 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)); - 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); - } - cuddCacheInsert(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube, r); - return (r); - -} /* end of cuddBddXorExistAbstractRecur */ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive steps of Cudd_bddBoleanDiff.] - - Description [Performs the recursive steps of Cudd_bddBoleanDiff. - Returns the BDD obtained by XORing the cofactors of f with respect to - var if successful; NULL otherwise. Exploits the fact that dF/dx = - dF'/dx.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -DdNode * -cuddBddBooleanDiffRecur( - DdManager * manager, - DdNode * f, - DdNode * var) -{ - DdNode *T, *E, *res, *res1, *res2; - - statLine(manager); - if (cuddI(manager,f->index) > manager->perm[var->index]) { - /* 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)); - return(res); - } - - /* From now on, cuddI(manager,f->index) < cuddI(manager,cube->index). */ - - /* Check the cache. */ - res = cuddCacheLookup2(manager, cuddBddBooleanDiffRecur, f, var); - if (res != NULL) { - return(res); - } - - /* Compute the cofactors of f. */ - T = cuddT(f); E = cuddE(f); - - res1 = cuddBddBooleanDiffRecur(manager, T, var); - if (res1 == NULL) return(NULL); - cuddRef(res1); - res2 = cuddBddBooleanDiffRecur(manager, Cudd_Regular(E), var); - if (res2 == 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); - } - cuddDeref(res1); - cuddDeref(res2); - cuddCacheInsert2(manager, cuddBddBooleanDiffRecur, f, var, res); - return(res); - -} /* end of cuddBddBooleanDiffRecur */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of static functions */ -/*---------------------------------------------------------------------------*/ - -/**Function******************************************************************** - - Synopsis [Checks whether cube is an BDD representing the product of - positive literals.] - - Description [Returns 1 in case of success; 0 otherwise.] - - SideEffects [None] - -******************************************************************************/ -static int -bddCheckPositiveCube( - 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) == Cudd_Not(DD_ONE(manager))) { - return(bddCheckPositiveCube(manager, cuddT(cube))); - } - return(0); - -} /* end of bddCheckPositiveCube */ - |