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, 39 insertions, 60 deletions

diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index 5a15d15fb..e55ca5d1c 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -19,100 +19,79 @@
 #pragma once
 
 #include "expr/node.h"
+#include "theory/theory_rewriter.h"
 #include "util/unsafe_interrupt_exception.h"
 
 namespace CVC4 {
 namespace theory {
 
-/**
- * Theory rewriters signal whether more rewriting is needed (or not)
- * by using a member of this enumeration.  See RewriteResponse, below.
- */
-enum RewriteStatus {
-  REWRITE_DONE,
-  REWRITE_AGAIN,
-  REWRITE_AGAIN_FULL
-};/* enum RewriteStatus */
-
-/**
- * Instances of this class serve as response codes from
- * Theory::preRewrite() and Theory::postRewrite().  Instances of
- * derived classes RewriteComplete(n), RewriteAgain(n), and
- * FullRewriteNeeded(n) should be used, giving self-documenting
- * rewrite behavior.
- */
-struct RewriteResponse {
-  const RewriteStatus status;
-  const Node node;
-  RewriteResponse(RewriteStatus status, Node node) :
-    status(status), node(node) {}
-};/* struct RewriteResponse */
-
 class RewriterInitializer;
 
 /**
- * The main rewriter class.  All functionality is static.
+ * The main rewriter class.
  */
 class Rewriter {
+ public:
+  Rewriter();
+
+  /**
+   * Rewrites the node using theoryOf() to determine which rewriter to
+   * use on the node.
+   */
+  static Node rewrite(TNode node);
+
+  /**
+   * Garbage collects the rewrite caches.
+   */
+  static void clearCaches();
+
+ private:
+  /**
+   * Get the (singleton) instance of the rewriter.
+   *
+   * TODO(#3468): Get rid of this singleton
+   */
+  static Rewriter& getInstance();
 
-  friend class RewriterInitializer;
-  static unsigned long d_iterationCount;
   /** Returns the appropriate cache for a node */
-  static Node getPreRewriteCache(theory::TheoryId theoryId, TNode node);
+  Node getPreRewriteCache(theory::TheoryId theoryId, TNode node);
 
   /** Returns the appropriate cache for a node */
-  static Node getPostRewriteCache(theory::TheoryId theoryId, TNode node);
+  Node getPostRewriteCache(theory::TheoryId theoryId, TNode node);
 
   /** Sets the appropriate cache for a node */
-  static void setPreRewriteCache(theory::TheoryId theoryId,
-                                 TNode node, TNode cache);
+  void setPreRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache);
 
   /** Sets the appropriate cache for a node */
-  static void setPostRewriteCache(theory::TheoryId theoryId,
-                                  TNode node, TNode cache);
-
-  // disable construction of rewriters; all functionality is static
-  Rewriter() = delete;
-  Rewriter(const Rewriter&) = delete;
+  void setPostRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache);
 
   /**
    * Rewrites the node using the given theory rewriter.
    */
-  static Node rewriteTo(theory::TheoryId theoryId, Node node);
+  Node rewriteTo(theory::TheoryId theoryId, Node node);
 
   /** Calls the pre-rewriter for the given theory */
-  static RewriteResponse callPreRewrite(theory::TheoryId theoryId, TNode node);
+  RewriteResponse callPreRewrite(theory::TheoryId theoryId, TNode node);
 
   /** Calls the post-rewriter for the given theory */
-  static RewriteResponse callPostRewrite(theory::TheoryId theoryId, TNode node);
+  RewriteResponse callPostRewrite(theory::TheoryId theoryId, TNode node);
 
   /**
    * Calls the equality-rewriter for the given theory.
    */
-  static Node callRewriteEquality(theory::TheoryId theoryId, TNode equality);
+  Node callRewriteEquality(theory::TheoryId theoryId, TNode equality);
 
-  /**
-   * Should be called before the rewriter gets used for the first time.
-   */
-  static void init();
+  void clearCachesInternal();
 
-  /**
-   * Should be called to clean up any state.
-   */
-  static void shutdown();
-  static void clearCachesInternal();
-public:
+  /** Theory rewriters managed by this rewriter instance */
+  std::unique_ptr<TheoryRewriter> d_theoryRewriters[theory::THEORY_LAST];
 
-  /**
-   * Rewrites the node using theoryOf() to determine which rewriter to
-   * use on the node.
-   */
-  static Node rewrite(TNode node);
+  unsigned long d_iterationCount = 0;
 
-  /**
-   * Garbage collects the rewrite caches.
-   */
-  static void clearCaches();
+#ifdef CVC4_ASSERTIONS
+  std::unique_ptr<std::unordered_set<Node, NodeHashFunction>> d_rewriteStack =
+      nullptr;
+#endif /* CVC4_ASSERTIONS */
 };/* class Rewriter */
 
 }/* CVC4::theory namespace */