summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/smt_engine.cpp6
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_simplification.h107
-rw-r--r--src/theory/bv/theory_bv_rewriter.cpp5
3 files changed, 88 insertions, 30 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index abefaf215..70dc04669 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4156,6 +4156,12 @@ void SmtEnginePrivate::processAssertions() {
dumpAssertions("post-substitution", d_assertions);
// Assertions ARE guaranteed to be rewritten by this point
+#ifdef CVC4_ASSERTIONS
+ for (unsigned i = 0; i < d_assertions.size(); ++i)
+ {
+ Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]);
+ }
+#endif
// Lift bit-vectors of size 1 to bool
if(options::bitvectorToBool()) {
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index a4be19253..397385996 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -1344,55 +1344,106 @@ inline Node RewriteRule<ZeroExtendUltConst>::apply(TNode node) {
*
* Rewrite sign_extend(x^n,m) < c^n+m to
*
- * x < c[n-1:0] if c <= (1 << (n - 1)).
+ * x < c[n-1:0] if (c <= (1 << (n - 1))) || (c >= (~0 << (n - 1)))
+ * x[n-1:n-1] = 0 if (1 << (n - 1)) < c <= (~0 << (n - 1)).
*
* Rewrite c^n+m < sign_extend(x^n,m) to
*
- * c[n-1:0] < x if c < (1 << (n - 1)).
+ * c[n-1:0] < x if (c < (1 << (n - 1))) || (c >= ~(1 << (n-1)))
+ * x[n-1:n-1] = 1 if ~(~0 << (n-1)) <= c <= ~(1 << (n-1))
+ *
+ * where ~(~0 << (n - 1)) == (1 << (n - 1)) - 1
+ *
*/
template <>
-inline bool RewriteRule<SignExtendUltConst>::applies(TNode node) {
- if (node.getKind() == kind::BITVECTOR_ULT &&
- ((node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND &&
- node[1].isConst()) ||
- (node[1].getKind() == kind::BITVECTOR_SIGN_EXTEND &&
- node[0].isConst()))) {
- TNode t, c;
+inline bool RewriteRule<SignExtendUltConst>::applies(TNode node)
+{
+ if (node.getKind() == kind::BITVECTOR_ULT
+ && ((node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND
+ && node[1].isConst())
+ || (node[1].getKind() == kind::BITVECTOR_SIGN_EXTEND
+ && node[0].isConst())))
+ {
+ TNode x, c;
bool is_lhs = node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND;
- if (is_lhs) {
- t = node[0][0];
+ if (is_lhs)
+ {
+ x = node[0][0];
c = node[1];
- } else {
- t = node[1][0];
+ }
+ else
+ {
+ x = node[1][0];
c = node[0];
}
BitVector bv_c = c.getConst<BitVector>();
- BitVector bv_max =
- BitVector(utils::getSize(c)).setBit(utils::getSize(t) - 1);
-
- return (is_lhs && bv_c <= bv_max) || (!is_lhs && bv_c < bv_max);
+ unsigned size_c = utils::getSize(c);
+ unsigned msb_x_pos = utils::getSize(x) - 1;
+ // (1 << (n - 1)))
+ BitVector bv_msb_x = BitVector(size_c).setBit(msb_x_pos);
+ // (~0 << (n - 1))
+ BitVector bv_upper_bits =
+ (~BitVector(size_c)).leftShift(BitVector(size_c, msb_x_pos));
+
+ return (is_lhs
+ && (bv_c <= bv_msb_x || bv_c >= bv_upper_bits
+ || (bv_msb_x < bv_c && bv_c <= bv_upper_bits)))
+ || (!is_lhs
+ && (bv_c < bv_msb_x || bv_c >= ~bv_msb_x
+ || (~bv_upper_bits <= bv_c && bv_c <= ~bv_msb_x)));
}
return false;
}
template <>
-inline Node RewriteRule<SignExtendUltConst>::apply(TNode node) {
- TNode t, c;
+inline Node RewriteRule<SignExtendUltConst>::apply(TNode node)
+{
+ TNode x, c;
bool is_lhs = node[0].getKind() == kind::BITVECTOR_SIGN_EXTEND;
- if (is_lhs) {
- t = node[0][0];
+ if (is_lhs)
+ {
+ x = node[0][0];
c = node[1];
- } else {
- t = node[1][0];
+ }
+ else
+ {
+ x = node[1][0];
c = node[0];
}
- Node c_lo =
- utils::mkConst(c.getConst<BitVector>().extract(utils::getSize(t) - 1, 0));
+ BitVector bv_c = c.getConst<BitVector>();
- if (is_lhs) {
- return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, t, c_lo);
+ unsigned size_c = utils::getSize(c);
+ unsigned msb_x_pos = utils::getSize(x) - 1;
+ Node c_lo = utils::mkConst(bv_c.extract(msb_x_pos, 0));
+ // (1 << (n - 1)))
+ BitVector bv_msb_x = BitVector(size_c).setBit(msb_x_pos);
+ // (~0 << (n - 1))
+ BitVector bv_upper_bits =
+ (~BitVector(size_c)).leftShift(BitVector(size_c, msb_x_pos));
+
+ NodeManager* nm = NodeManager::currentNM();
+ if (is_lhs)
+ {
+ // x[n-1:n-1] = 0
+ if (bv_msb_x < bv_c && bv_c <= bv_upper_bits)
+ {
+ Node msb_x = utils::mkExtract(x, msb_x_pos, msb_x_pos);
+ return nm->mkNode(kind::EQUAL, msb_x, utils::mkZero(1));
+ }
+ // x < c[n-1:0]
+ Assert(bv_c <= bv_msb_x || bv_c >= bv_upper_bits);
+ return nm->mkNode(kind::BITVECTOR_ULT, x, c_lo);
}
- return NodeManager::currentNM()->mkNode(kind::BITVECTOR_ULT, c_lo, t);
+
+ // x[n-1:n-1] = 1
+ if (~bv_upper_bits <= bv_c && bv_c <= ~bv_msb_x)
+ {
+ Node msb_x = utils::mkExtract(x, msb_x_pos, msb_x_pos);
+ return nm->mkNode(kind::EQUAL, msb_x, utils::mkOne(1));
+ }
+ // c[n-1:0] < x
+ Assert(bv_c < bv_msb_x || bv_c >= ~bv_msb_x);
+ return nm->mkNode(kind::BITVECTOR_ULT, c_lo, x);
}
template<> inline
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 6bdd2ec28..c05e67947 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -73,8 +73,9 @@ RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool prerewrite) {
RewriteRule<SignExtendUltConst>,
RewriteRule<ZeroExtendUltConst>
>::apply(node);
-
- return RewriteResponse(REWRITE_DONE, resultNode);
+
+ return RewriteResponse(resultNode == node ? REWRITE_DONE : REWRITE_AGAIN_FULL,
+ resultNode);
}
RewriteResponse TheoryBVRewriter::RewriteUltBv(TNode node, bool prerewrite) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback