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, 10 insertions, 14 deletions

diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index d483bf994..d9fe2fecc 100644
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -15,11 +15,12 @@
  ** \todo document this file
  **/
 
-#include "expr/attribute.h"
 #include "theory/builtin/theory_builtin_rewriter.h"
 
+#include "expr/attribute.h"
 #include "expr/chain.h"
 #include "expr/node_algorithm.h"
+#include "theory/rewriter.h"
 
 using namespace std;
 
diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h
index 5f703fa00..05b1b643c 100644
--- a/src/theory/builtin/theory_builtin_rewriter.h
+++ b/src/theory/builtin/theory_builtin_rewriter.h
@@ -20,15 +20,15 @@
 #ifndef CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H
 #define CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H
 
-#include "theory/rewriter.h"
 #include "theory/theory.h"
+#include "theory/theory_rewriter.h"
 
 namespace CVC4 {
 namespace theory {
 namespace builtin {
 
-class TheoryBuiltinRewriter {
-
+class TheoryBuiltinRewriter : public TheoryRewriter
+{
   static Node blastDistinct(TNode node);
   static Node blastChain(TNode node);
 
@@ -45,17 +45,12 @@ public:
     }
   }
 
-  static RewriteResponse postRewrite(TNode node);
-
-  static inline RewriteResponse preRewrite(TNode node) {
-    return doRewrite(node);
-  }
+  RewriteResponse postRewrite(TNode node) override;
 
-  static inline void init() {}
-  static inline void shutdown() {}
+  RewriteResponse preRewrite(TNode node) override { return doRewrite(node); }
 
-// conversions between lambdas and arrays
-private:  
+  // conversions between lambdas and arrays
+ private:
   /** recursive helper for getLambdaForArrayRepresentation */
   static Node getLambdaForArrayRepresentationRec( TNode a, TNode bvl, unsigned bvlIndex, 
                                                   std::unordered_map< TNode, Node, TNodeHashFunction >& visited );
@@ -124,7 +119,7 @@ private:
    * to n, this method returns null.
    */
   static Node getArrayRepresentationForLambda(TNode n);
-};/* class TheoryBuiltinRewriter */
+}; /* class TheoryBuiltinRewriter */
 
 }/* CVC4::theory::builtin namespace */
 }/* CVC4::theory namespace */