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

2 files changed, 18 insertions, 1 deletions

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();