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

2 files changed, 8 insertions, 0 deletions

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 */