From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 7 Feb 2022 20:00:49 +0000 (-0800)
Subject: [BV] Fix response of `RewriteConcat` (#8074)
X-Git-Tag: cvc5-1.0.0~446
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=67708218de9a83f395daabea57f8f0a9643c2e7a;p=cvc5.git

[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 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<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 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();