From 55329ea9358e5b32ea6867d26bdc14249be35463 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 2 Apr 2020 14:47:06 -0700
Subject: [PATCH] more fixes in patching of monomials

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

diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 6b81d6faa..654d314bd 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -2398,7 +2398,7 @@ bool lar_solver::try_to_patch(lpvar j, const mpq& val, const std::function<bool
         VERIFY(remove_from_basis(j));
     }
     impq ival(val);
-    if (!inside_bounds(j, ival))
+    if (!inside_bounds(j, ival) || blocker(j))
         return false;
 
     impq delta = get_column_value(j) - ival;
@@ -2414,6 +2414,7 @@ bool lar_solver::try_to_patch(lpvar j, const mpq& val, const std::function<bool
     }
 
     set_column_value(j, ival);
+    report_change(j);
     for (const auto &c : A_r().column(j)) {
         unsigned row_index = c.var();
         const mpq & a = c.coeff();        
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 6d31bba99..8b1970afc 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1379,6 +1379,21 @@ bool in_power(const svector<lpvar>& vs, unsigned l) {
     return (l != 0 && vs[l - 1] == k) || (l + 1 < vs.size() && k == vs[l + 1]);
 }
 
+bool core::to_refine_is_correct() const {
+    for (unsigned j = 0; j < m_lar_solver.number_of_vars(); j++) {
+        if (!emons().is_monic_var(j)) continue;
+        bool valid = check_monic(emons()[j]);
+        if (valid != m_to_refine.contains(j)) {
+            TRACE("nla_solver", tout << "inconstency in m_to_refine : ";
+                  print_monic(emons()[j], tout) << "\n";
+                  if (valid) tout << "should NOT be there\n";
+                  else tout << "should be there\n";);
+            return false;
+        }
+    }
+    return true;
+}
+
 // looking for any real var to patch
 void core::patch_monomial_with_real_var(lpvar j) {    
     const monic& m = emons()[j];
@@ -1393,11 +1408,23 @@ void core::patch_monomial_with_real_var(lpvar j) {
         return;
 
     if (!var_is_int(j) && !var_is_used_in_a_correct_monic(j) && try_to_patch(j, v, m)) {
-        // SASSERT(mul_val(m) == var_val(m));        
-        m_to_refine.erase(j);
+        SASSERT(to_refine_is_correct());        
         return;
-    } 
+    }
 
+    // handle perfect squares
+    if (m.vars().size() == 2 && m.vars()[0] == m.vars()[1]) {        
+        rational root;
+        if (v.is_perfect_square(root)) {
+            lpvar k = m.vars()[0];
+            if (!var_is_int(k) && 
+                !var_is_used_in_a_correct_monic(k) &&
+                (try_to_patch(k, root, m) || try_to_patch(k, -root, m))
+                ) { 
+            }
+        }
+        return;
+    }
     // We have v != abc. Let us suppose we patch b. Then b should
     // be equal to v/ac = v/(abc/b) = b(v/abc)
     rational r = val(j) / v;
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 9972df832..171397d89 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -420,6 +420,7 @@ public:
     bool var_is_used_in_a_correct_monic(lpvar) const;
     void update_to_refine_of_var(lpvar j);
     bool try_to_patch(lpvar, const rational&, const monic&);
+    bool to_refine_is_correct() const;
 };  // end of core
 
 struct pp_mon {