Tidy, document and expand Integer/DoubleVector classes.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7168 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/include/DoubleVector.h

@@ -47,6 +47,14 @@ JNIEXPORT jdouble JNICALL Java_dv_DoubleVector_DV_1GetElement
 JNIEXPORT void JNICALL Java_dv_DoubleVector_DV_1SetElement
   (JNIEnv *, jobject, jlong, jint, jint, jdouble);
 
+/*
+ * Class:     dv_DoubleVector
+ * Method:    DV_SetAllElements
+ * Signature: (JID)V
+ */
+JNIEXPORT void JNICALL Java_dv_DoubleVector_DV_1SetAllElements
+  (JNIEnv *, jobject, jlong, jint, jdouble);
+
 /*
  * Class:     dv_DoubleVector
  * Method:    DV_RoundOff

prism/include/IntegerVector.h

@@ -39,6 +39,14 @@ JNIEXPORT jint JNICALL Java_dv_IntegerVector_IV_1GetElement
 JNIEXPORT void JNICALL Java_dv_IntegerVector_IV_1SetElement
   (JNIEnv *, jobject, jlong, jint, jint, jint);
 
+/*
+ * Class:     dv_IntegerVector
+ * Method:    IV_SetAllElements
+ * Signature: (JII)V
+ */
+JNIEXPORT void JNICALL Java_dv_IntegerVector_IV_1SetAllElements
+  (JNIEnv *, jobject, jlong, jint, jint);
+
 /*
  * Class:     dv_IntegerVector
  * Method:    IV_Clear

prism/src/dv/DoubleVector.cc

@@ -132,6 +132,22 @@ jdouble d
 
 //------------------------------------------------------------------------------
 
+JNIEXPORT void JNICALL Java_dv_DoubleVector_DV_1SetAllElements
+(
+JNIEnv *env,
+jobject obj,
+jlong __jlongpointer v,
+jint n,
+jdouble d
+)
+{
+	double *vector = jlong_to_double(v);
+	for(int i = 0; i < n; i++)
+		vector[i] = d;
+}
+
+//------------------------------------------------------------------------------
+
 JNIEXPORT void JNICALL Java_dv_DoubleVector_DV_1RoundOff
 (
 JNIEnv *env,

prism/src/dv/DoubleVector.java

@@ -36,7 +36,7 @@ import odd.*;
 public class DoubleVector
 {
 	//------------------------------------------------------------------------------
-	// load jni stuff from shared library
+	// Load JNI stuff from shared library
 	//------------------------------------------------------------------------------
 
 	static
@@ -51,20 +51,21 @@ public class DoubleVector
 	}
 	
 	//------------------------------------------------------------------------------
-	// cudd manager
+	// CUDD manager
 	//------------------------------------------------------------------------------
 
-	// cudd manager
+	// CUDD manager
 	
-	// jni method to set cudd manager for native code
-	private static native void DV_SetCUDDManager(long ddm);
+	// JNI method to set CUDD manager for native code
 	public static void setCUDDManager()
 	{
 		DV_SetCUDDManager(JDD.GetCUDDManager());
 	}
 	
+	private static native void DV_SetCUDDManager(long ddm);
+	
 	//------------------------------------------------------------------------------
-	// instance variables/methods
+	// Instance variables/methods
 	//------------------------------------------------------------------------------
 
 	/**
@@ -76,7 +77,7 @@ public class DoubleVector
 	 */
 	private int n;
 	
-	// constructors
+	// Constructors
 	
 	/**
 	 * Create a new DoubleVector of size {@code size} with all entries set to 0.
@@ -111,32 +112,56 @@ public class DoubleVector
 	
 	private native long DV_ConvertMTBDD(long dd, long vars, int num_vars, long odd);
 
-	// get methods
+	// Accessors
 	
+	/**
+	 * Get the pointer to the native vector (C/C++ pointer cast to a long).
+	 */
 	public long getPtr()
 	{
 		return v;
 	}
 
+	/**
+	 * Get the size of the vector.
+	 */
 	public int getSize()
 	{
 		return n;
 	}
 
-	// get element
-	private native double DV_GetElement(long v, int n, int i);
+	/**
+	 * Get element {@code i} of the vector.
+	 */
 	public double getElement(int i)
 	{
 		return DV_GetElement(v, n, i);
 	}
 
-	// set element
-	private native void DV_SetElement(long v, int n, int i, double d);
+	private native double DV_GetElement(long v, int n, int i);
+	
+	// Mutators
+	
+	/**
+	 * Set element {@code i} of the vector to value {@code d}.
+	 */
 	public void setElement(int i, double d)
 	{
 		DV_SetElement(v, n, i, d);
 	}
 
+	private native void DV_SetElement(long v, int n, int i, double d);
+	
+	/**
+	 * Set all elements of the vector to the same value {@code d}.
+	 */
+	public void setAllElements(double d)
+	{
+		DV_SetAllElements(v, n, d);
+	}
+
+	private native void DV_SetAllElements(long v, int n, double d);
+	
 	// round off
 	private native void DV_RoundOff(long v, int n, int places);
 	public void roundOff(int places)

prism/src/dv/IntegerVector.cc

@@ -113,6 +113,22 @@ jint j
 
 //------------------------------------------------------------------------------
 
+JNIEXPORT void JNICALL Java_dv_IntegerVector_IV_1SetAllElements
+(
+JNIEnv *env,
+jobject obj,
+jlong __jlongpointer v,
+jint n,
+jint j
+)
+{
+	int *vector = (int *) jlong_to_ptr(v);
+	for(int i = 0; i < n; i++)
+		vector[i] = j;
+}
+
+//------------------------------------------------------------------------------
+
 JNIEXPORT void JNICALL Java_dv_IntegerVector_IV_1Clear
 (
 JNIEnv *env,
@@ -121,7 +137,7 @@ jlong __jlongpointer vector
 )
 {
 	// note we assume that this memory was created with new
-	delete (int *) jlong_to_ptr(vector);
+	if (vector) delete (int *) jlong_to_ptr(vector);
 }
 
 //------------------------------------------------------------------------------

prism/src/dv/IntegerVector.java

@@ -36,7 +36,7 @@ import odd.*;
 public class IntegerVector
 {
 	//------------------------------------------------------------------------------
-	// load jni stuff from shared library
+	// Load JNI stuff from shared library
 	//------------------------------------------------------------------------------
 
 	static
@@ -51,7 +51,7 @@ public class IntegerVector
 	}
 	
 	//------------------------------------------------------------------------------
-	// instance variables/methods
+	// Instance variables/methods
 	//------------------------------------------------------------------------------
 
 	/**
@@ -63,7 +63,7 @@ public class IntegerVector
 	 */
 	private int n;
 	
-	// constructors
+	// Constructors
 	
 	/**
 	 * Create a new IntegerVector of size {@code size} with all entries set to 0.
@@ -87,47 +87,80 @@ public class IntegerVector
 		n = size;
 	}
 	
-	private native long IV_ConvertMTBDD(long dd, long vars, int num_vars, long odd);
+	/**
+	 * Create a new DoubleVector from an existing MTBDD representation of an array.
+	 */
 	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
+	private native long IV_ConvertMTBDD(long dd, long vars, int num_vars, long odd);
+	
+	// Accessors
 	
+	/**
+	 * Get the pointer to the native vector (C/C++ pointer cast to a long).
+	 */
 	public long getPtr()
 	{
 		return v;
 	}
 
+	/**
+	 * Get the size of the vector.
+	 */
 	public int getSize()
 	{
 		return n;
 	}
 
-	// get element
-	private native int IV_GetElement(long v, int n, int i);
+	/**
+	 * Get element {@code i} of the vector.
+	 */
 	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);
+	private native int IV_GetElement(long v, int n, int i);
+	
+	// Mutators
+	
+	/**
+	 * Set element {@code i} of the vector to value {@code j}.
+	 */
 	public void setElement(int i, int j)
 	{
 		IV_SetElement(v, n, i, j);
 	}
 
-	// clear (free memory)
-	private native void IV_Clear(long v);
+	private native void IV_SetElement(long v, int n, int i, int j);
+	
+	/**
+	 * Set all elements of the vector to the same value {@code j}.
+	 */
+	public void setAllElements(int j)
+	{
+		IV_SetAllElements(v, n, j);
+	}
+
+	private native void IV_SetAllElements(long v, int n, int j);
+	
+	/**
+	 * Clear storage of the vector.
+	 */
 	public void clear() 
 	{
 		IV_Clear(v);
 	}
 
-	// print (all, including nonzeros)
+	private native void IV_Clear(long v);
+	
+	/**
+	 * Print the (all elements, including non-zeros) to a log.
+	 */
 	public void print(PrismLog log)
 	{
 		int i, j;