diff options
Diffstat (limited to 'src/compat/cvc3_compat.h')
| -rw-r--r-- | src/compat/cvc3_compat.h | 4 |
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(); |