From 2e52615489d7930403217cb208d74932ddd3003e Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 7 Mar 2006 17:11:51 +0000 Subject: [PATCH] Addition of VariablesGreaterThan etc. functions to dd/jdd (used for symmetry). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/include/JDD.h | 40 ++++++++++ prism/include/dd_vars.h | 5 ++ prism/src/dd/dd_vars.cc | 165 ++++++++++++++++++++++++++++++++++++++++ prism/src/jdd/JDD.cc | 36 ++++++++- prism/src/jdd/JDD.java | 45 +++++++++++ 5 files changed, 290 insertions(+), 1 deletion(-) diff --git a/prism/include/JDD.h b/prism/include/JDD.h index ea5bb467..1e37955e 100644 --- a/prism/include/JDD.h +++ b/prism/include/JDD.h @@ -269,6 +269,46 @@ JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1PermuteVariables JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1SwapVariables (JNIEnv *, jclass, jint, jint, jint, jint); +/* + * Class: jdd_JDD + * Method: DD_VariablesGreaterThan + * Signature: (III)I + */ +JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1VariablesGreaterThan + (JNIEnv *, jclass, jint, jint, jint); + +/* + * Class: jdd_JDD + * Method: DD_VariablesGreaterThanEquals + * Signature: (III)I + */ +JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1VariablesGreaterThanEquals + (JNIEnv *, jclass, jint, jint, jint); + +/* + * Class: jdd_JDD + * Method: DD_VariablesLessThan + * Signature: (III)I + */ +JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1VariablesLessThan + (JNIEnv *, jclass, jint, jint, jint); + +/* + * Class: jdd_JDD + * Method: DD_VariablesLessThanEquals + * Signature: (III)I + */ +JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1VariablesLessThanEquals + (JNIEnv *, jclass, jint, jint, jint); + +/* + * Class: jdd_JDD + * Method: DD_VariablesEquals + * Signature: (III)I + */ +JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1VariablesEquals + (JNIEnv *, jclass, jint, jint, jint); + /* * Class: jdd_JDD * Method: DD_ThereExists diff --git a/prism/include/dd_vars.h b/prism/include/dd_vars.h index b1e475a0..02237c20 100644 --- a/prism/include/dd_vars.h +++ b/prism/include/dd_vars.h @@ -34,5 +34,10 @@ DdNode *DD_PermuteVariables(DdManager *ddman, DdNode *dd, DdNode **old_vars, DdNode **new_vars, int num_vars); DdNode *DD_SwapVariables(DdManager *ddman, DdNode *dd, DdNode **old_vars, DdNode **new_vars, int num_vars); +DdNode *DD_VariablesGreaterThan(DdManager *ddman, DdNode **x_vars, DdNode **y_vars, int num_vars); +DdNode *DD_VariablesGreaterThanEquals(DdManager *ddman, DdNode **x_vars, DdNode **y_vars, int num_vars); +DdNode *DD_VariablesLessThan(DdManager *ddman, DdNode **x_vars, DdNode **y_vars, int num_vars); +DdNode *DD_VariablesLessThanEquals(DdManager *ddman, DdNode **x_vars, DdNode **y_vars, int num_vars); +DdNode *DD_VariablesEquals(DdManager *ddman, DdNode **x_vars, DdNode **y_vars, int num_vars); //------------------------------------------------------------------------------ diff --git a/prism/src/dd/dd_vars.cc b/prism/src/dd/dd_vars.cc index b3dfdf3f..37d965cb 100644 --- a/prism/src/dd/dd_vars.cc +++ b/prism/src/dd/dd_vars.cc @@ -30,6 +30,7 @@ #include #include #include "dd_vars.h" +#include "dd_basics.h" //------------------------------------------------------------------------------ @@ -88,3 +89,167 @@ int num_vars } //------------------------------------------------------------------------------ + +// Generates BDD for the function x > y +// where x, y are num_vars-bit numbers encoded by variables x_vars, y_vars + +DdNode *DD_VariablesGreaterThan +( +DdManager *ddman, +DdNode **x_vars, +DdNode **y_vars, +int num_vars +) +{ + DdNode *tmp, *res; + DdNode **x_bdd_vars, **y_bdd_vars; + int i; + + // create bdd vars from add vars + x_bdd_vars = new DdNode*[num_vars]; + y_bdd_vars = new DdNode*[num_vars]; + for (i = 0; i < num_vars; i++) { + x_bdd_vars[i] = Cudd_bddIthVar(ddman, x_vars[i]->index); + Cudd_Ref(x_bdd_vars[i]); + y_bdd_vars[i] = Cudd_bddIthVar(ddman, y_vars[i]->index); + Cudd_Ref(y_bdd_vars[i]); + } + // call main function + tmp = Cudd_Xgty(ddman, num_vars, NULL, x_bdd_vars, y_bdd_vars); + Cudd_Ref(tmp); + // convert bdd to add + res = Cudd_BddToAdd(ddman, tmp); + Cudd_Ref(res); + Cudd_RecursiveDeref(ddman, tmp); + // free variables + for (i = 0; i < num_vars; i++) { + Cudd_RecursiveDeref(ddman, x_bdd_vars[i]); + Cudd_RecursiveDeref(ddman, y_bdd_vars[i]); + } + delete x_bdd_vars; + delete y_bdd_vars; + + return res; +} + +//------------------------------------------------------------------------------ + +// Generates BDD for the function x >= y +// where x, y are num_vars-bit numbers encoded by variables x_vars, y_vars + +DdNode *DD_VariablesGreaterThanEquals +( +DdManager *ddman, +DdNode **x_vars, +DdNode **y_vars, +int num_vars +) +{ + return DD_Not(ddman, DD_VariablesLessThan(ddman, x_vars, y_vars, num_vars)); +} + +//------------------------------------------------------------------------------ + +// Generates BDD for the function x < y +// where x, y are num_vars-bit numbers encoded by variables x_vars, y_vars + +DdNode *DD_VariablesLessThan +( +DdManager *ddman, +DdNode **x_vars, +DdNode **y_vars, +int num_vars +) +{ + DdNode *tmp, *res; + DdNode **x_bdd_vars, **y_bdd_vars; + int i; + + // create bdd vars from add vars + x_bdd_vars = new DdNode*[num_vars]; + y_bdd_vars = new DdNode*[num_vars]; + for (i = 0; i < num_vars; i++) { + x_bdd_vars[i] = Cudd_bddIthVar(ddman, x_vars[i]->index); + Cudd_Ref(x_bdd_vars[i]); + y_bdd_vars[i] = Cudd_bddIthVar(ddman, y_vars[i]->index); + Cudd_Ref(y_bdd_vars[i]); + } + // call main function + tmp = Cudd_Xgty(ddman, num_vars, NULL, y_bdd_vars, x_bdd_vars); + Cudd_Ref(tmp); + // convert bdd to add + res = Cudd_BddToAdd(ddman, tmp); + Cudd_Ref(res); + Cudd_RecursiveDeref(ddman, tmp); + // free variables + for (i = 0; i < num_vars; i++) { + Cudd_RecursiveDeref(ddman, x_bdd_vars[i]); + Cudd_RecursiveDeref(ddman, y_bdd_vars[i]); + } + delete x_bdd_vars; + delete y_bdd_vars; + + return res; +} + +//------------------------------------------------------------------------------ + +// Generates BDD for the function x <= y +// where x, y are num_vars-bit numbers encoded by variables x_vars, y_vars + +DdNode *DD_VariablesLessThanEquals +( +DdManager *ddman, +DdNode **x_vars, +DdNode **y_vars, +int num_vars +) +{ + return DD_Not(ddman, DD_VariablesGreaterThan(ddman, x_vars, y_vars, num_vars)); +} + +//------------------------------------------------------------------------------ + +// Generates BDD for the function x == y +// where x, y are num_vars-bit numbers encoded by variables x_vars, y_vars + +DdNode *DD_VariablesEquals +( +DdManager *ddman, +DdNode **x_vars, +DdNode **y_vars, +int num_vars +) +{ + DdNode *tmp, *res; + DdNode **x_bdd_vars, **y_bdd_vars; + int i; + + // create bdd vars from add vars + x_bdd_vars = new DdNode*[num_vars]; + y_bdd_vars = new DdNode*[num_vars]; + for (i = 0; i < num_vars; i++) { + x_bdd_vars[i] = Cudd_bddIthVar(ddman, x_vars[i]->index); + Cudd_Ref(x_bdd_vars[i]); + y_bdd_vars[i] = Cudd_bddIthVar(ddman, y_vars[i]->index); + Cudd_Ref(y_bdd_vars[i]); + } + // call main function + tmp = Cudd_Xeqy(ddman, num_vars, x_bdd_vars, y_bdd_vars); + Cudd_Ref(tmp); + // convert bdd to add + res = Cudd_BddToAdd(ddman, tmp); + Cudd_Ref(res); + Cudd_RecursiveDeref(ddman, tmp); + // free variables + for (i = 0; i < num_vars; i++) { + Cudd_RecursiveDeref(ddman, x_bdd_vars[i]); + Cudd_RecursiveDeref(ddman, y_bdd_vars[i]); + } + delete x_bdd_vars; + delete y_bdd_vars; + + return res; +} + +//------------------------------------------------------------------------------ diff --git a/prism/src/jdd/JDD.cc b/prism/src/jdd/JDD.cc index 117831e5..e74892c0 100644 --- a/prism/src/jdd/JDD.cc +++ b/prism/src/jdd/JDD.cc @@ -251,12 +251,46 @@ JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1PermuteVariables(JNIEnv *env, jclass cls //------------------------------------------------------------------------------ - JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1SwapVariables(JNIEnv *env, jclass cls, jint dd, jint old_vars, jint new_vars, jint num_vars) { return (int)DD_SwapVariables(ddman, (DdNode *)dd, (DdNode **)old_vars, (DdNode **)new_vars, num_vars); } +//------------------------------------------------------------------------------ + +JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1VariablesGreaterThan(JNIEnv *env, jclass cls, jint x_vars, jint y_vars, jint num_vars) +{ + return (int)DD_VariablesGreaterThan(ddman, (DdNode **)x_vars, (DdNode **)y_vars, num_vars); +} + +//------------------------------------------------------------------------------ + +JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1VariablesGreaterThanEquals(JNIEnv *env, jclass cls, jint x_vars, jint y_vars, jint num_vars) +{ + return (int)DD_VariablesGreaterThanEquals(ddman, (DdNode **)x_vars, (DdNode **)y_vars, num_vars); +} + +//------------------------------------------------------------------------------ + +JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1VariablesLessThan(JNIEnv *env, jclass cls, jint x_vars, jint y_vars, jint num_vars) +{ + return (int)DD_VariablesLessThan(ddman, (DdNode **)x_vars, (DdNode **)y_vars, num_vars); +} + +//------------------------------------------------------------------------------ + +JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1VariablesLessThanEquals(JNIEnv *env, jclass cls, jint x_vars, jint y_vars, jint num_vars) +{ + return (int)DD_VariablesLessThanEquals(ddman, (DdNode **)x_vars, (DdNode **)y_vars, num_vars); +} + +//------------------------------------------------------------------------------ + +JNIEXPORT jint JNICALL Java_jdd_JDD_DD_1VariablesEquals(JNIEnv *env, jclass cls, jint x_vars, jint y_vars, jint num_vars) +{ + return (int)DD_VariablesEquals(ddman, (DdNode **)x_vars, (DdNode **)y_vars, num_vars); +} + //============================================================================== // // Wrapper functions for dd_abstr diff --git a/prism/src/jdd/JDD.java b/prism/src/jdd/JDD.java index ef3d3660..33c37944 100644 --- a/prism/src/jdd/JDD.java +++ b/prism/src/jdd/JDD.java @@ -65,6 +65,11 @@ public class JDD // dd_vars private static native int DD_PermuteVariables(int dd, int old_vars, int new_vars, int num_vars); private static native int DD_SwapVariables(int dd, int old_vars, int new_vars, int num_vars); + private static native int DD_VariablesGreaterThan(int x_vars, int y_vars, int num_vars); + private static native int DD_VariablesGreaterThanEquals(int x_vars, int y_vars, int num_vars); + private static native int DD_VariablesLessThan(int x_vars, int y_vars, int num_vars); + private static native int DD_VariablesLessThanEquals(int x_vars, int y_vars, int num_vars); + private static native int DD_VariablesEquals(int x_vars, int y_vars, int num_vars); // dd_abstr private static native int DD_ThereExists(int dd, int vars, int num_vars); private static native int DD_ForAll(int dd, int vars, int num_vars); @@ -376,6 +381,46 @@ public class JDD return new JDDNode(DD_SwapVariables(dd.ptr(), old_vars.array(), new_vars.array(), old_vars.n())); } + // build x > y for variables x, y + // [ REFS: , DEREFS: ] + + public static JDDNode VariablesGreaterThan(JDDVars x_vars, JDDVars y_vars) + { + return new JDDNode(DD_VariablesGreaterThan(x_vars.array(), y_vars.array(), x_vars.n())); + } + + // build x >= y for variables x, y + // [ REFS: , DEREFS: ] + + public static JDDNode VariablesGreaterThanEquals(JDDVars x_vars, JDDVars y_vars) + { + return new JDDNode(DD_VariablesGreaterThanEquals(x_vars.array(), y_vars.array(), x_vars.n())); + } + + // build x < y for variables x, y + // [ REFS: , DEREFS: ] + + public static JDDNode VariablesLessThan(JDDVars x_vars, JDDVars y_vars) + { + return new JDDNode(DD_VariablesLessThan(x_vars.array(), y_vars.array(), x_vars.n())); + } + + // build x <= y for variables x, y + // [ REFS: , DEREFS: ] + + public static JDDNode VariablesLessThanEquals(JDDVars x_vars, JDDVars y_vars) + { + return new JDDNode(DD_VariablesLessThanEquals(x_vars.array(), y_vars.array(), x_vars.n())); + } + + // build x == y for variables x, y + // [ REFS: , DEREFS: ] + + public static JDDNode VariablesEquals(JDDVars x_vars, JDDVars y_vars) + { + return new JDDNode(DD_VariablesEquals(x_vars.array(), y_vars.array(), x_vars.n())); + } + // wrapper methods for dd_abstr // existential abstraction of vars from dd