mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

fix build warnings part 6

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-05-11 08:57:17 -07:00
parent f176e1e5e5
commit 49d2b86d35
6 changed files with 56 additions and 55 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

56
src/util/lp/lp_core_solver_base.h
View file

@ -28,37 +28,37 @@ public:
bool m_using_infeas_costs;
vector<unsigned> m_columns_nz; // m_columns_nz[i] keeps an approximate value of non zeroes the i-th column
vector<unsigned> m_rows_nz; // m_rows_nz[i] keeps an approximate value of non zeroes in the i-th row
indexed_vector<T> m_pivot_row_of_B_1; // the pivot row of the reverse of B
indexed_vector<T> m_pivot_row; // this is the real pivot row of the simplex tableu
vector<unsigned> m_columns_nz; // m_columns_nz[i] keeps an approximate value of non zeroes the i-th column
vector<unsigned> m_rows_nz; // m_rows_nz[i] keeps an approximate value of non zeroes in the i-th row
indexed_vector<T> m_pivot_row_of_B_1; // the pivot row of the reverse of B
indexed_vector<T> m_pivot_row; // this is the real pivot row of the simplex tableu
static_matrix<T, X> & m_A; // the matrix A
vector<X> & m_b; // the right side
vector<unsigned> & m_basis;
vector<unsigned>& m_nbasis;
vector<int>& m_basis_heading;
vector<X> & m_x; // a feasible solution, the fist time set in the constructor
vector<T> & m_costs;
lp_settings & m_settings;
vector<T> m_y; // the buffer for yB = cb
vector<X> & m_b; // the right side
vector<unsigned> & m_basis;
vector<unsigned>& m_nbasis;
vector<int>& m_basis_heading;
vector<X> & m_x; // a feasible solution, the fist time set in the constructor
vector<T> & m_costs;
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
lu<T, X> * m_factorization;
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
unsigned m_iters_with_no_cost_growing;
lu<T, X> * m_factorization;
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
unsigned m_iters_with_no_cost_growing;
const vector<column_type> & m_column_types;
const vector<X> & m_low_bounds;
const vector<X> & m_upper_bounds;
vector<T> m_column_norms; // the approximate squares of column norms that help choosing a profitable column
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;
int_set* m_pivoted_rows;
bool m_look_for_feasible_solution_only;
const vector<X> & m_low_bounds;
const vector<X> & m_upper_bounds;
vector<T> m_column_norms; // the approximate squares of column norms that help choosing a profitable column
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;
int_set* m_pivoted_rows;
bool m_look_for_feasible_solution_only;
void start_tracing_basis_changes() {
m_trace_of_basis_change_vector.resize(0);
m_tracing_basis_changes = true;

11
src/util/lp/lp_core_solver_base.hpp
View file

@ -24,6 +24,7 @@ lp_core_solver_base(static_matrix<T, X> & A,
const vector<X> & upper_bound_values):
m_status(FEASIBLE),
m_inf_set(A.column_count()),
m_using_infeas_costs(false),
m_pivot_row_of_B_1(A.row_count()),
m_pivot_row(A.column_count()),
m_A(A),
@ -45,14 +46,14 @@ lp_core_solver_base(static_matrix<T, X> & A,
m_upper_bounds(upper_bound_values),
m_column_norms(m_n()),
m_copy_of_xB(m_m()),
m_steepest_edge_coefficients(A.column_count()),
m_total_iterations(0),
m_using_infeas_costs(false),
m_iters_with_no_cost_growing(0),
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) {
m_look_for_feasible_solution_only(false),
m_total_iterations(0),
m_iters_with_no_cost_growing(0)
{
lean_assert(bounds_for_boxed_are_set_correctly());
init();
init_basis_heading_and_non_basic_columns_vector();

24
src/util/lp/lu.h
View file

@ -113,22 +113,22 @@ class lu {
LU_status m_status;
public:
// the fields
unsigned m_dim;
unsigned m_dim;
static_matrix<T, X> const &m_A;
permutation_matrix<T, X> m_Q;
permutation_matrix<T, X> m_R;
permutation_matrix<T, X> m_r_wave;
sparse_matrix<T, X> m_U;
permutation_matrix<T, X> m_Q;
permutation_matrix<T, X> m_R;
permutation_matrix<T, X> m_r_wave;
sparse_matrix<T, X> m_U;
square_dense_submatrix<T, X>* m_dense_LU;
vector<tail_matrix<T, X> *> m_tail;
lp_settings & m_settings;
bool m_failure;
indexed_vector<T> m_row_eta_work_vector;
indexed_vector<T> m_w_for_extension;
indexed_vector<T> m_y_copy;
indexed_vector<unsigned> m_ii; //to optimize the work with the m_index fields
unsigned m_refactor_counter;
lp_settings & m_settings;
bool m_failure;
indexed_vector<T> m_row_eta_work_vector;
indexed_vector<T> m_w_for_extension;
indexed_vector<T> m_y_copy;
indexed_vector<unsigned> m_ii; //to optimize the work with the m_index fields
unsigned m_refactor_counter;
// constructor
// if A is an m by n matrix then basis has length m and values in [0,n); the values are all different
// they represent the set of m columns

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

@ -111,6 +111,7 @@ template <typename T, typename X>
lu<T, X>::lu(static_matrix<T, X> const & A,
vector<unsigned>& basis,
lp_settings & settings):
m_status(LU_status::OK),
m_dim(A.row_count()),
m_A(A),
m_Q(m_dim),
@ -118,9 +119,8 @@ lu<T, X>::lu(static_matrix<T, X> const & A,
m_r_wave(m_dim),
m_U(A, basis), // create the square matrix that eventually will be factorized
m_settings(settings),
m_row_eta_work_vector(A.row_count()),
m_status(LU_status::OK),
m_failure(false),
m_row_eta_work_vector(A.row_count()),
m_refactor_counter(0) {
lean_assert(!(numeric_traits<T>::precise() && settings.use_tableau()));
#ifdef LEAN_DEBUG

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

@ -44,17 +44,17 @@ class sparse_matrix
}
};
unsigned m_n_of_active_elems;
unsigned m_n_of_active_elems;
binary_heap_upair_queue<unsigned> m_pivot_queue;
public:
vector<vector<indexed_value<T>>> m_rows;
vector<col_header> m_columns;
permutation_matrix<T, X> m_row_permutation;
permutation_matrix<T, X> m_column_permutation;
vector<col_header> m_columns;
permutation_matrix<T, X> m_row_permutation;
permutation_matrix<T, X> m_column_permutation;
// m_work_pivot_vector[j] = offset of elementh of j-th column in the row we are pivoting to
// if the column is not present then m_work_pivot_vector[j] is -1
vector<int> m_work_pivot_vector;
vector<bool> m_processed;
vector<int> m_work_pivot_vector;
vector<bool> m_processed;
unsigned get_n_of_active_elems() const { return m_n_of_active_elems; }
#ifdef LEAN_DEBUG

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

@ -36,12 +36,12 @@ void sparse_matrix<T, X>::copy_B(static_matrix<T, X> const &A, vector<unsigned>
// constructor that copies columns of the basis from A
template <typename T, typename X>
sparse_matrix<T, X>::sparse_matrix(static_matrix<T, X> const &A, vector<unsigned> & basis) :
m_n_of_active_elems(0),
m_pivot_queue(A.row_count()),
m_row_permutation(A.row_count()),
m_column_permutation(A.row_count()),
m_work_pivot_vector(A.row_count(), -1),
m_processed(A.row_count()),
m_n_of_active_elems(0) {
m_processed(A.row_count()) {
init_row_headers();
init_column_headers();
copy_B(A, basis);