mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

Merge pull request #1018 from levnach/master

Browse source 
fix init reorder warning
This commit is contained in:
Nikolaj Bjorner 2017-05-11 10:58:59 -07:00 • committed by GitHub
commit df1f7ee5e0
9 changed files with 38 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_lra.cpp
View file

@ -656,8 +656,8 @@ namespace smt {
m_asserted_qhead(0),
m_assume_eq_head(0),
m_num_conflicts(0),
m_solver(0),
m_model_eqs(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)),
m_solver(0),
m_resource_limit(*this) {
}

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

@ -18,6 +18,7 @@ namespace lean {
template <typename T, typename X> // X represents the type of the x variable and the bounds
class lp_core_solver_base {
unsigned m_total_iterations;
unsigned m_iters_with_no_cost_growing;
unsigned inc_total_iterations() { ++m_settings.st().m_total_iterations; return m_total_iterations++; }
private:
lp_status m_status;
@ -47,7 +48,6 @@ public:
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;
@ -678,6 +678,13 @@ public:
lean_assert(is_zero(this->m_costs[j]));
}
return true;
}
}
unsigned & iters_with_no_cost_growing() {
return m_iters_with_no_cost_growing;
}
const unsigned & iters_with_no_cost_growing() const {
return m_iters_with_no_cost_growing;
}
};
}

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

@ -22,6 +22,8 @@ lp_core_solver_base(static_matrix<T, X> & A,
const vector<column_type> & column_types,
const vector<X> & low_bound_values,
const vector<X> & upper_bound_values):
m_total_iterations(0),
m_iters_with_no_cost_growing(0),
m_status(FEASIBLE),
m_inf_set(A.column_count()),
m_using_infeas_costs(false),
@ -50,10 +52,7 @@ lp_core_solver_base(static_matrix<T, X> & A,
m_steepest_edge_coefficients(A.column_count()),
m_tracing_basis_changes(false),
m_pivoted_rows(nullptr),
m_look_for_feasible_solution_only(false),
m_total_iterations(0),
m_iters_with_no_cost_growing(0)
{
m_look_for_feasible_solution_only(false) {
lean_assert(bounds_for_boxed_are_set_correctly());
init();
init_basis_heading_and_non_basic_columns_vector();

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

@ -429,7 +429,7 @@ template <typename T, typename X> bool lp_dual_core_solver<T, X>::basis_change_a
if (snap_runaway_nonbasic_column(m_p)) {
if (!this->find_x_by_solving()) {
revert_to_previous_basis();
this->m_iters_with_no_cost_growing++;
this->iters_with_no_cost_growing()++;
return false;
}
}
@ -437,7 +437,7 @@ template <typename T, typename X> bool lp_dual_core_solver<T, X>::basis_change_a
if (!problem_is_dual_feasible()) {
// todo : shift the costs!!!!
revert_to_previous_basis();
this->m_iters_with_no_cost_growing++;
this->iters_with_no_cost_growing()++;
return false;
}
@ -730,14 +730,14 @@ template <typename T, typename X> void lp_dual_core_solver<T, X>::solve() { // s
lean_assert(problem_is_dual_feasible());
lean_assert(this->basis_heading_is_correct());
this->set_total_iterations(0);
this->m_iters_with_no_cost_growing = 0;
this->iters_with_no_cost_growing() = 0;
do {
if (this->print_statistics_with_iterations_and_nonzeroes_and_cost_and_check_that_the_time_is_over("", *this->m_settings.get_message_ostream())){
return;
}
one_iteration();
} while (this->get_status() != FLOATING_POINT_ERROR && this->get_status() != DUAL_UNBOUNDED && this->get_status() != OPTIMAL &&
this->m_iters_with_no_cost_growing <= this->m_settings.max_number_of_iterations_with_no_improvements
this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements
&& this->total_iterations() <= this->m_settings.max_total_number_of_iterations);
}
}

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

@ -905,8 +905,8 @@ public:
column_type_array,
low_bound_values,
upper_bound_values),
m_epsilon_of_reduced_cost(T(1)/T(10000000)),
m_beta(A.row_count()),
m_epsilon_of_reduced_cost(T(1)/T(10000000)),
m_bland_mode_threshold(1000) {
if (!(numeric_traits<T>::precise())) {

16
src/util/lp/lp_primal_core_solver.hpp
View file

@ -628,7 +628,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::backup_an
template <typename T, typename X> void lp_primal_core_solver<T, X>::init_run() {
this->m_basis_sort_counter = 0; // to initiate the sort of the basis
this->set_total_iterations(0);
this->m_iters_with_no_cost_growing = 0;
this->iters_with_no_cost_growing() = 0;
init_inf_set();
if (this->current_x_is_feasible() && this->m_look_for_feasible_solution_only)
return;
@ -664,7 +664,7 @@ void lp_primal_core_solver<T, X>::advance_on_entering_equal_leaving(int entering
this->init_lu();
if (!this->find_x_by_solving()) {
this->restore_x(entering, t * m_sign_of_entering_delta);
this->m_iters_with_no_cost_growing++;
this->iters_with_no_cost_growing()++;
LP_OUT(this->m_settings, "failing in advance_on_entering_equal_leaving for entering = " << entering << std::endl);
return;
}
@ -679,7 +679,7 @@ void lp_primal_core_solver<T, X>::advance_on_entering_equal_leaving(int entering
if (need_to_switch_costs() ||!this->current_x_is_feasible()) {
init_reduced_costs();
}
this->m_iters_with_no_cost_growing = 0;
this->iters_with_no_cost_growing() = 0;
}
template <typename T, typename X>void lp_primal_core_solver<T, X>::advance_on_entering_and_leaving(int entering, int leaving, X & t) {
@ -699,14 +699,14 @@ template <typename T, typename X>void lp_primal_core_solver<T, X>::advance_on_en
if (!pivot_compare_result){;}
else if (pivot_compare_result == 2) { // the sign is changed, cannot continue
this->set_status(UNSTABLE);
this->m_iters_with_no_cost_growing++;
this->iters_with_no_cost_growing()++;
return;
} else {
lean_assert(pivot_compare_result == 1);
this->init_lu();
if (this->m_factorization == nullptr || this->m_factorization->get_status() != LU_status::OK) {
this->set_status(UNSTABLE);
this->m_iters_with_no_cost_growing++;
this->iters_with_no_cost_growing()++;
return;
}
}
@ -728,7 +728,7 @@ template <typename T, typename X>void lp_primal_core_solver<T, X>::advance_on_en
}
if (!is_zero(t)) {
this->m_iters_with_no_cost_growing = 0;
this->iters_with_no_cost_growing() = 0;
init_infeasibility_after_update_x_if_inf(leaving);
}
@ -783,7 +783,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::advance_on_e
this->init_lu();
init_reduced_costs();
if (refresh_result == 2) {
this->m_iters_with_no_cost_growing++;
this->iters_with_no_cost_growing()++;
return;
}
}
@ -934,7 +934,7 @@ template <typename T, typename X> unsigned lp_primal_core_solver<T, X>::solve()
&&
this->get_status() != INFEASIBLE
&&
this->m_iters_with_no_cost_growing <= this->m_settings.max_number_of_iterations_with_no_improvements
this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements
&&
this->total_iterations() <= this->m_settings.max_total_number_of_iterations
&&

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

@ -169,7 +169,7 @@ unsigned lp_primal_core_solver<T, X>::solve_with_tableau() {
&&
this->get_status() != INFEASIBLE
&&
this->m_iters_with_no_cost_growing <= this->m_settings.max_number_of_iterations_with_no_improvements
this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements
&&
this->total_iterations() <= this->m_settings.max_total_number_of_iterations
&&
@ -202,7 +202,7 @@ template <typename T, typename X>void lp_primal_core_solver<T, X>::advance_on_en
}
this->update_basis_and_x_tableau(entering, leaving, t);
lean_assert(this->A_mult_x_is_off() == false);
this->m_iters_with_no_cost_growing = 0;
this->iters_with_no_cost_growing() = 0;
} else {
this->pivot_column_tableau(entering, this->m_basis_heading[leaving]);
this->change_basis(entering, leaving);
@ -233,7 +233,7 @@ void lp_primal_core_solver<T, X>::advance_on_entering_equal_leaving_tableau(int
if (need_to_switch_costs()) {
init_reduced_costs_tableau();
}
this->m_iters_with_no_cost_growing = 0;
this->iters_with_no_cost_growing() = 0;
}
template <typename T, typename X> int lp_primal_core_solver<T, X>::find_leaving_and_t_tableau(unsigned entering, X & t) {
unsigned k = 0;
@ -302,7 +302,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::init_run_tab
lean_assert(basis_columns_are_set_correctly());
this->m_basis_sort_counter = 0; // to initiate the sort of the basis
this->set_total_iterations(0);
this->m_iters_with_no_cost_growing = 0;
this->iters_with_no_cost_growing() = 0;
lean_assert(this->inf_set_is_correct());
if (this->current_x_is_feasible() && this->m_look_for_feasible_solution_only)
return;

11
src/util/lp/mps_reader.h
View file

@ -122,12 +122,15 @@ class mps_reader {
row_type m_type;
std::string m_name;
std::unordered_map<std::string, T> m_row_columns;
T m_right_side;
unsigned m_index;
T m_right_side;
T m_range;
row(row_type type, std::string name, unsigned index) : m_type(type), m_name(name), m_index(index),
m_right_side(zero_of_type<T>()),
m_range(zero_of_type<T>())
row(row_type type, std::string name, unsigned index) :
m_type(type),
m_name(name),
m_index(index),
m_right_side(zero_of_type<T>()),
m_range(zero_of_type<T>())
{
}
};

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

@ -16,7 +16,6 @@ namespace lean {
template <typename T> struct numeric_pair; // forward definition
class lar_core_solver; // forward definition
class random_updater {
unsigned range ;
struct interval {
bool upper_bound_is_set;
numeric_pair<mpq> upper_bound;
@ -61,6 +60,7 @@ class random_updater {
};
std::set<var_index> m_var_set;
lar_core_solver & m_core_solver;
unsigned range;
linear_combination_iterator<mpq>* m_column_j; // the actual column
interval find_shift_interval(unsigned j);
interval get_interval_of_non_basic_var(unsigned j);