add a check in gomory cut

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

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;
 }
 

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;
 };
 }

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 

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>();