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-06 07:56:04 -08:00
parent 1da4c018e4
commit bfe73c01a6
6 changed files with 1 additions and 110 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -274,47 +274,6 @@ public:
}
void prepare_solver_x_with_signature_tableau(const lar_solution_signature & signature) {
lp_assert(m_r_solver.inf_set_is_correct());
for (auto &t : signature) {
unsigned j = t.first;
if (m_r_heading[j] >= 0)
continue;
auto pos_type = t.second;
numeric_pair<mpq> delta;
if (!update_xj_and_get_delta(j, pos_type, delta))
continue;
for (const auto & cc : m_r_solver.m_A.m_columns[j]){
unsigned i = cc.var();
unsigned jb = m_r_solver.m_basis[i];
m_r_solver.add_delta_to_x_and_track_feasibility(jb, - delta * m_r_solver.m_A.get_val(cc));
}
}
lp_assert(m_r_solver.inf_set_is_correct());
}
bool adjust_x_of_column(unsigned j) {
/*
if (m_r_solver.m_basis_heading[j] >= 0) {
return false;
}
if (m_r_solver.column_is_feasible(j)) {
return false;
}
m_r_solver.snap_column_to_bound_tableau(j);
lp_assert(m_r_solver.column_is_feasible(j));
m_r_solver.m_inf_set.erase(j);
*/
lp_assert(false);
return true;
}
bool r_basis_is_OK() const {
#ifdef Z3DEBUG

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

@ -643,11 +643,6 @@ namespace lp {
bool lar_solver::use_tableau_costs() const {
return m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs;
}
void lar_solver::adjust_x_of_column(unsigned j) {
lp_assert(false);
}
bool lar_solver::row_is_correct(unsigned i) const {
numeric_pair<mpq> r = zero_of_type<numeric_pair<mpq>>();
for (const auto& c : A_r().m_rows[i]) {

1
src/math/lp/lar_solver.h
View file

@ -210,7 +210,6 @@ class lar_solver : public column_namer {
void detect_rows_of_bound_change_column_for_nbasic_column_tableau(unsigned j);
bool use_tableau_costs() const;
void detect_rows_of_column_with_bound_change(unsigned j);
void adjust_x_of_column(unsigned j);
bool tableau_with_costs() const;
bool costs_are_used() const;
void change_basic_columns_dependend_on_a_given_nb_column(unsigned j, const numeric_pair<mpq> & delta);

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

@ -24,7 +24,6 @@ Revision History:
#include <functional>
#include "math/lp/lp_core_solver_base_def.h"
template bool lp::lp_core_solver_base<double, double>::basis_heading_is_correct() const;
template void lp::lp_core_solver_base<double, double>::calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned);
template bool lp::lp_core_solver_base<double, double>::column_is_dual_feasible(unsigned int) const;
template void lp::lp_core_solver_base<double, double>::fill_reduced_costs_from_m_y_by_rows();
template lp::non_basic_column_value_position lp::lp_core_solver_base<double, double>::get_non_basic_column_value_position(unsigned int) const;
@ -44,12 +43,9 @@ template bool lp::lp_core_solver_base<double, double>::print_statistics_with_ite
template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::print_statistics_with_iterations_and_nonzeroes_and_cost_and_check_that_the_time_is_over(char const*, std::ostream &);
template void lp::lp_core_solver_base<double, double>::restore_x(unsigned int, double const&);
template void lp::lp_core_solver_base<double, double>::set_non_basic_x_to_correct_bounds();
template void lp::lp_core_solver_base<double, double>::snap_xN_to_bounds_and_free_columns_to_zeroes();
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>::add_delta_to_entering(unsigned int, const double&);
template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::basis_heading_is_correct() const ;
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned);
template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::column_is_dual_feasible(unsigned int) const;
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::fill_reduced_costs_from_m_y_by_rows();
template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::print_statistics_with_iterations_and_nonzeroes_and_cost_and_check_that_the_time_is_over(char const*, std::ostream &);
@ -57,7 +53,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>::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();
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::init_basis_heading_and_non_basic_columns_vector();
template lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::lp_core_solver_base(lp::static_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >&,
@ -85,18 +80,10 @@ template lp::lp_core_solver_base<lp::mpq, lp::mpq>::lp_core_solver_base(
template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::print_statistics_with_iterations_and_check_that_the_time_is_over(std::ostream &);
template std::string lp::lp_core_solver_base<double, double>::column_name(unsigned int) const;
template void lp::lp_core_solver_base<double, double>::pretty_print(std::ostream & out);
template void lp::lp_core_solver_base<double, double>::restore_state(double*, double*);
template void lp::lp_core_solver_base<double, double>::save_state(double*, double*);
template std::string lp::lp_core_solver_base<lp::mpq, lp::mpq>::column_name(unsigned int) const;
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::pretty_print(std::ostream & out);
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::restore_state(lp::mpq*, lp::mpq*);
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::save_state(lp::mpq*, lp::mpq*);
template std::string lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::column_name(unsigned int) const;
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::pretty_print(std::ostream & out);
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::restore_state(lp::mpq*, lp::mpq*);
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::save_state(lp::mpq*, lp::mpq*);
template void lp::lp_core_solver_base<double, double>::init_lu();
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::init_lu();
template int lp::lp_core_solver_base<double, double>::pivots_in_column_and_row_are_different(int, int) const;
template int lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::pivots_in_column_and_row_are_different(int, int) const;
template int lp::lp_core_solver_base<lp::mpq, lp::mpq>::pivots_in_column_and_row_are_different(int, int) const;
@ -109,7 +96,6 @@ template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::column_is_feasible(unsi
// template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::print_linear_combination_of_column_indices(vector<std::pair<lp::mpq, unsigned int>, std::allocator<std::pair<lp::mpq, unsigned int> > > const&, std::ostream&) const;
template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::column_is_feasible(unsigned int) const;
template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::snap_non_basic_x_to_bound();
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::init_lu();
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::restore_x(unsigned int, lp::numeric_pair<lp::mpq> const&);
template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq>>::pivot_column_tableau(unsigned int, unsigned int);
template bool lp::lp_core_solver_base<double, double>::pivot_column_tableau(unsigned int, unsigned int);

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

@ -156,10 +156,6 @@ public:
void pretty_print(std::ostream & out);
void save_state(T * w_buffer, T * d_buffer);
void restore_state(T * w_buffer, T * d_buffer);
X get_cost() const {
return dot_product(m_costs, m_x);
}
@ -173,8 +169,6 @@ public:
void restore_m_ed(T * buffer);
void calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned pivot_row);
void add_delta_to_entering(unsigned entering, const X & delta);
const X & get_var_value(unsigned j) const {
@ -422,11 +416,9 @@ public:
void snap_non_basic_x_to_bound_and_free_to_zeroes();
void snap_xN_to_bounds_and_fill_xB();
void snap_xN_to_bounds_and_free_columns_to_zeroes();
non_basic_column_value_position get_non_basic_column_value_position(unsigned j) const;
void init_lu();
int pivots_in_column_and_row_are_different(int entering, int leaving) const;
void pivot_fixed_vars_from_basis();
bool remove_from_basis(unsigned j);

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

@ -136,17 +136,6 @@ pretty_print(std::ostream & out) {
pp.print();
}
template <typename T, typename X> void lp_core_solver_base<T, X>::
save_state(T * w_buffer, T * d_buffer) {
copy_m_w(w_buffer);
copy_m_ed(d_buffer);
}
template <typename T, typename X> void lp_core_solver_base<T, X>::
restore_state(T * w_buffer, T * d_buffer) {
restore_m_w(w_buffer);
restore_m_ed(d_buffer);
}
template <typename T, typename X> void lp_core_solver_base<T, X>::
copy_m_w(T * buffer) {
@ -185,26 +174,6 @@ restore_m_ed(T * buffer) {
template <typename T, typename X> void lp_core_solver_base<T, X>::
calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned pivot_row) {
m_pivot_row.clear();
for (unsigned i : m_pivot_row_of_B_1.m_index) {
const T & pi_1 = m_pivot_row_of_B_1[i];
if (numeric_traits<T>::is_zero(pi_1)) {
continue;
}
for (auto & c : m_A.m_rows[i]) {
unsigned j = c.var();
if (m_basis_heading[j] < 0) {
m_pivot_row.add_value_at_index_with_drop_tolerance(j, c.coeff() * pi_1);
}
}
}
if (precise()) {
m_rows_nz[pivot_row] = m_pivot_row.m_index.size();
}
}
template <typename T, typename X> void lp_core_solver_base<T, X>::
add_delta_to_entering(unsigned entering, const X& delta) {
@ -631,11 +600,6 @@ snap_xN_to_bounds_and_fill_xB() {
solve_Ax_eq_b();
}
template <typename T, typename X> void lp_core_solver_base<T, X>::
snap_xN_to_bounds_and_free_columns_to_zeroes() {
snap_non_basic_x_to_bound_and_free_to_zeroes();
solve_Ax_eq_b();
}
template <typename T, typename X> non_basic_column_value_position lp_core_solver_base<T, X>::
@ -661,10 +625,6 @@ get_non_basic_column_value_position(unsigned j) const {
return at_lower_bound;
}
template <typename T, typename X> void lp_core_solver_base<T, X>::init_lu() {
init_factorization(this->m_factorization, this->m_A, this->m_basis, this->m_settings);
}
template <typename T, typename X> int lp_core_solver_base<T, X>::pivots_in_column_and_row_are_different(int entering, int leaving) const {
const T & column_p = this->m_ed[this->m_basis_heading[leaving]];
const T & row_p = this->m_pivot_row[entering];