google test: theory: Migrate theory_white. (#6006)

This moves test utils for theory tests to test_smt.h and consolidates
two implementations of dummy theories into one.

2 files changed, 0 insertions, 124 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index deb20ab70..8825126fa 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -988,7 +988,6 @@ libcvc4_add_sources(
   theory/theory_rewriter.h
   theory/theory_state.cpp
   theory/theory_state.h
-  theory/theory_test_utils.h
   theory/trust_node.cpp
   theory/trust_node.h
   theory/trust_substitutions.cpp
diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
deleted file mode 100644
index f37e4c942..000000000
--- a/src/theory/theory_test_utils.h
+++ /dev/null
@@ -1,123 +0,0 @@
-/*********************                                                        */
-/*! \file theory_test_utils.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Common utilities for testing theories
- **
- ** Common utilities for testing theories.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef CVC4__THEORY__THEORY_TEST_UTILS_H
-#define CVC4__THEORY__THEORY_TEST_UTILS_H
-
-#include <iostream>
-#include <memory>
-#include <utility>
-#include <vector>
-
-#include "expr/node.h"
-#include "theory/interrupted.h"
-#include "theory/output_channel.h"
-#include "util/resource_manager.h"
-#include "util/unsafe_interrupt_exception.h"
-
-namespace CVC4 {
-namespace theory {
-
-/**
- * Very basic OutputChannel for testing simple Theory Behaviour.
- * Stores a call sequence for the output channel
- */
-enum OutputChannelCallType {
-  CONFLICT,
-  PROPAGATE,
-  PROPAGATE_AS_DECISION,
-  AUG_LEMMA,
-  LEMMA,
-  EXPLANATION
-};/* enum OutputChannelCallType */
-
-}/* CVC4::theory namespace */
-
-inline std::ostream& operator<<(std::ostream& out, theory::OutputChannelCallType type) {
-  switch(type) {
-  case theory::CONFLICT: return out << "CONFLICT";
-  case theory::PROPAGATE: return out << "PROPAGATE";
-  case theory::PROPAGATE_AS_DECISION: return out << "PROPAGATE_AS_DECISION";
-  case theory::AUG_LEMMA: return out << "AUG_LEMMA";
-  case theory::LEMMA: return out << "LEMMA";
-  case theory::EXPLANATION: return out << "EXPLANATION";
-  default: return out << "UNDEFINED-OutputChannelCallType!" << int(type);
-  }
-}
-
-namespace theory {
-
-class TestOutputChannel : public theory::OutputChannel {
-public:
-  TestOutputChannel() {}
-  ~TestOutputChannel() override {}
-
-  void safePoint(ResourceManager::Resource r) override {}
-  void conflict(TNode n) override { push(CONFLICT, n); }
-
-  void trustedConflict(TrustNode n) override { push(CONFLICT, n.getNode()); }
-
-  bool propagate(TNode n) override {
-    push(PROPAGATE, n);
-    return true;
-  }
-
-  void lemma(TNode n, LemmaProperty p) override { push(LEMMA, n); }
-
-  void trustedLemma(TrustNode n, LemmaProperty p) override
-  {
-    push(LEMMA, n.getNode());
-  }
-
-  void requirePhase(TNode, bool) override {}
-  void setIncomplete() override {}
-  void handleUserAttribute(const char* attr, theory::Theory* t) override {}
-
-  void splitLemma(TNode n, bool removable = false) override { push(LEMMA, n); }
-
-  void clear() { d_callHistory.clear(); }
-
-  Node getIthNode(int i) const {
-    Node tmp = (d_callHistory[i]).second;
-    return tmp;
-  }
-
-  OutputChannelCallType getIthCallType(int i) const {
-    return (d_callHistory[i]).first;
-  }
-
-  unsigned getNumCalls() const { return d_callHistory.size(); }
-
-  void printIth(std::ostream& os, int i) const {
-    os << "[TestOutputChannel " << i;
-    os << " " << getIthCallType(i);
-    os << " " << getIthNode(i) << "]";
-  }
-
- 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 */
-}/* CVC4 namespace */
-
-#endif /* CVC4__THEORY__THEORY_TEST_UTILS_H */