mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +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 16:02:46 -08:00
parent 9a7c99da33
commit 5f03c93270
6 changed files with 4 additions and 100 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/math/lp/lp_core_solver_base.cpp
View file

@ -52,7 +52,6 @@ template void lp::lp_core_solver_base<double, double>::snap_xN_to_bounds_and_fre
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::snap_xN_to_bounds_and_free_columns_to_zeroes();
template void lp::lp_core_solver_base<double, double>::solve_Ax_eq_b();
template void lp::lp_core_solver_base<double, double>::solve_yB(vector<double >&) const;
template bool lp::lp_core_solver_base<double, double>::update_basis_and_x(int, int, double const&);
template void lp::lp_core_solver_base<double, double>::add_delta_to_entering(unsigned int, const double&);
template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::A_mult_x_is_off() const;
template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::A_mult_x_is_off_on_index(const vector<unsigned> &) const;
@ -67,7 +66,6 @@ template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::restore_x(unsigned int,
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::set_non_basic_x_to_correct_bounds();
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::solve_Ax_eq_b();
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::solve_yB(vector<lp::mpq>&) const;
template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::update_basis_and_x(int, int, lp::mpq const&);
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::add_delta_to_entering(unsigned int, const lp::mpq&);
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned);
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::init();
@ -82,7 +80,6 @@ template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::prin
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::snap_xN_to_bounds_and_fill_xB();
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::solve_Ax_eq_b();
template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::update_basis_and_x(int, int, lp::numeric_pair<lp::mpq> const&);
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::add_delta_to_entering(unsigned int, const lp::numeric_pair<lp::mpq>&);
template lp::lp_core_solver_base<lp::mpq, lp::mpq>::lp_core_solver_base(
lp::static_matrix<lp::mpq, lp::mpq>&,

3
src/math/lp/lp_core_solver_base.h
View file

@ -307,8 +307,7 @@ public:
bool find_x_by_solving();
bool update_basis_and_x(int entering, int leaving, X const & tt);
bool basis_has_no_doubles() const;
bool non_basis_has_no_doubles() const;

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

@ -457,66 +457,6 @@ template <typename T, typename X> bool lp_core_solver_base<T, X>::inf_set_is_cor
return true;
}
template <typename T, typename X> bool lp_core_solver_base<T, X>::
update_basis_and_x(int entering, int leaving, X const & tt) {
if (!is_zero(tt)) {
add_delta_to_entering(entering, tt);
if ((!numeric_traits<T>::precise()) && A_mult_x_is_off_on_index(m_ed.m_index) && !find_x_by_solving()) {
init_factorization(m_factorization, m_A, m_basis, m_settings);
if (!find_x_by_solving()) {
restore_x(entering, tt);
if(A_mult_x_is_off()) {
m_status = lp_status::FLOATING_POINT_ERROR;
m_iters_with_no_cost_growing++;
return false;
}
init_factorization(m_factorization, m_A, m_basis, m_settings);
m_iters_with_no_cost_growing++;
if (m_factorization->get_status() != LU_status::OK) {
std::stringstream s;
// s << "failing refactor on off_result for entering = " << entering << ", leaving = " << leaving << " total_iterations = " << total_iterations();
m_status = lp_status::FLOATING_POINT_ERROR;
return false;
}
return false;
}
}
}
bool refactor = m_factorization->need_to_refactor();
if (!refactor) {
const T & pivot = this->m_pivot_row[entering]; // m_ed[m_factorization->basis_heading(leaving)] is the same but the one that we are using is more precise
m_factorization->replace_column(pivot, m_w, m_basis_heading[leaving]);
if (m_factorization->get_status() == LU_status::OK) {
change_basis(entering, leaving);
return true;
}
}
// need to refactor == true
change_basis(entering, leaving);
init_lu();
if (m_factorization->get_status() != LU_status::OK) {
if (m_look_for_feasible_solution_only && !precise()) {
m_status = lp_status::UNSTABLE;
delete m_factorization;
m_factorization = nullptr;
return false;
}
// LP_OUT(m_settings, "failing refactor for entering = " << entering << ", leaving = " << leaving << " total_iterations = " << total_iterations() << std::endl);
restore_x_and_refactor(entering, leaving, tt);
if (m_status == lp_status::FLOATING_POINT_ERROR)
return false;
CASSERT("A_off", !A_mult_x_is_off());
m_iters_with_no_cost_growing++;
// LP_OUT(m_settings, "rolled back after failing of init_factorization()" << std::endl);
m_status = lp_status::UNSTABLE;
return false;
}
return true;
}
template <typename T, typename X> bool lp_core_solver_base<T, X>::
divide_row_by_pivot(unsigned pivot_row, unsigned pivot_col) {

28
src/math/lp/lp_dual_core_solver_def.h
View file

@ -411,33 +411,7 @@ template <typename T, typename X> void lp_dual_core_solver<T, X>::init_betas_pre
// step 7 of the algorithm from Progress
template <typename T, typename X> bool lp_dual_core_solver<T, X>::basis_change_and_update() {
update_betas();
update_d_and_xB();
// m_theta_P = m_delta / this->m_ed[m_r];
m_theta_P = m_delta / this->m_pivot_row[m_q];
// xb_minus_delta_p_pivot_column();
apply_flips();
if (!this->update_basis_and_x(m_q, m_p, m_theta_P)) {
init_betas_precisely();
return false;
}
if (snap_runaway_nonbasic_column(m_p)) {
if (!this->find_x_by_solving()) {
revert_to_previous_basis();
this->iters_with_no_cost_growing()++;
return false;
}
}
if (!problem_is_dual_feasible()) {
// todo : shift the costs!!!!
revert_to_previous_basis();
this->iters_with_no_cost_growing()++;
return false;
}
lp_assert(d_is_correct());
return true;
}

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

@ -552,9 +552,9 @@ public:
void clear_breakpoints();
void change_slope_on_breakpoint(unsigned entering, breakpoint<X> * b, T & slope_at_entering);
void advance_on_sorted_breakpoints(unsigned entering);
void update_basis_and_x_with_comparison(unsigned entering, unsigned leaving, X delta);
void decide_on_status_when_cannot_find_entering() {
lp_assert(!need_to_switch_costs());

6
src/math/lp/lp_primal_core_solver_def.h
View file

@ -855,12 +855,6 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::one_iteratio
}
}
template <typename T, typename X> void lp_primal_core_solver<T, X>::update_basis_and_x_with_comparison(unsigned entering, unsigned leaving, X delta) {
if (entering != leaving)
this->update_basis_and_x(entering, leaving, delta);
else
this->update_x(entering, delta);
}
template <typename T, typename X> void lp_primal_core_solver<T, X>::clear_breakpoints() {