mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-25 18:15:32 +00:00
Code Activity

rm lu

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2023-03-04 12:15:48 -08:00
parent 97c1ba4641
commit a38be43264
5 changed files with 11 additions and 74 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -229,7 +229,7 @@ public:
}
bool need_to_presolve_with_double_solver() const {
return settings().simplex_strategy() == simplex_strategy_enum::lu;
return false;
}
template <typename L>

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

@ -45,7 +45,7 @@ namespace lp {
delete t;
}
bool lar_solver::use_lu() const { return m_settings.simplex_strategy() == simplex_strategy_enum::lu; }
bool lar_solver::use_lu() const { return false; }
bool lar_solver::sizes_are_correct() const {
lp_assert(strategy_is_undecided() || !m_mpq_lar_core_solver.need_to_presolve_with_double_solver() || A_r().column_count() == A_d().column_count());
@ -478,10 +478,7 @@ namespace lp {
m_mpq_lar_core_solver.m_r_solver.set_status(lp_status::OPTIMAL);
return ret;
case simplex_strategy_enum::lu:
lp_assert(false); // not implemented
return false;
default:
lp_unreachable(); // wrong mode
}
@ -1999,20 +1996,14 @@ 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.set_simplex_strategy(simplex_strategy_enum::lu);
}
else {
m_settings.set_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();
}
void lar_solver::adjust_initial_state() {
switch (m_settings.simplex_strategy()) {
case simplex_strategy_enum::lu:
adjust_initial_state_for_lu();
break;
case simplex_strategy_enum::tableau_rows:
adjust_initial_state_for_tableau_rows();
break;

20
src/math/lp/lp_core_solver_base_def.h
View file

@ -894,27 +894,11 @@ template <typename T, typename X> bool lp_core_solver_base<T, X>::pivot_column_g
lp_assert(m_basis_heading[j] < 0);
lp_assert(m_basis_heading[j_basic] >= 0);
unsigned row_index = m_basis_heading[j_basic];
if (m_settings.m_simplex_strategy == simplex_strategy_enum::lu) {
if (m_factorization->need_to_refactor()) {
init_lu();
}
else {
m_factorization->prepare_entering(j, w); // to init vector w
m_factorization->replace_column(zero_of_type<T>(), w, row_index);
}
if (m_factorization->get_status() != LU_status::OK) {
init_lu();
return false;
}
else {
change_basis(j, j_basic);
}
}
else { // the tableau case
// the tableau case
if (pivot_column_tableau(j, row_index))
change_basis(j, j_basic);
else return false;
}
return true;
}

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

@ -55,8 +55,7 @@ inline std::ostream& operator<<(std::ostream& out, column_type const& t) {
enum class simplex_strategy_enum {
undecided = 3,
tableau_rows = 0,
tableau_costs = 1,
lu = 2
tableau_costs = 1
};
std::string column_type_to_string(column_type t);
@ -341,12 +340,11 @@ public:
}
bool use_lu() const {
return m_simplex_strategy == simplex_strategy_enum::lu;
return false;
}
bool use_tableau() const {
return m_simplex_strategy == simplex_strategy_enum::tableau_rows ||
m_simplex_strategy == simplex_strategy_enum::tableau_costs;
return true;
}
bool use_tableau_rows() const {