mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

getting rid of from_index_dummy

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-05-06 12:14:27 -07:00
parent e49dbbe465
commit 6d5fd5d980
3 changed files with 9 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -35,8 +35,8 @@ class signed_var {
public: public:
// constructor, sign = true means minus // constructor, sign = true means minus
signed_var(lpvar v, bool sign): m_sv((v << 1) + (sign ? 1 : 0)) {} signed_var(lpvar v, bool sign): m_sv((v << 1) + (sign ? 1 : 0)) {}
explicit signed_var(unsigned sv) : m_sv(sv) {}
// constructor // constructor
signed_var(unsigned sv, from_index_dummy): m_sv(sv) {}
bool sign() const { return 0 != (m_sv & 0x1); } bool sign() const { return 0 != (m_sv & 0x1); }
lpvar var() const { return m_sv >> 1; } lpvar var() const { return m_sv >> 1; }
unsigned index() const { return m_sv; } unsigned index() const { return m_sv; }

4
src/util/lp/var_eqs.cpp
View file

@ -62,7 +62,7 @@ signed_var var_eqs::find(signed_var v) const {
return v; return v;
} }
unsigned idx = m_uf.find(v.index()); unsigned idx = m_uf.find(v.index());
return signed_var(idx, from_index_dummy()); return signed_var(idx);
} }
void var_eqs::explain_dfs(signed_var v1, signed_var v2, lp::explanation& e) const { void var_eqs::explain_dfs(signed_var v1, signed_var v2, lp::explanation& e) const {
@ -174,7 +174,7 @@ std::ostream& var_eqs::display(std::ostream& out) const {
unsigned idx = 0; unsigned idx = 0;
for (auto const& edges : m_eqs) { for (auto const& edges : m_eqs) {
if (!edges.empty()) { if (!edges.empty()) {
auto v = signed_var(idx, from_index_dummy()); auto v = signed_var(idx);
out << v << " root: " << find(v) << " : "; out << v << " root: " << find(v) << " : ";
for (auto const& jv : edges) { for (auto const& jv : edges) {
out << jv.m_var << " "; out << jv.m_var << " ";

10
src/util/lp/var_eqs.h
View file

@ -161,7 +161,7 @@ public:
public: public:
iterator(var_eqs& ve, unsigned idx, bool t) : m_ve(ve), m_idx(idx), m_touched(t) {} iterator(var_eqs& ve, unsigned idx, bool t) : m_ve(ve), m_idx(idx), m_touched(t) {}
signed_var operator*() const { signed_var operator*() const {
return signed_var(m_idx, from_index()); // 0 is needed to call the right constructor return signed_var(m_idx);
} }
iterator& operator++() { m_idx = m_ve.m_uf.next(m_idx); m_touched = true; return *this; } iterator& operator++() { m_idx = m_ve.m_uf.next(m_idx); m_touched = true; return *this; }
bool operator==(iterator const& other) const { return m_idx == other.m_idx && m_touched == other.m_touched; } bool operator==(iterator const& other) const { return m_idx == other.m_idx && m_touched == other.m_touched; }
@ -191,18 +191,20 @@ public:
void unmerge_eh(unsigned i, unsigned j) { void unmerge_eh(unsigned i, unsigned j) {
if (m_merge_handler) { if (m_merge_handler) {
m_merge_handler->unmerge_eh(signed_var(i, from_index_dummy()), signed_var(j, from_index_dummy())); m_merge_handler->unmerge_eh(signed_var(i), signed_var(j));
} }
} }
void merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) { void merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) {
if (m_merge_handler) { if (m_merge_handler) {
m_merge_handler->merge_eh(signed_var(r2, from_index_dummy()), signed_var(r1, from_index_dummy()), signed_var(v2, from_index_dummy()), signed_var(v1, from_index_dummy())); m_merge_handler->merge_eh(signed_var(r2), signed_var(r1),
signed_var(v2), signed_var(v1));
} }
} }
void after_merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) { void after_merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) {
if (m_merge_handler) { if (m_merge_handler) {
m_merge_handler->after_merge_eh(signed_var(r2, from_index_dummy()), signed_var(r1, from_index_dummy()), signed_var(v2, from_index_dummy()), signed_var(v1, from_index_dummy())); m_merge_handler->after_merge_eh(signed_var(r2), signed_var(r1),
signed_var(v2), signed_var(v1));
} }
} }