mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

replace clp to clean

Browse source 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
This commit is contained in:
Lev Nachmanson 2017-07-10 11:30:08 -07:00
parent cc32e45471
commit 86ed01a63b
15 changed files with 33 additions and 36 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/util/lp/indexed_vector.h
View file

@ -86,7 +86,7 @@ public:
return m_data[i];
}
void clp_up() {
void clean_up() {
#if 0==1
for (unsigned k = 0; k < m_index.size(); k++) {
unsigned i = m_index[k];
@ -140,7 +140,7 @@ public:
}
}
void restore_index_and_clp_from_data() {
void restore_index_and_clean_from_data() {
m_index.resize(0);
for (unsigned i = 0; i < m_data.size(); i++) {
T & v = m_data[i];

17
src/util/lp/lar_solver.cpp
View file

@ -316,9 +316,6 @@ void lar_solver::fill_explanation_from_infeasible_column(vector<std::pair<mpq, c
unsigned lar_solver::get_total_iterations() const { return m_mpq_lar_core_solver.m_r_solver.total_iterations(); }
// see http://research.microsoft.com/projects/z3/smt07.pdf
// This method searches for a feasible solution with as many different values of variables, reverenced in vars, as it can find
// Attention, after a call to this method the non-basic variables don't necesserarly stick to their bounds anymore
vector<unsigned> lar_solver::get_list_of_all_var_indices() const {
vector<unsigned> ret;
for (unsigned j = 0; j < m_mpq_lar_core_solver.m_r_heading.size(); j++)
@ -338,7 +335,7 @@ void lar_solver::push() {
m_constraint_count.push();
}
void lar_solver::clp_large_elements_after_pop(unsigned n, int_set& set) {
void lar_solver::clean_large_elements_after_pop(unsigned n, int_set& set) {
vector<int> to_remove;
for (unsigned j: set.m_index)
if (j >= n)
@ -348,7 +345,7 @@ void lar_solver::clp_large_elements_after_pop(unsigned n, int_set& set) {
}
void lar_solver::shrink_inf_set_after_pop(unsigned n, int_set & set) {
clp_large_elements_after_pop(n, set);
clean_large_elements_after_pop(n, set);
set.resize(n);
}
@ -367,10 +364,10 @@ void lar_solver::pop(unsigned k) {
m_vars_to_ul_pairs.pop(k);
m_mpq_lar_core_solver.pop(k);
clp_large_elements_after_pop(n, m_columns_with_changed_bound);
clean_large_elements_after_pop(n, m_columns_with_changed_bound);
unsigned m = A_r().row_count();
clp_large_elements_after_pop(m, m_rows_with_changed_bounds);
clp_inf_set_of_r_solver_after_pop();
clean_large_elements_after_pop(m, m_rows_with_changed_bounds);
clean_inf_set_of_r_solver_after_pop();
lp_assert(m_settings.simplex_strategy() == simplex_strategy_enum::undecided ||
(!use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau());
@ -1346,9 +1343,9 @@ void lar_solver::pop_tableau() {
lp_assert(m_mpq_lar_core_solver.m_r_solver.basis_heading_is_correct());
}
void lar_solver::clp_inf_set_of_r_solver_after_pop() {
void lar_solver::clean_inf_set_of_r_solver_after_pop() {
vector<unsigned> became_feas;
clp_large_elements_after_pop(A_r().column_count(), m_mpq_lar_core_solver.m_r_solver.m_inf_set);
clean_large_elements_after_pop(A_r().column_count(), m_mpq_lar_core_solver.m_r_solver.m_inf_set);
std::unordered_set<unsigned> basic_columns_with_changed_cost;
auto inf_index_copy = m_mpq_lar_core_solver.m_r_solver.m_inf_set.m_index;
for (auto j: inf_index_copy) {

4
src/util/lp/lar_solver.h
View file

@ -222,7 +222,7 @@ public:
vector<unsigned> get_list_of_all_var_indices() const;
void push();
static void clp_large_elements_after_pop(unsigned n, int_set& set);
static void clean_large_elements_after_pop(unsigned n, int_set& set);
static void shrink_inf_set_after_pop(unsigned n, int_set & set);
@ -403,7 +403,7 @@ public:
void remove_last_column_from_basis_tableau(unsigned j);
void remove_column_from_tableau(unsigned j);
void pop_tableau();
void clp_inf_set_of_r_solver_after_pop();
void clean_inf_set_of_r_solver_after_pop();
void shrink_explanation_to_minimum(vector<std::pair<mpq, constraint_index>> & explanation) const;

2
src/util/lp/lp_dual_simplex.hpp
View file

@ -335,7 +335,7 @@ template <typename T, typename X> void lp_dual_simplex<T, X>::find_maximal_solut
this->flip_costs(); // do it for now, todo ( remove the flipping)
this->clpup();
this->cleanup();
if (this->m_status == INFEASIBLE) {
return;
}

2
src/util/lp/lp_primal_simplex.hpp
View file

@ -157,7 +157,7 @@ template <typename T, typename X> void lp_primal_simplex<T, X>::find_maximal_sol
return;
}
this->clpup();
this->cleanup();
this->fill_matrix_A_and_init_right_side();
if (this->m_status == lp_status::INFEASIBLE) {
return;

2
src/util/lp/lp_solver.h
View file

@ -205,7 +205,7 @@ protected:
unsigned try_to_remove_some_rows();
void clpup();
void cleanup();
void map_external_rows_to_core_solver_rows();

2
src/util/lp/lp_solver.hpp
View file

@ -381,7 +381,7 @@ template <typename T, typename X> unsigned lp_solver<T, X>::try_to_remove_some_r
return static_cast<unsigned>(rows_to_delete.size());
}
template <typename T, typename X> void lp_solver<T, X>::clpup() {
template <typename T, typename X> void lp_solver<T, X>::cleanup() {
int n = 0; // number of deleted rows
int d;
while ((d = try_to_remove_some_rows() > 0))

4
src/util/lp/lp_solver_instances.cpp
View file

@ -5,7 +5,7 @@
#include <string>
#include "util/lp/lp_solver.hpp"
template void lp::lp_solver<double, double>::add_constraint(lp::lp_relation, double, unsigned int);
template void lp::lp_solver<double, double>::clpup();
template void lp::lp_solver<double, double>::cleanup();
template void lp::lp_solver<double, double>::count_slacks_and_artificials();
template void lp::lp_solver<double, double>::fill_m_b();
template void lp::lp_solver<double, double>::fill_matrix_A_and_init_right_side();
@ -21,7 +21,7 @@ template void lp::lp_solver<double, double>::scale();
template void lp::lp_solver<double, double>::set_scaled_cost(unsigned int);
template lp::lp_solver<double, double>::~lp_solver();
template void lp::lp_solver<lp::mpq, lp::mpq>::add_constraint(lp::lp_relation, lp::mpq, unsigned int);
template void lp::lp_solver<lp::mpq, lp::mpq>::clpup();
template void lp::lp_solver<lp::mpq, lp::mpq>::cleanup();
template void lp::lp_solver<lp::mpq, lp::mpq>::count_slacks_and_artificials();
template void lp::lp_solver<lp::mpq, lp::mpq>::fill_m_b();
template void lp::lp_solver<lp::mpq, lp::mpq>::fill_matrix_A_and_init_right_side();

8
src/util/lp/lu.hpp
View file

@ -415,7 +415,7 @@ void lu<T, X>::solve_yB_with_error_check_indexed(indexed_vector<T> & y, const ve
solve_yB_indexed(y);
} else {
solve_yB(y.m_data);
y.restore_index_and_clp_from_data();
y.restore_index_and_clean_from_data();
}
return;
}
@ -429,7 +429,7 @@ void lu<T, X>::solve_yB_with_error_check_indexed(indexed_vector<T> & y, const ve
find_error_of_yB(m_y_copy.m_data, y.m_data, basis);
solve_yB(m_y_copy.m_data);
add_delta_to_solution(m_y_copy.m_data, y.m_data);
y.restore_index_and_clp_from_data();
y.restore_index_and_clean_from_data();
m_y_copy.clear_all();
} else {
find_error_of_yB_indexed(y, heading, settings); // this works with m_y_copy
@ -439,7 +439,7 @@ void lu<T, X>::solve_yB_with_error_check_indexed(indexed_vector<T> & y, const ve
lp_assert(m_y_copy.is_OK());
} else {
solve_yB_with_error_check(y.m_data, basis);
y.restore_index_and_clp_from_data();
y.restore_index_and_clean_from_data();
}
}
@ -894,7 +894,7 @@ void lu<T, X>::calculate_Lwave_Pwave_for_bump(unsigned replaced_column, unsigned
if (replaced_column < lowest_row_of_the_bump) {
diagonal_elem = m_row_eta_work_vector[lowest_row_of_the_bump];
// lp_assert(m_row_eta_work_vector.is_OK());
m_U.set_row_from_work_vector_and_clp_work_vector_not_adjusted(m_U.adjust_row(lowest_row_of_the_bump), m_row_eta_work_vector, m_settings);
m_U.set_row_from_work_vector_and_clean_work_vector_not_adjusted(m_U.adjust_row(lowest_row_of_the_bump), m_row_eta_work_vector, m_settings);
} else {
diagonal_elem = m_U(lowest_row_of_the_bump, lowest_row_of_the_bump); // todo - get it more efficiently
}

4
src/util/lp/sparse_matrix.h
View file

@ -190,13 +190,13 @@ public:
// set the max val as well
// returns false if the resulting row is all zeroes, and true otherwise
bool set_row_from_work_vector_and_clp_work_vector_not_adjusted(unsigned i0, indexed_vector<T> & work_vec,
bool set_row_from_work_vector_and_clean_work_vector_not_adjusted(unsigned i0, indexed_vector<T> & work_vec,
lp_settings & settings);
// set the max val as well
// returns false if the resulting row is all zeroes, and true otherwise
bool set_row_from_work_vector_and_clp_work_vector(unsigned i0);
bool set_row_from_work_vector_and_clean_work_vector(unsigned i0);
void remove_zero_elements_and_set_data_on_existing_elements(unsigned row);

8
src/util/lp/sparse_matrix.hpp
View file

@ -296,7 +296,7 @@ bool sparse_matrix<T, X>::pivot_row_to_row(unsigned i, const T& alpha, unsigned
}
// clp the work vector
// clean the work vector
for (unsigned k = 0; k < prev_size_i0; k++) {
m_work_pivot_vector[i0_row_vals[k].m_index] = -1;
}
@ -319,7 +319,7 @@ bool sparse_matrix<T, X>::pivot_row_to_row(unsigned i, const T& alpha, unsigned
// set the max val as well
// returns false if the resulting row is all zeroes, and true otherwise
template <typename T, typename X>
bool sparse_matrix<T, X>::set_row_from_work_vector_and_clp_work_vector_not_adjusted(unsigned i0, indexed_vector<T> & work_vec,
bool sparse_matrix<T, X>::set_row_from_work_vector_and_clean_work_vector_not_adjusted(unsigned i0, indexed_vector<T> & work_vec,
lp_settings & settings) {
remove_zero_elements_and_set_data_on_existing_elements_not_adjusted(i0, work_vec, settings);
// all non-zero elements in m_work_pivot_vector are new
@ -557,11 +557,11 @@ void sparse_matrix<T, X>::double_solve_U_y(indexed_vector<L>& y, const lp_settin
active_rows.clear();
solve_U_y_indexed_only(y_orig, settings, active_rows);
add_delta_to_solution(y_orig, y);
y.clp_up();
y.clean_up();
} else { // the dense version
solve_U_y(y_orig.m_data);
add_delta_to_solution(y_orig.m_data, y.m_data);
y.restore_index_and_clp_from_data();
y.restore_index_and_clean_from_data();
}
lp_assert(y.is_OK());
}

6
src/util/lp/sparse_matrix_instances.cpp
View file

@ -24,7 +24,7 @@ template void sparse_matrix<double, double>::remove_element(vector<indexed_value
template void sparse_matrix<double, double>::replace_column(unsigned int, indexed_vector<double>&, lp_settings&);
template void sparse_matrix<double, double>::set(unsigned int, unsigned int, double);
template void sparse_matrix<double, double>::set_max_in_row(vector<indexed_value<double> >&);
template bool sparse_matrix<double, double>::set_row_from_work_vector_and_clp_work_vector_not_adjusted(unsigned int, indexed_vector<double>&, lp_settings&);
template bool sparse_matrix<double, double>::set_row_from_work_vector_and_clean_work_vector_not_adjusted(unsigned int, indexed_vector<double>&, lp_settings&);
template bool sparse_matrix<double, double>::shorten_active_matrix(unsigned int, eta_matrix<double, double>*);
template void sparse_matrix<double, double>::solve_y_U(vector<double>&) const;
template sparse_matrix<double, double>::sparse_matrix(static_matrix<double, double> const&, vector<unsigned int>&);
@ -41,7 +41,7 @@ template void sparse_matrix<mpq, mpq>::prepare_for_factorization();
template void sparse_matrix<mpq, mpq>::remove_element(vector<indexed_value<mpq>> &, indexed_value<mpq>&);
template void sparse_matrix<mpq, mpq>::replace_column(unsigned int, indexed_vector<mpq>&, lp_settings&);
template void sparse_matrix<mpq, mpq>::set_max_in_row(vector<indexed_value<mpq>>&);
template bool sparse_matrix<mpq, mpq>::set_row_from_work_vector_and_clp_work_vector_not_adjusted(unsigned int, indexed_vector<mpq>&, lp_settings&);
template bool sparse_matrix<mpq, mpq>::set_row_from_work_vector_and_clean_work_vector_not_adjusted(unsigned int, indexed_vector<mpq>&, lp_settings&);
template bool sparse_matrix<mpq, mpq>::shorten_active_matrix(unsigned int, eta_matrix<mpq, mpq>*);
template void sparse_matrix<mpq, mpq>::solve_y_U(vector<mpq>&) const;
template sparse_matrix<mpq, mpq>::sparse_matrix(static_matrix<mpq, mpq> const&, vector<unsigned int>&);
@ -57,7 +57,7 @@ template void sparse_matrix<mpq, numeric_pair<mpq>>::prepare_for_factorizati
template void sparse_matrix<mpq, numeric_pair<mpq>>::remove_element(vector<indexed_value<mpq>>&, indexed_value<mpq>&);
template void sparse_matrix<mpq, numeric_pair<mpq>>::replace_column(unsigned int, indexed_vector<mpq>&, lp_settings&);
template void sparse_matrix<mpq, numeric_pair<mpq>>::set_max_in_row(vector<indexed_value<mpq>>&);
template bool sparse_matrix<mpq, numeric_pair<mpq>>::set_row_from_work_vector_and_clp_work_vector_not_adjusted(unsigned int, indexed_vector<mpq>&, lp_settings&);
template bool sparse_matrix<mpq, numeric_pair<mpq>>::set_row_from_work_vector_and_clean_work_vector_not_adjusted(unsigned int, indexed_vector<mpq>&, lp_settings&);
template bool sparse_matrix<mpq, numeric_pair<mpq>>::shorten_active_matrix(unsigned int, eta_matrix<mpq, numeric_pair<mpq> >*);
template void sparse_matrix<mpq, numeric_pair<mpq>>::solve_y_U(vector<mpq>&) const;
template sparse_matrix<mpq, numeric_pair<mpq>>::sparse_matrix(static_matrix<mpq, numeric_pair<mpq> > const&, vector<unsigned int>&);

2
src/util/lp/square_dense_submatrix.h
View file

@ -187,7 +187,7 @@ public:
}
}
}
m_work_vector.clp_up();
m_work_vector.clean_up();
lp_assert(m_work_vector.is_OK());
w = m_work_vector;
#endif

2
src/util/lp/static_matrix.h
View file

@ -193,7 +193,7 @@ public:
void scan_row_to_work_vector(unsigned i);
void clp_row_work_vector(unsigned i);
void clean_row_work_vector(unsigned i);
#ifdef LEAN_DEBUG

2
src/util/lp/static_matrix.hpp
View file

@ -61,7 +61,7 @@ template <typename T, typename X> bool static_matrix<T, X>::pivot_row_to_row_giv
}
}
// clp the work vector
// clean the work vector
for (unsigned k = 0; k < prev_size_ii; k++) {
m_vector_of_row_offsets[ii_row_vals[k].m_j] = -1;
}