diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 868e9b690..76f163b85 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -14,8 +14,8 @@ Version 4.next Version 4.12.2 ============== - remove MSF (Microsoft Solver Foundation) plugin -- add bound_simplifier tactic. - It eliminates occurrences of "mod" operators when bounds information +- updated propagate-ineqs tactic and implementing it as a simplifier, bound_simplifier. + It now eliminates occurrences of "mod" operators when bounds information implies that the modulus is redundant. This tactic is useful for benchmarks created by converting bit-vector semantics to integer reasoning. diff --git a/src/ast/simplifiers/bound_simplifier.cpp b/src/ast/simplifiers/bound_simplifier.cpp index cf39c78de..89ed6da05 100644 --- a/src/ast/simplifiers/bound_simplifier.cpp +++ b/src/ast/simplifiers/bound_simplifier.cpp @@ -3,12 +3,35 @@ Copyright (c) 2022 Microsoft Corporation Module Name: - bounds_simplifier.cpp + bound_simplifier.cpp Author: Nikolaj Bjorner (nbjorner) 2023-01-22 +Description: + +Extract bounds for sub-expressions and use the bounds for propagation and simplification. +It applies the simplificaitons from the bounds_propagator and it applies nested rewriting +of sub-expressions based on bounds information. Initially, rewriting amounts to eliminating +occurrences of mod N. + +From the description of propagate_ineqs_tactic: + + - Propagate bounds using the bound_propagator. + - Eliminate subsumed inequalities. + For example: + x - y >= 3 + can be replaced with true if we know that + x >= 3 and y <= 0 + + - Convert inequalities of the form p <= k and p >= k into p = k, + where p is a polynomial and k is a constant. + + This strategy assumes the input is in arith LHS mode. + This can be achieved by using option :arith-lhs true in the + simplifier. + --*/ @@ -17,74 +40,86 @@ Author: #include "ast/rewriter/rewriter_def.h" struct bound_simplifier::rw_cfg : public default_rewriter_cfg { - ast_manager& m; - bound_propagator& bp; bound_simplifier& s; - arith_util a; - rw_cfg(bound_simplifier& s):m(s.m), bp(s.bp), s(s), a(m) {} - + rw_cfg(bound_simplifier& s): s(s) {} br_status reduce_app(func_decl* f, unsigned num_args, expr * const* args, expr_ref& result, proof_ref& pr) { - rational N, hi, lo; - bool strict; - if (a.is_mod(f) && num_args == 2 && a.is_numeral(args[1], N)) { - expr* x = args[0]; - if (!s.has_upper(x, hi, strict) || strict) - return BR_FAILED; - if (!s.has_lower(x, lo, strict) || strict) - return BR_FAILED; - if (hi - lo >= N) - return BR_FAILED; - if (N > hi && lo >= 0) { - result = x; - return BR_DONE; - } - if (2*N > hi && lo >= N) { - result = a.mk_sub(x, a.mk_int(N)); - s.m_rewriter(result); - return BR_DONE; - } - IF_VERBOSE(2, verbose_stream() << "potentially missed simplification: " << mk_pp(x, m) << " " << lo << " " << hi << " not reduced\n"); - } - return BR_FAILED; + return s.reduce_app(f, num_args, args, result, pr); } }; struct bound_simplifier::rw : public rewriter_tpl { rw_cfg m_cfg; - rw(bound_simplifier& s): rewriter_tpl(s.m, false, m_cfg), m_cfg(s) { } }; +br_status bound_simplifier::reduce_app(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result, proof_ref& pr) { + rational N, hi, lo; + if (a.is_mod(f) && num_args == 2 && a.is_numeral(args[1], N)) { + expr* x = args[0]; + auto& im = m_interval; + scoped_dep_interval i(im); + get_bounds(x, i); + if (im.upper_is_inf(i) || im.lower_is_inf(i)) + return BR_FAILED; + if (im.upper_is_open(i) || im.lower_is_open(i)) + return BR_FAILED; + lo = im.lower(i); + hi = im.upper(i); + if (hi - lo >= N) + return BR_FAILED; + if (N > hi && lo >= 0) { + result = x; + return BR_DONE; + } + if (2 * N > hi && lo >= N) { + result = a.mk_sub(x, a.mk_int(N)); + m_rewriter(result); + return BR_DONE; + } + IF_VERBOSE(2, verbose_stream() << "potentially missed simplification: " << mk_pp(x, m) << " " << lo << " " << hi << " not reduced\n"); + } + return BR_FAILED; +} + void bound_simplifier::reduce() { - m_updated = true; - for (unsigned i = 0; i < 5 && m_updated; ++i) { - m_updated = false; + bool updated = true, found_bound = false; + for (unsigned i = 0; i < 5 && updated; ++i) { + updated = false; + found_bound = false; reset(); - for (unsigned idx : indices()) - insert_bound(m_fmls[idx]); + for (unsigned idx : indices()) { + if (insert_bound(m_fmls[idx])) { + m_fmls.update(idx, dependent_expr(m, m.mk_true(), nullptr, nullptr)); + found_bound = true; + } + } + if (!found_bound) + break; + for (unsigned idx : indices()) tighten_bound(m_fmls[idx]); - rw rw(*this); - - // TODO: take over propagate_ineq: - // bp.propagate(); - // serialize bounds + bp.propagate(); proof_ref pr(m); expr_ref r(m); + rw rw(*this); for (unsigned idx : indices()) { auto const& d = m_fmls[idx]; + if (d.pr()) + continue; rw(d.fml(), r, pr); if (r != d.fml()) { m_fmls.update(idx, dependent_expr(m, r, mp(d.pr(), pr), d.dep())); - m_updated = true; + ++m_num_reduced; + updated = true; } } + restore_bounds(); } } @@ -169,19 +204,22 @@ void bound_simplifier::tighten_bound(dependent_expr const& de) { bool strict; if (a.is_le(f, x, y)) { // x <= (x + k) mod N && x >= 0 -> x + k < N - if (a.is_mod(y, z, u) && a.is_numeral(u, n) && has_lower(x, k, strict) && k >= 0 && is_offset(z, x, k) && k > 0 && k < n) { + if (a.is_mod(y, z, u) && a.is_numeral(u, n) && has_lower(x, k, strict) && k >= 0 && is_offset(z, x, k) && k > 0 && k < n) assert_upper(x, n - k, true); - } + } + // x != k, k <= x -> k < x if (m.is_not(f, f) && m.is_eq(f, x, y)) { if (a.is_numeral(x)) std::swap(x, y); - bool strict; if (a.is_numeral(y, n)) { - if (has_lower(x, k, strict) && !strict && k == n) - assert_lower(x, k, true); - else if (has_upper(x, k, strict) && !strict && k == n) - assert_upper(x, k, true); + scoped_dep_interval i(m_interval); + get_bounds(x, i); + scoped_mpq k(nm); + if (!i.m().lower_is_inf(i) && !i.m().lower_is_open(i) && i.m().lower(i) == n) + assert_lower(x, n, true); + else if (!i.m().upper_is_inf(i) && !i.m().upper_is_open(i) && i.m().upper(i) == n) + assert_upper(x, n, true); } } } @@ -199,111 +237,33 @@ void bound_simplifier::assert_lower(expr* x, rational const& n, bool strict) { bp.assert_lower(to_var(x), c, strict); } -// -// TODO: Use math/interval/interval.h -// - bool bound_simplifier::has_lower(expr* x, rational& n, bool& strict) { - if (is_var(x)) { - unsigned v = to_var(x); - if (bp.has_lower(v)) { - mpq const & q = bp.lower(v, strict); - n = rational(q); - return true; - } - } - if (a.is_numeral(x, n)) { - strict = false; - return true; - } - if (a.is_mod(x)) { - n = rational::zero(); - strict = false; - return true; - } - expr* y, *z; - if (a.is_idiv(x, y, z) && has_lower(z, n, strict) && n > 0 && has_lower(y, n, strict)) - return true; - - if (a.is_add(x)) { - rational bound; - strict = false; - n = 0; - bool is_strict; - for (expr* arg : *to_app(x)) { - if (!has_lower(arg, bound, is_strict)) - return false; - strict |= is_strict; - n += bound; - } - return true; - } - - if (a.is_mul(x, y, z)) { - // TODO: this is done generally using math/interval/interval.h - rational bound1, bound2; - bool strict1, strict2; - if (has_lower(y, bound1, strict1) && !strict1 && - has_lower(z, bound1, strict2) && !strict2 && - bound1 >= 0 && bound2 >= 0) { - n = bound1*bound2; - strict = false; - return true; - } - } - - return false; + scoped_dep_interval i(m_interval); + get_bounds(x, i); + if (m_interval.lower_is_inf(i)) + return false; + strict = m_interval.lower_is_open(i); + n = m_interval.lower(i); + return true; } - bool bound_simplifier::has_upper(expr* x, rational& n, bool& strict) { - if (is_var(x)) { - unsigned v = to_var(x); - if (bp.has_upper(v)) { - mpq const & q = bp.upper(v, strict); - n = rational(q); - return true; - } - } - - // perform light-weight abstract analysis - // y * (u / y) is bounded by u, if y > 0 - - if (a.is_numeral(x, n)) { - strict = false; - return true; - } - - if (a.is_add(x)) { - rational bound; - strict = false; - n = 0; - bool is_strict; - for (expr* arg : *to_app(x)) { - if (!has_upper(arg, bound, is_strict)) - return false; - strict |= is_strict; - n += bound; - } - return true; - } - - expr* y, *z, *u, *v; - if (a.is_mul(x, y, z) && a.is_idiv(z, u, v) && v == y && has_lower(y, n, strict) && n > 0 && has_upper(u, n, strict)) - return true; - if (a.is_idiv(x, y, z) && has_lower(z, n, strict) && n > 0 && has_upper(y, n, strict)) - return true; - - return false; + scoped_dep_interval i(m_interval); + get_bounds(x, i); + if (m_interval.upper_is_inf(i)) + return false; + strict = m_interval.upper_is_open(i); + n = m_interval.upper(i); + return true; } -void bound_simplifier::get_bounds(expr* x, scoped_interval& i) { - i.m().reset_upper(i); - i.m().reset_lower(i); - +void bound_simplifier::get_bounds(expr* x, scoped_dep_interval& i) { + auto& im = m_interval; + im.reset(i); + scoped_dep_interval arg_i(im); rational n; if (a.is_numeral(x, n)) { - i.m().set(i, n.to_mpq()); + im.set_value(i, n); return; } @@ -311,51 +271,311 @@ void bound_simplifier::get_bounds(expr* x, scoped_interval& i) { unsigned v = to_var(x); bool strict; if (bp.has_upper(v)) { - mpq const& q = bp.upper(v, strict); - i_cfg.set_upper_is_open(i, strict); - i_cfg.set_upper(i, q); + im.set_upper(i, bp.upper(v, strict)); + im.set_upper_is_inf(i, false); + im.set_upper_is_open(i, strict); + } if (bp.has_lower(v)) { - mpq const& q = bp.lower(v, strict); - i_cfg.set_lower_is_open(i, strict); - i_cfg.set_lower(i, q); + im.set_lower(i, bp.lower(v, strict)); + im.set_lower_is_inf(i, false); + im.set_lower_is_open(i, strict); } } if (a.is_add(x)) { - scoped_interval sum_i(i.m()); - scoped_interval arg_i(i.m()); - i.m().set(sum_i, mpq(0)); + scoped_dep_interval tmp_i(im), sum_i(im); + im.set_value(sum_i, rational::zero()); for (expr* arg : *to_app(x)) { get_bounds(arg, arg_i); - i.m().add(sum_i, arg_i, sum_i); + im.add(sum_i, arg_i, tmp_i); + im.set(sum_i, tmp_i); } - // TODO: intersect - i.m().set(i, sum_i); + im.intersect (i, sum_i, i); } if (a.is_mul(x)) { - scoped_interval mul_i(i.m()); - scoped_interval arg_i(i.m()); - i.m().set(mul_i, mpq(1)); + scoped_dep_interval tmp_i(im); + im.set_value(tmp_i, rational::one()); for (expr* arg : *to_app(x)) { get_bounds(arg, arg_i); - i.m().add(mul_i, arg_i, mul_i); + im.mul(tmp_i, arg_i, tmp_i); } - // TODO: intersect - i.m().set(i, mul_i); + im.intersect (i, tmp_i, i); } - // etc: - // import interval from special case code for lower and upper. + expr* y, * z, * u, * v; + if (a.is_mod(x, y, z) && a.is_numeral(z, n) && n > 0) { + scoped_dep_interval tmp_i(im); + im.set_lower_is_inf(tmp_i, false); + im.set_lower_is_open(tmp_i, false); + im.set_lower(tmp_i, mpq(0)); + im.set_upper_is_inf(tmp_i, false); + im.set_upper_is_open(tmp_i, false); + im.set_upper(tmp_i, n - 1); + im.intersect (i, tmp_i, i); + } - - + // x = y*(u div y), y > 0 -> x <= u + if (a.is_mul(x, y, z) && a.is_idiv(z, u, v) && v == y) { + scoped_dep_interval iy(im), iu(im), tmp_i(im); + get_bounds(y, iy); + get_bounds(u, iu); + if (!im.lower_is_inf(iy) && im.lower(iy) > 0 && + !im.upper_is_inf(iu) && im.upper(iu) >= 0) { + im.set_upper_is_inf(tmp_i, false); + im.set_upper_is_open(tmp_i, im.upper_is_open(iu)); + im.set_upper(tmp_i, im.upper(iu)); + im.intersect(i, tmp_i, i); + } + } + + // x = y div z, z > 0 => x <= y + if (a.is_idiv(x, y, z)) { + scoped_dep_interval iy(im), iz(im), tmp_i(im); + get_bounds(y, iy); + get_bounds(z, iz); + if (!im.lower_is_inf(iz) && im.lower(iz) > 0 && + !im.upper_is_inf(iy) && im.upper(iy) >= 0) { + im.set_upper_is_inf(tmp_i, false); + im.set_upper_is_open(tmp_i, im.upper_is_open(iy)); + im.set_upper(tmp_i, im.upper(iy)); + im.set_lower_is_inf(tmp_i, false); + im.set_lower_is_open(tmp_i, false); // TODO - could be refined + im.set_lower(tmp_i, rational::zero()); + im.intersect(i, tmp_i, i); + } + } + if (a.is_div(x, y, z)) { + scoped_dep_interval iy(im), iz(im), tmp_i(im); + get_bounds(y, iy); + get_bounds(z, iz); + im.div(iy, iz, tmp_i); + im.intersect(i, tmp_i, i); + } } +void bound_simplifier::expr2linear_pol(expr* t, mpq_buffer& as, var_buffer& xs) { + scoped_mpq c_mpq_val(nm); + if (a.is_add(t)) { + rational c_val; + for (expr* mon : *to_app(t)) { + expr* c, * x; + if (a.is_mul(mon, c, x) && a.is_numeral(c, c_val)) { + nm.set(c_mpq_val, c_val.to_mpq()); + as.push_back(c_mpq_val); + xs.push_back(to_var(x)); + } + else { + as.push_back(mpq(1)); + xs.push_back(to_var(mon)); + } + } + } + else { + as.push_back(mpq(1)); + xs.push_back(to_var(t)); + } +} + +bool bound_simplifier::lower_subsumed(expr* p, mpq const& k, bool strict) { + if (!a.is_add(p)) + return false; + m_num_buffer.reset(); + m_var_buffer.reset(); + expr2linear_pol(p, m_num_buffer, m_var_buffer); + scoped_mpq implied_k(nm); + bool implied_strict; + return + bp.lower(m_var_buffer.size(), m_num_buffer.data(), m_var_buffer.data(), implied_k, implied_strict) && + (nm.gt(implied_k, k) || (nm.eq(implied_k, k) && (!strict || implied_strict))); +} + +bool bound_simplifier::upper_subsumed(expr* p, mpq const& k, bool strict) { + if (!a.is_add(p)) + return false; + m_num_buffer.reset(); + m_var_buffer.reset(); + expr2linear_pol(p, m_num_buffer, m_var_buffer); + scoped_mpq implied_k(nm); + bool implied_strict; + return + bp.upper(m_var_buffer.size(), m_num_buffer.data(), m_var_buffer.data(), implied_k, implied_strict) && + (nm.lt(implied_k, k) || (nm.eq(implied_k, k) && (!strict || implied_strict))); +} + +void bound_simplifier::restore_bounds() { + scoped_mpq l(nm), u(nm); + bool strict_l, strict_u, has_l, has_u; + unsigned ts; + unsigned sz = m_var2expr.size(); + + rw rw(*this); + auto add = [&](expr* fml) { + expr_ref tmp(fml, m); + rw(tmp, tmp); + m_rewriter(tmp); + m_fmls.add(dependent_expr(m, tmp, nullptr, nullptr)); + }; + + for (unsigned x = 0; x < sz; x++) { + expr* p = m_var2expr.get(x); + has_l = bp.lower(x, l, strict_l, ts); + has_u = bp.upper(x, u, strict_u, ts); + if (!has_l && !has_u) + continue; + if (has_l && has_u && nm.eq(l, u) && !strict_l && !strict_u) { + // l <= p <= l --> p = l + add(m.mk_eq(p, a.mk_numeral(rational(l), a.is_int(p)))); + continue; + } + if (has_l && !lower_subsumed(p, l, strict_l)) { + if (strict_l) + add(m.mk_not(a.mk_le(p, a.mk_numeral(rational(l), a.is_int(p))))); + else + add(a.mk_ge(p, a.mk_numeral(rational(l), a.is_int(p)))); + } + if (has_u && !upper_subsumed(p, u, strict_u)) { + if (strict_u) + add(m.mk_not(a.mk_ge(p, a.mk_numeral(rational(u), a.is_int(p))))); + else + add(a.mk_le(p, a.mk_numeral(rational(u), a.is_int(p)))); + } + } +} + + void bound_simplifier::reset() { bp.reset(); m_var2expr.reset(); m_expr2var.reset(); - m_num_vars = 0; } + +#if 0 +void find_ite_bounds(expr* root) { + TRACE("find_ite_bounds_bug", display_bounds(tout);); + expr* n = root; + expr* target = nullptr; + expr* c, * t, * e; + expr* x, * y; + bool has_l, has_u; + mpq l_min, u_max; + bool l_strict, u_strict; + mpq curr; + bool curr_strict; + while (true) { + TRACE("find_ite_bounds_bug", tout << mk_ismt2_pp(n, m) << "\n";); + + if (m.is_ite(n, c, t, e)) { + if (is_x_minus_y_eq_0(t, x, y)) + n = e; + else if (is_x_minus_y_eq_0(e, x, y)) + n = t; + else + break; + } + else if (is_x_minus_y_eq_0(n, x, y)) { + n = nullptr; + } + else { + break; + } + + TRACE("find_ite_bounds_bug", tout << "x: " << mk_ismt2_pp(x, m) << ", y: " << mk_ismt2_pp(y, m) << "\n"; + if (target) { + tout << "target: " << mk_ismt2_pp(target, m) << "\n"; + tout << "has_l: " << has_l << " " << nm.to_string(l_min) << " has_u: " << has_u << " " << nm.to_string(u_max) << "\n"; + }); + + if (is_unbounded(y)) + std::swap(x, y); + + if (!is_unbounded(x)) { + TRACE("find_ite_bounds_bug", tout << "x is already bounded\n";); + break; + } + + if (target == nullptr) { + target = x; + if (lower(y, curr, curr_strict)) { + has_l = true; + nm.set(l_min, curr); + l_strict = curr_strict; + } + else { + has_l = false; + TRACE("find_ite_bounds_bug", tout << "y does not have lower\n";); + } + if (upper(y, curr, curr_strict)) { + has_u = true; + nm.set(u_max, curr); + u_strict = curr_strict; + } + else { + has_u = false; + TRACE("find_ite_bounds_bug", tout << "y does not have upper\n";); + } + } + else if (target == x) { + if (has_l) { + if (lower(y, curr, curr_strict)) { + if (nm.lt(curr, l_min) || (!curr_strict && l_strict && nm.eq(curr, l_min))) { + nm.set(l_min, curr); + l_strict = curr_strict; + } + } + else { + has_l = false; + TRACE("find_ite_bounds_bug", tout << "y does not have lower\n";); + } + } + if (has_u) { + if (upper(y, curr, curr_strict)) { + if (nm.gt(curr, u_max) || (curr_strict && !u_strict && nm.eq(curr, u_max))) { + nm.set(u_max, curr); + u_strict = curr_strict; + } + } + else { + has_u = false; + TRACE("find_ite_bounds_bug", tout << "y does not have upper\n";); + } + } + } + else { + break; + } + + if (!has_l && !has_u) + break; + + if (n == nullptr) { + TRACE("find_ite_bounds", tout << "found bounds for: " << mk_ismt2_pp(target, m) << "\n"; + tout << "has_l: " << has_l << " " << nm.to_string(l_min) << " l_strict: " << l_strict << "\n"; + tout << "has_u: " << has_u << " " << nm.to_string(u_max) << " u_strict: " << u_strict << "\n"; + tout << "root:\n" << mk_ismt2_pp(root, m) << "\n";); + a_var x = mk_var(target); + if (has_l) + bp.assert_lower(x, l_min, l_strict); + if (has_u) + bp.assert_upper(x, u_max, u_strict); + break; + } + } + nm.del(l_min); + nm.del(u_max); + nm.del(curr); +} + +void find_ite_bounds() { + unsigned sz = m_new_goal->size(); + for (unsigned i = 0; i < sz; i++) { + expr* f = m_new_goal->form(i); + if (m.is_ite(f)) + find_ite_bounds(to_app(f)); + } + bp.propagate(); + TRACE("find_ite_bounds", display_bounds(tout);); +} + +#endif diff --git a/src/ast/simplifiers/bound_simplifier.h b/src/ast/simplifiers/bound_simplifier.h index 06e25920c..9d6b09955 100644 --- a/src/ast/simplifiers/bound_simplifier.h +++ b/src/ast/simplifiers/bound_simplifier.h @@ -23,25 +23,26 @@ Description: #include "ast/rewriter/th_rewriter.h" #include "ast/simplifiers/dependent_expr_state.h" #include "ast/simplifiers/bound_propagator.h" -#include "math/interval/interval.h" +#include "math/interval/dep_intervals.h" class bound_simplifier : public dependent_expr_simplifier { - typedef interval_manager _interval_manager; - typedef _interval_manager::interval interval; - typedef _scoped_interval<_interval_manager> scoped_interval; + typedef bound_propagator::var a_var; + typedef numeral_buffer mpq_buffer; + typedef svector var_buffer; arith_util a; + params_ref m_params; th_rewriter m_rewriter; unsynch_mpq_manager nm; small_object_allocator m_alloc; bound_propagator bp; - im_default_config i_cfg; - _interval_manager i_manager; - unsigned m_num_vars = 0; + dep_intervals m_interval; ptr_vector m_var2expr; unsigned_vector m_expr2var; - bool m_updated = false; + mpq_buffer m_num_buffer; + var_buffer m_var_buffer; + unsigned m_num_reduced = 0; struct rw_cfg; struct rw; @@ -62,20 +63,27 @@ class bound_simplifier : public dependent_expr_simplifier { unsigned to_var(expr* e) { unsigned v = m_expr2var.get(e->get_id(), UINT_MAX); if (v == UINT_MAX) { - v = m_num_vars++; + v = m_var2expr.size(); bp.mk_var(v, a.is_int(e)); m_expr2var.setx(e->get_id(), v, UINT_MAX); - m_var2expr.setx(v, e, nullptr); + m_var2expr.push_back(e); } return v; } + br_status reduce_app(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result, proof_ref& pr); + void assert_lower(expr* x, rational const& n, bool strict); void assert_upper(expr* x, rational const& n, bool strict); bool has_upper(expr* x, rational& n, bool& strict); bool has_lower(expr* x, rational& n, bool& strict); - void get_bounds(expr* x, scoped_interval&); + void get_bounds(expr* x, scoped_dep_interval&); + + void expr2linear_pol(expr* t, mpq_buffer& as, var_buffer& xs); + bool lower_subsumed(expr* p, mpq const& k, bool strict); + bool upper_subsumed(expr* p, mpq const& k, bool strict); + void restore_bounds(); // e = x + offset bool is_offset(expr* e, expr* x, rational& offset); @@ -87,14 +95,35 @@ public: a(m), m_rewriter(m), bp(nm, m_alloc, p), - i_cfg(nm), - i_manager(m.limit(), im_default_config(nm)) { + m_interval(m.limit()), + m_num_buffer(nm) { + updt_params(p); } - char const* name() const override { return "bounds-simplifier"; } + char const* name() const override { return "propagate-ineqs"; } bool supports_proofs() const override { return false; } void reduce() override; + + void updt_params(params_ref const& p) override { + m_params.append(p); + bp.updt_params(m_params); + } + + void collect_param_descrs(param_descrs & r) override { + bound_propagator::get_param_descrs(r); + } + + void collect_statistics(statistics& st) const override { + st.update("bound-propagations", bp.get_num_propagations()); + st.update("bound-false-alarms", bp.get_num_false_alarms()); + st.update("bound-simplifications", m_num_reduced); + } + + void reset_statistics() override { + m_num_reduced = 0; + bp.reset_statistics(); + } }; diff --git a/src/math/interval/dep_intervals.h b/src/math/interval/dep_intervals.h index d14a0fc53..d641a294d 100644 --- a/src/math/interval/dep_intervals.h +++ b/src/math/interval/dep_intervals.h @@ -172,6 +172,7 @@ public: void set_upper_is_inf(interval& a, bool inf) const { m_config.set_upper_is_inf(a, inf); } void set_lower_dep(interval& a, u_dependency* d) const { m_config.set_lower_dep(a, d); } void set_upper_dep(interval& a, u_dependency* d) const { m_config.set_upper_dep(a, d); } + void reset(interval& a) const { set_lower_is_inf(a, true); set_upper_is_inf(a, true); } void set_value(interval& a, rational const& n) const { set_lower(a, n); set_upper(a, n); @@ -331,6 +332,7 @@ public: } mpq const& lower(interval const& a) const { return m_config.lower(a); } mpq const& upper(interval const& a) const { return m_config.upper(a); } + bool is_empty(interval const& a) const; void set_interval_for_scalar(interval&, const rational&); template diff --git a/src/tactic/arith/CMakeLists.txt b/src/tactic/arith/CMakeLists.txt index c2539c2d3..4eabef4a6 100644 --- a/src/tactic/arith/CMakeLists.txt +++ b/src/tactic/arith/CMakeLists.txt @@ -17,7 +17,6 @@ z3_add_component(arith_tactics pb2bv_model_converter.cpp pb2bv_tactic.cpp probe_arith.cpp - propagate_ineqs_tactic.cpp purify_arith_tactic.cpp recover_01_tactic.cpp COMPONENT_DEPENDENCIES @@ -25,7 +24,6 @@ z3_add_component(arith_tactics sat TACTIC_HEADERS add_bounds_tactic.h - bound_simplifier_tactic.h card2bv_tactic.h degree_shift_tactic.h diff_neq_tactic.h diff --git a/src/tactic/arith/propagate_ineqs_tactic.cpp b/src/tactic/arith/propagate_ineqs_tactic.cpp deleted file mode 100644 index 56d07a5c2..000000000 --- a/src/tactic/arith/propagate_ineqs_tactic.cpp +++ /dev/null @@ -1,575 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - propagate_ineqs_tactic.h - -Abstract: - - This tactic performs the following tasks: - - - Propagate bounds using the bound_propagator. - - Eliminate subsumed inequalities. - For example: - x - y >= 3 - can be replaced with true if we know that - x >= 3 and y <= 0 - - - Convert inequalities of the form p <= k and p >= k into p = k, - where p is a polynomial and k is a constant. - - This strategy assumes the input is in arith LHS mode. - This can be achieved by using option :arith-lhs true in the - simplifier. - -Author: - - Leonardo (leonardo) 2012-02-19 - -Notes: - ---*/ -#include "tactic/tactical.h" -#include "ast/simplifiers/bound_propagator.h" -#include "ast/arith_decl_plugin.h" -#include "tactic/core/simplify_tactic.h" -#include "ast/ast_smt2_pp.h" - -class propagate_ineqs_tactic : public tactic { - struct imp; - imp * m_imp; - params_ref m_params; -public: - propagate_ineqs_tactic(ast_manager & m, params_ref const & p); - - tactic * translate(ast_manager & m) override { - return alloc(propagate_ineqs_tactic, m, m_params); - } - - ~propagate_ineqs_tactic() override; - - char const* name() const override { return "propagate_ineqs"; } - - void updt_params(params_ref const & p) override; - void collect_param_descrs(param_descrs & r) override {} - - void operator()(goal_ref const & g, goal_ref_buffer & result) override; - - void cleanup() override; -}; - -tactic * mk_propagate_ineqs_tactic(ast_manager & m, params_ref const & p) { - return clean(alloc(propagate_ineqs_tactic, m, p)); -} - -struct propagate_ineqs_tactic::imp { - ast_manager & m; - unsynch_mpq_manager nm; - small_object_allocator m_allocator; - bound_propagator bp; - arith_util m_util; - typedef bound_propagator::var a_var; - obj_map m_expr2var; - expr_ref_vector m_var2expr; - - typedef numeral_buffer mpq_buffer; - typedef svector var_buffer; - - mpq_buffer m_num_buffer; - var_buffer m_var_buffer; - goal_ref m_new_goal; - - imp(ast_manager & _m, params_ref const & p): - m(_m), - m_allocator("ineq-simplifier"), - bp(nm, m_allocator, p), - m_util(m), - m_var2expr(m), - m_num_buffer(nm) { - updt_params_core(p); - } - - void updt_params_core(params_ref const & p) { - } - - void updt_params(params_ref const & p) { - updt_params_core(p); - bp.updt_params(p); - } - - void display_bounds(std::ostream & out) { - unsigned sz = m_var2expr.size(); - mpq k; - bool strict; - unsigned ts; - for (unsigned x = 0; x < sz; x++) { - if (bp.lower(x, k, strict, ts)) - out << nm.to_string(k) << " " << (strict ? "<" : "<="); - else - out << "-oo <"; - out << " " << mk_ismt2_pp(m_var2expr.get(x), m) << " "; - if (bp.upper(x, k, strict, ts)) - out << (strict ? "<" : "<=") << " " << nm.to_string(k); - else - out << "< oo"; - out << "\n"; - } - nm.del(k); - } - - a_var mk_var(expr * t) { - if (m_util.is_to_real(t)) - t = to_app(t)->get_arg(0); - a_var x; - if (m_expr2var.find(t, x)) - return x; - x = m_var2expr.size(); - bp.mk_var(x, m_util.is_int(t)); - m_var2expr.push_back(t); - m_expr2var.insert(t, x); - return x; - } - - void expr2linear_pol(expr * t, mpq_buffer & as, var_buffer & xs) { - mpq c_mpq_val; - if (m_util.is_add(t)) { - rational c_val; - for (expr* mon : *to_app(t)) { - expr * c, * x; - if (m_util.is_mul(mon, c, x) && m_util.is_numeral(c, c_val)) { - nm.set(c_mpq_val, c_val.to_mpq()); - as.push_back(c_mpq_val); - xs.push_back(mk_var(x)); - } - else { - as.push_back(mpq(1)); - xs.push_back(mk_var(mon)); - } - } - } - else { - as.push_back(mpq(1)); - xs.push_back(mk_var(t)); - } - nm.del(c_mpq_val); - } - - a_var mk_linear_pol(expr * t) { - a_var x; - if (m_expr2var.find(t, x)) - return x; - x = mk_var(t); - if (m_util.is_add(t)) { - m_num_buffer.reset(); - m_var_buffer.reset(); - expr2linear_pol(t, m_num_buffer, m_var_buffer); - m_num_buffer.push_back(mpq(-1)); - m_var_buffer.push_back(x); - bp.mk_eq(m_num_buffer.size(), m_num_buffer.data(), m_var_buffer.data()); - } - return x; - } - - enum kind { EQ, LE, GE }; - - bool process(expr * t) { - bool sign = false; - while (m.is_not(t, t)) - sign = !sign; - bool strict = false; - kind k; - if (m.is_eq(t)) { - if (sign) - return false; - k = EQ; - } - else if (m_util.is_le(t)) { - if (sign) { - k = GE; - strict = true; - } - else { - k = LE; - } - } - else if (m_util.is_ge(t)) { - if (sign) { - k = LE; - strict = true; - } - else { - k = GE; - } - } - else if (m_util.is_lt(t)) { - if (sign) { - k = GE; - strict = false; - } else { - k = LE; - strict = true; - } - } - else if (m_util.is_gt(t)) { - //x > y == x <=y, strict = false - if (sign) { - k = LE; - strict = false; - } else { - k = GE; - strict = true; - } - } - else - return false; - - expr * lhs = to_app(t)->get_arg(0); - expr * rhs = to_app(t)->get_arg(1); - expr* a, *b; - if (m_util.is_numeral(lhs)) { - std::swap(lhs, rhs); - if (k == LE) - k = GE; - else if (k == GE) - k = LE; - } - - rational c; - // x = y mod c => 0 <= x < c - if (k == EQ && m_util.is_mod(rhs, a, b) && m_util.is_numeral(b, c) && c > 0) { - a_var x = mk_linear_pol(lhs); - mpq c_prime; - nm.set(c_prime, (c-1).to_mpq()); - bp.assert_lower(x, mpq(0), false); - bp.assert_upper(x, c_prime, false); - nm.del(c_prime); - return lhs == a; - } - if (!m_util.is_numeral(rhs, c)) - return false; - a_var x = mk_linear_pol(lhs); - mpq c_prime; - nm.set(c_prime, c.to_mpq()); - if (k == EQ) { - SASSERT(!strict); - bp.assert_lower(x, c_prime, false); - bp.assert_upper(x, c_prime, false); - } - else if (k == LE) { - bp.assert_upper(x, c_prime, strict); - } - else { - SASSERT(k == GE); - bp.assert_lower(x, c_prime, strict); - } - nm.del(c_prime); - return true; - } - - bool collect_bounds(goal const & g) { - bool found = false; - unsigned sz = g.size(); - for (unsigned i = 0; i < sz; i++) { - expr * t = g.form(i); - if (process(t)) - found = true; - else - m_new_goal->assert_expr(t); // save non-bounds here - } - return found; - } - - bool lower_subsumed(expr * p, mpq const & k, bool strict) { - if (!m_util.is_add(p)) - return false; - m_num_buffer.reset(); - m_var_buffer.reset(); - expr2linear_pol(p, m_num_buffer, m_var_buffer); - mpq implied_k; - bool implied_strict; - bool result = - bp.lower(m_var_buffer.size(), m_num_buffer.data(), m_var_buffer.data(), implied_k, implied_strict) && - (nm.gt(implied_k, k) || (nm.eq(implied_k, k) && (!strict || implied_strict))); - nm.del(implied_k); - return result; - } - - bool upper_subsumed(expr * p, mpq const & k, bool strict) { - if (!m_util.is_add(p)) - return false; - m_num_buffer.reset(); - m_var_buffer.reset(); - expr2linear_pol(p, m_num_buffer, m_var_buffer); - mpq implied_k; - bool implied_strict; - bool result = - bp.upper(m_var_buffer.size(), m_num_buffer.data(), m_var_buffer.data(), implied_k, implied_strict) && - (nm.lt(implied_k, k) || (nm.eq(implied_k, k) && (!strict || implied_strict))); - nm.del(implied_k); - return result; - } - - void restore_bounds() { - mpq l, u; - bool strict_l, strict_u, has_l, has_u; - unsigned ts; - unsigned sz = m_var2expr.size(); - for (unsigned x = 0; x < sz; x++) { - expr * p = m_var2expr.get(x); - has_l = bp.lower(x, l, strict_l, ts); - has_u = bp.upper(x, u, strict_u, ts); - if (!has_l && !has_u) - continue; - if (has_l && has_u && nm.eq(l, u) && !strict_l && !strict_u) { - // l <= p <= l --> p = l - m_new_goal->assert_expr(m.mk_eq(p, m_util.mk_numeral(rational(l), m_util.is_int(p)))); - continue; - } - if (has_l && !lower_subsumed(p, l, strict_l)) { - if (strict_l) - m_new_goal->assert_expr(m.mk_not(m_util.mk_le(p, m_util.mk_numeral(rational(l), m_util.is_int(p))))); - else - m_new_goal->assert_expr(m_util.mk_ge(p, m_util.mk_numeral(rational(l), m_util.is_int(p)))); - } - if (has_u && !upper_subsumed(p, u, strict_u)) { - if (strict_u) - m_new_goal->assert_expr(m.mk_not(m_util.mk_ge(p, m_util.mk_numeral(rational(u), m_util.is_int(p))))); - else - m_new_goal->assert_expr(m_util.mk_le(p, m_util.mk_numeral(rational(u), m_util.is_int(p)))); - } - } - nm.del(l); - nm.del(u); - } - - bool is_x_minus_y_eq_0(expr * t, expr * & x, expr * & y) { - expr * lhs, * rhs, * m1, * m2; - if (m.is_eq(t, lhs, rhs) && m_util.is_zero(rhs) && m_util.is_add(lhs, m1, m2)) { - if (m_util.is_times_minus_one(m2, y) && is_uninterp_const(m1)) { - x = m1; - return true; - } - if (m_util.is_times_minus_one(m1, y) && is_uninterp_const(m2)) { - x = m2; - return true; - } - } - return false; - } - - bool is_unbounded(expr * t) { - a_var x; - if (m_expr2var.find(t, x)) - return !bp.has_lower(x) && !bp.has_upper(x); - return true; - } - - bool lower(expr * t, mpq & k, bool & strict) { - unsigned ts; - a_var x; - if (m_expr2var.find(t, x)) - return bp.lower(x, k, strict, ts); - return false; - } - - bool upper(expr * t, mpq & k, bool & strict) { - unsigned ts; - a_var x; - if (m_expr2var.find(t, x)) - return bp.upper(x, k, strict, ts); - return false; - } - - void find_ite_bounds(expr * root) { - TRACE("find_ite_bounds_bug", display_bounds(tout);); - expr * n = root; - expr * target = nullptr; - expr * c, * t, * e; - expr * x, * y; - bool has_l, has_u; - mpq l_min, u_max; - bool l_strict, u_strict; - mpq curr; - bool curr_strict; - while (true) { - TRACE("find_ite_bounds_bug", tout << mk_ismt2_pp(n, m) << "\n";); - - if (m.is_ite(n, c, t, e)) { - if (is_x_minus_y_eq_0(t, x, y)) - n = e; - else if (is_x_minus_y_eq_0(e, x, y)) - n = t; - else - break; - } - else if (is_x_minus_y_eq_0(n, x, y)) { - n = nullptr; - } - else { - break; - } - - TRACE("find_ite_bounds_bug", tout << "x: " << mk_ismt2_pp(x, m) << ", y: " << mk_ismt2_pp(y, m) << "\n"; - if (target) { - tout << "target: " << mk_ismt2_pp(target, m) << "\n"; - tout << "has_l: " << has_l << " " << nm.to_string(l_min) << " has_u: " << has_u << " " << nm.to_string(u_max) << "\n"; - }); - - if (is_unbounded(y)) - std::swap(x, y); - - if (!is_unbounded(x)) { - TRACE("find_ite_bounds_bug", tout << "x is already bounded\n";); - break; - } - - if (target == nullptr) { - target = x; - if (lower(y, curr, curr_strict)) { - has_l = true; - nm.set(l_min, curr); - l_strict = curr_strict; - } - else { - has_l = false; - TRACE("find_ite_bounds_bug", tout << "y does not have lower\n";); - } - if (upper(y, curr, curr_strict)) { - has_u = true; - nm.set(u_max, curr); - u_strict = curr_strict; - } - else { - has_u = false; - TRACE("find_ite_bounds_bug", tout << "y does not have upper\n";); - } - } - else if (target == x) { - if (has_l) { - if (lower(y, curr, curr_strict)) { - if (nm.lt(curr, l_min) || (!curr_strict && l_strict && nm.eq(curr, l_min))) { - nm.set(l_min, curr); - l_strict = curr_strict; - } - } - else { - has_l = false; - TRACE("find_ite_bounds_bug", tout << "y does not have lower\n";); - } - } - if (has_u) { - if (upper(y, curr, curr_strict)) { - if (nm.gt(curr, u_max) || (curr_strict && !u_strict && nm.eq(curr, u_max))) { - nm.set(u_max, curr); - u_strict = curr_strict; - } - } - else { - has_u = false; - TRACE("find_ite_bounds_bug", tout << "y does not have upper\n";); - } - } - } - else { - break; - } - - if (!has_l && !has_u) - break; - - if (n == nullptr) { - TRACE("find_ite_bounds", tout << "found bounds for: " << mk_ismt2_pp(target, m) << "\n"; - tout << "has_l: " << has_l << " " << nm.to_string(l_min) << " l_strict: " << l_strict << "\n"; - tout << "has_u: " << has_u << " " << nm.to_string(u_max) << " u_strict: " << u_strict << "\n"; - tout << "root:\n" << mk_ismt2_pp(root, m) << "\n";); - a_var x = mk_var(target); - if (has_l) - bp.assert_lower(x, l_min, l_strict); - if (has_u) - bp.assert_upper(x, u_max, u_strict); - break; - } - } - nm.del(l_min); - nm.del(u_max); - nm.del(curr); - } - - void find_ite_bounds() { - unsigned sz = m_new_goal->size(); - for (unsigned i = 0; i < sz; i++) { - expr * f = m_new_goal->form(i); - if (m.is_ite(f)) - find_ite_bounds(to_app(f)); - } - bp.propagate(); - TRACE("find_ite_bounds", display_bounds(tout);); - } - - void operator()(goal * g, goal_ref & r) { - tactic_report report("propagate-ineqs", *g); - - m_new_goal = alloc(goal, *g, true); - m_new_goal->inc_depth(); - r = m_new_goal.get(); - if (!collect_bounds(*g)) { - m_new_goal = nullptr; - r = g; - return; // nothing to be done - } - - TRACE("propagate_ineqs_tactic", g->display(tout); display_bounds(tout); tout << "bound propagator:\n"; bp.display(tout);); - - bp.propagate(); - - report_tactic_progress(":bound-propagations", bp.get_num_propagations()); - report_tactic_progress(":bound-false-alarms", bp.get_num_false_alarms()); - - if (bp.inconsistent()) { - r->reset(); - r->assert_expr(m.mk_false()); - return; - } - - // find_ite_bounds(); // did not help - - restore_bounds(); - - TRACE("propagate_ineqs_tactic", tout << "after propagation:\n"; display_bounds(tout); bp.display(tout);); - TRACE("propagate_ineqs_tactic", r->display(tout);); - } - -}; - -propagate_ineqs_tactic::propagate_ineqs_tactic(ast_manager & m, params_ref const & p): - m_params(p) { - m_imp = alloc(imp, m, p); -} - -propagate_ineqs_tactic::~propagate_ineqs_tactic() { - dealloc(m_imp); -} - -void propagate_ineqs_tactic::updt_params(params_ref const & p) { - m_params.append(p); - m_imp->updt_params(m_params); -} - -void propagate_ineqs_tactic::operator()(goal_ref const & g, - goal_ref_buffer & result) { - fail_if_proof_generation("propagate-ineqs", g); - fail_if_unsat_core_generation("propagate-ineqs", g); - result.reset(); - goal_ref r; - (*m_imp)(g.get(), r); - result.push_back(r.get()); - SASSERT(r->is_well_formed()); -} - - -void propagate_ineqs_tactic::cleanup() { - imp * d = alloc(imp, m_imp->m, m_params); - std::swap(d, m_imp); - dealloc(d); -} diff --git a/src/tactic/arith/propagate_ineqs_tactic.h b/src/tactic/arith/propagate_ineqs_tactic.h index 6341bf281..1dbb0844b 100644 --- a/src/tactic/arith/propagate_ineqs_tactic.h +++ b/src/tactic/arith/propagate_ineqs_tactic.h @@ -51,11 +51,17 @@ This can be achieved by using option :arith-lhs true in the simplifier. --*/ #pragma once -#include "util/params.h" -class ast_manager; -class tactic; -tactic * mk_propagate_ineqs_tactic(ast_manager & m, params_ref const & p = params_ref()); +#include "util/params.h" +#include "tactic/tactic.h" +#include "tactic/dependent_expr_state_tactic.h" +#include "ast/simplifiers/bound_simplifier.h" + +inline tactic* mk_propagate_ineqs_tactic(ast_manager& m, params_ref const& p = params_ref()) { + return alloc(dependent_expr_state_tactic, m, p, + [](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(bound_simplifier, m, p, s); }); +} + /* ADD_TACTIC("propagate-ineqs", "propagate ineqs/bounds, remove subsumed inequalities.", "mk_propagate_ineqs_tactic(m, p)") */