From 1f47ed4a01d5cca1730bb27fb3c2a4e7a8ade232 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 1 Feb 2022 12:27:56 -0800
Subject: [PATCH] [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.
---
 src/theory/bv/theory_bv_rewriter.cpp | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

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);
 }
 
-- 
2.30.2