summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/proof/proof_output_channel.cpp8
-rw-r--r--src/proof/proof_output_channel.h14
-rw-r--r--src/theory/output_channel.h13
-rw-r--r--src/theory/theory_engine.cpp37
-rw-r--r--src/theory/theory_engine.h5
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();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback