diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-10-17 03:12:17 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-10-17 03:12:17 +0000 |
commit | bb59480a36fb0f799af53676c07b8fca43c2fff4 (patch) | |
tree | 555fb1210e2e94ba09bb9dd447cac30a6ad2ab70 /src/theory/rewriter.h | |
parent | 5cb65d8beac0f06fcafbef99d109c09ad029b14d (diff) |
Sharing work
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. |