From 316f2194e0e3278f871693a4b842196433a0c06f Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 19 Mar 2020 11:17:45 -0700 Subject: [PATCH] rename Signed-off-by: Lev Nachmanson --- src/math/lp/lar_solver.cpp | 18 +++++++++--------- src/math/lp/lar_solver.h | 9 +++++---- 2 files changed, 14 insertions(+), 13 deletions(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 08d7b0502..886c31f9f 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -21,7 +21,7 @@ void clear() {lp_assert(false); // not implemented lar_solver::lar_solver() : m_status(lp_status::UNKNOWN), - m_infeasible_column(-1), + m_crossed_bounds_column(-1), m_mpq_lar_core_solver(m_settings, *this), m_int_solver(nullptr), m_need_register_terms(false), @@ -293,12 +293,12 @@ lp_status lar_solver::solve() { return m_status; } -void lar_solver::fill_explanation_from_infeasible_column(explanation & evidence) const{ - lp_assert(static_cast(get_column_type(m_infeasible_column)) >= static_cast(column_type::boxed)); - lp_assert(!m_mpq_lar_core_solver.m_r_solver.column_is_feasible(m_infeasible_column)); +void lar_solver::fill_explanation_from_crossed_bounds_column(explanation & evidence) const{ + lp_assert(static_cast(get_column_type(m_crossed_bounds_column)) >= static_cast(column_type::boxed)); + lp_assert(!m_mpq_lar_core_solver.m_r_solver.column_is_feasible(m_crossed_bounds_column)); // this is the case when the lower bound is in conflict with the upper one - const ul_pair & ul = m_columns_to_ul_pairs[m_infeasible_column]; + const ul_pair & ul = m_columns_to_ul_pairs[m_crossed_bounds_column]; evidence.push_justification(ul.upper_bound_witness(), numeric_traits::one()); evidence.push_justification(ul.lower_bound_witness(), -numeric_traits::one()); } @@ -317,7 +317,7 @@ void lar_solver::push() { m_simplex_strategy = m_settings.simplex_strategy(); m_simplex_strategy.push(); m_columns_to_ul_pairs.push(); - m_infeasible_column.push(); + m_crossed_bounds_column.push(); m_mpq_lar_core_solver.push(); m_term_count = m_terms.size(); m_term_count.push(); @@ -341,7 +341,7 @@ void lar_solver::shrink_inf_set_after_pop(unsigned n, int_set & set) { void lar_solver::pop(unsigned k) { TRACE("lar_solver", tout << "k = " << k << std::endl;); - m_infeasible_column.pop(k); + m_crossed_bounds_column.pop(k); unsigned n = m_columns_to_ul_pairs.peek_size(k); m_var_register.shrink(n); if (m_settings.use_tableau()) { @@ -1163,8 +1163,8 @@ bool lar_solver::has_value(var_index var, mpq& value) const { void lar_solver::get_infeasibility_explanation(explanation& exp) const { exp.clear(); - if (m_infeasible_column != -1) { - fill_explanation_from_infeasible_column(exp); + if (m_crossed_bounds_column != -1) { + fill_explanation_from_crossed_bounds_column(exp); return; } if (m_mpq_lar_core_solver.get_infeasible_sum_sign() == 0) { diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 5615808f0..51885e39b 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -82,7 +82,8 @@ class lar_solver : public column_namer { lp_settings m_settings; lp_status m_status; stacked_value m_simplex_strategy; - stacked_value m_infeasible_column; // such can be found at the initialization step + // such can be found at the initialization step: u < l + stacked_value m_crossed_bounds_column; public: lar_core_solver m_mpq_lar_core_solver; private: @@ -100,7 +101,7 @@ public: // these are basic columns with the value changed, so the the corresponding row in the tableau // does not sum to zero anymore int_set m_incorrect_columns; - stacked_value m_infeasible_column_index; // such can be found at the initialization step + stacked_value m_crossed_bounds_column_index; // such can be found at the initialization step stacked_value m_term_count; vector m_terms; indexed_vector m_column_buffer; @@ -208,7 +209,7 @@ public: void set_infeasible_column(unsigned j) { set_status(lp_status::INFEASIBLE); - m_infeasible_column = j; + m_crossed_bounds_column = j; } constraint_index add_constraint_from_term_and_create_new_column_row(unsigned term_j, const lar_term* term, @@ -322,7 +323,7 @@ public: lp_status solve(); - void fill_explanation_from_infeasible_column(explanation & evidence) const; + void fill_explanation_from_crossed_bounds_column(explanation & evidence) const; unsigned get_total_iterations() const;