From 822b0c1d5c8e73b114e9524c45191b174141ec1c Mon Sep 17 00:00:00 2001 From: Lev Date: Fri, 7 Sep 2018 15:56:36 -0700 Subject: [PATCH] in get_modele do not return values for terms Signed-off-by: Lev --- src/util/lp/lar_solver.cpp | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index c5520507c..840c32fbb 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -1253,7 +1253,7 @@ void lar_solver::get_infeasibility_explanation_for_inf_sign( void lar_solver::get_model(std::unordered_map & variable_values) const { lp_assert(m_mpq_lar_core_solver.m_r_solver.calc_current_x_is_feasible_include_non_basis()); mpq delta = mpq(1, 2); // start from 0.5 to have less clashes - unsigned i; + unsigned j; unsigned n = m_mpq_lar_core_solver.m_r_x.size(); variable_values.resize(n); do { @@ -1261,8 +1261,9 @@ void lar_solver::get_model(std::unordered_map & variable_values) std::unordered_set set_of_different_pairs; std::unordered_set set_of_different_singles; delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(delta); - for (i = 0; i < n; i++ ) { - const numeric_pair & rp = m_mpq_lar_core_solver.m_r_x[i]; + for (j = 0; j < n; j++ ) { + + const numeric_pair & rp = m_mpq_lar_core_solver.m_r_x[j]; set_of_different_pairs.insert(rp); mpq x = rp.x + delta * rp.y; set_of_different_singles.insert(x); @@ -1271,11 +1272,11 @@ void lar_solver::get_model(std::unordered_map & variable_values) delta /= mpq(2); break; } - TRACE("get_model", tout << get_column_name(i) << " := " << x << "\n";); - variable_values[i] = x; + if (!column_corresponds_to_term(j)) + variable_values[j] = x; } - } while (i != m_mpq_lar_core_solver.m_r_x.size()); + } while (j != m_mpq_lar_core_solver.m_r_x.size()); } void lar_solver::get_model_do_not_care_about_diff_vars(std::unordered_map & variable_values) const {