diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-03-11 06:54:50 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-11 06:54:50 -0700 |
commit | 2b355305ef635ddfaad7fe75c29221cb2f744a62 (patch) | |
tree | 1667cc362fcf2f770bf7a47b81d887f648c8a857 /src/theory/rewriter.h | |
parent | edcc81b08b4d6c67da81b7ba2fcefbab3286f02c (diff) |
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.
Diffstat (limited to 'src/theory/rewriter.h')
-rw-r--r-- | src/theory/rewriter.h | 80 |
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; |