mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

rm dead code

Browse source
This commit is contained in:
Lev Nachmanson 2023-03-06 15:35:54 -08:00
parent f33f8c265e
commit 569f5be91f
5 changed files with 7 additions and 135 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -86,21 +86,18 @@ public:
lp_settings & m_settings;
vector<T> m_y; // the buffer for yB = cb
// a device that is able to solve Bx=c, xB=d, and change the basis
const column_namer & m_column_names;
indexed_vector<T> m_w; // the vector featuring in 24.3 of the Chvatal book
vector<T> m_d; // the vector of reduced costs
indexed_vector<T> m_ed; // the solution of B*m_ed = a
const vector<column_type> & m_column_types;
const vector<X> & m_lower_bounds;
const vector<X> & m_upper_bounds;
vector<T> m_column_norms; // the approximate squares of column norms that help choosing a profitable column
const vector<X> & m_upper_bounds;
vector<X> m_copy_of_xB;
unsigned m_basis_sort_counter;
vector<T> m_steepest_edge_coefficients;
vector<unsigned> m_trace_of_basis_change_vector; // the even positions are entering, the odd positions are leaving
bool m_tracing_basis_changes;
u_set* m_pivoted_rows;
u_set* m_pivoted_rows;
bool m_look_for_feasible_solution_only;
void start_tracing_basis_changes() {

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

@ -62,10 +62,8 @@ lp_core_solver_base(static_matrix<T, X> & A,
m_column_types(column_types),
m_lower_bounds(lower_bound_values),
m_upper_bounds(upper_bound_values),
m_column_norms(m_n()),
m_copy_of_xB(m_m()),
m_basis_sort_counter(0),
m_steepest_edge_coefficients(A.column_count()),
m_tracing_basis_changes(false),
m_pivoted_rows(nullptr),
m_look_for_feasible_solution_only(false) {

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

@ -369,24 +369,12 @@ public:
unsigned get_number_of_non_basic_column_to_try_for_enter();
void print_column_norms(std::ostream & out);
// returns the number of iterations
unsigned solve();
// according to Swietanowski, " A new steepest edge approximation for the simplex method for linear programming"
void init_column_norms();
T calculate_column_norm_exactly(unsigned j);
void update_or_init_column_norms(unsigned entering, unsigned leaving);
// following Swietanowski - A new steepest ...
void update_column_norms(unsigned entering, unsigned leaving);
T calculate_norm_of_entering_exactly();
void find_feasible_solution();
// bool is_tiny() const {return this->m_m < 10 && this->m_n < 20;}

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

@ -58,14 +58,8 @@ void lp_primal_core_solver<T, X>::sort_non_basis() {
sort_non_basis_rational();
return;
}
for (unsigned j : this->m_nbasis) {
T const & da = this->m_d[j];
this->m_steepest_edge_coefficients[j] = da * da / this->m_column_norms[j];
}
std::sort(this->m_nbasis.begin(), this->m_nbasis.end(), [this](unsigned a, unsigned b) {
return this->m_steepest_edge_coefficients[a] > this->m_steepest_edge_coefficients[b];
});
m_non_basis_list.clear();
// reinit m_basis_heading
for (unsigned j = 0; j < this->m_nbasis.size(); j++) {
@ -190,41 +184,7 @@ int lp_primal_core_solver<T, X>::choose_entering_column_presize(unsigned number_
template <typename T, typename X>
int lp_primal_core_solver<T, X>::choose_entering_column(unsigned number_of_benefitial_columns_to_go_over) { // at this moment m_y = cB * B(-1)
if (numeric_traits<T>::precise())
return choose_entering_column_presize(number_of_benefitial_columns_to_go_over);
if (number_of_benefitial_columns_to_go_over == 0)
return -1;
if (this->m_basis_sort_counter == 0) {
sort_non_basis();
this->m_basis_sort_counter = 20;
} else {
this->m_basis_sort_counter--;
}
T steepest_edge = zero_of_type<T>();
std::list<unsigned>::iterator entering_iter = m_non_basis_list.end();
for (auto non_basis_iter= m_non_basis_list.begin(); number_of_benefitial_columns_to_go_over && non_basis_iter != m_non_basis_list.end(); ++non_basis_iter) {
unsigned j = *non_basis_iter;
if (!column_is_benefitial_for_entering_basis(j))
continue;
// if we are here then j is a candidate to enter the basis
T dj = this->m_d[j];
T t = dj * dj / this->m_column_norms[j];
if (t > steepest_edge) {
steepest_edge = t;
entering_iter = non_basis_iter;
if (number_of_benefitial_columns_to_go_over)
number_of_benefitial_columns_to_go_over--;
}
}// while (number_of_benefitial_columns_to_go_over && initial_offset_in_non_basis != offset_in_nb);
if (entering_iter != m_non_basis_list.end()) {
unsigned entering = *entering_iter;
m_sign_of_entering_delta = this->m_d[entering] > 0? 1 : -1;
m_non_basis_list.erase(entering_iter);
m_non_basis_list.push_back(entering);
return entering;
}
return -1;
return choose_entering_column_presize(number_of_benefitial_columns_to_go_over);
}
@ -607,13 +567,6 @@ template <typename T, typename X> unsigned lp_primal_core_solver<T, X>::get_num
return std::max(static_cast<unsigned>(this->m_settings.random_next() % ret), 1u);
}
template <typename T, typename X> void lp_primal_core_solver<T, X>::print_column_norms(std::ostream & out) {
out << " column norms " << std::endl;
for (unsigned j = 0; j < this->m_n(); j++) {
out << this->m_column_norms[j] << " ";
}
out << std::endl;
}
// returns the number of iterations
template <typename T, typename X> unsigned lp_primal_core_solver<T, X>::solve() {
@ -677,67 +630,6 @@ template <typename T, typename X> unsigned lp_primal_core_solver<T, X>::solve()
return this->total_iterations();
}
// according to Swietanowski, " A new steepest edge approximation for the simplex method for linear programming"
template <typename T, typename X> void lp_primal_core_solver<T, X>::init_column_norms() {
lp_assert(numeric_traits<T>::precise() == false);
for (unsigned j = 0; j < this->m_n(); j++) {
this->m_column_norms[j] = T(static_cast<int>(this->m_A.m_columns[j].size() + 1))
+ T(static_cast<int>(this->m_settings.random_next() % 10000)) / T(100000);
}
}
// debug only
template <typename T, typename X> T lp_primal_core_solver<T, X>::calculate_column_norm_exactly(unsigned j) {
lp_assert(false);
}
template <typename T, typename X> void lp_primal_core_solver<T, X>::update_or_init_column_norms(unsigned entering, unsigned leaving) {
lp_assert(numeric_traits<T>::precise() == false);
lp_assert(m_column_norm_update_counter <= this->m_settings.column_norms_update_frequency);
if (m_column_norm_update_counter == this->m_settings.column_norms_update_frequency) {
m_column_norm_update_counter = 0;
init_column_norms();
} else {
m_column_norm_update_counter++;
update_column_norms(entering, leaving);
}
}
// following Swietanowski - A new steepest ...
template <typename T, typename X> void lp_primal_core_solver<T, X>::update_column_norms(unsigned entering, unsigned leaving) {
lp_assert(numeric_traits<T>::precise() == false);
T pivot = this->m_pivot_row[entering];
T g_ent = calculate_norm_of_entering_exactly() / pivot / pivot;
if (!numeric_traits<T>::precise()) {
if (g_ent < T(0.000001))
g_ent = T(0.000001);
}
this->m_column_norms[leaving] = g_ent;
for (unsigned j : this->m_pivot_row.m_index) {
if (j == leaving)
continue;
const T & t = this->m_pivot_row[j];
T s = this->m_A.dot_product_with_column(m_beta.m_data, j);
T k = -2 / pivot;
T tp = t/pivot;
if (this->m_column_types[j] != column_type::fixed) { // a fixed columns do not enter the basis, we don't use the norm of a fixed column
this->m_column_norms[j] = std::max(this->m_column_norms[j] + t * (t * g_ent + k * s), // see Istvan Maros, page 196
1 + tp * tp);
}
}
}
template <typename T, typename X> T lp_primal_core_solver<T, X>::calculate_norm_of_entering_exactly() {
T r = numeric_traits<T>::one();
for (auto i : this->m_ed.m_index) {
T t = this->m_ed[i];
r += t * t;
}
return r;
}
// calling it stage1 is too cryptic
template <typename T, typename X> void lp_primal_core_solver<T, X>::find_feasible_solution() {
this->m_look_for_feasible_solution_only = true;

5
src/math/lp/lp_primal_core_solver_tableau_def.h
View file

@ -295,10 +295,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::init_run_tab
if (this->m_settings.backup_costs)
backup_and_normalize_costs();
m_epsilon_of_reduced_cost = numeric_traits<X>::precise() ? zero_of_type<T>() : T(1) / T(10000000);
if (!numeric_traits<X>::precise()) {
this->m_column_norm_update_counter = 0;
init_column_norms();
}
if (this->m_settings.simplex_strategy() == simplex_strategy_enum::tableau_rows)
init_tableau_rows();
lp_assert(this->reduced_costs_are_correct_tableau());