From c967b4aead6d576e94b37d4dbab0190011f7b263 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 29 May 2020 17:06:34 -0700 Subject: [PATCH] more efficient patching Signed-off-by: Lev Nachmanson --- src/math/lp/lar_solver.h | 2 +- src/math/lp/nla_core.cpp | 81 +++++++++++++++++++++------------------- src/math/lp/nla_core.h | 6 ++- 3 files changed, 47 insertions(+), 42 deletions(-) diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index a3fb26bbe..6216fafe2 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -367,7 +367,7 @@ public: impq ival(val); if (is_blocked(j, ival)) return false; - TRACE("nla_solver", tout << "not blocked\n";); + TRACE("nla_solver", tout << "j" << j << " not blocked\n";); impq delta = get_column_value(j) - ival; for (const auto &c : A_r().column(j)) { unsigned row_index = c.var(); diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 8c5cc5071..e3cc00816 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1289,36 +1289,41 @@ bool core::has_real(const monic& m) const { } // returns true if the patching is blocking -bool core::patch_is_blocked(lpvar u, const monic& patched_m, const lp::impq& ival) const { +bool core::is_patch_blocked(lpvar u, const lp::impq& ival) const { + TRACE("nla_solver", tout << "u = " << u << '\n';); if (m_cautious_patching && (!m_lar_solver.inside_bounds(u, ival) || (var_is_int(u) && ival.is_int() == false))) { TRACE("nla_solver", tout << "u = " << u << " blocked, for feas or integr\n";); - return true; // blocking + return true; // block } + + if (u == m_patched_var) { + TRACE("nla_solver", tout << "u == m_patched_var, no block\n";); + + return false; // do not block + } + // we can change only one variable in variables of m_patched_var + if (m_patched_monic->contains_var(u) || u == var(*m_patched_monic)) { + TRACE("nla_solver", tout << "u = " << u << " blocked as contained\n";); + return true; // block + } + 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 == patched_m.var() || (patched_m.contains_var(u) && var_breaks_correct_monic_as_factor(u, patched_m)); + TRACE("nla_solver", tout << "u = " << u << ", m_patched_m = "; print_monic(*m_patched_monic, tout) << + ", not blocked\n";); - TRACE("nla_solver", tout << "u = " << u << ", patched_m = "; print_monic(patched_m, tout) << - "ret = " << ret << "\n";); - - return ret; + return false; } -bool core::try_to_patch(lpvar patched_var, const rational& v, const monic & m) { - auto is_blocked = [this, patched_var, m](lpvar u, const lp::impq& iv) - { - if (!m_lar_solver.inside_bounds(u, iv)) - return true; - if (u == patched_var) - return false; - return patch_is_blocked(u, m, iv); - }; +// it tries to patch m_patched_var +bool core::try_to_patch(const rational& v) { + auto is_blocked = [this](lpvar u, const lp::impq& iv) { return is_patch_blocked(u, iv); }; auto change_report = [this](lpvar u) { update_to_refine_of_var(u); }; - return m_lar_solver.try_to_patch(patched_var, v, is_blocked, change_report); + return m_lar_solver.try_to_patch(m_patched_var, v, is_blocked, change_report); } bool in_power(const svector& vs, unsigned l) { @@ -1341,31 +1346,28 @@ bool core::to_refine_is_correct() const { return true; } -// looking for any real var to patch void core::patch_monomial(lpvar j) { - const monic& m = emons()[j]; - TRACE("nla_solver", tout << "m = "; print_monic(m, tout) << "\n";); - rational v = mul_val(m); - SASSERT(j == var(m)); - if (var_val(m) == v) { + m_patched_monic =& (emons()[j]); + m_patched_var = j; + TRACE("nla_solver", tout << "m = "; print_monic(*m_patched_monic, tout) << "\n";); + rational v = mul_val(*m_patched_monic); + if (val(j) == v) { erase_from_to_refine(j); return; } - - if (!var_breaks_correct_monic(j) && try_to_patch(j, v, m)) { + if (!var_breaks_correct_monic(j) && try_to_patch(v)) { SASSERT(to_refine_is_correct()); return; } - - // Now we try patching the factor variables. + // We could not patch j, now we try patching the factor variables. TRACE("nla_solver", tout << " trying squares\n";); // handle perfect squares - if (m.vars().size() == 2 && m.vars()[0] == m.vars()[1]) { + if ((*m_patched_monic).vars().size() == 2 && (*m_patched_monic).vars()[0] == (*m_patched_monic).vars()[1]) { rational root; if (v.is_perfect_square(root)) { - lpvar k = m.vars()[0]; - if (!var_breaks_correct_monic(k) && (try_to_patch(k, root, m) || try_to_patch(k, -root, m))) { + m_patched_var = (*m_patched_monic).vars()[0]; + if (!var_breaks_correct_monic(m_patched_var) && (try_to_patch(root) || try_to_patch(-root))) { TRACE("nla_solver", tout << "patched square\n";); return; } @@ -1378,16 +1380,15 @@ void core::patch_monomial(lpvar j) { // If we patch b then b should be equal to v/ac = v/(abc/b) = b(v/abc) if (!v.is_zero()) { rational r = val(j) / v; - SASSERT(m.is_sorted()); + SASSERT((*m_patched_monic).is_sorted()); TRACE("nla_solver", tout << "r = " << r << ", v = " << v << "\n";); - for (unsigned l = 0; l < m.size(); l++) { - lpvar k = m.vars()[l]; - if (!in_power(m.vars(), l) && - !var_is_int(k) && - !var_breaks_correct_monic(k) && - try_to_patch(k, r * val(k), m)) { // r * val(k) gives the right value of k - TRACE("nla_solver", tout << "patched j " << j << "\n";); - SASSERT(mul_val(m) == var_val(m)); + for (unsigned l = 0; l < (*m_patched_monic).size(); l++) { + m_patched_var = (*m_patched_monic).vars()[l]; + if (!in_power((*m_patched_monic).vars(), l) && + !var_breaks_correct_monic(m_patched_var) && + try_to_patch(r * val(m_patched_var))) { // r * val(k) gives the right value of k + TRACE("nla_solver", tout << "patched " << m_patched_var << "\n";); + SASSERT(mul_val((*m_patched_monic)) == val(j)); erase_from_to_refine(j); break; } @@ -1438,6 +1439,7 @@ void core::constrain_nl_in_tableau() { bool core::solve_tableau() { NOT_IMPLEMENTED_YET(); + return false; } void core::restore_tableau() { @@ -1450,6 +1452,7 @@ void core::save_tableau() { bool core::integrality_holds() { NOT_IMPLEMENTED_YET(); + return false; } diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 02c5e2f77..170ef52b9 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -176,6 +176,8 @@ public: nra::solver m_nra; private: bool m_cautious_patching; + lpvar m_patched_var; + monic const* m_patched_monic; public: void insert_to_refine(lpvar j); void erase_from_to_refine(lpvar j); @@ -472,9 +474,9 @@ public: 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 try_to_patch(const rational&); bool to_refine_is_correct() const; - bool patch_is_blocked(lpvar u, const monic& m, const lp::impq&) const; + bool is_patch_blocked(lpvar u, const lp::impq&) const; bool has_big_num(const monic&) const; bool var_is_big(lpvar) const; bool has_real(const factorization&) const;