From 0dbe8982cea49620c63af6bf688e06d2fc287a7c Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Sat, 11 Aug 2018 20:17:56 +0800
Subject: [PATCH] simplify lar_solver::get_model

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/smt/theory_lra.cpp      | 6 +++---
 src/util/lp/lar_solver.cpp  | 7 +++++--
 src/util/lp/niil_solver.cpp | 4 ++--
 src/util/lp/nra_solver.cpp  | 4 ++--
 4 files changed, 12 insertions(+), 9 deletions(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 216bcd559..425770c30 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1489,7 +1489,7 @@ public:
         }
             
         lp::var_index vi = m_theory_var2var_index[v];
-        if (m_variable_values.count(vi) > 0)
+        if (vi < m_variable_values.size())
             return m_variable_values[vi];
         
         if (!m_solver->is_term(vi)) {
@@ -1505,7 +1505,7 @@ public:
             if (m_solver->is_term(wi)) {
                 const lp::lar_term& term = m_solver->get_term(wi);
                 for (const auto & i : term) {
-                    if (m_variable_values.count(i.var()) > 0) {
+                    if (i.var() < m_variable_values.size()) {
                         result += m_variable_values[i.var()] * coeff * i.coeff();
                     }
                     else {
@@ -1517,7 +1517,7 @@ public:
                 result += m_variable_values[wi] * coeff;
             }
         }
-        m_variable_values[vi] = result;
+        m_term_values[vi] = result;
         return result;
     }
 
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 90505945e..da25e9648 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -1252,15 +1252,18 @@ void lar_solver::get_infeasibility_explanation_for_inf_sign(
 
 void lar_solver::get_model(std::unordered_map<var_index, mpq> & variable_values) const {
     lp_assert(m_mpq_lar_core_solver.m_r_solver.calc_current_x_is_feasible_include_non_basis());
+    if (m_status != lp_status::OPTIMAL)
+        return;
     mpq delta = mpq(1, 2); // start from 0.5 to have less clashes
     unsigned i;
+    unsigned n = m_mpq_lar_core_solver.m_r_x.size();
+    variable_values.resize(n);
     do {
         // different pairs have to produce different singleton values
         std::unordered_set<impq> set_of_different_pairs; 
         std::unordered_set<mpq> set_of_different_singles;
         delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(delta);
-        TRACE("get_model", tout << "delta=" << delta << "size = " << m_mpq_lar_core_solver.m_r_x.size() << std::endl;);
-        for (i = 0; i < m_mpq_lar_core_solver.m_r_x.size(); i++ ) {
+        for (i = 0; i < n; i++ ) {
             const numeric_pair<mpq> & rp = m_mpq_lar_core_solver.m_r_x[i];
             set_of_different_pairs.insert(rp);
             mpq x = rp.x + delta * rp.y;
diff --git a/src/util/lp/niil_solver.cpp b/src/util/lp/niil_solver.cpp
index c496a39ea..e46b29792 100644
--- a/src/util/lp/niil_solver.cpp
+++ b/src/util/lp/niil_solver.cpp
@@ -24,9 +24,9 @@ struct solver::imp {
 
     vector<mon_eq>         m_monomials;
     unsigned_vector        m_monomials_lim;
+    lp::lar_solver&        m_solver;
     imp(lp::lar_solver& s, reslimit& lim, params_ref const& p)
-    // :
-        // s(s), 
+        : m_solver(s)
         // m_limit(lim),
         // m_params(p)
     {
diff --git a/src/util/lp/nra_solver.cpp b/src/util/lp/nra_solver.cpp
index 200bdd2bc..a4d452bee 100644
--- a/src/util/lp/nra_solver.cpp
+++ b/src/util/lp/nra_solver.cpp
@@ -29,8 +29,8 @@ namespace nra {
         scoped_ptr<scoped_anum>    m_zero;
         vector<mon_eq>         m_monomials;
         unsigned_vector        m_monomials_lim;
-        mutable std::unordered_map<lp::var_index, rational> m_variable_values; // current model        
-
+        mutable vector<rational> m_variable_values; // current model        
+        mutable std::unordered_map<lp::var_index, rational> m_term_values;
         imp(lp::lar_solver& s, reslimit& lim, params_ref const& p): 
             s(s), 
             m_limit(lim),