diff --git a/prism/include/DebugJDD.h b/prism/include/DebugJDD.h deleted file mode 100644 index 47c56198..00000000 --- a/prism/include/DebugJDD.h +++ /dev/null @@ -1,51 +0,0 @@ -/* DO NOT EDIT THIS FILE - it is machine generated */ -#include -/* Header for class jdd_DebugJDD */ - -#ifndef _Included_jdd_DebugJDD -#define _Included_jdd_DebugJDD -#ifdef __cplusplus -extern "C" { -#endif -/* - * Class: jdd_DebugJDD - * Method: DebugJDD_GetRefCount - * Signature: (J)I - */ -JNIEXPORT jint JNICALL Java_jdd_DebugJDD_DebugJDD_1GetRefCount - (JNIEnv *, jclass, jlong); - -/* - * Class: jdd_DebugJDD - * Method: DebugJDD_GetExternalRefCounts - * Signature: ()[J - */ -JNIEXPORT jlongArray JNICALL Java_jdd_DebugJDD_DebugJDD_1GetExternalRefCounts - (JNIEnv *, jclass); - -#ifdef __cplusplus -} -#endif -#endif -/* Header for class jdd_DebugJDD_DebugJDDNodeLight */ - -#ifndef _Included_jdd_DebugJDD_DebugJDDNodeLight -#define _Included_jdd_DebugJDD_DebugJDDNodeLight -#ifdef __cplusplus -extern "C" { -#endif -#ifdef __cplusplus -} -#endif -#endif -/* Header for class jdd_DebugJDD_DebugJDDNode */ - -#ifndef _Included_jdd_DebugJDD_DebugJDDNode -#define _Included_jdd_DebugJDD_DebugJDDNode -#ifdef __cplusplus -extern "C" { -#endif -#ifdef __cplusplus -} -#endif -#endif diff --git a/prism/include/JDD.h b/prism/include/JDD.h index 5c87f2bd..ef18ba45 100644 --- a/prism/include/JDD.h +++ b/prism/include/JDD.h @@ -679,6 +679,22 @@ JNIEXPORT void JNICALL Java_jdd_JDD_DD_1ExportMatrixToMatlabFile JNIEXPORT void JNICALL Java_jdd_JDD_DD_1ExportMatrixToSpyFile (JNIEnv *, jclass, jlong, jlong, jint, jlong, jint, jint, jstring); +/* + * Class: jdd_JDD + * Method: DebugJDD_GetRefCount + * Signature: (J)I + */ +JNIEXPORT jint JNICALL Java_jdd_JDD_DebugJDD_1GetRefCount + (JNIEnv *, jclass, jlong); + +/* + * Class: jdd_JDD + * Method: DebugJDD_GetExternalRefCounts + * Signature: ()[J + */ +JNIEXPORT jlongArray JNICALL Java_jdd_JDD_DebugJDD_1GetExternalRefCounts + (JNIEnv *, jclass); + #ifdef __cplusplus } #endif diff --git a/prism/src/jdd/DebugJDD.java b/prism/src/jdd/DebugJDD.java index cc7d6e92..7f0ca8ce 100644 --- a/prism/src/jdd/DebugJDD.java +++ b/prism/src/jdd/DebugJDD.java @@ -82,19 +82,6 @@ import prism.PrismLog; */ public class DebugJDD { - private static native int DebugJDD_GetRefCount(long dd); - - private static native long[] DebugJDD_GetExternalRefCounts(); - - static { - try { - System.loadLibrary("jdd"); - } catch (UnsatisfiedLinkError e) { - System.out.println(e); - System.exit(1); - } - } - /** * A DebugJDDNode extends a JDDNode with additional information * useful for tracking refs/derefs and tracing. @@ -172,7 +159,7 @@ public class DebugJDD throw new RuntimeException("DebugJDD: The number of Java references is negative for\n " + toStringVerbose()); } // (2) There are more Java references than CUDD references - if (jrefs > DebugJDD_GetRefCount(ptr())) { + if (jrefs > JDD.DebugJDD_GetRefCount(ptr())) { throw new RuntimeException("DebugJDD: More Java refs than CUDD refs for\n " + toStringVerbose()); } // (3) This node has more refs than there are Java refs in total @@ -194,7 +181,7 @@ public class DebugJDD + ", refs for this JDDNode = " + getNodeRefs() + ", refs from Java = " + getJavaRefCount(ptr()) + ", refs from CUDD (including internal MTBDD refs) = " - + DebugJDD_GetRefCount(ptr()); + + JDD.DebugJDD_GetRefCount(ptr()); } public String ptrAsHex() @@ -370,7 +357,7 @@ public class DebugJDD /** Get the CUDD reference count for the pointer of the JDDNode */ public static int getRefCount(JDDNode n) { - return DebugJDD_GetRefCount(n.ptr()); + return JDD.DebugJDD_GetRefCount(n.ptr()); } /** Get the number of DebugJDDNodes that reference the pointer */ @@ -387,7 +374,7 @@ public class DebugJDD { Map result = new TreeMap(); // Array consists of (pointer, count) pairs - long[] externalRefCounts = DebugJDD_GetExternalRefCounts(); + long[] externalRefCounts = JDD.DebugJDD_GetExternalRefCounts(); int i = 0; while (i < externalRefCounts.length) { long node = externalRefCounts[i++]; @@ -403,9 +390,9 @@ public class DebugJDD private static String nodeInfo(long ptr) { if (JDDNode.DDN_IsConstant(ptr)) { - return "constant(" + JDDNode.DDN_GetValue(ptr) + "), CUDD refs=" + DebugJDD_GetRefCount(ptr); + return "constant(" + JDDNode.DDN_GetValue(ptr) + "), CUDD refs=" + JDD.DebugJDD_GetRefCount(ptr); } else { - return "var(" + JDDNode.DDN_GetIndex(ptr) + "), CUDD refs=" + DebugJDD_GetRefCount(ptr); + return "var(" + JDDNode.DDN_GetIndex(ptr) + "), CUDD refs=" + JDD.DebugJDD_GetRefCount(ptr); } } @@ -515,7 +502,7 @@ public class DebugJDD throw new RuntimeException("DebugJDD: Trying to Deref a JDDNode with non-positive Java ref count:\n " + dNode.toStringVerbose()); } - int cuddRefCount = DebugJDD_GetRefCount(node.ptr()); + int cuddRefCount = JDD.DebugJDD_GetRefCount(node.ptr()); if (cuddRefCount <= 0) { throw new RuntimeException("DebugJDD: Trying to Deref a JDDNode with a non-positive CUDD ref count\n " + dNode.toStringVerbose()); } @@ -626,7 +613,7 @@ public class DebugJDD throw new RuntimeException("DebugJDD: Trying to use a JDDNode with non-positive Java ref count in a method call:\n " + dNode.toStringVerbose()); } - int cuddRefCount = DebugJDD_GetRefCount(node.ptr()); + int cuddRefCount = JDD.DebugJDD_GetRefCount(node.ptr()); if (cuddRefCount <= 0) { throw new RuntimeException("DebugJDD: Trying to use a JDDNode with a non-positive CUDD ref count in a method call:\n " + dNode.toStringVerbose()); } diff --git a/prism/src/jdd/JDD.cc b/prism/src/jdd/JDD.cc index 5b248e04..afb6acba 100644 --- a/prism/src/jdd/JDD.cc +++ b/prism/src/jdd/JDD.cc @@ -28,7 +28,6 @@ #include "JDD.h" #include "JDDNode.h" #include "JDDVars.h" -#include "DebugJDD.h" #include "jnipointer.h" #include @@ -881,14 +880,14 @@ JNIEXPORT jint JNICALL Java_jdd_JDDVars_DDV_1GetIndex(JNIEnv *env, jobject obj, //------------------------------------------------------------------------------ -JNIEXPORT jint JNICALL Java_jdd_DebugJDD_DebugJDD_1GetRefCount(JNIEnv *env, jclass cls, jlong __jlongpointer dd) +JNIEXPORT jint JNICALL Java_jdd_JDD_DebugJDD_1GetRefCount(JNIEnv *env, jclass cls, jlong __jlongpointer dd) { return (jlong_to_DdNode(dd))->ref; } //------------------------------------------------------------------------------ -JNIEXPORT jlongArray JNICALL Java_jdd_DebugJDD_DebugJDD_1GetExternalRefCounts(JNIEnv *env, jclass cls) +JNIEXPORT jlongArray JNICALL Java_jdd_JDD_DebugJDD_1GetExternalRefCounts(JNIEnv *env, jclass cls) { // get external reference counts and return as a long[] Java array // the entries of the array will be alternating ptr / count values diff --git a/prism/src/jdd/JDD.java b/prism/src/jdd/JDD.java index 5682c5fa..ebfe9e75 100644 --- a/prism/src/jdd/JDD.java +++ b/prism/src/jdd/JDD.java @@ -123,6 +123,10 @@ public class JDD private static native void DD_ExportMatrixToMatlabFile(long dd, long rvars, int num_rvars, long cvars, int num_cvars, String name, String filename); private static native void DD_ExportMatrixToSpyFile(long dd, long rvars, int num_rvars, long cvars, int num_cvars, int depth, String filename); + // helpers for DebugJDD, package visibility + static native int DebugJDD_GetRefCount(long dd); + static native long[] DebugJDD_GetExternalRefCounts(); + /** * An exception indicating that CUDD ran out of memory or that another internal error * occurred. diff --git a/prism/src/jdd/Makefile b/prism/src/jdd/Makefile index 85e523e8..bdbeb417 100644 --- a/prism/src/jdd/Makefile +++ b/prism/src/jdd/Makefile @@ -33,7 +33,7 @@ O_FILES = $(CC_FILES:%.cc=$(PRISM_DIR_REL)/$(OBJ_DIR)/$(THIS_DIR)/%.o) default: all -all: checks $(CLASS_FILES) $(PRISM_DIR_REL)/$(INCLUDE_DIR)/JDD.h $(PRISM_DIR_REL)/$(INCLUDE_DIR)/JDDNode.h $(PRISM_DIR_REL)/$(INCLUDE_DIR)/JDDVars.h $(PRISM_DIR_REL)/$(INCLUDE_DIR)/DebugJDD.h $(PRISM_DIR_REL)/$(LIB_DIR)/$(LIBPREFIX)jdd$(LIBSUFFIX) +all: checks $(CLASS_FILES) $(PRISM_DIR_REL)/$(INCLUDE_DIR)/JDD.h $(PRISM_DIR_REL)/$(INCLUDE_DIR)/JDDNode.h $(PRISM_DIR_REL)/$(INCLUDE_DIR)/JDDVars.h $(PRISM_DIR_REL)/$(LIB_DIR)/$(LIBPREFIX)jdd$(LIBSUFFIX) # Try and prevent accidental makes (i.e. called manually, not from top-level Makefile) checks: @@ -62,12 +62,6 @@ $(PRISM_DIR_REL)/$(INCLUDE_DIR)/JDDVars.h: $(PRISM_DIR_REL)/$(CLASSES_DIR)/$(THI (dos2unix $@) \ fi; -$(PRISM_DIR_REL)/$(INCLUDE_DIR)/DebugJDD.h: $(PRISM_DIR_REL)/$(CLASSES_DIR)/$(THIS_DIR)/DebugJDD.class - ($(JAVAH) -classpath $(PRISM_DIR_REL)/$(CLASSES_DIR) -jni -o $@ $(THIS_DIR).DebugJDD; touch $@) - @if [ "$(LIBSUFFIX)" = ".dll" ]; then \ - (dos2unix $@) \ - fi; - $(PRISM_DIR_REL)/$(LIB_DIR)/$(LIBPREFIX)jdd$(LIBSUFFIX): $(O_FILES) $(LD) $(SHARED) $(LDFLAGS) -o $@ $(O_FILES) $(LIBRARIES)