From 69d6b022b8535fce5b48234326fcbba073e0fbb4 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@microsoft.com>
Date: Mon, 10 Jul 2017 22:14:56 -0700
Subject: [PATCH] speed up in get_model and fix in git_model_do_not_care_...

Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
---
 src/util/lp/int_solver.cpp | 36 +++++++++++++++++++-----------------
 src/util/lp/lar_solver.cpp |  7 +++++--
 2 files changed, 24 insertions(+), 19 deletions(-)

diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp
index 46d46e981..176d67733 100644
--- a/src/util/lp/int_solver.cpp
+++ b/src/util/lp/int_solver.cpp
@@ -39,24 +39,26 @@ void int_solver::failed() {
 }
 
 void int_solver::trace_inf_rows() const {
-    unsigned num = m_lar_solver->A_r().column_count();
-    for (unsigned v = 0; v < num; v++) {
-        if (is_int(v) && !get_value(v).is_int()) {
-            display_column(tout, v);
-        }
-    }
+    TRACE("arith_int_rows",
+          unsigned num = m_lar_solver->A_r().column_count();
+          for (unsigned v = 0; v < num; v++) {
+              if (is_int(v) && !get_value(v).is_int()) {
+                  display_column(tout, v);
+              }
+          }
     
-    num = 0;
-    for (unsigned i = 0; i < m_lar_solver->A_r().row_count(); i++) {
-        unsigned j = m_lar_solver->m_mpq_lar_core_solver.m_r_basis[i];
-        if (column_is_int_inf(j)) {
-            num++;
-            iterator_on_row<mpq> it(m_lar_solver->A_r().m_rows[i]);
-            m_lar_solver->print_linear_iterator(&it, tout);
-            tout << "\n";
-        }
-    }
-    tout << "num of int infeasible: " << num << "\n";
+          num = 0;
+          for (unsigned i = 0; i < m_lar_solver->A_r().row_count(); i++) {
+              unsigned j = m_lar_solver->m_mpq_lar_core_solver.m_r_basis[i];
+              if (column_is_int_inf(j)) {
+                  num++;
+                  iterator_on_row<mpq> it(m_lar_solver->A_r().m_rows[i]);
+                  m_lar_solver->print_linear_iterator(&it, tout);
+                  tout << "\n";
+              }
+          }
+          tout << "num of int infeasible: " << num << "\n";
+          );
 }
 
 int int_solver::find_inf_int_base_column() {
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 8dcd5a327..3cef85ce2 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -368,7 +368,6 @@ void lar_solver::pop(unsigned k) {
     unsigned m = A_r().row_count();
     clean_popped_elements(m, m_rows_with_changed_bounds);
     clean_inf_set_of_r_solver_after_pop();
-    m_status = m_mpq_lar_core_solver.m_r_solver.current_x_is_feasible()? lp_status::OPTIMAL: lp_status::UNKNOWN;
     lp_assert(m_settings.simplex_strategy() == simplex_strategy_enum::undecided ||
                 (!use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau());
         
@@ -389,6 +388,8 @@ void lar_solver::pop(unsigned k) {
     m_settings.simplex_strategy() = m_simplex_strategy;
     lp_assert(sizes_are_correct());
     lp_assert((!m_settings.use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau());
+    m_status = m_mpq_lar_core_solver.m_r_solver.current_x_is_feasible()? lp_status::OPTIMAL: lp_status::UNKNOWN;
+
 }
     
 vector<constraint_index> lar_solver::get_all_constraint_indices() const {
@@ -1139,9 +1140,11 @@ void lar_solver::get_model(std::unordered_map<var_index, mpq> & variable_values)
 }
 
 void lar_solver::get_model_do_not_care_about_diff_vars(std::unordered_map<var_index, mpq> & variable_values) const {
+    mpq delta = mpq(1);
+    delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(delta);
     for (unsigned i = 0; i < m_mpq_lar_core_solver.m_r_x.size(); i++ ) {
         const impq & rp = m_mpq_lar_core_solver.m_r_x[i];
-        variable_values[i] = rp.x + rp.y;
+        variable_values[i] = rp.x + delta * rp.y;
     }
 }