diff --git a/src/math/lp/lar_core_solver.h b/src/math/lp/lar_core_solver.h index 0043ed23d93..bcd33966f90 100644 --- a/src/math/lp/lar_core_solver.h +++ b/src/math/lp/lar_core_solver.h @@ -222,7 +222,7 @@ class lar_core_solver { m_d_x.resize(m_d_A.column_count()); pop_basis(k); m_stacked_simplex_strategy.pop(k); - settings().simplex_strategy() = m_stacked_simplex_strategy; + settings().set_simplex_strategy(m_stacked_simplex_strategy); lp_assert(m_r_solver.basis_heading_is_correct()); lp_assert(!need_to_presolve_with_double_solver() || m_d_solver.basis_heading_is_correct()); } diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index f78dab1197a..46ed0b5a93b 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -300,7 +300,7 @@ namespace lp { m_term_register.shrink(m_term_count); m_terms.resize(m_term_count); m_simplex_strategy.pop(k); - m_settings.simplex_strategy() = m_simplex_strategy; + m_settings.set_simplex_strategy(m_simplex_strategy); lp_assert(sizes_are_correct()); lp_assert((!m_settings.use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); m_usage_in_terms.pop(k); @@ -465,10 +465,10 @@ namespace lp { switch (settings().simplex_strategy()) { case simplex_strategy_enum::tableau_rows: - settings().simplex_strategy() = simplex_strategy_enum::tableau_costs; + settings().set_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; + settings().set_simplex_strategy(simplex_strategy_enum::tableau_rows); set_costs_to_zero(term); m_mpq_lar_core_solver.m_r_solver.set_status(lp_status::OPTIMAL); return ret; @@ -2006,10 +2006,10 @@ namespace lp { void lar_solver::decide_on_strategy_and_adjust_initial_state() { lp_assert(strategy_is_undecided()); if (m_columns_to_ul_pairs.size() > m_settings.column_number_threshold_for_using_lu_in_lar_solver) { - m_settings.simplex_strategy() = simplex_strategy_enum::lu; + m_settings.set_simplex_strategy(simplex_strategy_enum::lu); } else { - m_settings.simplex_strategy() = simplex_strategy_enum::tableau_rows; // todo: when to switch to tableau_costs? + m_settings.set_simplex_strategy(simplex_strategy_enum::tableau_rows); // todo: when to switch to tableau_costs? } adjust_initial_state(); } diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index aa06cb26361..2245f6f4ed1 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -336,8 +336,8 @@ struct lp_settings { return m_simplex_strategy; } - simplex_strategy_enum & simplex_strategy() { - return m_simplex_strategy; + void set_simplex_strategy(simplex_strategy_enum s) { + m_simplex_strategy = s; } bool use_lu() const { diff --git a/src/shell/lp_frontend.cpp b/src/shell/lp_frontend.cpp index 70d2cffb1f0..8d6425533c8 100644 --- a/src/shell/lp_frontend.cpp +++ b/src/shell/lp_frontend.cpp @@ -80,7 +80,7 @@ void run_solver(smt_params_helper & params, char const * mps_file_name) { solver->settings().set_message_ostream(&std::cout); solver->settings().report_frequency = params.arith_rep_freq(); solver->settings().print_statistics = params.arith_print_stats(); - solver->settings().simplex_strategy() = lp:: simplex_strategy_enum::lu; + solver->settings().set_simplex_strategy(lp:: simplex_strategy_enum::lu); solver->find_maximal_solution();