From 67708218de9a83f395daabea57f8f0a9643c2e7a Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 7 Feb 2022 12:00:49 -0800 Subject: [PATCH] [BV] Fix response of `RewriteConcat` (#8074) RewriteConcat was returning REWRITE_DONE, but it could happen that applying ExtractWhole was removing an extract around another concat that could then be flattened (see added unit test for an example). This commit makes the response more conservative and only returns REWRITE_DONE if the node did not change. --- src/theory/bv/theory_bv_rewriter.cpp | 6 +++++- test/unit/theory/theory_bv_rewriter_white.cpp | 19 +++++++++++++++++++ 2 files changed, 24 insertions(+), 1 deletion(-) diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index bfadbd370..c85e57b65 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -291,7 +291,11 @@ RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node, bool prerewrite) ApplyRuleToChildren, // Merge the adjacent extracts on constants RewriteRule>::apply(node); - return RewriteResponse(REWRITE_DONE, resultNode); + + // Applying ExtractWhole to the children may result in concat nodes that can + // be flattened by this method. + return RewriteResponse(resultNode != node ? REWRITE_AGAIN : REWRITE_DONE, + resultNode); } RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool prerewrite) diff --git a/test/unit/theory/theory_bv_rewriter_white.cpp b/test/unit/theory/theory_bv_rewriter_white.cpp index 31d9cfac9..25c332236 100644 --- a/test/unit/theory/theory_bv_rewriter_white.cpp +++ b/test/unit/theory/theory_bv_rewriter_white.cpp @@ -19,6 +19,7 @@ #include "expr/node.h" #include "test_smt.h" +#include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" #include "util/bitvector.h" @@ -65,6 +66,24 @@ TEST_F(TestTheoryWhiteBvRewriter, rewrite_to_fixpoint) ASSERT_EQ(nr, Rewriter::rewrite(nr)); } +TEST_F(TestTheoryWhiteBvRewriter, rewrite_concat_to_fixpoint) +{ + TypeNode boolType = d_nodeManager->booleanType(); + TypeNode bvType = d_nodeManager->mkBitVectorType(4); + + Node zero = d_nodeManager->mkConst(BitVector(1, 0u)); + Node x = d_nodeManager->mkVar("bv", bvType); + Node y = d_nodeManager->mkVar("bv", bvType); + Node z = d_nodeManager->mkVar("bv", bvType); + + Node n = d_nodeManager->mkNode( + BITVECTOR_CONCAT, + bv::utils::mkExtract(d_nodeManager->mkNode(BITVECTOR_CONCAT, x, y), 7, 0), + z); + Node nr = Rewriter::rewrite(n); + ASSERT_EQ(nr, Rewriter::rewrite(nr)); +} + TEST_F(TestTheoryWhiteBvRewriter, rewrite_bv_ite) { TypeNode boolType = d_nodeManager->booleanType(); -- 2.30.2