From 91d9b0319e58c1124e65684ba617a5487da34d45 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 28 May 2020 10:21:04 -0700 Subject: [PATCH] toward full patching in nl Signed-off-by: Lev Nachmanson --- src/math/lp/lar_solver.h | 15 +++++---------- src/math/lp/nla_core.cpp | 33 ++++++++++++++++++--------------- src/math/lp/nla_core.h | 4 +++- 3 files changed, 26 insertions(+), 26 deletions(-) diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index f431a2604..a2bf376b9 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -312,10 +312,9 @@ public: inline void remove_column_from_inf_set(unsigned j) { m_mpq_lar_core_solver.m_r_solver.remove_column_from_inf_set(j); } - template + template void change_basic_columns_dependend_on_a_given_nb_column_report(unsigned j, const numeric_pair & delta, - const CallBeforeChange& before, const ChangeReport& after) { if (use_tableau()) { for (const auto & c : A_r().m_columns[j]) { @@ -323,7 +322,6 @@ public: if (tableau_with_costs()) { m_basic_columns_with_changed_cost.insert(bj); } - before(bj); m_mpq_lar_core_solver.m_r_solver.add_delta_to_x_and_track_feasibility(bj, - A_r().get_val(c) * delta); after(bj); TRACE("change_x_del", @@ -344,25 +342,22 @@ public: } } - template + template void set_value_for_nbasic_column_report(unsigned j, const impq & new_val, - const CallBeforeChange& before, const ChangeReport& after) { lp_assert(!is_base(j)); - before(j); auto & x = m_mpq_lar_core_solver.m_r_x[j]; auto delta = new_val - x; x = new_val; after(j); - change_basic_columns_dependend_on_a_given_nb_column_report(j, delta, before, after); + change_basic_columns_dependend_on_a_given_nb_column_report(j, delta, after); } - template + template bool try_to_patch(lpvar j, const mpq& val, const Blocker& blocker, - const CallBeforeChange& before, const ChangeReport& change_report) { if (is_base(j)) { TRACE("nla_solver", get_int_solver()->display_row_info(tout, row_of_basic_column(j)) << "\n";); @@ -385,7 +380,7 @@ public: return false; } - set_value_for_nbasic_column_report(j, ival, before, change_report); + set_value_for_nbasic_column_report(j, ival, change_report); return true; } inline bool column_has_upper_bound(unsigned j) const { diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 2bb14b841..18e2865ea 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1306,11 +1306,10 @@ bool core::patch_blocker(lpvar u, const monic& m, const lp::impq& ival) const { } bool core::try_to_patch(lpvar k, const rational& v, const monic & m) { - auto call_before_change = [this](lpvar u) { m_changes_of_patch.insert_if_not_there(u, val(u)); }; auto blocker = [this, k, m](lpvar u, const lp::impq& v) { return u != k && patch_blocker(u, m, v); }; auto change_report = [this](lpvar u) { update_to_refine_of_var(u); }; - return m_lar_solver.try_to_patch(k, v, blocker, call_before_change, change_report); + return m_lar_solver.try_to_patch(k, v, blocker, change_report); } bool in_power(const svector& vs, unsigned l) { @@ -1382,16 +1381,7 @@ void core::patch_monomial(lpvar j) { } } -void core::restore_patched_values() { - for (const auto & p : m_changes_of_patch) { - m_lar_solver.set_column_value(p.m_key, lp::impq(p.m_value)); - m_lar_solver.remove_column_from_inf_set(p.m_key); - } -} - -void core::patch_monomials() { - m_changes_of_patch.reset(); - m_cautious_patching = true; +void core::patch_monomials_on_to_refine() { auto to_refine = m_to_refine.index(); // the rest of the function might change m_to_refine, so have to copy unsigned sz = to_refine.size(); @@ -1402,19 +1392,24 @@ void core::patch_monomials() { if (m_to_refine.size() == 0) break; } - +} + +void core::patch_monomials() { + m_cautious_patching = true; + patch_monomials_on_to_refine(); if (m_to_refine.size() == 0 || !m_nla_settings.expensive_patching()) { return; } m_cautious_patching = false; // - NOT_IMPLEMENTED_YET(); // have to repeat the patching + patch_monomials_on_to_refine(); m_lar_solver.push(); + save_tableau(); constrain_nl_in_tableau(); if (solve_tableau() && integrality_holds()) { m_lar_solver.pop(1); } else { m_lar_solver.pop(); - restore_patched_values(); + restore_tableau(); m_lar_solver.clear_inf_set(); } SASSERT(m_lar_solver.ax_is_correct()); @@ -1428,6 +1423,14 @@ bool core::solve_tableau() { NOT_IMPLEMENTED_YET(); } +void core::restore_tableau() { + NOT_IMPLEMENTED_YET(); +} + +void core::save_tableau() { + NOT_IMPLEMENTED_YET(); +} + bool core::integrality_holds() { NOT_IMPLEMENTED_YET(); } diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index e15e0ddac..133a70755 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -170,7 +170,6 @@ private: svector m_add_buffer; mutable lp::u_set m_active_var_set; lp::u_set m_rows; - u_map m_changes_of_patch; public: reslimit& m_reslim; bool m_use_nra_model; @@ -468,6 +467,7 @@ public: bool is_nl_var(lpvar) const; bool is_used_in_monic(lpvar) const; void patch_monomials(); + void patch_monomials_on_to_refine(); void patch_monomial(lpvar); bool var_breaks_correct_monic(lpvar) const; bool var_breaks_correct_monic_as_factor(lpvar, const monic&) const; @@ -486,6 +486,8 @@ private: void restore_patched_values(); void constrain_nl_in_tableau(); bool solve_tableau(); + void restore_tableau(); + void save_tableau(); bool integrality_holds(); }; // end of core