From 98a92b92554e1e1a496b184a0e7a869fdfffa317 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 17 Feb 2016 10:02:40 +0000 Subject: [PATCH] bv_bounds tactic: change representation to intervals Code by myself and Nikolaj Bjorner --- src/tactic/bv/bv_bounds_tactic.cpp | 338 ++++++++++++++++------------- 1 file changed, 184 insertions(+), 154 deletions(-) diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp index 10f050166..d1b96fa23 100644 --- a/src/tactic/bv/bv_bounds_tactic.cpp +++ b/src/tactic/bv/bv_bounds_tactic.cpp @@ -21,191 +21,221 @@ Author: #include "bv_decl_plugin.h" #include "ast_pp.h" +static rational uMaxInt(unsigned sz) { + return rational::power_of_two(sz) - rational::one(); +} + +namespace { + +struct interval { + // l < h: [l, h] + // l > h: [0, h] U [l, UMAX_INT] + rational l, h; + unsigned sz; + + explicit interval() : l(0), h(0), sz(0) {} + interval(const rational& l, const rational& h, unsigned sz) : l(l), h(h), sz(sz) { + SASSERT(invariant()); + } + + bool invariant() const { + return !l.is_neg() && !h.is_neg() && l <= uMaxInt(sz) && h <= uMaxInt(sz); + } + + bool is_full() const { return l.is_zero() && h == uMaxInt(sz); } + bool is_wrapped() const { return l > h; } + + bool implies(const interval& b) const { + if (b.is_full()) + return true; + if (is_full()) + return false; + + if (is_wrapped()) { + // l >= b.l >= b.h >= h + return b.is_wrapped() && h <= b.h && l >= b.l; + } else if (b.is_wrapped()) { + // b.l > b.h >= h >= l + // h >= l >= b.l > b.h + return h <= b.h || l >= b.l; + } else { + // + return l >= b.l && h <= b.h; + } + } + + /// return false if intersection is unsat + bool intersect(const interval& b, interval& result) const { + if (is_full() || (l == b.l && h == b.h)) { + result = b; + return true; + } + if (b.is_full()) { + result = *this; + return true; + } + + if (is_wrapped()) { + if (b.is_wrapped()) { + if (h > b.l) { + result = b; + } else if (b.h > l) { + result = *this; + } else { + result = interval(std::max(l, b.l), std::min(h, b.h), sz); + } + } else { + return b.intersect(*this, result); + } + } else if (b.is_wrapped()) { + // ... b.h ... l ... h ... b.l .. + if (h < b.l && l > b.h) { + return false; + } + // ... l ... b.l ... h ... + if (h >= b.l && l <= b.h) { + result = b; + } else if (h >= b.l) { + result = interval(b.l, h, sz); + } else { + // ... l .. b.h .. h .. b.l ... + SASSERT(l <= b.h); + result = interval(l, std::min(h, b.h), sz); + } + } else { + // 0 .. l.. l' ... h ... h' + result = interval(std::max(l, b.l), std::min(h, b.h), sz); + } + return true; + } + + /// return false if negation is empty + bool negate(interval& result) const { + if (is_full()) + return false; + if (l.is_zero()) { + result = interval(h + rational::one(), uMaxInt(sz), sz); + } else if (uMaxInt(sz) == h) { + result = interval(rational::zero(), l - rational::one(), sz); + } else { + result = interval(h + rational::one(), l - rational::one(), sz); + } + return true; + } +}; + +std::ostream& operator<<(std::ostream& o, const interval& I) { + o << "[" << I.l << ", " << I.h << "]"; + return o; +} + + class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { - ast_manager& m; - bv_util m_bv; - unsigned_vector m_scopes; - expr_ref_vector m_trail; - unsigned_vector m_trail_kind; - obj_map m_bound[4]; + ast_manager& m; + bv_util m_bv; + vector > m_scopes; + obj_map *m_bound; - obj_map & sle() { return m_bound[0]; } - obj_map & ule() { return m_bound[1]; } - obj_map & sge() { return m_bound[2]; } - obj_map & uge() { return m_bound[3]; } + bool is_bound(expr *e, expr*& v, interval& b) { + rational n; + expr *lhs, *rhs; + unsigned sz; - obj_map & bound(bool lo, bool s) { - if (lo) { - if (s) return sle(); return ule(); - } - else { - if (s) return sge(); return uge(); + 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); + v = rhs; + return true; + } + if (m_bv.is_numeral(rhs, n, sz)) { // x ule C + b = interval(rational::zero(), n, sz); + 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); + 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); + 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); + v = rhs; + return true; + } + if (m_bv.is_numeral(rhs, n, sz)) { + b = interval(n, n, sz); + v = lhs; + return true; + } } + return false; } - void add_bound(bool lo, bool s, expr* t, rational const& n) { + bool add_bound(expr* t, const interval& b) { push(); - bound(lo, s).insert(t, n); - m_trail.push_back(t); - m_trail_kind.push_back(lo?(s?0:1):(s?2:3)); + interval& r = m_bound->insert_if_not_there2(t, b)->get_data().m_value; + return r.intersect(b, r); } - bool is_bound(expr* t, expr*& b, bool& lo, bool& sign, rational& n) { - expr* t1, *t2; - unsigned sz; - if (m_bv.is_bv_ule(t, t1, t2)) { - sign = false; - if (m_bv.is_numeral(t1, n, sz)) { - lo = true; - b = t2; - return true; - } - else if (m_bv.is_numeral(t2, n, sz)) { - lo = false; - b = t1; - return true; - } - } - else if (m_bv.is_bv_sle(t, t1, t2)) { - sign = true; - if (m_bv.is_numeral(t2, n, sz)) { - n = m_bv.norm(n, sz, true); - lo = false; - b = t1; - return true; - } - else if (m_bv.is_numeral(t1, n, sz)) { - n = m_bv.norm(n, sz, true); - lo = true; - b = t2; - return true; - } - } - return false; - } - - bool is_eq_const(expr* t, expr*& b, rational& n) { - expr* t1, *t2; - unsigned sz; - if (m.is_eq(t, t1, t2)) { - if (m_bv.is_numeral(t1, n, sz)) { - b = t2; - return true; - } - if (m_bv.is_numeral(t2, n, sz)) { - b = t1; - return true; - } - } - return false; - } - public: - bv_bounds_simplifier(ast_manager& m): m(m), m_bv(m), m_trail(m) {} + bv_bounds_simplifier(ast_manager& m) : m(m), m_bv(m) { + m_scopes.push_back(obj_map()); + m_bound = &m_scopes.back(); + } virtual ~bv_bounds_simplifier() {} virtual void assert_expr(expr * t, bool sign) { - bool lo, s; + interval b; expr* t1; - rational n; - if (!shared(t)) { - return; - } - if (is_bound(t, t1, lo, s, n)) { - if (sign) { - // !(n <= t1) <=> t1 <= n - 1 - // !(t1 <= n) <=> t1 >= n + 1 - if (lo) { - n -= rational::one(); - } - else { - n += rational::one(); - } - // check overflow conditions: - rational n1 = m_bv.norm(n, m_bv.get_bv_size(t1), s); - if (n1 == n) { - TRACE("bv", tout << "(not " << mk_pp(t, m) << "): " << mk_pp(t1, m) << (lo?" <= ":" >= ") << n << "\n";); - add_bound(!lo, s, t1, n); - } - } - else { - TRACE("bv", tout << mk_pp(t, m) << ": " << mk_pp(t1, m) << (lo?" >= ":" <= ") << n << "\n";); - add_bound(lo, s, t1, n); - } + if (is_bound(t, t1, b)) { + if (sign) + VERIFY(b.negate(b)); + + TRACE("bv", tout << (sign?"(not ":"") << mk_pp(t, m) << (sign ? ")" : "") << ": " << mk_pp(t1, m) << " in " << b << "\n";); + VERIFY(add_bound(t1, b)); } } virtual bool simplify(expr* t, expr_ref& result) { - bool lo, s; expr* t1; - rational b1, b2; + interval b, ctx, intr; result = 0; - if (is_bound(t, t1, lo, s, b1)) { - if (bound(!lo, s).find(t1, b2)) { - // t1 >= b1 > b2 >= t1 - if (lo && b1 > b2) { - result = m.mk_false(); - } - // t1 <= b1 < b2 <= t1 - else if (!lo && b1 < b2) { - result = m.mk_false(); - } - else if (b1 == b2) { - result = m.mk_eq(t1, m_bv.mk_numeral(b1, m.get_sort(t1))); - } - } - if (result == 0 && bound(lo, s).find(t1, b2)) { - // b1 <= b2 <= t1 - if (lo && b1 <= b2) { - result = m.mk_true(); - } - // b1 >= b2 >= t1 - else if (!lo && b1 >= b2) { - result = m.mk_true(); - } + if (!is_bound(t, t1, b)) + return false; + + if (m_bound->find(t1, ctx)) { + 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 (ctx.implies(b)) { + result = m.mk_true(); } } - if (is_eq_const(t, t1, b1)) { - if (bound(true, false).find(t1, b2) && b2 > b1) { - result = m.mk_false(); - } - else if (bound(false, false).find(t1, b2) && b2 < b1) { - result = m.mk_false(); - } - else { - if (bound(true, true).find(t1, b2)) { - b1 = m_bv.norm(b1, m_bv.get_bv_size(t1), true); - if (b2 > b1) result = m.mk_false(); - } - if (result == 0 && bound(false, true).find(t1, b2)) { - b1 = m_bv.norm(b1, m_bv.get_bv_size(t1), true); - if (b2 < b1) result = m.mk_false(); - } - } - } - CTRACE("bv", result != 0, tout << mk_pp(t, m) << " " << (lo?"lo":"hi") << " " << b1 << " " << b2 << ": " << result << "\n";); + + CTRACE("bv", result != 0, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << result << "\n";); return result != 0; } virtual void push() { TRACE("bv", tout << "push\n";); - m_scopes.push_back(m_trail.size()); + m_scopes.push_back(*m_bound); + m_bound = &m_scopes.back(); } virtual void pop(unsigned num_scopes) { TRACE("bv", tout << "pop: " << num_scopes << "\n";); - if (num_scopes == 0) return; - unsigned old_sz = m_scopes[m_scopes.size() - num_scopes]; - for (unsigned i = old_sz; i < m_trail.size(); ++i) { - TRACE("bv", tout << "remove: " << mk_pp(m_trail[i].get(), m) << "\n";); - SASSERT(m_bound[m_trail_kind[i]].contains(m_trail[i].get())); - m_bound[m_trail_kind[i]].erase(m_trail[i].get()); - } - m_trail_kind.resize(old_sz); - m_trail.resize(old_sz); m_scopes.shrink(m_scopes.size() - num_scopes); + m_bound = &m_scopes.back(); } virtual simplifier * translate(ast_manager & m) { @@ -213,12 +243,12 @@ public: } virtual unsigned scope_level() const { - return m_scopes.size(); + return m_scopes.size() - 1; } - }; +} + tactic * mk_bv_bounds_tactic(ast_manager & m, params_ref const & p) { return clean(alloc(ctx_simplify_tactic, m, alloc(bv_bounds_simplifier, m), p)); } -