Merge branch 'master' into fixNonDumping

3 files changed, 40 insertions, 111 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..7efdc2c81 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -489,48 +489,22 @@ Node RewriteRule<AndOne>::apply(TNode node) {
 /* -------------------------------------------------------------------------- */
 
 /**
- * AndOrConcatPullUp
+ * 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)
+ * 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 <>
-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,11 +531,10 @@ 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;
   size_t nc;
   Kind kind = node.getKind();
@@ -586,24 +559,12 @@ inline Node RewriteRule<AndOrConcatPullUp>::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))
-      {
-        is_const = 0;
-        c = child;
-      }
-      else if (utils::isOne(child))
-      {
-        is_const = 1;
-        c = child;
-      }
-      else if (utils::isOnes(child))
+      if (utils::isZero(child) || utils::isOne(child) || utils::isOnes(child))
       {
-        is_const = -1;
         c = child;
       }
       else
@@ -638,49 +599,14 @@ inline Node RewriteRule<AndOrConcatPullUp>::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);
-      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
-    {
-      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);
-    if (kind == kind::BITVECTOR_AND)
-    {
-      res << utils::mkExtract(x, m - my - 1, mz);
-    }
-    else
-    {
-      Assert(kind == kind::BITVECTOR_OR);
-      res << c;
-    }
-  }
+
+  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;
 }
 
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) {