mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 21:33:39 +00:00
Code Activity

use setter method to easier track updates to settings.

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-01-26 13:53:51 -08:00
parent 19fed09122
commit 0f86a00229
4 changed files with 9 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/lar_core_solver.h
View file

@ -222,7 +222,7 @@ public:
m_d_x.resize(m_d_A.column_count()); m_d_x.resize(m_d_A.column_count());
pop_basis(k); pop_basis(k);
m_stacked_simplex_strategy.pop(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(m_r_solver.basis_heading_is_correct());
lp_assert(!need_to_presolve_with_double_solver() || m_d_solver.basis_heading_is_correct()); lp_assert(!need_to_presolve_with_double_solver() || m_d_solver.basis_heading_is_correct());
} }

10
src/math/lp/lar_solver.cpp
View file

@ -300,7 +300,7 @@ namespace lp {
m_term_register.shrink(m_term_count); m_term_register.shrink(m_term_count);
m_terms.resize(m_term_count); m_terms.resize(m_term_count);
m_simplex_strategy.pop(k); 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(sizes_are_correct());
lp_assert((!m_settings.use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); 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); m_usage_in_terms.pop(k);
@ -465,10 +465,10 @@ namespace lp {
switch (settings().simplex_strategy()) { switch (settings().simplex_strategy()) {
case simplex_strategy_enum::tableau_rows: 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); prepare_costs_for_r_solver(term);
ret = maximize_term_on_tableau(term, term_max); 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); set_costs_to_zero(term);
m_mpq_lar_core_solver.m_r_solver.set_status(lp_status::OPTIMAL); m_mpq_lar_core_solver.m_r_solver.set_status(lp_status::OPTIMAL);
return ret; return ret;
@ -2006,10 +2006,10 @@ namespace lp {
void lar_solver::decide_on_strategy_and_adjust_initial_state() { void lar_solver::decide_on_strategy_and_adjust_initial_state() {
lp_assert(strategy_is_undecided()); lp_assert(strategy_is_undecided());
if (m_columns_to_ul_pairs.size() > m_settings.column_number_threshold_for_using_lu_in_lar_solver) { 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 { 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(); adjust_initial_state();
} }

4
src/math/lp/lp_settings.h
View file

@ -336,8 +336,8 @@ public:
return m_simplex_strategy; return m_simplex_strategy;
} }
simplex_strategy_enum & simplex_strategy() { void set_simplex_strategy(simplex_strategy_enum s) {
return m_simplex_strategy; m_simplex_strategy = s;
} }
bool use_lu() const { bool use_lu() const {

2
src/shell/lp_frontend.cpp
View file

@ -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().set_message_ostream(&std::cout);
solver->settings().report_frequency = params.arith_rep_freq(); solver->settings().report_frequency = params.arith_rep_freq();
solver->settings().print_statistics = params.arith_print_stats(); 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(); solver->find_maximal_solution();