Infrastructure for deallocating ODDs

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11467 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/include/ODDUtils.h

@@ -23,6 +23,14 @@ JNIEXPORT void JNICALL Java_odd_ODDUtils_ODD_1SetCUDDManager
 JNIEXPORT jlong JNICALL Java_odd_ODDUtils_ODD_1BuildODD
   (JNIEnv *, jclass, jlong, jlong, jint);
 
+/*
+ * Class:     odd_ODDUtils
+ * Method:    ODD_ClearODD
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_odd_ODDUtils_ODD_1ClearODD
+  (JNIEnv *, jclass, jlong);
+
 /*
  * Class:     odd_ODDUtils
  * Method:    ODD_GetNumODDNodes

prism/include/odd.h

@@ -49,8 +49,8 @@ struct ODDNode
 	//int index;
 	DdNode *dd;
 	ODDNode *next;
-    	ODDNode *e;
-    	ODDNode *t;
+	ODDNode *e;
+	ODDNode *t;
 	long eoff;
 	long toff;
 };
@@ -58,6 +58,7 @@ struct ODDNode
 // function prototypes
 
 EXPORT ODDNode *build_odd(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars);
+EXPORT void clear_odd(ODDNode *odd);
 EXPORT int get_index_of_first_from_bdd(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, ODDNode *odd);
 EXPORT DdNode *single_index_to_bdd(DdManager *ddman, int i, DdNode **vars, int num_vars, ODDNode *odd);
 EXPORT int get_num_odd_nodes();

prism/src/odd/ODDUtils.cc

@@ -64,6 +64,18 @@ jint num_vars
 	);
 }
 
+//------------------------------------------------------------------------------
+// clear odd
+//------------------------------------------------------------------------------
+JNIEXPORT void JNICALL Java_odd_ODDUtils_ODD_1ClearODD
+(
+JNIEnv *env,
+jclass cls,
+jlong __jlongpointer odd)
+{
+	clear_odd(jlong_to_ODDNode(odd));
+}
+
 //------------------------------------------------------------------------------
 
 JNIEXPORT jint JNICALL Java_odd_ODDUtils_ODD_1GetNumODDNodes

prism/src/odd/ODDUtils.java

@@ -68,11 +68,29 @@ public class ODDUtils
 	 */
 	public static ODDNode BuildODD(JDDNode dd, JDDVars vars)
 	{
+		if (jdd.SanityJDD.enabled) {
+			// ODD construction requires the JDDVars to be in ascending order
+			jdd.SanityJDD.checkVarsAreSorted(vars);
+		}
+
 		return new ODDNode(
 			ODD_BuildODD(dd.ptr(), vars.array(), vars.n())
 		);
 	}
-	
+
+	private static native void ODD_ClearODD(long ptr);
+	/**
+	 * Clear the ODD with root node {@code odd}.
+	 *<br>
+	 * Note: {@code odd} has to be an ODDNode previously returned by a
+	 * call to the {@code BuildODD} method. Any other odd will
+	 * lead to unexpected behaviour, possibly including crash, etc.
+	 */
+	public static void ClearODD(ODDNode odd)
+	{
+		ODD_ClearODD(odd.ptr());
+	}
+
 	private static native int ODD_GetNumODDNodes();
 	/**
 	 *  Get the number of nodes in the ODD just built.

prism/src/odd/odd.cc

@@ -3,6 +3,7 @@
 //	Copyright (c) 2002-
 //	Authors:
 //	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham)
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
 //	
 //------------------------------------------------------------------------------
 //	
@@ -42,24 +43,50 @@ ODDNode *build_odd(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars)
 	ODDNode **tables;
 	ODDNode *res;
 
-	// build tables to store odd nodes
+	// build tables to store odd nodes during construction
 	tables = new ODDNode*[num_vars+1];
 	for (i = 0; i < num_vars+1; i++) {
 		tables[i] = NULL;
 	}
-	
+
 	// reset node counter
 	num_odd_nodes = 0;
-	
+
 	// call recursive bit
 	res = build_odd_rec(ddman, dd, 0, vars, num_vars, tables);
-	
+
+	// At this point, all the allocated ODDNodes for this ODD are
+	// chained by linked lists (ODD->next), one for each non-empty tables[i].
+	// To facilitate deallocation later on, we chain all these
+	// individual linked lists together.
+	// By construction, the root node (res) is the only node in
+	// the top-most, non-empty table and is thus at the
+	// start of the resulting chain.
+
+	// The current end of the linked list
+	ODDNode *last = NULL;
+	for (i = 0; i < num_vars+1; i++) {
+		if (tables[i] != NULL) {
+			// non-empty tables slot
+			if (last != NULL) {
+				// chain the first node in this tables slot to
+				// the last one above
+				last->next = tables[i];
+			}
+			// search for last node in this tables slot
+			last = tables[i];
+			while (last->next != NULL) {
+				last = last->next;
+			}
+		}
+	}
+
 	// add offsets to odd
 	add_offsets(ddman, res, 0, num_vars);
 
 	// free memory
 	delete tables;
-	
+
 	return res;
 }
 
@@ -135,6 +162,22 @@ long add_offsets(DdManager *ddman, ODDNode *odd, int level, int num_vars)
 
 //------------------------------------------------------------------------------
 
+void clear_odd(ODDNode *odd) {
+	// We assume that odd is the root node of an ODD, i.e.,
+	// was returned previously from a build_odd call.
+	// It is thus the first element of the linked list
+	// (with ODDNode->next pointers) that references all the
+	// allocated ODDNodes of this ODD and we can simply
+	// delete each ODDNode in turn.
+	while (odd != NULL) {
+		ODDNode *next = odd->next;
+		delete odd;
+		odd = next;
+	}
+}
+
+//------------------------------------------------------------------------------
+
 // Get the index (according to an ODD) of the first non-zero enetry of a BDD
 
 int get_index_of_first_from_bdd(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, ODDNode *odd)