BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_OR) with special const. (#2643)

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)`

Match:       `x_m | concat(y_my, 1_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, x[m-my-1:m-my-n+1], 1_1, 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, ~0_n, x[m-my-n-1:0] | z)`

On QF_BV with eager and CaDiCaL (time limit 600s, penalty 600s):
```
          | CVC4-base                              | CVC4-concatpullup-or                     |
BENCHMARK | SLVD   SAT   UNSAT   TO   MO   CPU[s]  | SLVD   SAT   UNSAT   TO  MO   CPU[s]  |
   totals | 38992 13844  25148  1082  28  984887.4 | 39028 13845  25183  1046 28  974819.1 |
```

diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 991d30824cdbc19fdc0e29c0d43a14f0a01abf1a..b52cb91a478e21a6924319521ba988faa901445b 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -119,7 +119,7 @@ enum RewriteRuleId
   BitwiseIdemp,
   AndZero,
   AndOne,
-  AndConcatPullUp,
+  AndOrConcatPullUp,
   OrZero,
   OrOne,
   XorDuplicate,
@@ -201,7 +201,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case ConcatFlatten:       out << "ConcatFlatten";       return out;
   case ConcatExtractMerge:  out << "ConcatExtractMerge";  return out;
   case ConcatConstantMerge: out << "ConcatConstantMerge"; return out;
-  case AndConcatPullUp:     out << "AndConcatPullUp";     return out;
+  case AndOrConcatPullUp:   out << "AndOrConcatPullUp";   return out;
   case ExtractExtract:      out << "ExtractExtract";      return out;
   case ExtractWhole:        out << "ExtractWhole";        return out;
   case ExtractConcat:       out << "ExtractConcat";       return out;
@@ -581,7 +581,7 @@ struct AllRewriteRules {
   RewriteRule<BvIteMergeElseIf>               rule136;
   RewriteRule<BvIteMergeThenElse>             rule137;
   RewriteRule<BvIteMergeElseElse>             rule138;
-  RewriteRule<AndConcatPullUp>                rule139;
+  RewriteRule<AndOrConcatPullUp>              rule139;
 };
 
 template<> inline

diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index ea298d0e14414a84774772f904d03c75072d06ad..5e9d2b34951f8113e384924716bb23f3944afa09 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -489,27 +489,51 @@ Node RewriteRule<AndOne>::apply(TNode node) {
 /* -------------------------------------------------------------------------- */
 
 /**
- * AndConcatPullUp
- *
- * 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)
- *
- * 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)
+ * AndOrConcatPullUp
+ *
+ * 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 & 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)
  */
 
 template <>
-inline bool RewriteRule<AndConcatPullUp>::applies(TNode node)
+inline bool RewriteRule<AndOrConcatPullUp>::applies(TNode node)
 {
-  if (node.getKind() != kind::BITVECTOR_AND) return false;
+  if (node.getKind() != kind::BITVECTOR_AND
+      && node.getKind() != kind::BITVECTOR_OR)
+  {
+    return false;
+  }
 
   TNode n;
 
@@ -533,20 +557,21 @@ inline bool RewriteRule<AndConcatPullUp>::applies(TNode node)
 }
 
 template <>
-inline Node RewriteRule<AndConcatPullUp>::apply(TNode node)
+inline Node RewriteRule<AndOrConcatPullUp>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<AndConcatPullUp>(" << node << ")"
+  Debug("bv-rewrite") << "RewriteRule<AndOrConcatPullUp>(" << node << ")"
                       << std::endl;
   int32_t is_const;
   uint32_t m, my, mz, n;
   size_t nc;
+  Kind kind = node.getKind();
   TNode concat;
   Node x, y, z, c;
-  NodeBuilder<> xb(kind::BITVECTOR_AND);
+  NodeBuilder<> xb(kind);
   NodeBuilder<> yb(kind::BITVECTOR_CONCAT);
   NodeBuilder<> zb(kind::BITVECTOR_CONCAT);
   NodeBuilder<> res(kind::BITVECTOR_CONCAT);
-  NodeManager *nm = NodeManager::currentNM();
+  NodeManager* nm = NodeManager::currentNM();
 
   for (const TNode& child : node)
   {
@@ -611,27 +636,50 @@ inline Node RewriteRule<AndConcatPullUp>::apply(TNode node)
 
   if (my)
   {
-    res << nm->mkNode(
-        kind::BITVECTOR_AND, utils::mkExtract(x, m - 1, m - my), y);
+    res << nm->mkNode(kind, utils::mkExtract(x, m - 1, m - my), y);
   }
   if (is_const == 0)
   {
-    res << c;
+    if (kind == kind::BITVECTOR_AND)
+    {
+      res << c;
+    }
+    else
+    {
+      Assert(kind == kind::BITVECTOR_OR);
+      res << utils::mkExtract(x, m - my - 1, mz);
+    }
   }
   else if (is_const == 1)
   {
-    if (n > 1) res << utils::mkZero(n-1);
-    res << utils::mkExtract(x, m-my-n, m-my-n);
+    if (kind == kind::BITVECTOR_AND)
+    {
+      if (n > 1) res << utils::mkZero(n - 1);
+      res << utils::mkExtract(x, mz, mz);
+    }
+    else
+    {
+      Assert(kind == kind::BITVECTOR_OR);
+      if (n > 1) res << utils::mkExtract(x, m - my - 1, mz + 1);
+      res << utils::mkOne(1);
+    }
   }
   else
   {
     Assert(is_const == -1);
-    res << utils::mkExtract(x, m-my-1, m-my-n);
+    if (kind == kind::BITVECTOR_AND)
+    {
+      res << utils::mkExtract(x, m - my - 1, mz);
+    }
+    else
+    {
+      Assert(kind == kind::BITVECTOR_OR);
+      res << c;
+    }
   }
   if (mz)
   {
-    res << nm->mkNode(
-        kind::BITVECTOR_AND, utils::mkExtract(x, m - my - n - 1, 0), z);
+    res << nm->mkNode(kind, utils::mkExtract(x, mz - 1, 0), z);
   }
   return res;
 }

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index cfcd8f6927183eae801bee6eae52a6367c70130b..3f018f800d42090a87d0d71cbedf4155da671c64 100644 (file)
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -253,8 +253,7 @@ RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool prerewrite)
   resultNode =
       LinearRewriteStrategy<RewriteRule<FlattenAssocCommutNoDuplicates>,
                             RewriteRule<AndSimplify>,
-                            RewriteRule<AndConcatPullUp>>::apply(node);
-
+                            RewriteRule<AndOrConcatPullUp>>::apply(node);
   if (!prerewrite)
   {
     resultNode =
@@ -269,24 +268,26 @@ RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool prerewrite)
   return RewriteResponse(REWRITE_DONE, resultNode);
 }
 
-RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool prerewrite){
+RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool prerewrite)
+{
   Node resultNode = node;
-  resultNode = LinearRewriteStrategy
-    < RewriteRule<FlattenAssocCommutNoDuplicates>,
-      RewriteRule<OrSimplify>
-      >::apply(node);
+  resultNode =
+      LinearRewriteStrategy<RewriteRule<FlattenAssocCommutNoDuplicates>,
+                            RewriteRule<OrSimplify>,
+                            RewriteRule<AndOrConcatPullUp>>::apply(node);
 
-  if (!prerewrite) {
-    resultNode = LinearRewriteStrategy
-      < RewriteRule<BitwiseSlicing>
-        >::apply(resultNode);
-    
-    if (resultNode.getKind() != node.getKind()) {
-      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+  if (!prerewrite)
+  {
+    resultNode =
+        LinearRewriteStrategy<RewriteRule<BitwiseSlicing>>::apply(resultNode);
+
+    if (resultNode.getKind() != node.getKind())
+    {
+      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
     }
   }
-  
-  return RewriteResponse(REWRITE_DONE, resultNode); 
+
+  return RewriteResponse(REWRITE_DONE, resultNode);
 }
 
 RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool prerewrite) {