From 09530bb6bcb09cba18115124496f30ca667716e6 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 24 May 2017 10:12:42 -0700
Subject: [PATCH] adding some content to the new check_int_feasibility()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/util/lp/lar_solver.cpp |  9 +++++++--
 src/util/lp/lar_solver.h   | 10 ++++++++++
 2 files changed, 17 insertions(+), 2 deletions(-)

diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index aed5e32db..14d3535af 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -1382,8 +1382,13 @@ void lar_solver::shrink_explanation_to_minimum(vector<std::pair<mpq, constraint_
 }
 
 final_check_status lar_solver::check_int_feasibility() {
-    std::cout << "lar_solver::check_int_feasibility()\n";
-	return final_check_status::GIVEUP;
+    unsigned n = A_r().column_count();
+    for (unsigned j = 0; j < n; j++) {
+        if (column_is_integer(j) && column_value_is_integer(j))
+            continue;
+        return final_check_status::GIVEUP;
+    }
+	return final_check_status::DONE;
 }
 } // namespace lean
 
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 6fba62fe8..a47240fdd 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -401,6 +401,16 @@ public:
         unsigned ext_var = m_columns_to_ext_vars_or_term_indices[j];
         return m_ext_vars_to_columns.find(ext_var)->second.is_integer();
     }
+
+    static bool impq_is_int(const impq& v) {
+        return v.x.is_int() && is_zero(v.y);
+    }
+    
+    inline
+    bool column_value_is_integer(unsigned j) const {
+        const impq & v = m_mpq_lar_core_solver.m_r_x[j];
+        return impq_is_int(v);
+    }
     inline bool column_is_real(unsigned j) const { return !column_is_integer(j); }	
 	final_check_status check_int_feasibility();
 };