From dbc299efbb0ad79c5f92dc6f8df2aff34a951411 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 22 Jan 2023 14:41:53 -0800 Subject: [PATCH] revise bv-bounds-tactic - share common functionality - rename propagate-bv-bounds-new to propagate-bv-bound2 for now - expose configuration options in bounds propagation --- src/tactic/bv/bv_bounds_tactic.cpp | 744 +++++++++++------------- src/tactic/bv/bv_bounds_tactic.h | 2 +- src/tactic/core/dom_simplify_tactic.cpp | 4 + src/tactic/core/dom_simplify_tactic.h | 12 +- 4 files changed, 341 insertions(+), 421 deletions(-) diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp index 58183287d..f91068b40 100644 --- a/src/tactic/bv/bv_bounds_tactic.cpp +++ b/src/tactic/bv/bv_bounds_tactic.cpp @@ -32,39 +32,35 @@ static uint64_t uMaxInt(unsigned sz) { namespace { - struct interval { - // l < h: [l, h] - // l > h: [0, h] U [l, UMAX_INT] - uint64_t l = 0, h = 0; + template + struct interval_tpl : public Base { + T l, h; unsigned sz = 0; bool tight = true; - - interval() {} - - interval(uint64_t l, uint64_t h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) { - // canonicalize full set - if (is_wrapped() && l == h + 1) { - this->l = 0; - this->h = uMaxInt(sz); - } - SASSERT(invariant()); - } + + interval_tpl(T const& l, T const& h, unsigned sz, bool tight = false): l(l), h(h), sz(sz), tight(tight) {} + interval_tpl() {} bool invariant() const { - return l <= uMaxInt(sz) && h <= uMaxInt(sz) && (!is_wrapped() || l != h+1); + return + 0 <= l && (l <= Base::bound(sz)) && + 0 <= h && (h <= Base::bound(sz)) && + (!is_wrapped() || l != h + 1); } - bool is_full() const { return l == 0 && h == uMaxInt(sz); } + bool is_full() const { + return l == 0 && h == Base::bound(sz); + } bool is_wrapped() const { return l > h; } bool is_singleton() const { return l == h; } - bool operator==(const interval& b) const { + bool operator==(const interval_tpl& b) const { SASSERT(sz == b.sz); return l == b.l && h == b.h && tight == b.tight; } - bool operator!=(const interval& b) const { return !(*this == b); } + bool operator!=(const interval_tpl& b) const { return !(*this == b); } - bool implies(const interval& b) const { + bool implies(const interval_tpl& b) const { if (b.is_full()) return true; else if (is_full()) @@ -81,7 +77,7 @@ namespace { } /// return false if intersection is unsat - bool intersect(const interval& b, interval& result) const { + bool intersect(const interval_tpl& b, interval_tpl& result) const { if (is_full() || *this == b) { result = b; return true; @@ -98,7 +94,7 @@ namespace { else if (b.h >= l) result = *this; else - result = interval(std::max(l, b.l), std::min(h, b.h), sz); + result = interval_tpl(std::max(l, b.l), std::min(h, b.h), sz); } else return b.intersect(*this, result); @@ -111,45 +107,145 @@ namespace { if (h >= b.l && l <= b.h) result = b; else if (h >= b.l) - result = interval(b.l, h, sz); + result = interval_tpl(b.l, h, sz); else { // ... l .. b.h .. h .. b.l ... SASSERT(l <= b.h); - result = interval(l, std::min(h, b.h), sz); + result = interval_tpl(l, std::min(h, b.h), sz); } } else { if (l > b.h || h < b.l) return false; // 0 .. l.. l' ... h ... h' - result = interval(std::max(l, b.l), std::min(h, b.h), sz, tight && b.tight); + result = interval_tpl(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 { + bool negate(interval_tpl& result) const { if (!tight) - result = interval(0, uMaxInt(sz), true); + result = interval_tpl(Base::zero(), Base::bound(sz), sz, true); else if (is_full()) return false; - else if (l == 0) - result = interval(h + 1, uMaxInt(sz), sz); - else if (uMaxInt(sz) == h) - result = interval(0, l - 1, sz); + else if (l == 0 && Base::bound(sz) == h) + result = interval_tpl(Base::zero(), Base::bound(sz), sz); + else if (l == 0) + result = interval_tpl(h + 1, Base::bound(sz), sz); + else if (Base::bound(sz) == h) + result = interval_tpl(Base::zero(), l - 1, sz); else - result = interval(h + 1, l - 1, sz); + result = interval_tpl(h + 1, l - 1, sz); return true; } + + }; -#ifdef _TRACE - std::ostream& operator<<(std::ostream& o, const interval& I) { - o << "[" << I.l << ", " << I.h << "]"; - return o; - } -#endif + struct rinterval_base { + static rational bound(unsigned sz) { + return rational::power_of_two(sz) - 1; + } + static rational zero() { return rational::zero(); } + }; + + struct rinterval : public interval_tpl { + rinterval(rational const& l, rational const& h, unsigned sz, bool tight = false) { + this->l = l; this->h = h; this->sz = sz; this->tight = tight; + } + rinterval() { l = 0; h = 0; tight = true; } + }; + + struct iinterval_base { + static uint64_t bound(unsigned sz) { return uMaxInt(sz); } + static uint64_t zero() { return 0; } + }; + + struct iinterval : public interval_tpl { + iinterval(uint64_t l, uint64_t h, unsigned sz, bool tight = false) { + this->l = l; this->h = h; this->sz = sz; this->tight = tight; + } + iinterval() { l = 0; h = 0; sz = 0; tight = true; } + }; + + struct interval { + bool is_small = true; + iinterval i; + rinterval r; + + interval() {} + + interval(rational const& l, rational const& h, unsigned sz, bool tight = false) { + if (sz <= 64) { + is_small = true; + i.l = l.get_uint64(); + i.h = h.get_uint64(); + i.tight = tight; + i.sz = sz; + } + else { + is_small = false; + r.l = l; + r.h = h; + r.tight = tight; + r.sz = sz; + } + } + + unsigned size() const { + return is_small ? i.sz : r.sz; + } + + bool negate(interval& result) const { + result.is_small = is_small; + if (is_small) + return i.negate(result.i); + else + return r.negate(result.r); + } + + bool intersect(interval const& b, interval & result) const { + result.is_small = is_small; + SASSERT(b.is_small == is_small); + if (is_small) + return i.intersect(b.i, result.i); + else + return r.intersect(b.r, result.r); + } + + bool operator==(interval const& other) const { + SASSERT(is_small == other.is_small); + return is_small ? i == other.i : r == other.r; + } + + bool operator!=(interval const& other) const { + return !(*this == other); + } + + bool is_singleton() const { return is_small ? i.is_singleton() : r.is_singleton(); } + + bool is_full() const { return is_small ? i.is_full() : r.is_full(); } + + bool tight() const { return is_small ? i.tight : r.tight; } + + bool implies(const interval& b) const { + SASSERT(is_small == b.is_small); + return is_small ? i.implies(b.i) : r.implies(b.r); + } + + rational lo() const { return is_small ? rational(i.l, rational::ui64()) : r.l; } + rational hi() const { return is_small ? rational(i.h, rational::ui64()) : r.h; } + }; + + + std::ostream& operator<<(std::ostream& o, const interval& I) { + if (I.is_small) + return o << "[" << I.i.l << ", " << I.i.h << "]"; + else + return o << "[" << I.r.l << ", " << I.r.h << "]"; + } struct undo_bound { expr* e = nullptr; @@ -158,113 +254,100 @@ namespace { undo_bound(expr* e, const interval& b, bool fresh) : e(e), b(b), fresh(fresh) {} }; - class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { + struct bv_bounds_base { typedef obj_map map; typedef obj_map expr_set; typedef obj_map expr_cnt; ast_manager& m; - params_ref m_params; - bool m_propagate_eq = false; bv_util m_bv; vector m_scopes; - map m_bound; svector m_expr_vars; svector m_bound_exprs; + map m_bound; + bool m_propagate_eq = false; - bool is_number(expr *e, uint64_t& n, unsigned& sz) const { - rational r; - if (m_bv.is_numeral(e, r, sz) && sz <= 64) { - n = r.get_uint64(); - return true; - } - return false; + bv_bounds_base(ast_manager& m):m(m), m_bv(m) {} + + virtual ~bv_bounds_base() { + for (auto* e : m_expr_vars) + dealloc(e); + for (auto* b : m_bound_exprs) + dealloc(b); } bool is_bound(expr *e, expr*& v, interval& b) const { - uint64_t n; + rational r; expr *lhs = nullptr, *rhs = nullptr; unsigned sz; if (m_bv.is_bv_ule(e, lhs, rhs)) { - if (is_number(lhs, n, sz)) { // C ule x <=> x uge C + if (m_bv.is_numeral(lhs, r, sz)) { // C ule x <=> x uge C if (m_bv.is_numeral(rhs)) return false; - b = interval(n, uMaxInt(sz), sz, true); + b = interval(r, rational::power_of_two(sz) - 1, sz, true); v = rhs; - return true; + return true; } - if (is_number(rhs, n, sz)) { // x ule C - b = interval(0, n, sz, true); + if (m_bv.is_numeral(rhs, r, sz)) { // x ule C + b = interval(rational::zero(), r, sz, true); v = lhs; return true; } + // TBD: x + s <= x + q + // x + s <= x + // x <= x + q } else if (m_bv.is_bv_sle(e, lhs, rhs)) { - if (is_number(lhs, n, sz)) { // C sle x <=> x sge C + if (m_bv.is_numeral(lhs, r, sz)) { // C sle x <=> x sge C if (m_bv.is_numeral(rhs)) return false; - b = interval(n, (1ull << (sz-1)) - 1, sz, true); + b = interval(r, rational::power_of_two(sz-1) - 1, sz, true); v = rhs; return true; } - if (is_number(rhs, n, sz)) { // x sle C - b = interval(1ull << (sz-1), n, sz, true); + if (m_bv.is_numeral(rhs, r, sz)) { // x sle C + b = interval(rational::power_of_two(sz-1), r, sz, true); v = lhs; return true; } + // TBD: other cases for forbidden intervals } else if (m.is_eq(e, lhs, rhs)) { - if (is_number(lhs, n, sz)) { - if (m_bv.is_numeral(rhs)) - return false; - b = interval(n, n, sz, true); + if (m_bv.is_numeral(rhs)) + std::swap(lhs, rhs); + if (m_bv.is_numeral(rhs)) + return false; + if (m_bv.is_numeral(lhs, r, sz)) { + unsigned lo, hi; + expr* rhs2; + if (m_bv.is_extract(rhs, lo, hi, rhs2) && r == 0) { + unsigned sz2 = m_bv.get_bv_size(rhs2); + if (sz2 - 1 == hi) { + b = interval(rational::zero(), rational::power_of_two(lo) - 1, sz2, false); + v = rhs2; + return true; + } + } + b = interval(r, r, sz, true); v = rhs; return true; } - if (is_number(rhs, n, sz)) { - b = interval(n, n, sz, true); - v = lhs; - return true; - } } return false; } - - public: - bv_bounds_simplifier(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_bv(m) { - updt_params(p); - } - - void updt_params(params_ref const & p) override { - m_propagate_eq = p.get_bool("propagate_eq", false); - } - - static void get_param_descrs(param_descrs& r) { - r.insert("propagate-eq", CPK_BOOL, "propagate equalities from inequalities", "false"); - } - - ~bv_bounds_simplifier() override { - for (auto* v : m_expr_vars) dealloc(v); - for (auto* b : m_bound_exprs) dealloc(b); - } - - bool assert_expr(expr * t, bool sign) override { - TRACE("bv", tout << expr_ref(t, m) << "\n";); - while (m.is_not(t, t)) { - sign = !sign; - } + bool assert_expr_core(expr * t, bool sign) { + while (m.is_not(t, t)) + sign = !sign; interval b; expr* t1; if (is_bound(t, t1, b)) { - SASSERT(!m_bv.is_numeral(t1)); - if (sign) { - if (!b.negate(b)) { - return false; - } - } + SASSERT(m_bv.get_bv_size(t1) == b.size()); + SASSERT(!m_bv.is_numeral(t1)); + if (sign && !b.negate(b)) + return false; TRACE("bv", tout << (sign?"(not ":"") << mk_pp(t, m) << (sign ? ")" : "") << ": " << mk_pp(t1, m) << " in " << b << "\n";); map::obj_map_entry* e = m_bound.find_core(t1); @@ -275,22 +358,44 @@ namespace { return false; if (old == intr) return true; - m_scopes.insert(undo_bound(t1, old, false)); + m_scopes.push_back(undo_bound(t1, old, false)); old = intr; - } else { + SASSERT(old.size() == m_bv.get_bv_size(t1)); + } + else { + SASSERT(b.size() == m_bv.get_bv_size(t1)); m_bound.insert(t1, b); - m_scopes.insert(undo_bound(t1, interval(), true)); + m_scopes.push_back(undo_bound(t1, interval(), true)); } } return true; } - bool simplify(expr* t, expr_ref& result) override { + // + // x + q <= s <=> x not in [s - q + 1, -q[ + // <=> x in [-q, s - q], s != -1 + // + // x in [lo, hi] + // q = -lo + // hi = s + lo => s = hi - lo + // hi - lo != -1 + // + + expr_ref mk_bound(expr* t, rational const& lo, rational const& hi) { + sort* s = t->get_sort(); + + if (lo == hi + 1) + return expr_ref(m.mk_true(), m); + else + return expr_ref(m_bv.mk_ule(m_bv.mk_bv_add(t, m_bv.mk_numeral(-lo, s)), m_bv.mk_numeral(hi - lo, s)), m); + } + + bool simplify_core(expr* t, expr_ref& result) { expr* t1; interval b; if (m_bound.find(t, b) && b.is_singleton()) { - result = m_bv.mk_numeral(b.l, m_bv.get_bv_size(t)); + result = m_bv.mk_numeral(b.lo(), m_bv.get_bv_size(t)); return true; } @@ -298,14 +403,13 @@ namespace { return false; bool sign = false; - while (m.is_not(t, t)) { + while (m.is_not(t, t)) sign = !sign; - } if (!is_bound(t, t1, b)) return false; - if (sign && b.tight) { + if (sign && b.tight()) { sign = false; if (!b.negate(b)) { result = m.mk_false(); @@ -316,24 +420,26 @@ namespace { interval ctx, intr; result = nullptr; - if (b.is_full() && b.tight) { + if (b.is_full() && b.tight()) result = m.mk_true(); - } else 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 (m_propagate_eq && intr.is_singleton()) { - result = m.mk_eq(t1, m_bv.mk_numeral(rational(intr.l, rational::ui64()), t1->get_sort())); - } + else if (!m_bound.find(t1, ctx)) { + } + else if (ctx.implies(b)) + result = m.mk_true(); + else if (!b.intersect(ctx, intr)) + result = m.mk_false(); + else if (m_propagate_eq && intr.is_singleton()) + result = m.mk_eq(t1, m_bv.mk_numeral(intr.lo(), t1->get_sort())); + else if (false && intr != b) + result = mk_bound(t1, intr.lo(), intr.hi()); + else { + TRACE("bv", tout << mk_pp(t, m) << " b: " << b << " ctx: " << ctx << " intr " << intr << "\n"); } - CTRACE("bv", result != 0, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << result << "\n";); - if (sign && result != 0) + CTRACE("bv", result, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << result << "\n";); + if (sign && result) result = m.mk_not(result); - return result != 0; + return result != nullptr; } // check if t contains v @@ -344,18 +450,16 @@ namespace { while (!todo.empty()) { t = todo.back(); todo.pop_back(); - if (mark.is_marked(t)) { - continue; - } + if (mark.is_marked(t)) + continue; if (t == v) { todo.reset(); return true; } mark.mark(t); - if (!is_app(t)) { - continue; - } + if (!is_app(t)) + continue; app* a = to_app(t); todo.append(a->get_num_args(), a->get_args()); } @@ -398,293 +502,7 @@ namespace { return false; } - bool may_simplify(expr* t) override { - if (m_bv.is_numeral(t)) - return false; - - while (m.is_not(t, t)); - - for (auto & v : m_bound) { - if (contains(t, v.m_key)) return true; - } - - expr* t1; - interval b; - // skip common case: single bound constraint without any context for simplification - if (is_bound(t, t1, b)) { - return b.is_full() || m_bound.contains(t1); - } - - if (contains_bound(t)) { - return true; - } - return false; - } - - void pop(unsigned num_scopes) override { - TRACE("bv", tout << "pop: " << num_scopes << "\n";); - if (m_scopes.empty()) - return; - unsigned target = m_scopes.size() - num_scopes; - if (target == 0) { - m_bound.reset(); - m_scopes.reset(); - return; - } - for (unsigned i = m_scopes.size()-1; i >= target; --i) { - undo_bound& undo = m_scopes[i]; - SASSERT(m_bound.contains(undo.e)); - if (undo.fresh) { - m_bound.erase(undo.e); - } else { - m_bound.insert(undo.e, undo.b); - } - } - m_scopes.shrink(target); - } - - simplifier * translate(ast_manager & m) override { - return alloc(bv_bounds_simplifier, m, m_params); - } - - unsigned scope_level() const override { - return m_scopes.size(); - } - }; - - - class dom_bv_bounds_simplifier : public dom_simplifier { - typedef obj_map map; - typedef obj_map expr_set; - typedef obj_map expr_cnt; - - ast_manager& m; - params_ref m_params; - bool m_propagate_eq; - bv_util m_bv; - vector m_scopes; - map m_bound; - svector m_expr_vars; - svector m_bound_exprs; - - bool is_number(expr *e, uint64_t& n, unsigned& sz) const { - rational r; - if (m_bv.is_numeral(e, r, sz) && sz <= 64) { - n = r.get_uint64(); - return true; - } - return false; - } - - bool is_bound(expr *e, expr*& v, interval& b) const { - uint64_t n; - expr *lhs = nullptr, *rhs = nullptr; - unsigned sz = 0; - - if (m_bv.is_bv_ule(e, lhs, rhs)) { - if (is_number(lhs, n, sz)) { // C ule x <=> x uge C - if (m_bv.is_numeral(rhs)) - return false; - b = interval(n, uMaxInt(sz), sz, true); - v = rhs; - return true; - } - if (is_number(rhs, n, sz)) { // x ule C - b = interval(0, n, sz, true); - v = lhs; - return true; - } - } - else if (m_bv.is_bv_sle(e, lhs, rhs)) { - if (is_number(lhs, n, sz)) { // C sle x <=> x sge C - if (m_bv.is_numeral(rhs)) - return false; - b = interval(n, (1ull << (sz-1)) - 1, sz, true); - v = rhs; - return true; - } - if (is_number(rhs, n, sz)) { // x sle C - b = interval(1ull << (sz-1), n, sz, true); - v = lhs; - return true; - } - } else if (m.is_eq(e, lhs, rhs)) { - if (is_number(lhs, n, sz)) { - if (m_bv.is_numeral(rhs)) - return false; - b = interval(n, n, sz, true); - v = rhs; - return true; - } - if (is_number(rhs, n, sz)) { - b = interval(n, n, sz, true); - v = lhs; - return true; - } - } - return false; - } - - - public: - dom_bv_bounds_simplifier(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_bv(m) { - updt_params(p); - } - - virtual void updt_params(params_ref const & p) { - m_propagate_eq = p.get_bool("propagate_eq", false); - } - - static void get_param_descrs(param_descrs& r) { - r.insert("propagate-eq", CPK_BOOL, "propagate equalities from inequalities", "false"); - } - - ~dom_bv_bounds_simplifier() override { - for (auto* e : m_expr_vars) - dealloc(e); - for (auto* b : m_bound_exprs) - dealloc(b); - } - - bool assert_expr(expr * t, bool sign) override { - while (m.is_not(t, t)) - sign = !sign; - - interval b; - expr* t1; - if (is_bound(t, t1, b)) { - SASSERT(!m_bv.is_numeral(t1)); - if (sign) - VERIFY(b.negate(b)); - - TRACE("bv", tout << (sign?"(not ":"") << mk_pp(t, m) << (sign ? ")" : "") << ": " << mk_pp(t1, m) << " in " << b << "\n";); - map::obj_map_entry* e = m_bound.find_core(t1); - if (e) { - interval& old = e->get_data().m_value; - interval intr; - if (!old.intersect(b, intr)) - return false; - if (old == intr) - return true; - m_scopes.push_back(undo_bound(t1, old, false)); - old = intr; - } - else { - m_bound.insert(t1, b); - m_scopes.push_back(undo_bound(t1, interval(), true)); - } - } - return true; - } - - void operator()(expr_ref& r) override { - expr* t1, * t = r; - interval b; - - if (m_bound.find(t, b) && b.is_singleton()) { - r = m_bv.mk_numeral(b.l, m_bv.get_bv_size(t)); - return; - } - - if (!m.is_bool(t)) - return; - - bool sign = false; - while (m.is_not(t, t)) - sign = !sign; - - if (!is_bound(t, t1, b)) - return; - - if (sign && b.tight) { - sign = false; - if (!b.negate(b)) { - r = m.mk_false(); - return; - } - } - - interval ctx, intr; - bool was_updated = true; - if (b.is_full() && b.tight) - r = m.mk_true(); - else if (m_bound.find(t1, ctx)) { - if (ctx.implies(b)) - r = m.mk_true(); - else if (!b.intersect(ctx, intr)) - r = m.mk_false(); - else if (m_propagate_eq && intr.is_singleton()) - r = m.mk_eq(t1, m_bv.mk_numeral(rational(intr.l, rational::ui64()), - t1->get_sort())); - else - was_updated = false; - } - else - was_updated = false; - - TRACE("bv", tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << r << "\n";); - if (sign && was_updated) - r = m.mk_not(r); - } - - // check if t contains v - ptr_vector todo; - bool contains(expr* t, expr* v) { - ast_fast_mark1 mark; - todo.push_back(t); - while (!todo.empty()) { - t = todo.back(); - todo.pop_back(); - if (mark.is_marked(t)) - continue; - if (t == v) { - todo.reset(); - return true; - } - mark.mark(t); - - if (!is_app(t)) - continue; - app* a = to_app(t); - todo.append(a->get_num_args(), a->get_args()); - } - return false; - } - - bool contains_bound(expr* t) { - ast_fast_mark1 mark1; - ast_fast_mark2 mark2; - - todo.push_back(t); - while (!todo.empty()) { - t = todo.back(); - todo.pop_back(); - if (mark1.is_marked(t)) - continue; - mark1.mark(t); - if (!is_app(t)) - continue; - interval b; - expr* e; - if (is_bound(t, e, b)) { - if (mark2.is_marked(e)) { - todo.reset(); - return true; - } - mark2.mark(e); - if (m_bound.contains(e)) { - todo.reset(); - return true; - } - } - - app* a = to_app(t); - todo.append(a->get_num_args(), a->get_args()); - } - return false; - } - - void pop(unsigned num_scopes) override { + void pop_core(unsigned num_scopes) { TRACE("bv", tout << "pop: " << num_scopes << "\n";); if (m_scopes.empty()) return; @@ -705,16 +523,110 @@ namespace { m_scopes.shrink(target); } - dom_simplifier * translate(ast_manager & m) override { - return alloc(dom_bv_bounds_simplifier, m, m_params); + }; + + class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier, public bv_bounds_base { + params_ref m_params; + + public: + bv_bounds_simplifier(ast_manager& m, params_ref const& p) : bv_bounds_base(m), m_params(p) { + updt_params(p); + } + + void updt_params(params_ref const & p) override { + m_propagate_eq = p.get_bool("propagate_eq", false); + } + + static void get_param_descrs(param_descrs& r) { + r.insert("propagate-eq", CPK_BOOL, "propagate equalities from inequalities", "false"); + } + + ~bv_bounds_simplifier() override {} + + bool assert_expr(expr * t, bool sign) override { + return assert_expr_core(t, sign); + } + + bool simplify(expr* t, expr_ref& result) override { + return simplify_core(t, result); + } + + bool may_simplify(expr* t) override { + if (m_bv.is_numeral(t)) + return false; + + while (m.is_not(t, t)); + + for (auto & v : m_bound) + if (contains(t, v.m_key)) + return true; + + expr* t1; + interval b; + // skip common case: single bound constraint without any context for simplification + if (is_bound(t, t1, b)) + return b.is_full() || m_bound.contains(t1); + + return contains_bound(t); + } + + void pop(unsigned num_scopes) override { + pop_core(num_scopes); + } + + simplifier * translate(ast_manager & m) override { + return alloc(bv_bounds_simplifier, m, m_params); } unsigned scope_level() const override { return m_scopes.size(); } - }; + + class dom_bv_bounds_simplifier : public dom_simplifier, public bv_bounds_base { + params_ref m_params; + + public: + dom_bv_bounds_simplifier(ast_manager& m, params_ref const& p) : bv_bounds_base(m), m_params(p) { + updt_params(p); + } + + ~dom_bv_bounds_simplifier() override { + } + + void updt_params(params_ref const & p) override { + m_propagate_eq = p.get_bool("propagate_eq", false); + } + + void collect_param_descrs(param_descrs& r) override { + r.insert("propagate-eq", CPK_BOOL, "propagate equalities from inequalities", "false"); + } + + bool assert_expr(expr * t, bool sign) override { + return assert_expr_core(t, sign); + } + + void operator()(expr_ref& r) override { + expr_ref result(m); + simplify_core(r, result); + if (result) + r = result; + } + + void pop(unsigned num_scopes) override { + pop_core(num_scopes); + } + + dom_simplifier * translate(ast_manager & m) override { + return alloc(dom_bv_bounds_simplifier, m, m_params); + } + + unsigned scope_level() const override { + return m_scopes.size(); + } + }; + } tactic * mk_bv_bounds_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/tactic/bv/bv_bounds_tactic.h b/src/tactic/bv/bv_bounds_tactic.h index 325cca89e..8153ad52f 100644 --- a/src/tactic/bv/bv_bounds_tactic.h +++ b/src/tactic/bv/bv_bounds_tactic.h @@ -46,7 +46,7 @@ tactic * mk_dom_bv_bounds_tactic(ast_manager & m, params_ref const & p = params_ ADD_TACTIC("propagate-bv-bounds", "propagate bit-vector bounds by simplifying implied or contradictory bounds.", "mk_bv_bounds_tactic(m, p)") - ADD_TACTIC("propagate-bv-bounds-new", "propagate bit-vector bounds by simplifying implied or contradictory bounds.", "mk_dom_bv_bounds_tactic(m, p)") + ADD_TACTIC("propagate-bv-bounds2", "propagate bit-vector bounds by simplifying implied or contradictory bounds.", "mk_dom_bv_bounds_tactic(m, p)") */ diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 9bf70ab16..82fb7ec44 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -542,6 +542,10 @@ class expr_substitution_simplifier : public dom_simplifier { public: expr_substitution_simplifier(ast_manager& m): m(m), m_subst(m), m_scoped_substitution(m_subst), m_trail(m) {} + void updt_params(params_ref const & p) override {} + + void collect_param_descrs(param_descrs& r) override {} + bool assert_expr(expr * t, bool sign) override { expr* tt; if (m.is_not(t, tt)) diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index b4c83d04e..771c8c654 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -105,9 +105,13 @@ class dom_simplifier { virtual dom_simplifier * translate(ast_manager & m) = 0; virtual unsigned scope_level() const = 0; - + + virtual void updt_params(params_ref const & p) = 0; + + virtual void collect_param_descrs(param_descrs& r) = 0; }; + class dom_simplify_tactic : public tactic { ast_manager& m; dom_simplifier* m_simplifier; @@ -156,13 +160,13 @@ public: char const* name() const override { return "dom_simplify"; } tactic * translate(ast_manager & m) override; - void updt_params(params_ref const & p) override {} - static void get_param_descrs(param_descrs & r) {} - void collect_param_descrs(param_descrs & r) override { get_param_descrs(r); } + void updt_params(params_ref const & p) override { m_simplifier->updt_params(p); } + void collect_param_descrs(param_descrs & r) override { m_simplifier->collect_param_descrs(r); } void operator()(goal_ref const & in, goal_ref_buffer & result) override; void cleanup() override; }; + tactic * mk_dom_simplify_tactic(ast_manager & m, params_ref const & p = params_ref()); /*