From 26764b076f2eab2656a5093946877376999a5530 Mon Sep 17 00:00:00 2001
From: Lev <levnach@hotmail.com>
Date: Fri, 14 Sep 2018 12:39:46 -0700
Subject: [PATCH] adjust cuts and branch (m_t and m_k) for terms

Signed-off-by: Lev <levnach@hotmail.com>
---
 src/util/lp/int_solver.cpp | 18 ++++++++++++------
 src/util/lp/int_solver.h   |  2 +-
 src/util/lp/lar_solver.cpp | 10 ++++++++++
 src/util/lp/lar_solver.h   |  1 +
 4 files changed, 24 insertions(+), 7 deletions(-)

diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp
index c416c63f3..f12e93103 100644
--- a/src/util/lp/int_solver.cpp
+++ b/src/util/lp/int_solver.cpp
@@ -383,19 +383,25 @@ typedef monomial mono;
 
 
 // this will allow to enable and disable tracking of the pivot rows
-struct pivoted_rows_tracking_control {
-    lar_solver * m_lar_solver;
-    bool m_track_pivoted_rows;
-    pivoted_rows_tracking_control(lar_solver* ls) :
+struct check_return_helper {
+    lar_solver *     m_lar_solver;
+    const lia_move & m_r;
+    bool             m_track_pivoted_rows;
+    check_return_helper(lar_solver* ls, const lia_move& r) :
         m_lar_solver(ls),
+        m_r(r),
         m_track_pivoted_rows(ls->get_track_pivoted_rows())
     {
         TRACE("pivoted_rows", tout << "pivoted rows = " << ls->m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows->size() << std::endl;);
         m_lar_solver->set_track_pivoted_rows(false);
     }
-    ~pivoted_rows_tracking_control() {
+    ~check_return_helper() {
         TRACE("pivoted_rows", tout << "pivoted rows = " << m_lar_solver->m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows->size() << std::endl;);
         m_lar_solver->set_track_pivoted_rows(m_track_pivoted_rows);
+        if (m_r == lia_move::cut || m_r == lia_move::branch) {
+            int_solver * s = m_lar_solver->get_int_solver();
+            m_lar_solver->adjust_cut_for_terms(*(s->m_t), *(s->m_k));
+        }
     }
 };
 
@@ -615,7 +621,7 @@ lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex, bool & upper) {
     lia_move r = run_gcd_test();
     if (r != lia_move::undef) return r;
 
-    pivoted_rows_tracking_control pc(m_lar_solver);
+    check_return_helper pc(m_lar_solver, r);
 
     if(settings().m_int_pivot_fixed_vars_from_basis)
         m_lar_solver->pivot_fixed_vars_from_basis();
diff --git a/src/util/lp/int_solver.h b/src/util/lp/int_solver.h
index 82fcb6eb4..414ca3006 100644
--- a/src/util/lp/int_solver.h
+++ b/src/util/lp/int_solver.h
@@ -160,5 +160,5 @@ public:
     bool hnf_has_var_with_non_integral_value() const;
     bool hnf_cutter_is_full() const;
     void patch_nbasic_column(unsigned j, bool patch_only_int_vals);
-};
+  };
 }
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 1340d1826..89044c7d6 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -2265,6 +2265,16 @@ void lar_solver::set_cut_strategy(unsigned cut_frequency) {
     } 
 }
 
+void lar_solver::adjust_cut_for_terms(const lar_term& t, mpq & rs) {
+    for (const auto& p : t) {
+        if (!is_term(p.var())) continue;
+        const lar_term & p_term = get_term(p.var());
+        if (p_term.m_v.is_zero()) continue;
+        rs -= p.coeff() * p_term.m_v;
+    }
+}
+
+
 } // namespace lp
 
 
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 9afb70c72..6ef0ea596 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -584,5 +584,6 @@ public:
     lar_term get_term_to_maximize(unsigned ext_j) const;
     void set_cut_strategy(unsigned cut_frequency);
     bool sum_first_coords(const lar_term& t, mpq & val) const;
+    void adjust_cut_for_terms(const lar_term& t, mpq & rs);
 };
 }