use setter method to easier track updates to settings.

Z3Prover · Feb 1, 2023 · 0f86a00 · 0f86a00
1 parent 19fed09
commit 0f86a00
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 9 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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();