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

31 files changed, 130 insertions, 19 deletions

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=
@@ -140,8 +139,6 @@ function rewriter {
 
   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()));
 "
   post_rewrite_attribute_ids="${post_rewrite_attribute_ids} postids.push_back(expr::attr::AttributeManager::getAttributeId(RewriteAttibute<${theory_id}>::post_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
@@ -63,6 +63,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.
    *
    * @param k The kind to register a rewrite for.
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"
 
@@ -317,6 +318,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
    * rather use range checks (or use the helper functions below).
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;