From e7bb8e57cb1ed9d537146b8653d25bf12fc7e9da Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 28 May 2020 18:12:01 -0700
Subject: [PATCH] fixes in patch blocking

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/lar_solver.h |  6 +++---
 src/math/lp/nla_core.cpp | 12 ++++++------
 src/math/lp/nla_core.h   |  2 +-
 3 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 73189de79..5047486e7 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -358,7 +358,7 @@ public:
     
     template <typename Blocker, typename ChangeReport>
     bool try_to_patch(lpvar j, const mpq& val,
-                      const Blocker& blocker,
+                      const Blocker& is_blocked,
                       const ChangeReport& change_report) {
         if (is_base(j)) {
             TRACE("nla_solver", get_int_solver()->display_row_info(tout, row_of_basic_column(j)) << "\n";);
@@ -367,7 +367,7 @@ public:
         }
 
         impq ival(val);
-        if (!blocker(j, ival))
+        if (is_blocked(j, ival))
             return false;
 
         impq delta = get_column_value(j) - ival;
@@ -378,7 +378,7 @@ public:
             impq rj_new_val = a * delta + get_column_value(rj);
             // if (column_is_int(rj) && !rj_new_val.is_int())
             //     return false;
-            if (blocker(rj, rj_new_val))
+            if (is_blocked(rj, rj_new_val))
                 return false;
         }
 
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 18e2865ea..0884eaf08 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1287,11 +1287,11 @@ bool core::has_real(const monic& m) const {
             return true;
     return false;
 }
-
-bool core::patch_blocker(lpvar u, const monic& m, const lp::impq& ival) const {
+// returns true if the patching is blocking
+bool core::patch_is_blocked(lpvar u, const monic& m, const lp::impq& ival) const {
     SASSERT(m_to_refine.contains(m.var()));
     if (m_cautious_patching && !m_lar_solver.inside_bounds(u, ival))
-        return false;
+        return true; // blocking
     if (var_breaks_correct_monic(u)) {
         TRACE("nla_solver", tout << "u = " << u << " blocked as used in a correct monomial\n";);
         return true;
@@ -1306,10 +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 blocker = [this, k, m](lpvar u, const lp::impq& v)
-        { return u != k && patch_blocker(u, m, v); };
+    auto is_blocked = [this, k, m](lpvar u, const lp::impq& v)
+        { return u != k && patch_is_blocked(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, change_report);
+    return m_lar_solver.try_to_patch(k, v, is_blocked, change_report);
 }
 
 bool in_power(const svector<lpvar>& vs, unsigned l) {
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 133a70755..02c5e2f77 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -474,7 +474,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 u, const monic& m, const lp::impq&) const;
+    bool patch_is_blocked(lpvar u, const monic& m, const lp::impq&) const;
     bool has_big_num(const monic&) const;
     bool var_is_big(lpvar) const;
     bool has_real(const factorization&) const;