From 9ece01bfd469cb677a574f4db43b532ed4e6bf8b Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Thu, 29 Jan 2009 10:09:20 +0000
Subject: [PATCH] Addition of function Cudd_addFirstFilter.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@919 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 cudd/cudd/cudd.h       |   1 +
 cudd/cudd/cuddAddAbs.c | 161 ++++++++++++++++++++++++++++++++++++++---
 cudd/cudd/cuddInt.h    |   1 +
 cudd/modified/README   |   5 ++
 4 files changed, 158 insertions(+), 10 deletions(-)

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 @@
 		<li> Cudd_addOrAbstract()
 		<li> Cudd_addMinAbstract()
 		<li> Cudd_addMaxAbstract()
+		<li> Cudd_addFirstAbstract()
 		</ul>
 	Internal procedures included in this module:
 		<ul>
@@ -21,6 +22,7 @@
 		<li> cuddAddOrAbstractRecur()
 		<li> cuddAddMinAbstractRecur()
 		<li> cuddAddMaxAbstractRecur()
+		<li> cuddAddFirstAbstractRecur()
 		</ul>
 	Static procedures included in this module:
 		<ul>
@@ -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()
 
 ------------------