From c8469022857aec6c23c8d829a0057ed5ac9f71d8 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 6 Apr 2020 15:32:35 -0700 Subject: [PATCH] simplify patch_blocker() Signed-off-by: Lev Nachmanson --- src/math/lp/nla_core.cpp | 7 +++++-- src/math/lp/nla_core.h | 2 +- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index a7eb6af6f..426adcbc0 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1370,7 +1370,7 @@ void core::update_to_refine_of_var(lpvar j) { } } -bool core::patch_blocker(lpvar patched_j, lpvar u, 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)) { TRACE("nla_solver", tout << "u = " << u << " blocked as used in a correct monomial\n";); @@ -1391,7 +1391,10 @@ bool core::patch_blocker(lpvar patched_j, lpvar u, const monic& m) const { bool core::try_to_patch(lpvar k, const rational& v, const monic & m) { return m_lar_solver.try_to_patch(k, v, - [this, k, m](lpvar u) { return patch_blocker(k, u, m); }, + [this, k, m](lpvar u) { + if (u == k) + return false; // ok to patch + return patch_blocker(u, m); }, [this](lpvar u) { update_to_refine_of_var(u); }); } diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index c0b037d18..2f2f15efe 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -423,7 +423,7 @@ public: void update_to_refine_of_var(lpvar j); bool try_to_patch(lpvar, const rational&, const monic&); bool to_refine_is_correct() const; - bool patch_blocker(lpvar patched_j, lpvar u, const monic& m) const; + bool patch_blocker(lpvar u, const monic& m) const; }; // end of core struct pp_mon {