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

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 2632a6f38..5ab285766 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -15,18 +15,18 @@
  ** \todo document this file
  **/
 
-
-#include "options/fp_options.h"
-#include "theory/rewriter.h"
-#include "theory/theory_model.h"
 #include "theory/fp/theory_fp.h"
 
-
 #include <set>
 #include <stack>
 #include <unordered_set>
 #include <vector>
 
+#include "options/fp_options.h"
+#include "theory/fp/theory_fp_rewriter.h"
+#include "theory/rewriter.h"
+#include "theory/theory_model.h"
+
 using namespace std;
 
 namespace CVC4 {
@@ -177,6 +177,11 @@ TheoryFp::TheoryFp(context::Context *c,
 
 } /* TheoryFp::TheoryFp() */
 
+std::unique_ptr<TheoryRewriter> TheoryFp::mkTheoryRewriter()
+{
+  return std::unique_ptr<TheoryRewriter>(new TheoryFpRewriter());
+}
+
 Node TheoryFp::minUF(Node node) {
   Assert(node.getKind() == kind::FLOATINGPOINT_MIN);
   TypeNode t(node.getType());
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index ad093f924..802a70435 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -38,6 +38,8 @@ class TheoryFp : public Theory {
   TheoryFp(context::Context* c, context::UserContext* u, OutputChannel& out,
            Valuation valuation, const LogicInfo& logicInfo);
 
+  std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+
   Node expandDefinition(LogicRequest& lr, Node node) override;
 
   void preRegisterTerm(TNode node) override;