From 04824e737284670b424c84b978b0db6eee732dc6 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@microsoft.com>
Date: Thu, 20 Jul 2017 18:12:16 -0700
Subject: [PATCH] add a check in gomory cut

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

diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp
index 793663bf1..7753dd600 100644
--- a/src/util/lp/int_solver.cpp
+++ b/src/util/lp/int_solver.cpp
@@ -273,6 +273,12 @@ void int_solver::gomory_cut_adjust_t_and_k_for_size_1(const vector<std::pair<mpq
 }
 
 
+bool int_solver::current_solution_is_inf_on_cut(const lar_term& t, const mpq& k) const {
+    const auto & x = m_lar_solver->m_mpq_lar_core_solver.m_r_x;
+    impq v = t.apply(x);
+    TRACE("gomory_cut", tout << "v = " << v << " k = " << k << std::endl;);
+    return v > k;
+}
 
 lia_move int_solver::report_gomory_cut(lar_term& t, mpq& k, mpq &lcm_den, unsigned num_ints) {
     lp_assert(!t.is_empty());
@@ -282,6 +288,7 @@ lia_move int_solver::report_gomory_cut(lar_term& t, mpq& k, mpq &lcm_den, unsign
     else
         gomory_cut_adjust_t_and_k_for_size_gt_1(pol, t, k, num_ints, lcm_den);
     m_lar_solver->subs_term_columns(t);
+    lp_assert(current_solution_is_inf_on_cut(t, k));
     return lia_move::cut;
 }
 
diff --git a/src/util/lp/int_solver.h b/src/util/lp/int_solver.h
index 53ae94ff8..b5a7e74f5 100644
--- a/src/util/lp/int_solver.h
+++ b/src/util/lp/int_solver.h
@@ -133,5 +133,6 @@ private:
     void display_row_info(std::ostream & out, unsigned row_index) const;
     void gomory_cut_adjust_t_and_k_for_size_1(const vector<std::pair<mpq, unsigned>> & pol, lar_term & t, mpq &k);
     void gomory_cut_adjust_t_and_k_for_size_gt_1(vector<std::pair<mpq, unsigned>> & pol, lar_term & t, mpq &k, unsigned num_ints, mpq &lcm_den);
+    bool current_solution_is_inf_on_cut(const lar_term& t, const mpq& k) const;
 };
 }
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 3a48c4d79..31a33d9d3 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -466,8 +466,6 @@ public:
         for (const auto & m : t.m_coeffs) {
             pol.push_back(std::make_pair(m.second, adjust_column_index_to_term_index(m.first)));
         }
-
-
         mpq v = t.m_v;
         vector<std::pair<mpq, unsigned>> pol_after_subs;
         // todo : remove the call to substitute_terms_in_linear_expression 
diff --git a/src/util/lp/lar_term.h b/src/util/lp/lar_term.h
index dc3921767..10e58dafa 100644
--- a/src/util/lp/lar_term.h
+++ b/src/util/lp/lar_term.h
@@ -70,6 +70,16 @@ struct lar_term {
             t.second.neg();
     }
 
+    template <typename T>
+    T apply(const vector<T>& x) const {
+        T ret = T(m_v);
+        for (const auto & t : m_coeffs) {
+            ret += t.second * x[t.first];
+        }
+        return ret;
+    }
+   
+    
     void clear() {
         m_coeffs.clear();
         m_v = zero_of_type<mpq>();