diff --git a/cudd/cudd/cudd.h b/cudd/cudd/cudd.h
index 9ac4e0cf..278ec3a2 100644
--- a/cudd/cudd/cudd.h
+++ b/cudd/cudd/cudd.h
@@ -725,6 +725,7 @@ extern DdNode * Cudd_addUnivAbstract (DdManager *manager, DdNode *f, DdNode *cub
extern DdNode * Cudd_addOrAbstract (DdManager *manager, DdNode *f, DdNode *cube);
extern DdNode * Cudd_addMinAbstract (DdManager *manager, DdNode *f, DdNode *cube);
extern DdNode * Cudd_addMaxAbstract (DdManager *manager, DdNode *f, DdNode *cube);
+extern DdNode * Cudd_addFirstFilter (DdManager *manager, DdNode *f, DdNode *cube);
extern DdNode * Cudd_addApply (DdManager *dd, DdNode * (*)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g);
extern DdNode * Cudd_addPlus (DdManager *dd, DdNode **f, DdNode **g);
extern DdNode * Cudd_addTimes (DdManager *dd, DdNode **f, DdNode **g);
diff --git a/cudd/cudd/cuddAddAbs.c b/cudd/cudd/cuddAddAbs.c
index 87965838..59b5c42c 100644
--- a/cudd/cudd/cuddAddAbs.c
+++ b/cudd/cudd/cuddAddAbs.c
@@ -13,6 +13,7 @@
Cudd_addOrAbstract()
Cudd_addMinAbstract()
Cudd_addMaxAbstract()
+ Cudd_addFirstAbstract()
Internal procedures included in this module:
@@ -21,6 +22,7 @@
- cuddAddOrAbstractRecur()
- cuddAddMinAbstractRecur()
- cuddAddMaxAbstractRecur()
+
- cuddAddFirstAbstractRecur()
Static procedures included in this module:
@@ -210,9 +212,9 @@ Cudd_addOrAbstract(
/**Function********************************************************************
Synopsis [Abstracts all the variables in cube from the
- 0-1 ADD f by taking the minimum.]
+ ADD f by taking the minimum.]
- Description [Abstracts all the variables in cube from the 0-1 ADD f
+ Description [Abstracts all the variables in cube from the ADD f
by taking the minimum over all possible values taken by the
variables. Returns the abstracted ADD if successful; NULL
otherwise.]
@@ -249,9 +251,9 @@ Cudd_addMinAbstract(
/**Function********************************************************************
Synopsis [Abstracts all the variables in cube from the
- 0-1 ADD f by taking the maximum.]
+ ADD f by taking the maximum.]
- Description [Abstracts all the variables in cube from the 0-1 ADD f
+ Description [Abstracts all the variables in cube from the ADD f
by taking the maximum over all possible values taken by the
variables. Returns the abstracted ADD if successful; NULL
otherwise.]
@@ -285,6 +287,45 @@ Cudd_addMaxAbstract(
} /* end of Cudd_addMaxAbstract */
+/**Function********************************************************************
+
+ Synopsis [Filters over all the variables in cube from the
+ ADD f by taking the first element.]
+
+ Description [Filters over all the variables in cube from the ADD f
+ by taking the first of all possible values taken by the
+ variables. Returns the filtered ADD if successful; NULL
+ otherwise.]
+
+ SideEffects [None]
+
+ SeeAlso [Cudd_addUnivAbstract Cudd_addExistAbstract]
+
+ Note: Added by Dave Parker 14/6/99
+
+******************************************************************************/
+DdNode *
+Cudd_addFirstFilter(
+ 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 = cuddAddFirstFilterRecur(manager, f, cube);
+ } while (manager->reordered == 1);
+ return(res);
+
+} /* end of Cudd_addFirstFilter */
+
+
/*---------------------------------------------------------------------------*/
/* Definition of internal functions */
/*---------------------------------------------------------------------------*/
@@ -625,11 +666,10 @@ cuddAddMinAbstractRecur(
return(f);
}
+ /* Abstract a variable that does not appear in f. */
if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
res = cuddAddMinAbstractRecur(manager, f, cuddT(cube));
- cuddRef(res);
- cuddDeref(res);
- return(res);
+ return(res);
}
if ((res = cuddCacheLookup2(manager, Cudd_addMinAbstract, f, cube)) != NULL) {
@@ -718,11 +758,10 @@ cuddAddMaxAbstractRecur(
return(f);
}
+ /* Abstract a variable that does not appear in f. */
if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
res = cuddAddMaxAbstractRecur(manager, f, cuddT(cube));
- cuddRef(res);
- cuddDeref(res);
- return(res);
+ return(res);
}
if ((res = cuddCacheLookup2(manager, Cudd_addMaxAbstract, f, cube)) != NULL) {
@@ -783,6 +822,108 @@ cuddAddMaxAbstractRecur(
} /* end of cuddAddMaxAbstractRecur */
+/**Function********************************************************************
+
+ Synopsis [Performs the recursive step of Cudd_addFirstFilterRecur.]
+
+ Description [Performs the recursive step of Cudd_addFirstFilterRecur.
+ Returns the ADD obtained by filtering the variables of cube from f,
+ if successful; NULL otherwise.]
+
+ SideEffects [None]
+
+ SeeAlso []
+
+******************************************************************************/
+DdNode *
+cuddAddFirstFilterRecur(
+ DdManager * manager,
+ DdNode * f,
+ DdNode * cube)
+{
+ DdNode *T, *E, *res, *res1, *res2, *zero;
+
+ zero = DD_ZERO(manager);
+
+ /* Cube is guaranteed to be a cube at this point. */
+ if (f == zero || cuddIsConstant(cube)) {
+ return(f);
+ }
+
+ if ((res = cuddCacheLookup2(manager, Cudd_addFirstFilter, f, cube)) != NULL) {
+ return(res);
+ }
+
+
+ T = cuddT(f);
+ E = cuddE(f);
+
+ /* Case where a variable that does not appear in f. */
+ if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
+ res1 = zero;
+ res2 = cuddAddFirstFilterRecur(manager, f, cuddT(cube));
+ res = (res1 == res2) ? res1 :
+ cuddUniqueInter(manager, (int) cube->index, res1, res2);
+ if (res == NULL) {
+ Cudd_RecursiveDeref(manager,res1);
+ Cudd_RecursiveDeref(manager,res2);
+ return(NULL);
+ }
+ cuddCacheInsert2(manager, Cudd_addFirstFilter, f, cube, res);
+ return(res);
+ }
+
+ /* If the two indices are the same, so are their levels. */
+ if (f->index == cube->index) {
+ res2 = cuddAddFirstFilterRecur(manager, E, cuddT(cube));
+ if (res2 == NULL) return(NULL);
+ cuddRef(res2);
+ if (res2 != zero) {
+ res1 = zero;
+ } else {
+ res1 = cuddAddFirstFilterRecur(manager, T, cuddT(cube));
+ if (res1 == NULL) {
+ Cudd_RecursiveDeref(manager, res2);
+ return(NULL);
+ }
+ cuddRef(res1);
+ }
+ res = (res1 == res2) ? res1 :
+ cuddUniqueInter(manager, (int) cube->index, res1, res2);
+ if (res == NULL) {
+ Cudd_RecursiveDeref(manager, res1);
+ Cudd_RecursiveDeref(manager, res2);
+ return(NULL);
+ }
+ cuddCacheInsert2(manager, Cudd_addFirstFilter, f, cube, res);
+ return(res);
+ }
+ else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
+ res1 = cuddAddFirstFilterRecur(manager, T, cube);
+ if (res1 == NULL) return(NULL);
+ cuddRef(res1);
+ res2 = cuddAddFirstFilterRecur(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_addFirstFilter, f, cube, res);
+ return(res);
+ }
+
+} /* end of cuddAddFirstFilterRecur */
+
+
/*---------------------------------------------------------------------------*/
/* Definition of static functions */
/*---------------------------------------------------------------------------*/
diff --git a/cudd/cudd/cuddInt.h b/cudd/cudd/cuddInt.h
index 3c41e454..9275bdee 100644
--- a/cudd/cudd/cuddInt.h
+++ b/cudd/cudd/cuddInt.h
@@ -993,6 +993,7 @@ extern DdNode * cuddAddUnivAbstractRecur (DdManager *manager, DdNode *f, DdNode
extern DdNode * cuddAddOrAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube);
extern DdNode * cuddAddMinAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube);
extern DdNode * cuddAddMaxAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube);
+extern DdNode * cuddAddFirstFilterRecur (DdManager *manager, DdNode *f, DdNode *cube);
extern DdNode * cuddAddApplyRecur (DdManager *dd, DdNode * (*)(DdManager *, DdNode **, DdNode **), DdNode *f, DdNode *g);
extern DdNode * cuddAddMonadicApplyRecur (DdManager * dd, DdNode * (*op)(DdManager *, DdNode *), DdNode * f);
extern DdNode * cuddAddScalarInverseRecur (DdManager *dd, DdNode *f, DdNode *epsilon);
diff --git a/cudd/modified/README b/cudd/modified/README
index ab31b11e..829961d1 100644
--- a/cudd/modified/README
+++ b/cudd/modified/README
@@ -55,6 +55,9 @@ Details
cuddAddMinAbstractRecur()
cuddAddMaxAbstractRecur()
+* Added another abstraction functions to do "first", ie:
+ Cudd_addFirstAbstract()
+ cuddAddFirstAbstractRecur()
------------------
[cudd/cuddAddApply.c]
@@ -112,6 +115,7 @@ Details
* Added prototypes for:
Cudd_addMinAbstract()
Cudd_addMaxAbstract()
+ Cudd_addFirstAbstract()
Cudd_addEquals()
Cudd_addNotEquals()
Cudd_addGreaterThan()
@@ -126,6 +130,7 @@ Details
Cudd_EqualSupNormRel()
cuddAddMinAbstractRecur()
cuddAddMaxAbstractRecur()
+ cuddAddFirstAbstractRecur()
------------------