Initialize theory rewriters in theories (#4197)

Until now, the `Rewriter` was responsible for creating `TheoryRewriter`
instances. This commit adds a method `mkTheoryRewriter()` that theories
override to create an instance of their corresponding theory rewriter.
The advantage is that the theories can pass additional information to
their theory rewriter (e.g. a statistics object).

12 files changed, 118 insertions, 122 deletions

diff --git a/test/unit/preprocessing/pass_bv_gauss_white.h b/test/unit/preprocessing/pass_bv_gauss_white.h
index 4037c7191..bd21ed69c 100644
--- a/test/unit/preprocessing/pass_bv_gauss_white.h
+++ b/test/unit/preprocessing/pass_bv_gauss_white.h
@@ -176,6 +176,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
     d_nm = NodeManager::fromExprManager(d_em);
     d_smt = new SmtEngine(d_em);
     d_scope = new SmtScope(d_smt);
+    d_smt->finalOptionsAreSet();
 
     d_zero = bv::utils::mkZero(16);
 
@@ -2373,7 +2374,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
 
     AssertionPipeline apipe;
     apipe.push_back(a);
-    passes::BVGauss bgauss(nullptr);
+    passes::BVGauss bgauss(nullptr, "bv-gauss-unit");
     std::unordered_map<Node, Node, NodeHashFunction> res;
     PreprocessingPassResult pres = bgauss.applyInternal(&apipe);
     TS_ASSERT (pres == PreprocessingPassResult::NO_CONFLICT);
@@ -2457,7 +2458,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
     apipe.push_back(a);
     apipe.push_back(eq4);
     apipe.push_back(eq5);
-    passes::BVGauss bgauss(nullptr);
+    passes::BVGauss bgauss(nullptr, "bv-gauss-unit");
     std::unordered_map<Node, Node, NodeHashFunction> res;
     PreprocessingPassResult pres = bgauss.applyInternal(&apipe);
     TS_ASSERT (pres == PreprocessingPassResult::NO_CONFLICT);
@@ -2507,7 +2508,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
     AssertionPipeline apipe;
     apipe.push_back(eq1);
     apipe.push_back(eq2);
-    passes::BVGauss bgauss(nullptr);
+    passes::BVGauss bgauss(nullptr, "bv-gauss-unit");
     std::unordered_map<Node, Node, NodeHashFunction> res;
     PreprocessingPassResult pres = bgauss.applyInternal(&apipe);
     TS_ASSERT (pres == PreprocessingPassResult::NO_CONFLICT);
diff --git a/test/unit/theory/evaluator_white.h b/test/unit/theory/evaluator_white.h
index c02aaaed8..547ce27cf 100644
--- a/test/unit/theory/evaluator_white.h
+++ b/test/unit/theory/evaluator_white.h
@@ -52,6 +52,7 @@ class TheoryEvaluatorWhite : public CxxTest::TestSuite
     d_nm = NodeManager::fromExprManager(d_em);
     d_smt = new SmtEngine(d_em);
     d_scope = new SmtScope(d_smt);
+    d_smt->finalOptionsAreSet();
   }
 
   void tearDown() override
diff --git a/test/unit/theory/regexp_operation_black.h b/test/unit/theory/regexp_operation_black.h
index 81f5cf34a..826e14a31 100644
--- a/test/unit/theory/regexp_operation_black.h
+++ b/test/unit/theory/regexp_operation_black.h
@@ -45,6 +45,10 @@ class RegexpOperationBlack : public CxxTest::TestSuite
     d_scope = new SmtScope(d_smt);
     d_regExpOpr = new RegExpOpr();
 
+    // Ensure that the SMT engine is fully initialized (required for the
+    // rewriter)
+    d_smt->push();
+
     d_nm = NodeManager::currentNM();
   }
 
diff --git a/test/unit/theory/sequences_rewriter_white.h b/test/unit/theory/sequences_rewriter_white.h
index 200a36d0b..c823c0704 100644
--- a/test/unit/theory/sequences_rewriter_white.h
+++ b/test/unit/theory/sequences_rewriter_white.h
@@ -45,6 +45,7 @@ class SequencesRewriterWhite : public CxxTest::TestSuite
     d_em = new ExprManager(opts);
     d_smt = new SmtEngine(d_em);
     d_scope = new SmtScope(d_smt);
+    d_smt->finalOptionsAreSet();
     d_rewriter = new ExtendedRewriter(true);
 
     d_nm = NodeManager::currentNM();
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 8ae90c4c3..72b74a7b9 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -37,19 +37,15 @@ using namespace CVC4::theory;
 using namespace CVC4::smt;
 
 class TheoryBlack : public CxxTest::TestSuite {
-private:
-
-  ExprManager* d_em;
-  SmtEngine* d_smt;
-  NodeManager* d_nm;
-  SmtScope* d_scope;
-
  public:
   void setUp() override
   {
     d_em = new ExprManager();
     d_smt = new SmtEngine(d_em);
     d_scope = new SmtScope(d_smt);
+    // Ensure that the SMT engine is fully initialized (required for the
+    // rewriter)
+    d_smt->push();
 
     d_nm = NodeManager::fromExprManager(d_em);
   }
@@ -152,4 +148,9 @@ private:
 
   }
 
+ private:
+  ExprManager* d_em;
+  SmtEngine* d_smt;
+  NodeManager* d_nm;
+  SmtScope* d_scope;
 };
diff --git a/test/unit/theory/theory_bv_rewriter_white.h b/test/unit/theory/theory_bv_rewriter_white.h
index bf0ca73b3..b6348339b 100644
--- a/test/unit/theory/theory_bv_rewriter_white.h
+++ b/test/unit/theory/theory_bv_rewriter_white.h
@@ -43,6 +43,7 @@ class TheoryBvRewriterWhite : public CxxTest::TestSuite
     d_em = new ExprManager(opts);
     d_smt = new SmtEngine(d_em);
     d_scope = new SmtScope(d_smt);
+    d_smt->finalOptionsAreSet();
 
     d_nm = NodeManager::currentNM();
   }
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 5af670d5e..4a019ac08 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -38,6 +38,7 @@
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
+#include "theory/theory_rewriter.h"
 #include "theory/valuation.h"
 #include "util/integer.h"
 #include "util/proof.h"
@@ -91,118 +92,72 @@ struct RewriteItem {
   bool d_topLevel;
 };/* struct RewriteItem */
 
+class FakeTheoryRewriter : public TheoryRewriter
+{
+ public:
+  RewriteResponse preRewrite(TNode n) override
+  {
+    return RewriteResponse(REWRITE_DONE, n);
+  }
+
+  RewriteResponse postRewrite(TNode n) override
+  {
+    return RewriteResponse(REWRITE_DONE, n);
+  }
+};
+
 /**
- * Fake Theory interface.  Looks like a Theory, but really all it does is note when and
- * how rewriting behavior is requested.
+ * Fake Theory interface.  Looks like a Theory, but really all it does is note
+ * when and how rewriting behavior is requested.
  */
-template<TheoryId theoryId>
-class FakeTheory : public Theory {
+template <TheoryId theoryId>
+class FakeTheory : public Theory
+{
   /**
-   * This fake theory class is equally useful for bool, uf, arith, etc.  It keeps an
-   * identifier to identify itself.
+   * This fake theory class is equally useful for bool, uf, arith, etc.  It
+   * keeps an identifier to identify itself.
    */
   std::string d_id;
 
   /**
-   * The expected sequence of rewrite calls.  Filled by FakeTheory::expect() and consumed
-   * by FakeTheory::preRewrite() and FakeTheory::postRewrite().
+   * The expected sequence of rewrite calls.  Filled by FakeTheory::expect() and
+   * consumed by FakeTheory::preRewrite() and FakeTheory::postRewrite().
    */
   // static std::deque<RewriteItem> s_expected;
 
-public:
-  FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
-      Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo)
-  { }
-
-  /** Register an expected rewrite call */
-  static void expect(RewriteType type, FakeTheory* thy, TNode n, bool topLevel)
-      throw()
+ public:
+  FakeTheory(context::Context* ctxt,
+             context::UserContext* uctxt,
+             OutputChannel& out,
+             Valuation valuation,
+             const LogicInfo& logicInfo)
+      : Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo)
   {
-    RewriteItem item = { type, thy, n, topLevel };
-    //s_expected.push_back(item);
   }
 
-  /**
-   * Returns whether the expected queue is empty.  This is done after a call into
-   * the rewriter to ensure that the actual set of observed rewrite calls completed
-   * the sequence of expected rewrite calls.
-   */
-  static bool nothingMoreExpected() throw() {
-    return true; // s_expected.empty();
+  std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override
+  {
+    return std::unique_ptr<TheoryRewriter>(new FakeTheoryRewriter());
   }
 
-  /**
-   * Overrides Theory::preRewrite().  This "fake theory" version ensures that
-   * this actual, observed pre-rewrite call matches the next "expected" call set up
-   * by the test.
-   */
-  RewriteResponse preRewrite(TNode n, bool topLevel) {
-//    if(false) { //s_expected.empty()) {
-//      cout << std::endl
-//           << "didn't expect anything more, but got" << std::endl
-//           << "     PRE  " << topLevel << " " << identify() << " " << n
-//           << std::endl;
-//    }
-//    TS_ASSERT(!s_expected.empty());
-//
-//    RewriteItem expected = s_expected.front();
-//    s_expected.pop_front();
-//
-//    if(expected.d_type != PRE ||
-////       expected.d_theory != this ||
-//       expected.d_node != n ||
-//       expected.d_topLevel != topLevel) {
-//      cout << std::endl
-//           << "HAVE PRE  " << topLevel << " " << identify() << " " << n
-//           << std::endl
-//           << "WANT " << (expected.d_type == PRE ? "PRE  " : "POST ")
-//  //         << expected.d_topLevel << " " << expected.d_theory->identify()
-//           << " " << expected.d_node << std::endl << std::endl;
-//    }
-//
-//    TS_ASSERT_EQUALS(expected.d_type, PRE);
-////    TS_ASSERT_EQUALS(expected.d_theory, this);
-//    TS_ASSERT_EQUALS(expected.d_node, n);
-//    TS_ASSERT_EQUALS(expected.d_topLevel, topLevel);
-
-    return RewriteResponse(REWRITE_DONE, n);
+  /** Register an expected rewrite call */
+  static void expect(RewriteType type,
+                     FakeTheory* thy,
+                     TNode n,
+                     bool topLevel) throw()
+  {
+    RewriteItem item = {type, thy, n, topLevel};
+    // s_expected.push_back(item);
   }
 
   /**
-   * Overrides Theory::postRewrite().  This "fake theory" version ensures that
-   * this actual, observed post-rewrite call matches the next "expected" call set up
-   * by the test.
+   * Returns whether the expected queue is empty.  This is done after a call
+   * into the rewriter to ensure that the actual set of observed rewrite calls
+   * completed the sequence of expected rewrite calls.
    */
-  RewriteResponse postRewrite(TNode n, bool topLevel) {
-//    if(s_expected.empty()) {
-//      cout << std::endl
-//           << "didn't expect anything more, but got" << std::endl
-//           << "     POST " << topLevel << " " << identify() << " " << n
-//           << std::endl;
-//    }
-//    TS_ASSERT(!s_expected.empty());
-//
-//    RewriteItem expected = s_expected.front();
-//    s_expected.pop_front();
-//
-//    if(expected.d_type != POST ||
-////       expected.d_theory != this ||
-//       expected.d_node != n ||
-//       expected.d_topLevel != topLevel) {
-//      cout << std::endl
-//           << "HAVE POST " << topLevel << " " << identify() << " " << n
-//           << std::endl
-//           << "WANT " << (expected.d_type == PRE ? "PRE  " : "POST ")
-////           << expected.d_topLevel << " " << expected.d_theory->identify()
-//           << " " << expected.d_node << std::endl << std::endl;
-//    }
-//
-//    TS_ASSERT_EQUALS(expected.d_type, POST);
-//    TS_ASSERT_EQUALS(expected.d_theory, this);
-//    TS_ASSERT_EQUALS(expected.d_node, n);
-//    TS_ASSERT_EQUALS(expected.d_topLevel, topLevel);
-
-    return RewriteResponse(REWRITE_DONE, n);
+  static bool nothingMoreExpected() throw()
+  {
+    return true;  // s_expected.empty();
   }
 
   std::string identify() const override {
@@ -221,8 +176,7 @@ public:
     return Node::null();
   }
   Node getValue(TNode n) { return Node::null(); }
-};/* class FakeTheory */
-
+}; /* class FakeTheory */
 
 /* definition of the s_expected static field in FakeTheory; see above */
 // std::deque<RewriteItem> FakeTheory::s_expected;
diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h
index 0fa7a3f82..7c37b1a85 100644
--- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h
+++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h
@@ -65,6 +65,7 @@ void BvInstantiatorWhite::setUp()
   d_nm = NodeManager::fromExprManager(d_em);
   d_smt = new SmtEngine(d_em);
   d_scope = new SmtScope(d_smt);
+  d_smt->finalOptionsAreSet();
 }
 
 void BvInstantiatorWhite::tearDown()
diff --git a/test/unit/theory/theory_sets_type_enumerator_white.h b/test/unit/theory/theory_sets_type_enumerator_white.h
index 3b5016fad..0ece5a056 100644
--- a/test/unit/theory/theory_sets_type_enumerator_white.h
+++ b/test/unit/theory/theory_sets_type_enumerator_white.h
@@ -18,9 +18,12 @@
 
 #include <cxxtest/TestSuite.h>
 
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
 #include "theory/sets/theory_sets_type_enumerator.h"
 
 using namespace CVC4;
+using namespace CVC4::smt;
 using namespace CVC4::theory;
 using namespace CVC4::kind;
 using namespace CVC4::theory::sets;
@@ -28,21 +31,20 @@ using namespace std;
 
 class SetEnumeratorWhite : public CxxTest::TestSuite
 {
-  ExprManager* d_em;
-  NodeManager* d_nm;
-  NodeManagerScope* d_scope;
-
  public:
   void setUp() override
   {
     d_em = new ExprManager();
+    d_smt = new SmtEngine(d_em);
     d_nm = NodeManager::fromExprManager(d_em);
-    d_scope = new NodeManagerScope(d_nm);
+    d_scope = new SmtScope(d_smt);
+    d_smt->finalOptionsAreSet();
   }
 
   void tearDown() override
   {
     delete d_scope;
+    delete d_smt;
     delete d_em;
   }
 
@@ -68,8 +70,9 @@ class SetEnumeratorWhite : public CxxTest::TestSuite
     TS_ASSERT_EQUALS(expected2, actual2);
     TS_ASSERT(!setEnumerator.isFinished());
 
-    Node actual3 = *++setEnumerator;
-    Node expected3 = d_nm->mkNode(Kind::UNION, expected1, expected2);
+    Node actual3 = Rewriter::rewrite(*++setEnumerator);
+    Node expected3 =
+        Rewriter::rewrite(d_nm->mkNode(Kind::UNION, expected1, expected2));
     TS_ASSERT_EQUALS(expected3, actual3);
     TS_ASSERT(!setEnumerator.isFinished());
 
@@ -301,4 +304,9 @@ class SetEnumeratorWhite : public CxxTest::TestSuite
     TS_ASSERT(setEnumerator.isFinished());
   }
 
+ private:
+  ExprManager* d_em;
+  SmtEngine* d_smt;
+  NodeManager* d_nm;
+  SmtScope* d_scope;
 }; /* class SetEnumeratorWhite */
diff --git a/test/unit/theory/theory_strings_skolem_cache_black.h b/test/unit/theory/theory_strings_skolem_cache_black.h
index e1b84492c..8f41153f3 100644
--- a/test/unit/theory/theory_strings_skolem_cache_black.h
+++ b/test/unit/theory/theory_strings_skolem_cache_black.h
@@ -16,13 +16,17 @@
 
 #include <memory>
 
+#include "expr/expr_manager.h"
 #include "expr/node.h"
 #include "expr/node_manager.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
 #include "theory/strings/skolem_cache.h"
 #include "util/rational.h"
 #include "util/string.h"
 
 using namespace CVC4;
+using namespace CVC4::smt;
 using namespace CVC4::theory::strings;
 
 class TheoryStringsSkolemCacheBlack : public CxxTest::TestSuite
@@ -30,8 +34,14 @@ class TheoryStringsSkolemCacheBlack : public CxxTest::TestSuite
  public:
   void setUp() override
   {
-    d_nm.reset(new NodeManager(nullptr));
-    d_scope.reset(new NodeManagerScope(d_nm.get()));
+    d_em.reset(new ExprManager());
+    d_smt.reset(new SmtEngine(d_em.get()));
+    d_scope.reset(new SmtScope(d_smt.get()));
+    // Ensure that the SMT engine is fully initialized (required for the
+    // rewriter)
+    d_smt->push();
+
+    d_nm = NodeManager::fromExprManager(d_em.get());
   }
 
   void tearDown() override {}
@@ -87,6 +97,8 @@ class TheoryStringsSkolemCacheBlack : public CxxTest::TestSuite
   }
 
  private:
-  std::unique_ptr<NodeManager> d_nm;
-  std::unique_ptr<NodeManagerScope> d_scope;
+  std::unique_ptr<ExprManager> d_em;
+  std::unique_ptr<SmtEngine> d_smt;
+  NodeManager* d_nm;
+  std::unique_ptr<SmtScope> d_scope;
 };
diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index 0dd52be8c..eb43e00cb 100644
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -93,7 +93,7 @@ class TestOutputChannel : public OutputChannel {
 };
 
 class DummyTheory : public Theory {
-public:
+ public:
   set<Node> d_registered;
   vector<Node> d_getSequence;
 
@@ -102,6 +102,11 @@ public:
       : Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo)
   {}
 
+  std::unique_ptr<TheoryRewriter> mkTheoryRewriter()
+  {
+    return std::unique_ptr<TheoryRewriter>();
+  }
+
   void registerTerm(TNode n) {
     // check that we registerTerm() a term only once
     TS_ASSERT(d_registered.find(n) == d_registered.end());
diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h
index da915b7ee..58dadd27a 100644
--- a/test/unit/theory/type_enumerator_white.h
+++ b/test/unit/theory/type_enumerator_white.h
@@ -25,30 +25,32 @@
 #include "expr/node_manager.h"
 #include "expr/type_node.h"
 #include "options/language.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
 #include "theory/type_enumerator.h"
 
 using namespace CVC4;
+using namespace CVC4::smt;
 using namespace CVC4::theory;
 using namespace CVC4::kind;
 
 using namespace std;
 
 class TypeEnumeratorWhite : public CxxTest::TestSuite {
-  ExprManager* d_em;
-  NodeManager* d_nm;
-  NodeManagerScope* d_scope;
-
  public:
   void setUp() override
   {
     d_em = new ExprManager();
+    d_smt = new SmtEngine(d_em);
     d_nm = NodeManager::fromExprManager(d_em);
-    d_scope = new NodeManagerScope(d_nm);
+    d_scope = new SmtScope(d_smt);
+    d_smt->finalOptionsAreSet();
   }
 
   void tearDown() override
   {
     delete d_scope;
+    delete d_smt;
     delete d_em;
   }
 
@@ -272,4 +274,9 @@ class TypeEnumeratorWhite : public CxxTest::TestSuite {
     TS_ASSERT_THROWS(*++te, NoMoreValuesException&);
   }
 
+ private:
+  ExprManager* d_em;
+  SmtEngine* d_smt;
+  NodeManager* d_nm;
+  SmtScope* d_scope;
 };/* class TypeEnumeratorWhite */