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.

2 files changed, 22 insertions, 39 deletions

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 6b160ea67..282ae2e27 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -29,23 +29,7 @@ using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
 
-
-// thread_local AllRewriteRules* TheoryBVRewriter::s_allRules = NULL;
-// thread_local TimerStat* TheoryBVRewriter::d_rewriteTimer = NULL;
-RewriteFunction TheoryBVRewriter::d_rewriteTable[kind::LAST_KIND]; 
-void TheoryBVRewriter::init() {
-   // s_allRules = new AllRewriteRules;
-   // d_rewriteTimer = new TimerStat("theory::bv::rewriteTimer");
-   // smtStatisticsRegistry()->registerStat(d_rewriteTimer); 
-   initializeRewrites();
-
-}
-
-void TheoryBVRewriter::shutdown() {
-   // delete s_allRules;
-   // smtStatisticsRegistry()->unregisterStat(d_rewriteTimer); 
-   //delete d_rewriteTimer;
-}
+TheoryBVRewriter::TheoryBVRewriter() { initializeRewrites(); }
 
 RewriteResponse TheoryBVRewriter::preRewrite(TNode node) {
   RewriteResponse res = d_rewriteTable[node.getKind()](node, true);
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index bf707c268..8c8b7846c 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -20,7 +20,7 @@
 #ifndef CVC4__THEORY__BV__THEORY_BV_REWRITER_H
 #define CVC4__THEORY__BV__THEORY_BV_REWRITER_H
 
-#include "theory/rewriter.h"
+#include "theory/theory_rewriter.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
@@ -30,14 +30,27 @@ namespace bv {
 struct AllRewriteRules;
 typedef RewriteResponse (*RewriteFunction) (TNode, bool);
 
-class TheoryBVRewriter {
+class TheoryBVRewriter : public TheoryRewriter
+{
+ public:
+  /**
+   * Temporary hack for devision-by-zero until we refactor theory code from
+   * smt engine.
+   *
+   * @param node
+   *
+   * @return
+   */
+  static Node eliminateBVSDiv(TNode node);
 
-  static RewriteFunction d_rewriteTable[kind::LAST_KIND];
+  TheoryBVRewriter();
 
+  RewriteResponse postRewrite(TNode node) override;
+  RewriteResponse preRewrite(TNode node) override;
+
+ private:
   static RewriteResponse IdentityRewrite(TNode node, bool prerewrite = false);
   static RewriteResponse UndefinedRewrite(TNode node, bool prerewrite = false); 
-
-  static void initializeRewrites();
   
   static RewriteResponse RewriteEqual(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteUlt(TNode node, bool prerewrite = false);
@@ -86,24 +99,10 @@ class TheoryBVRewriter {
   static RewriteResponse RewriteBVToNat(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteIntToBV(TNode node, bool prerewrite = false);
 
-public:
+  void initializeRewrites();
 
-  static RewriteResponse postRewrite(TNode node);
-
-  static RewriteResponse preRewrite(TNode node);
-  
-  static void init();
-  static void shutdown();
-  /** 
-   * Temporary hack for devision-by-zero until we refactor theory code from
-   * smt engine. 
-   * 
-   * @param node 
-   * 
-   * @return 
-   */
-  static Node eliminateBVSDiv(TNode node); 
-};/* class TheoryBVRewriter */
+  RewriteFunction d_rewriteTable[kind::LAST_KIND];
+}; /* class TheoryBVRewriter */
 
 }/* CVC4::theory::bv namespace */
 }/* CVC4::theory namespace */