Removing throw specifiers from OutputChannel and subclasses. (#1209)

2 files changed, 30 insertions, 79 deletions

diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index cf1712534..9e99ce884 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -52,40 +52,20 @@ using namespace CVC4::theory::bv;
 using namespace std;
 
 class FakeOutputChannel : public OutputChannel {
-  void conflict(TNode n, Proof* pf = NULL) throw(AssertionException) {
+  void conflict(TNode n, Proof* pf) override { Unimplemented(); }
+  bool propagate(TNode n) override { Unimplemented(); }
+  LemmaStatus lemma(TNode n, ProofRule rule, bool removable, bool preprocess,
+                    bool sendAtoms) override {
     Unimplemented();
   }
-  bool propagate(TNode n) throw(AssertionException) {
+  void requirePhase(TNode, bool) override { Unimplemented(); }
+  bool flipDecision() override { Unimplemented(); }
+  void setIncomplete() override { Unimplemented(); }
+  void handleUserAttribute(const char* attr, Theory* t) override {
     Unimplemented();
   }
-  void propagateAsDecision(TNode n) throw(AssertionException) {
-    Unimplemented();
-  }
-  LemmaStatus lemma(TNode n, ProofRule rule,
-                    bool removable,
-                    bool preprocess,
-                    bool sendAtoms) throw(AssertionException) {
-    Unimplemented();
-  }
-  void requirePhase(TNode, bool) throw(AssertionException) {
-    Unimplemented();
-  }
-  bool flipDecision() throw(AssertionException) {
-    Unimplemented();
-  }
-  void explanation(TNode n) throw(AssertionException) {
-    Unimplemented();
-  }
-  void setIncomplete() throw(AssertionException) {
-    Unimplemented();
-  }
-  void handleUserAttribute( const char* attr, Theory* t ){
-    Unimplemented();
-  }
-  LemmaStatus splitLemma(TNode n, bool removable) throw(TypeCheckingExceptionPrivate, AssertionException){
-    Unimplemented();
-  }
-};/* class FakeOutputChannel */
+  LemmaStatus splitLemma(TNode n, bool removable) override { Unimplemented(); }
+}; /* class FakeOutputChannel */
 
 template<TheoryId theory>
 class FakeTheory;
diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index 85d1a1c02..d1517d7c2 100644
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -41,83 +41,54 @@ using namespace std;
  */
 enum OutputChannelCallType{CONFLICT, PROPAGATE, LEMMA, EXPLANATION};
 class TestOutputChannel : public OutputChannel {
-private:
-  void push(OutputChannelCallType call, TNode n) {
-    d_callHistory.push_back(make_pair(call, n));
-  }
-
-public:
-  vector< pair<OutputChannelCallType, Node> > d_callHistory;
-
+ public:
   TestOutputChannel() {}
+  ~TestOutputChannel() override {}
 
-  ~TestOutputChannel() {}
-
-  void safePoint(uint64_t amount)
-      throw(Interrupted, UnsafeInterruptException, AssertionException)
-  {}
+  void safePoint(uint64_t amount) override {}
 
-  void conflict(TNode n, Proof* pf = NULL)
-    throw(AssertionException) {
+  void conflict(TNode n, Proof* pf = nullptr) override {
     push(CONFLICT, n);
   }
 
-  bool propagate(TNode n)
-    throw(AssertionException) {
+  bool propagate(TNode n) override {
     push(PROPAGATE, n);
     return true;
   }
 
-  void propagateAsDecision(TNode n)
-    throw(AssertionException) {
-    // ignore
-  }
-
-  LemmaStatus lemma(TNode n, ProofRule rule,
-                    bool removable = false,
-                    bool preprocess = false,
-                    bool sendAtoms = false)
-    throw(AssertionException) {
+  LemmaStatus lemma(TNode n, ProofRule rule, bool removable = false,
+                    bool preprocess = false, bool sendAtoms = false) override {
     push(LEMMA, n);
     return LemmaStatus(Node::null(), 0);
   }
 
-  LemmaStatus splitLemma(TNode n, bool removable) throw (TypeCheckingExceptionPrivate, AssertionException){
+  LemmaStatus splitLemma(TNode n, bool removable) override {
     push(LEMMA, n);
     return LemmaStatus(Node::null(), 0);
   }
 
-  void requirePhase(TNode, bool)
-    throw(Interrupted, AssertionException) {
-    Unreachable();
-  }
+  void requirePhase(TNode, bool) override { Unreachable(); }
+  bool flipDecision() override { Unreachable(); }
+  void setIncomplete() override { Unreachable(); }
 
-  bool flipDecision()
-    throw(Interrupted, AssertionException) {
-    Unreachable();
-  }
+  void clear() { d_callHistory.clear(); }
 
-  void setIncomplete()
-    throw(AssertionException) {
-    Unreachable();
-  }
-
-  void clear() {
-    d_callHistory.clear();
-  }
-
-  Node getIthNode(int i) {
+  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(); }
+
+ private:
+  void push(OutputChannelCallType call, TNode n) {
+    d_callHistory.push_back(make_pair(call, n));
   }
+  vector<pair<OutputChannelCallType, Node> > d_callHistory;
 };
 
 class DummyTheory : public Theory {