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 | |
parent | 0e3f99d90a5fcafd04b04adf0d3e7e71ccfa65b0 (diff) |
Removing throw specifiers from OutputChannel and subclasses. (#1209)
-rw-r--r-- | src/proof/proof_output_channel.cpp | 33 | ||||
-rw-r--r-- | src/proof/proof_output_channel.h | 46 | ||||
-rw-r--r-- | src/proof/theory_proof.cpp | 38 | ||||
-rw-r--r-- | src/theory/output_channel.h | 87 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 20 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 85 | ||||
-rw-r--r-- | src/theory/theory_test_utils.h | 62 | ||||
-rw-r--r-- | test/unit/theory/theory_engine_white.h | 40 | ||||
-rw-r--r-- | test/unit/theory/theory_white.h | 69 |
9 files changed, 208 insertions, 272 deletions
diff --git a/src/proof/proof_output_channel.cpp b/src/proof/proof_output_channel.cpp index 819cc0102..85a742dfa 100644 --- a/src/proof/proof_output_channel.cpp +++ b/src/proof/proof_output_channel.cpp @@ -15,25 +15,32 @@ **/ +#include "proof/proof_output_channel.h" + #include "base/cvc4_assert.h" -#include "proof_output_channel.h" #include "theory/term_registration_visitor.h" #include "theory/valuation.h" namespace CVC4 { -ProofOutputChannel::ProofOutputChannel() : d_conflict(), d_proof(NULL) {} +ProofOutputChannel::ProofOutputChannel() : d_conflict(), d_proof(nullptr) {} + +Proof* ProofOutputChannel::getConflictProof() { + Assert(hasConflict()); + return d_proof; +} -void ProofOutputChannel::conflict(TNode n, Proof* pf) throw() { +void ProofOutputChannel::conflict(TNode n, Proof* pf) { Trace("pf::tp") << "ProofOutputChannel: CONFLICT: " << n << std::endl; - Assert(d_conflict.isNull()); - Assert(!n.isNull()); + Assert(!hasConflict()); + Assert(!d_proof); d_conflict = n; - Assert(pf != NULL); d_proof = pf; + Assert(hasConflict()); + Assert(d_proof); } -bool ProofOutputChannel::propagate(TNode x) throw() { +bool ProofOutputChannel::propagate(TNode x) { Trace("pf::tp") << "ProofOutputChannel: got a propagation: " << x << std::endl; d_propagations.insert(x); @@ -43,6 +50,12 @@ bool ProofOutputChannel::propagate(TNode x) throw() { theory::LemmaStatus ProofOutputChannel::lemma(TNode n, ProofRule rule, bool, bool, bool) { Trace("pf::tp") << "ProofOutputChannel: new lemma: " << n << std::endl; + // TODO(#1231): We should transition to supporting multiple lemmas. The + // following assertion cannot be enabled due to + // "test/regress/regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smt". + // Assert( + // d_lemma.isNull(), + // "Multiple calls to ProofOutputChannel::lemma() are not supported."); d_lemma = n; return theory::LemmaStatus(TNode::null(), 0); } @@ -52,18 +65,18 @@ theory::LemmaStatus ProofOutputChannel::splitLemma(TNode, bool) { return theory::LemmaStatus(TNode::null(), 0); } -void ProofOutputChannel::requirePhase(TNode n, bool b) throw() { +void ProofOutputChannel::requirePhase(TNode n, bool b) { Debug("pf::tp") << "ProofOutputChannel::requirePhase called" << std::endl; Trace("pf::tp") << "requirePhase " << n << " " << b << std::endl; } -bool ProofOutputChannel::flipDecision() throw() { +bool ProofOutputChannel::flipDecision() { Debug("pf::tp") << "ProofOutputChannel::flipDecision called" << std::endl; AlwaysAssert(false); return false; } -void ProofOutputChannel::setIncomplete() throw() { +void ProofOutputChannel::setIncomplete() { Debug("pf::tp") << "ProofOutputChannel::setIncomplete called" << std::endl; AlwaysAssert(false); } diff --git a/src/proof/proof_output_channel.h b/src/proof/proof_output_channel.h index b114ec25f..9516eb71b 100644 --- a/src/proof/proof_output_channel.h +++ b/src/proof/proof_output_channel.h @@ -16,31 +16,49 @@ #ifndef __CVC4__PROOF_OUTPUT_CHANNEL_H #define __CVC4__PROOF_OUTPUT_CHANNEL_H +#include <set> #include <unordered_set> +#include "expr/node.h" +#include "util/proof.h" #include "theory/output_channel.h" +#include "theory/theory.h" namespace CVC4 { class ProofOutputChannel : public theory::OutputChannel { -public: + public: + ProofOutputChannel(); + ~ProofOutputChannel() override {} + + /** + * This may be called at most once per ProofOutputChannel. + * Requires that `n` and `pf` are non-null. + */ + void conflict(TNode n, Proof* pf) override; + bool propagate(TNode x) override; + theory::LemmaStatus lemma(TNode n, ProofRule rule, bool, bool, bool) override; + theory::LemmaStatus splitLemma(TNode, bool) override; + void requirePhase(TNode n, bool b) override; + bool flipDecision() override; + void setIncomplete() override; + + /** Has conflict() has been called? */ + bool hasConflict() const { return !d_conflict.isNull(); } + + /** + * Returns the proof passed into the conflict() call. + * Requires hasConflict() to hold. + */ + Proof* getConflictProof(); + Node getLastLemma() const { return d_lemma; } + + private: Node d_conflict; Proof* d_proof; Node d_lemma; std::set<Node> d_propagations; - - ProofOutputChannel(); - - virtual ~ProofOutputChannel() throw() {} - - virtual void conflict(TNode n, Proof* pf) throw(); - virtual bool propagate(TNode x) throw(); - virtual theory::LemmaStatus lemma(TNode n, ProofRule rule, bool, bool, bool); - virtual theory::LemmaStatus splitLemma(TNode, bool); - virtual void requirePhase(TNode n, bool b) throw(); - virtual bool flipDecision() throw(); - virtual void setIncomplete() throw(); -};/* class ProofOutputChannel */ +}; /* class ProofOutputChannel */ class MyPreRegisterVisitor { theory::Theory* d_theory; diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 7dee924be..62dcd0006 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -1021,31 +1021,32 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma, th->check(theory::Theory::EFFORT_FULL); Debug("pf::tp") << "TheoryProof::printTheoryLemmaProof - th->check() DONE" << std::endl; - if(oc.d_conflict.isNull()) { + if(!oc.hasConflict()) { Trace("pf::tp") << "; conflict is null" << std::endl; - Assert(!oc.d_lemma.isNull()); - Trace("pf::tp") << "; ++ but got lemma: " << oc.d_lemma << std::endl; + Node lastLemma = oc.getLastLemma(); + Assert(!lastLemma.isNull()); + Trace("pf::tp") << "; ++ but got lemma: " << lastLemma << std::endl; - if (oc.d_lemma.getKind() == kind::OR) { + if (lastLemma.getKind() == kind::OR) { Debug("pf::tp") << "OR lemma. Negating each child separately" << std::endl; - for (unsigned i = 0; i < oc.d_lemma.getNumChildren(); ++i) { - if (oc.d_lemma[i].getKind() == kind::NOT) { - Trace("pf::tp") << "; asserting fact: " << oc.d_lemma[i][0] << std::endl; - th->assertFact(oc.d_lemma[i][0], false); + for (unsigned i = 0; i < lastLemma.getNumChildren(); ++i) { + if (lastLemma[i].getKind() == kind::NOT) { + Trace("pf::tp") << "; asserting fact: " << lastLemma[i][0] << std::endl; + th->assertFact(lastLemma[i][0], false); } else { - Trace("pf::tp") << "; asserting fact: " << oc.d_lemma[i].notNode() << std::endl; - th->assertFact(oc.d_lemma[i].notNode(), false); + Trace("pf::tp") << "; asserting fact: " << lastLemma[i].notNode() << std::endl; + th->assertFact(lastLemma[i].notNode(), false); } } - } - else { + } else { Unreachable(); - Assert(oc.d_lemma.getKind() == kind::NOT); + Assert(oc.getLastLemma().getKind() == kind::NOT); Debug("pf::tp") << "NOT lemma" << std::endl; - Trace("pf::tp") << "; asserting fact: " << oc.d_lemma[0] << std::endl; - th->assertFact(oc.d_lemma[0], false); + Trace("pf::tp") << "; asserting fact: " << oc.getLastLemma()[0] + << std::endl; + th->assertFact(oc.getLastLemma()[0], false); } // Trace("pf::tp") << "; ++ but got lemma: " << oc.d_lemma << std::endl; @@ -1054,10 +1055,11 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma, // th->check(theory::Theory::EFFORT_FULL); + } else { + Debug("pf::tp") << "Calling oc.d_proof->toStream(os)" << std::endl; + oc.getConflictProof()->toStream(os, map); + Debug("pf::tp") << "Calling oc.d_proof->toStream(os) -- DONE!" << std::endl; } - Debug("pf::tp") << "Calling oc.d_proof->toStream(os)" << std::endl; - oc.d_proof->toStream(os, map); - Debug("pf::tp") << "Calling oc.d_proof->toStream(os) -- DONE!" << std::endl; Debug("pf::tp") << "About to delete the theory solver used for proving the lemma... " << std::endl; delete th; diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 355936d77..2c11097db 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -20,9 +20,10 @@ #define __CVC4__THEORY__OUTPUT_CHANNEL_H #include "base/cvc4_assert.h" +#include "proof/proof_manager.h" #include "smt/logic_exception.h" #include "theory/interrupted.h" -#include "proof/proof_manager.h" +#include "util/proof.h" #include "util/resource_manager.h" namespace CVC4 { @@ -36,14 +37,9 @@ class Theory; * for inspection and the user-level at which the lemma will reside. */ class LemmaStatus { - Node d_rewrittenLemma; - unsigned d_level; - -public: - LemmaStatus(TNode rewrittenLemma, unsigned level) : - d_rewrittenLemma(rewrittenLemma), - d_level(level) { - } + public: + LemmaStatus(TNode rewrittenLemma, unsigned level) + : d_rewrittenLemma(rewrittenLemma), d_level(level) {} /** Get the T-rewritten form of the lemma. */ TNode getRewrittenLemma() const throw() { return d_rewrittenLemma; } @@ -55,41 +51,39 @@ public: */ unsigned getLevel() const throw() { return d_level; } -};/* class LemmaStatus */ + private: + Node d_rewrittenLemma; + unsigned d_level; +}; /* class LemmaStatus */ /** * Generic "theory output channel" interface. + * + * All methods can throw unrecoverable CVC4::Exception's unless otherwise + * documented. */ class OutputChannel { - /** Disallow copying: private constructor */ - OutputChannel(const OutputChannel&) CVC4_UNDEFINED; - - /** Disallow assignment: private operator=() */ - OutputChannel& operator=(const OutputChannel&) CVC4_UNDEFINED; - -public: - - /** - * Construct an OutputChannel. - */ - OutputChannel() { - } + public: + /** Construct an OutputChannel. */ + OutputChannel() {} /** * Destructs an OutputChannel. This implementation does nothing, * but we need a virtual destructor for safety in case subclasses * have a destructor. */ - virtual ~OutputChannel() { - } + virtual ~OutputChannel() {} + + OutputChannel(const OutputChannel&) = delete; + OutputChannel& operator=(const OutputChannel&) = delete; /** * With safePoint(), the theory signals that it is at a safe point * and can be interrupted. + * + * @throws Interrupted if the theory can be safely interrupted. */ - virtual void safePoint(uint64_t amount) - throw(Interrupted, UnsafeInterruptException, AssertionException) - {} + virtual void safePoint(uint64_t amount) {} /** * Indicate a theory conflict has arisen. @@ -103,7 +97,7 @@ public: * @param pf - a proof of the conflict. This is only non-null if proofs * are enabled. */ - virtual void conflict(TNode n, Proof* pf = NULL) throw(AssertionException, UnsafeInterruptException) = 0; + virtual void conflict(TNode n, Proof* pf = nullptr) = 0; /** * Propagate a theory literal. @@ -111,7 +105,7 @@ public: * @param n - a theory consequence at the current decision level * @return false if an immediate conflict was encountered */ - virtual bool propagate(TNode n) throw(AssertionException, UnsafeInterruptException) = 0; + virtual bool propagate(TNode n) = 0; /** * Tell the core that a valid theory lemma at decision level 0 has @@ -125,18 +119,15 @@ public: * @return the "status" of the lemma, including user level at which * the lemma resides; the lemma will be removed when this user level pops */ - virtual LemmaStatus lemma(TNode n, ProofRule rule, - bool removable = false, + virtual LemmaStatus lemma(TNode n, ProofRule rule, bool removable = false, bool preprocess = false, bool sendAtoms = false) = 0; /** * Variant of the lemma function that does not require providing a proof rule. */ - virtual LemmaStatus lemma(TNode n, - bool removable = false, - bool preprocess = false, - bool sendAtoms = false) { + virtual LemmaStatus lemma(TNode n, bool removable = false, + bool preprocess = false, bool sendAtoms = false) { return lemma(n, RULE_INVALID, removable, preprocess, sendAtoms); } @@ -146,10 +137,7 @@ public: * * @param n - a theory atom; must be of Boolean type */ - LemmaStatus split(TNode n) - throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { - return splitLemma(n.orNode(n.notNode())); - } + LemmaStatus split(TNode n) { return splitLemma(n.orNode(n.notNode())); } virtual LemmaStatus splitLemma(TNode n, bool removable = false) = 0; @@ -165,8 +153,7 @@ public: * been pre-registered * @param phase - the phase to decide on n */ - virtual void requirePhase(TNode n, bool phase) - throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0; + virtual void requirePhase(TNode n, bool phase) = 0; /** * Flips the most recent unflipped decision to the other phase and @@ -208,15 +195,14 @@ public: * @return true if a decision was flipped; false if no decision * could be flipped, or if the root decision was re-flipped */ - virtual bool flipDecision() - throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0; + virtual bool flipDecision() = 0; /** * Notification from a theory that it realizes it is incomplete at * this context level. If SAT is later determined by the * TheoryEngine, it should actually return an UNKNOWN result. */ - virtual void setIncomplete() throw(AssertionException, UnsafeInterruptException) = 0; + virtual void setIncomplete() = 0; /** * "Spend" a "resource." The meaning is specific to the context in @@ -229,7 +215,7 @@ public: * long-running operations, they cannot rely on resource() to break * out of infinite or intractable computations. */ - virtual void spendResource(unsigned ammount) throw(UnsafeInterruptException) {} + virtual void spendResource(unsigned amount) {} /** * Handle user attribute. @@ -239,16 +225,15 @@ public: */ virtual void handleUserAttribute(const char* attr, Theory* t) {} - /** Demands that the search restart from sat search level 0. * Using this leads to non-termination issues. * It is appropriate for prototyping for theories. */ - virtual void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {} + virtual void demandRestart() {} -};/* class OutputChannel */ +}; /* class OutputChannel */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ +} // namespace theory +} // namespace CVC4 #endif /* __CVC4__THEORY__OUTPUT_CHANNEL_H */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 892b331ea..402ba61ff 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -193,19 +193,21 @@ theory::LemmaStatus TheoryEngine::EngineOutputChannel::splitLemma( return result; } -bool TheoryEngine::EngineOutputChannel::propagate(TNode literal) - throw(AssertionException, UnsafeInterruptException) { - Debug("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl; - ++ d_statistics.propagations; +bool TheoryEngine::EngineOutputChannel::propagate(TNode literal) { + Debug("theory::propagate") << "EngineOutputChannel<" << d_theory + << ">::propagate(" << literal << ")" << std::endl; + ++d_statistics.propagations; d_engine->d_outputChannelUsed = true; return d_engine->propagate(literal, d_theory); } -void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, Proof* pf) - throw(AssertionException, UnsafeInterruptException) { - Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl; - Assert (pf == NULL); // Theory shouldn't be producing proofs yet - ++ d_statistics.conflicts; +void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, + Proof* proof) { + Trace("theory::conflict") + << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode + << ")" << std::endl; + Assert(!proof); // Theory shouldn't be producing proofs yet + ++d_statistics.conflicts; d_engine->d_outputChannelUsed = true; d_engine->conflict(conflictNode, d_theory); } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index a897f9456..6fd7e9e78 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -235,13 +235,11 @@ class TheoryEngine { ~Statistics(); };/* class TheoryEngine::Statistics */ - /** * An output channel for Theory that passes messages * back to a TheoryEngine. */ class EngineOutputChannel : public theory::OutputChannel { - friend class TheoryEngine; /** @@ -254,84 +252,75 @@ class TheoryEngine { */ Statistics d_statistics; - /** - * The theory owning this chanell. - */ + /** The theory owning this channel. */ theory::TheoryId d_theory; - public: + public: + EngineOutputChannel(TheoryEngine* engine, theory::TheoryId theory) + : d_engine(engine), d_statistics(theory), d_theory(theory) {} - EngineOutputChannel(TheoryEngine* engine, theory::TheoryId theory) : - d_engine(engine), - d_statistics(theory), - d_theory(theory) - { - } - - void safePoint(uint64_t ammount) throw(theory::Interrupted, UnsafeInterruptException, AssertionException) { - spendResource(ammount); + void safePoint(uint64_t amount) override { + spendResource(amount); if (d_engine->d_interrupted) { throw theory::Interrupted(); } } - void conflict(TNode conflictNode, Proof* pf = NULL) throw(AssertionException, UnsafeInterruptException); + void conflict(TNode conflictNode, Proof* pf = nullptr) override; + bool propagate(TNode literal) override; - bool propagate(TNode literal) throw(AssertionException, UnsafeInterruptException); + theory::LemmaStatus lemma(TNode lemma, ProofRule rule, + bool removable = false, bool preprocess = false, + bool sendAtoms = false) override; - theory::LemmaStatus lemma(TNode lemma, - ProofRule rule, - bool removable = false, - bool preprocess = false, - bool sendAtoms = false); + theory::LemmaStatus splitLemma(TNode lemma, + bool removable = false) override; - theory::LemmaStatus splitLemma(TNode lemma, bool removable = false); - - void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { + void demandRestart() override { NodeManager* curr = NodeManager::currentNM(); - Node restartVar = curr->mkSkolem("restartVar", - curr->booleanType(), - "A boolean variable asserted to be true to force a restart"); - Trace("theory::restart") << "EngineOutputChannel<" << d_theory << ">::restart(" << restartVar << ")" << std::endl; - ++ d_statistics.restartDemands; + Node restartVar = curr->mkSkolem( + "restartVar", curr->booleanType(), + "A boolean variable asserted to be true to force a restart"); + Trace("theory::restart") + << "EngineOutputChannel<" << d_theory << ">::restart(" << restartVar + << ")" << std::endl; + ++d_statistics.restartDemands; lemma(restartVar, RULE_INVALID, true); } - void requirePhase(TNode n, bool phase) - throw(theory::Interrupted, AssertionException, UnsafeInterruptException) { - Debug("theory") << "EngineOutputChannel::requirePhase(" - << n << ", " << phase << ")" << std::endl; - ++ d_statistics.requirePhase; + void requirePhase(TNode n, bool phase) override { + Debug("theory") << "EngineOutputChannel::requirePhase(" << n << ", " + << phase << ")" << std::endl; + ++d_statistics.requirePhase; d_engine->d_propEngine->requirePhase(n, phase); } - bool flipDecision() - throw(theory::Interrupted, AssertionException, UnsafeInterruptException) { + bool flipDecision() override { Debug("theory") << "EngineOutputChannel::flipDecision()" << std::endl; - ++ d_statistics.flipDecision; + ++d_statistics.flipDecision; return d_engine->d_propEngine->flipDecision(); } - void setIncomplete() throw(AssertionException, UnsafeInterruptException) { + void setIncomplete() override { Trace("theory") << "TheoryEngine::setIncomplete()" << std::endl; d_engine->setIncomplete(d_theory); } - void spendResource(unsigned ammount) throw(UnsafeInterruptException) { - d_engine->spendResource(ammount); + void spendResource(unsigned amount) override { + d_engine->spendResource(amount); } - void handleUserAttribute( const char* attr, theory::Theory* t ){ - d_engine->handleUserAttribute( attr, t ); + void handleUserAttribute(const char* attr, theory::Theory* t) override { + d_engine->handleUserAttribute(attr, t); } - private: - + private: /** * A helper function for registering lemma recipes with the proof engine */ - void registerLemmaRecipe(Node lemma, Node originalLemma, bool preprocess, theory::TheoryId theoryId); - };/* class TheoryEngine::EngineOutputChannel */ + void registerLemmaRecipe(Node lemma, Node originalLemma, bool preprocess, + theory::TheoryId theoryId); + }; /* class TheoryEngine::EngineOutputChannel */ /** * Output channels for individual theories. @@ -475,7 +464,7 @@ public: /** * "Spend" a resource during a search or preprocessing. */ - void spendResource(unsigned ammount); + void spendResource(unsigned amount); /** * Adds a theory. Only one theory per TheoryId can be present, so if 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 */ 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 { |