From f7eb28b85addc21ad55952c0cb00b9e5127beced Mon Sep 17 00:00:00 2001 From: Morgan Deters 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 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 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() ? TRUE_VAL : FALSE_VAL; + try { + return d_smt->getValue(e).getConst() ? 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& 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