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, 5 insertions, 3 deletions

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