From 7b433bee2b4774cae125ce09d256f05c84732352 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 16 May 2017 17:36:32 -0700 Subject: [PATCH] track which var is an integer Signed-off-by: Lev Nachmanson --- src/smt/theory_lra.cpp | 2 +- src/util/lp/init_lar_solver.cpp | 15 ++++++++------- src/util/lp/lar_solver.cpp | 8 ++++++-- src/util/lp/lar_solver.h | 13 +++++++++++-- src/util/lp/quick_xplain.cpp | 4 ++-- 5 files changed, 28 insertions(+), 14 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 05aa33d13..0072aea7d 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -487,7 +487,7 @@ namespace smt { result = m_theory_var2var_index[v]; } if (result == UINT_MAX) { - result = m_solver->add_var(v); + result = m_solver->add_var(v, false); m_theory_var2var_index.setx(v, result, UINT_MAX); m_var_index2theory_var.setx(result, v, UINT_MAX); m_var_trail.push_back(v); diff --git a/src/util/lp/init_lar_solver.cpp b/src/util/lp/init_lar_solver.cpp index 97ebbdd5a..1f004198d 100644 --- a/src/util/lp/init_lar_solver.cpp +++ b/src/util/lp/init_lar_solver.cpp @@ -10,15 +10,15 @@ bool lar_solver::strategy_is_undecided() const { return m_settings.simplex_strategy() == simplex_strategy_enum::undecided; } -var_index lar_solver::add_var(unsigned ext_j) { +var_index lar_solver::add_var(unsigned ext_j, bool is_integer) { var_index i; lean_assert (ext_j < m_terms_start_index); if (ext_j >= m_terms_start_index) throw 0; // todo : what is the right way to exit? - - if (try_get_val(m_ext_vars_to_columns, ext_j, i)) { - return i; + auto it = m_ext_vars_to_columns.find(ext_j); + if (it != m_ext_vars_to_columns.end()) { + return it->second.ext_j(); } lean_assert(m_vars_to_ul_pairs.size() == A_r().column_count()); i = A_r().column_count(); @@ -31,7 +31,7 @@ var_index lar_solver::add_var(unsigned ext_j) { void lar_solver::register_new_ext_var_index(unsigned ext_v) { lean_assert(!contains(m_ext_vars_to_columns, ext_v)); unsigned j = static_cast(m_ext_vars_to_columns.size()); - m_ext_vars_to_columns[ext_v] = j; + m_ext_vars_to_columns.insert(std::make_pair(ext_v, ext_var_info(j))); lean_assert(m_columns_to_ext_vars_or_term_indices.size() == j); m_columns_to_ext_vars_or_term_indices.push_back(ext_v); } @@ -190,8 +190,9 @@ void lar_solver::update_column_type_and_bound(var_index j, lconstraint_kind kind void lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) { lean_assert(is_term(j)); unsigned adjusted_term_index = adjust_term_index(j); - unsigned term_j; - if (try_get_val(m_ext_vars_to_columns, j, term_j)) { + auto it = m_ext_vars_to_columns.find(j); + if (it != m_ext_vars_to_columns.end()) { + unsigned term_j = it->second.ext_j(); mpq rs = right_side - m_orig_terms[adjusted_term_index]->m_v; m_constraints.push_back(new lar_term_constraint(m_orig_terms[adjusted_term_index], kind, right_side)); update_column_type_and_bound(term_j, kind, rs, ci); diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index ba0f74201..594abae46 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -224,14 +224,18 @@ const lar_base_constraint& lar_solver::get_constraint(unsigned ci) const { int j_sign = (ib.m_coeff_before_j_is_pos ? 1 :-1) * bound_sign; unsigned m_j = ib.m_j; if (is_term(m_j)) { - m_j = m_ext_vars_to_columns[m_j]; + auto it = m_ext_vars_to_columns.find(m_j); + lean_assert(it != m_ext_vars_to_columns.end()); + m_j = it->second.ext_j(); } for (auto const& r : A_r().m_rows[i]) { unsigned j = r.m_j; mpq const& a = r.get_val(); if (j == m_j) continue; if (is_term(j)) { - j = m_ext_vars_to_columns[j]; + auto it = m_ext_vars_to_columns.find(j); + lean_assert(it != m_ext_vars_to_columns.end()); + j = it->second.ext_j(); } int a_sign = is_pos(a)? 1: -1; int sign = j_sign * a_sign; diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index f752d6734..2d2016dbe 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -35,11 +35,20 @@ namespace lean { class lar_solver : public column_namer { + class ext_var_info { + unsigned m_ext_j; // the external index + bool m_is_integer; + public: + ext_var_info(unsigned j): ext_var_info(j, false) {} + ext_var_info(unsigned j , bool is_int) : m_ext_j(j), m_is_integer(is_int) {} + unsigned ext_j() const { return m_ext_j;} + bool is_integer() const {return m_is_integer;} + }; //////////////////// fields ////////////////////////// lp_settings m_settings; stacked_value m_status; stacked_value m_simplex_strategy; - std::unordered_map m_ext_vars_to_columns; + std::unordered_map m_ext_vars_to_columns; vector m_columns_to_ext_vars_or_term_indices; stacked_vector m_vars_to_ul_pairs; vector m_constraints; @@ -74,7 +83,7 @@ public: // init region bool strategy_is_undecided() const; - var_index add_var(unsigned ext_j); + var_index add_var(unsigned ext_j, bool is_integer); void register_new_ext_var_index(unsigned ext_v); diff --git a/src/util/lp/quick_xplain.cpp b/src/util/lp/quick_xplain.cpp index a4b6fb0e6..df409240e 100644 --- a/src/util/lp/quick_xplain.cpp +++ b/src/util/lp/quick_xplain.cpp @@ -20,7 +20,7 @@ void quick_xplain::copy_constraint_and_add_constraint_vars(const lar_constraint& vector < std::pair> ls; for (auto & p : lar_c.get_left_side_coefficients()) { unsigned j = p.second; - unsigned lj = m_qsol.add_var(j); + unsigned lj = m_qsol.add_var(j, false); ls.push_back(std::make_pair(p.first, lj)); } m_constraints_in_local_vars.push_back(lar_constraint(ls, lar_c.m_kind, lar_c.m_right_side)); @@ -94,7 +94,7 @@ bool quick_xplain::is_feasible(const vector & x, unsigned k) const { vector < std::pair> ls; const lar_constraint & c = m_constraints_in_local_vars[i]; for (auto & p : c.get_left_side_coefficients()) { - unsigned lj = l.add_var(p.second); + unsigned lj = l.add_var(p.second, false); ls.push_back(std::make_pair(p.first, lj)); } l.add_constraint(ls, c.m_kind, c.m_right_side);