diff options
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. |