BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with ones...

diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index d40bbcfada5317305237dd9da98029d1ba49ac90..ea298d0e14414a84774772f904d03c75072d06ad 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -499,6 +499,11 @@ Node RewriteRule<AndOne>::apply(TNode node) {
  *                     0_[n-1],
  *                     x[m-my-n:m-my-n],
  *                     x[m-my-n-1:0] & z)
+ *
+ * Match:       x_m & concat(y_my, ~0_n, z_mz)
+ * Rewrites to: concat(x[m-1:m-my] & y,
+ *                     x[m-my-1:m-my-n],
+ *                     x[m-my-n-1:0] & z)
  */
 
 template <>
@@ -524,7 +529,7 @@ inline bool RewriteRule<AndConcatPullUp>::applies(TNode node)
     }
   }
   if (n.isNull()) return false;
-  return utils::isZero(n) || utils::isOne(n);
+  return utils::isZero(n) || utils::isOne(n) || utils::isOnes(n);
 }
 
 template <>
@@ -556,7 +561,7 @@ inline Node RewriteRule<AndConcatPullUp>::apply(TNode node)
   }
   x = xb.getNumChildren() > 1 ? xb.constructNode() : xb[0];
 
-  is_const = -1;
+  is_const = -2;
   for (const TNode& child : concat)
   {
     if (c.isNull())
@@ -571,6 +576,11 @@ inline Node RewriteRule<AndConcatPullUp>::apply(TNode node)
         is_const = 1;
         c = child;
       }
+      else if (utils::isOnes(child))
+      {
+        is_const = -1;
+        c = child;
+      }
       else
       {
         yb << child;
@@ -608,12 +618,16 @@ inline Node RewriteRule<AndConcatPullUp>::apply(TNode node)
   {
     res << c;
   }
-  else
+  else if (is_const == 1)
   {
-    Assert(is_const == 1);
     if (n > 1) res << utils::mkZero(n-1);
     res << utils::mkExtract(x, m-my-n, m-my-n);
   }
+  else
+  {
+    Assert(is_const == -1);
+    res << utils::mkExtract(x, m-my-1, m-my-n);
+  }
   if (mz)
   {
     res << nm->mkNode(