From 4a8285eec74715da5642bb7c5a1f440cd847e98d Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 21 Feb 2012 13:41:48 +0000 Subject: [PATCH] Utility method in ODDUtils for converting state index to BDD (already existed at C++ level). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4681 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/include/ODDUtils.h | 8 ++++++++ prism/src/odd/ODDUtils.cc | 22 ++++++++++++++++++++++ prism/src/odd/ODDUtils.java | 9 +++++++++ 3 files changed, 39 insertions(+) diff --git a/prism/include/ODDUtils.h b/prism/include/ODDUtils.h index 7fbf14a5..b3e46b7d 100644 --- a/prism/include/ODDUtils.h +++ b/prism/include/ODDUtils.h @@ -39,6 +39,14 @@ JNIEXPORT jint JNICALL Java_odd_ODDUtils_ODD_1GetNumODDNodes JNIEXPORT jint JNICALL Java_odd_ODDUtils_ODD_1GetIndexOfFirstFromDD (JNIEnv *, jclass, jlong, jlong, jlong, jint); +/* + * Class: odd_ODDUtils + * Method: ODD_SingleIndexToDD + * Signature: (IJJI)J + */ +JNIEXPORT jlong JNICALL Java_odd_ODDUtils_ODD_1SingleIndexToDD + (JNIEnv *, jclass, jint, jlong, jlong, jint); + /* * Class: odd_ODDUtils * Method: ODD_GetTOff diff --git a/prism/src/odd/ODDUtils.cc b/prism/src/odd/ODDUtils.cc index b59ea1e8..33b6709f 100644 --- a/prism/src/odd/ODDUtils.cc +++ b/prism/src/odd/ODDUtils.cc @@ -95,6 +95,28 @@ jint num_vars ); } +//------------------------------------------------------------------------------ + +JNIEXPORT jlong __jlongpointer JNICALL Java_odd_ODDUtils_ODD_1SingleIndexToDD +( +JNIEnv *env, +jclass cls, +jint i, +jlong __jlongpointer odd, +jlong __jlongpointer vars, +jint num_vars +) +{ + return ptr_to_jlong( + single_index_to_bdd( + ddman, + i, + jlong_to_DdNode_array(vars), num_vars, + jlong_to_ODDNode(odd) + ) + ); +} + //------------------------------------------------------------------------------ // ODDNode methods //------------------------------------------------------------------------------ diff --git a/prism/src/odd/ODDUtils.java b/prism/src/odd/ODDUtils.java index 64990a00..d4041dbe 100644 --- a/prism/src/odd/ODDUtils.java +++ b/prism/src/odd/ODDUtils.java @@ -91,6 +91,15 @@ public class ODDUtils return ODD_GetIndexOfFirstFromDD(dd.ptr(), odd.ptr(), vars.array(), vars.n()); } + public static native long ODD_SingleIndexToDD(int i, long odd, long vars, int num_vars); + /** + * Convert a state index to a 0-1 MTBDD representing it, according to an ODD. + */ + public static JDDNode SingleIndexToDD(int i, ODDNode odd, JDDVars vars) + { + return new JDDNode(ODD_SingleIndexToDD(i, odd.ptr(), vars.array(), vars.n())); + } + //------------------------------------------------------------------------------ // ODDNode methods //------------------------------------------------------------------------------