[BV] Fix strategy for `RewriteExtract` (#8011)

`RewriteExtract` was being too eager to return `REWRITE_DONE`. In
particular, it could happen that a term could be rewritten by a series
of `ExtractExtract` and `ExtractConcat` rewrites, but the method would
return `REWRITE_AGAIN` after the first application of `ExtractExtract`.
This commit fixes the method to be more conservative and return
`REWRITE_AGAIN` whenever a rewrite changed the node being rewritten.
Additionally, the commit makes constant folding the last step (to
maximize the chances that it applies) and makes `ExtractExtract` rewrite
multiple nested applications of `extract` with a single application.

diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h
index cdb0a6f81565555fde2953ee634665e69b0aaab2..d3caec63acb5734b38a66acb28e188f2827fb964 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules_core.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_core.h
@@ -248,12 +248,17 @@ Node RewriteRule<ExtractExtract>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<ExtractExtract>(" << node << ")" << std::endl;
 
   // x[i:j][k:l] ~>  x[k+j:l+j]
+  uint32_t j = 0;
   Node child = node[0];
-  unsigned k = utils::getExtractHigh(node);
-  unsigned l = utils::getExtractLow(node);
-  unsigned j = utils::getExtractLow(child);
-
-  Node result = utils::mkExtract(child[0], k + j, l + j);
+  do
+  {
+    j += utils::getExtractLow(child);
+    child = child[0];
+  } while (child.getKind() == kind::BITVECTOR_EXTRACT);
+
+  uint32_t k = utils::getExtractHigh(node);
+  uint32_t l = utils::getExtractLow(node);
+  Node result = utils::mkExtract(child, k + j, l + j);
   return result;
 }
 

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 4bfddf1a7f97e46b0dd43a3d19de6849037002fb..bfadbd370f23c58a189e879b1260a4d14a0d2723 100644 (file)
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -263,17 +263,21 @@ RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool prerewrite) {
     }
   }
 
-  
-  resultNode = LinearRewriteStrategy
-    < RewriteRule<ExtractConstant>, 
+  resultNode = LinearRewriteStrategy<
+      // We could have an extract over extract
       RewriteRule<ExtractExtract>,
-      // We could get another extract over extract
+      // The extract may cover the whole bit-vector
       RewriteRule<ExtractWhole>,
-      // At this point only Extract-Whole could apply
-      RewriteRule<ExtractMultLeadingBit>
-      >::apply(node);
-  
-  return RewriteResponse(REWRITE_DONE, resultNode); 
+      // Rewrite extracts over wide multiplications
+      RewriteRule<ExtractMultLeadingBit>,
+      // Perform constant folding last to maximize chances that it applies
+      RewriteRule<ExtractConstant>>::apply(node);
+
+  // There are terms that can be rewritten by repeatedly alternating between
+  // ExtractExtract and ExtractConcat, so we have to be conservative here and
+  // return REWRITE_AGAIN if the node changed.
+  return RewriteResponse(resultNode != node ? REWRITE_AGAIN : REWRITE_DONE,
+                         resultNode);
 }
 
 RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node, bool prerewrite)