mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

roll back in maximize_term if the integrality is broken

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-03-30 13:19:07 -07:00
parent f21b60a6e1
commit cf0952c232
4 changed files with 27 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/math/lp/lar_solver.cpp
View file

@ -1586,6 +1586,10 @@ var_index lar_solver::add_var(unsigned ext_j, bool is_int) {
return local_j;
}
bool lar_solver::has_int_var() const {
return m_var_register.has_int_var();
}
void lar_solver::register_new_ext_var_index(unsigned ext_v, bool is_int) {
lp_assert(!m_var_register.external_is_used(ext_v));
m_var_register.add_var(ext_v, is_int);

12
src/math/lp/lar_solver.h
View file

@ -95,18 +95,19 @@ public:
stacked_vector<ul_pair> m_columns_to_ul_pairs;
constraint_set m_constraints;
// the set of column indices j such that bounds have changed for j
u_set m_columns_with_changed_bound;
u_set m_rows_with_changed_bounds;
u_set m_basic_columns_with_changed_cost;
u_set m_columns_with_changed_bound;
u_set m_rows_with_changed_bounds;
u_set m_basic_columns_with_changed_cost;
// these are basic columns with the value changed, so the the corresponding row in the tableau
// does not sum to zero anymore
u_set m_incorrect_columns;
u_set m_incorrect_columns;
stacked_value<int> m_crossed_bounds_column_index; // such can be found at the initialization step
stacked_value<unsigned> m_term_count;
vector<lar_term*> m_terms;
indexed_vector<mpq> m_column_buffer;
std::unordered_map<lar_term, std::pair<mpq, unsigned>, term_hasher, term_comparer>
m_normalized_terms_to_columns;
vector<impq> m_backup_x;
// end of fields
const vector<lar_term*> & terms() const { return m_terms; }
@ -127,6 +128,7 @@ public:
bool column_value_is_int(unsigned j) const {
return m_mpq_lar_core_solver.m_r_x[j].is_int();
}
const impq& get_column_value(unsigned j) const {
return m_mpq_lar_core_solver.m_r_x[j];
@ -643,5 +645,7 @@ public:
bool fetch_normalized_term_column(const lar_term& t, std::pair<mpq, lpvar>& ) const;
bool try_to_patch(lpvar, const mpq&, const std::function<bool (lpvar)>& blocker,const std::function<void (lpvar)>& change_report);
bool inside_bounds(lpvar, const impq&) const;
void backup_x() { m_backup_x = m_mpq_lar_core_solver.m_r_x; }
void restore_x() { m_mpq_lar_core_solver.m_r_x = m_backup_x; }
};
}

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

@ -125,6 +125,13 @@ public:
return true;
}
bool has_int_var() const {
for (const auto & vi : m_local_to_external) {
if (vi.is_integer())
return true;
}
return false;
}
bool local_is_int(unsigned j) const {
return m_local_to_external[j & m_locals_mask_inverted].is_integer();

8
src/smt/theory_lra.cpp
View file

@ -3548,6 +3548,9 @@ public:
lp::impq term_max;
lp::lp_status st;
lpvar vi = 0;
if (has_int()) {
lp().backup_x();
}
if (!can_get_bound(v)) {
TRACE("arith", tout << "cannot get bound for v" << v << "\n";);
st = lp::lp_status::UNBOUNDED;
@ -3558,6 +3561,11 @@ public:
else {
vi = get_lpvar(v);
st = lp().maximize_term(vi, term_max);
if (has_int() && lp().has_inf_int()) {
st = lp::lp_status::FEASIBLE;
lp().restore_x();
}
}
switch (st) {
case lp::lp_status::OPTIMAL: {