diff options
author | Andres Notzli <andres.noetzli@gmail.com> | 2017-03-29 23:27:56 +0200 |
---|---|---|
committer | Andres Notzli <andres.noetzli@gmail.com> | 2017-03-30 11:36:14 -0700 |
commit | faec717e89cfd657daaa370a061f4a8e282b0eff (patch) | |
tree | 067f9df357725c07ea7d04a5895801152b5f1a27 /src/smt/smt_engine.h | |
parent | 100037d531ff1fd30ed3dd5bed91076c383ad55c (diff) |
[Coverity] Remove throw qualifiers in src/smtremove_throw
Addresses coverity issues:
1172167
1172174
1172176
1172183
1172185
1172186
1172188
1172189
1172191
1172192
1172193
1172194
1172197
1172197
1172198
1172434
1172437
1172438
1172443
1172445
1172446
1172447
1172448
1362695
1362700
1362717
1362736
1362768
1362786
1362811
1379599
1421404
1421405
1421406
1421407
1421408
1421409
1421410
1421411
1421412
1421413
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 |