diff options
author | Andres Noetzli <noetzli@stanford.edu> | 2019-05-17 18:47:09 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-05-17 18:47:09 -0700 |
commit | d7514f640835ba6e7c8c4db4fa6fd041bbf0fe3c (patch) | |
tree | d68a7c6816e9c86bd9ce456a5a8dad52fc6b90f1 /src/theory/bv | |
parent | 5c38c59cb40df00e29cbd9d30495833f88c6d4fb (diff) |
Fix BV ITE rewrite (#3004)
The rewrite `BvIteConstChildren` assumes that `BvIteEqualChildren` has
been applied before it runs. However, with nested ITEs, it was possible
to violate that assertion. Given `bvite(c1, bvite(c2, 0, 0), bvite(c3,
0, 0))`, `BvIteEqualChildren` would rewrite that term to `bvite(c2, 0,
0)`. The `LinearRewriteStrategy` then ran `BvIteConstChildren` on
`bvite(c2, 0, 0)` which complained about the equal children. This commit
implements a simple fix that splits the `LinearRewriteStrategy` into two
strategies to make sure that if `BvIteEqualChildren` rewrites a node, we
drop back to the `Rewriter`. This ensures that the rewrites on the
rewritten node are invoked in the correct order.
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 0f7629c5f..6b160ea67 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -171,9 +171,20 @@ RewriteResponse TheoryBVRewriter::RewriteITEBv(TNode node, bool prerewrite) Node resultNode = LinearRewriteStrategy<RewriteRule<EvalITEBv>, RewriteRule<BvIteConstCond>, - RewriteRule<BvIteEqualChildren>, - RewriteRule<BvIteConstChildren>, - RewriteRule<BvIteEqualCond>>::apply(node); + RewriteRule<BvIteEqualChildren>>::apply(node); + // If the node has been rewritten, we return here because we need to make + // sure that `BvIteEqualChildren` has been applied until we reach a fixpoint + // before applying `BvIteConstChildren`. Otherwise, `BvIteConstChildren` + // potentially performs an unsound rewrite. Returning hands back the control + // to the `Rewriter` which will then call this method again, ensuring that + // the rewrites are applied in the correct order. + if (resultNode != node) + { + return RewriteResponse(REWRITE_AGAIN, resultNode); + } + + resultNode = LinearRewriteStrategy<RewriteRule<BvIteConstChildren>, + RewriteRule<BvIteEqualCond>>::apply(node); if (resultNode != node) { return RewriteResponse(REWRITE_AGAIN, resultNode); |