Make theory rewriters non-static (#3547)

This commit changes theory rewriters to be non-static. This refactoring
is needed as a stepping stone to making our rewriter configurable: If we
have multiple solver objects with different rewrite configurations, we
cannot use `static` variables for the rewriter table in the BV rewriter
for example. It is also in line with our goal of getting rid of
  singletons in general. Note that the `Rewriter` class is still a
  singleton, which will be changed in a future commit.

1 files changed, 7 insertions, 11 deletions

diff --git a/src/theory/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h
index 250f36efa..8fc65932e 100644
--- a/src/theory/booleans/theory_bool_rewriter.h
+++ b/src/theory/booleans/theory_bool_rewriter.h
@@ -20,23 +20,19 @@
 #ifndef CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H
 #define CVC4__THEORY__BOOLEANS__THEORY_BOOL_REWRITER_H
 
-#include "theory/rewriter.h"
+#include "theory/theory_rewriter.h"
 
 namespace CVC4 {
 namespace theory {
 namespace booleans {
 
-class TheoryBoolRewriter {
+class TheoryBoolRewriter : public TheoryRewriter
+{
+ public:
+  RewriteResponse preRewrite(TNode node) override;
+  RewriteResponse postRewrite(TNode node) override;
 
-public:
-
-  static RewriteResponse preRewrite(TNode node);
-  static RewriteResponse postRewrite(TNode node);
-
-  static void init() {}
-  static void shutdown() {}
-
-};/* class TheoryBoolRewriter */
+}; /* class TheoryBoolRewriter */
 
 }/* CVC4::theory::booleans namespace */
 }/* CVC4::theory namespace */