Introduce tables in the rewriter (#3742)

This commit adds tables in the rewriter that store which function should
be used to rewrite which kind. We have separate tables for `EQUAL`
because every theory has its own equality rewriter.

1 files changed, 78 insertions, 2 deletions

diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index e55ca5d1c..f7298e1fb 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -28,6 +28,23 @@ namespace theory {
 class RewriterInitializer;
 
 /**
+ * The rewrite environment holds everything that the individual rewrites have
+ * access to.
+ */
+class RewriteEnvironment
+{
+};
+
+/**
+ * The identity rewrite just returns the original node.
+ *
+ * @param re The rewrite environment
+ * @param n The node to rewrite
+ * @return The original node
+ */
+RewriteResponse identityRewrite(RewriteEnvironment* re, TNode n);
+
+/**
  * The main rewriter class.
  */
 class Rewriter {
@@ -45,6 +62,44 @@ class Rewriter {
    */
   static void clearCaches();
 
+  /**
+   * Register a prerewrite for a given kind.
+   *
+   * @param k The kind to register a rewrite for.
+   * @param fn The function that performs the rewrite.
+   */
+  void registerPreRewrite(
+      Kind k, std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn);
+
+  /**
+   * Register a postrewrite for a given kind.
+   *
+   * @param k The kind to register a rewrite for.
+   * @param fn The function that performs the rewrite.
+   */
+  void registerPostRewrite(
+      Kind k, std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn);
+
+  /**
+   * Register a prerewrite for equalities belonging to a given theory.
+   *
+   * @param tid The theory to register a rewrite for.
+   * @param fn The function that performs the rewrite.
+   */
+  void registerPreRewriteEqual(
+      theory::TheoryId tid,
+      std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn);
+
+  /**
+   * Register a postrewrite for equalities belonging to a given theory.
+   *
+   * @param tid The theory to register a rewrite for.
+   * @param fn The function that performs the rewrite.
+   */
+  void registerPostRewriteEqual(
+      theory::TheoryId tid,
+      std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn);
+
  private:
   /**
    * Get the (singleton) instance of the rewriter.
@@ -71,10 +126,10 @@ class Rewriter {
   Node rewriteTo(theory::TheoryId theoryId, Node node);
 
   /** Calls the pre-rewriter for the given theory */
-  RewriteResponse callPreRewrite(theory::TheoryId theoryId, TNode node);
+  RewriteResponse preRewrite(theory::TheoryId theoryId, TNode n);
 
   /** Calls the post-rewriter for the given theory */
-  RewriteResponse callPostRewrite(theory::TheoryId theoryId, TNode node);
+  RewriteResponse postRewrite(theory::TheoryId theoryId, TNode n);
 
   /**
    * Calls the equality-rewriter for the given theory.
@@ -88,6 +143,27 @@ class Rewriter {
 
   unsigned long d_iterationCount = 0;
 
+  /** Rewriter table for prewrites. Maps kinds to rewriter function. */
+  std::function<RewriteResponse(RewriteEnvironment*, TNode)>
+      d_preRewriters[kind::LAST_KIND];
+  /** Rewriter table for postrewrites. Maps kinds to rewriter function. */
+  std::function<RewriteResponse(RewriteEnvironment*, TNode)>
+      d_postRewriters[kind::LAST_KIND];
+  /**
+   * Rewriter table for prerewrites of equalities. Maps theory to rewriter
+   * function.
+   */
+  std::function<RewriteResponse(RewriteEnvironment*, TNode)>
+      d_preRewritersEqual[theory::THEORY_LAST];
+  /**
+   * Rewriter table for postrewrites of equalities. Maps theory to rewriter
+   * function.
+   */
+  std::function<RewriteResponse(RewriteEnvironment*, TNode)>
+      d_postRewritersEqual[theory::THEORY_LAST];
+
+  RewriteEnvironment d_re;
+
 #ifdef CVC4_ASSERTIONS
   std::unique_ptr<std::unordered_set<Node, NodeHashFunction>> d_rewriteStack =
       nullptr;