diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-01-27 20:00:54 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-01-27 20:00:54 +0000 |
commit | f7eb28b85addc21ad55952c0cb00b9e5127beced (patch) | |
tree | 0832cb03056873f76eaa3b92631a8c4229c2f835 /src/compat | |
parent | c6654673bfbf2358f2461f7ba3735d9142aa91b7 (diff) |
effecting the same change in the compat Java binding as was done to CVC3 yesterday (ValidityChecker::value() and ValidityChecker::getValue())
Diffstat (limited to 'src/compat')
-rw-r--r-- | src/compat/cvc3_compat.cpp | 15 | ||||
-rw-r--r-- | src/compat/cvc3_compat.h | 4 |
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(); |