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 | |
parent | 0e3f99d90a5fcafd04b04adf0d3e7e71ccfa65b0 (diff) |
Removing throw specifiers from OutputChannel and subclasses. (#1209)
Diffstat (limited to 'src/theory')
-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 |
4 files changed, 103 insertions, 151 deletions
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 */ |