diff --git a/prism/include/IntegerVector.h b/prism/include/IntegerVector.h new file mode 100644 index 00000000..d681b82a --- /dev/null +++ b/prism/include/IntegerVector.h @@ -0,0 +1,53 @@ +/* DO NOT EDIT THIS FILE - it is machine generated */ +#include +/* Header for class dv_IntegerVector */ + +#ifndef _Included_dv_IntegerVector +#define _Included_dv_IntegerVector +#ifdef __cplusplus +extern "C" { +#endif +/* + * Class: dv_IntegerVector + * Method: IV_CreateZeroVector + * Signature: (I)J + */ +JNIEXPORT jlong JNICALL Java_dv_IntegerVector_IV_1CreateZeroVector + (JNIEnv *, jobject, jint); + +/* + * Class: dv_IntegerVector + * Method: IV_ConvertMTBDD + * Signature: (JJIJ)J + */ +JNIEXPORT jlong JNICALL Java_dv_IntegerVector_IV_1ConvertMTBDD + (JNIEnv *, jobject, jlong, jlong, jint, jlong); + +/* + * Class: dv_IntegerVector + * Method: IV_GetElement + * Signature: (JII)I + */ +JNIEXPORT jint JNICALL Java_dv_IntegerVector_IV_1GetElement + (JNIEnv *, jobject, jlong, jint, jint); + +/* + * Class: dv_IntegerVector + * Method: IV_SetElement + * Signature: (JIII)V + */ +JNIEXPORT void JNICALL Java_dv_IntegerVector_IV_1SetElement + (JNIEnv *, jobject, jlong, jint, jint, jint); + +/* + * Class: dv_IntegerVector + * Method: IV_Clear + * Signature: (J)V + */ +JNIEXPORT void JNICALL Java_dv_IntegerVector_IV_1Clear + (JNIEnv *, jobject, jlong); + +#ifdef __cplusplus +} +#endif +#endif diff --git a/prism/include/iv.h b/prism/include/iv.h new file mode 100644 index 00000000..02fab62f --- /dev/null +++ b/prism/include/iv.h @@ -0,0 +1,53 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Oxford, formerly University of Birmingham) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +#ifndef IV_H +#define IV_H + +//------------------------------------------------------------------------------ + +#include +#include +#include + +// Flags for building Windows DLLs +#ifdef __MINGW32__ + #define EXPORT __declspec(dllexport) +#else + #define EXPORT +#endif + +// function prototypes + +EXPORT int *mtbdd_to_integer_vector(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, ODDNode *odd); +EXPORT int *mtbdd_to_integer_vector(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, ODDNode *odd, int *res); +EXPORT DdNode *integer_vector_to_mtbdd(DdManager *ddman, int *vec, DdNode **vars, int num_vars, ODDNode *odd); + +//------------------------------------------------------------------------------ + +#endif + +//------------------------------------------------------------------------------ diff --git a/prism/src/dv/DoubleVector.cc b/prism/src/dv/DoubleVector.cc index 8514af8c..5a080dbf 100644 --- a/prism/src/dv/DoubleVector.cc +++ b/prism/src/dv/DoubleVector.cc @@ -27,6 +27,7 @@ #include "dv.h" #include "DoubleVector.h" +#include "DoubleVectorGlob.h" #include "jnipointer.h" #include diff --git a/prism/src/dv/DoubleVector.java b/prism/src/dv/DoubleVector.java index 4dbe8bf5..4da7e5a3 100644 --- a/prism/src/dv/DoubleVector.java +++ b/prism/src/dv/DoubleVector.java @@ -2,8 +2,7 @@ // // Copyright (c) 2002- // Authors: -// * Dave Parker (University of Oxford, formerly University of Birmingham) -// Description: Java wrapper class for double vector +// * Dave Parker (University of Birmingham/Oxford) // //------------------------------------------------------------------------------ // @@ -31,6 +30,9 @@ import prism.*; import jdd.*; import odd.*; +/** + * Class to encapsulate a vector of doubles, stored natively. + */ public class DoubleVector { //------------------------------------------------------------------------------ diff --git a/prism/src/dv/IntegerVector.cc b/prism/src/dv/IntegerVector.cc new file mode 100644 index 00000000..73f8c59a --- /dev/null +++ b/prism/src/dv/IntegerVector.cc @@ -0,0 +1,127 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Oxford, formerly University of Birmingham) +// Description: C++ code for integer vector +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +#include "iv.h" +#include "DoubleVectorGlob.h" +#include "IntegerVector.h" +#include "jnipointer.h" + +#include +#include + +//------------------------------------------------------------------------------ +// IntegerVector methods +//------------------------------------------------------------------------------ + +JNIEXPORT jlong __jlongpointer JNICALL Java_dv_IntegerVector_IV_1CreateZeroVector +( +JNIEnv *env, +jobject obj, +jint n +) +{ + int *vector; + int i; + try { + vector = new int[n]; + } catch (std::bad_alloc e) { + return 0; + } + for (i = 0; i < n; i++) { + vector[i] = 0; + } + + return ptr_to_jlong(vector); +} + +//------------------------------------------------------------------------------ + +JNIEXPORT jlong __jlongpointer JNICALL Java_dv_IntegerVector_IV_1ConvertMTBDD +( +JNIEnv *env, +jobject obj, +jlong __jlongpointer dd, +jlong __jlongpointer vars, +jint num_vars, +jlong __jlongpointer odd +) +{ + return ptr_to_jlong( + mtbdd_to_integer_vector( + ddman, + jlong_to_DdNode(dd), + jlong_to_DdNode_array(vars), num_vars, + jlong_to_ODDNode(odd) + ) + ); +} + +//------------------------------------------------------------------------------ + +JNIEXPORT jint JNICALL Java_dv_IntegerVector_IV_1GetElement +( +JNIEnv *env, +jobject obj, +jlong __jlongpointer v, +jint n, +jint i +) +{ + int *vector = (int *) jlong_to_ptr(v); + return (jint)vector[i]; +} + +//------------------------------------------------------------------------------ + +JNIEXPORT void JNICALL Java_dv_IntegerVector_IV_1SetElement +( +JNIEnv *env, +jobject obj, +jlong __jlongpointer v, +jint n, +jint i, +jint j +) +{ + int *vector = (int *) jlong_to_ptr(v); + vector[i] = j; +} + +//------------------------------------------------------------------------------ + +JNIEXPORT void JNICALL Java_dv_IntegerVector_IV_1Clear +( +JNIEnv *env, +jobject obj, +jlong __jlongpointer vector +) +{ + // note we assume that this memory was created with new + delete (int *) jlong_to_ptr(vector); +} + +//------------------------------------------------------------------------------ diff --git a/prism/src/dv/IntegerVector.java b/prism/src/dv/IntegerVector.java new file mode 100644 index 00000000..5cc2c746 --- /dev/null +++ b/prism/src/dv/IntegerVector.java @@ -0,0 +1,130 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Birmingham/Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package dv; + +import prism.*; +import jdd.*; +import odd.*; + +/** + * Class to encapsulate a vector of integer, stored natively. + */ +public class IntegerVector +{ + //------------------------------------------------------------------------------ + // load jni stuff from shared library + //------------------------------------------------------------------------------ + + static + { + try { + System.loadLibrary("dv"); + } + catch (UnsatisfiedLinkError e) { + System.out.println(e); + System.exit(1); + } + } + + //------------------------------------------------------------------------------ + // instance variables/methods + //------------------------------------------------------------------------------ + + // data + private long v; // vector (actually a C/C++ pointer cast to a long) + private int n; // size + + // constructors + + private native long IV_CreateZeroVector(int n); + public IntegerVector(int size) throws PrismException + { + v = IV_CreateZeroVector(size); + if (v == 0) throw new PrismException("Out of memory"); + n = size; + } + + public IntegerVector(long vector, int size) + { + v = vector; + n = size; + } + + private native long IV_ConvertMTBDD(long dd, long vars, int num_vars, long odd); + public IntegerVector(JDDNode dd, JDDVars vars, ODDNode odd) + { + v = IV_ConvertMTBDD(dd.ptr(), vars.array(), vars.n(), odd.ptr()); + n = (int)(odd.getEOff() + odd.getTOff()); + } + + // get methods + + public long getPtr() + { + return v; + } + + public int getSize() + { + return n; + } + + // get element + private native int IV_GetElement(long v, int n, int i); + public int getElement(int i) + { + return IV_GetElement(v, n, i); + } + + // set element + private native void IV_SetElement(long v, int n, int i, int j); + public void setElement(int i, int j) + { + IV_SetElement(v, n, i, j); + } + + // clear (free memory) + private native void IV_Clear(long v); + public void clear() + { + IV_Clear(v); + } + + // print (all, including nonzeros) + public void print(PrismLog log) + { + int i, j; + + for (i = 0; i < n; i++) { + j = IV_GetElement(v, n, i); + log.print(j + " "); + } + log.println(); + } +} + +//------------------------------------------------------------------------------ diff --git a/prism/src/dv/Makefile b/prism/src/dv/Makefile index b5ee3a48..84baba28 100644 --- a/prism/src/dv/Makefile +++ b/prism/src/dv/Makefile @@ -35,7 +35,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)/DoubleVector.h $(PRISM_DIR_REL)/$(LIB_DIR)/$(LIBPREFIX)dv$(LIBSUFFIX) +all: checks $(CLASS_FILES) $(PRISM_DIR_REL)/$(INCLUDE_DIR)/DoubleVector.h $(PRISM_DIR_REL)/$(INCLUDE_DIR)/IntegerVector.h $(PRISM_DIR_REL)/$(LIB_DIR)/$(LIBPREFIX)dv$(LIBSUFFIX) # Try and prevent accidental makes (i.e. called manually, not from top-level Makefile) checks: @@ -49,6 +49,9 @@ $(PRISM_DIR_REL)/$(CLASSES_DIR)/$(THIS_DIR)/%.class: %.java $(PRISM_DIR_REL)/$(INCLUDE_DIR)/DoubleVector.h: $(PRISM_DIR_REL)/$(CLASSES_DIR)/$(THIS_DIR)/DoubleVector.class ($(JAVAH) -classpath $(PRISM_DIR_REL)/$(CLASSES_DIR) -jni -o $@ $(THIS_DIR).DoubleVector; touch $@) +$(PRISM_DIR_REL)/$(INCLUDE_DIR)/IntegerVector.h: $(PRISM_DIR_REL)/$(CLASSES_DIR)/$(THIS_DIR)/IntegerVector.class + ($(JAVAH) -classpath $(PRISM_DIR_REL)/$(CLASSES_DIR) -jni -o $@ $(THIS_DIR).IntegerVector; touch $@) + $(PRISM_DIR_REL)/$(LIB_DIR)/$(LIBPREFIX)dv$(LIBSUFFIX): $(O_FILES) $(LD) $(SHARED) $(LDFLAGS) -o $@ $(O_FILES) $(LIBRARIES) diff --git a/prism/src/dv/iv.cc b/prism/src/dv/iv.cc new file mode 100644 index 00000000..79b2d42d --- /dev/null +++ b/prism/src/dv/iv.cc @@ -0,0 +1,133 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Oxford, formerly University of Birmingham) +// Description: C++ code for double vector stuff +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +#include "iv.h" +#include +#include + +// local function prototypes + +static void mtbdd_to_integer_vector_rec(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, int level, ODDNode *odd, long o, int *res); +static DdNode *integer_vector_to_mtbdd_rec(DdManager *ddman, int *vec, DdNode **vars, int num_vars, int level, ODDNode *odd, long o); + +//------------------------------------------------------------------------------ + +// converts an mtbdd representing a vector to an array of integers +// values are cast from double to integer when extracting from the mtbdd +// it is optional whether or not an array is passed in to be used +// if so, it should be the right size (as determined by row->eoff+row->toff) +// if not, a new one is created +// in either the case, a pointer to the array is returned +// throws std::bad_alloc on out-of-memory + +EXPORT int *mtbdd_to_integer_vector(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, ODDNode *odd) +{ + return mtbdd_to_integer_vector(ddman, dd, vars, num_vars, odd, NULL); +} + +EXPORT int *mtbdd_to_integer_vector(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, ODDNode *odd, int *res) +{ + int i, n; + + // determine size + n = odd->eoff + odd->toff; + // create array (if not supplied) + if (!res) res = new int[n]; + // initialise to zero + for (i = 0; i < n; i++) { + res[i] = 0.0; + } + // build array recursively + mtbdd_to_integer_vector_rec(ddman, dd, vars, num_vars, 0, odd, 0, res); + + return res; +} + +void mtbdd_to_integer_vector_rec(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, int level, ODDNode *odd, long o, int *res) +{ + DdNode *e, *t; + + if (dd == Cudd_ReadZero(ddman)) return; + + if (level == num_vars) { + res[o] = (int) Cudd_V(dd); + return; + } + else if (dd->index > vars[level]->index) { + e = t = dd; + } + else { + e = Cudd_E(dd); + t = Cudd_T(dd); + } + + mtbdd_to_integer_vector_rec(ddman, e, vars, num_vars, level+1, odd->e, o, res); + mtbdd_to_integer_vector_rec(ddman, t, vars, num_vars, level+1, odd->t, o+odd->eoff, res); +} + +//------------------------------------------------------------------------------ + +// converts an array of integers to an mtbdd + +EXPORT DdNode *integer_vector_to_mtbdd(DdManager *ddman, int *vec, DdNode **vars, int num_vars, ODDNode *odd) +{ + return integer_vector_to_mtbdd_rec(ddman, vec, vars, num_vars, 0, odd, 0); +} + +DdNode *integer_vector_to_mtbdd_rec(DdManager *ddman, int *vec, DdNode **vars, int num_vars, int level, ODDNode *odd, long o) +{ + DdNode *e, *t; + + if (level == num_vars) { + return DD_Constant(ddman, vec[o]); + } + else { + if (odd->eoff > 0) { + e = integer_vector_to_mtbdd_rec(ddman, vec, vars, num_vars, level+1, odd->e, o); + } + else { + e = DD_Constant(ddman, 0); + } + if (odd->toff > 0) { + t = integer_vector_to_mtbdd_rec(ddman, vec, vars, num_vars, level+1, odd->t, o+odd->eoff); + } + else { + t = DD_Constant(ddman, 0); + } + if (e == t) { + Cudd_RecursiveDeref(ddman, t); + return e; + } + else { + Cudd_Ref(vars[level]); + return DD_ITE(ddman, vars[level], t, e); + } + } +} + +//------------------------------------------------------------------------------ +