[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.

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index bfadbd370f23c58a189e879b1260a4d14a0d2723..c85e57b65b782f267a39c1cc7d9cb7269910bbb5 100644 (file)
--- 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<kind::BITVECTOR_CONCAT, ExtractWhole>,
       // Merge the adjacent extracts on constants
       RewriteRule<ConcatConstantMerge>>::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 31d9cfac9efbc5f40799056ed8cc26e7cba73c43..25c3322367f5b7f0c63db7ebb0b73cae8a52f247 100644 (file)
--- 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();