From 044e20567fa7252be33aa0108b2f795b8181fb04 Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 18 Nov 2016 15:17:31 -0800 Subject: [PATCH] Removing some throw specifiers from OutputChannel. Fixes bug 716. --- src/proof/proof_output_channel.cpp | 8 ++++--- src/proof/proof_output_channel.h | 14 +++++------ src/theory/output_channel.h | 13 ++++------- src/theory/theory_engine.cpp | 37 +++++++++++++++--------------- src/theory/theory_engine.h | 5 ++-- 5 files changed, 37 insertions(+), 40 deletions(-) diff --git a/src/proof/proof_output_channel.cpp b/src/proof/proof_output_channel.cpp index 6d729db1f..c87ccd37c 100644 --- a/src/proof/proof_output_channel.cpp +++ b/src/proof/proof_output_channel.cpp @@ -26,18 +26,20 @@ void ProofOutputChannel::conflict(TNode n, Proof* pf) throw() { } bool ProofOutputChannel::propagate(TNode x) throw() { - Trace("pf::tp") << "ProofOutputChannel: got a propagation: " << x << std::endl; + Trace("pf::tp") << "ProofOutputChannel: got a propagation: " << x + << std::endl; d_propagations.insert(x); return true; } -theory::LemmaStatus ProofOutputChannel::lemma(TNode n, ProofRule rule, bool, bool, bool) throw() { +theory::LemmaStatus ProofOutputChannel::lemma(TNode n, ProofRule rule, bool, + bool, bool) { Trace("pf::tp") << "ProofOutputChannel: new lemma: " << n << std::endl; d_lemma = n; return theory::LemmaStatus(TNode::null(), 0); } -theory::LemmaStatus ProofOutputChannel::splitLemma(TNode, bool) throw() { +theory::LemmaStatus ProofOutputChannel::splitLemma(TNode, bool) { AlwaysAssert(false); return theory::LemmaStatus(TNode::null(), 0); } diff --git a/src/proof/proof_output_channel.h b/src/proof/proof_output_channel.h index b85af5fb5..b44689fe5 100644 --- a/src/proof/proof_output_channel.h +++ b/src/proof/proof_output_channel.h @@ -24,13 +24,13 @@ public: virtual ~ProofOutputChannel() throw() {} - void conflict(TNode n, Proof* pf) throw(); - bool propagate(TNode x) throw(); - theory::LemmaStatus lemma(TNode n, ProofRule rule, bool, bool, bool) throw(); - theory::LemmaStatus splitLemma(TNode, bool) throw(); - void requirePhase(TNode n, bool b) throw(); - bool flipDecision() throw(); - void setIncomplete() 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 MyPreRegisterVisitor { diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 639793c7f..4ca113eed 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -101,7 +101,7 @@ public: * unit conflict) which is assigned TRUE (and T-conflicting) in the * current assignment. * @param pf - a proof of the conflict. This is only non-null if proofs - * are enabled. + * are enabled. */ virtual void conflict(TNode n, Proof* pf = NULL) throw(AssertionException, UnsafeInterruptException) = 0; @@ -128,17 +128,15 @@ public: virtual LemmaStatus lemma(TNode n, ProofRule rule, bool removable = false, bool preprocess = false, - bool sendAtoms = false) - throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0; + bool sendAtoms = false) = 0; /** * Variant of the lemma function that does not require providing a proof rule. */ - virtual LemmaStatus lemma(TNode n, + virtual LemmaStatus lemma(TNode n, bool removable = false, bool preprocess = false, - bool sendAtoms = false) - throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { + bool sendAtoms = false) { return lemma(n, RULE_INVALID, removable, preprocess, sendAtoms); } @@ -153,8 +151,7 @@ public: return splitLemma(n.orNode(n.notNode())); } - virtual LemmaStatus splitLemma(TNode n, bool removable = false) - throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0; + virtual LemmaStatus splitLemma(TNode n, bool removable = false) = 0; /** * If a decision is made on n, it must be in the phase specified. diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index c21aa5445..5ef768fd3 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -77,22 +77,18 @@ theory::LemmaStatus TheoryEngine::EngineOutputChannel::lemma(TNode lemma, ProofRule rule, bool removable, bool preprocess, - bool sendAtoms) - throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { - Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << ", preprocess = " << preprocess << std::endl; - ++ d_statistics.lemmas; + bool sendAtoms) { + Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" + << lemma << ")" + << ", preprocess = " << preprocess << std::endl; + ++d_statistics.lemmas; d_engine->d_outputChannelUsed = true; - PROOF({ - registerLemmaRecipe(lemma, lemma, preprocess, d_theory); - }); + PROOF({ registerLemmaRecipe(lemma, lemma, preprocess, d_theory); }); - theory::LemmaStatus result = d_engine->lemma(lemma, - rule, - false, - removable, - preprocess, - sendAtoms ? d_theory : theory::THEORY_LAST); + theory::LemmaStatus result = + d_engine->lemma(lemma, rule, false, removable, preprocess, + sendAtoms ? d_theory : theory::THEORY_LAST); return result; } @@ -179,14 +175,17 @@ void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node ori ProofManager::getCnfProof()->setProofRecipe(&proofRecipe); } -theory::LemmaStatus TheoryEngine::EngineOutputChannel::splitLemma(TNode lemma, bool removable) - throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { - Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; - ++ d_statistics.lemmas; +theory::LemmaStatus TheoryEngine::EngineOutputChannel::splitLemma( + TNode lemma, bool removable) { + Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" + << lemma << ")" << std::endl; + ++d_statistics.lemmas; d_engine->d_outputChannelUsed = true; - Debug("pf::explain") << "TheoryEngine::EngineOutputChannel::splitLemma( " << lemma << " )" << std::endl; - theory::LemmaStatus result = d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory); + Debug("pf::explain") << "TheoryEngine::EngineOutputChannel::splitLemma( " + << lemma << " )" << std::endl; + theory::LemmaStatus result = + d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory); return result; } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index fc98c6e3a..3273b3d19 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -279,10 +279,9 @@ class TheoryEngine { ProofRule rule, bool removable = false, bool preprocess = false, - bool sendAtoms = false) - throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException); + bool sendAtoms = false); - theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException); + theory::LemmaStatus splitLemma(TNode lemma, bool removable = false); void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) { NodeManager* curr = NodeManager::currentNM(); -- 2.30.2