From 852df6f7d9cec0fc138eadfbada3dec87e97b96c Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 5 Jul 2018 16:35:05 -0700 Subject: [PATCH] reshufle var_register to faster access Signed-off-by: Lev Nachmanson --- src/util/lp/lar_solver.cpp | 5 ----- src/util/lp/lar_solver.h | 2 -- src/util/lp/var_register.h | 46 ++++++++++++++++++-------------------- 3 files changed, 22 insertions(+), 31 deletions(-) diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 8b5d8814a..6fec5b329 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -1507,11 +1507,6 @@ bool lar_solver::column_is_fixed(unsigned j) const { return m_mpq_lar_core_solver.column_is_fixed(j); } - -bool lar_solver::ext_var_is_int(var_index ext_var) const { - return m_var_register.external_is_int(ext_var); -} - // below is the initialization functionality of lar_solver bool lar_solver::strategy_is_undecided() const { diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 9f79ff835..f17aa4a0d 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -155,8 +155,6 @@ public: bool var_is_int(var_index v) const; - bool ext_var_is_int(var_index ext_var) const; - void add_non_basic_var_to_core_fields(unsigned ext_j, bool is_int); void add_new_var_to_core_fields_for_doubles(bool register_in_basis); diff --git a/src/util/lp/var_register.h b/src/util/lp/var_register.h index 86c238e12..93404bf91 100644 --- a/src/util/lp/var_register.h +++ b/src/util/lp/var_register.h @@ -19,19 +19,19 @@ Revision History: #pragma once namespace lp { class ext_var_info { - unsigned m_internal_j; // the internal index + unsigned m_external_j; // the internal index bool m_is_integer; public: ext_var_info() {} ext_var_info(unsigned j): ext_var_info(j, true) {} - ext_var_info(unsigned j , bool is_int) : m_internal_j(j), m_is_integer(is_int) {} - unsigned internal_j() const { return m_internal_j;} + ext_var_info(unsigned j , bool is_int) : m_external_j(j), m_is_integer(is_int) {} + unsigned external_j() const { return m_external_j;} bool is_integer() const {return m_is_integer;} }; class var_register { - svector m_local_to_external; - std::unordered_map m_external_to_local; + svector m_local_to_external; + std::unordered_map m_external_to_local; public: unsigned add_var(unsigned user_var) { return add_var(user_var, true); @@ -39,19 +39,23 @@ public: unsigned add_var(unsigned user_var, bool is_int) { auto t = m_external_to_local.find(user_var); if (t != m_external_to_local.end()) { - return t->second.internal_j(); + return t->second; } - unsigned j = size(); - m_external_to_local[user_var] = ext_var_info(j, is_int); - m_local_to_external.push_back(user_var); - return j; + m_local_to_external.push_back(ext_var_info(user_var, is_int)); + return m_external_to_local[user_var] = size() - 1; } - const svector & vars() const { return m_local_to_external; } + svector vars() const { + svector ret; + for (const auto& p : m_local_to_external) { + ret.push_back(p.external_j()); + } + return ret; + } unsigned local_to_external(unsigned local_var) const { - return m_local_to_external[local_var]; + return m_local_to_external[local_var].external_j(); } unsigned size() const { return m_local_to_external.size(); @@ -64,13 +68,7 @@ public: unsigned external_to_local(unsigned j) const { auto it = m_external_to_local.find(j); lp_assert(it != m_external_to_local.end()); - return it->second.internal_j(); - } - - bool external_is_int(unsigned j) const { - auto it = m_external_to_local.find(j); - lp_assert(it != m_external_to_local.end()); - return it->second.is_integer(); + return it->second; } bool external_is_used(unsigned ext_j) const { @@ -82,7 +80,7 @@ public: auto it = m_external_to_local.find(ext_j); if ( it == m_external_to_local.end()) return false; - local_j = it->second.internal_j(); + local_j = it->second; return true; } @@ -90,19 +88,19 @@ public: auto it = m_external_to_local.find(ext_j); if ( it == m_external_to_local.end()) return false; - local_j = it->second.internal_j(); - is_int = it->second.is_integer(); + local_j = it->second; + is_int = m_local_to_external[local_j].is_integer(); return true; } bool local_is_int(unsigned j) const { - return external_is_int(m_local_to_external[j]); + return m_local_to_external[j].is_integer(); } void shrink(unsigned shrunk_size) { for (unsigned j = size(); j-- > shrunk_size;) { - m_external_to_local.erase(m_local_to_external[j]); + m_external_to_local.erase(m_local_to_external[j].external_j()); } m_local_to_external.resize(shrunk_size); }