summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.h
diff options
context:
space:
mode:
authorAndres Notzli <andres.noetzli@gmail.com>2017-03-29 23:27:56 +0200
committerAndres Notzli <andres.noetzli@gmail.com>2017-03-30 11:36:14 -0700
commitfaec717e89cfd657daaa370a061f4a8e282b0eff (patch)
tree067f9df357725c07ea7d04a5895801152b5f1a27 /src/smt/smt_engine.h
parent100037d531ff1fd30ed3dd5bed91076c383ad55c (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.h17
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback