diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-04-01 14:26:23 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-04-01 14:26:23 -0700 |
commit | 41355e412a142809f63a1939a4515486ccd4c6fb (patch) | |
tree | b8b7ee334c8cdc52c72a10356adfaf769793c539 /src/theory/bv | |
parent | ae536749a2342e51c450deb62a13d5cfda965881 (diff) |
Fix RewriteITEBv to ensure rewrite to fixpoint (#2878)
`TheoryBVRewriter::RewriteITEBv()` is currently always returning the
status `REWRITE_DONE`. This can result in a situation where a rewritten
node can be rewritten again (which breaks the contract of our rewriter).
The unit test in this commit illustrates the issue. The commit fixes the
issue by returning `REWRITE_AGAIN` or `REWRITE_AGAIN_FULL` if a node
changed. `REWRITE_AGAIN_FULL` is needed if the resulting node may have a
child that is not a subterm of the original expression.
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 8f9e6614c..0f7629c5f 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -173,12 +173,19 @@ RewriteResponse TheoryBVRewriter::RewriteITEBv(TNode node, bool prerewrite) RewriteRule<BvIteConstCond>, RewriteRule<BvIteEqualChildren>, RewriteRule<BvIteConstChildren>, - RewriteRule<BvIteEqualCond>, - RewriteRule<BvIteMergeThenIf>, + RewriteRule<BvIteEqualCond>>::apply(node); + if (resultNode != node) + { + return RewriteResponse(REWRITE_AGAIN, resultNode); + } + + resultNode = + LinearRewriteStrategy<RewriteRule<BvIteMergeThenIf>, RewriteRule<BvIteMergeElseIf>, RewriteRule<BvIteMergeThenElse>, RewriteRule<BvIteMergeElseElse>>::apply(node); - return RewriteResponse(REWRITE_DONE, resultNode); + return RewriteResponse(resultNode == node ? REWRITE_DONE : REWRITE_AGAIN_FULL, + resultNode); } RewriteResponse TheoryBVRewriter::RewriteNot(TNode node, bool prerewrite){ |