diff options
author | lianah <lianahady@gmail.com> | 2013-05-07 16:32:07 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-05-07 16:32:07 -0400 |
commit | 778004b0fe366f6ecfb53a594bd5be335a2dc4b7 (patch) | |
tree | 12971c38959858dedffe8601027ffe508f67c73a /src/theory | |
parent | 861d976c5c4c3d2898d6148cabd2763a020aa7ba (diff) |
one more fix for rewrites
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 25 |
1 files changed, 17 insertions, 8 deletions
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 621ae25c0..534347c4a 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -230,7 +230,7 @@ RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool prerewrite) { if (!prerewrite) { resultNode = LinearRewriteStrategy < RewriteRule<BitwiseSlicing> - >::apply(node); + >::apply(resultNode); if (resultNode.getKind() != node.getKind()) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); @@ -250,7 +250,7 @@ RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool prerewrite){ if (!prerewrite) { resultNode = LinearRewriteStrategy < RewriteRule<BitwiseSlicing> - >::apply(node); + >::apply(resultNode); if (resultNode.getKind() != node.getKind()) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); @@ -273,7 +273,7 @@ RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool prerewrite) { resultNode = LinearRewriteStrategy < RewriteRule<XorOne>, RewriteRule <BitwiseSlicing> - >::apply(node); + >::apply(resultNode); if (resultNode.getKind() != node.getKind()) { return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); @@ -341,15 +341,24 @@ RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool prerewrite) { } RewriteResponse TheoryBVRewriter::RewritePlus(TNode node, bool prerewrite) { - Node resultNode = LinearRewriteStrategy - < RewriteRule<FlattenAssocCommut>, + Node resultNode = node; + if (prerewrite) { + resultNode = LinearRewriteStrategy + < RewriteRule<FlattenAssocCommut> + >::apply(node); + return RewriteResponse(REWRITE_DONE, resultNode); + } + + resultNode = LinearRewriteStrategy + < RewriteRule<FlattenAssocCommut>, RewriteRule<PlusCombineLikeTerms> >::apply(node); - if (prerewrite || node == resultNode) { - return RewriteResponse(REWRITE_DONE, resultNode); + + if (node != resultNode) { + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } - return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); + return RewriteResponse(REWRITE_DONE, resultNode); } RewriteResponse TheoryBVRewriter::RewriteSub(TNode node, bool prerewrite){ |