From c309d522831b4b62812399b6571624899e1557cd Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 13 Sep 2023 08:12:00 -0700 Subject: [PATCH] runs a simple test --- src/math/lp/bound_analyzer_on_row.h | 31 ++++++- src/math/lp/implied_bound.h | 31 +++---- src/math/lp/lar_solver.h | 56 ++++++++---- src/math/lp/lp_bound_propagator.h | 132 ++++++++++++++++++++++++++-- src/math/lp/monomial_bounds.cpp | 74 +++++++--------- src/math/lp/monomial_bounds.h | 6 +- src/math/lp/nla_core.cpp | 8 +- src/math/lp/nla_core.h | 4 +- src/math/lp/nla_solver.h | 3 +- src/sat/smt/arith_solver.cpp | 2 +- src/smt/theory_lra.cpp | 56 ++++++++---- 11 files changed, 291 insertions(+), 112 deletions(-) diff --git a/src/math/lp/bound_analyzer_on_row.h b/src/math/lp/bound_analyzer_on_row.h index 0008a0ee9..35e3bb6ed 100644 --- a/src/math/lp/bound_analyzer_on_row.h +++ b/src/math/lp/bound_analyzer_on_row.h @@ -26,6 +26,8 @@ Revision History: #include "math/lp/test_bound_analyzer.h" namespace lp { + + template // C plays a role of a container, B - lp_bound_propagator class bound_analyzer_on_row { const C& m_row; @@ -301,8 +303,12 @@ private: // */ // } - void limit_j(unsigned j, const mpq& u, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict){ - m_bp.try_add_bound(u, j, is_lower_bound, coeff_before_j_is_pos, m_row_index, strict); + + void limit_j(unsigned bound_j, const mpq& u, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict){ + lar_solver* lar = & this->m_bp.lp(); + unsigned row_index = this->m_row_index; + auto explain = [lar, bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index]() { return explain_bound_on_var_on_coeff(lar, bound_j, coeff_before_j_is_pos, is_lower_bound, strict, row_index); }; + m_bp.add_bound(u, bound_j, is_lower_bound, strict, explain ); } void advance_u(unsigned j) { @@ -335,6 +341,27 @@ private: break; } } + static u_dependency* explain_bound_on_var_on_coeff(lar_solver* lar, unsigned bound_j, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict, unsigned row_index) { + int bound_sign = (is_lower_bound ? 1 : -1); + int j_sign = (coeff_before_j_is_pos ? 1 : -1) * bound_sign; + + if (tv::is_term(bound_j)) + bound_j = lar->map_term_index_to_column_index(bound_j); + u_dependency* ret = nullptr; + for (auto const& r : lar->get_row(row_index)) { + unsigned j = r.var(); + if (j == bound_j) + continue; + mpq const& a = r.coeff(); + int a_sign = is_pos(a) ? 1 : -1; + int sign = j_sign * a_sign; + u_dependency* witness = sign > 0 ? lar->get_column_upper_bound_witness(j) : lar->get_column_lower_bound_witness(j); + ret = lar->join_deps(ret, witness); + } + return ret; + } }; + + } diff --git a/src/math/lp/implied_bound.h b/src/math/lp/implied_bound.h index 9435edcdc..2e7fcbbcb 100644 --- a/src/math/lp/implied_bound.h +++ b/src/math/lp/implied_bound.h @@ -21,37 +21,34 @@ Revision History: #include "math/lp/lp_settings.h" #include "math/lp/lar_constraints.h" namespace lp { -struct implied_bound { +class implied_bound { + public: mpq m_bound; unsigned m_j; // the column for which the bound has been found bool m_is_lower_bound; - bool m_coeff_before_j_is_pos; - unsigned m_row_or_term_index; - bool m_strict; + bool m_strict; + private: + std::function m_explain_bound = nullptr; + public: + u_dependency* explain() const { return m_explain_bound(); } + void set_explain(std::function f) { m_explain_bound = f; } lconstraint_kind kind() const { lconstraint_kind k = m_is_lower_bound? GE : LE; if (m_strict) k = static_cast(k / 2); return k; } - bool operator==(const implied_bound & o) const { - return m_j == o.m_j && m_is_lower_bound == o.m_is_lower_bound && m_bound == o.m_bound && - m_coeff_before_j_is_pos == o.m_coeff_before_j_is_pos && - m_row_or_term_index == o.m_row_or_term_index && m_strict == o.m_strict; - } implied_bound(){} implied_bound(const mpq & a, unsigned j, - bool lower_bound, - bool coeff_before_j_is_pos, - unsigned row_or_term_index, - bool strict): + bool is_lower_bound, + bool is_strict, + std::function get_dep): m_bound(a), m_j(j), - m_is_lower_bound(lower_bound), - m_coeff_before_j_is_pos(coeff_before_j_is_pos), - m_row_or_term_index(row_or_term_index), - m_strict(strict) { + m_is_lower_bound(is_lower_bound), + m_strict(is_strict), + m_explain_bound(get_dep) { } }; } diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index acab137b5..7d16c7b63 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -311,26 +311,34 @@ class lar_solver : public column_namer { template void explain_implied_bound(const implied_bound& ib, lp_bound_propagator& bp) { - unsigned i = ib.m_row_or_term_index; - int bound_sign = (ib.m_is_lower_bound ? 1 : -1); - int j_sign = (ib.m_coeff_before_j_is_pos ? 1 : -1) * bound_sign; - unsigned bound_j = ib.m_j; - if (tv::is_term(bound_j)) - bound_j = m_var_register.external_to_local(bound_j); + u_dependency* dep = ib.explain(); + for (auto ci : flatten(dep)) + bp.consume(mpq(1), ci); // TODO: flatten should provid the coefficients + /* + if (ib.m_is_monic) { + NOT_IMPLEMENTED_YET(); + } else { + unsigned i = ib.m_row_or_term_index; + int bound_sign = (ib.m_is_lower_bound ? 1 : -1); + int j_sign = (ib.m_coeff_before_j_is_pos ? 1 : -1) * bound_sign; + unsigned bound_j = ib.m_j; + if (tv::is_term(bound_j)) + bound_j = m_var_register.external_to_local(bound_j); - for (auto const& r : get_row(i)) { - unsigned j = r.var(); - if (j == bound_j) - continue; - mpq const& a = r.coeff(); - int a_sign = is_pos(a) ? 1 : -1; - int sign = j_sign * a_sign; - const ul_pair& ul = m_columns_to_ul_pairs[j]; - auto* witness = sign > 0 ? ul.upper_bound_witness() : ul.lower_bound_witness(); - lp_assert(witness); - for (auto ci : flatten(witness)) - bp.consume(a, ci); - } + for (auto const& r : get_row(i)) { + unsigned j = r.var(); + if (j == bound_j) + continue; + mpq const& a = r.coeff(); + int a_sign = is_pos(a) ? 1 : -1; + int sign = j_sign * a_sign; + const ul_pair& ul = m_columns_to_ul_pairs[j]; + auto* witness = sign > 0 ? ul.upper_bound_witness() : ul.lower_bound_witness(); + lp_assert(witness); + for (auto ci : flatten(witness)) + bp.consume(a, ci); + } + }*/ } void set_value_for_nbasic_column(unsigned j, const impq& new_val); @@ -564,6 +572,16 @@ class lar_solver : public column_namer { const ul_pair& ul = m_columns_to_ul_pairs[j]; return m_dependencies.mk_join(ul.lower_bound_witness(), ul.upper_bound_witness()); } + template + u_dependency* get_bound_constraint_witnesses_for_columns(const T& collection) { + u_dependency* dep = nullptr; + for (auto j : collection) { + u_dependency* d = get_bound_constraint_witnesses_for_column(j); + dep = m_dependencies.mk_join(dep, d); + } + return dep; + } + u_dependency* join_deps(u_dependency* a, u_dependency *b) { return m_dependencies.mk_join(a, b); } inline constraint_set const& constraints() const { return m_constraints; } void push(); void pop(); diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index f676b0e1d..7ee647200 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -40,6 +40,7 @@ class lp_bound_propagator { return x != UINT_MAX; } + void try_add_equation_with_internal_fixed_tables(unsigned r1) { unsigned v1, v2; if (!only_one_nfixed(r1, v1)) @@ -94,6 +95,115 @@ class lp_bound_propagator { m_ibounds.reset(); m_column_types = &lp().get_column_types(); } + + bool is_linear(const svector& m, lpvar& zero_var, lpvar& non_fixed) { + zero_var = non_fixed = null_lpvar; + unsigned n_of_non_fixed = 0; + bool big_bound = false; + for (lpvar v : m) { + if (!this->column_is_fixed(v)) { + n_of_non_fixed++; + non_fixed = v; + continue; + } + const auto & b = get_lower_bound(v).x; + if (b.is_zero()) { + zero_var = v; + return true; + } + if (b.is_big()) { + big_bound |= true; + } + } + return n_of_non_fixed <= 1 && !big_bound; + } + + void add_bounds_for_zero_var(lpvar monic_var, lpvar zero_var) { + add_lower_bound_monic(monic_var, mpq(0), false, [&](){return lp().get_bound_constraint_witnesses_for_column(zero_var);}); + add_upper_bound_monic(monic_var, mpq(0), false, [&](){return lp().get_bound_constraint_witnesses_for_column(zero_var);}); + } + + void add_lower_bound_monic(lpvar monic_var, const mpq& v, bool is_strict, std::function explain_dep) { + unsigned k; + if (!try_get_value(m_improved_lower_bounds, monic_var, k)) { + m_improved_lower_bounds[monic_var] = m_ibounds.size(); + m_ibounds.push_back(implied_bound(v, monic_var, true, is_strict, explain_dep)); + } else { + auto& found_bound = m_ibounds[k]; + if (v > found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && is_strict)) { + found_bound = implied_bound(v, monic_var, true, is_strict, explain_dep); + TRACE("add_bound", m_imp.lp().print_implied_bound(found_bound, tout);); + } + } + } + + void add_upper_bound_monic(lpvar monic_var, const mpq& bound_val, bool is_strict, std::function explain_bound) { + unsigned k; + if (!try_get_value(m_improved_upper_bounds, monic_var, k)) { + m_improved_upper_bounds[monic_var] = m_ibounds.size(); + m_ibounds.push_back(implied_bound(bound_val, monic_var, false, is_strict, explain_bound)); + } else { + auto& found_bound = m_ibounds[k]; + if (bound_val > found_bound.m_bound || (bound_val == found_bound.m_bound && !found_bound.m_strict && is_strict)) { + found_bound = implied_bound(bound_val, monic_var, false, is_strict, explain_bound); + TRACE("add_bound", m_imp.lp().print_implied_bound(found_bound, tout);); + } + } + } + + void propagate_monic(lpvar monic_var, const svector& vars) { + lpvar non_fixed, zero_var; + if (!is_linear(vars, zero_var, non_fixed)) { + return; + } + + if (zero_var != null_lpvar) { + add_bounds_for_zero_var(monic_var, zero_var); + } else { + if (non_fixed != null_lpvar && get_column_type(non_fixed) == column_type::free_column) return; + rational k = rational(1); + for (auto v : vars) + if (v != non_fixed) { + k *= lp().get_column_value(v).x; + if (k.is_big()) return; + } + u_dependency* dep; + lp::mpq bound_value; + bool is_strict; + if (non_fixed != null_lpvar) { + if (this->lp().has_lower_bound(non_fixed, dep, bound_value, is_strict)) { + if (k.is_pos()) + add_lower_bound_monic(monic_var, k * bound_value, is_strict, [&]() { return dep; }); + else + add_upper_bound_monic(monic_var, k * bound_value, is_strict, [&]() {return dep;}); + } + if (this->lp().has_upper_bound(non_fixed, dep, bound_value, is_strict)) { + if (k.is_neg()) + add_lower_bound_monic(monic_var, k * bound_value, is_strict, [&]() {return dep;}); + else + add_upper_bound_monic(monic_var, k * bound_value, is_strict, [&]() {return dep;}); + } + + if (this->lp().has_lower_bound(monic_var, dep, bound_value, is_strict)) { + if (k.is_pos()) + add_lower_bound_monic(non_fixed, bound_value / k, is_strict, [&]() {return dep;}); + else + add_upper_bound_monic(non_fixed, bound_value / k, is_strict, [&]() {return dep;}); + } + + if (this->lp().has_upper_bound(monic_var, dep, bound_value, is_strict)) { + if (k.is_neg()) + add_lower_bound_monic(non_fixed, bound_value / k, is_strict, [&]() {return dep;}); + else + add_upper_bound_monic(non_fixed, bound_value / k, is_strict, [&]() {return dep;}); + } + + } else { // all variables are fixed + add_lower_bound_monic(monic_var, k, false, [&](){return lp().get_bound_constraint_witnesses_for_columns(vars);}); + add_upper_bound_monic(monic_var, k, false, [&](){return lp().get_bound_constraint_witnesses_for_columns(vars);}); + } + } + } const lar_solver& lp() const { return m_imp.lp(); } lar_solver& lp() { return m_imp.lp(); } @@ -123,7 +233,7 @@ class lp_bound_propagator { return (*m_column_types)[j] == column_type::fixed && get_lower_bound(j).y.is_zero(); } - void try_add_bound(mpq const& v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) { + void add_bound(mpq const& v, unsigned j, bool is_low, bool strict, std::function explain_bound) { j = m_imp.lp().column_to_reported_index(j); lconstraint_kind kind = is_low ? GE : LE; @@ -137,25 +247,29 @@ class lp_bound_propagator { if (try_get_value(m_improved_lower_bounds, j, k)) { auto& found_bound = m_ibounds[k]; if (v > found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && strict)) { - found_bound = implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict); - TRACE("try_add_bound", m_imp.lp().print_implied_bound(found_bound, tout);); + found_bound.m_bound = v; + found_bound.m_strict = strict; + found_bound.set_explain(explain_bound); + TRACE("add_bound", m_imp.lp().print_implied_bound(found_bound, tout);); } } else { m_improved_lower_bounds[j] = m_ibounds.size(); - m_ibounds.push_back(implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict)); - TRACE("try_add_bound", m_imp.lp().print_implied_bound(m_ibounds.back(), tout);); + m_ibounds.push_back(implied_bound(v, j, is_low, strict, explain_bound)); + TRACE("add_bound", m_imp.lp().print_implied_bound(m_ibounds.back(), tout);); } } else { // the upper bound case if (try_get_value(m_improved_upper_bounds, j, k)) { auto& found_bound = m_ibounds[k]; if (v < found_bound.m_bound || (v == found_bound.m_bound && !found_bound.m_strict && strict)) { - found_bound = implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict); - TRACE("try_add_bound", m_imp.lp().print_implied_bound(found_bound, tout);); + found_bound.m_bound = v; + found_bound.m_strict = strict; + found_bound.set_explain(explain_bound); + TRACE("add_bound", m_imp.lp().print_implied_bound(found_bound, tout);); } } else { m_improved_upper_bounds[j] = m_ibounds.size(); - m_ibounds.push_back(implied_bound(v, j, is_low, coeff_before_j_is_pos, row_or_term_index, strict)); - TRACE("try_add_bound", m_imp.lp().print_implied_bound(m_ibounds.back(), tout);); + m_ibounds.push_back(implied_bound(v, j, is_low, strict, explain_bound)); + TRACE("add_bound", m_imp.lp().print_implied_bound(m_ibounds.back(), tout);); } } } diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp index 77e01c2db..ad2b20c07 100644 --- a/src/math/lp/monomial_bounds.cpp +++ b/src/math/lp/monomial_bounds.cpp @@ -261,6 +261,7 @@ namespace nla { void monomial_bounds::unit_propagate() { for (lpvar v : c().m_monics_with_changed_bounds) unit_propagate(c().emons()[v]); + c().m_monics_with_changed_bounds.clear(); } void monomial_bounds::unit_propagate(monic const& m) { @@ -268,68 +269,61 @@ namespace nla { if (m_propagated[m.var()]) return; - if (!is_linear(m)) + lpvar non_fixed = null_lpvar, zero_var = null_lpvar; + if (!is_linear(m, zero_var, non_fixed)) return; c().trail().push(set_bitvector_trail(m_propagated, m.var())); - rational k = fixed_var_product(m); - new_lemma lemma(c(), "fixed-values"); - if (k == 0) { - for (auto v : m) { - if (c().var_is_fixed(v) && c().val(v).is_zero()) { - lemma.explain_fixed(v); - break; - } - } + if (zero_var != null_lpvar) { + new_lemma lemma(c(), "fixed-values"); + lemma.explain_fixed(zero_var); lemma += ineq(m.var(), lp::lconstraint_kind::EQ, 0); } else { + rational k = rational(1); for (auto v : m) - if (c().var_is_fixed(v)) + if (v != non_fixed) { + k *= c().lra.get_column_value(v).x; + if (k.is_big()) return; + } + + new_lemma lemma(c(), "fixed-values"); + + for (auto v : m) + if (v != non_fixed) lemma.explain_fixed(v); - lpvar w = non_fixed_var(m); - if (w != null_lpvar) { + if (non_fixed != null_lpvar) { lp::lar_term term; term.add_var(m.var()); - term.add_monomial(-k, w); + term.add_monomial(-k, non_fixed); lemma += ineq(term, lp::lconstraint_kind::EQ, 0); } else { lemma += ineq(m.var(), lp::lconstraint_kind::EQ, k); } } - } - - bool monomial_bounds::is_linear(monic const& m) { - unsigned non_fixed = 0; + // returns true iff (all variables are fixed, + // or all but one variable are fixed) and the bounds are not big, + // or at least one variable is fixed to zero. + bool monomial_bounds::is_linear(monic const& m, lpvar& zero_var, lpvar& non_fixed) { + zero_var = non_fixed = null_lpvar; + unsigned n_of_non_fixed = 0; + bool big_bound = false; for (lpvar v : m) { - if (!c().var_is_fixed(v)) - ++non_fixed; - else if (c().val(v).is_zero()) + if (!c().var_is_fixed(v)) { + n_of_non_fixed++; + non_fixed = v; + } else if (c().var_is_fixed_to_zero(v)) { + zero_var = v; return true; + } else if (c().fixed_var_has_big_bound(v)) { + big_bound |= true; + } } - return non_fixed <= 1; + return n_of_non_fixed <= 1 && !big_bound; } - - - rational monomial_bounds::fixed_var_product(monic const& m) { - rational r(1); - for (lpvar v : m) { - if (c().var_is_fixed(v)) - r *= c().lra.get_column_value(v).x; - } - return r; - } - - lpvar monomial_bounds::non_fixed_var(monic const& m) { - for (lpvar v : m) - if (!c().var_is_fixed(v)) - return v; - return null_lpvar; - } - } diff --git a/src/math/lp/monomial_bounds.h b/src/math/lp/monomial_bounds.h index c728d1a4c..15ab6b992 100644 --- a/src/math/lp/monomial_bounds.h +++ b/src/math/lp/monomial_bounds.h @@ -33,10 +33,8 @@ namespace nla { // monomial propagation bool_vector m_propagated; void unit_propagate(monic const& m); - bool is_linear(monic const& m); - rational fixed_var_product(monic const& m); - lpvar non_fixed_var(monic const& m); - + bool is_linear(monic const& m, lpvar& zero_var, lpvar& non_fixed); + public: monomial_bounds(core* core); void propagate(); diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index cc2f0f1b5..20003f947 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -40,7 +40,6 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit& lim) : m_evars(), m_nra(s, m_nra_lim, *this) { m_nlsat_delay = lp_settings().nlsat_delay(); lra.m_find_monics_with_changed_bounds_func = [&](const indexed_uint_set& columns_with_changed_bounds) { - m_monics_with_changed_bounds.clear(); for (const auto& m : m_emons) { if (columns_with_changed_bounds.contains(m.var())) { m_monics_with_changed_bounds.push_back(m.var()); @@ -553,6 +552,13 @@ bool core::var_is_fixed_to_zero(lpvar j) const { lra.column_is_fixed(j) && lra.get_lower_bound(j) == lp::zero_of_type(); } + +bool core::fixed_var_has_big_bound(lpvar j) const { + SASSERT(lra.column_is_fixed(j)); + const auto& b = lra.get_lower_bound(j); + return b.x.is_big() || b.y.is_big(); +} + bool core::var_is_fixed_to_val(lpvar j, const rational& v) const { return lra.column_is_fixed(j) && diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 8dee571ae..3b888f8ef 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -120,7 +120,8 @@ class core { public: // constructor core(lp::lar_solver& s, params_ref const& p, reslimit&); - + const auto& monics_with_changed_bounds() const { return m_monics_with_changed_bounds; } + void reset_monics_with_changed_bounds() { m_monics_with_changed_bounds.reset(); } void insert_to_refine(lpvar j); void erase_from_to_refine(lpvar j); @@ -310,6 +311,7 @@ public: bool sign_contradiction(const monic& m) const; bool var_is_fixed_to_zero(lpvar j) const; + bool fixed_var_has_big_bound(lpvar j) const; bool var_is_fixed_to_val(lpvar j, const rational& v) const; bool var_is_fixed(lpvar j) const; diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index 7a8a97b3f..07bf095a6 100644 --- a/src/math/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -26,7 +26,8 @@ namespace nla { solver(lp::lar_solver& s, params_ref const& p, reslimit& limit); ~solver(); - + const auto& monics_with_changed_bounds() const { return m_core->monics_with_changed_bounds(); } + void reset_monics_with_changed_bounds() { m_core->reset_monics_with_changed_bounds(); } void add_monic(lpvar v, unsigned sz, lpvar const* vs); void add_idivision(lpvar q, lpvar x, lpvar y); void add_rdivision(lpvar q, lpvar x, lpvar y); diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index c06b8fafb..e4bec83cc 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -253,7 +253,7 @@ namespace arith { first = false; reset_evidence(); m_explanation.clear(); - lp().explain_implied_bound(be, m_bp); + be.explain(); } CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";); updt_unassigned_bounds(v, -1); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 29a46db19..1a022e087 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2150,7 +2150,7 @@ public: case l_true: propagate_basic_bounds(); propagate_bounds_with_lp_solver(); - propagate_nla(); + propagate_bounds_with_nlp(); break; case l_undef: UNREACHABLE(); @@ -2185,33 +2185,55 @@ public: set_evidence(j, m_core, m_eqs); m_explanation.add_pair(j, v); } - - void propagate_bounds_with_lp_solver() { - if (!should_propagate()) - return; - - m_bp.init(); - lp().propagate_bounds_for_touched_rows(m_bp); - - if (!m.inc()) - return; + void finish_bound_propagation() { if (is_infeasible()) { get_infeasibility_explanation_and_set_conflict(); // verbose_stream() << "unsat\n"; - } - else { - unsigned count = 0, prop = 0; - for (auto& ib : m_bp.ibounds()) { + } else { + for (auto &ib : m_bp.ibounds()) { m.inc(); if (ctx().inconsistent()) break; - ++prop; - count += propagate_lp_solver_bound(ib); + propagate_lp_solver_bound(ib); } } } + void propagate_bounds_with_lp_solver() { + if (!should_propagate()) + return; + m_bp.init(); + lp().propagate_bounds_for_touched_rows(m_bp); + + if (m.inc()) + finish_bound_propagation(); + } + + void calculate_implied_bounds_for_monic(lpvar monic_var, const svector& vars) { + m_bp.propagate_monic(monic_var, vars); + } + + void propagate_bounds_for_touched_monomials() { + for (unsigned v : m_nla->monics_with_changed_bounds()) { + calculate_implied_bounds_for_monic(v, m_nla->get_core().emons()[v].vars()); + } + m_nla->reset_monics_with_changed_bounds(); + } + + void propagate_bounds_with_nlp() { + if (!m_nla) + return; + if (is_infeasible() || !should_propagate()) + return; + + m_bp.init(); + propagate_bounds_for_touched_monomials(); + + if (m.inc()) + finish_bound_propagation(); + } + bool bound_is_interesting(unsigned vi, lp::lconstraint_kind kind, const rational & bval) const { theory_var v = lp().local_to_external(vi); if (v == null_theory_var)