From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 1 Feb 2022 20:27:56 +0000 (-0800)
Subject: [BV] Fix order of rewrites for `concat` (#8010)
X-Git-Tag: cvc5-1.0.0~484
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1f47ed4a01d5cca1730bb27fb3c2a4e7a8ade232;p=cvc5.git

[BV] Fix order of rewrites for `concat` (#8010)

This commit fixes the order of the rewrites for bit-vector
concatentation such that the rewrite that merges adjacents constants
comes last (the commit also updates the comments to be less confusing).
Before, it could happen that the rewrite step that removes unnecessary
extract operations introduces constants then then would not get merged
before returning REWRITE_DONE.
---

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 97ca24437..4bfddf1a7 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -279,13 +279,14 @@ RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool prerewrite) {
 RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node, bool prerewrite)
 {
   Node resultNode = LinearRewriteStrategy<
-      RewriteRule<ConcatFlatten>,
       // Flatten the top level concatenations
-      RewriteRule<ConcatExtractMerge>,
+      RewriteRule<ConcatFlatten>,
       // Merge the adjacent extracts on non-constants
-      RewriteRule<ConcatConstantMerge>,
+      RewriteRule<ConcatExtractMerge>,
+      // Remove extracts that have no effect
+      ApplyRuleToChildren<kind::BITVECTOR_CONCAT, ExtractWhole>,
       // Merge the adjacent extracts on constants
-      ApplyRuleToChildren<kind::BITVECTOR_CONCAT, ExtractWhole>>::apply(node);
+      RewriteRule<ConcatConstantMerge>>::apply(node);
   return RewriteResponse(REWRITE_DONE, resultNode);
 }