diff --git a/prism/include/JDD.h b/prism/include/JDD.h index 26a63a50..cb9a1bd9 100644 --- a/prism/include/JDD.h +++ b/prism/include/JDD.h @@ -143,6 +143,14 @@ JNIEXPORT void JNICALL Java_jdd_JDD_DD_1Deref JNIEXPORT void JNICALL Java_jdd_JDD_DD_1PrintCacheInfo (JNIEnv *, jclass); +/* + * Class: jdd_JDD + * Method: DD_GetErrorFlag + * Signature: ()Z + */ +JNIEXPORT jboolean JNICALL Java_jdd_JDD_DD_1GetErrorFlag + (JNIEnv *, jclass); + /* * Class: jdd_JDD * Method: DD_Create diff --git a/prism/include/dd_cudd.h b/prism/include/dd_cudd.h index ac374d3a..d33cde6f 100644 --- a/prism/include/dd_cudd.h +++ b/prism/include/dd_cudd.h @@ -36,5 +36,7 @@ void DD_SetCUDDEpsilon(DdManager *ddman, double epsilon); void DD_PrintCacheInfo(DdManager *ddman); void DD_CloseDownCUDD(DdManager *ddman); void DD_CloseDownCUDD(DdManager *ddman, bool check); +bool DD_GetErrorFlag(DdManager *ddman); +void DD_SetErrorFlag(); //------------------------------------------------------------------------------ diff --git a/prism/src/dd/dd_cudd.cc b/prism/src/dd/dd_cudd.cc index 00aad40e..f4714f8d 100644 --- a/prism/src/dd/dd_cudd.cc +++ b/prism/src/dd/dd_cudd.cc @@ -31,6 +31,11 @@ extern FILE *dd_out; +// A flag indicating that a CuDD error has occurred +// that could not be signaled by returning a NULL DdNode* +// from a function +bool dd_cudd_error_flag = false; + static int Cudd_CheckZeroRefVerbose(DdManager *ddman); //----------------------------------------------------------------------------------- @@ -226,3 +231,23 @@ int Cudd_CheckZeroRefVerbose(DdManager *manager) //----------------------------------------------------------------------------------- +// Get the value of the DD error flag +bool DD_GetErrorFlag(DdManager *ddman) +{ + return dd_cudd_error_flag || (ddman->errorCode != CUDD_NO_ERROR); +} + +//----------------------------------------------------------------------------------- + +// Set the DD error flag. Should be set if a CuDD error has been +// detected that could not be signaled by returning a NULL DdNode* +// from the function +void DD_SetErrorFlag() +{ + dd_cudd_error_flag = true; +} + + +//----------------------------------------------------------------------------------- + + diff --git a/prism/src/jdd/JDD.cc b/prism/src/jdd/JDD.cc index af550c42..14c4e77a 100644 --- a/prism/src/jdd/JDD.cc +++ b/prism/src/jdd/JDD.cc @@ -872,3 +872,10 @@ JNIEXPORT jint JNICALL Java_jdd_DebugJDD_DebugJDD_1GetRefCount(JNIEnv *env, jcla { return (jlong_to_DdNode(dd))->ref; } + +//------------------------------------------------------------------------------ + +JNIEXPORT jboolean JNICALL Java_jdd_JDD_DD_1GetErrorFlag(JNIEnv *env, jclass cls) +{ + return DD_GetErrorFlag(ddman); +} diff --git a/prism/src/jdd/JDD.java b/prism/src/jdd/JDD.java index 3880eaea..4ba76078 100644 --- a/prism/src/jdd/JDD.java +++ b/prism/src/jdd/JDD.java @@ -48,6 +48,7 @@ public class JDD private static native void DD_Ref(long dd); private static native void DD_Deref(long dd); private static native void DD_PrintCacheInfo(); + private static native boolean DD_GetErrorFlag(); // dd_basics private static native long DD_Create(); private static native long DD_Constant(double value); @@ -1380,6 +1381,17 @@ public class JDD return new JDDNode(ptr); } + /** + * Check whether the DD error flag is set, indicating an + * out-of-meory situation in CuDD or another internal error. + * If the flag is set, throws a {@code CuddOutOfMemoryException}. + */ + public static void checkForCuddError() + { + if (DD_GetErrorFlag()) + throw new CuddOutOfMemoryException(); + } + } //------------------------------------------------------------------------------