From caa384f6c9306ef12880ed76f6766d20de4f1a18 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 25 May 2020 13:46:47 -0700 Subject: [PATCH] make m_inf_set private and cosmetic improvements in nla patching Signed-off-by: Lev Nachmanson --- src/math/lp/core_solver_pretty_printer_def.h | 5 +++ src/math/lp/int_solver.cpp | 9 ++-- src/math/lp/int_solver.h | 2 +- src/math/lp/lar_core_solver_def.h | 6 +-- src/math/lp/lar_solver.cpp | 32 ++++++++------ src/math/lp/lar_solver.h | 2 + src/math/lp/lp_core_solver_base.h | 20 ++++++++- src/math/lp/lp_primal_core_solver.h | 6 +-- src/math/lp/lp_primal_core_solver_def.h | 2 +- src/math/lp/nla_core.cpp | 45 ++++++++++++++------ src/math/lp/nla_core.h | 3 +- src/smt/theory_lra.cpp | 6 ++- 12 files changed, 95 insertions(+), 43 deletions(-) diff --git a/src/math/lp/core_solver_pretty_printer_def.h b/src/math/lp/core_solver_pretty_printer_def.h index f4c0b8d76..63520f014 100644 --- a/src/math/lp/core_solver_pretty_printer_def.h +++ b/src/math/lp/core_solver_pretty_printer_def.h @@ -347,6 +347,11 @@ template void core_solver_pretty_printer::print() if (!m_core_solver.m_column_norms.empty()) print_approx_norms(); m_out << std::endl; + if (m_core_solver.inf_set().size()) { + m_out << "inf columns: "; + print_vector(m_core_solver.inf_set(), m_out); + m_out << std::endl; + } } template void core_solver_pretty_printer::print_basis_heading() { diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 91cf8bebd..54bbe6d12 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -503,18 +503,19 @@ bool int_solver::at_upper(unsigned j) const { } } -void int_solver::display_row_info(std::ostream & out, unsigned row_index) const { +std::ostream& int_solver::display_row_info(std::ostream & out, unsigned row_index) const { auto & rslv = lrac.m_r_solver; for (const auto &c: rslv.m_A.m_rows[row_index]) { if (numeric_traits::is_pos(c.coeff())) out << "+"; out << c.coeff() << rslv.column_name(c.var()) << " "; } - + out << "\n"; for (const auto& c: rslv.m_A.m_rows[row_index]) { - rslv.print_column_bound_info(c.var(), out); + rslv.print_column_info(c.var(), out); + if (is_base(c.var())) out << "j" << c.var() << " base\n"; } - rslv.print_column_bound_info(rslv.m_basis[row_index], out); + return out; } bool int_solver::shift_var(unsigned j, unsigned range) { diff --git a/src/math/lp/int_solver.h b/src/math/lp/int_solver.h index 55a308f54..d281411f5 100644 --- a/src/math/lp/int_solver.h +++ b/src/math/lp/int_solver.h @@ -118,8 +118,8 @@ public: bool current_solution_is_inf_on_cut() const; bool shift_var(unsigned j, unsigned range); + std::ostream& display_row_info(std::ostream & out, unsigned row_index) const; private: - void display_row_info(std::ostream & out, unsigned row_index) const; unsigned random(); bool has_inf_int() const; public: diff --git a/src/math/lp/lar_core_solver_def.h b/src/math/lp/lar_core_solver_def.h index 4ff4197d2..abd9922ab 100644 --- a/src/math/lp/lar_core_solver_def.h +++ b/src/math/lp/lar_core_solver_def.h @@ -217,8 +217,8 @@ void lar_core_solver::calculate_pivot_row(unsigned i) { m_d_solver.m_steepest_edge_coefficients.resize(m_d_solver.m_n()); m_d_solver.m_column_norms.clear(); m_d_solver.m_column_norms.resize(m_d_solver.m_n(), 2); - m_d_solver.m_inf_set.clear(); - m_d_solver.m_inf_set.resize(m_d_solver.m_n()); + m_d_solver.clear_inf_set(); + m_d_solver.resize_inf_set(m_d_solver.m_n()); } void lar_core_solver::fill_not_improvable_zero_sum_from_inf_row() { @@ -268,7 +268,7 @@ void lar_core_solver::solve() { TRACE("lar_solver", tout << m_r_solver.get_status() << "\n";); lp_assert(m_r_solver.non_basic_columns_are_set_correctly()); lp_assert(m_r_solver.inf_set_is_correct()); - TRACE("find_feas_stats", tout << "infeasibles = " << m_r_solver.m_inf_set.size() << ", int_infs = " << get_number_of_non_ints() << std::endl;); + TRACE("find_feas_stats", tout << "infeasibles = " << m_r_solver.inf_set_size() << ", int_infs = " << get_number_of_non_ints() << std::endl;); if (m_r_solver.current_x_is_feasible() && m_r_solver.m_look_for_feasible_solution_only) { m_r_solver.set_status(lp_status::OPTIMAL); TRACE("lar_solver", tout << m_r_solver.get_status() << "\n";); diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index dfc69fe48..0306261cc 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -420,7 +420,7 @@ bool lar_solver::reduced_costs_are_zeroes_for_r_solver() const { void lar_solver::set_costs_to_zero(const lar_term& term) { auto & rslv = m_mpq_lar_core_solver.m_r_solver; - auto & jset = m_mpq_lar_core_solver.m_r_solver.m_inf_set; // hijack this set that should be empty right now + auto & jset = m_mpq_lar_core_solver.m_r_solver.inf_set(); // hijack this set that should be empty right now lp_assert(jset.is_empty()); for (const auto & p : term) { @@ -558,7 +558,6 @@ bool lar_solver::maximize_term_on_corrected_r_solver(lar_term & term, return false; } - bool lar_solver::remove_from_basis(unsigned j) { return m_mpq_lar_core_solver.m_r_solver.remove_from_basis(j); } @@ -787,9 +786,9 @@ void lar_solver::change_basic_columns_dependend_on_a_given_nb_column(unsigned j, void lar_solver::update_x_and_inf_costs_for_column_with_changed_bounds(unsigned j) { if (m_mpq_lar_core_solver.m_r_heading[j] >= 0) { if (costs_are_used()) { - bool was_infeas = m_mpq_lar_core_solver.m_r_solver.m_inf_set.contains(j); + bool was_infeas = m_mpq_lar_core_solver.m_r_solver.inf_set_contains(j); m_mpq_lar_core_solver.m_r_solver.track_column_feasibility(j); - if (was_infeas != m_mpq_lar_core_solver.m_r_solver.m_inf_set.contains(j)) + if (was_infeas != m_mpq_lar_core_solver.m_r_solver.inf_set_contains(j)) m_basic_columns_with_changed_cost.insert(j); } else { m_mpq_lar_core_solver.m_r_solver.track_column_feasibility(j); @@ -1208,7 +1207,7 @@ void lar_solver::get_model(std::unordered_map & variable_values) lp_assert(m_mpq_lar_core_solver.m_r_solver.calc_current_x_is_feasible_include_non_basis()); variable_values.clear(); - mpq delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(mpq(1, 2)); // start from 0.5 to have less clashes + mpq delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(mpq(1)); unsigned j; unsigned n = m_mpq_lar_core_solver.m_r_x.size(); std::unordered_set set_of_different_pairs; @@ -1484,9 +1483,9 @@ void lar_solver::pop_tableau() { void lar_solver::clean_inf_set_of_r_solver_after_pop() { vector became_feas; - clean_popped_elements(A_r().column_count(), m_mpq_lar_core_solver.m_r_solver.m_inf_set); + clean_popped_elements(A_r().column_count(), m_mpq_lar_core_solver.m_r_solver.inf_set()); std::unordered_set basic_columns_with_changed_cost; - auto inf_index_copy = m_mpq_lar_core_solver.m_r_solver.m_inf_set; + auto inf_index_copy = m_mpq_lar_core_solver.m_r_solver.inf_set(); for (auto j: inf_index_copy) { if (m_mpq_lar_core_solver.m_r_heading[j] >= 0) { continue; @@ -1504,16 +1503,16 @@ void lar_solver::clean_inf_set_of_r_solver_after_pop() { lp_assert(m_mpq_lar_core_solver.m_r_solver.m_basis_heading[j] < 0); m_mpq_lar_core_solver.m_r_solver.m_d[j] -= m_mpq_lar_core_solver.m_r_solver.m_costs[j]; m_mpq_lar_core_solver.m_r_solver.m_costs[j] = zero_of_type(); - m_mpq_lar_core_solver.m_r_solver.m_inf_set.erase(j); + m_mpq_lar_core_solver.m_r_solver.remove_column_from_inf_set(j); } became_feas.clear(); - for (unsigned j : m_mpq_lar_core_solver.m_r_solver.m_inf_set) { + for (unsigned j : m_mpq_lar_core_solver.m_r_solver.inf_set()) { lp_assert(m_mpq_lar_core_solver.m_r_heading[j] >= 0); if (m_mpq_lar_core_solver.m_r_solver.column_is_feasible(j)) became_feas.push_back(j); } for (unsigned j : became_feas) - m_mpq_lar_core_solver.m_r_solver.m_inf_set.erase(j); + m_mpq_lar_core_solver.m_r_solver.remove_column_from_inf_set(j); if (use_tableau_costs()) { @@ -1662,7 +1661,7 @@ void lar_solver::add_new_var_to_core_fields_for_mpq(bool register_in_basis) { m_mpq_lar_core_solver.m_r_x.resize(j + 1); m_mpq_lar_core_solver.m_r_lower_bounds.increase_size_by_one(); m_mpq_lar_core_solver.m_r_upper_bounds.increase_size_by_one(); - m_mpq_lar_core_solver.m_r_solver.m_inf_set.increase_size_by_one(); + m_mpq_lar_core_solver.m_r_solver.inf_set_increase_size_by_one(); m_mpq_lar_core_solver.m_r_solver.m_costs.resize(j + 1); m_mpq_lar_core_solver.m_r_solver.m_d.resize(j + 1); lp_assert(m_mpq_lar_core_solver.m_r_heading.size() == j); // as A().column_count() on the entry to the method @@ -2429,10 +2428,17 @@ bool lar_solver::inside_bounds(lpvar j, const impq& val) const { return true; } +void lar_solver::pivot_column_tableau(unsigned j, unsigned row_index) { + m_mpq_lar_core_solver.m_r_solver.pivot_column_tableau(j, row_index); + m_mpq_lar_core_solver.m_r_solver.change_basis(j, r_basis()[row_index]); +} + bool lar_solver::try_to_patch(lpvar j, const mpq& val, const std::function& blocker, const std::function& report_change) { - if (is_base(j)) { - VERIFY(remove_from_basis(j)); + if (is_base(j)) { + TRACE("nla_solver", get_int_solver()->display_row_info(tout, row_of_basic_column(j)) << "\n";); + remove_from_basis(j); } + impq ival(val); if (!inside_bounds(j, ival) || blocker(j)) return false; diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 9f646ccd3..f563d0594 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -362,6 +362,8 @@ public: return m_mpq_lar_core_solver.lower_bound(j); } + void pivot_column_tableau(unsigned j, unsigned row_index); + inline const impq & column_upper_bound(unsigned j) const { return m_mpq_lar_core_solver.upper_bound(j); } diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h index 02330fd5b..60d0f3fe0 100644 --- a/src/math/lp/lp_core_solver_base.h +++ b/src/math/lp/lp_core_solver_base.h @@ -51,10 +51,15 @@ public: return m_inf_set.size() == 0; } bool current_x_is_infeasible() const { return m_inf_set.size() != 0; } - u_set m_inf_set; private: + u_set m_inf_set; bool m_using_infeas_costs; public: + const u_set& inf_set() const { return m_inf_set; } + u_set& inf_set() { return m_inf_set; } + void inf_set_increase_size_by_one() { m_inf_set.increase_size_by_one(); } + bool inf_set_contains(unsigned j) const { return m_inf_set.contains(j); } + unsigned inf_set_size() const { return m_inf_set.size(); } bool using_infeas_costs() const { return m_using_infeas_costs; } void set_using_infeas_costs(bool val) { m_using_infeas_costs = val; } vector m_columns_nz; // m_columns_nz[i] keeps an approximate value of non zeroes the i-th column @@ -723,13 +728,26 @@ public: insert_column_into_inf_set(j); } void insert_column_into_inf_set(unsigned j) { + TRACE("lar_solver", tout << "j = " << j << "\n";); m_inf_set.insert(j); lp_assert(!column_is_feasible(j)); } void remove_column_from_inf_set(unsigned j) { + TRACE("lar_solver", tout << "j = " << j << "\n";); m_inf_set.erase(j); lp_assert(column_is_feasible(j)); } + + void resize_inf_set(unsigned size) { + TRACE("lar_solver",); + m_inf_set.resize(size); + } + + void clear_inf_set() { + TRACE("lar_solver",); + m_inf_set.clear(); + } + bool costs_on_nbasis_are_zeros() const { lp_assert(this->basis_heading_is_correct()); for (unsigned j = 0; j < this->m_n(); j++) { diff --git a/src/math/lp/lp_primal_core_solver.h b/src/math/lp/lp_primal_core_solver.h index a8f4fcb7a..806ad1932 100644 --- a/src/math/lp/lp_primal_core_solver.h +++ b/src/math/lp/lp_primal_core_solver.h @@ -484,7 +484,7 @@ public: int find_smallest_inf_column() { int j = -1; - for (unsigned k : this->m_inf_set) { + for (unsigned k : this->inf_set()) { if (k < static_cast(j)) { j = k; } @@ -821,12 +821,12 @@ public: if (this->using_infeas_costs()) { init_infeasibility_costs_for_changed_basis_only(); this->m_costs[leaving] = zero_of_type(); - this->m_inf_set.erase(leaving); + this->remove_column_from_inf_set(leaving); } } void init_inf_set() { - this->m_inf_set.clear(); + this->clear_inf_set(); for (unsigned j = 0; j < this->m_n(); j++) { if (this->m_basis_heading[j] < 0) continue; diff --git a/src/math/lp/lp_primal_core_solver_def.h b/src/math/lp/lp_primal_core_solver_def.h index 85c1c4fe8..aeaf485a7 100644 --- a/src/math/lp/lp_primal_core_solver_def.h +++ b/src/math/lp/lp_primal_core_solver_def.h @@ -1179,7 +1179,7 @@ lp_primal_core_solver::init_infeasibility_cost_for_column(unsigned j) { // set zero cost for each non-basis column if (this->m_basis_heading[j] < 0) { this->m_costs[j] = numeric_traits::zero(); - this->m_inf_set.erase(j); + this->remove_column_from_inf_set(j); return; } // j is a basis column diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 8cc347eec..245ad9321 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1210,17 +1210,34 @@ bool core::elists_are_consistent(bool check_in_model) const { return true; } -bool core::var_is_used_in_a_correct_monic(lpvar j) const { - if (emons().is_monic_var(j)) { - if (!m_to_refine.contains(j)) - return true; - } - for (const monic & m : emons().get_use_list(j)) { - if (!m_to_refine.contains(m.var())) { - TRACE("nla_solver", tout << "j" << j << " is used in a correct monic \n";); - return true; +bool core::var_breaks_correct_monic_as_factor(lpvar j, const monic& m) const { + if (!val(var(m)).is_zero()) + return true; + + if (!val(j).is_zero()) // j was not zero: the new value does not matter - m must have another zero product + return false; + // do we have another zero in m? + for (lpvar k : m) { + if (k != j && val(k).is_zero()) { + return false; // not breaking } } + // j was the only zero in m + return true; +} + +bool core::var_breaks_correct_monic(lpvar j) const { + if (emons().is_monic_var(j) && !m_to_refine.contains(j)) { + TRACE("nla_solver", tout << "j = " << j << ", m = "; print_monic(emons()[j], tout) << "\n";); + return true; // changing the value of a correct monic + } + + for (const monic & m : emons().get_use_list(j)) { + if (m_to_refine.contains(m.var())) + continue; + if (var_breaks_correct_monic_as_factor(j, m)) + return true; + } return false; } @@ -1274,12 +1291,12 @@ bool core::has_real(const monic& m) const { bool core::patch_blocker(lpvar u, const monic& m) const { SASSERT(m_to_refine.contains(m.var())); - if (var_is_used_in_a_correct_monic(u)) { + if (var_breaks_correct_monic(u)) { TRACE("nla_solver", tout << "u = " << u << " blocked as used in a correct monomial\n";); return true; } - bool ret = u == m.var() || m.contains_var(u); + bool ret = u == m.var() || (m.contains_var(u) && var_breaks_correct_monic_as_factor(u, m)); TRACE("nla_solver", tout << "u = " << u << ", m = "; print_monic(m, tout) << "ret = " << ret << "\n";); @@ -1326,7 +1343,7 @@ void core::patch_monomial_with_real_var(lpvar j) { if (val(j).is_zero() || v.is_zero()) // a lemma will catch it return; - if (!var_is_int(j) && !var_is_used_in_a_correct_monic(j) && try_to_patch(j, v, m)) { + if (!var_breaks_correct_monic(j) && try_to_patch(j, v, m)) { SASSERT(to_refine_is_correct()); return; } @@ -1337,7 +1354,7 @@ void core::patch_monomial_with_real_var(lpvar j) { if (v.is_perfect_square(root)) { lpvar k = m.vars()[0]; if (!var_is_int(k) && - !var_is_used_in_a_correct_monic(k) && + !var_breaks_correct_monic(k) && (try_to_patch(k, root, m) || try_to_patch(k, -root, m)) ) { } @@ -1352,7 +1369,7 @@ void core::patch_monomial_with_real_var(lpvar j) { lpvar k = m.vars()[l]; if (!in_power(m.vars(), l) && !var_is_int(k) && - !var_is_used_in_a_correct_monic(k) && + !var_breaks_correct_monic(k) && try_to_patch(k, r * val(k), m)) { // r * val(k) gives the right value of k SASSERT(mul_val(m) == var_val(m)); erase_from_to_refine(j); diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 09bc44e91..62c026dd8 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -466,7 +466,8 @@ public: bool is_used_in_monic(lpvar) const; void patch_monomials_with_real_vars(); void patch_monomial_with_real_var(lpvar); - bool var_is_used_in_a_correct_monic(lpvar) const; + bool var_breaks_correct_monic(lpvar) const; + bool var_breaks_correct_monic_as_factor(lpvar, const monic&) const; void update_to_refine_of_var(lpvar j); bool try_to_patch(lpvar, const rational&, const monic&); bool to_refine_is_correct() const; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index f9352d798..a2fb5acab 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1712,7 +1712,6 @@ public: final_check_status st = FC_DONE; switch (is_sat) { case l_true: - TRACE("arith", display(tout);); switch (check_lia()) { case l_true: @@ -2189,7 +2188,10 @@ public: TRACE("arith", tout << "canceled\n";); return l_undef; } - if (!m_nla) return l_true; + if (!m_nla) { + TRACE("arith", tout << "no nla\n";); + return l_true; + } if (!m_nla->need_check()) return l_true; return check_nla_continue(); }