From 4cbb5869476f43c1c50d5136da27e40efa520d5f Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sun, 21 Apr 2019 12:03:36 -0700 Subject: [PATCH] unite smon and mon Signed-off-by: Lev Nachmanson --- src/util/lp/emonomials.cpp | 38 ++++++++-------- src/util/lp/emonomials.h | 89 +++++++++++++++++++------------------- 2 files changed, 64 insertions(+), 63 deletions(-) diff --git a/src/util/lp/emonomials.cpp b/src/util/lp/emonomials.cpp index e2bcc0b84..a2129323b 100644 --- a/src/util/lp/emonomials.cpp +++ b/src/util/lp/emonomials.cpp @@ -29,7 +29,7 @@ namespace nla { ++m_visited; if (m_visited == 0) { for (auto& svt : m_canonized) { - svt.m_visited = 0; + svt.visited() = 0; } ++m_visited; } @@ -144,7 +144,7 @@ namespace nla { } unsigned idx = m_monomials.size(); 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); do_canonize(m_monomials[idx]); smon const* result = nullptr; @@ -180,9 +180,9 @@ namespace nla { } void emonomials::remove_cg(unsigned idx, monomial const& m) { - smon_ts& sv = m_canonized[idx]; - unsigned next = sv.m_next; - unsigned prev = sv.m_prev; + smon& sv = m_canonized[idx]; + unsigned next = sv.next(); + unsigned prev = sv.prev(); lpvar u = m.var(), w; // equivalence class of u: @@ -194,10 +194,10 @@ namespace nla { } } if (prev != idx) { - m_canonized[next].m_prev = prev; - m_canonized[prev].m_next = next; - sv.m_next = idx; - sv.m_prev = idx; + m_canonized[next].prev() = prev; + m_canonized[prev].next() = next; + sv.next() = idx; + sv.prev() = idx; } } @@ -234,25 +234,25 @@ namespace nla { if (m_cg_table.find(v, w)) { SASSERT(w != v); unsigned idxr = m_var2index[w]; - unsigned idxl = m_canonized[idxr].m_prev; - m_canonized[idx].m_next = idxr; - m_canonized[idx].m_prev = idxl; - m_canonized[idxr].m_prev = idx; - m_canonized[idxl].m_next = idx; + unsigned idxl = m_canonized[idxr].prev(); + m_canonized[idx].next() = idxr; + m_canonized[idx].prev() = idxl; + m_canonized[idxr].prev() = idx; + m_canonized[idxl].next() = idx; } else { m_cg_table.insert(v); - SASSERT(m_canonized[idx].m_next == idx); - SASSERT(m_canonized[idx].m_prev == idx); + SASSERT(m_canonized[idx].next() == idx); + SASSERT(m_canonized[idx].prev() == idx); } } 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 { - 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) { unsigned idx = m_monomials.size(); 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; for (unsigned i = 0; i < sz; ++i) { lpvar w = vs[i]; diff --git a/src/util/lp/emonomials.h b/src/util/lp/emonomials.h index 79bfb8cbc..3e65a23a5 100644 --- a/src/util/lp/emonomials.h +++ b/src/util/lp/emonomials.h @@ -31,34 +31,43 @@ namespace nla { \brief class used to summarize the coefficients to a monomial after canonization with respect to current equalities. */ - class smon { - lpvar m_var; // variable representing original monomial - svector m_vars; - bool m_sign; - public: - smon(lpvar v) : m_var(v), m_sign(false) {} - lpvar var() const { return m_var; } - svector const& vars() const { return m_vars; } - svector::const_iterator begin() const { return vars().begin(); } - svector::const_iterator end() const { return vars().end(); } - unsigned size() const { return m_vars.size(); } - lpvar operator[](unsigned i) const { return m_vars[i]; } - bool sign() const { return m_sign; } - rational rsign() const { return rational(m_sign ? -1 : 1); } - 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; - } - }; +class smon { + lpvar m_var; // variable representing original monomial + svector m_vars; + bool m_sign; + unsigned m_next; // next congruent node. + unsigned m_prev; // previous congruent node + mutable unsigned m_visited; +public: + smon(lpvar v, unsigned idx): m_var(v), m_sign(false), m_next(idx), m_prev(idx), m_visited(0) {} + lpvar var() const { return m_var; } + unsigned next() const { return m_next; } + unsigned& next() { return m_next; } + unsigned prev() const { return m_prev; } + unsigned& prev() { return m_prev; } + unsigned visited() const { return m_visited; } + unsigned& visited() { return m_visited; } + svector const& vars() const { return m_vars; } + svector::const_iterator begin() const { return vars().begin(); } + svector::const_iterator end() const { return vars().end(); } + unsigned size() const { return m_vars.size(); } + lpvar operator[](unsigned i) const { return m_vars[i]; } + bool sign() const { return m_sign; } + rational rsign() const { return rational(m_sign ? -1 : 1); } + 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 { @@ -81,28 +90,21 @@ namespace nla { cell* m_head; 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 { emonomials& em; hash_canonical(emonomials& em): em(em) {} - + unsigned operator()(lpvar v) const { auto const& vec = em.m_canonized[em.m_var2index[v]].vars(); return string_hash(reinterpret_cast(vec.c_ptr()), sizeof(lpvar)*vec.size(), 10); } }; + + + + /** + \brief private fields used by emonomials for maintaining state of canonized monomials. + */ struct eq_canonical { emonomials& em; @@ -120,7 +122,7 @@ namespace nla { unsigned_vector m_lim; // backtracking point mutable unsigned m_visited; // timestamp of visited monomials during pf_iterator region m_region; // region for allocating linked lists - mutable vector m_canonized; // canonized versions of signed variables + mutable vector m_canonized; // canonized versions of signed variables mutable svector m_use_lists; // use list of monomials where variables occur. hash_canonical m_cg_hash; eq_canonical m_cg_eq; @@ -274,7 +276,6 @@ namespace nla { class pf_iterator { emonomials const& m; 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_end; @@ -321,7 +322,7 @@ namespace nla { sign_equiv_monomials_it& operator++() { m_touched = true; - m_index = m.m_canonized[m_index].m_next; + m_index = m.m_canonized[m_index].next(); return *this; }