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, 8 insertions, 20 deletions

diff --git a/src/theory/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h
index 463d02d6d..b6c14e30a 100644
--- a/src/theory/sets/theory_sets_rewriter.h
+++ b/src/theory/sets/theory_sets_rewriter.h
@@ -25,9 +25,9 @@ namespace CVC4 {
 namespace theory {
 namespace sets {
 
-class TheorySetsRewriter {
-public:
-
+class TheorySetsRewriter : public TheoryRewriter
+{
+ public:
   /**
    * Rewrite a node into the normal form for the theory of sets.
    * Called in post-order (really reverse-topological order) when
@@ -49,7 +49,7 @@ public:
    * expression belongs to a different theory, it will be fully
    * rewritten by that theory's rewriter.
    */
-  static RewriteResponse postRewrite(TNode node);
+  RewriteResponse postRewrite(TNode node) override;
 
   /**
    * Rewrite a node into the normal form for the theory of sets
@@ -60,30 +60,18 @@ public:
    * nasty expression).  Since it's only an optimization, the
    * implementation here can do nothing.
    */
-  static RewriteResponse preRewrite(TNode node);
+  RewriteResponse preRewrite(TNode node) override;
 
   /**
    * Rewrite an equality, in case special handling is required.
    */
-  static Node rewriteEquality(TNode equality) {
+  Node rewriteEquality(TNode equality)
+  {
     // often this will suffice
     return postRewrite(equality).node;
   }
 
-  /**
-   * Initialize the rewriter.
-   */
-  static inline void init() {
-    // nothing to do
-  }
-
-  /**
-   * Shut down the rewriter.
-   */
-  static inline void shutdown() {
-    // nothing to do
-  }
-};/* class TheorySetsRewriter */
+}; /* class TheorySetsRewriter */
 
 }/* CVC4::theory::sets namespace */
 }/* CVC4::theory namespace */