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

unite smon and mon

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-04-21 12:03:36 -07:00
parent c327f8799b
commit 4cbb586947
2 changed files with 64 additions and 63 deletions
Download patch file Download diff file Expand all files Collapse all files

38
src/util/lp/emonomials.cpp
View file

@ -29,7 +29,7 @@ namespace nla {
++m_visited; ++m_visited;
if (m_visited == 0) { if (m_visited == 0) {
for (auto& svt : m_canonized) { for (auto& svt : m_canonized) {
svt.m_visited = 0; svt.visited() = 0;
} }
++m_visited; ++m_visited;
} }
@ -144,7 +144,7 @@ namespace nla {
} }
unsigned idx = m_monomials.size(); unsigned idx = m_monomials.size();
m_monomials.push_back(monomial(v, vars.size(), vars.c_ptr())); m_monomials.push_back(monomial(v, vars.size(), vars.c_ptr()));
m_canonized.push_back(smon_ts(v, idx)); m_canonized.push_back(smon(v, idx));
m_var2index.setx(v, idx, UINT_MAX); m_var2index.setx(v, idx, UINT_MAX);
do_canonize(m_monomials[idx]); do_canonize(m_monomials[idx]);
smon const* result = nullptr; smon const* result = nullptr;
@ -180,9 +180,9 @@ namespace nla {
} }
void emonomials::remove_cg(unsigned idx, monomial const& m) { void emonomials::remove_cg(unsigned idx, monomial const& m) {
smon_ts& sv = m_canonized[idx]; smon& sv = m_canonized[idx];
unsigned next = sv.m_next; unsigned next = sv.next();
unsigned prev = sv.m_prev; unsigned prev = sv.prev();
lpvar u = m.var(), w; lpvar u = m.var(), w;
// equivalence class of u: // equivalence class of u:
@ -194,10 +194,10 @@ namespace nla {
} }
} }
if (prev != idx) { if (prev != idx) {
m_canonized[next].m_prev = prev; m_canonized[next].prev() = prev;
m_canonized[prev].m_next = next; m_canonized[prev].next() = next;
sv.m_next = idx; sv.next() = idx;
sv.m_prev = idx; sv.prev() = idx;
} }
} }
@ -234,25 +234,25 @@ namespace nla {
if (m_cg_table.find(v, w)) { if (m_cg_table.find(v, w)) {
SASSERT(w != v); SASSERT(w != v);
unsigned idxr = m_var2index[w]; unsigned idxr = m_var2index[w];
unsigned idxl = m_canonized[idxr].m_prev; unsigned idxl = m_canonized[idxr].prev();
m_canonized[idx].m_next = idxr; m_canonized[idx].next() = idxr;
m_canonized[idx].m_prev = idxl; m_canonized[idx].prev() = idxl;
m_canonized[idxr].m_prev = idx; m_canonized[idxr].prev() = idx;
m_canonized[idxl].m_next = idx; m_canonized[idxl].next() = idx;
} }
else { else {
m_cg_table.insert(v); m_cg_table.insert(v);
SASSERT(m_canonized[idx].m_next == idx); SASSERT(m_canonized[idx].next() == idx);
SASSERT(m_canonized[idx].m_prev == idx); SASSERT(m_canonized[idx].prev() == idx);
} }
} }
void emonomials::set_visited(monomial const& m) const { void emonomials::set_visited(monomial const& m) const {
m_canonized[m_var2index[m.var()]].m_visited = m_visited; m_canonized[m_var2index[m.var()]].visited() = m_visited;
} }
bool emonomials::is_visited(monomial const& m) const { bool emonomials::is_visited(monomial const& m) const {
return m_visited == m_canonized[m_var2index[m.var()]].m_visited; return m_visited == m_canonized[m_var2index[m.var()]].visited();
} }
/** /**
@ -265,7 +265,7 @@ namespace nla {
void emonomials::add(lpvar v, unsigned sz, lpvar const* vs) { void emonomials::add(lpvar v, unsigned sz, lpvar const* vs) {
unsigned idx = m_monomials.size(); unsigned idx = m_monomials.size();
m_monomials.push_back(monomial(v, sz, vs)); m_monomials.push_back(monomial(v, sz, vs));
m_canonized.push_back(smon_ts(v, idx)); m_canonized.push_back(smon(v, idx));
lpvar last_var = UINT_MAX; lpvar last_var = UINT_MAX;
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
lpvar w = vs[i]; lpvar w = vs[i];

87
src/util/lp/emonomials.h
View file

@ -31,34 +31,43 @@ namespace nla {
\brief class used to summarize the coefficients to a monomial after \brief class used to summarize the coefficients to a monomial after
canonization with respect to current equalities. canonization with respect to current equalities.
*/ */
class smon { class smon {
lpvar m_var; // variable representing original monomial lpvar m_var; // variable representing original monomial
svector<lpvar> m_vars; svector<lpvar> m_vars;
bool m_sign; bool m_sign;
public: unsigned m_next; // next congruent node.
smon(lpvar v) : m_var(v), m_sign(false) {} unsigned m_prev; // previous congruent node
lpvar var() const { return m_var; } mutable unsigned m_visited;
svector<lpvar> const& vars() const { return m_vars; } public:
svector<lp::var_index>::const_iterator begin() const { return vars().begin(); } smon(lpvar v, unsigned idx): m_var(v), m_sign(false), m_next(idx), m_prev(idx), m_visited(0) {}
svector<lp::var_index>::const_iterator end() const { return vars().end(); } lpvar var() const { return m_var; }
unsigned size() const { return m_vars.size(); } unsigned next() const { return m_next; }
lpvar operator[](unsigned i) const { return m_vars[i]; } unsigned& next() { return m_next; }
bool sign() const { return m_sign; } unsigned prev() const { return m_prev; }
rational rsign() const { return rational(m_sign ? -1 : 1); } unsigned& prev() { return m_prev; }
void reset() { m_sign = false; m_vars.reset(); } unsigned visited() const { return m_visited; }
void push_var(signed_var sv) { m_sign ^= sv.sign(); m_vars.push_back(sv.var()); } unsigned& visited() { return m_visited; }
void done_push() { svector<lpvar> const& vars() const { return m_vars; }
std::sort(m_vars.begin(), m_vars.end()); svector<lp::var_index>::const_iterator begin() const { return vars().begin(); }
} svector<lp::var_index>::const_iterator end() const { return vars().end(); }
std::ostream& display(std::ostream& out) const { unsigned size() const { return m_vars.size(); }
out << "v" << var() << " := "; lpvar operator[](unsigned i) const { return m_vars[i]; }
if (sign()) out << "- "; bool sign() const { return m_sign; }
for (lpvar v : vars()) out << "v" << v << " "; rational rsign() const { return rational(m_sign ? -1 : 1); }
return out; void reset() { m_sign = false; m_vars.reset(); }
} void push_var(signed_var sv) { m_sign ^= sv.sign(); m_vars.push_back(sv.var()); }
}; void done_push() {
std::sort(m_vars.begin(), m_vars.end());
}
std::ostream& display(std::ostream& out) const {
out << "v" << var() << " := ";
if (sign()) out << "- ";
for (lpvar v : vars()) out << "v" << v << " ";
return out;
}
};
inline std::ostream& operator<<(std::ostream& out, smon const& m) { return m.display(out); } inline std::ostream& operator<<(std::ostream& out, smon const& m) { return m.display(out); }
class emonomials : public var_eqs_merge_handler { class emonomials : public var_eqs_merge_handler {
@ -81,19 +90,6 @@ namespace nla {
cell* m_head; cell* m_head;
cell* m_tail; cell* m_tail;
}; };
/**
\brief private fields used by emonomials for maintaining state of canonized monomials.
*/
class smon_ts : public smon {
public:
smon_ts(lpvar v, unsigned idx): smon(v), m_next(idx), m_prev(idx), m_visited(0) {}
unsigned m_next; // next congruent node.
unsigned m_prev; // previous congruent node
mutable unsigned m_visited;
};
struct hash_canonical { struct hash_canonical {
emonomials& em; emonomials& em;
hash_canonical(emonomials& em): em(em) {} hash_canonical(emonomials& em): em(em) {}
@ -104,6 +100,12 @@ namespace nla {
} }
}; };
/**
\brief private fields used by emonomials for maintaining state of canonized monomials.
*/
struct eq_canonical { struct eq_canonical {
emonomials& em; emonomials& em;
eq_canonical(emonomials& em): em(em) {} eq_canonical(emonomials& em): em(em) {}
@ -120,7 +122,7 @@ namespace nla {
unsigned_vector m_lim; // backtracking point unsigned_vector m_lim; // backtracking point
mutable unsigned m_visited; // timestamp of visited monomials during pf_iterator mutable unsigned m_visited; // timestamp of visited monomials during pf_iterator
region m_region; // region for allocating linked lists region m_region; // region for allocating linked lists
mutable vector<smon_ts> m_canonized; // canonized versions of signed variables mutable vector<smon> m_canonized; // canonized versions of signed variables
mutable svector<head_tail> m_use_lists; // use list of monomials where variables occur. mutable svector<head_tail> m_use_lists; // use list of monomials where variables occur.
hash_canonical m_cg_hash; hash_canonical m_cg_hash;
eq_canonical m_cg_eq; eq_canonical m_cg_eq;
@ -274,7 +276,6 @@ namespace nla {
class pf_iterator { class pf_iterator {
emonomials const& m; emonomials const& m;
monomial const* m_mon; // monomial monomial const* m_mon; // monomial
lpvar m_var;
iterator m_it; // iterator over the first variable occurs list, ++ filters out elements that are not factors. iterator m_it; // iterator over the first variable occurs list, ++ filters out elements that are not factors.
iterator m_end; iterator m_end;
@ -321,7 +322,7 @@ namespace nla {
sign_equiv_monomials_it& operator++() { sign_equiv_monomials_it& operator++() {
m_touched = true; m_touched = true;
m_index = m.m_canonized[m_index].m_next; m_index = m.m_canonized[m_index].next();
return *this; return *this;
} }