diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-10 14:43:58 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-10 14:43:58 +0000 |
commit | 48f837c9d53e2e93b14786943f9961228e0d9933 (patch) | |
tree | 6caf8bc4dc9e6d937b7db30587257504be632589 | |
parent | 103d6a6aad30410f8d7546c25c1f5e67f1c334d7 (diff) |
Added a very fruitful assertion to the rewriter: checks that rewriting after "REWRITE_DONE" is idempotent
Found several problems where this is not the case and fixed them
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 8 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 2 | ||||
-rw-r--r-- | src/theory/rewriter.cpp | 11 |
3 files changed, 16 insertions, 5 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 197134b6a..4fa96c231 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -429,8 +429,11 @@ Node RewriteRule<SolveEq>::apply(TNode node) { // If both constants are nonzero, combine on right, otherwise leave them where they are if (rightConst != zero) { + leftConst = zero; rightConst = rightConst - leftConst; - childrenRight.push_back(utils::mkConst(rightConst)); + if (rightConst != zero) { + childrenRight.push_back(utils::mkConst(rightConst)); + } } else if (leftConst != zero) { childrenLeft.push_back(utils::mkConst(leftConst)); @@ -540,6 +543,9 @@ Node RewriteRule<SolveEq>::apply(TNode node) { newRight = utils::mkSortedNode(kind::BITVECTOR_PLUS, childrenRight); } + Assert(newLeft == Rewriter::rewrite(newLeft)); + Assert(newRight == Rewriter::rewrite(newRight)); + if (newLeft == newRight) { Assert (newLeft == utils::mkConst(size, (unsigned)0)); return utils::mkTrue(); diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index d6de6edbd..47725444d 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -107,7 +107,7 @@ RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool preregister){ RewriteRule<UleZero>, RewriteRule<UleSelf> >::apply(node); - return RewriteResponse(REWRITE_DONE, resultNode); + return RewriteResponse(resultNode == node ? REWRITE_DONE : REWRITE_AGAIN, resultNode); } RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool preregister){ diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 9e69738d3..18274e060 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -160,15 +160,20 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { // Do the post-rewrite RewriteResponse response = Rewriter::callPostRewrite((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node); // We continue with the response we got - rewriteStackTop.node = response.node; - TheoryId newTheoryId = Theory::theoryOf(rewriteStackTop.node); + TheoryId newTheoryId = Theory::theoryOf(response.node); if (newTheoryId != (TheoryId) rewriteStackTop.theoryId || response.status == REWRITE_AGAIN_FULL) { // In the post rewrite if we've changed theories, we must do a full rewrite - rewriteStackTop.node = rewriteTo(newTheoryId, rewriteStackTop.node); + rewriteStackTop.node = rewriteTo(newTheoryId, response.node); break; } else if (response.status == REWRITE_DONE) { +#ifdef CVC4_ASSERTIONS + RewriteResponse r2 = Rewriter::callPostRewrite(newTheoryId, response.node); + Assert(r2.node == response.node); +#endif + rewriteStackTop.node = response.node; break; } + rewriteStackTop.node = response.node; } // We're done with the post rewrite, so we add to the cache Rewriter::setPostRewriteCache((TheoryId) rewriteStackTop.originalTheoryId, rewriteStackTop.original, rewriteStackTop.node); |