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

1 files changed, 6 insertions, 0 deletions

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