From e705e5a3094a0ffde405d32afaae9d26492fe6fe Mon Sep 17 00:00:00 2001
From: Lev <levnach@hotmail.com>
Date: Thu, 13 Sep 2018 11:38:22 -0700
Subject: [PATCH] branch on inf basic in gomory

Signed-off-by: Lev <levnach@hotmail.com>
---
 src/util/lp/gomory.h       | 46 ++++++++++++++++++++++++++++++++++++++
 src/util/lp/int_solver.cpp | 17 +++-----------
 src/util/lp/int_solver.h   |  1 -
 3 files changed, 49 insertions(+), 15 deletions(-)
 create mode 100644 src/util/lp/gomory.h

diff --git a/src/util/lp/gomory.h b/src/util/lp/gomory.h
new file mode 100644
index 000000000..87879f9f1
--- /dev/null
+++ b/src/util/lp/gomory.h
@@ -0,0 +1,46 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    <name>
+
+Abstract:
+
+    <abstract>
+
+Author:
+    Nikolaj Bjorner (nbjorner)
+    Lev Nachmanson (levnach)
+
+Revision History:
+
+
+--*/
+#pragma once
+#include "util/lp/lar_term.h"
+#include "util/lp/lia_move.h"
+#include "util/lp/explanation.h"
+
+namespace lp {
+class gomory {
+    lar_term   &          m_t; // the term to return in the cut
+    mpq        &          m_k; // the right side of the cut
+    explanation&          m_ex; // the conflict explanation
+    bool       &          m_upper; // we have a cut m_t*x <= k if m_upper is true nad m_t*x >= k otherwise
+    unsigned              m_basic_inf_int_j; // a basis column which has to be an integer but has a not integral value
+    const row_strip<mpq>& m_row
+public :
+    gomory(lar_term   &         m_t,
+           mpq        &         m_k,
+           explanation&         m_ex,
+           bool       &         m_upper, 
+           unsigned             m_basic_inf_int_j ) :
+        m_t(t),
+        m_k(k),
+        m_ex(ex),
+        m_upper(upper), 
+        m_basic_inf_int_j(j) {
+    }
+};
+}
diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp
index a77c202a0..c416c63f3 100644
--- a/src/util/lp/int_solver.cpp
+++ b/src/util/lp/int_solver.cpp
@@ -102,6 +102,8 @@ bool int_solver::is_gomory_cut_target(const row_strip<mpq>& row) {
     for (const auto & p : row) {
         j = p.var();
         if (is_base(j)) continue;
+        if (is_free(j))
+            return false;
         if (!at_bound(j))
             return false;
         if (!is_zero(get_value(j).y)) {
@@ -350,24 +352,11 @@ lia_move int_solver::mk_gomory_cut( unsigned inf_col, const row_strip<mpq> & row
     return lia_move::cut;
 }
 
-int int_solver::find_free_var_in_gomory_row(const row_strip<mpq>& row) {
-    unsigned j;
-    for (const auto & p : row) {
-        j = p.var();
-        if (!is_base(j) && is_free(j))
-            return static_cast<int>(j);
-    }
-    return -1;
-}
-
 lia_move int_solver::proceed_with_gomory_cut(unsigned j) {
     const row_strip<mpq>& row = m_lar_solver->get_row(row_of_basic_column(j));
 
-    if (-1 != find_free_var_in_gomory_row(row))  
-        return lia_move::undef;
-
     if (!is_gomory_cut_target(row)) 
-        return lia_move::undef;
+        return create_branch_on_column(j);
 
     *m_upper = true;
     return mk_gomory_cut(j, row);
diff --git a/src/util/lp/int_solver.h b/src/util/lp/int_solver.h
index ec708918d..82fcb6eb4 100644
--- a/src/util/lp/int_solver.h
+++ b/src/util/lp/int_solver.h
@@ -107,7 +107,6 @@ private:
     lia_move report_conflict_from_gomory_cut();
     void adjust_term_and_k_for_some_ints_case_gomory(mpq& lcm_den);
     lia_move proceed_with_gomory_cut(unsigned j);
-    int find_free_var_in_gomory_row(const row_strip<mpq>& );
     bool is_gomory_cut_target(const row_strip<mpq>&);
     bool at_bound(unsigned j) const;
     bool at_low(unsigned j) const;