effecting the same change in the compat Java binding as was done to CVC3 yesterday (ValidityChecker::value() and ValidityChecker::getValue())

3 files changed, 17 insertions, 5 deletions

diff --git a/src/bindings/compat/java/Makefile.am b/src/bindings/compat/java/Makefile.am
index e99127422..7c22e6231 100644
--- a/src/bindings/compat/java/Makefile.am
+++ b/src/bindings/compat/java/Makefile.am
@@ -132,7 +132,7 @@ $(JNI_CPP_FILES): %.cpp: src/cvc3/%_impl.cpp $(builddir)/cvc3/%.h include/cvc3/J
 		$*.cpp
 
 JniUtils.lo: src/cvc3/JniUtils.cpp .headers
-	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_INCLUDES) -I . -o $@ $<
+	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_INCLUDES) $(JAVA_CPPFLAGS) -I . -o $@ $<
 
 $(LIB_FILES:%=classes/cvc3/%.class): .classes
 .classes:
diff --git a/src/bindings/compat/java/src/cvc3/ValidityChecker.java b/src/bindings/compat/java/src/cvc3/ValidityChecker.java
index 1ddac6a0b..7407d0251 100644
--- a/src/bindings/compat/java/src/cvc3/ValidityChecker.java
+++ b/src/bindings/compat/java/src/cvc3/ValidityChecker.java
@@ -383,8 +383,10 @@ public class ValidityChecker extends Embedded {
 	jniGetCounterExample(Object ValidityChecker, boolean inOrder) throws Cvc3Exception;
     private static native Object[]
 	jniGetConcreteModel(Object ValidityChecker) throws Cvc3Exception;
-    private static native String
+    private static native Object
 	jniGetValue(Object ValidityChecker, Object Expr) throws Cvc3Exception;
+    private static native String
+	jniValue(Object ValidityChecker, Object Expr) throws Cvc3Exception;
     private static native boolean
 	jniInconsistent1(Object ValidityChecker) throws Cvc3Exception;
     private static native Object[]
@@ -1591,8 +1593,14 @@ public class ValidityChecker extends Embedded {
 	return JniUtils.embedHashMap(model, Expr.class, Expr.class, embeddedManager());
     }
 
-    public FormulaValue getValue(Expr expr) throws Cvc3Exception {
-	return FormulaValue.get(jniGetValue(embedded(), expr.embedded()));
+    public FormulaValue value(Expr expr) throws Cvc3Exception {
+	return FormulaValue.get(jniValue(embedded(), expr.embedded()));
+    }
+
+    public Expr getValue(Expr expr) throws Cvc3Exception {
+	return new ExprMut(
+	  jniGetValue(embedded(), expr.embedded()),
+	  embeddedManager());
     }
 
     public boolean inconsistent() throws Cvc3Exception {
diff --git a/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp b/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp
index d74af5460..e27e44913 100644
--- a/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp
+++ b/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp
@@ -733,10 +733,14 @@ vector<Expr> result;
 vc->getCounterExample(result, inOrder);
 return toJavaVCopy(env, result);
 
-DEFINITION: Java_cvc3_ValidityChecker_jniGetValue
+DEFINITION: Java_cvc3_ValidityChecker_jniValue
 jstring m ValidityChecker vc c Expr expr
 return toJava(env, vc->value(*expr));
 
+DEFINITION: Java_cvc3_ValidityChecker_jniGetValue
+jobject m ValidityChecker vc c Expr expr
+return embed_copy(env, vc->getValue(*expr));
+
 DEFINITION: Java_cvc3_ValidityChecker_jniGetConcreteModel
 jobjectArray m ValidityChecker vc
 ExprMap<Expr> result;