summaryrefslogtreecommitdiffstats
path: root/src/bdd/cudd/cuddClip.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/bdd/cudd/cuddClip.c')
-rw-r--r--src/bdd/cudd/cuddClip.c531
1 files changed, 531 insertions, 0 deletions
diff --git a/src/bdd/cudd/cuddClip.c b/src/bdd/cudd/cuddClip.c
new file mode 100644
index 00000000..3c728a56
--- /dev/null
+++ b/src/bdd/cudd/cuddClip.c
@@ -0,0 +1,531 @@
+/**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.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 */
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 22:11:04 +0000