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