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

1 files changed, 19 insertions, 43 deletions

diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index f5c85fc35..4e0fd3e4d 100644
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -63,85 +63,61 @@ namespace theory {
 
 class TestOutputChannel : public theory::OutputChannel {
 public:
-  std::vector< std::pair<enum OutputChannelCallType, Node> > d_callHistory;
-
   TestOutputChannel() {}
+  ~TestOutputChannel() override {}
 
-  ~TestOutputChannel() {}
-
-  void safePoint(uint64_t ammount)  throw(Interrupted, AssertionException) {}
+  void safePoint(uint64_t amount) override {}
 
-  void conflict(TNode n, Proof* pf = NULL)
-    throw(AssertionException, UnsafeInterruptException) {
+  void conflict(TNode n, Proof* pf = nullptr) override {
     push(CONFLICT, n);
   }
 
-  bool propagate(TNode n)
-    throw(AssertionException, UnsafeInterruptException) {
+  bool propagate(TNode n) override {
     push(PROPAGATE, n);
     return true;
   }
 
-  void propagateAsDecision(TNode n)
-    throw(AssertionException, UnsafeInterruptException) {
-    push(PROPAGATE_AS_DECISION, n);
-  }
-
-  LemmaStatus lemma(TNode n, ProofRule rule,
-                    bool removable = false,
-                    bool preprocess = false,
-                    bool sendAtoms = false) throw(AssertionException, UnsafeInterruptException) {
+  LemmaStatus lemma(TNode n, ProofRule rule, bool removable = false,
+                    bool preprocess = false, bool sendAtoms = false) override {
     push(LEMMA, n);
     return LemmaStatus(Node::null(), 0);
   }
 
-  void requirePhase(TNode, bool) throw(Interrupted, AssertionException, UnsafeInterruptException) {
-  }
+  void requirePhase(TNode, bool) override {}
+  bool flipDecision() override { return true; }
+  void setIncomplete() override {}
+  void handleUserAttribute(const char* attr, theory::Theory* t) override {}
 
-  bool flipDecision() throw(Interrupted, AssertionException, UnsafeInterruptException) {
-    return true;
-  }
-
-  void setIncomplete() throw(AssertionException, UnsafeInterruptException) {
-  }
-
-  void handleUserAttribute( const char* attr, theory::Theory* t ) {
-  }
-
-  void clear() {
-    d_callHistory.clear();
-  }
-
-  LemmaStatus splitLemma(TNode n, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
+  LemmaStatus splitLemma(TNode n, bool removable = false) override {
     push(LEMMA, n);
     return LemmaStatus(Node::null(), 0);
   }
 
-  Node getIthNode(int i) {
+  void clear() { d_callHistory.clear(); }
+
+  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(); }
 
-  void printIth(std::ostream& os, int i) {
+  void printIth(std::ostream& os, int i) const {
     os << "[TestOutputChannel " << i;
     os << " " << getIthCallType(i);
     os << " " << getIthNode(i) << "]";
   }
 
-private:
-
+ private:
   void push(OutputChannelCallType call, TNode n) {
     d_callHistory.push_back(std::make_pair(call, n));
   }
 
+  std::vector< std::pair<enum OutputChannelCallType, Node> > d_callHistory;
 };/* class TestOutputChannel */
 
 }/* CVC4::theory namespace */