Removing some throw specifiers from OutputChannel. Fixes bug 716.

diff --git a/src/proof/proof_output_channel.cpp b/src/proof/proof_output_channel.cpp
index 6d729db1fac4922ca60f5f1724c1f1f7a680a474..c87ccd37ce7a884a44de108f7a1f9db89a15c132 100644 (file)
--- 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 b85af5fb581abc37726565b986fe280491aa74f7..b44689fe5304b9ba7c1c3e83f2b9d22a7fc495f8 100644 (file)
--- 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 639793c7fa9e4a44d0a8db2d4e2d1519f0c3e994..4ca113eed364318a6c3cbf8edd4d6663c296777c 100644 (file)
--- 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 c21aa544584dea158c2933586c908546c8ff0843..5ef768fd3ed2057a30bb29c9c179468ea27b8831 100644 (file)
--- 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 fc98c6e3a5209ad1c87764024c689ba145e422e8..3273b3d19701536a75178d9d46decef250f3ed44 100644 (file)
--- 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();