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 /test | |
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 'test')
-rw-r--r-- | test/unit/theory/theory_bv_rewriter_white.h | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test/unit/theory/theory_bv_rewriter_white.h b/test/unit/theory/theory_bv_rewriter_white.h index 1f4cc0c2c..bf0ca73b3 100644 --- a/test/unit/theory/theory_bv_rewriter_white.h +++ b/test/unit/theory/theory_bv_rewriter_white.h @@ -85,6 +85,21 @@ class TheoryBvRewriterWhite : public CxxTest::TestSuite TS_ASSERT_EQUALS(nr, Rewriter::rewrite(nr)); } + void testRewriteBvIte() + { + TypeNode boolType = d_nm->booleanType(); + TypeNode bvType = d_nm->mkBitVectorType(1); + + Node zero = d_nm->mkConst(BitVector(1, 0u)); + Node c1 = d_nm->mkVar("c1", bvType); + Node c2 = d_nm->mkVar("c2", bvType); + + Node ite = d_nm->mkNode(BITVECTOR_ITE, c2, zero, zero); + Node n = d_nm->mkNode(BITVECTOR_ITE, c1, ite, ite); + Node nr = Rewriter::rewrite(n); + TS_ASSERT_EQUALS(nr, Rewriter::rewrite(nr)); + } + private: ExprManager* d_em; SmtEngine* d_smt; |