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, 10 insertions, 0 deletions

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.