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

3 files changed, 63 insertions, 31 deletions

diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index b52cb91a4..c6cd9eb1c 100644
--- 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,
-  AndOrConcatPullUp,
+  AndOrXorConcatPullUp,
   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 AndOrConcatPullUp:   out << "AndOrConcatPullUp";   return out;
+  case AndOrXorConcatPullUp:out << "AndOrXorConcatPullUp";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<AndOrConcatPullUp>              rule139;
+  RewriteRule<AndOrXorConcatPullUp>           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 5e9d2b349..8ac3036cd 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -489,7 +489,7 @@ Node RewriteRule<AndOne>::apply(TNode node) {
 /* -------------------------------------------------------------------------- */
 
 /**
- * AndOrConcatPullUp
+ * AndOrXorConcatPullUp
  *
  * And:
  * ----------------------------------------------------------------
@@ -524,13 +524,32 @@ Node RewriteRule<AndOne>::apply(TNode node) {
  *   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)
  */
 
 template <>
-inline bool RewriteRule<AndOrConcatPullUp>::applies(TNode node)
+inline bool RewriteRule<AndOrXorConcatPullUp>::applies(TNode node)
 {
   if (node.getKind() != kind::BITVECTOR_AND
-      && node.getKind() != kind::BITVECTOR_OR)
+      && node.getKind() != kind::BITVECTOR_OR
+      && node.getKind() != kind::BITVECTOR_XOR)
   {
     return false;
   }
@@ -557,9 +576,9 @@ inline bool RewriteRule<AndOrConcatPullUp>::applies(TNode node)
 }
 
 template <>
-inline Node RewriteRule<AndOrConcatPullUp>::apply(TNode node)
+inline Node RewriteRule<AndOrXorConcatPullUp>::apply(TNode node)
 {
-  Debug("bv-rewrite") << "RewriteRule<AndOrConcatPullUp>(" << node << ")"
+  Debug("bv-rewrite") << "RewriteRule<AndOrXorConcatPullUp>(" << node << ")"
                       << std::endl;
   int32_t is_const;
   uint32_t m, my, mz, n;
@@ -646,7 +665,7 @@ inline Node RewriteRule<AndOrConcatPullUp>::apply(TNode node)
     }
     else
     {
-      Assert(kind == kind::BITVECTOR_OR);
+      Assert(kind == kind::BITVECTOR_OR || kind == kind::BITVECTOR_XOR);
       res << utils::mkExtract(x, m - my - 1, mz);
     }
   }
@@ -657,12 +676,17 @@ inline Node RewriteRule<AndOrConcatPullUp>::apply(TNode node)
       if (n > 1) res << utils::mkZero(n - 1);
       res << utils::mkExtract(x, mz, mz);
     }
-    else
+    else if (kind == kind::BITVECTOR_OR)
     {
-      Assert(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
   {
@@ -671,11 +695,16 @@ inline Node RewriteRule<AndOrConcatPullUp>::apply(TNode node)
     {
       res << utils::mkExtract(x, m - my - 1, mz);
     }
-    else
+    else if (kind == kind::BITVECTOR_OR)
     {
-      Assert(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));
+    }
   }
   if (mz)
   {
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 3f018f800..0c6f1d37a 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -253,7 +253,7 @@ RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool prerewrite)
   resultNode =
       LinearRewriteStrategy<RewriteRule<FlattenAssocCommutNoDuplicates>,
                             RewriteRule<AndSimplify>,
-                            RewriteRule<AndOrConcatPullUp>>::apply(node);
+                            RewriteRule<AndOrXorConcatPullUp>>::apply(node);
   if (!prerewrite)
   {
     resultNode =
@@ -274,7 +274,7 @@ RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool prerewrite)
   resultNode =
       LinearRewriteStrategy<RewriteRule<FlattenAssocCommutNoDuplicates>,
                             RewriteRule<OrSimplify>,
-                            RewriteRule<AndOrConcatPullUp>>::apply(node);
+                            RewriteRule<AndOrXorConcatPullUp>>::apply(node);
 
   if (!prerewrite)
   {
@@ -290,27 +290,30 @@ RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool prerewrite)
   return RewriteResponse(REWRITE_DONE, resultNode);
 }
 
-RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool prerewrite) {
+RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool prerewrite)
+{
   Node resultNode = node;
-  resultNode = LinearRewriteStrategy
-    < RewriteRule<FlattenAssocCommut>, // flatten the expression 
-      RewriteRule<XorSimplify>,        // simplify duplicates and constants
-      RewriteRule<XorZero>,            // checks if the constant part is zero and eliminates it
-      RewriteRule<BitwiseSlicing>
-      >::apply(node);
+  resultNode = LinearRewriteStrategy<
+      RewriteRule<FlattenAssocCommut>,  // flatten the expression
+      RewriteRule<XorSimplify>,         // simplify duplicates and constants
+      RewriteRule<XorZero>,  // checks if the constant part is zero and
+                             // eliminates it
+      RewriteRule<AndOrXorConcatPullUp>,
+      RewriteRule<BitwiseSlicing>>::apply(node);
 
-  if (!prerewrite) {
-    resultNode = LinearRewriteStrategy
-      < RewriteRule<XorOne>, 
-      RewriteRule <BitwiseSlicing>
-        >::apply(resultNode);
-    
-    if (resultNode.getKind() != node.getKind()) {
-      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+  if (!prerewrite)
+  {
+    resultNode =
+        LinearRewriteStrategy<RewriteRule<XorOne>,
+                              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::RewriteXnor(TNode node, bool prerewrite) {