effecting the same change in the compat Java binding as was done to CVC3 yesterday...

diff --git a/src/bindings/compat/java/Makefile.am b/src/bindings/compat/java/Makefile.am
index e991274220d014dffabefb350d31d7ad545cc74d..7c22e6231cc81c00f6ceebf3cbb5b14784b1748d 100644 (file)
--- 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 1ddac6a0b8cc6a46f7ba8961f17cd6c010547bde..7407d0251826343364c46a74b6a1cac180ece9a2 100644 (file)
--- 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 d74af54600c65fb15a0cf314d8688ef6e4775663..e27e44913ef90097dca6eac991383ef1df8c1364 100644 (file)
--- 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 a5d85821da1a5af2330c723f265a65a93d58d9b2..a30ccb27ded6d7ab6bd6fca6df3cb31de9863ea7 100644 (file)
--- 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 71bea5cf835f6bc38dacf4d40d96110cde0d0569..beef53006d3b0abd9c7d91f7ce788f008ff6cc23 100644 (file)
--- 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();