From a05dec99cf1b86f40606dd38c3182dab454bd5cc Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 3 Feb 2020 12:48:07 -0800 Subject: [PATCH] do not random_update int vars Signed-off-by: Lev Nachmanson --- src/math/lp/lar_core_solver.h | 2 +- src/math/lp/lar_solver.cpp | 15 ++++++++++----- src/math/lp/lp_core_solver_base.cpp | 6 +++--- src/math/lp/lp_core_solver_base.h | 16 ++++++++++------ src/math/lp/lp_core_solver_base_def.h | 4 ++-- src/math/lp/lp_primal_core_solver_def.h | 2 +- src/math/lp/lp_primal_core_solver_tableau_def.h | 6 +++--- 7 files changed, 30 insertions(+), 21 deletions(-) diff --git a/src/math/lp/lar_core_solver.h b/src/math/lp/lar_core_solver.h index b248d28f4..54430a3f5 100644 --- a/src/math/lp/lar_core_solver.h +++ b/src/math/lp/lar_core_solver.h @@ -338,7 +338,7 @@ public: for (const auto & cc : m_r_solver.m_A.m_columns[j]){ unsigned i = cc.var(); unsigned jb = m_r_solver.m_basis[i]; - m_r_solver.update_x_with_delta_and_track_feasibility(jb, - delta * m_r_solver.m_A.get_val(cc)); + m_r_solver.add_delta_to_x_and_track_feasibility(jb, - delta * m_r_solver.m_A.get_val(cc)); } CASSERT("A_off", m_r_solver.A_mult_x_is_off() == false); } diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index e6a493bd4..b766cfeac 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -784,7 +784,7 @@ void lar_solver::change_basic_columns_dependend_on_a_given_nb_column(unsigned j, if (tableau_with_costs()) { m_basic_columns_with_changed_cost.insert(bj); } - m_mpq_lar_core_solver.m_r_solver.update_x_with_delta_and_track_feasibility(bj, - A_r().get_val(c) * delta); + m_mpq_lar_core_solver.m_r_solver.add_delta_to_x_and_track_feasibility(bj, - A_r().get_val(c) * delta); TRACE("change_x_del", tout << "changed basis column " << bj << ", it is " << ( m_mpq_lar_core_solver.m_r_solver.column_is_feasible(bj)? "feas":"inf") << std::endl;); @@ -796,7 +796,7 @@ void lar_solver::change_basic_columns_dependend_on_a_given_nb_column(unsigned j, m_mpq_lar_core_solver.m_r_solver.solve_Bd(j, m_column_buffer); for (unsigned i : m_column_buffer.m_index) { unsigned bj = m_mpq_lar_core_solver.m_r_basis[i]; - m_mpq_lar_core_solver.m_r_solver.update_x_with_delta_and_track_feasibility(bj, -m_column_buffer[i] * delta); + m_mpq_lar_core_solver.m_r_solver.add_delta_to_x_and_track_feasibility(bj, -m_column_buffer[i] * delta); } } } @@ -1439,11 +1439,15 @@ void lar_solver::fill_var_set_for_random_update(unsigned sz, var_index const * v for (unsigned i = 0; i < sz; i++) { var_index var = vars[i]; if (var >= m_terms_start_index) { // handle the term + lpvar j = adjust_term_index(var); + if (column_is_int(j)) + continue; for (auto it : *m_terms[var - m_terms_start_index]) { column_list.push_back(it.var()); } } else { - column_list.push_back(var); + if (!column_is_int(var)) + column_list.push_back(var); } } } @@ -1728,6 +1732,7 @@ void lar_solver::add_new_var_to_core_fields_for_doubles(bool register_in_basis) void lar_solver::add_new_var_to_core_fields_for_mpq(bool register_in_basis) { unsigned j = A_r().column_count(); + TRACE("add_var", tout << "j = " << j << std::endl;); A_r().add_column(); lp_assert(m_mpq_lar_core_solver.m_r_x.size() == j); // lp_assert(m_mpq_lar_core_solver.m_r_lower_bounds.size() == j && m_mpq_lar_core_solver.m_r_upper_bounds.size() == j); // restore later @@ -1841,7 +1846,7 @@ void lar_solver::add_row_from_term_no_constraint(const lar_term * term, unsigned else { fill_last_row_of_A_r(A_r(), term); } - m_mpq_lar_core_solver.m_r_solver.update_x_and_call_tracker(j, get_basic_var_value_from_row(A_r().row_count() - 1)); + m_mpq_lar_core_solver.m_r_solver.update_x(j, get_basic_var_value_from_row(A_r().row_count() - 1)); if (use_lu()) fill_last_row_of_A_d(A_d(), term); } @@ -2313,7 +2318,7 @@ void lar_solver::fix_terms_with_rounded_columns() { if (need_to_fix) { lpvar j = external_to_local(ti); impq v = t.apply(m_mpq_lar_core_solver.m_r_x); - m_mpq_lar_core_solver.m_r_solver.update_x_and_call_tracker(j, v); + m_mpq_lar_core_solver.m_r_solver.update_x(j, v); } } SASSERT(ax_is_correct()); diff --git a/src/math/lp/lp_core_solver_base.cpp b/src/math/lp/lp_core_solver_base.cpp index 8219c3f26..6a711029e 100644 --- a/src/math/lp/lp_core_solver_base.cpp +++ b/src/math/lp/lp_core_solver_base.cpp @@ -56,7 +56,7 @@ template void lp::lp_core_solver_base::solve_Bd(unsigned int); template void lp::lp_core_solver_base>::solve_Bd(unsigned int, indexed_vector&); template void lp::lp_core_solver_base::solve_yB(vector&); template bool lp::lp_core_solver_base::update_basis_and_x(int, int, double const&); -template void lp::lp_core_solver_base::update_x(unsigned int, const double&); +template void lp::lp_core_solver_base::add_delta_to_entering(unsigned int, const double&); template bool lp::lp_core_solver_base::A_mult_x_is_off() const; template bool lp::lp_core_solver_base::A_mult_x_is_off_on_index(const vector &) const; template bool lp::lp_core_solver_base::basis_heading_is_correct() const ; @@ -73,7 +73,7 @@ template void lp::lp_core_solver_base::solve_Ax_eq_b(); template void lp::lp_core_solver_base::solve_Bd(unsigned int); template void lp::lp_core_solver_base::solve_yB(vector&); template bool lp::lp_core_solver_base::update_basis_and_x(int, int, lp::mpq const&); -template void lp::lp_core_solver_base::update_x(unsigned int, const lp::mpq&); +template void lp::lp_core_solver_base::add_delta_to_entering(unsigned int, const lp::mpq&); template void lp::lp_core_solver_base >::calculate_pivot_row_of_B_1(unsigned int); template void lp::lp_core_solver_base >::calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned); template void lp::lp_core_solver_base >::init(); @@ -87,7 +87,7 @@ template void lp::lp_core_solver_base >::snap template void lp::lp_core_solver_base >::solve_Ax_eq_b(); template void lp::lp_core_solver_base >::solve_Bd(unsigned int); template bool lp::lp_core_solver_base >::update_basis_and_x(int, int, lp::numeric_pair const&); -template void lp::lp_core_solver_base >::update_x(unsigned int, const lp::numeric_pair&); +template void lp::lp_core_solver_base >::add_delta_to_entering(unsigned int, const lp::numeric_pair&); template lp::lp_core_solver_base::lp_core_solver_base( lp::static_matrix&, vector&, diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h index 6b1f75e54..9eb55c32e 100644 --- a/src/math/lp/lp_core_solver_base.h +++ b/src/math/lp/lp_core_solver_base.h @@ -180,7 +180,7 @@ public: void calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned pivot_row); - void update_x(unsigned entering, const X & delta); + void add_delta_to_entering(unsigned entering, const X & delta); const T & get_var_value(unsigned j) const { return m_x[j]; @@ -429,7 +429,7 @@ public: break; } if (ret) - add_delta_to_x_and_do_not_track_feasibility(j, delta); + add_delta_to_x(j, delta); return ret; @@ -685,21 +685,25 @@ public: } void update_x_with_feasibility_tracking(unsigned j, const X & v) { + TRACE("lar_solver", tout << "j = " << j << ", v = " << v << "\n";); m_x[j] = v; track_column_feasibility(j); } - void update_x_with_delta_and_track_feasibility(unsigned j, const X & del) { + void add_delta_to_x_and_track_feasibility(unsigned j, const X & del) { + TRACE("lar_solver", tout << "del = " << del << ", was x[" << j << "] = " << m_x[j] << "\n";); m_x[j] += del; + TRACE("lar_solver", tout << "became x[" << j << "] = " << m_x[j] << "\n";); track_column_feasibility(j); } - void update_x_and_call_tracker(unsigned j, const X & v) { - TRACE("lar_solver", tout << "j = " << j << "\n";); + void update_x(unsigned j, const X & v) { + TRACE("lar_solver", tout << "j = " << j << ", v = " << v << "\n";); m_x[j] = v; } - void add_delta_to_x_and_do_not_track_feasibility(unsigned j, const X & delta) { + void add_delta_to_x(unsigned j, const X & delta) { + TRACE("lar_solver", tout << "j = " << j << ", delta = " << delta << "\n";); m_x[j] += delta; } diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h index b5f5c222f..ce560b92b 100644 --- a/src/math/lp/lp_core_solver_base_def.h +++ b/src/math/lp/lp_core_solver_base_def.h @@ -321,7 +321,7 @@ calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned pivot_row) { } template void lp_core_solver_base:: -update_x(unsigned entering, const X& delta) { +add_delta_to_entering(unsigned entering, const X& delta) { m_x[entering] += delta; if (!use_tableau()) for (unsigned i : m_ed.m_index) { @@ -526,7 +526,7 @@ template bool lp_core_solver_base:: update_basis_and_x(int entering, int leaving, X const & tt) { if (!is_zero(tt)) { - update_x(entering, tt); + add_delta_to_entering(entering, tt); if ((!numeric_traits::precise()) && A_mult_x_is_off_on_index(m_ed.m_index) && !find_x_by_solving()) { init_factorization(m_factorization, m_A, m_basis, m_settings); if (!find_x_by_solving()) { diff --git a/src/math/lp/lp_primal_core_solver_def.h b/src/math/lp/lp_primal_core_solver_def.h index 4e4b2e71e..015ac3694 100644 --- a/src/math/lp/lp_primal_core_solver_def.h +++ b/src/math/lp/lp_primal_core_solver_def.h @@ -675,7 +675,7 @@ template void lp_primal_core_solver::calc_work template void lp_primal_core_solver::advance_on_entering_equal_leaving(int entering, X & t) { CASSERT("A_off", !this->A_mult_x_is_off() ); - this->update_x(entering, t * m_sign_of_entering_delta); + this->add_delta_to_entering(entering, t * m_sign_of_entering_delta); if (this->A_mult_x_is_off_on_index(this->m_ed.m_index) && !this->find_x_by_solving()) { this->init_lu(); if (!this->find_x_by_solving()) { diff --git a/src/math/lp/lp_primal_core_solver_tableau_def.h b/src/math/lp/lp_primal_core_solver_tableau_def.h index fa7b5e883..357de7421 100644 --- a/src/math/lp/lp_primal_core_solver_tableau_def.h +++ b/src/math/lp/lp_primal_core_solver_tableau_def.h @@ -358,11 +358,11 @@ update_basis_and_x_tableau(int entering, int leaving, X const & tt) { } template void lp_primal_core_solver:: update_x_tableau(unsigned entering, const X& delta) { - this->add_delta_to_x_and_do_not_track_feasibility(entering, delta); + this->add_delta_to_x(entering, delta); if (!this->m_using_infeas_costs) { for (const auto & c : this->m_A.m_columns[entering]) { unsigned i = c.var(); - this->update_x_with_delta_and_track_feasibility(this->m_basis[i], - delta * this->m_A.get_val(c)); + this->add_delta_to_x_and_track_feasibility(this->m_basis[i], - delta * this->m_A.get_val(c)); } } else { // m_using_infeas_costs == true lp_assert(this->column_is_feasible(entering)); @@ -371,7 +371,7 @@ update_x_tableau(unsigned entering, const X& delta) { for (const auto & c : this->m_A.m_columns[entering]) { unsigned i = c.var(); unsigned j = this->m_basis[i]; - this->add_delta_to_x_and_do_not_track_feasibility(j, -delta * this->m_A.get_val(c)); + this->add_delta_to_x(j, -delta * this->m_A.get_val(c)); update_inf_cost_for_column_tableau(j); if (is_zero(this->m_costs[j])) this->remove_column_from_inf_set(j);