diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 08ff3b0d4..4db3a9531 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -200,16 +200,10 @@ namespace lp { } lp_status lar_solver::solve() { - if (m_status == lp_status::INFEASIBLE) { + if (m_status == lp_status::INFEASIBLE) return m_status; - } + solve_with_core_solver(); - if (m_status != lp_status::INFEASIBLE) { - if (m_settings.bound_propagation()) - detect_rows_with_changed_bounds(); - } - - clear_columns_with_changed_bounds(); return m_status; } @@ -789,8 +783,7 @@ namespace lp { void lar_solver::detect_rows_with_changed_bounds() { for (auto j : m_columns_with_changed_bounds) detect_rows_with_changed_bounds_for_column(j); - if (m_find_monics_with_changed_bounds_func) - m_find_monics_with_changed_bounds_func(m_columns_with_changed_bounds); + } void lar_solver::update_x_and_inf_costs_for_columns_with_changed_bounds_tableau() { @@ -1623,10 +1616,9 @@ namespace lp { SASSERT(m_terms.size() == m_term_register.size()); unsigned adjusted_term_index = m_terms.size() - 1; var_index ret = tv::mask_term(adjusted_term_index); - if (!coeffs.empty()) { + if (!coeffs.empty()) add_row_from_term_no_constraint(m_terms.back(), ret); - add_touched_row(A_r().row_count() - 1); - } + lp_assert(m_var_register.size() == A_r().column_count()); if (m_need_register_terms) register_normalized_term(*t, A_r().column_count() - 1); diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 9f878e363..2a1f8644c 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -89,6 +89,11 @@ class lar_solver : public column_namer { constraint_set m_constraints; // the set of column indices j such that bounds have changed for j indexed_uint_set m_columns_with_changed_bounds; +public: + const indexed_uint_set& columns_with_changed_bounds() const { return m_columns_with_changed_bounds; } + inline void clear_columns_with_changed_bounds() { m_columns_with_changed_bounds.reset(); } +private: + // m_touched_rows contains rows that have been changed by a pivoting or have a column with changed bounds indexed_uint_set m_touched_rows; unsigned_vector m_row_bounds_to_replay; u_dependency_manager m_dependencies; @@ -138,9 +143,7 @@ class lar_solver : public column_namer { void add_row_from_term_no_constraint(const lar_term* term, unsigned term_ext_index); void add_basic_var_to_core_fields(); bool compare_values(impq const& lhs, lconstraint_kind k, const mpq& rhs); - - inline void clear_columns_with_changed_bounds() { m_columns_with_changed_bounds.reset(); } - public: +public: void insert_to_columns_with_changed_bounds(unsigned j); const u_dependency* crossed_bounds_deps() const { return m_crossed_bounds_deps;} u_dependency*& crossed_bounds_deps() { return m_crossed_bounds_deps;} @@ -149,12 +152,12 @@ class lar_solver : public column_namer { lpvar& crossed_bounds_column() { return m_crossed_bounds_column; } - private: +private: void update_column_type_and_bound_check_on_equal(unsigned j, const mpq& right_side, constraint_index ci, unsigned&); void update_column_type_and_bound(unsigned j, const mpq& right_side, constraint_index ci); - public: +public: void update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); - private: +private: void update_column_type_and_bound_with_ub(var_index j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); void update_column_type_and_bound_with_no_ub(var_index j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); void update_bound_with_ub_lb(var_index j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); @@ -358,6 +361,8 @@ class lar_solver : public column_namer { void add_column_rows_to_touched_rows(lpvar j); template void propagate_bounds_for_touched_rows(lp_bound_propagator& bp) { + detect_rows_with_changed_bounds(); + clear_columns_with_changed_bounds(); if (settings().propagate_eqs()) { if (settings().random_next() % 10 == 0) remove_fixed_vars_from_base(); @@ -688,7 +693,6 @@ class lar_solver : public column_namer { return 0; return m_usage_in_terms[j]; } - std::function m_find_monics_with_changed_bounds_func = nullptr; friend int_solver; friend int_branch; }; diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index f574f20ad..6641347e4 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -41,19 +41,7 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit& lim, std_vector & m_implied_bounds; // try to improve bounds for variables in monomials. bool improve_bounds(); - + void clear_monics_with_changed_bounds() { m_monics_with_changed_bounds.reset(); } public: // constructor core(lp::lar_solver& s, params_ref const& p, reslimit&, std_vector & implied_bounds); diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index 144ecefd3..53d8b0da6 100644 --- a/src/math/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -110,7 +110,12 @@ namespace nla { void solver::propagate_bounds_for_touched_monomials() { init_bound_propagation(); - for (unsigned v : monics_with_changed_bounds()) - calculate_implied_bounds_for_monic(v); + for (unsigned v : m_core->monics_with_changed_bounds()) { + calculate_implied_bounds_for_monic(v); + if (m_core->lra.get_status() == lp::lp_status::INFEASIBLE) { + break; + } + } + m_core->clear_monics_with_changed_bounds(); } } diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index 0fe9733f1..acd724af9 100644 --- a/src/math/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -26,7 +26,6 @@ namespace nla { solver(lp::lar_solver& s, params_ref const& p, reslimit& limit, std_vector & implied_bounds); ~solver(); - const auto& monics_with_changed_bounds() const { return m_core->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);