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

1 files changed, 4 insertions, 0 deletions

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