mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-10 21:20:52 +00:00
Code Activity

[bv_bounds] introduce a tight bit in intervals to denote they are tight (over and under approx)

Browse source 
use this to ensure certain transformations remain sound
This commit is contained in:
Nuno Lopes 2016-02-18 15:53:11 +00:00
parent 67958efed2
commit d32b4c71d1
3 changed files with 69 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

72
src/tactic/bv/bv_bounds_tactic.cpp
View file

@ -32,14 +32,16 @@ struct interval {
// l > h: [0, h] U [l, UMAX_INT]
rational l, h;
unsigned sz;
bool tight;
explicit interval() : l(0), h(0), sz(0) {}
interval(const rational& l, const rational& h, unsigned sz) : l(l), h(h), sz(sz) {
explicit interval() : l(0), h(0), sz(0), tight(false) {}
interval(const rational& l, const rational& h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) {
SASSERT(invariant());
}
bool invariant() const {
return !l.is_neg() && !h.is_neg() && l <= uMaxInt(sz) && h <= uMaxInt(sz);
return !l.is_neg() && !h.is_neg() && l <= uMaxInt(sz) && h <= uMaxInt(sz) &&
(!is_wrapped() || l != h+rational::one());
}
bool is_full() const { return l.is_zero() && h == uMaxInt(sz); }
@ -113,13 +115,18 @@ struct interval {
return false;
// 0 .. l.. l' ... h ... h'
result = interval(std::max(l, b.l), std::min(h, b.h), sz);
result = interval(std::max(l, b.l), std::min(h, b.h), sz, tight && b.tight);
}
return true;
}
/// return false if negation is empty
bool negate(interval& result) const {
if (!tight) {
result = interval(rational::zero(), uMaxInt(sz), true);
return true;
}
if (is_full())
return false;
if (l.is_zero()) {
@ -152,40 +159,43 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
if (m_bv.is_bv_ule(e, lhs, rhs)) {
if (m_bv.is_numeral(lhs, n, sz)) { // C ule x <=> x uge C
b = interval(n, uMaxInt(sz), sz);
if (m_bv.is_numeral(rhs))
return false;
b = interval(n, uMaxInt(sz), sz, true);
v = rhs;
return true;
}
if (m_bv.is_numeral(rhs, n, sz)) { // x ule C
b = interval(rational::zero(), n, sz);
b = interval(rational::zero(), n, sz, true);
v = lhs;
return true;
}
} else if (m_bv.is_bv_sle(e, lhs, rhs)) {
if (m_bv.is_numeral(lhs, n, sz)) { // C sle x <=> x sge C
b = interval(n, rational::power_of_two(sz-1) - rational::one(), sz);
if (m_bv.is_numeral(rhs))
return false;
b = interval(n, rational::power_of_two(sz-1) - rational::one(), sz, true);
v = rhs;
return true;
}
if (m_bv.is_numeral(rhs, n, sz)) { // x sle C
b = interval(rational::power_of_two(sz-1), n, sz);
b = interval(rational::power_of_two(sz-1), n, sz, true);
v = lhs;
return true;
}
} else if (m.is_eq(e, lhs, rhs)) {
if (m_bv.is_numeral(lhs, n, sz)) {
b = interval(n, n, sz);
if (m_bv.is_numeral(rhs))
return false;
b = interval(n, n, sz, true);
v = rhs;
return true;
}
if (m_bv.is_numeral(rhs, n, sz)) {
b = interval(n, n, sz);
b = interval(n, n, sz, true);
v = lhs;
return true;
}
} else if (m.is_not(e, lhs)) {
if (is_bound(lhs, v, b))
return b.negate(b);
}
return false;
}
@ -199,7 +209,7 @@ public:
virtual ~bv_bounds_simplifier() {}
virtual void assert_expr(expr * t, bool sign) {
virtual bool assert_expr(expr * t, bool sign) {
while (m.is_not(t, t)) {
sign = !sign;
}
@ -207,34 +217,54 @@ public:
interval b;
expr* t1;
if (is_bound(t, t1, b)) {
SASSERT(!m_bv.is_numeral(t1));
if (sign)
VERIFY(b.negate(b));
push();
TRACE("bv", tout << (sign?"(not ":"") << mk_pp(t, m) << (sign ? ")" : "") << ": " << mk_pp(t1, m) << " in " << b << "\n";);
interval& r = m_bound->insert_if_not_there2(t1, b)->get_data().m_value;
VERIFY(r.intersect(b, r));
return r.intersect(b, r);
}
return true;
}
virtual bool simplify(expr* t, expr_ref& result) {
expr* t1;
interval b, ctx, intr;
result = 0;
bool sign = false;
while (m.is_not(t, t)) {
sign = !sign;
}
if (!is_bound(t, t1, b))
return false;
if (m_bound->find(t1, ctx)) {
if (!b.intersect(ctx, intr)) {
if (sign && b.tight) {
sign = false;
if (!b.negate(b)) {
result = m.mk_false();
} else if (intr.l == intr.h && intr != b) {
result = m.mk_eq(t1, m_bv.mk_numeral(intr.l, m.get_sort(t1)));
} else if (ctx.implies(b)) {
result = m.mk_true();
return true;
}
}
if (m_bound->find(t1, ctx)) {
if (ctx.implies(b)) {
result = m.mk_true();
} else if (!b.intersect(ctx, intr)) {
result = m.mk_false();
} else if (intr.l == intr.h) {
result = m.mk_eq(t1, m_bv.mk_numeral(intr.l, m.get_sort(t1)));
}
} else if (b.is_full() && b.tight) {
result = m.mk_true();
}
CTRACE("bv", result != 0, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << result << "\n";);
if (sign && result != 0)
result = m.mk_not(result);
return result != 0;
}