patch reals

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/math/lp/lar_solver.cpp

@@ -2381,6 +2381,47 @@ std::pair<constraint_index, constraint_index> lar_solver::add_equality(lpvar j,
         add_var_bound(term_index, lconstraint_kind::GE, mpq(0)));
 }
 
+bool lar_solver::inside_bounds(lpvar j, const impq& val) const {
+    if (column_has_upper_bound(j) && val > get_upper_bound(j))
+        return false;
+    if (column_has_lower_bound(j) && val < get_lower_bound(j))
+        return false;
+    return true;
+}
+
+bool lar_solver::try_to_patch(lpvar j, const mpq& val, std::function<bool (lpvar)> blocker, std::function<void (lpvar)> report_change) {
+    if (is_base(j)) {        
+        bool r = remove_from_basis(j);
+        SASSERT(r);
+        (void)r;        
+    }
+    impq ival(val);
+    if (!inside_bounds(j, ival))
+        return false;
+
+    impq delta = ival - get_column_value(j);
+    for (const auto &c : A_r().column(j)) {
+        unsigned row_index = c.var();
+        const mpq & a = c.coeff();        
+        unsigned rj = m_mpq_lar_core_solver.m_r_basis[row_index];      
+        impq rj_new_val = a * delta + get_column_value(rj);
+        if (column_is_int(rj) && ! rj_new_val.is_int())
+            return  false;
+        if (!inside_bounds(rj, rj_new_val) || blocker(rj))
+            return  false;
+    }
+
+    set_column_value(j, ival);
+    for (const auto &c : A_r().column(j)) {
+        unsigned row_index = c.var();
+        const mpq & a = c.coeff();        
+        unsigned rj = m_mpq_lar_core_solver.m_r_basis[row_index];      
+        set_column_value(rj,a * delta + get_column_value(rj));
+        report_change(rj);
+    }
+    return true;
+}
+
 } // namespace lp
 
 

src/math/lp/lar_solver.h

@@ -641,5 +641,7 @@ public:
     void register_normalized_term(const lar_term&, lpvar);
     void deregister_normalized_term(const lar_term&);
     bool fetch_normalized_term_column(const lar_term& t, std::pair<mpq, lpvar>& ) const;
+    bool try_to_patch(lpvar, const mpq&, std::function<bool (lpvar)> blocker, std::function<void (lpvar)> change_report);
+    bool inside_bounds(lpvar, const impq&) const;
 };
 }

src/math/lp/nla_core.cpp

@@ -971,7 +971,8 @@ void core::init_to_refine() {
     
     TRACE("nla_solver", 
           tout << m_to_refine.size() << " mons to refine:\n";
-          for (lpvar v : m_to_refine) tout << pp_mon(*this, m_emons[v]) << "\n";);
+          for (lpvar v : m_to_refine) tout << pp_mon(*this, m_emons[v]) << ":error = " <<
+                                          (val(v) - mul_val(m_emons[v])).get_double() << "\n";);
 }
         
 std::unordered_set<lpvar> core::collect_vars(const lemma& l) const {
@@ -1329,6 +1330,59 @@ bool core::elists_are_consistent(bool check_in_model) const {
     return true;
 }
 
+bool core::var_is_used_in_a_correct_monic(lpvar j) const {
+    for (const monic & m : emons().get_use_list(j)) {
+        if (!m_to_refine.contains(m.var()))
+            return true;
+    }
+    return false;
+}
+
+void core::update_to_refine_of_var(lpvar j) {
+    for (const monic & m : emons().get_use_list(j)) {
+        if (val(var(m)) == mul_val(m))
+            m_to_refine.erase(var(m));
+        else
+            m_to_refine.insert(var(m));
+    }
+    if (is_monic_var(j)) {
+        const monic& m = emons()[j];
+        if (val(var(m)) == mul_val(m))
+            m_to_refine.erase(j);
+        else
+            m_to_refine.insert(j);
+        
+    }
+}
+
+
+
+void core::patch_real_var(lpvar j) {
+    SASSERT(!var_is_int(j));
+    rational v = mul_val(emons()[j]);
+    if (val(j) == v)
+        return;
+    if (var_is_used_in_a_correct_monic(j))
+        return;
+    if(m_lar_solver.try_to_patch(j, v,
+                              [this](lpvar k) { return var_is_used_in_a_correct_monic(k);},
+                              [this](lpvar k) { update_to_refine_of_var(k); }))
+        m_to_refine.erase(j);
+                              
+}
+
+
+void core::patch_real_vars() {
+    auto to_refine = m_to_refine.index();
+    // the rest of the function might change m_to_refine, so have to copy
+    for (lpvar j : to_refine) {
+        if (var_is_int(j))
+            continue;
+        patch_real_var(j);
+    }
+    SASSERT(m_lar_solver.ax_is_correct());
+}
+
 lbool core::check(vector<lemma>& l_vec) {
     lp_settings().stats().m_nla_calls++;
     TRACE("nla_solver", tout << "calls = " << lp_settings().stats().m_nla_calls << "\n";);
@@ -1340,10 +1394,13 @@ lbool core::check(vector<lemma>& l_vec) {
     }
 
     init_to_refine();
+    patch_real_vars();
     if (m_to_refine.is_empty()) {
         return l_true;
     }
+    
     init_search();
+    
     lbool ret = inner_check(true);
     if (ret == l_undef)
         ret = inner_check(false);

src/math/lp/nla_core.h

@@ -79,7 +79,7 @@ public:
     var_eqs<emonics>         m_evars;
     lp::lar_solver&          m_lar_solver;
     vector<lemma> *          m_lemma_vec;
-    lp::u_set              m_to_refine;
+    lp::u_set                m_to_refine;
     tangents                 m_tangents;
     basics                   m_basics;
     order                    m_order;
@@ -415,6 +415,10 @@ public:
     bool influences_nl_var(lpvar) const;
     bool is_nl_var(lpvar) const;
     bool is_used_in_monic(lpvar) const;
+    void patch_real_vars();
+    void patch_real_var(lpvar);
+    bool var_is_used_in_a_correct_monic(lpvar) const;
+    void update_to_refine_of_var(lpvar j);
 };  // end of core
 
 struct pp_mon {

src/math/lp/u_set.h

@@ -103,5 +103,6 @@ public:
     }
     const unsigned * begin() const { return m_index.begin(); }
     const unsigned * end() const { return m_index.end(); }
+    const unsigned_vector& index() { return m_index; }
 };
 }