diff options
Diffstat (limited to 'src/bdd/cudd/cuddClip.c')
-rw-r--r-- | src/bdd/cudd/cuddClip.c | 531 |
1 files changed, 0 insertions, 531 deletions
diff --git a/src/bdd/cudd/cuddClip.c b/src/bdd/cudd/cuddClip.c deleted file mode 100644 index 4da296ef..00000000 --- a/src/bdd/cudd/cuddClip.c +++ /dev/null @@ -1,531 +0,0 @@ -/**CFile*********************************************************************** - - FileName [cuddClip.c] - - PackageName [cudd] - - Synopsis [Clipping functions.] - - Description [External procedures included in this module: - <ul> - <li> Cudd_bddClippingAnd() - <li> Cudd_bddClippingAndAbstract() - </ul> - Internal procedures included in this module: - <ul> - <li> cuddBddClippingAnd() - <li> cuddBddClippingAndAbstract() - </ul> - Static procedures included in this module: - <ul> - <li> cuddBddClippingAndRecur() - <li> cuddBddClipAndAbsRecur() - </ul> - - SeeAlso [] - - 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: cuddClip.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $"; -#endif - -/*---------------------------------------------------------------------------*/ -/* Macro declarations */ -/*---------------------------------------------------------------------------*/ - - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - -static DdNode * cuddBddClippingAndRecur ARGS((DdManager *manager, DdNode *f, DdNode *g, int distance, int direction)); -static DdNode * cuddBddClipAndAbsRecur ARGS((DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, int distance, int direction)); - -/**AutomaticEnd***************************************************************/ - - -/*---------------------------------------------------------------------------*/ -/* Definition of exported functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Approximates the conjunction of two BDDs f and g.] - - Description [Approximates the conjunction of two BDDs f and g. Returns a - pointer to the resulting BDD if successful; NULL if the intermediate - result blows up.] - - SideEffects [None] - - SeeAlso [Cudd_bddAnd] - -******************************************************************************/ -DdNode * -Cudd_bddClippingAnd( - DdManager * dd /* manager */, - DdNode * f /* first conjunct */, - DdNode * g /* second conjunct */, - int maxDepth /* maximum recursion depth */, - int direction /* under (0) or over (1) approximation */) -{ - DdNode *res; - - do { - dd->reordered = 0; - res = cuddBddClippingAnd(dd,f,g,maxDepth,direction); - } while (dd->reordered == 1); - return(res); - -} /* end of Cudd_bddClippingAnd */ - - -/**Function******************************************************************** - - Synopsis [Approximates the conjunction of two BDDs f and g and - simultaneously abstracts the variables in cube.] - - Description [Approximates the conjunction of two BDDs f and g and - simultaneously abstracts the variables in cube. The variables are - existentially abstracted. Returns a pointer to the resulting BDD if - successful; NULL if the intermediate result blows up.] - - SideEffects [None] - - SeeAlso [Cudd_bddAndAbstract Cudd_bddClippingAnd] - -******************************************************************************/ -DdNode * -Cudd_bddClippingAndAbstract( - DdManager * dd /* manager */, - DdNode * f /* first conjunct */, - DdNode * g /* second conjunct */, - DdNode * cube /* cube of variables to be abstracted */, - int maxDepth /* maximum recursion depth */, - int direction /* under (0) or over (1) approximation */) -{ - DdNode *res; - - do { - dd->reordered = 0; - res = cuddBddClippingAndAbstract(dd,f,g,cube,maxDepth,direction); - } while (dd->reordered == 1); - return(res); - -} /* end of Cudd_bddClippingAndAbstract */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of internal functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Approximates the conjunction of two BDDs f and g.] - - Description [Approximates the conjunction of two BDDs f and g. Returns a - pointer to the resulting BDD if successful; NULL if the intermediate - result blows up.] - - SideEffects [None] - - SeeAlso [Cudd_bddClippingAnd] - -******************************************************************************/ -DdNode * -cuddBddClippingAnd( - DdManager * dd /* manager */, - DdNode * f /* first conjunct */, - DdNode * g /* second conjunct */, - int maxDepth /* maximum recursion depth */, - int direction /* under (0) or over (1) approximation */) -{ - DdNode *res; - - res = cuddBddClippingAndRecur(dd,f,g,maxDepth,direction); - - return(res); - -} /* end of cuddBddClippingAnd */ - - -/**Function******************************************************************** - - Synopsis [Approximates the conjunction of two BDDs f and g and - simultaneously abstracts the variables in cube.] - - Description [Approximates the conjunction of two BDDs f and g and - simultaneously abstracts the variables in cube. Returns a - pointer to the resulting BDD if successful; NULL if the intermediate - result blows up.] - - SideEffects [None] - - SeeAlso [Cudd_bddClippingAndAbstract] - -******************************************************************************/ -DdNode * -cuddBddClippingAndAbstract( - DdManager * dd /* manager */, - DdNode * f /* first conjunct */, - DdNode * g /* second conjunct */, - DdNode * cube /* cube of variables to be abstracted */, - int maxDepth /* maximum recursion depth */, - int direction /* under (0) or over (1) approximation */) -{ - DdNode *res; - - res = cuddBddClipAndAbsRecur(dd,f,g,cube,maxDepth,direction); - - return(res); - -} /* end of cuddBddClippingAndAbstract */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of static functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Implements the recursive step of Cudd_bddClippingAnd.] - - Description [Implements the recursive step of Cudd_bddClippingAnd by taking - the conjunction of two BDDs. Returns a pointer to the result is - successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [cuddBddClippingAnd] - -******************************************************************************/ -static DdNode * -cuddBddClippingAndRecur( - DdManager * manager, - DdNode * f, - DdNode * g, - int distance, - int direction) -{ - DdNode *F, *ft, *fe, *G, *gt, *ge; - DdNode *one, *zero, *r, *t, *e; - unsigned int topf, topg, index; - DdNode *(*cacheOp)(DdManager *, DdNode *, DdNode *); - - statLine(manager); - one = DD_ONE(manager); - zero = Cudd_Not(one); - - /* Terminal cases. */ - if (f == zero || g == zero || f == Cudd_Not(g)) return(zero); - if (f == g || g == one) return(f); - if (f == one) return(g); - if (distance == 0) { - /* One last attempt at returning the right result. We sort of - ** cheat by calling Cudd_bddLeq. */ - if (Cudd_bddLeq(manager,f,g)) return(f); - if (Cudd_bddLeq(manager,g,f)) return(g); - if (direction == 1) { - if (Cudd_bddLeq(manager,f,Cudd_Not(g)) || - Cudd_bddLeq(manager,g,Cudd_Not(f))) return(zero); - } - return(Cudd_NotCond(one,(direction == 0))); - } - - /* At this point f and g are not constant. */ - distance--; - - /* Check cache. Try to increase cache efficiency by sorting the - ** pointers. */ - if (f > g) { - DdNode *tmp = f; - f = g; g = tmp; - } - F = Cudd_Regular(f); - G = Cudd_Regular(g); - cacheOp = (DdNode *(*)(DdManager *, DdNode *, DdNode *)) - (direction ? Cudd_bddClippingAnd : cuddBddClippingAnd); - if (F->ref != 1 || G->ref != 1) { - r = cuddCacheLookup2(manager, cacheOp, f, g); - if (r != NULL) return(r); - } - - /* Here we can skip the use of cuddI, because the operands are known - ** to be non-constant. - */ - topf = manager->perm[F->index]; - topg = manager->perm[G->index]; - - /* Compute cofactors. */ - if (topf <= topg) { - 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; - } - - if (topg <= topf) { - gt = cuddT(G); - ge = cuddE(G); - if (Cudd_IsComplement(g)) { - gt = Cudd_Not(gt); - ge = Cudd_Not(ge); - } - } else { - gt = ge = g; - } - - t = cuddBddClippingAndRecur(manager, ft, gt, distance, direction); - if (t == NULL) return(NULL); - cuddRef(t); - e = cuddBddClippingAndRecur(manager, fe, ge, distance, direction); - if (e == NULL) { - Cudd_RecursiveDeref(manager, t); - return(NULL); - } - cuddRef(e); - - if (t == e) { - r = t; - } else { - if (Cudd_IsComplement(t)) { - r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e)); - if (r == NULL) { - Cudd_RecursiveDeref(manager, t); - Cudd_RecursiveDeref(manager, e); - return(NULL); - } - r = Cudd_Not(r); - } else { - r = cuddUniqueInter(manager,(int)index,t,e); - if (r == NULL) { - Cudd_RecursiveDeref(manager, t); - Cudd_RecursiveDeref(manager, e); - return(NULL); - } - } - } - cuddDeref(e); - cuddDeref(t); - if (F->ref != 1 || G->ref != 1) - cuddCacheInsert2(manager, cacheOp, f, g, r); - return(r); - -} /* end of cuddBddClippingAndRecur */ - - -/**Function******************************************************************** - - Synopsis [Approximates the AND of two BDDs and simultaneously abstracts the - variables in cube.] - - Description [Approximates the AND 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_bddClippingAndAbstract] - -******************************************************************************/ -static DdNode * -cuddBddClipAndAbsRecur( - DdManager * manager, - DdNode * f, - DdNode * g, - DdNode * cube, - int distance, - int direction) -{ - DdNode *F, *ft, *fe, *G, *gt, *ge; - DdNode *one, *zero, *r, *t, *e, *Cube; - unsigned int topf, topg, topcube, top, index; - ptruint cacheTag; - - statLine(manager); - one = DD_ONE(manager); - zero = Cudd_Not(one); - - /* Terminal cases. */ - if (f == zero || g == zero || f == Cudd_Not(g)) return(zero); - if (f == one && g == one) return(one); - if (cube == one) { - return(cuddBddClippingAndRecur(manager, f, g, distance, direction)); - } - if (f == one || f == g) { - return (cuddBddExistAbstractRecur(manager, g, cube)); - } - if (g == one) { - return (cuddBddExistAbstractRecur(manager, f, cube)); - } - if (distance == 0) return(Cudd_NotCond(one,(direction == 0))); - - /* At this point f, g, and cube are not constant. */ - distance--; - - /* Check cache. */ - if (f > g) { /* Try to increase cache efficiency. */ - DdNode *tmp = f; - f = g; g = tmp; - } - F = Cudd_Regular(f); - G = Cudd_Regular(g); - cacheTag = direction ? DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG : - DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG; - if (F->ref != 1 || G->ref != 1) { - r = cuddCacheLookup(manager, cacheTag, - 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. - */ - topf = manager->perm[F->index]; - topg = manager->perm[G->index]; - top = ddMin(topf, topg); - topcube = manager->perm[cube->index]; - - if (topcube < top) { - return(cuddBddClipAndAbsRecur(manager, f, g, cuddT(cube), - distance, direction)); - } - /* Now, topcube >= top. */ - - if (topf == top) { - 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; - } - - if (topg == top) { - gt = cuddT(G); - ge = cuddE(G); - if (Cudd_IsComplement(g)) { - gt = Cudd_Not(gt); - ge = Cudd_Not(ge); - } - } else { - gt = ge = g; - } - - if (topcube == top) { - Cube = cuddT(cube); - } else { - Cube = cube; - } - - t = cuddBddClipAndAbsRecur(manager, ft, gt, Cube, distance, direction); - 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) { - if (F->ref != 1 || G->ref != 1) - cuddCacheInsert(manager, cacheTag, f, g, cube, one); - return(one); - } - cuddRef(t); - - e = cuddBddClipAndAbsRecur(manager, fe, ge, Cube, distance, direction); - if (e == NULL) { - Cudd_RecursiveDeref(manager, t); - return(NULL); - } - cuddRef(e); - - if (topcube == top) { /* abstract */ - r = cuddBddClippingAndRecur(manager, Cudd_Not(t), Cudd_Not(e), - distance, (direction == 0)); - if (r == NULL) { - Cudd_RecursiveDeref(manager, t); - Cudd_RecursiveDeref(manager, e); - return(NULL); - } - r = Cudd_Not(r); - cuddRef(r); - Cudd_RecursiveDeref(manager, t); - Cudd_RecursiveDeref(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_RecursiveDeref(manager, t); - Cudd_RecursiveDeref(manager, e); - return(NULL); - } - r = Cudd_Not(r); - } else { - r = cuddUniqueInter(manager,(int)index,t,e); - if (r == NULL) { - Cudd_RecursiveDeref(manager, t); - Cudd_RecursiveDeref(manager, e); - return(NULL); - } - } - cuddDeref(e); - cuddDeref(t); - } - if (F->ref != 1 || G->ref != 1) - cuddCacheInsert(manager, cacheTag, f, g, cube, r); - return (r); - -} /* end of cuddBddClipAndAbsRecur */ - |