JDD: add JDD.IsZeroOneMTBDD() method for checking if an MTBDD is a 0/1-MTBDD

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

prism/include/JDD.h

@@ -455,6 +455,14 @@ JNIEXPORT jdouble JNICALL Java_jdd_JDD_DD_1FindMax
 JNIEXPORT jlong JNICALL Java_jdd_JDD_DD_1RestrictToFirst
   (JNIEnv *, jclass, jlong, jlong, jint);
 
+/*
+ * Class:     jdd_JDD
+ * Method:    DD_IsZeroOneMTBDD
+ * Signature: (J)Z
+ */
+JNIEXPORT jboolean JNICALL Java_jdd_JDD_DD_1IsZeroOneMTBDD
+  (JNIEnv *, jclass, jlong);
+
 /*
  * Class:     jdd_JDD
  * Method:    DD_GetNumNodes

prism/include/dd_term.h

@@ -43,5 +43,7 @@ bool DD_EqualSupNormRel(DdManager *ddman, DdNode *dd1, DdNode *dd2, double epsil
 double DD_FindMin(DdManager *ddman, DdNode *dd);
 double DD_FindMax(DdManager *ddman, DdNode *dd);
 DdNode *DD_RestrictToFirst(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars);
+bool DD_IsZeroOneMTBDD(DdManager *ddman, DdNode *dd);
+
 
 //------------------------------------------------------------------------------

prism/src/dd/dd_term.cc

@@ -264,6 +264,33 @@ DdNode *dd
 	return Cudd_V(v);
 }
 
+
+//------------------------------------------------------------------------------
+
+bool DD_IsZeroOneMTBDD
+(
+DdManager *ddman,
+DdNode *dd
+)
+{
+	DdGen *gen;
+	DdNode *node;
+	bool rv = true;
+
+	Cudd_ForeachNode(ddman, dd, gen, node) {
+		if (Cudd_IsConstant(node)) {
+			if (node != Cudd_ReadOne(ddman) && node != Cudd_ReadZero(ddman)) {
+				rv = false;
+				// we could break here, as it's clear that we are done
+				// however, it looks like CUDD would then not free the
+				// DdGen* gen
+			}
+		}
+	}
+
+	return rv;
+}
+
 //------------------------------------------------------------------------------
 
 DdNode *DD_RestrictToFirst

prism/src/jdd/JDD.cc

@@ -440,6 +440,15 @@ JNIEXPORT jlong __jlongpointer JNICALL Java_jdd_JDD_DD_1RestrictToFirst(JNIEnv *
 	return ptr_to_jlong(DD_RestrictToFirst(ddman, jlong_to_DdNode(dd), jlong_to_DdNode_array(vars), num_vars));
 }
 
+//------------------------------------------------------------------------------
+
+
+JNIEXPORT jboolean JNICALL Java_jdd_JDD_DD_1IsZeroOneMTBDD(JNIEnv *env, jclass cls, jlong __jlongpointer dd)
+{
+	return DD_IsZeroOneMTBDD(ddman, jlong_to_DdNode(dd));
+}
+
+
 //==============================================================================
 //
 //	Wrapper functions for dd_info

prism/src/jdd/JDD.java

@@ -91,6 +91,7 @@ public class JDD
 	private static native double DD_FindMin(long dd);
 	private static native double DD_FindMax(long dd);
 	private static native long DD_RestrictToFirst(long dd, long vars, int num_vars);
+	private static native boolean DD_IsZeroOneMTBDD(long dd);
 	// dd_info
 	private static native int DD_GetNumNodes(long dd);
 	private static native int DD_GetNumTerminals(long dd);
@@ -861,7 +862,16 @@ public class JDD
 		checkForCuddError();
 		return rv;
 	}
-	
+
+	/**
+	 * returns true if dd is a 0/1-MTBDD, i.e., all terminal nodes are either 0 or 1
+	 * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]
+	 */
+	public static boolean IsZeroOneMTBDD(JDDNode dd)
+	{
+		return DD_IsZeroOneMTBDD(dd.ptr());
+	}
+
 	/**
 	 * returns minimum terminal in dd
 	 * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]