diff options
Diffstat (limited to 'src/theory/rewriter.h')
| -rw-r--r-- | src/theory/rewriter.h | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index 30267ce48..dacc4d212 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -73,7 +73,10 @@ class Rewriter { Rewriter() CVC4_UNUSED; Rewriter(const Rewriter&) CVC4_UNUSED; -public: + /** + * Rewrites the node using the given theory rewriter. + */ + static Node rewriteTo(theory::TheoryId theoryId, Node node); /** Calls the pre-rewriter for the given theory */ static RewriteResponse callPreRewrite(theory::TheoryId theoryId, TNode node); @@ -82,15 +85,24 @@ public: static RewriteResponse callPostRewrite(theory::TheoryId theoryId, TNode node); /** + * Calls the equality-rewruter for the given theory. + */ + static Node callRewriteEquality(theory::TheoryId theoryId, TNode equality); + +public: + + + /** * Rewrites the node using theoryOf() to determine which rewriter to * use on the node. */ static Node rewrite(Node node); /** - * Rewrites the node using the given theory rewriter. + * Rewrite an equality between two terms that are already in normal form, so + * that the equality is in theory-normal form. */ - static Node rewriteTo(theory::TheoryId theoryId, Node node); + static Node rewriteEquality(theory::TheoryId theoryId, TNode node); /** * Should be called before the rewriter gets used for the first time. |