From 401ec04ec301d4b61aa5990cebd2beb31be33874 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Fri, 14 Jul 2023 20:19:13 -0700 Subject: [PATCH] code cleaning around m_touched_rows of lar_solver (#6814) --- src/math/lp/int_solver.cpp | 8 ++-- src/math/lp/lar_solver.cpp | 67 +++++++++++---------------- src/math/lp/lar_solver.h | 20 ++++---- src/math/lp/lp_core_solver_base.h | 3 +- src/math/lp/lp_core_solver_base_def.h | 6 +-- src/sat/smt/arith_solver.cpp | 2 +- src/smt/theory_arith.h | 2 +- src/smt/theory_arith_core.h | 6 +-- src/smt/theory_lra.cpp | 2 +- 9 files changed, 51 insertions(+), 65 deletions(-) diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 88a31e65d..fc1c8d3dc 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -358,14 +358,14 @@ int_solver::int_solver(lar_solver& lar_slv) : // this will allow to enable and disable tracking of the pivot rows struct check_return_helper { lar_solver& lra; - bool m_track_pivoted_rows; + bool m_track_touched_rows; check_return_helper(lar_solver& ls) : lra(ls), - m_track_pivoted_rows(lra.get_track_pivoted_rows()) { - lra.set_track_pivoted_rows(false); + m_track_touched_rows(lra.touched_rows_are_tracked()) { + lra.track_touched_rows(false); } ~check_return_helper() { - lra.set_track_pivoted_rows(m_track_pivoted_rows); + lra.track_touched_rows(m_track_touched_rows); } }; diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 735f835e0..84f1b70c7 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -16,7 +16,7 @@ namespace lp { void lar_solver::updt_params(params_ref const& _p) { smt_params_helper p(_p); - set_track_pivoted_rows(p.arith_bprop_on_pivoted_rows()); + track_touched_rows(p.arith_bprop_on_pivoted_rows()); set_cut_strategy(p.arith_branch_cut_ratio()); m_settings.updt_params(_p); } @@ -28,12 +28,14 @@ namespace lp { m_term_register(true), m_constraints(*this) {} - void lar_solver::set_track_pivoted_rows(bool v) { - m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows = v ? (&m_rows_with_changed_bounds) : nullptr; + // start or ends tracking the rows that were changed by solve() + void lar_solver::track_touched_rows(bool v) { + m_mpq_lar_core_solver.m_r_solver.m_touched_rows = v ? (&m_touched_rows) : nullptr; } - - bool lar_solver::get_track_pivoted_rows() const { - return m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows != nullptr; + + // returns true iff the solver tracks the rows that were changed by solve() + bool lar_solver::touched_rows_are_tracked() const { + return m_mpq_lar_core_solver.m_r_solver.m_touched_rows != nullptr; } lar_solver::~lar_solver() { @@ -201,12 +203,6 @@ namespace lp { 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; } @@ -271,11 +267,11 @@ namespace lp { clean_popped_elements(n, m_incorrect_columns); for (auto rid : m_row_bounds_to_replay) - insert_row_with_changed_bounds(rid); + add_touched_row(rid); m_row_bounds_to_replay.reset(); unsigned m = A_r().row_count(); - clean_popped_elements(m, m_rows_with_changed_bounds); + clean_popped_elements(m, m_touched_rows); clean_inf_heap_of_r_solver_after_pop(); lp_assert( m_settings.simplex_strategy() == simplex_strategy_enum::undecided || @@ -616,17 +612,11 @@ namespace lp { left_side.push_back(std::make_pair(c, v)); } - void lar_solver::insert_row_with_changed_bounds(unsigned rid) { - m_rows_with_changed_bounds.insert(rid); - } - - - - void lar_solver::detect_rows_of_bound_change_column_for_nbasic_column_tableau(unsigned j) { - for (auto& rc : m_mpq_lar_core_solver.m_r_A.m_columns[j]) - insert_row_with_changed_bounds(rc.var()); + void lar_solver::add_touched_row(unsigned rid) { + m_touched_rows.insert(rid); } + bool lar_solver::use_tableau_costs() const { return m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs; @@ -697,9 +687,9 @@ namespace lp { void lar_solver::detect_rows_with_changed_bounds_for_column(unsigned j) { if (m_mpq_lar_core_solver.m_r_heading[j] >= 0) - insert_row_with_changed_bounds(m_mpq_lar_core_solver.m_r_heading[j]); + add_touched_row(m_mpq_lar_core_solver.m_r_heading[j]); else - detect_rows_of_bound_change_column_for_nbasic_column_tableau(j); + add_column_rows_to_touched_rows(j); } void lar_solver::detect_rows_with_changed_bounds() { @@ -710,6 +700,8 @@ namespace lp { void lar_solver::update_x_and_inf_costs_for_columns_with_changed_bounds_tableau() { for (auto j : m_columns_with_changed_bounds) update_x_and_inf_costs_for_column_with_changed_bounds(j); + // whoever consumes this should clear it + m_columns_with_changed_bounds.clear(); } @@ -1170,10 +1162,10 @@ namespace lp { ru.update(); } - void lar_solver::mark_rows_for_bound_prop(lpvar j) { - auto& column = A_r().m_columns[j]; + void lar_solver::add_column_rows_to_touched_rows(lpvar j) { + const auto& column = A_r().m_columns[j]; for (auto const& r : column) - insert_row_with_changed_bounds(r.var()); + add_touched_row(r.var()); } void lar_solver::pop() { @@ -1457,8 +1449,7 @@ namespace lp { A_r().add_row(); m_mpq_lar_core_solver.m_r_heading.push_back(m_mpq_lar_core_solver.m_r_basis.size()); m_mpq_lar_core_solver.m_r_basis.push_back(j); - if (m_settings.bound_propagation()) - insert_row_with_changed_bounds(A_r().row_count() - 1); + add_touched_row(A_r().row_count() - 1); } else { m_mpq_lar_core_solver.m_r_heading.push_back(-static_cast(m_mpq_lar_core_solver.m_r_nbasis.size()) - 1); @@ -1545,8 +1536,7 @@ namespace lp { var_index ret = tv::mask_term(adjusted_term_index); if (!coeffs.empty()) { add_row_from_term_no_constraint(m_terms.back(), ret); - if (m_settings.bound_propagation()) - insert_row_with_changed_bounds(A_r().row_count() - 1); + add_touched_row(A_r().row_count() - 1); } lp_assert(m_var_register.size() == A_r().column_count()); if (m_need_register_terms) @@ -1594,7 +1584,7 @@ namespace lp { m_mpq_lar_core_solver.m_column_types.push_back(column_type::free_column); increase_by_one_columns_with_changed_bounds(); m_incorrect_columns.increase_size_by_one(); - m_rows_with_changed_bounds.increase_size_by_one(); + m_touched_rows.increase_size_by_one(); add_new_var_to_core_fields_for_mpq(true); } @@ -1745,23 +1735,20 @@ namespace lp { update_column_type_and_bound_with_no_ub(j, kind, right_side, constr_index); TRACE("lar_solver_feas", tout << "j = " << j << " became " << (this->column_is_feasible(j)?"feas":"non-feas") << ", and " << (this->column_is_bounded(j)? "bounded":"non-bounded") << std::endl;); } - // clang-format on void lar_solver::insert_to_columns_with_changed_bounds(unsigned j) { m_columns_with_changed_bounds.insert(j); TRACE("lar_solver", tout << "column " << j << (column_is_feasible(j) ? " feas" : " non-feas") << "\n";); } - // clang-format off void lar_solver::update_column_type_and_bound_check_on_equal(unsigned j, - lconstraint_kind kind, - const mpq& right_side, - constraint_index constr_index, - unsigned& equal_to_j) { + lconstraint_kind kind, + const mpq& right_side, + constraint_index constr_index, + unsigned& equal_to_j) { update_column_type_and_bound(j, kind, right_side, constr_index); equal_to_j = null_lpvar; if (column_is_fixed(j)) { register_in_fixed_var_table(j, equal_to_j); } - } constraint_index lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq& right_side) { diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 75fb4338c..e73e6818c 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -86,7 +86,7 @@ class lar_solver : public column_namer { constraint_set m_constraints; // the set of column indices j such that bounds have changed for j u_set m_columns_with_changed_bounds; - u_set m_rows_with_changed_bounds; + u_set m_touched_rows; unsigned_vector m_row_bounds_to_replay; u_set m_basic_columns_with_changed_cost; @@ -190,14 +190,12 @@ class lar_solver : public column_namer { void substitute_terms_in_linear_expression(const vector>& left_side_with_terms, vector>& left_side) const; - void detect_rows_of_bound_change_column_for_nbasic_column_tableau(unsigned j); bool use_tableau_costs() const; bool tableau_with_costs() const; bool costs_are_used() const; void change_basic_columns_dependend_on_a_given_nb_column(unsigned j, const numeric_pair& delta); void update_x_and_inf_costs_for_column_with_changed_bounds(unsigned j); - unsigned num_changed_bounds() const { return m_rows_with_changed_bounds.size(); } - void insert_row_with_changed_bounds(unsigned rid); + void add_touched_row(unsigned rid); void detect_rows_with_changed_bounds_for_column(unsigned j); void detect_rows_with_changed_bounds(); @@ -328,11 +326,11 @@ class lar_solver : public column_namer { void activate_check_on_equal(constraint_index, var_index&); void activate(constraint_index); void random_update(unsigned sz, var_index const* vars); - void mark_rows_for_bound_prop(lpvar j); + void add_column_rows_to_touched_rows(lpvar j); template void propagate_bounds_for_touched_rows(lp_bound_propagator& bp) { unsigned num_prop = 0; - for (unsigned i : m_rows_with_changed_bounds) { + for (unsigned i : m_touched_rows) { num_prop += calculate_implied_bounds_for_row(i, bp); if (settings().get_cancel_flag()) return; @@ -342,7 +340,7 @@ class lar_solver : public column_namer { // and add fixed columns this way if (settings().propagate_eqs()) { bp.clear_for_eq(); - for (unsigned i : m_rows_with_changed_bounds) { + for (unsigned i : m_touched_rows) { unsigned offset_eqs = stats().m_offset_eqs; bp.cheap_eq_tree(i); if (settings().get_cancel_flag()) @@ -351,13 +349,13 @@ class lar_solver : public column_namer { m_row_bounds_to_replay.push_back(i); } } - m_rows_with_changed_bounds.clear(); + m_touched_rows.clear(); } template void check_missed_propagations(lp_bound_propagator& bp) { for (unsigned i = 0; i < A_r().row_count(); i++) - if (!m_rows_with_changed_bounds.contains(i)) + if (!m_touched_rows.contains(i)) if (0 < calculate_implied_bounds_for_row(i, bp)) { verbose_stream() << i << ": " << get_row(i) << "\n"; } @@ -612,8 +610,8 @@ class lar_solver : public column_namer { bool term_is_used_as_row(unsigned term) const; bool tighten_term_bounds_by_delta(tv const& t, const impq&); lar_solver(); - void set_track_pivoted_rows(bool v); - bool get_track_pivoted_rows() const; + void track_touched_rows(bool v); + bool touched_rows_are_tracked() const; ~lar_solver() override; const vector& r_x() const { return m_mpq_lar_core_solver.m_r_x; } bool column_is_int(unsigned j) const; diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h index 66154368e..6db4776db 100644 --- a/src/math/lp/lp_core_solver_base.h +++ b/src/math/lp/lp_core_solver_base.h @@ -91,7 +91,8 @@ public: unsigned m_basis_sort_counter; vector m_trace_of_basis_change_vector; // the even positions are entering, the odd positions are leaving bool m_tracing_basis_changes; - u_set* m_pivoted_rows; + // these rows are changed by adding to them a multiple of the pivot row + u_set* m_touched_rows; bool m_look_for_feasible_solution_only; void start_tracing_basis_changes() { diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h index 319966091..1687786a8 100644 --- a/src/math/lp/lp_core_solver_base_def.h +++ b/src/math/lp/lp_core_solver_base_def.h @@ -58,7 +58,7 @@ lp_core_solver_base(static_matrix & A, m_upper_bounds(upper_bound_values), m_basis_sort_counter(0), m_tracing_basis_changes(false), - m_pivoted_rows(nullptr), + m_touched_rows(nullptr), m_look_for_feasible_solution_only(false) { lp_assert(bounds_for_boxed_are_set_correctly()); init(); @@ -324,8 +324,8 @@ pivot_column_tableau(unsigned j, unsigned piv_row_index) { if(! m_A.pivot_row_to_row_given_cell(piv_row_index, c, j)) { return false; } - if (m_pivoted_rows!= nullptr) - m_pivoted_rows->insert(c.var()); + if (m_touched_rows!= nullptr) + m_touched_rows->insert(c.var()); } if (m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs) diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index bd5dd315f..ccbe2591b 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -396,7 +396,7 @@ namespace arith { propagate_eqs(b.tv(), ci, k, b, value.get_rational()); #if 0 if (propagation_mode() != BP_NONE) - lp().mark_rows_for_bound_prop(b.tv().id()); + lp().add_column_rows_to_touched_rows(b.tv().id()); #endif } diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 92aa4baec..8cbf844b9 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -788,7 +788,7 @@ namespace smt { // // ----------------------------------- void mark_row_for_bound_prop(unsigned r1); - void mark_rows_for_bound_prop(theory_var v); + void add_column_rows_to_touched_rows(theory_var v); void is_row_useful_for_bound_prop(row const & r, int & lower_idx, int & upper_idx) const; unsigned imply_bound_for_monomial(row const & r, int idx, bool lower); unsigned imply_bound_for_all_monomials(row const & r, bool lower); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 0a4c1869b..9fb99c0b4 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -2486,7 +2486,7 @@ namespace smt { set_bound(b, false); if (propagation_mode() != bound_prop_mode::BP_NONE) - mark_rows_for_bound_prop(v); + add_column_rows_to_touched_rows(v); return true; } @@ -2534,7 +2534,7 @@ namespace smt { set_bound(b, true); if (propagation_mode() != bound_prop_mode::BP_NONE) - mark_rows_for_bound_prop(v); + add_column_rows_to_touched_rows(v); return true; } @@ -2603,7 +2603,7 @@ namespace smt { \brief Mark all rows that contain v for bound propagation. */ template - void theory_arith::mark_rows_for_bound_prop(theory_var v) { + void theory_arith::add_column_rows_to_touched_rows(theory_var v) { for (col_entry const& ce : m_columns[v]) { if (!ce.is_dead()) mark_row_for_bound_prop(ce.m_row_id); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 0c182dce5..6ffefbdc6 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2989,7 +2989,7 @@ public: } #if 0 if (should_propagate()) - lp().mark_rows_for_bound_prop(b.tv().id()); + lp().add_column_rows_to_touched_rows(b.tv().id()); #endif }