diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 1964262f3..e248a0081 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -172,7 +172,8 @@ namespace lp { lia_move int_solver::check(lp::explanation * e) { SASSERT(lra.ax_is_correct()); - if (!has_inf_int()) return lia_move::sat; + if (!has_inf_int()) + return lia_move::sat; m_t.clear(); m_k.reset(); @@ -181,7 +182,8 @@ namespace lp { m_upper = false; lia_move r = lia_move::undef; - if (m_gcd.should_apply()) r = m_gcd(); + if (m_gcd.should_apply()) + r = m_gcd(); check_return_helper pc(lra); @@ -298,7 +300,6 @@ namespace lp { return m_number_of_calls % settings().m_int_find_cube_period == 0; } - bool int_solver::should_gomory_cut() { return m_number_of_calls % settings().m_int_gomory_cut_period == 0; } diff --git a/src/math/lp/lia_move.h b/src/math/lp/lia_move.h index ca61d7b7a..12e3d8e35 100644 --- a/src/math/lp/lia_move.h +++ b/src/math/lp/lia_move.h @@ -19,34 +19,38 @@ Revision History: --*/ #pragma once namespace lp { -enum class lia_move { - sat, - branch, - cut, - conflict, - continue_with_check, - undef, - unsat -}; -inline std::string lia_move_to_string(lia_move m) { - switch (m) { - case lia_move::sat: - return "sat"; - case lia_move::branch: - return "branch"; - case lia_move::cut: - return "cut"; - case lia_move::conflict: - return "conflict"; - case lia_move::continue_with_check: - return "continue_with_check"; - case lia_move::undef: - return "undef"; - case lia_move::unsat: - return "unsat"; - default: - UNREACHABLE(); + enum class lia_move { + sat, + branch, + cut, + conflict, + continue_with_check, + undef, + unsat }; - return "strange"; -} + inline std::string lia_move_to_string(lia_move m) { + switch (m) { + case lia_move::sat: + return "sat"; + case lia_move::branch: + return "branch"; + case lia_move::cut: + return "cut"; + case lia_move::conflict: + return "conflict"; + case lia_move::continue_with_check: + return "continue_with_check"; + case lia_move::undef: + return "undef"; + case lia_move::unsat: + return "unsat"; + default: + UNREACHABLE(); + }; + return "strange"; + } + + inline std::ostream& operator<<(std::ostream& out, lia_move const& m) { + return out << lia_move_to_string(m); + } } diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp index c79d3f8e4..b94dcbf57 100644 --- a/src/math/lp/monomial_bounds.cpp +++ b/src/math/lp/monomial_bounds.cpp @@ -58,38 +58,42 @@ namespace nla { auto const& upper = dep.upper(range); auto cmp = dep.upper_is_open(range) ? llc::LT : llc::LE; ++c().lra.settings().stats().m_nla_propagate_bounds; -#if UNIT_PROPAGATE_BOUNDS - auto* d = dep.get_upper_dep(range); - c().lra.update_column_type_and_bound(v, cmp, upper, d); -#else - lp::explanation ex; - dep.get_upper_dep(range, ex); - if (is_too_big(upper)) - return false; - new_lemma lemma(c(), "propagate value - upper bound of range is below value"); - lemma &= ex; - lemma |= ineq(v, cmp, upper); - TRACE("nla_solver", dep.display(tout << c().val(v) << " > ", range) << "\n" << lemma << "\n";); -#endif + if (c().params().arith_nl_internal_bounds()) { + auto* d = dep.get_upper_dep(range); + TRACE("arith", tout << "upper " << cmp << " " << upper << "\n"); + propagate_bound(v, cmp, upper, d); + } + else { + lp::explanation ex; + dep.get_upper_dep(range, ex); + if (is_too_big(upper)) + return false; + new_lemma lemma(c(), "propagate value - upper bound of range is below value"); + lemma &= ex; + lemma |= ineq(v, cmp, upper); + TRACE("nla_solver", dep.display(tout << c().val(v) << " > ", range) << "\n" << lemma << "\n";); + } return true; } else if (dep.is_above(range, val)) { auto const& lower = dep.lower(range); auto cmp = dep.lower_is_open(range) ? llc::GT : llc::GE; ++c().lra.settings().stats().m_nla_propagate_bounds; -#if UNIT_PROPAGATE_BOUNDS - auto* d = dep.get_lower_dep(range); - c().lra.update_column_type_and_bound(v, cmp, lower, d); -#else - lp::explanation ex; - dep.get_lower_dep(range, ex); - if (is_too_big(lower)) - return false; - new_lemma lemma(c(), "propagate value - lower bound of range is above value"); - lemma &= ex; - lemma |= ineq(v, cmp, lower); - TRACE("nla_solver", dep.display(tout << c().val(v) << " < ", range) << "\n" << lemma << "\n";); -#endif + if (c().params().arith_nl_internal_bounds()) { + auto* d = dep.get_lower_dep(range); + propagate_bound(v, cmp, lower, d); + TRACE("arith", tout << v << " " << cmp << " " << lower << "\n"); + } + else { + lp::explanation ex; + dep.get_lower_dep(range, ex); + if (is_too_big(lower)) + return false; + new_lemma lemma(c(), "propagate value - lower bound of range is above value"); + lemma &= ex; + lemma |= ineq(v, cmp, lower); + TRACE("nla_solver", dep.display(tout << c().val(v) << " < ", range) << "\n" << lemma << "\n";); + } return true; } else { @@ -97,6 +101,28 @@ namespace nla { } } + /** + * Ensure that bounds are integral when the variable is integer. + */ + void monomial_bounds::propagate_bound(lpvar v, lp::lconstraint_kind cmp, rational const& q, u_dependency* d) { + SASSERT(cmp != llc::EQ && cmp != llc::NE); + if (!c().var_is_int(v)) + c().lra.update_column_type_and_bound(v, cmp, q, d); + else if (q.is_int()) { + if (cmp == llc::GT) + c().lra.update_column_type_and_bound(v, llc::GE, q + 1, d); + else if(cmp == llc::LT) + c().lra.update_column_type_and_bound(v, llc::LE, q - 1, d); + else + c().lra.update_column_type_and_bound(v, cmp, q, d); + } + else if (cmp == llc::GE || cmp == llc::GT) + c().lra.update_column_type_and_bound(v, llc::GE, ceil(q), d); + else + c().lra.update_column_type_and_bound(v, llc::LE, floor(q), d); + } + + /** * val(v)^p should be in range. * if val(v)^p > upper(range) add @@ -129,28 +155,30 @@ namespace nla { if ((p % 2 == 1) || val_v.is_pos()) { ++c().lra.settings().stats().m_nla_propagate_bounds; auto le = dep.upper_is_open(range) ? llc::LT : llc::LE; -#if UNIT_PROPAGATE_BOUNDS - auto* d = dep.get_upper_dep(); - c().lra.update_column_type_and_bound(v, le, r, d); -#else - new_lemma lemma(c(), "propagate value - root case - upper bound of range is below value"); - lemma &= ex; - lemma |= ineq(v, le, r); -#endif + if (c().params().arith_nl_internal_bounds()) { + auto* d = dep.get_upper_dep(range); + propagate_bound(v, le, r, d); + } + else { + new_lemma lemma(c(), "propagate value - root case - upper bound of range is below value"); + lemma &= ex; + lemma |= ineq(v, le, r); + } return true; } if (p % 2 == 0 && val_v.is_neg()) { ++c().lra.settings().stats().m_nla_propagate_bounds; SASSERT(!r.is_neg()); auto ge = dep.upper_is_open(range) ? llc::GT : llc::GE; -#if UNIT_PROPAGATE_BOUNDS - auto* d = dep.get_upper_dep(); - c().lra.update_column_type_and_bound(v, ge, -r, d); -#else - new_lemma lemma(c(), "propagate value - root case - upper bound of range is below negative value"); - lemma &= ex; - lemma |= ineq(v, ge, -r); -#endif + if (c().params().arith_nl_internal_bounds()) { + auto* d = dep.get_upper_dep(range); + propagate_bound(v, ge, -r, d); + } + else { + new_lemma lemma(c(), "propagate value - root case - upper bound of range is below negative value"); + lemma &= ex; + lemma |= ineq(v, ge, -r); + } return true; } } @@ -306,10 +334,11 @@ namespace nla { if (m.is_propagated()) return; lpvar w, fixed_to_zero; - if (!is_linear(m, w, fixed_to_zero)) { -#if UNIT_PROPAGATE_BOUNDS - propagate(m); -#endif + + if (!is_linear(m)) { + if (c().params().arith_nl_internal_bounds()) { + propagate(m); + } return; } diff --git a/src/math/lp/monomial_bounds.h b/src/math/lp/monomial_bounds.h index 9e62e1520..554fb6109 100644 --- a/src/math/lp/monomial_bounds.h +++ b/src/math/lp/monomial_bounds.h @@ -17,6 +17,7 @@ namespace nla { class monomial_bounds : common { dep_intervals& dep; + void propagate_bound(lpvar v, lp::lconstraint_kind cmp, rational const& q, u_dependency* d); void var2interval(lpvar v, scoped_dep_interval& i); bool is_too_big(mpq const& q) const; bool propagate_down(monic const& m, lpvar u); diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 9fcda7f64..6d14e7cc6 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -83,6 +83,7 @@ def_module_params(module_name='smt', ('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'), ('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'), ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'), + ('arith.nl.internal_bounds', BOOL, False, 'use internal bounds propagation'), ('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'), ('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'), ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'), diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp index 9bc830dd1..d1a6c6f11 100644 --- a/src/smt/params/theory_arith_params.cpp +++ b/src/smt/params/theory_arith_params.cpp @@ -39,6 +39,7 @@ void theory_arith_params::updt_params(params_ref const & _p) { m_nl_arith_propagate_linear_monomials = p.arith_nl_propagate_linear_monomials(); m_nl_arith_optimize_bounds = p.arith_nl_optimize_bounds(); m_nl_arith_cross_nested = p.arith_nl_cross_nested(); + m_nl_arith_internal_bounds = p.arith_nl_internal_bounds(); arith_rewriter_params ap(_p); m_arith_eq2ineq = ap.eq2ineq(); @@ -95,4 +96,5 @@ void theory_arith_params::display(std::ostream & out) const { DISPLAY_PARAM(m_nl_arith_propagate_linear_monomials); DISPLAY_PARAM(m_nl_arith_optimize_bounds); DISPLAY_PARAM(m_nl_arith_cross_nested); + DISPLAY_PARAM(m_nl_arith_internal_bounds); } diff --git a/src/smt/params/theory_arith_params.h b/src/smt/params/theory_arith_params.h index f78086300..c84cca23b 100644 --- a/src/smt/params/theory_arith_params.h +++ b/src/smt/params/theory_arith_params.h @@ -108,6 +108,7 @@ struct theory_arith_params { bool m_nl_arith_propagate_linear_monomials = true; bool m_nl_arith_optimize_bounds = true; bool m_nl_arith_cross_nested = true; + bool m_nl_arith_internal_bounds = false; theory_arith_params(params_ref const & p = params_ref()) { diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index db4dba137..d38c44340 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2113,7 +2113,6 @@ public: bool propagate_core() { m_model_is_initialized = false; flush_bound_axioms(); - // disabled in master: propagate_nla(); if (ctx().inconsistent()) return true; @@ -3175,14 +3174,13 @@ public: ctx().display_detailed_literal(tout << ctx().get_assign_level(c.var()) << " " << c << " ", c) << "\n"; for (auto e : m_eqs) tout << pp(e.first, m) << " = " << pp(e.second, m) << "\n"; - tout << " ==> "; - tout << pp(x, m) << " = " << pp(y, m) << "\n"; + tout << " ==> " << pp(x, m) << " = " << pp(y, m) << "\n"; ); std::function fn = [&]() { return m.mk_eq(x->get_expr(), y->get_expr()); }; scoped_trace_stream _sts(th, fn); - //VERIFY(validate_eq(x, y)); + // VERIFY(validate_eq(x, y)); ctx().assign_eq(x, y, eq_justification(js)); } @@ -3291,11 +3289,11 @@ public: tout << "lemma scope: " << ctx().get_scope_level(); for (auto const& p : m_params) tout << " " << p; tout << "\n"; - display_evidence(tout, m_explanation); - display(tout << "is-conflict: " << is_conflict << "\n");); + display_evidence(tout, m_explanation);); for (auto ev : m_explanation) set_evidence(ev.ci(), m_core, m_eqs); + SASSERT(!m_core.empty() || !m_eqs.empty()); // SASSERT(validate_conflict(m_core, m_eqs)); if (is_conflict) { @@ -3517,7 +3515,7 @@ public: cancel_eh eh(m.limit()); scoped_timer timer(1000, &eh); bool result = l_true != nctx.check(); - CTRACE("arith", !result, ctx().display_lemma_as_smt_problem(tout, core.size(), core.data(), eqs.size(), eqs.data(), false_literal);); + CTRACE("arith", !result, ctx().display_lemma_as_smt_problem(tout, core.size(), core.data(), eqs.size(), eqs.data(), false_literal);); return result; }