From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Mon, 8 Oct 2018 17:35:21 +0000 (-0700)
Subject: BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_AND) with 0 (#2596).
X-Git-Tag: cvc5-1.0.0~4419
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=026c5b171924e7e8411215aec0a3d8305f99af47;p=cvc5.git

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

diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 97284a01b..991d30824 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -119,6 +119,7 @@ enum RewriteRuleId
   BitwiseIdemp,
   AndZero,
   AndOne,
+  AndConcatPullUp,
   OrZero,
   OrOne,
   XorDuplicate,
@@ -200,6 +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 ExtractExtract:      out << "ExtractExtract";      return out;
   case ExtractWhole:        out << "ExtractWhole";        return out;
   case ExtractConcat:       out << "ExtractConcat";       return out;
@@ -579,6 +581,7 @@ struct AllRewriteRules {
   RewriteRule<BvIteMergeElseIf>               rule136;
   RewriteRule<BvIteMergeThenElse>             rule137;
   RewriteRule<BvIteMergeElseElse>             rule138;
+  RewriteRule<AndConcatPullUp>                rule139;
 };
 
 template<> inline
diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h
index 34d8cbab1..42bf09d92 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_core.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_core.h
@@ -26,6 +26,8 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
+/* -------------------------------------------------------------------------- */
+
 template<> inline
 bool RewriteRule<ConcatFlatten>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_CONCAT);
@@ -52,6 +54,8 @@ Node RewriteRule<ConcatFlatten>::apply(TNode node) {
   return resultNode;
 }
 
+/* -------------------------------------------------------------------------- */
+
 template<> inline
 bool RewriteRule<ConcatExtractMerge>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_CONCAT);
@@ -113,6 +117,8 @@ Node RewriteRule<ConcatExtractMerge>::apply(TNode node) {
   return utils::mkConcat(mergedExtracts);
 }
 
+/* -------------------------------------------------------------------------- */
+
 template<> inline
 bool RewriteRule<ConcatConstantMerge>::applies(TNode node) {
   return node.getKind() == kind::BITVECTOR_CONCAT;
@@ -155,6 +161,8 @@ Node RewriteRule<ConcatConstantMerge>::apply(TNode node) {
   return utils::mkConcat(mergedConstants);
 }
 
+/* -------------------------------------------------------------------------- */
+
 template<> inline
 bool RewriteRule<ExtractWhole>::applies(TNode node) {
   if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
@@ -172,6 +180,8 @@ Node RewriteRule<ExtractWhole>::apply(TNode node) {
   return node[0];
 }
 
+/* -------------------------------------------------------------------------- */
+
 template<> inline
 bool RewriteRule<ExtractConstant>::applies(TNode node) {
   if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
@@ -187,6 +197,8 @@ Node RewriteRule<ExtractConstant>::apply(TNode node) {
   return utils::mkConst(childValue.extract(utils::getExtractHigh(node), utils::getExtractLow(node)));
 }
 
+/* -------------------------------------------------------------------------- */
+
 template<> inline
 bool RewriteRule<ExtractConcat>::applies(TNode node) {
   //Debug("bv-rewrite") << "RewriteRule<ExtractConcat>(" << node << ")" << std::endl;
@@ -221,6 +233,8 @@ Node RewriteRule<ExtractConcat>::apply(TNode node) {
   return utils::mkConcat(resultChildren);
 }
 
+/* -------------------------------------------------------------------------- */
+
 template<> inline
 bool RewriteRule<ExtractExtract>::applies(TNode node) {
   if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
@@ -242,6 +256,8 @@ Node RewriteRule<ExtractExtract>::apply(TNode node) {
   return result;
 }
 
+/* -------------------------------------------------------------------------- */
+
 template<> inline
 bool RewriteRule<FailEq>::applies(TNode node) {
   //Debug("bv-rewrite") << "RewriteRule<FailEq>(" << node << ")" << std::endl;
@@ -256,6 +272,8 @@ Node RewriteRule<FailEq>::apply(TNode node) {
   return utils::mkFalse();
 }
 
+/* -------------------------------------------------------------------------- */
+
 template<> inline
 bool RewriteRule<SimplifyEq>::applies(TNode node) {
   if (node.getKind() != kind::EQUAL) return false;
@@ -268,6 +286,8 @@ Node RewriteRule<SimplifyEq>::apply(TNode node) {
   return utils::mkTrue();
 }
 
+/* -------------------------------------------------------------------------- */
+
 template<> inline
 bool RewriteRule<ReflexivityEq>::applies(TNode node) {
   return (node.getKind() == kind::EQUAL && node[0] < node[1]);
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 9df3a0cd5..b505addaa 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -27,7 +27,8 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
-// FIXME: this rules subsume the constant evaluation ones
+
+/* -------------------------------------------------------------------------- */
 
 /**
  * BvIteConstCond
@@ -48,6 +49,8 @@ inline Node RewriteRule<BvIteConstCond>::apply(TNode node)
   return utils::isZero(node[0]) ? node[2] : node[1];
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * BvIteEqualChildren
  *
@@ -67,6 +70,8 @@ inline Node RewriteRule<BvIteEqualChildren>::apply(TNode node)
   return node[1];
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * BvIteConstChildren
  *
@@ -93,6 +98,8 @@ inline Node RewriteRule<BvIteConstChildren>::apply(TNode node)
   return NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, node[0]);
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * BvIteEqualCond
  *
@@ -126,6 +133,8 @@ inline Node RewriteRule<BvIteEqualCond>::apply(TNode node)
   return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ITE, node[0], t0, e1);
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * BvIteMergeThenIf
  *
@@ -153,6 +162,8 @@ inline Node RewriteRule<BvIteMergeThenIf>::apply(TNode node)
   return nm->mkNode(kind::BITVECTOR_ITE, cond, node[1][2], node[2]);
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * BvIteMergeElseIf
  *
@@ -178,6 +189,8 @@ inline Node RewriteRule<BvIteMergeElseIf>::apply(TNode node)
   return nm->mkNode(kind::BITVECTOR_ITE, cond, node[1][1], node[2]);
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * BvIteMergeThenElse
  *
@@ -205,6 +218,8 @@ inline Node RewriteRule<BvIteMergeThenElse>::apply(TNode node)
   return nm->mkNode(kind::BITVECTOR_ITE, cond, node[2][2], node[1]);
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * BvIteMergeElseElse
  *
@@ -232,6 +247,8 @@ inline Node RewriteRule<BvIteMergeElseElse>::apply(TNode node)
   return nm->mkNode(kind::BITVECTOR_ITE, cond, node[2][1], node[1]);
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * BvComp
  *
@@ -259,6 +276,8 @@ inline Node RewriteRule<BvComp>::apply(TNode node)
                                 : Node(node[0]);
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * ShlByConst
  *
@@ -297,6 +316,8 @@ Node RewriteRule<ShlByConst>::apply(TNode node) {
   return utils::mkConcat(left, right); 
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * LshrByConst
  *
@@ -336,6 +357,8 @@ Node RewriteRule<LshrByConst>::apply(TNode node) {
   return utils::mkConcat(left, right); 
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * AshrByConst
  *
@@ -380,6 +403,8 @@ Node RewriteRule<AshrByConst>::apply(TNode node) {
   return utils::mkConcat(left, right); 
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * BitwiseIdemp
  *
@@ -403,6 +428,8 @@ Node RewriteRule<BitwiseIdemp>::apply(TNode node) {
   return node[0]; 
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * AndZero
  * 
@@ -426,6 +453,8 @@ Node RewriteRule<AndZero>::apply(TNode node) {
   return utils::mkConst(utils::getSize(node), 0); 
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * AndOne
  * 
@@ -457,9 +486,79 @@ Node RewriteRule<AndOne>::apply(TNode node) {
   }
 }
 
+/* -------------------------------------------------------------------------- */
+
+/**
+ * AndConcatPullUp
+ *
+ * x_m & concat(0_n, z_[m-n]) --> concat(0_n, x[m-n-1:0] & z)
+ */
+
+template <>
+inline bool RewriteRule<AndConcatPullUp>::applies(TNode node)
+{
+  if (node.getKind() != kind::BITVECTOR_AND) return false;
+
+  TNode n;
+
+  for (const TNode& c : node)
+  {
+    if (c.getKind() == kind::BITVECTOR_CONCAT)
+    {
+      n = c[0];
+      break;
+    }
+  }
+  if (n.isNull()) return false;
+  return utils::isZero(n);
+}
+
+template <>
+inline Node RewriteRule<AndConcatPullUp>::apply(TNode node)
+{
+  Debug("bv-rewrite") << "RewriteRule<AndConcatPullUp>(" << node << ")"
+                      << std::endl;
+  uint32_t m, n;
+  TNode concat;
+  Node x, z;
+  NodeBuilder<> xb(kind::BITVECTOR_AND);
+  NodeBuilder<> zb(kind::BITVECTOR_CONCAT);
+
+  for (const TNode& c : node)
+  {
+    if (concat.isNull() && c.getKind() == kind::BITVECTOR_CONCAT)
+    {
+      concat = c;
+    }
+    else
+    {
+      xb << c;
+    }
+  }
+  x = xb.getNumChildren() > 1 ? xb.constructNode() : xb[0];
+  Assert(utils::isZero(concat[0]));
+
+  m = utils::getSize(x);
+  n = utils::getSize(concat[0]);
+
+  for (size_t i = 1, nchildren = concat.getNumChildren(); i < nchildren; i++)
+  {
+    zb << concat[i];
+  }
+  z = zb.getNumChildren() > 1 ? zb.constructNode() : zb[0];
+  Assert(utils::getSize(z) == m - n);
+
+  return utils::mkConcat(
+      concat[0],
+      NodeManager::currentNM()->mkNode(
+          kind::BITVECTOR_AND, utils::mkExtract(x, m - n - 1, 0), z));
+}
+
+/* -------------------------------------------------------------------------- */
+
 /**
  * OrZero
- * 
+ *
  * (a bvor 0) ==> a
  */
 
@@ -487,6 +586,8 @@ Node RewriteRule<OrZero>::apply(TNode node) {
   }
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * OrOne
  * 
@@ -511,6 +612,7 @@ Node RewriteRule<OrOne>::apply(TNode node) {
   return utils::mkOnes(utils::getSize(node)); 
 }
 
+/* -------------------------------------------------------------------------- */
 
 /**
  * XorDuplicate
@@ -533,6 +635,8 @@ Node RewriteRule<XorDuplicate>::apply(TNode node) {
   return utils::mkZero(utils::getSize(node));
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * XorOne
  *
@@ -583,6 +687,8 @@ inline Node RewriteRule<XorOne>::apply(TNode node)
   return result;
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * XorZero
  *
@@ -622,6 +728,8 @@ inline Node RewriteRule<XorZero>::apply(TNode node)
   return res;
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * BitwiseNotAnd
  *
@@ -644,6 +752,8 @@ Node RewriteRule<BitwiseNotAnd>::apply(TNode node) {
   return utils::mkZero(utils::getSize(node));
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * BitwiseNegOr
  *
@@ -667,6 +777,8 @@ Node RewriteRule<BitwiseNotOr>::apply(TNode node) {
   return utils::mkOnes(size);
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * XorNot
  *
@@ -688,6 +800,8 @@ inline Node RewriteRule<XorNot>::apply(TNode node)
   return NodeManager::currentNM()->mkNode(kind::BITVECTOR_XOR, a, b);
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * NotXor
  *
@@ -715,6 +829,8 @@ inline Node RewriteRule<NotXor>::apply(TNode node)
   return utils::mkSortedNode(kind::BITVECTOR_XOR, children);
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * NotIdemp
  *
@@ -733,7 +849,7 @@ Node RewriteRule<NotIdemp>::apply(TNode node) {
   return node[0][0];
 }
 
-
+/* -------------------------------------------------------------------------- */
 
 /**
  * LtSelf
@@ -754,6 +870,8 @@ Node RewriteRule<LtSelf>::apply(TNode node) {
   return utils::mkFalse(); 
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * LteSelf
  *
@@ -773,6 +891,8 @@ Node RewriteRule<LteSelf>::apply(TNode node) {
   return utils::mkTrue(); 
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * ZeroUlt
  *
@@ -794,6 +914,8 @@ inline Node RewriteRule<ZeroUlt>::apply(TNode node)
   return nm->mkNode(kind::NOT, nm->mkNode(kind::EQUAL, node[0], node[1]));
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * UltZero
  *
@@ -813,6 +935,8 @@ Node RewriteRule<UltZero>::apply(TNode node) {
 }
 
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * 
  */
@@ -830,6 +954,8 @@ inline Node RewriteRule<UltOne>::apply(TNode node)
       kind::EQUAL, node[0], utils::mkZero(utils::getSize(node[0])));
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * 
  */
@@ -849,6 +975,8 @@ inline Node RewriteRule<SltZero>::apply(TNode node)
       kind::EQUAL, most_significant_bit, utils::mkOne(1));
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * UltSelf
  *
@@ -868,6 +996,8 @@ Node RewriteRule<UltSelf>::apply(TNode node) {
 }
 
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * UleZero
  *
@@ -887,6 +1017,8 @@ inline Node RewriteRule<UleZero>::apply(TNode node)
   return NodeManager::currentNM()->mkNode(kind::EQUAL, node[0], node[1]);
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * UleSelf
  *
@@ -905,6 +1037,7 @@ Node RewriteRule<UleSelf>::apply(TNode node) {
   return utils::mkTrue(); 
 }
 
+/* -------------------------------------------------------------------------- */
 
 /**
  * ZeroUle
@@ -924,6 +1057,8 @@ Node RewriteRule<ZeroUle>::apply(TNode node) {
   return utils::mkTrue(); 
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * UleMax
  *
@@ -946,6 +1081,8 @@ Node RewriteRule<UleMax>::apply(TNode node) {
   return utils::mkTrue(); 
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * NotUlt
  *
@@ -968,6 +1105,8 @@ inline Node RewriteRule<NotUlt>::apply(TNode node)
   return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULE, b, a);
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * NotUle
  *
@@ -990,6 +1129,8 @@ inline Node RewriteRule<NotUle>::apply(TNode node)
   return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, b, a);
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * MultPow2
  *
@@ -1065,6 +1206,8 @@ inline Node RewriteRule<MultPow2>::apply(TNode node)
   return utils::mkConcat(extract, zeros); 
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * ExtractMultLeadingBit
  *
@@ -1142,6 +1285,8 @@ Node RewriteRule<ExtractMultLeadingBit>::apply(TNode node) {
   return result;
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * NegIdemp
  *
@@ -1160,6 +1305,8 @@ Node RewriteRule<NegIdemp>::apply(TNode node) {
   return node[0][0]; 
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * UdivPow2 
  *
@@ -1206,6 +1353,8 @@ inline Node RewriteRule<UdivPow2>::apply(TNode node)
   return ret;
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * UdivZero
  *
@@ -1224,6 +1373,8 @@ inline Node RewriteRule<UdivZero>::apply(TNode node) {
   return utils::mkOnes(utils::getSize(node));
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * UdivOne
  *
@@ -1242,6 +1393,8 @@ inline Node RewriteRule<UdivOne>::apply(TNode node) {
   return node[0];
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * UremPow2
  *
@@ -1282,6 +1435,8 @@ inline Node RewriteRule<UremPow2>::apply(TNode node)
   return ret;
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * UremOne
  *
@@ -1300,6 +1455,8 @@ Node RewriteRule<UremOne>::apply(TNode node) {
   return utils::mkConst(utils::getSize(node), 0); 
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * UremSelf 
  *
@@ -1318,6 +1475,8 @@ Node RewriteRule<UremSelf>::apply(TNode node) {
   return utils::mkConst(utils::getSize(node), 0); 
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * ShiftZero
  *
@@ -1338,6 +1497,8 @@ Node RewriteRule<ShiftZero>::apply(TNode node) {
   return node[0]; 
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * BBPlusNeg
  * 
@@ -1385,6 +1546,8 @@ inline Node RewriteRule<BBPlusNeg>::apply(TNode node)
   return utils::mkNaryNode(kind::BITVECTOR_PLUS, children);
 }
 
+/* -------------------------------------------------------------------------- */
+
 template<> inline
 bool RewriteRule<MergeSignExtend>::applies(TNode node) {
   if (node.getKind() != kind::BITVECTOR_SIGN_EXTEND ||
@@ -1425,6 +1588,8 @@ Node RewriteRule<MergeSignExtend>::apply(TNode node) {
   return utils::mkSignExtend(node[0][0], amount1 + amount2);
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * ZeroExtendEqConst
  *
@@ -1464,6 +1629,8 @@ inline Node RewriteRule<ZeroExtendEqConst>::apply(TNode node) {
   return utils::mkFalse();
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * SignExtendEqConst
  *
@@ -1505,6 +1672,8 @@ inline Node RewriteRule<SignExtendEqConst>::apply(TNode node) {
   return utils::mkFalse();
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * ZeroExtendUltConst
  *
@@ -1568,6 +1737,8 @@ inline Node RewriteRule<ZeroExtendUltConst>::apply(TNode node) {
   return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, c_lo, t);
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * SignExtendUltConst
  *
@@ -1675,6 +1846,8 @@ inline Node RewriteRule<SignExtendUltConst>::apply(TNode node)
   return nm->mkNode(kind::BITVECTOR_ULT, c_lo, x);
 }
 
+/* -------------------------------------------------------------------------- */
+
 template<> inline
 bool RewriteRule<MultSlice>::applies(TNode node) {
   if (node.getKind() != kind::BITVECTOR_MULT || node.getNumChildren() != 2) {
@@ -1719,6 +1892,8 @@ inline Node RewriteRule<MultSlice>::apply(TNode node)
   return nm->mkNode(kind::BITVECTOR_PLUS, term1, term2, term3);
 }
 
+/* -------------------------------------------------------------------------- */
+
 /** 
  * x < y + 1 <=> (not y < x) and y != 1...1
  * 
@@ -1764,6 +1939,8 @@ inline Node RewriteRule<UltPlusOne>::apply(TNode node)
   return nm->mkNode(kind::AND, not_y_eq_1, not_y_lt_x);
 }
 
+/* -------------------------------------------------------------------------- */
+
 /** 
  * x ^(x-1) = 0 => 1 << sk
  * WARNING: this is an **EQUISATISFIABLE** transformation!
@@ -1814,6 +1991,8 @@ inline Node RewriteRule<IsPowerOfTwo>::apply(TNode node)
   return x_eq_sh;
 }
 
+/* -------------------------------------------------------------------------- */
+
 /**
  * Rewrite
  *   sign_extend(x+t,n) * sign_extend(a,m) < sign_extend(x,n) * sign_extend(a,m)
@@ -1867,6 +2046,8 @@ extract_ext_tuple(TNode node)
   return std::make_tuple(Node::null(), Node::null(), false);
 }
 
+/* -------------------------------------------------------------------------- */
+
 template<> inline
 bool RewriteRule<MultSltMult>::applies(TNode node)
 {
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 2c9ccf46a..cfcd8f692 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -234,39 +234,39 @@ RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool prerewrite) {
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-
-RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node, bool prerewrite) {
-  
-  Node resultNode = LinearRewriteStrategy
-    < RewriteRule<ConcatFlatten>,
+RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node, bool prerewrite)
+{
+  Node resultNode = LinearRewriteStrategy<
+      RewriteRule<ConcatFlatten>,
       // Flatten the top level concatenations
       RewriteRule<ConcatExtractMerge>,
       // Merge the adjacent extracts on non-constants
       RewriteRule<ConcatConstantMerge>,
       // Merge the adjacent extracts on constants
-      ApplyRuleToChildren<kind::BITVECTOR_CONCAT, ExtractWhole>
-      >::apply(node);
-   return RewriteResponse(REWRITE_DONE, resultNode);  
+      ApplyRuleToChildren<kind::BITVECTOR_CONCAT, ExtractWhole>>::apply(node);
+  return RewriteResponse(REWRITE_DONE, resultNode);
 }
 
-RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool prerewrite) {
+RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool prerewrite)
+{
   Node resultNode = node;
-  resultNode = LinearRewriteStrategy
-    < RewriteRule<FlattenAssocCommutNoDuplicates>,
-      RewriteRule<AndSimplify>
-      >::apply(node);
-
-  if (!prerewrite) {
-    resultNode = LinearRewriteStrategy
-      < RewriteRule<BitwiseSlicing>
-        >::apply(resultNode);
-  
-    if (resultNode.getKind() != node.getKind()) {
-      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+  resultNode =
+      LinearRewriteStrategy<RewriteRule<FlattenAssocCommutNoDuplicates>,
+                            RewriteRule<AndSimplify>,
+                            RewriteRule<AndConcatPullUp>>::apply(node);
+
+  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::RewriteOr(TNode node, bool prerewrite){