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.

1 files changed, 191 insertions, 0 deletions

diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h
index f87ec5e64..7aecdd3b2 100644
--- a/test/unit/test_smt.h
+++ b/test/unit/test_smt.h
@@ -15,14 +15,23 @@
 #ifndef CVC4__TEST__UNIT__TEST_SMT_H
 #define CVC4__TEST__UNIT__TEST_SMT_H
 
+#include "expr/node.h"
 #include "expr/node_manager.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "test.h"
+#include "theory/theory.h"
+#include "theory/valuation.h"
+#include "util/resource_manager.h"
+#include "util/unsafe_interrupt_exception.h"
 
 namespace CVC4 {
 namespace test {
 
+/* -------------------------------------------------------------------------- */
+/* Test fixtures.                                                             */
+/* -------------------------------------------------------------------------- */
+
 class TestSmt : public TestInternal
 {
  protected:
@@ -53,6 +62,188 @@ class TestSmtNoFinishInit : public TestInternal
   std::unique_ptr<NodeManager> d_nodeManager;
   std::unique_ptr<SmtEngine> d_smtEngine;
 };
+
+/* -------------------------------------------------------------------------- */
+/* Helpers.                                                                   */
+/* -------------------------------------------------------------------------- */
+
+/**
+ * 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
+};
+
+inline std::ostream& operator<<(std::ostream& out, OutputChannelCallType type)
+{
+  switch (type)
+  {
+    case CONFLICT: return out << "CONFLICT";
+    case PROPAGATE: return out << "PROPAGATE";
+    case PROPAGATE_AS_DECISION: return out << "PROPAGATE_AS_DECISION";
+    case AUG_LEMMA: return out << "AUG_LEMMA";
+    case LEMMA: return out << "LEMMA";
+    case EXPLANATION: return out << "EXPLANATION";
+    default: return out << "UNDEFINED-OutputChannelCallType!" << int(type);
+  }
+}
+
+class DummyOutputChannel : public CVC4::theory::OutputChannel
+{
+ public:
+  DummyOutputChannel() {}
+  ~DummyOutputChannel() override {}
+
+  void safePoint(ResourceManager::Resource r) override {}
+  void conflict(TNode n) override { push(CONFLICT, n); }
+
+  void trustedConflict(theory::TrustNode n) override
+  {
+    push(CONFLICT, n.getNode());
+  }
+
+  bool propagate(TNode n) override
+  {
+    push(PROPAGATE, n);
+    return true;
+  }
+
+  void lemma(TNode n,
+             theory::LemmaProperty p = theory::LemmaProperty::NONE) override
+  {
+    push(LEMMA, n);
+  }
+
+  void trustedLemma(theory::TrustNode n, theory::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 << "[DummyOutputChannel " << 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 DymmyTheoryRewriter : public theory::TheoryRewriter
+{
+ public:
+  theory::RewriteResponse preRewrite(TNode n) override
+  {
+    return theory::RewriteResponse(theory::REWRITE_DONE, n);
+  }
+
+  theory::RewriteResponse postRewrite(TNode n) override
+  {
+    return theory::RewriteResponse(theory::REWRITE_DONE, n);
+  }
+};
+
+/** Dummy Theory interface.  */
+template <theory::TheoryId theoryId>
+class DummyTheory : public theory::Theory
+{
+ public:
+  DummyTheory(context::Context* ctxt,
+              context::UserContext* uctxt,
+              theory::OutputChannel& out,
+              theory::Valuation valuation,
+              const LogicInfo& logicInfo,
+              ProofNodeManager* pnm)
+      : Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo, pnm),
+        d_state(ctxt, uctxt, valuation)
+  {
+    // use a default theory state object
+    d_theoryState = &d_state;
+  }
+
+  theory::TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
+
+  void registerTerm(TNode n)
+  {
+    // check that we registerTerm() a term only once
+    ASSERT_TRUE(d_registered.find(n) == d_registered.end());
+
+    for (TNode::iterator i = n.begin(); i != n.end(); ++i)
+    {
+      // check that registerTerm() is called in reverse topological order
+      ASSERT_TRUE(d_registered.find(*i) != d_registered.end());
+    }
+
+    d_registered.insert(n);
+  }
+
+  void presolve() override { Unimplemented(); }
+  void preRegisterTerm(TNode n) override { Unimplemented(); }
+  void propagate(Effort level) override { Unimplemented(); }
+  bool preNotifyFact(
+      TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal) override
+  {
+    // do not assert to equality engine, since this theory does not use one
+    return true;
+  }
+  theory::TrustNode explain(TNode n) override
+  {
+    return theory::TrustNode::null();
+  }
+  Node getValue(TNode n) { return Node::null(); }
+  std::string identify() const override { return "DummyTheory" + d_id; }
+
+  std::set<Node> d_registered;
+
+ private:
+  /** Default theory state object */
+  theory::TheoryState d_state;
+  /**
+   * This fake theory class is equally useful for bool, uf, arith, etc.  It
+   * keeps an identifier to identify itself.
+   */
+  std::string d_id;
+  /** The theory rewriter for this theory. */
+  DymmyTheoryRewriter d_rewriter;
+};
+
+/* -------------------------------------------------------------------------- */
 }  // namespace test
 }  // namespace CVC4
 #endif