From 6c5d7fbe96106d1a9cc41812d4c2148de30ba7c5 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 18 Mar 2020 13:47:43 -0700 Subject: [PATCH] fixes in max term with tableau Signed-off-by: Lev Nachmanson --- src/math/lp/lar_solver.cpp | 14 ++++++++++---- src/math/lp/lp_primal_core_solver_tableau_def.h | 4 +++- src/smt/theory_lra.cpp | 1 + 3 files changed, 14 insertions(+), 5 deletions(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index e7aa0ff20..3ece75d40 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -392,6 +392,7 @@ bool lar_solver::maximize_term_on_tableau(const lar_term & term, m_mpq_lar_core_solver.solve(); lp_status st = m_mpq_lar_core_solver.m_r_solver.get_status(); TRACE("lar_solver", tout << st << "\n";); + SASSERT( m_mpq_lar_core_solver.m_r_solver.calc_current_x_is_feasible_include_non_basis()); if (st == lp_status::UNBOUNDED) { return false; } @@ -442,6 +443,8 @@ void lar_solver::set_costs_to_zero(const lar_term& term) { void lar_solver::prepare_costs_for_r_solver(const lar_term & term) { TRACE("lar_solver", print_term(term, tout << "prepare: ") << "\n";); + m_basic_columns_with_changed_cost.clear(); + m_basic_columns_with_changed_cost.resize(m_mpq_lar_core_solver.m_r_x.size()); if (move_non_basic_columns_to_bounds()) find_feasible_solution(); auto & rslv = m_mpq_lar_core_solver.m_r_solver; @@ -457,6 +460,7 @@ void lar_solver::prepare_costs_for_r_solver(const lar_term & term) { else rslv.update_reduced_cost_for_basic_column_cost_change(- p.coeff(), j); } + rslv.m_costs_backup = rslv.m_costs; lp_assert(rslv.reduced_costs_are_correct_tableau()); } @@ -525,8 +529,8 @@ bool lar_solver::maximize_term_on_corrected_r_solver(lar_term & term, switch (settings().simplex_strategy()) { case simplex_strategy_enum::tableau_rows: - prepare_costs_for_r_solver(term); settings().simplex_strategy() = simplex_strategy_enum::tableau_costs; + prepare_costs_for_r_solver(term); ret = maximize_term_on_tableau(term, term_max); settings().simplex_strategy() = simplex_strategy_enum::tableau_rows; set_costs_to_zero(term); @@ -818,9 +822,11 @@ void lar_solver::update_x_and_inf_costs_for_columns_with_changed_bounds_tableau( update_x_and_inf_costs_for_column_with_changed_bounds(j); if (tableau_with_costs()) { - for (unsigned j : m_basic_columns_with_changed_cost.m_index) - m_mpq_lar_core_solver.m_r_solver.update_inf_cost_for_column_tableau(j); - lp_assert(m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); + if (m_mpq_lar_core_solver.m_r_solver.m_using_infeas_costs) { + for (unsigned j : m_basic_columns_with_changed_cost.m_index) + m_mpq_lar_core_solver.m_r_solver.update_inf_cost_for_column_tableau(j); + lp_assert(m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); + } } } 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 357de7421..59d23a745 100644 --- a/src/math/lp/lp_primal_core_solver_tableau_def.h +++ b/src/math/lp/lp_primal_core_solver_tableau_def.h @@ -161,7 +161,7 @@ unsigned lp_primal_core_solver::solve_with_tableau() { break; case lp_status::UNBOUNDED: if (this->current_x_is_infeasible()) { - init_reduced_costs(); + init_reduced_costs_tableau(); this->set_status(lp_status::UNKNOWN); } break; @@ -385,7 +385,9 @@ update_x_tableau(unsigned entering, const X& delta) { template void lp_primal_core_solver:: update_inf_cost_for_column_tableau(unsigned j) { lp_assert(this->m_settings.simplex_strategy() != simplex_strategy_enum::tableau_rows); + lp_assert(this->m_using_infeas_costs); + T new_cost = get_infeasibility_cost_for_column(j); T delta = this->m_costs[j] - new_cost; if (is_zero(delta)) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index e6896e863..505b975cf 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -863,6 +863,7 @@ class theory_lra::imp { bool is_infeasible() const { return lp().get_status() == lp::lp_status::INFEASIBLE; + // || lp().get_status() == lp::lp_status::UNKNOWN; } void internalize_eq(theory_var v1, theory_var v2) {