From 123734eeab4fb568d754152ad76301e3a617f621 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Wed, 6 Jul 2016 11:48:21 +0000 Subject: [PATCH] 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 | 8 ++++++ prism/include/odd.h | 5 ++-- prism/src/odd/ODDUtils.cc | 12 +++++++++ prism/src/odd/ODDUtils.java | 20 +++++++++++++- prism/src/odd/odd.cc | 53 +++++++++++++++++++++++++++++++++---- 5 files changed, 90 insertions(+), 8 deletions(-) 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)