From f7eb28b85addc21ad55952c0cb00b9e5127beced Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 27 Jan 2012 20:00:54 +0000
Subject: [PATCH] effecting the same change in the compat Java binding as was
 done to CVC3 yesterday (ValidityChecker::value() and
 ValidityChecker::getValue())

---
 src/bindings/compat/java/Makefile.am              |  2 +-
 .../compat/java/src/cvc3/ValidityChecker.java     | 14 +++++++++++---
 .../compat/java/src/cvc3/ValidityChecker_impl.cpp |  6 +++++-
 src/compat/cvc3_compat.cpp                        | 15 ++++++++++++++-
 src/compat/cvc3_compat.h                          |  4 ++++
 5 files changed, 35 insertions(+), 6 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;
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index a5d85821d..a30ccb27d 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -1950,7 +1950,20 @@ QueryResult ValidityChecker::tryModelGeneration() {
 
 FormulaValue ValidityChecker::value(const Expr& e) {
   CheckArgument(e.getType() == d_em->booleanType(), e, "argument must be a formula");
-  return d_smt->getValue(e).getConst<bool>() ? TRUE_VAL : FALSE_VAL;
+  try {
+    return d_smt->getValue(e).getConst<bool>() ? TRUE_VAL : FALSE_VAL;
+  } catch(CVC4::Exception& e) {
+    return UNKNOWN_VAL;
+  }
+}
+
+Expr ValidityChecker::getValue(const Expr& e) {
+  try {
+    return d_smt->getValue(e);
+  } catch(CVC4::ModalException& e) {
+    // by contract, we return null expr
+    return Expr();
+  }
 }
 
 bool ValidityChecker::inconsistent(std::vector<Expr>& assumptions) {
diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h
index 71bea5cf8..beef53006 100644
--- a/src/compat/cvc3_compat.h
+++ b/src/compat/cvc3_compat.h
@@ -1355,6 +1355,10 @@ public:
   */
   virtual Proof getProof();
 
+  //! Evaluate an expression and return a concrete value in the model
+  /*! If the last query was not invalid, should return NULL expr */
+  virtual Expr getValue(const Expr& e);
+
   //! Returns the TCC of the last assumption or query
   /*! Returns Null if no assumptions or queries were performed. */
   virtual Expr getTCC();
-- 
2.30.2