Removing some throw specifiers from OutputChannel. Fixes bug 716.

3 files changed, 25 insertions, 30 deletions

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();