Browse Source
Add integer vector storage class to dv package.
Add integer vector storage class to dv package.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7114 bbc10eb1-c90d-0410-af57-cb519fbb1720master
Dave Parker
13 years ago
8 changed files with 505 additions and 3 deletions
-
53prism/include/IntegerVector.h
-
53prism/include/iv.h
-
1prism/src/dv/DoubleVector.cc
-
6prism/src/dv/DoubleVector.java
-
127prism/src/dv/IntegerVector.cc
-
130prism/src/dv/IntegerVector.java
-
5prism/src/dv/Makefile
-
133prism/src/dv/iv.cc
@ -0,0 +1,53 @@ |
|||||
|
/* DO NOT EDIT THIS FILE - it is machine generated */ |
||||
|
#include <jni.h> |
||||
|
/* 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 |
||||
@ -0,0 +1,53 @@ |
|||||
|
//============================================================================== |
||||
|
// |
||||
|
// Copyright (c) 2002- |
||||
|
// Authors: |
||||
|
// * Dave Parker <david.parker@comlab.ox.ac.uk> (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 <util.h> |
||||
|
#include <cudd.h> |
||||
|
#include <odd.h> |
||||
|
|
||||
|
// 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 |
||||
|
|
||||
|
//------------------------------------------------------------------------------ |
||||
@ -0,0 +1,127 @@ |
|||||
|
//==============================================================================
|
||||
|
//
|
||||
|
// Copyright (c) 2002-
|
||||
|
// Authors:
|
||||
|
// * Dave Parker <david.parker@comlab.ox.ac.uk> (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 <math.h>
|
||||
|
#include <new>
|
||||
|
|
||||
|
//------------------------------------------------------------------------------
|
||||
|
// 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); |
||||
|
} |
||||
|
|
||||
|
//------------------------------------------------------------------------------
|
||||
@ -0,0 +1,130 @@ |
|||||
|
//============================================================================== |
||||
|
// |
||||
|
// Copyright (c) 2002- |
||||
|
// Authors: |
||||
|
// * Dave Parker <d.a.parker@cs.bham.ac.uk> (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(); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
//------------------------------------------------------------------------------ |
||||
@ -0,0 +1,133 @@ |
|||||
|
//==============================================================================
|
||||
|
//
|
||||
|
// Copyright (c) 2002-
|
||||
|
// Authors:
|
||||
|
// * Dave Parker <david.parker@comlab.ox.ac.uk> (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 <math.h>
|
||||
|
#include <new>
|
||||
|
|
||||
|
// 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); |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
//------------------------------------------------------------------------------
|
||||
|
|
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue