diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/theory/theory_engine_white.h | 40 | ||||
-rw-r--r-- | test/unit/theory/theory_white.h | 69 |
2 files changed, 30 insertions, 79 deletions
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index cf1712534..9e99ce884 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -52,40 +52,20 @@ using namespace CVC4::theory::bv; using namespace std; class FakeOutputChannel : public OutputChannel { - void conflict(TNode n, Proof* pf = NULL) throw(AssertionException) { + void conflict(TNode n, Proof* pf) override { Unimplemented(); } + bool propagate(TNode n) override { Unimplemented(); } + LemmaStatus lemma(TNode n, ProofRule rule, bool removable, bool preprocess, + bool sendAtoms) override { Unimplemented(); } - bool propagate(TNode n) throw(AssertionException) { + void requirePhase(TNode, bool) override { Unimplemented(); } + bool flipDecision() override { Unimplemented(); } + void setIncomplete() override { Unimplemented(); } + void handleUserAttribute(const char* attr, Theory* t) override { Unimplemented(); } - void propagateAsDecision(TNode n) throw(AssertionException) { - Unimplemented(); - } - LemmaStatus lemma(TNode n, ProofRule rule, - bool removable, - bool preprocess, - bool sendAtoms) throw(AssertionException) { - Unimplemented(); - } - void requirePhase(TNode, bool) throw(AssertionException) { - Unimplemented(); - } - bool flipDecision() throw(AssertionException) { - Unimplemented(); - } - void explanation(TNode n) throw(AssertionException) { - Unimplemented(); - } - void setIncomplete() throw(AssertionException) { - Unimplemented(); - } - void handleUserAttribute( const char* attr, Theory* t ){ - Unimplemented(); - } - LemmaStatus splitLemma(TNode n, bool removable) throw(TypeCheckingExceptionPrivate, AssertionException){ - Unimplemented(); - } -};/* class FakeOutputChannel */ + LemmaStatus splitLemma(TNode n, bool removable) override { Unimplemented(); } +}; /* class FakeOutputChannel */ template<TheoryId theory> class FakeTheory; diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h index 85d1a1c02..d1517d7c2 100644 --- a/test/unit/theory/theory_white.h +++ b/test/unit/theory/theory_white.h @@ -41,83 +41,54 @@ using namespace std; */ enum OutputChannelCallType{CONFLICT, PROPAGATE, LEMMA, EXPLANATION}; class TestOutputChannel : public OutputChannel { -private: - void push(OutputChannelCallType call, TNode n) { - d_callHistory.push_back(make_pair(call, n)); - } - -public: - vector< pair<OutputChannelCallType, Node> > d_callHistory; - + public: TestOutputChannel() {} + ~TestOutputChannel() override {} - ~TestOutputChannel() {} - - void safePoint(uint64_t amount) - throw(Interrupted, UnsafeInterruptException, AssertionException) - {} + void safePoint(uint64_t amount) override {} - void conflict(TNode n, Proof* pf = NULL) - throw(AssertionException) { + void conflict(TNode n, Proof* pf = nullptr) override { push(CONFLICT, n); } - bool propagate(TNode n) - throw(AssertionException) { + bool propagate(TNode n) override { push(PROPAGATE, n); return true; } - void propagateAsDecision(TNode n) - throw(AssertionException) { - // ignore - } - - LemmaStatus lemma(TNode n, ProofRule rule, - bool removable = false, - bool preprocess = false, - bool sendAtoms = false) - throw(AssertionException) { + LemmaStatus lemma(TNode n, ProofRule rule, bool removable = false, + bool preprocess = false, bool sendAtoms = false) override { push(LEMMA, n); return LemmaStatus(Node::null(), 0); } - LemmaStatus splitLemma(TNode n, bool removable) throw (TypeCheckingExceptionPrivate, AssertionException){ + LemmaStatus splitLemma(TNode n, bool removable) override { push(LEMMA, n); return LemmaStatus(Node::null(), 0); } - void requirePhase(TNode, bool) - throw(Interrupted, AssertionException) { - Unreachable(); - } + void requirePhase(TNode, bool) override { Unreachable(); } + bool flipDecision() override { Unreachable(); } + void setIncomplete() override { Unreachable(); } - bool flipDecision() - throw(Interrupted, AssertionException) { - Unreachable(); - } + void clear() { d_callHistory.clear(); } - void setIncomplete() - throw(AssertionException) { - Unreachable(); - } - - void clear() { - d_callHistory.clear(); - } - - Node getIthNode(int i) { + 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(); } + + private: + void push(OutputChannelCallType call, TNode n) { + d_callHistory.push_back(make_pair(call, n)); } + vector<pair<OutputChannelCallType, Node> > d_callHistory; }; class DummyTheory : public Theory { |