From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 16 Oct 2018 00:10:47 +0000 (-0700)
Subject: BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with 1 (#2596).
X-Git-Tag: cvc5-1.0.0~4417
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a2157ec8a1a34a1b12a5d8f49529b835ac62d001;p=cvc5.git

BV rewrites (mined): Rule 35: Generalized ConcatPullUp (BITVECTOR_AND) with 1 (#2596).
---

diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 36e1a9329..d40bbcfad 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -493,6 +493,12 @@ Node RewriteRule<AndOne>::apply(TNode node) {
  *
  * Match:       x_m & concat(y_my, 0_n, z_mz)
  * Rewrites to: concat(x[m-1:m-my] & y, 0_n, x[m-my-n-1:0] & z)
+ *
+ * Match:       x_m & concat(y_my, 1_n, z_mz)
+ * Rewrites to: concat(x[m-1:m-my] & y,
+ *                     0_[n-1],
+ *                     x[m-my-n:m-my-n],
+ *                     x[m-my-n-1:0] & z)
  */
 
 template <>
@@ -518,7 +524,7 @@ inline bool RewriteRule<AndConcatPullUp>::applies(TNode node)
     }
   }
   if (n.isNull()) return false;
-  return utils::isZero(n);
+  return utils::isZero(n) || utils::isOne(n);
 }
 
 template <>
@@ -526,6 +532,7 @@ inline Node RewriteRule<AndConcatPullUp>::apply(TNode node)
 {
   Debug("bv-rewrite") << "RewriteRule<AndConcatPullUp>(" << node << ")"
                       << std::endl;
+  int32_t is_const;
   uint32_t m, my, mz, n;
   size_t nc;
   TNode concat;
@@ -549,12 +556,19 @@ inline Node RewriteRule<AndConcatPullUp>::apply(TNode node)
   }
   x = xb.getNumChildren() > 1 ? xb.constructNode() : xb[0];
 
+  is_const = -1;
   for (const TNode& child : concat)
   {
     if (c.isNull())
     {
       if (utils::isZero(child))
       {
+        is_const = 0;
+        c = child;
+      }
+      else if (utils::isOne(child))
+      {
+        is_const = 1;
         c = child;
       }
       else
@@ -590,7 +604,16 @@ inline Node RewriteRule<AndConcatPullUp>::apply(TNode node)
     res << nm->mkNode(
         kind::BITVECTOR_AND, utils::mkExtract(x, m - 1, m - my), y);
   }
-  res << c;
+  if (is_const == 0)
+  {
+    res << c;
+  }
+  else
+  {
+    Assert(is_const == 1);
+    if (n > 1) res << utils::mkZero(n-1);
+    res << utils::mkExtract(x, m-my-n, m-my-n);
+  }
   if (mz)
   {
     res << nm->mkNode(