From 7a950dd6671ca9cb27356e74bfd95f8caf11d460 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sun, 29 Mar 2020 13:25:59 -0700 Subject: [PATCH] patch reals Signed-off-by: Lev Nachmanson --- src/math/lp/lar_solver.cpp | 41 ++++++++++++++++++++++++++ src/math/lp/lar_solver.h | 2 ++ src/math/lp/nla_core.cpp | 59 +++++++++++++++++++++++++++++++++++++- src/math/lp/nla_core.h | 6 +++- src/math/lp/u_set.h | 1 + 5 files changed, 107 insertions(+), 2 deletions(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index c602707cf..5e782e58b 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -2381,6 +2381,47 @@ std::pair lar_solver::add_equality(lpvar j, add_var_bound(term_index, lconstraint_kind::GE, mpq(0))); } +bool lar_solver::inside_bounds(lpvar j, const impq& val) const { + if (column_has_upper_bound(j) && val > get_upper_bound(j)) + return false; + if (column_has_lower_bound(j) && val < get_lower_bound(j)) + return false; + return true; +} + +bool lar_solver::try_to_patch(lpvar j, const mpq& val, std::function blocker, std::function report_change) { + if (is_base(j)) { + bool r = remove_from_basis(j); + SASSERT(r); + (void)r; + } + impq ival(val); + if (!inside_bounds(j, ival)) + return false; + + impq delta = ival - get_column_value(j); + for (const auto &c : A_r().column(j)) { + unsigned row_index = c.var(); + const mpq & a = c.coeff(); + unsigned rj = m_mpq_lar_core_solver.m_r_basis[row_index]; + impq rj_new_val = a * delta + get_column_value(rj); + if (column_is_int(rj) && ! rj_new_val.is_int()) + return false; + if (!inside_bounds(rj, rj_new_val) || blocker(rj)) + return false; + } + + set_column_value(j, ival); + for (const auto &c : A_r().column(j)) { + unsigned row_index = c.var(); + const mpq & a = c.coeff(); + unsigned rj = m_mpq_lar_core_solver.m_r_basis[row_index]; + set_column_value(rj,a * delta + get_column_value(rj)); + report_change(rj); + } + return true; +} + } // namespace lp diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index cf52c2ca8..9e5f3d852 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -641,5 +641,7 @@ public: void register_normalized_term(const lar_term&, lpvar); void deregister_normalized_term(const lar_term&); bool fetch_normalized_term_column(const lar_term& t, std::pair& ) const; + bool try_to_patch(lpvar, const mpq&, std::function blocker, std::function change_report); + bool inside_bounds(lpvar, const impq&) const; }; } diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 5497414ed..5cad0056d 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -971,7 +971,8 @@ void core::init_to_refine() { TRACE("nla_solver", tout << m_to_refine.size() << " mons to refine:\n"; - for (lpvar v : m_to_refine) tout << pp_mon(*this, m_emons[v]) << "\n";); + for (lpvar v : m_to_refine) tout << pp_mon(*this, m_emons[v]) << ":error = " << + (val(v) - mul_val(m_emons[v])).get_double() << "\n";); } std::unordered_set core::collect_vars(const lemma& l) const { @@ -1329,6 +1330,59 @@ bool core::elists_are_consistent(bool check_in_model) const { return true; } +bool core::var_is_used_in_a_correct_monic(lpvar j) const { + for (const monic & m : emons().get_use_list(j)) { + if (!m_to_refine.contains(m.var())) + return true; + } + return false; +} + +void core::update_to_refine_of_var(lpvar j) { + for (const monic & m : emons().get_use_list(j)) { + if (val(var(m)) == mul_val(m)) + m_to_refine.erase(var(m)); + else + m_to_refine.insert(var(m)); + } + if (is_monic_var(j)) { + const monic& m = emons()[j]; + if (val(var(m)) == mul_val(m)) + m_to_refine.erase(j); + else + m_to_refine.insert(j); + + } +} + + + +void core::patch_real_var(lpvar j) { + SASSERT(!var_is_int(j)); + rational v = mul_val(emons()[j]); + if (val(j) == v) + return; + if (var_is_used_in_a_correct_monic(j)) + return; + if(m_lar_solver.try_to_patch(j, v, + [this](lpvar k) { return var_is_used_in_a_correct_monic(k);}, + [this](lpvar k) { update_to_refine_of_var(k); })) + m_to_refine.erase(j); + +} + + +void core::patch_real_vars() { + auto to_refine = m_to_refine.index(); + // the rest of the function might change m_to_refine, so have to copy + for (lpvar j : to_refine) { + if (var_is_int(j)) + continue; + patch_real_var(j); + } + SASSERT(m_lar_solver.ax_is_correct()); +} + lbool core::check(vector& l_vec) { lp_settings().stats().m_nla_calls++; TRACE("nla_solver", tout << "calls = " << lp_settings().stats().m_nla_calls << "\n";); @@ -1340,10 +1394,13 @@ lbool core::check(vector& l_vec) { } init_to_refine(); + patch_real_vars(); if (m_to_refine.is_empty()) { return l_true; } + init_search(); + lbool ret = inner_check(true); if (ret == l_undef) ret = inner_check(false); diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index d077d14f5..14e20fabe 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -79,7 +79,7 @@ public: var_eqs m_evars; lp::lar_solver& m_lar_solver; vector * m_lemma_vec; - lp::u_set m_to_refine; + lp::u_set m_to_refine; tangents m_tangents; basics m_basics; order m_order; @@ -415,6 +415,10 @@ public: bool influences_nl_var(lpvar) const; bool is_nl_var(lpvar) const; bool is_used_in_monic(lpvar) const; + void patch_real_vars(); + void patch_real_var(lpvar); + bool var_is_used_in_a_correct_monic(lpvar) const; + void update_to_refine_of_var(lpvar j); }; // end of core struct pp_mon { diff --git a/src/math/lp/u_set.h b/src/math/lp/u_set.h index 7f8b1bd6f..589ef9232 100644 --- a/src/math/lp/u_set.h +++ b/src/math/lp/u_set.h @@ -103,5 +103,6 @@ public: } const unsigned * begin() const { return m_index.begin(); } const unsigned * end() const { return m_index.end(); } + const unsigned_vector& index() { return m_index; } }; }