From cf0952c2325d1b508bad2471765a18dfdb0ccc78 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 30 Mar 2020 13:19:07 -0700 Subject: [PATCH] roll back in maximize_term if the integrality is broken Signed-off-by: Lev Nachmanson --- src/math/lp/lar_solver.cpp | 4 ++++ src/math/lp/lar_solver.h | 12 ++++++++---- src/math/lp/var_register.h | 7 +++++++ src/smt/theory_lra.cpp | 8 ++++++++ 4 files changed, 27 insertions(+), 4 deletions(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 8d885a8d1..5772888e4 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -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); diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 2c979d813..ae66764be 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -95,18 +95,19 @@ public: stacked_vector 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 m_crossed_bounds_column_index; // such can be found at the initialization step stacked_value m_term_count; vector m_terms; indexed_vector m_column_buffer; std::unordered_map, term_hasher, term_comparer> m_normalized_terms_to_columns; + vector m_backup_x; // end of fields const vector & 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& ) const; bool try_to_patch(lpvar, const mpq&, const std::function& blocker,const std::function& 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; } }; } diff --git a/src/math/lp/var_register.h b/src/math/lp/var_register.h index 69f07204f..6b1f02ca1 100644 --- a/src/math/lp/var_register.h +++ b/src/math/lp/var_register.h @@ -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(); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 40d648429..49524f38e 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -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: {