BV rewrites (mined): Rule 35: ConcatPullUp with special const simplified. (#2647)

Simplifications based on the special const is now delegated down, only
the concat is pulled up.

diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 8ac3036cdb626e9b3ef3038a01dafc3a6de302f3..7efdc2c81b70c2a7eb553d586533c47311da220a 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -491,57 +491,12 @@ Node RewriteRule<AndOne>::apply(TNode node) {
 /**
  * AndOrXorConcatPullUp
  *
- * And:
- * ----------------------------------------------------------------
- *   Match:       x_m & concat(y_my, 0_n, z_mz)
- *   Rewrites to: concat(x[m-1:m-my] & y, 0_n, x[mz-1:0] & z)
+ * Match:       x_m <op> concat(y_my, <const>_n, z_mz)
+ *              <const>_n in { 0_n, 1_n, ~0_n }
  *
- *   Match:       x_m & concat(y_my, 1_n, z_mz)
- *   Rewrites to: concat(x[m-1:m-my] & y,
- *                       0_[n-1],
- *                       x[mz:mz],
- *                       x[mz-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:mz],
- *                     x[mz-1:0] & z)
- *
- * Or:
- * ----------------------------------------------------------------
- *   Match:       x_m | concat(y_my, 0_n, z_mz)
- *   Rewrites to: concat(x[m-1:m-my] | y,
- *                       x[m-my-1:mz],
- *                       x[mz-1:0] | z)
- *
- *   Match:       x_m | concat(y_my, 1_n, z_mz)
- *   Rewrites to: concat(x[m-1:m-my] | y,
- *                       x[m-my-1:mz+1],
- *                       1_1,
- *                       x[mz-1:0] | z)
- *
- *   Match:       x_m | concat(y_my, ~0_n, z_mz)
- *   Rewrites to: concat(x[m-1:m-my] | y,
- *                       ~0_n,
- *                       x[mz-1:0] | z)
- *
- * Xor:
- * ----------------------------------------------------------------
- *   Match:       x_m ^ concat(y_my, 0_n, z_mz)
- *   Rewrites to: concat(x[m-1:m-my] ^ y,
- *                       x[m-my-1:mz],
- *                       x[mz-1:0] ^ z)
- *
- *   Match:       x_m ^ concat(y_my, 1_n, z_mz)
- *   Rewrites to: concat(x[m-1:m-my] ^ y,
- *                       x[m-my-1:mz+1],
- *                       ~x[mz:mz],
- *                       x[mz-1:0] ^ z)
- *
- *   Match:       x_m ^ concat(y_my, ~0_n, z_mz)
- *   Rewrites to: concat(x[m-1:m-my] ^ y,
- *                       ~[m-my-1:mz],
- *                       x[mz-1:0] ^ z)
+ * Rewrites to: concat(x[m-1:m-my]  <op> y,
+ *                     x[m-my-1:mz] <op> <const>_n,
+ *                     x[mz-1:0]    <op> z)
  */
 
 template <>
@@ -580,7 +535,6 @@ inline Node RewriteRule<AndOrXorConcatPullUp>::apply(TNode node)
 {
   Debug("bv-rewrite") << "RewriteRule<AndOrXorConcatPullUp>(" << node << ")"
                       << std::endl;
-  int32_t is_const;
   uint32_t m, my, mz, n;
   size_t nc;
   Kind kind = node.getKind();
@@ -605,24 +559,12 @@ inline Node RewriteRule<AndOrXorConcatPullUp>::apply(TNode node)
   }
   x = xb.getNumChildren() > 1 ? xb.constructNode() : xb[0];
 
-  is_const = -2;
   for (const TNode& child : concat)
   {
     if (c.isNull())
     {
-      if (utils::isZero(child))
+      if (utils::isZero(child) || utils::isOne(child) || utils::isOnes(child))
       {
-        is_const = 0;
-        c = child;
-      }
-      else if (utils::isOne(child))
-      {
-        is_const = 1;
-        c = child;
-      }
-      else if (utils::isOnes(child))
-      {
-        is_const = -1;
         c = child;
       }
       else
@@ -657,59 +599,14 @@ inline Node RewriteRule<AndOrXorConcatPullUp>::apply(TNode node)
   {
     res << nm->mkNode(kind, utils::mkExtract(x, m - 1, m - my), y);
   }
-  if (is_const == 0)
-  {
-    if (kind == kind::BITVECTOR_AND)
-    {
-      res << c;
-    }
-    else
-    {
-      Assert(kind == kind::BITVECTOR_OR || kind == kind::BITVECTOR_XOR);
-      res << utils::mkExtract(x, m - my - 1, mz);
-    }
-  }
-  else if (is_const == 1)
-  {
-    if (kind == kind::BITVECTOR_AND)
-    {
-      if (n > 1) res << utils::mkZero(n - 1);
-      res << utils::mkExtract(x, mz, mz);
-    }
-    else if (kind == kind::BITVECTOR_OR)
-    {
-      if (n > 1) res << utils::mkExtract(x, m - my - 1, mz + 1);
-      res << utils::mkOne(1);
-    }
-    else
-    {
-      Assert(kind == kind::BITVECTOR_XOR);
-      if (n > 1) res << utils::mkExtract(x, m - my - 1, mz + 1);
-      res << nm->mkNode(kind::BITVECTOR_NOT, utils::mkExtract(x, mz, mz));
-    }
-  }
-  else
-  {
-    Assert(is_const == -1);
-    if (kind == kind::BITVECTOR_AND)
-    {
-      res << utils::mkExtract(x, m - my - 1, mz);
-    }
-    else if (kind == kind::BITVECTOR_OR)
-    {
-      res << c;
-    }
-    else
-    {
-      Assert(kind == kind::BITVECTOR_XOR);
-      res << nm->mkNode(kind::BITVECTOR_NOT,
-                        utils::mkExtract(x, m - my - 1, mz));
-    }
-  }
+
+  res << nm->mkNode(kind, utils::mkExtract(x, m - my - 1, mz), c);
+
   if (mz)
   {
     res << nm->mkNode(kind, utils::mkExtract(x, mz - 1, 0), z);
   }
+
   return res;
 }