diff --git a/prism/include/ODDUtils.h b/prism/include/ODDUtils.h
index b3e46b7d..a83395fa 100644
--- a/prism/include/ODDUtils.h
+++ b/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
diff --git a/prism/include/odd.h b/prism/include/odd.h
index 01ec5982..c7c8f2f6 100644
--- a/prism/include/odd.h
+++ b/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();
diff --git a/prism/src/odd/ODDUtils.cc b/prism/src/odd/ODDUtils.cc
index 33b6709f..be7483a9 100644
--- a/prism/src/odd/ODDUtils.cc
+++ b/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
diff --git a/prism/src/odd/ODDUtils.java b/prism/src/odd/ODDUtils.java
index 0c91683b..c209c881 100644
--- a/prism/src/odd/ODDUtils.java
+++ b/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}.
+ *
+ * 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.
diff --git a/prism/src/odd/odd.cc b/prism/src/odd/odd.cc
index 187e1b7e..9efea586 100644
--- a/prism/src/odd/odd.cc
+++ b/prism/src/odd/odd.cc
@@ -3,6 +3,7 @@
// Copyright (c) 2002-
// Authors:
// * Dave Parker (University of Oxford, formerly University of Birmingham)
+// * Joachim Klein (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)