2 files changed, 19 insertions, 9 deletions
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index e670121d1..29f5bb82d 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -33,9 +33,13 @@ namespace CVC4 {
 namespace theory {
 namespace booleans {
 
-std::unique_ptr<TheoryRewriter> TheoryBool::mkTheoryRewriter()
+TheoryBool::TheoryBool(context::Context* c,
+                       context::UserContext* u,
+                       OutputChannel& out,
+                       Valuation valuation,
+                       const LogicInfo& logicInfo)
+    : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo)
 {
-  return std::unique_ptr<TheoryRewriter>(new TheoryBoolRewriter());
 }
 
 Theory::PPAssertStatus TheoryBool::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index 75e375ee6..ae498165f 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -19,27 +19,33 @@
 #ifndef CVC4__THEORY__BOOLEANS__THEORY_BOOL_H
 #define CVC4__THEORY__BOOLEANS__THEORY_BOOL_H
 
-#include "theory/theory.h"
 #include "context/context.h"
+#include "theory/booleans/theory_bool_rewriter.h"
+#include "theory/theory.h"
 
 namespace CVC4 {
 namespace theory {
 namespace booleans {
 
 class TheoryBool : public Theory {
-public:
-  TheoryBool(context::Context* c, context::UserContext* u, OutputChannel& out,
-             Valuation valuation, const LogicInfo& logicInfo)
-      : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo)
-  {}
+ public:
+  TheoryBool(context::Context* c,
+             context::UserContext* u,
+             OutputChannel& out,
+             Valuation valuation,
+             const LogicInfo& logicInfo);
 
-  std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override;
+  TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
 
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
 
   //void check(Effort);
 
   std::string identify() const override { return std::string("TheoryBool"); }
+
+ private:
+  /** The theory rewriter for this theory. */
+  TheoryBoolRewriter d_rewriter;
 };/* class TheoryBool */
 
 }/* CVC4::theory::booleans namespace */