mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

reshufle var_register to faster access

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-07-05 16:35:05 -07:00
parent 905282ffe4
commit 852df6f7d9
3 changed files with 22 additions and 31 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/util/lp/lar_solver.cpp
View file

@ -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 {

2
src/util/lp/lar_solver.h
View file

@ -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);

46
src/util/lp/var_register.h
View file

@ -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<unsigned> m_local_to_external;
std::unordered_map<unsigned, ext_var_info> m_external_to_local;
svector<ext_var_info> m_local_to_external;
std::unordered_map<unsigned, unsigned> 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<unsigned> & vars() const { return m_local_to_external; }
svector<unsigned> vars() const {
svector<unsigned> 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);
}