diff options
Diffstat (limited to 'src/smt/smt_engine.h')
| -rw-r--r-- | src/smt/smt_engine.h | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index f1ce2e0e9..d17dd204b 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -394,7 +394,7 @@ class CVC4_PUBLIC SmtEngine { * or INVALID query). Only permitted if CVC4 was built with model * support and produce-models is on. */ - Model* getModel() throw(ModalException, UnsafeInterruptException); + Model* getModel(); // disallow copy/assignment SmtEngine(const SmtEngine&) CVC4_UNDEFINED; @@ -443,8 +443,7 @@ public: /** * Query information about the SMT environment. */ - CVC4::SExpr getInfo(const std::string& key) const - throw(OptionException, ModalException); + CVC4::SExpr getInfo(const std::string& key) const; /** * Set an aspect of the current SMT execution environment. @@ -533,21 +532,21 @@ public: * this function returns true if the expression was added and false * if this request was ignored. */ - bool addToAssignment(const Expr& e) throw(); + bool addToAssignment(const Expr& e); /** * Get the assignment (only if immediately preceded by a SAT or * INVALID query). Only permitted if the SmtEngine is set to * operate interactively and produce-assignments is on. */ - CVC4::SExpr getAssignment() throw(ModalException, UnsafeInterruptException); + CVC4::SExpr getAssignment(); /** * Get the last proof (only if immediately preceded by an UNSAT * or VALID query). Only permitted if CVC4 was built with proof * support and produce-proofs is on. */ - Proof* getProof() throw(ModalException, UnsafeInterruptException); + Proof* getProof(); /** * Print all instantiations made by the quantifiers module. @@ -580,13 +579,13 @@ public: * UNSAT or VALID query). Only permitted if CVC4 was built with * unsat-core support and produce-unsat-cores is on. */ - UnsatCore getUnsatCore() throw(ModalException, UnsafeInterruptException); + UnsatCore getUnsatCore(); /** * Get the current set of assertions. Only permitted if the * SmtEngine is set to operate interactively. */ - std::vector<Expr> getAssertions() throw(ModalException); + std::vector<Expr> getAssertions(); /** * Push a user-level context. @@ -596,7 +595,7 @@ public: /** * Pop a user-level context. Throws an exception if nothing to pop. */ - void pop() throw(ModalException, UnsafeInterruptException); + void pop(); /** * Completely reset the state of the solver, as though destroyed and |