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.c314
1 files changed, 172 insertions, 142 deletions
diff --git a/src/bdd/cudd/cuddClip.c b/src/bdd/cudd/cuddClip.c
index 23331339..028474fe 100644
--- a/src/bdd/cudd/cuddClip.c
+++ b/src/bdd/cudd/cuddClip.c
@@ -7,29 +7,56 @@
Synopsis [Clipping functions.]
Description [External procedures included in this module:
- <ul>
- <li> Cudd_bddClippingAnd()
- <li> Cudd_bddClippingAndAbstract()
- </ul>
+ <ul>
+ <li> Cudd_bddClippingAnd()
+ <li> Cudd_bddClippingAndAbstract()
+ </ul>
Internal procedures included in this module:
- <ul>
- <li> cuddBddClippingAnd()
- <li> cuddBddClippingAndAbstract()
- </ul>
+ <ul>
+ <li> cuddBddClippingAnd()
+ <li> cuddBddClippingAndAbstract()
+ </ul>
Static procedures included in this module:
- <ul>
- <li> cuddBddClippingAndRecur()
- <li> cuddBddClipAndAbsRecur()
- </ul>
+ <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.]
+ 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.]
******************************************************************************/
@@ -40,6 +67,7 @@ ABC_NAMESPACE_IMPL_START
+
/*---------------------------------------------------------------------------*/
/* Constant declarations */
/*---------------------------------------------------------------------------*/
@@ -59,7 +87,7 @@ ABC_NAMESPACE_IMPL_START
/*---------------------------------------------------------------------------*/
#ifndef lint
-static char rcsid[] DD_UNUSED = "$Id: cuddClip.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $";
+static char rcsid[] DD_UNUSED = "$Id: cuddClip.c,v 1.8 2004/08/13 18:04:47 fabio Exp $";
#endif
/*---------------------------------------------------------------------------*/
@@ -73,8 +101,8 @@ static char rcsid[] DD_UNUSED = "$Id: cuddClip.c,v 1.1.1.1 2003/02/24 22:23:51 w
/* 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));
+static DdNode * cuddBddClippingAndRecur (DdManager *manager, DdNode *f, DdNode *g, int distance, int direction);
+static DdNode * cuddBddClipAndAbsRecur (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, int distance, int direction);
/**AutomaticEnd***************************************************************/
@@ -108,8 +136,8 @@ Cudd_bddClippingAnd(
DdNode *res;
do {
- dd->reordered = 0;
- res = cuddBddClippingAnd(dd,f,g,maxDepth,direction);
+ dd->reordered = 0;
+ res = cuddBddClippingAnd(dd,f,g,maxDepth,direction);
} while (dd->reordered == 1);
return(res);
@@ -143,8 +171,8 @@ Cudd_bddClippingAndAbstract(
DdNode *res;
do {
- dd->reordered = 0;
- res = cuddBddClippingAndAbstract(dd,f,g,cube,maxDepth,direction);
+ dd->reordered = 0;
+ res = cuddBddClippingAndAbstract(dd,f,g,cube,maxDepth,direction);
} while (dd->reordered == 1);
return(res);
@@ -248,7 +276,7 @@ cuddBddClippingAndRecur(
DdNode *F, *ft, *fe, *G, *gt, *ge;
DdNode *one, *zero, *r, *t, *e;
unsigned int topf, topg, index;
- DdNode *(*cacheOp)(DdManager *, DdNode *, DdNode *);
+ DD_CTFP cacheOp;
statLine(manager);
one = DD_ONE(manager);
@@ -259,15 +287,15 @@ cuddBddClippingAndRecur(
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)));
+ /* 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. */
@@ -276,16 +304,16 @@ cuddBddClippingAndRecur(
/* Check cache. Try to increase cache efficiency by sorting the
** pointers. */
if (f > g) {
- DdNode *tmp = f;
- f = g; g = tmp;
+ DdNode *tmp = f;
+ f = g; g = tmp;
}
F = Cudd_Regular(f);
G = Cudd_Regular(g);
- cacheOp = (DdNode *(*)(DdManager *, DdNode *, DdNode *))
- (direction ? Cudd_bddClippingAnd : cuddBddClippingAnd);
+ cacheOp = (DD_CTFP)
+ (direction ? Cudd_bddClippingAnd : cuddBddClippingAnd);
if (F->ref != 1 || G->ref != 1) {
- r = cuddCacheLookup2(manager, cacheOp, f, g);
- if (r != NULL) return(r);
+ r = cuddCacheLookup2(manager, cacheOp, f, g);
+ if (r != NULL) return(r);
}
/* Here we can skip the use of cuddI, because the operands are known
@@ -296,27 +324,27 @@ cuddBddClippingAndRecur(
/* 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);
- }
+ 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;
+ 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);
- }
+ gt = cuddT(G);
+ ge = cuddE(G);
+ if (Cudd_IsComplement(g)) {
+ gt = Cudd_Not(gt);
+ ge = Cudd_Not(ge);
+ }
} else {
- gt = ge = g;
+ gt = ge = g;
}
t = cuddBddClippingAndRecur(manager, ft, gt, distance, direction);
@@ -324,35 +352,35 @@ cuddBddClippingAndRecur(
cuddRef(t);
e = cuddBddClippingAndRecur(manager, fe, ge, distance, direction);
if (e == NULL) {
- Cudd_RecursiveDeref(manager, t);
- return(NULL);
+ Cudd_RecursiveDeref(manager, t);
+ return(NULL);
}
cuddRef(e);
if (t == e) {
- r = t;
+ 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);
+ 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);
+ cuddCacheInsert2(manager, cacheOp, f, g, r);
return(r);
} /* end of cuddBddClippingAndRecur */
@@ -393,15 +421,15 @@ cuddBddClipAndAbsRecur(
/* Terminal cases. */
if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
- if (f == one && g == one) return(one);
+ if (f == one && g == one) return(one);
if (cube == one) {
- return(cuddBddClippingAndRecur(manager, f, g, distance, direction));
+ return(cuddBddClippingAndRecur(manager, f, g, distance, direction));
}
if (f == one || f == g) {
- return (cuddBddExistAbstractRecur(manager, g, cube));
+ return (cuddBddExistAbstractRecur(manager, g, cube));
}
if (g == one) {
- return (cuddBddExistAbstractRecur(manager, f, cube));
+ return (cuddBddExistAbstractRecur(manager, f, cube));
}
if (distance == 0) return(Cudd_NotCond(one,(direction == 0)));
@@ -410,19 +438,19 @@ cuddBddClipAndAbsRecur(
/* Check cache. */
if (f > g) { /* Try to increase cache efficiency. */
- DdNode *tmp = f;
- f = g; g = tmp;
+ 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;
+ 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);
- }
+ 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
@@ -434,39 +462,39 @@ cuddBddClipAndAbsRecur(
topcube = manager->perm[cube->index];
if (topcube < top) {
- return(cuddBddClipAndAbsRecur(manager, f, g, cuddT(cube),
- distance, direction));
+ 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);
- }
+ 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;
+ 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);
- }
+ gt = cuddT(G);
+ ge = cuddE(G);
+ if (Cudd_IsComplement(g)) {
+ gt = Cudd_Not(gt);
+ ge = Cudd_Not(ge);
+ }
} else {
- gt = ge = g;
+ gt = ge = g;
}
if (topcube == top) {
- Cube = cuddT(cube);
+ Cube = cuddT(cube);
} else {
- Cube = cube;
+ Cube = cube;
}
t = cuddBddClipAndAbsRecur(manager, ft, gt, Cube, distance, direction);
@@ -476,61 +504,63 @@ cuddBddClipAndAbsRecur(
** 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);
+ 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));
+ 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);
+ 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) {
+ cuddRef(r);
Cudd_RecursiveDeref(manager, t);
Cudd_RecursiveDeref(manager, e);
- return(NULL);
+ 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);
+ cuddDeref(e);
+ cuddDeref(t);
}
if (F->ref != 1 || G->ref != 1)
- cuddCacheInsert(manager, cacheTag, f, g, cube, r);
+ cuddCacheInsert(manager, cacheTag, f, g, cube, r);
return (r);
} /* end of cuddBddClipAndAbsRecur */
+
ABC_NAMESPACE_IMPL_END
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-02 17:18:13 +0000