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

diff --git a/src/theory/sep/theory_sep_rewriter.h b/src/theory/sep/theory_sep_rewriter.h
index f4639efa3..0d1de3463 100644
--- a/src/theory/sep/theory_sep_rewriter.h
+++ b/src/theory/sep/theory_sep_rewriter.h
@@ -20,30 +20,32 @@
 #ifndef CVC4__THEORY__SEP__THEORY_SEP_REWRITER_H
 #define CVC4__THEORY__SEP__THEORY_SEP_REWRITER_H
 
-#include "theory/rewriter.h"
+#include "theory/theory_rewriter.h"
 #include "theory/type_enumerator.h"
 
 namespace CVC4 {
 namespace theory {
 namespace sep {
 
-
-class TheorySepRewriter {
-private:
-  static void getStarChildren( Node n, std::vector< Node >& s_children, std::vector< Node >& ns_children );
-  static void getAndChildren( Node n, std::vector< Node >& s_children, std::vector< Node >& ns_children );
-  static bool isSpatial( Node n, std::map< Node, bool >& visited );
-public:
-
-  static RewriteResponse postRewrite(TNode node);
-  static inline RewriteResponse preRewrite(TNode node) {
+class TheorySepRewriter : public TheoryRewriter
+{
+ public:
+  RewriteResponse postRewrite(TNode node) override;
+  RewriteResponse preRewrite(TNode node) override
+  {
     Trace("sep-prerewrite") << "Sep::preRewrite returning " << node << std::endl;
     return RewriteResponse(REWRITE_DONE, node);
   }
 
-  static inline void init() {}
-  static inline void shutdown() {}
-};/* class TheorySepRewriter */
+ private:
+  static void getStarChildren(Node n,
+                              std::vector<Node>& s_children,
+                              std::vector<Node>& ns_children);
+  static void getAndChildren(Node n,
+                             std::vector<Node>& s_children,
+                             std::vector<Node>& ns_children);
+  static bool isSpatial(Node n, std::map<Node, bool>& visited);
+}; /* class TheorySepRewriter */
 
 }/* CVC4::theory::sep namespace */
 }/* CVC4::theory namespace */