diff options
author | Tim King <taking@cs.nyu.edu> | 2017-10-25 17:07:01 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2017-10-25 17:07:01 -0700 |
commit | 13c8e4a7b8575142ce9b70747969b71039389dfa (patch) | |
tree | b132e1b95223b2e9aa525388788912037037799a /src/theory/theory_test_utils.h | |
parent | 0e3f99d90a5fcafd04b04adf0d3e7e71ccfa65b0 (diff) |
Removing throw specifiers from OutputChannel and subclasses. (#1209)
Diffstat (limited to 'src/theory/theory_test_utils.h')
-rw-r--r-- | src/theory/theory_test_utils.h | 62 |
1 files changed, 19 insertions, 43 deletions
diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index f5c85fc35..4e0fd3e4d 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -63,85 +63,61 @@ namespace theory { class TestOutputChannel : public theory::OutputChannel { public: - std::vector< std::pair<enum OutputChannelCallType, Node> > d_callHistory; - TestOutputChannel() {} + ~TestOutputChannel() override {} - ~TestOutputChannel() {} - - void safePoint(uint64_t ammount) throw(Interrupted, AssertionException) {} + void safePoint(uint64_t amount) override {} - void conflict(TNode n, Proof* pf = NULL) - throw(AssertionException, UnsafeInterruptException) { + void conflict(TNode n, Proof* pf = nullptr) override { push(CONFLICT, n); } - bool propagate(TNode n) - throw(AssertionException, UnsafeInterruptException) { + bool propagate(TNode n) override { push(PROPAGATE, n); return true; } - void propagateAsDecision(TNode n) - throw(AssertionException, UnsafeInterruptException) { - push(PROPAGATE_AS_DECISION, n); - } - - LemmaStatus lemma(TNode n, ProofRule rule, - bool removable = false, - bool preprocess = false, - bool sendAtoms = false) throw(AssertionException, UnsafeInterruptException) { + LemmaStatus lemma(TNode n, ProofRule rule, bool removable = false, + bool preprocess = false, bool sendAtoms = false) override { push(LEMMA, n); return LemmaStatus(Node::null(), 0); } - void requirePhase(TNode, bool) throw(Interrupted, AssertionException, UnsafeInterruptException) { - } + void requirePhase(TNode, bool) override {} + bool flipDecision() override { return true; } + void setIncomplete() override {} + void handleUserAttribute(const char* attr, theory::Theory* t) override {} - bool flipDecision() throw(Interrupted, AssertionException, UnsafeInterruptException) { - return true; - } - - void setIncomplete() throw(AssertionException, UnsafeInterruptException) { - } - - void handleUserAttribute( const char* attr, theory::Theory* t ) { - } - - void clear() { - d_callHistory.clear(); - } - - LemmaStatus splitLemma(TNode n, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { + LemmaStatus splitLemma(TNode n, bool removable = false) override { push(LEMMA, n); return LemmaStatus(Node::null(), 0); } - Node getIthNode(int i) { + void clear() { d_callHistory.clear(); } + + Node getIthNode(int i) const { Node tmp = (d_callHistory[i]).second; return tmp; } - OutputChannelCallType getIthCallType(int i) { + OutputChannelCallType getIthCallType(int i) const { return (d_callHistory[i]).first; } - unsigned getNumCalls() { - return d_callHistory.size(); - } + unsigned getNumCalls() const { return d_callHistory.size(); } - void printIth(std::ostream& os, int i) { + void printIth(std::ostream& os, int i) const { os << "[TestOutputChannel " << i; os << " " << getIthCallType(i); os << " " << getIthNode(i) << "]"; } -private: - + private: void push(OutputChannelCallType call, TNode n) { d_callHistory.push_back(std::make_pair(call, n)); } + std::vector< std::pair<enum OutputChannelCallType, Node> > d_callHistory; };/* class TestOutputChannel */ }/* CVC4::theory namespace */ |