From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Thu, 2 Apr 2020 02:35:25 +0000 (-0700)
Subject: Initialize theory rewriters in theories (#4197)
X-Git-Tag: cvc5-1.0.0~3413
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3915eb7b497bd185385048f8c7f2b4c8f2bf7c03;p=cvc5.git

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).
---

diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp
index 683716410..b08f69b50 100644
--- a/src/preprocessing/passes/bv_gauss.cpp
+++ b/src/preprocessing/passes/bv_gauss.cpp
@@ -687,8 +687,9 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem(
   return ret;
 }
 
-BVGauss::BVGauss(PreprocessingPassContext* preprocContext)
-    : PreprocessingPass(preprocContext, "bv-gauss")
+BVGauss::BVGauss(PreprocessingPassContext* preprocContext,
+                 const std::string& name)
+    : PreprocessingPass(preprocContext, name)
 {
 }
 
diff --git a/src/preprocessing/passes/bv_gauss.h b/src/preprocessing/passes/bv_gauss.h
index 93d61be9e..7fb23814a 100644
--- a/src/preprocessing/passes/bv_gauss.h
+++ b/src/preprocessing/passes/bv_gauss.h
@@ -30,7 +30,8 @@ namespace passes {
 class BVGauss : public PreprocessingPass
 {
  public:
-  BVGauss(PreprocessingPassContext* preprocContext);
+  BVGauss(PreprocessingPassContext* preprocContext,
+          const std::string& name = "bv-gauss");
 
  protected:
   /**
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 8986e6894..2c748f188 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -19,6 +19,7 @@
 
 #include "options/smt_options.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/arith/arith_rewriter.h"
 #include "theory/arith/infer_bounds.h"
 #include "theory/arith/theory_arith_private.h"
 #include "theory/ext_theory.h"
@@ -53,6 +54,11 @@ TheoryArith::~TheoryArith(){
   delete d_internal;
 }
 
+std::unique_ptr<TheoryRewriter> TheoryArith::mkTheoryRewriter()
+{
+  return std::unique_ptr<TheoryRewriter>(new ArithRewriter());
+}
+
 void TheoryArith::preRegisterTerm(TNode n){
   d_internal->preRegisterTerm(n);
 }
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index b39ab961f..92892d2ae 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -51,6 +51,8 @@ public:
               Valuation valuation, const LogicInfo& logicInfo);
   virtual ~TheoryArith();
 
+  std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
   /**
    * Does non-context dependent setup for a node connected to a theory.
    */
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index dcf82e6b4..787ae84e2 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -29,6 +29,7 @@
 #include "smt/command.h"
 #include "smt/logic_exception.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/arrays/theory_arrays_rewriter.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
 #include "theory/valuation.h"
@@ -178,6 +179,11 @@ TheoryArrays::~TheoryArrays() {
   smtStatisticsRegistry()->unregisterStat(&d_numSetModelValConflicts);
 }
 
+std::unique_ptr<TheoryRewriter> TheoryArrays::mkTheoryRewriter()
+{
+  return std::unique_ptr<TheoryRewriter>(new TheoryArraysRewriter());
+}
+
 void TheoryArrays::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   d_equalityEngine.setMasterEqualityEngine(eq);
 }
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 3d6d0692e..d1f912d95 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -144,6 +144,8 @@ class TheoryArrays : public Theory {
                std::string name = "");
   ~TheoryArrays();
 
+  std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
   void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
 
   std::string identify() const override { return std::string("TheoryArrays"); }
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index 8fbe83951..e670121d1 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -14,15 +14,17 @@
  ** The theory of booleans.
  **/
 
-#include "theory/theory.h"
 #include "theory/booleans/theory_bool.h"
-#include "theory/booleans/circuit_propagator.h"
-#include "theory/valuation.h"
-#include "smt_util/boolean_simplification.h"
-#include "theory/substitutions.h"
 
-#include <vector>
 #include <stack>
+#include <vector>
+
+#include "smt_util/boolean_simplification.h"
+#include "theory/booleans/circuit_propagator.h"
+#include "theory/booleans/theory_bool_rewriter.h"
+#include "theory/substitutions.h"
+#include "theory/theory.h"
+#include "theory/valuation.h"
 #include "util/hash.h"
 
 using namespace std;
@@ -31,6 +33,11 @@ namespace CVC4 {
 namespace theory {
 namespace booleans {
 
+std::unique_ptr<TheoryRewriter> TheoryBool::mkTheoryRewriter()
+{
+  return std::unique_ptr<TheoryRewriter>(new TheoryBoolRewriter());
+}
+
 Theory::PPAssertStatus TheoryBool::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
 
   if (in.getKind() == kind::CONST_BOOLEAN && !in.getConst<bool>()) {
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index abe024282..75e375ee6 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -33,6 +33,8 @@ public:
       : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo)
   {}
 
+  std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
 
   //void check(Effort);
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index 505aa503f..8df5a8535 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -17,6 +17,7 @@
 #include "theory/builtin/theory_builtin.h"
 
 #include "expr/kind.h"
+#include "theory/builtin/theory_builtin_rewriter.h"
 #include "theory/theory_model.h"
 #include "theory/valuation.h"
 
@@ -35,6 +36,11 @@ TheoryBuiltin::TheoryBuiltin(context::Context* c,
 {
 }
 
+std::unique_ptr<TheoryRewriter> TheoryBuiltin::mkTheoryRewriter()
+{
+  return std::unique_ptr<TheoryRewriter>(new TheoryBuiltinRewriter());
+}
+
 std::string TheoryBuiltin::identify() const
 {
   return std::string("TheoryBuiltin");
diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index 6e99ef040..d240f4f63 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -34,6 +34,8 @@ class TheoryBuiltin : public Theory
                 Valuation valuation,
                 const LogicInfo& logicInfo);
 
+  std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
   std::string identify() const override;
 
   /** finish initialization */
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 94fc1e34c..27718b63f 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -112,6 +112,11 @@ TheoryBV::TheoryBV(context::Context* c,
 
 TheoryBV::~TheoryBV() {}
 
+std::unique_ptr<TheoryRewriter> TheoryBV::mkTheoryRewriter()
+{
+  return std::unique_ptr<TheoryRewriter>(new TheoryBVRewriter());
+}
+
 void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   if (options::bitblastMode() == options::BitblastMode::EAGER)
   {
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 196535a19..ff1c9245a 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -72,6 +72,8 @@ public:
 
   ~TheoryBV();
 
+  std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
   void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
 
   void finishInit() override;
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 7fbe5bc68..15220b9dc 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -25,6 +25,7 @@
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
 #include "options/theory_options.h"
+#include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/datatypes/theory_datatypes_type_rules.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers_engine.h"
@@ -85,6 +86,11 @@ TheoryDatatypes::~TheoryDatatypes() {
   }
 }
 
+std::unique_ptr<TheoryRewriter> TheoryDatatypes::mkTheoryRewriter()
+{
+  return std::unique_ptr<TheoryRewriter>(new DatatypesRewriter());
+}
+
 void TheoryDatatypes::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   d_equalityEngine.setMasterEqualityEngine(eq);
 }
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index a878647bc..7ccd04f39 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -271,6 +271,8 @@ private:
                   const LogicInfo& logicInfo);
   ~TheoryDatatypes();
 
+  std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
   void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
 
   /** propagate */
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 2632a6f38..5ab285766 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -15,18 +15,18 @@
  ** \todo document this file
  **/
 
-
-#include "options/fp_options.h"
-#include "theory/rewriter.h"
-#include "theory/theory_model.h"
 #include "theory/fp/theory_fp.h"
 
-
 #include <set>
 #include <stack>
 #include <unordered_set>
 #include <vector>
 
+#include "options/fp_options.h"
+#include "theory/fp/theory_fp_rewriter.h"
+#include "theory/rewriter.h"
+#include "theory/theory_model.h"
+
 using namespace std;
 
 namespace CVC4 {
@@ -177,6 +177,11 @@ TheoryFp::TheoryFp(context::Context *c,
 
 } /* TheoryFp::TheoryFp() */
 
+std::unique_ptr<TheoryRewriter> TheoryFp::mkTheoryRewriter()
+{
+  return std::unique_ptr<TheoryRewriter>(new TheoryFpRewriter());
+}
+
 Node TheoryFp::minUF(Node node) {
   Assert(node.getKind() == kind::FLOATINGPOINT_MIN);
   TypeNode t(node.getType());
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index ad093f924..802a70435 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -38,6 +38,8 @@ class TheoryFp : public Theory {
   TheoryFp(context::Context* c, context::UserContext* u, OutputChannel& out,
            Valuation valuation, const LogicInfo& logicInfo);
 
+  std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
   Node expandDefinition(LogicRequest& lr, Node node) override;
 
   void preRegisterTerm(TNode node) override;
diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter
index dd5abd219..3c27f1b53 100755
--- a/src/theory/mkrewriter
+++ b/src/theory/mkrewriter
@@ -37,7 +37,6 @@ me=$(basename "$0")
 template=$1; shift
 
 rewriter_includes=
-rewrite_init=
 
 pre_rewrite_get_cache=
 pre_rewrite_set_cache=
@@ -139,8 +138,6 @@ function rewriter {
   header="$2"
 
   rewriter_includes="${rewriter_includes}#include \"$header\"
-"
-  rewrite_init="${rewrite_init}   d_theoryRewriters[${theory_id}].reset(new ${class});
 "
   pre_rewrite_attribute_ids="${pre_rewrite_attribute_ids} preids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<${theory_id}>::pre_rewrite()));
 "
@@ -257,7 +254,6 @@ for var in \
     post_rewrite_get_cache \
     pre_rewrite_set_cache \
     post_rewrite_set_cache \
-    rewrite_init \
     pre_rewrite_attribute_ids \
     post_rewrite_attribute_ids \
     template \
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 227f4d5b5..e3e3c3824 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -22,6 +22,7 @@
 #include "theory/quantifiers/ematching/instantiation_engine.h"
 #include "theory/quantifiers/fmf/model_engine.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
@@ -53,6 +54,11 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output
 TheoryQuantifiers::~TheoryQuantifiers() {
 }
 
+std::unique_ptr<TheoryRewriter> TheoryQuantifiers::mkTheoryRewriter()
+{
+  return std::unique_ptr<TheoryRewriter>(new QuantifiersRewriter());
+}
+
 void TheoryQuantifiers::finishInit()
 {
   // quantifiers are not evaluated in getModelValue
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index b5b07f2e6..7efe7419c 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -39,6 +39,8 @@ class TheoryQuantifiers : public Theory {
                     const LogicInfo& logicInfo);
   ~TheoryQuantifiers();
 
+  std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
   /** finish initialization */
   void finishInit() override;
   void preRegisterTerm(TNode n) override;
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index b3f1e23d7..54b9f319d 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -96,6 +96,12 @@ Node Rewriter::rewrite(TNode node) {
   return getInstance().rewriteTo(theoryOf(node), node);
 }
 
+void Rewriter::registerTheoryRewriter(theory::TheoryId tid,
+                                      std::unique_ptr<TheoryRewriter> trew)
+{
+  getInstance().d_theoryRewriters[tid] = std::move(trew);
+}
+
 void Rewriter::registerPreRewrite(
     Kind k, std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn)
 {
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index f7298e1fb..8a641743b 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -62,6 +62,16 @@ class Rewriter {
    */
   static void clearCaches();
 
+  /**
+   * Registers a theory rewriter with this rewriter. This transfers the
+   * ownership of the theory rewriter to the rewriter.
+   *
+   * @param tid The theory that the theory rewriter should be associated with.
+   * @param trew The theory rewriter to register.
+   */
+  static void registerTheoryRewriter(theory::TheoryId tid,
+                                     std::unique_ptr<TheoryRewriter> trew);
+
   /**
    * Register a prerewrite for a given kind.
    *
diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h
index 1bb03e253..9f6b07389 100644
--- a/src/theory/rewriter_tables_template.h
+++ b/src/theory/rewriter_tables_template.h
@@ -63,8 +63,6 @@ ${post_rewrite_set_cache}
 
 Rewriter::Rewriter()
 {
-${rewrite_init}
-
 for (size_t i = 0; i < kind::LAST_KIND; ++i)
 {
   d_preRewriters[i] = nullptr;
@@ -75,7 +73,6 @@ for (size_t i = 0; i < theory::THEORY_LAST; ++i)
 {
   d_preRewritersEqual[i] = nullptr;
   d_postRewritersEqual[i] = nullptr;
-  d_theoryRewriters[i]->registerRewrites(this);
 }
 }
 
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 0b6e7a5fb..1d0ad904c 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -29,6 +29,7 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/rewriter.h"
+#include "theory/sep/theory_sep_rewriter.h"
 #include "theory/theory_model.h"
 #include "theory/valuation.h"
 
@@ -64,6 +65,11 @@ TheorySep::~TheorySep() {
   }
 }
 
+std::unique_ptr<TheoryRewriter> TheorySep::mkTheoryRewriter()
+{
+  return std::unique_ptr<TheoryRewriter>(new TheorySepRewriter());
+}
+
 void TheorySep::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   d_equalityEngine.setMasterEqualityEngine(eq);
 }
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index ae044f6d7..df3294882 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -66,6 +66,8 @@ class TheorySep : public Theory {
   TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
   ~TheorySep();
 
+  std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
   void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
 
   std::string identify() const override { return std::string("TheorySep"); }
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 3b0427ec5..0b9e6d934 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -15,8 +15,10 @@
  **/
 
 #include "theory/sets/theory_sets.h"
+
 #include "options/sets_options.h"
 #include "theory/sets/theory_sets_private.h"
+#include "theory/sets/theory_sets_rewriter.h"
 #include "theory/theory_model.h"
 
 using namespace CVC4::kind;
@@ -44,6 +46,11 @@ TheorySets::~TheorySets()
   // Do not move me to the header. See explanation in the constructor.
 }
 
+std::unique_ptr<TheoryRewriter> TheorySets::mkTheoryRewriter()
+{
+  return std::unique_ptr<TheoryRewriter>(new TheorySetsRewriter());
+}
+
 void TheorySets::finishInit()
 {
   TheoryModel* tm = d_valuation.getModel();
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index ed2459b32..a55a22600 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -42,6 +42,8 @@ class TheorySets : public Theory
              const LogicInfo& logicInfo);
   ~TheorySets() override;
 
+  std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
   /** finish initialization */
   void finishInit() override;
   void addSharedTerm(TNode) override;
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index a81c96318..f9eeb2010 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -26,6 +26,7 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/ext_theory.h"
 #include "theory/rewriter.h"
+#include "theory/strings/sequences_rewriter.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "theory/strings/type_enumerator.h"
 #include "theory/strings/word.h"
@@ -129,6 +130,11 @@ TheoryStrings::~TheoryStrings() {
 
 }
 
+std::unique_ptr<TheoryRewriter> TheoryStrings::mkTheoryRewriter()
+{
+  return std::unique_ptr<TheoryRewriter>(new SequencesRewriter());
+}
+
 bool TheoryStrings::areCareDisequal( TNode x, TNode y ) {
   Assert(d_equalityEngine.hasTerm(x));
   Assert(d_equalityEngine.hasTerm(y));
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 76c8f0469..0e95628bc 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -109,6 +109,8 @@ class TheoryStrings : public Theory {
                 const LogicInfo& logicInfo);
   ~TheoryStrings();
 
+  std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
   void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
 
   std::string identify() const override { return std::string("TheoryStrings"); }
diff --git a/src/theory/theory.h b/src/theory/theory.h
index d6b02e070..63ca46b41 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -42,6 +42,7 @@
 #include "theory/logic_info.h"
 #include "theory/output_channel.h"
 #include "theory/theory_id.h"
+#include "theory/theory_rewriter.h"
 #include "theory/valuation.h"
 #include "util/statistics_registry.h"
 
@@ -316,6 +317,11 @@ public:
    */
   virtual ~Theory();
 
+  /**
+   * Creates a new theory rewriter for the theory.
+   */
+  virtual std::unique_ptr<TheoryRewriter> mkTheoryRewriter() = 0;
+
   /**
    * Subclasses of Theory may add additional efforts.  DO NOT CHECK
    * equality with one of these values (e.g. if STANDARD xxx) but
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index e665f6115..2c27c6054 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -266,7 +266,6 @@ void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode,
 }
 
 void TheoryEngine::finishInit() {
-
   //initialize the quantifiers engine, master equality engine, model, model builder
   if( d_logicInfo.isQuantified() ) {
     // initialize the quantifiers engine
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 840d42417..dec654e76 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -494,6 +494,8 @@ class TheoryEngine {
                                               *d_theoryOut[theoryId],
                                               theory::Valuation(this),
                                               d_logicInfo);
+    theory::Rewriter::registerTheoryRewriter(
+        theoryId, d_theoryTable[theoryId]->mkTheoryRewriter());
   }
 
   void setPropEngine(prop::PropEngine* propEngine)
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 3b42fa6a1..1ea5449b7 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -66,6 +66,11 @@ TheoryUF::TheoryUF(context::Context* c,
 TheoryUF::~TheoryUF() {
 }
 
+std::unique_ptr<TheoryRewriter> TheoryUF::mkTheoryRewriter()
+{
+  return std::unique_ptr<TheoryRewriter>(new TheoryUfRewriter());
+}
+
 void TheoryUF::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   d_equalityEngine.setMasterEqualityEngine(eq);
 }
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 93a709fe5..623c5c64b 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -188,6 +188,8 @@ private:
 
   ~TheoryUF();
 
+  std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
   void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
   void finishInit() override;
 
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 */