From 47d5515b78d121c40cf8e2e782423d650bb768f6 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 26 May 2020 17:01:46 -0700
Subject: [PATCH] change try_patch to a template

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

diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index e9d6cc890..baab8c18e 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -306,8 +306,59 @@ public:
     bool column_corresponds_to_term(unsigned) const;
     inline unsigned row_count() const { return A_r().row_count(); }
     bool var_is_registered(var_index vj) const;
-    template <typename Blocker, typename ChangeReport>
-    bool try_to_patch(lpvar j, const mpq& val, const Blocker& blocker,const ChangeReport& change_report) {
+
+    template <typename CallBeforeChange, typename ChangeReport>
+    void change_basic_columns_dependend_on_a_given_nb_column_report(unsigned j,
+                                                                    const numeric_pair<mpq> & delta,
+                                                                    const CallBeforeChange& before,
+                                                                    const ChangeReport& after) {
+        if (use_tableau()) {
+            for (const auto & c : A_r().m_columns[j]) {
+                unsigned bj = m_mpq_lar_core_solver.m_r_basis[c.var()];
+                if (tableau_with_costs()) {
+                    m_basic_columns_with_changed_cost.insert(bj);
+                }
+                before(bj);
+                m_mpq_lar_core_solver.m_r_solver.add_delta_to_x_and_track_feasibility(bj, - A_r().get_val(c) * delta);
+                after(bj);
+                TRACE("change_x_del",
+                      tout << "changed basis column " << bj << ", it is " <<
+                      ( m_mpq_lar_core_solver.m_r_solver.column_is_feasible(bj)?  "feas":"inf") << std::endl;);
+                
+                  
+            }
+        } else {
+            NOT_IMPLEMENTED_YET();
+            m_column_buffer.clear();
+            m_column_buffer.resize(A_r().row_count());
+            m_mpq_lar_core_solver.m_r_solver.solve_Bd(j, m_column_buffer);
+            for (unsigned i : m_column_buffer.m_index) {
+                unsigned bj = m_mpq_lar_core_solver.m_r_basis[i];
+                m_mpq_lar_core_solver.m_r_solver.add_delta_to_x_and_track_feasibility(bj, -m_column_buffer[i] * delta); 
+            }
+        }
+    }
+
+    template <typename CallBeforeChange, typename ChangeReport>
+    void set_value_for_nbasic_column_report(unsigned j,
+                                            const impq & new_val,
+                                            const CallBeforeChange& before,
+                                            const ChangeReport& after) {
+
+        lp_assert(!is_base(j));
+        before(j);
+        auto & x = m_mpq_lar_core_solver.m_r_x[j];        
+        auto delta = new_val - x;
+        x = new_val;
+        after(j);
+        change_basic_columns_dependend_on_a_given_nb_column_report(j, delta, before, after);
+    }
+    
+    template <typename Blocker, typename CallBeforeChange, typename ChangeReport>
+    bool try_to_patch(lpvar j, const mpq& val,
+                      const Blocker& blocker,
+                      const CallBeforeChange& before,
+                      const ChangeReport& change_report) {
         if (is_base(j)) {
             TRACE("nla_solver", get_int_solver()->display_row_info(tout, row_of_basic_column(j)) << "\n";);
             remove_from_basis(j);
@@ -329,13 +380,7 @@ public:
                 return false;
         }
 
-        set_value_for_nbasic_column(j, ival);
-        change_report(j);
-        for (const auto &c : A_r().column(j)) {
-            unsigned rj = m_mpq_lar_core_solver.m_r_basis[c.var()];      
-            change_report(rj);
-        }
-
+        set_value_for_nbasic_column_report(j, ival, before, change_report);
         return true;
     }
     inline bool column_has_upper_bound(unsigned j) const {
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index a5280d47f..7f9920ad0 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1306,9 +1306,10 @@ bool core::patch_blocker(lpvar u, const monic& m) const {
 }
 
 bool core::try_to_patch(lpvar k, const rational& v, const monic & m) {
+    auto call_before_change = [this](lpvar u) { m_changes_of_patch.insert_if_not_there(u, val(u)); };
     auto blocker = [this, k, m](lpvar u) { return u != k && patch_blocker(u, m); };
     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, blocker, call_before_change, change_report);
 }
 
 bool in_power(const svector<lpvar>& vs, unsigned l) {
@@ -1381,6 +1382,7 @@ void core::patch_monomial(lpvar j) {
 }
 
 void core::patch_monomials() {
+    m_changes_of_patch.reset();
     auto to_refine = m_to_refine.index();
     // the rest of the function might change m_to_refine, so have to copy
     unsigned sz = to_refine.size();
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index b36bd2519..32e9e5668 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -170,6 +170,7 @@ private:
     svector<lpvar>           m_add_buffer;
     mutable lp::u_set        m_active_var_set;
     lp::u_set                m_rows;
+    u_map<rational>          m_changes_of_patch;
 public:
     reslimit&                m_reslim;
     bool                     m_use_nra_model;