diff options
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 17 | ||||
-rw-r--r-- | test/unit/theory/theory_bv_rewriter_white.h | 15 |
2 files changed, 29 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); 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; |