diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-11-09 19:18:58 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-11-09 19:18:58 +0000 |
commit | ca6647503475fb36827e960d9e01c3f8a04c4ed3 (patch) | |
tree | b951d83522c8d82709abfcd2707298b3a4916d07 /src/smt/smt_engine.h | |
parent | 63e4a6775daa1b7a986cc9dec0bd178b7e023c47 (diff) |
Bug-fix for a crash involving improperly-thrown exceptions; also, add LogicException for errors where the user uses a feature not permitted in the current logic (e.g., a quantifier in a QF logic)
Diffstat (limited to 'src/smt/smt_engine.h')
-rw-r--r-- | src/smt/smt_engine.h | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index db6084c86..5c383071a 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -28,6 +28,7 @@ #include "expr/expr_manager.h" #include "util/proof.h" #include "smt/modal_exception.h" +#include "smt/logic_exception.h" #include "util/hash.h" #include "options/options.h" #include "util/result.h" @@ -370,20 +371,20 @@ public: * literals and conjunction of literals. Returns false iff * inconsistent. */ - Result assertFormula(const Expr& e) throw(TypeCheckingException); + Result assertFormula(const Expr& e) throw(TypeCheckingException, LogicException); /** * Check validity of an expression with respect to the current set * of assertions by asserting the query expression's negation and * calling check(). Returns valid, invalid, or unknown result. */ - Result query(const Expr& e) throw(TypeCheckingException, ModalException); + Result query(const Expr& e) throw(TypeCheckingException, ModalException, LogicException); /** * Assert a formula (if provided) to the current context and call * check(). Returns sat, unsat, or unknown result. */ - Result checkSat(const Expr& e = Expr()) throw(TypeCheckingException, ModalException); + Result checkSat(const Expr& e = Expr()) throw(TypeCheckingException, ModalException, LogicException); /** * Simplify a formula without doing "much" work. Does not involve @@ -394,20 +395,20 @@ public: * @todo (design) is this meant to give an equivalent or an * equisatisfiable formula? */ - Expr simplify(const Expr& e) throw(TypeCheckingException); + Expr simplify(const Expr& e) throw(TypeCheckingException, LogicException); /** * Expand the definitions in a term or formula. No other * simplification or normalization is done. */ - Expr expandDefinitions(const Expr& e) throw(TypeCheckingException); + Expr expandDefinitions(const Expr& e) throw(TypeCheckingException, LogicException); /** * Get the assigned value of an expr (only if immediately preceded * by a SAT or INVALID query). Only permitted if the SmtEngine is * set to operate interactively and produce-models is on. */ - Expr getValue(const Expr& e) throw(ModalException); + Expr getValue(const Expr& e) throw(ModalException, LogicException); /** * Add a function to the set of expressions whose value is to be @@ -443,7 +444,7 @@ public: /** * Push a user-level context. */ - void push() throw(ModalException); + void push() throw(ModalException, LogicException); /** * Pop a user-level context. Throws an exception if nothing to pop. |