From 2e6582c10893d09b9d49969e81b5913ab8f8a782 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 21 Feb 2012 12:38:02 +0000
Subject: [PATCH] Utility method in ODDUtils for finding index of first state
 in a BDD.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4676 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/odd/ODDUtils.cc   | 20 ++++++++++++++++++++
 prism/src/odd/ODDUtils.java | 19 +++++++++++++++----
 2 files changed, 35 insertions(+), 4 deletions(-)

diff --git a/prism/src/odd/ODDUtils.cc b/prism/src/odd/ODDUtils.cc
index f5aa85b3..b59ea1e8 100644
--- a/prism/src/odd/ODDUtils.cc
+++ b/prism/src/odd/ODDUtils.cc
@@ -75,6 +75,26 @@ jclass cls
 	return get_num_odd_nodes();
 }
 
+//------------------------------------------------------------------------------
+
+JNIEXPORT jint JNICALL Java_odd_ODDUtils_ODD_1GetIndexOfFirstFromDD
+(
+JNIEnv *env,
+jclass cls,
+jlong __jlongpointer dd,
+jlong __jlongpointer odd,
+jlong __jlongpointer vars,
+jint num_vars
+)
+{
+	return get_index_of_first_from_bdd(
+		ddman,
+		jlong_to_DdNode(dd),
+		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 67cca8ca..64990a00 100644
--- a/prism/src/odd/ODDUtils.java
+++ b/prism/src/odd/ODDUtils.java
@@ -62,8 +62,10 @@ public class ODDUtils
 	// JNI wrappers
 	//------------------------------------------------------------------------------
 	
-	// build odd
 	private static native long ODD_BuildODD(long dd, long vars, int num_vars);
+	/**
+	 *  Build an ODD.
+	 */
 	public static ODDNode BuildODD(JDDNode dd, JDDVars vars)
 	{
 		return new ODDNode(
@@ -71,15 +73,24 @@ public class ODDUtils
 		);
 	}
 	
-	//------------------------------------------------------------------------------
-
-	// get number of nodes in odd just built
 	private static native int ODD_GetNumODDNodes();
+	/**
+	 *  Get the number of nodes in the ODD just built.
+	 */
 	public static int GetNumODDNodes()
 	{
 		return ODD_GetNumODDNodes();
 	}
 	
+	public static native int ODD_GetIndexOfFirstFromDD(long dd, long odd, long vars, int num_vars);
+	/**
+	 *  Get the index of the first non-zero element of a 0-1 MTBDD, according to an ODD.
+	 */
+	public static int GetIndexOfFirstFromDD(JDDNode dd, ODDNode odd, JDDVars vars)
+	{
+		return ODD_GetIndexOfFirstFromDD(dd.ptr(), odd.ptr(), vars.array(), vars.n());
+	}
+	
 	//------------------------------------------------------------------------------
 	// ODDNode methods
 	//------------------------------------------------------------------------------