summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules.h3
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_core.h20
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_simplification.h187
-rw-r--r--src/theory/bv/theory_bv_rewriter.cpp46
4 files changed, 230 insertions, 26 deletions
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){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback