mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 03:07:07 +00:00
Code Activity

track the set of integer variables that are not set to integer values

Browse source 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
This commit is contained in:
Lev Nachmanson 2017-07-21 21:09:51 -07:00
parent 64e542bd70
commit bd4fb22665
9 changed files with 66 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
src/util/lp/int_solver.cpp
View file

@ -21,7 +21,6 @@ void int_solver::fix_non_base_columns() {
return;
if (m_lar_solver->find_feasible_solution() == lp_status::INFEASIBLE)
failed();
init_inf_int_set();
lp_assert(is_feasible() && inf_int_set_is_correct());
}
@ -61,14 +60,22 @@ void int_solver::trace_inf_rows() const {
);
}
int_set& int_solver::inf_int_set() {
return m_lar_solver->m_inf_int_set;
}
const int_set& int_solver::inf_int_set() const {
return m_lar_solver->m_inf_int_set;
}
int int_solver::find_inf_int_base_column() {
if (m_inf_int_set.is_empty())
if (inf_int_set().is_empty())
return -1;
int j = find_inf_int_boxed_base_column_with_smallest_range();
if (j != -1)
return j;
unsigned k = settings().random_next() % m_inf_int_set.m_index.size();
return m_inf_int_set.m_index[k];
unsigned k = settings().random_next() % inf_int_set().m_index.size();
return inf_int_set().m_index[k];
}
int int_solver::find_inf_int_boxed_base_column_with_smallest_range() {
@ -79,7 +86,7 @@ int int_solver::find_inf_int_boxed_base_column_with_smallest_range() {
unsigned n = 0;
lar_core_solver & lcs = m_lar_solver->m_mpq_lar_core_solver;
for (int j : m_inf_int_set.m_index) {
for (int j : inf_int_set().m_index) {
lp_assert(is_base(j) && column_is_int_inf(j));
if (!is_boxed(j))
continue;
@ -331,7 +338,6 @@ lia_move int_solver::mk_gomory_cut(lar_term& t, mpq& k, explanation & expl) {
}
void int_solver::init_check_data() {
init_inf_int_set();
unsigned n = m_lar_solver->A_r().column_count();
m_old_values_set.resize(n);
m_old_values_data.resize(n);
@ -402,12 +408,13 @@ lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex) {
if ((++m_branch_cut_counter) % settings().m_int_branch_cut_threshold == 0) {
move_non_base_vars_to_bounds();
move_non_base_vars_to_bounds(); // todo track changed variables
lp_status st = m_lar_solver->find_feasible_solution();
if (st != lp_status::FEASIBLE && st != lp_status::OPTIMAL) {
return lia_move::give_up;
}
init_inf_int_set(); // todo - can we avoid this call?
lp_assert(inf_int_set_is_correct());
// init_inf_int_set(); // todo - can we avoid this call?
int j = find_inf_int_base_column();
if (j != -1) {
// setup the call for gomory cut
@ -862,7 +869,7 @@ void int_solver::display_column(std::ostream & out, unsigned j) const {
bool int_solver::inf_int_set_is_correct() const {
for (unsigned j = 0; j < m_lar_solver->A_r().column_count(); j++) {
if (m_inf_int_set.contains(j) != (is_int(j) && (!value_is_int(j))))
if (inf_int_set().contains(j) != (is_int(j) && (!value_is_int(j))))
return false;
}
return true;
@ -872,20 +879,11 @@ bool int_solver::column_is_int_inf(unsigned j) const {
return is_int(j) && (!value_is_int(j));
}
void int_solver::init_inf_int_set() {
m_inf_int_set.clear();
m_inf_int_set.resize(m_lar_solver->A_r().column_count());
for (unsigned j = 0; j < m_lar_solver->A_r().column_count(); j++) {
if (column_is_int_inf(j))
m_inf_int_set.insert(j);
}
}
void int_solver::update_column_in_int_inf_set(unsigned j) {
if (is_int(j) && (!value_is_int(j)))
m_inf_int_set.insert(j);
inf_int_set().insert(j);
else
m_inf_int_set.erase(j);
inf_int_set().erase(j);
}
bool int_solver::is_base(unsigned j) const {

5
src/util/lp/int_solver.h
View file

@ -34,13 +34,15 @@ public:
lar_solver *m_lar_solver;
int_set m_old_values_set;
vector<impq> m_old_values_data;
int_set m_inf_int_set;
unsigned m_branch_cut_counter;
linear_combination_iterator<mpq>* m_iter_on_gomory_row;
unsigned m_gomory_cut_inf_column;
bool m_found_free_var_in_gomory_row;
// methods
int_solver(lar_solver* lp);
int_set& inf_int_set();
const int_set& inf_int_set() const;
// main function to check that solution provided by lar_solver is valid for integral values,
// or provide a way of how it can be adjusted.
lia_move check(lar_term& t, mpq& k, explanation& ex);
@ -96,7 +98,6 @@ private:
const impq & get_value(unsigned j) const;
void display_column(std::ostream & out, unsigned j) const;
bool inf_int_set_is_correct() const;
void init_inf_int_set();
void update_column_in_int_inf_set(unsigned j);
bool column_is_int_inf(unsigned j) const;
void trace_inf_rows() const;

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

@ -30,7 +30,17 @@ void clear() {lp_assert(false); // not implemented
lar_solver::lar_solver() : m_status(lp_status::OPTIMAL),
m_infeasible_column_index(-1),
m_terms_start_index(1000000),
m_mpq_lar_core_solver(m_settings, *this)
m_mpq_lar_core_solver(m_settings, *this),
m_tracker_of_x_change([&](unsigned j, const impq & x){
if (!var_is_int(j)) {
lp_assert(m_inf_int_set.contains(j) == false);
return;
}
if (m_mpq_lar_core_solver.m_r_x[j].is_int())
m_inf_int_set.erase(j);
else
m_inf_int_set.insert(j);
})
{
}
@ -279,6 +289,10 @@ lp_status lar_solver::get_status() const { return m_status;}
void lar_solver::set_status(lp_status s) {m_status = s;}
bool lar_solver::has_int_var() const {
return m_mpq_lar_core_solver.m_r_solver.m_tracker_of_x_change != nullptr;
}
lp_status lar_solver::find_feasible_solution() {
m_settings.st().m_make_feasible++;
if (A_r().column_count() > m_settings.st().m_max_cols)
@ -288,6 +302,10 @@ lp_status lar_solver::find_feasible_solution() {
if (strategy_is_undecided())
decide_on_strategy_and_adjust_initial_state();
if (has_int_var()) {
m_inf_int_set.resize(A_r().column_count());
}
m_mpq_lar_core_solver.m_r_solver.m_look_for_feasible_solution_only = true;
return solve();
}
@ -1474,6 +1492,9 @@ var_index lar_solver::add_var(unsigned ext_j, bool is_int) {
m_columns_to_ul_pairs.push_back(ul_pair(static_cast<unsigned>(-1)));
add_non_basic_var_to_core_fields(ext_j, is_int);
lp_assert(sizes_are_correct());
if (is_int) {
m_mpq_lar_core_solver.m_r_solver.set_tracker_of_x(& m_tracker_of_x_change);
}
return i;
}

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

@ -68,7 +68,8 @@ public:
lar_core_solver m_mpq_lar_core_solver;
unsigned constraint_count() const;
const lar_base_constraint& get_constraint(unsigned ci) const;
std::function<void (unsigned, const impq&)> m_tracker_of_x_change;
int_set m_inf_int_set;
////////////////// methods ////////////////////////////////
static_matrix<mpq, numeric_pair<mpq>> & A_r();
static_matrix<mpq, numeric_pair<mpq>> const & A_r() const;
@ -473,5 +474,7 @@ public:
t.clear();
t = lar_term(pol_after_subs, v);
}
bool has_int_var() const;
};
}

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

@ -69,6 +69,12 @@ public:
bool m_tracing_basis_changes;
int_set* m_pivoted_rows;
bool m_look_for_feasible_solution_only;
std::function<void (unsigned, const X &)> * m_tracker_of_x_change;
void set_tracker_of_x(std::function<void (unsigned, const X&)>* tracker) {
m_tracker_of_x_change = tracker;
}
void start_tracing_basis_changes() {
m_trace_of_basis_change_vector.resize(0);
m_tracing_basis_changes = true;
@ -670,16 +676,20 @@ public:
void update_column_in_inf_set(unsigned j) {
if (column_is_feasible(j)) {
m_inf_set.erase(j);
remove_column_from_inf_set(j);
} else {
m_inf_set.insert(j);
insert_column_into_inf_set(j);
}
}
void insert_column_into_inf_set(unsigned j) {
if (m_tracker_of_x_change != nullptr)
(*m_tracker_of_x_change)(j, m_x[j]);
m_inf_set.insert(j);
lp_assert(!column_is_feasible(j));
}
void remove_column_from_inf_set(unsigned j) {
if (m_tracker_of_x_change != nullptr)
(*m_tracker_of_x_change)(j, m_x[j]);
m_inf_set.erase(j);
lp_assert(column_is_feasible(j));
}

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

@ -52,7 +52,8 @@ 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_look_for_feasible_solution_only(false),
m_tracker_of_x_change(nullptr) {
lp_assert(bounds_for_boxed_are_set_correctly());
init();
init_basis_heading_and_non_basic_columns_vector();

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

@ -779,7 +779,7 @@ public:
if (this->m_basis_heading[j] < 0)
continue;
if (!this->column_is_feasible(j))
this->m_inf_set.insert(j);
this->insert_column_into_inf_set(j);
}
}

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

@ -1197,9 +1197,9 @@ lp_primal_core_solver<T, X>::init_infeasibility_cost_for_column(unsigned j) {
}
if (numeric_traits<T>::is_zero(this->m_costs[j])) {
this->m_inf_set.erase(j);
this->remove_column_from_inf_set(j);
} else {
this->m_inf_set.insert(j);
this->insert_column_into_inf_set(j);
}
if (!this->m_settings.use_breakpoints_in_feasibility_search) {
this->m_costs[j] = - this->m_costs[j];

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

@ -349,9 +349,9 @@ update_x_tableau(unsigned entering, const X& delta) {
this->m_x[j] -= delta * this->m_A.get_val(c);
update_inf_cost_for_column_tableau(j);
if (is_zero(this->m_costs[j]))
this->m_inf_set.erase(j);
this->remove_column_from_inf_set(j);
else
this->m_inf_set.insert(j);
this->insert_column_into_inf_set(j);
}
}
lp_assert(this->A_mult_x_is_off() == false);