diff --git a/src/util/lp/CMakeLists.txt b/src/util/lp/CMakeLists.txt index bda497378..26b95fefb 100644 --- a/src/util/lp/CMakeLists.txt +++ b/src/util/lp/CMakeLists.txt @@ -39,7 +39,6 @@ z3_add_component(lp square_dense_submatrix.cpp square_sparse_matrix.cpp static_matrix.cpp - var_eqs.cpp COMPONENT_DEPENDENCIES util polynomial diff --git a/src/util/lp/emonomials.cpp b/src/util/lp/emonomials.cpp index 90735d23e..c6bcf89fe 100644 --- a/src/util/lp/emonomials.cpp +++ b/src/util/lp/emonomials.cpp @@ -399,5 +399,4 @@ std::ostream& emonomials::display(std::ostream& out) const { return out; } - } diff --git a/src/util/lp/emonomials.h b/src/util/lp/emonomials.h index 163d363de..76ae6f5a2 100644 --- a/src/util/lp/emonomials.h +++ b/src/util/lp/emonomials.h @@ -29,7 +29,7 @@ namespace nla { class core; -class emonomials : public var_eqs_merge_handler { +class emonomials { /** \brief singly-lined cyclic list of monomial indices where variable occurs. Each variable points to the head and tail of the cyclic list. @@ -75,7 +75,7 @@ class emonomials : public var_eqs_merge_handler { }; mutable svector m_find_key; // the key used when looking for a monomial with the specific variables - var_eqs& m_ve; + var_eqs& m_ve; mutable vector m_monomials; // set of monomials mutable unsigned_vector m_var2index; // var_mIndex -> mIndex unsigned_vector m_lim; // backtracking point @@ -110,7 +110,7 @@ public: push and pop on emonomials calls push/pop on var_eqs, so no other calls to push/pop to the var_eqs should take place. */ - emonomials(var_eqs& ve): + emonomials(var_eqs& ve): m_ve(ve), m_visited(0), m_cg_hash(*this), @@ -288,11 +288,11 @@ public: these are merge event handlers to interect the union-find handlers. r2 becomes the new root. r2 is the root of v2, r1 is the old root of v1 */ - void merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1) override; + void merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1); - void after_merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1) override; + void after_merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1); - void unmerge_eh(signed_var r2, signed_var r1) override; + void unmerge_eh(signed_var r2, signed_var r1); bool is_monomial_var(lpvar v) const { return m_var2index.get(v, UINT_MAX) != UINT_MAX; } }; diff --git a/src/util/lp/nla_core.h b/src/util/lp/nla_core.h index aa2369118..75b5c4173 100644 --- a/src/util/lp/nla_core.h +++ b/src/util/lp/nla_core.h @@ -76,7 +76,7 @@ public: class core { public: - var_eqs m_evars; + var_eqs m_evars; lp::lar_solver& m_lar_solver; vector * m_lemma_vec; svector m_to_refine; diff --git a/src/util/lp/var_eqs.cpp b/src/util/lp/var_eqs.cpp deleted file mode 100644 index 16708180a..000000000 --- a/src/util/lp/var_eqs.cpp +++ /dev/null @@ -1,189 +0,0 @@ -/*++ - Copyright (c) 2017 Microsoft Corporation - - Module Name: - - - - Abstract: - - - - Author: - Nikolaj Bjorner (nbjorner) - Lev Nachmanson (levnach) - - Revision History: - - - --*/ - -#include "util/lp/var_eqs.h" - -namespace nla { - - -var_eqs::var_eqs(): m_merge_handler(nullptr), m_uf(*this), m_stack(*this) {} - -void var_eqs::push() { - m_trail_lim.push_back(m_trail.size()); - m_stack.push_scope(); -} - -void var_eqs::pop(unsigned n) { - unsigned old_sz = m_trail_lim[m_trail_lim.size() - n]; - for (unsigned i = m_trail.size(); i-- > old_sz; ) { - auto const& sv = m_trail[i]; - m_eqs[sv.first.index()].pop_back(); - m_eqs[sv.second.index()].pop_back(); - m_eqs[(~sv.first).index()].pop_back(); - m_eqs[(~sv.second).index()].pop_back(); - } - m_trail_lim.shrink(m_trail_lim.size() - n); - m_trail.shrink(old_sz); - m_stack.pop_scope(n); -} - -void var_eqs::merge(signed_var v1, signed_var v2, eq_justification const& j) { - unsigned max_i = std::max(v1.index(), v2.index()) + 2; - m_eqs.reserve(max_i); - while (m_uf.get_num_vars() <= max_i) m_uf.mk_var(); - m_trail.push_back(std::make_pair(v1, v2)); - m_uf.merge(v1.index(), v2.index()); - m_uf.merge((~v1).index(), (~v2).index()); - m_eqs[v1.index()].push_back(eq_edge(v2, j)); - m_eqs[v2.index()].push_back(eq_edge(v1, j)); - m_eqs[(~v1).index()].push_back(eq_edge(~v2, j)); - m_eqs[(~v2).index()].push_back(eq_edge(~v1, j)); -} - -signed_var var_eqs::find(signed_var v) const { - if (v.index() >= m_uf.get_num_vars()) { - return v; - } - unsigned idx = m_uf.find(v.index()); - return signed_var(idx); -} - -void var_eqs::explain_dfs(signed_var v1, signed_var v2, lp::explanation& e) const { - SASSERT(find(v1) == find(v2)); - if (v1 == v2) { - return; - } - m_todo.push_back(var_frame(v1, 0)); - m_justtrail.reset(); - m_marked.reserve(m_eqs.size(), false); - SASSERT(m_marked_trail.empty()); - m_marked[v1.index()] = true; - m_marked_trail.push_back(v1.index()); - while (true) { - SASSERT(!m_todo.empty()); - var_frame& f = m_todo.back(); - signed_var v = f.m_var; - if (v == v2) { - break; - } - auto const& next = m_eqs[v.index()]; - bool seen_all = true; - unsigned sz = next.size(); - for (unsigned i = f.m_index; seen_all && i < sz; ++i) { - eq_edge const& jv = next[i]; - signed_var v3 = jv.m_var; - if (!m_marked[v3.index()]) { - seen_all = false; - f.m_index = i + 1; - m_todo.push_back(var_frame(v3, 0)); - m_justtrail.push_back(jv.m_just); - m_marked_trail.push_back(v3.index()); - m_marked[v3.index()] = true; - } - } - if (seen_all) { - m_todo.pop_back(); - m_justtrail.pop_back(); - } - } - - for (eq_justification const& j : m_justtrail) { - j.explain(e); - } - m_stats.m_num_explains += m_justtrail.size(); - m_stats.m_num_explain_calls++; - m_todo.reset(); - m_justtrail.reset(); - for (unsigned idx : m_marked_trail) { - m_marked[idx] = false; - } - m_marked_trail.reset(); - - // IF_VERBOSE(2, verbose_stream() << (double)m_stats.m_num_explains / m_stats.m_num_explain_calls << "\n"); -} - -void var_eqs::explain_bfs(signed_var v1, signed_var v2, lp::explanation& e) const { - SASSERT(find(v1) == find(v2)); - if (v1 == v2) { - return; - } - m_todo.push_back(var_frame(v1, 0)); - m_justtrail.push_back(eq_justification({})); - m_marked.reserve(m_eqs.size(), false); - SASSERT(m_marked_trail.empty()); - m_marked[v1.index()] = true; - m_marked_trail.push_back(v1.index()); - unsigned head = 0; - for (; ; ++head) { - var_frame& f = m_todo[head]; - signed_var v = f.m_var; - if (v == v2) { - break; - } - auto const& next = m_eqs[v.index()]; - unsigned sz = next.size(); - for (unsigned i = sz; i-- > 0; ) { - eq_edge const& jv = next[i]; - signed_var v3 = jv.m_var; - if (!m_marked[v3.index()]) { - m_todo.push_back(var_frame(v3, head)); - m_justtrail.push_back(jv.m_just); - m_marked_trail.push_back(v3.index()); - m_marked[v3.index()] = true; - } - } - } - - while (head != 0) { - m_justtrail[head].explain(e); - head = m_todo[head].m_index; - ++m_stats.m_num_explains; - } - ++m_stats.m_num_explain_calls; - - m_todo.reset(); - m_justtrail.reset(); - for (unsigned idx : m_marked_trail) { - m_marked[idx] = false; - } - m_marked_trail.reset(); - - // IF_VERBOSE(2, verbose_stream() << (double)m_stats.m_num_explains / m_stats.m_num_explain_calls << "\n"); -} - - -std::ostream& var_eqs::display(std::ostream& out) const { - m_uf.display(out); - unsigned idx = 0; - for (auto const& edges : m_eqs) { - if (!edges.empty()) { - auto v = signed_var(idx); - out << v << " root: " << find(v) << " : "; - for (auto const& jv : edges) { - out << jv.m_var << " "; - } - out << "\n"; - } - ++idx; - } - return out; -} - -} diff --git a/src/util/lp/var_eqs.h b/src/util/lp/var_eqs.h index df673f163..7c4d95ff1 100644 --- a/src/util/lp/var_eqs.h +++ b/src/util/lp/var_eqs.h @@ -45,13 +45,7 @@ public: } }; -class var_eqs_merge_handler { -public: - virtual void merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1) = 0; - virtual void after_merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1) = 0; - virtual void unmerge_eh(signed_var r2, signed_var r1) = 0; -}; - +template class var_eqs { struct eq_edge { signed_var m_var; @@ -70,7 +64,7 @@ class var_eqs { stats() { memset(this, 0, sizeof(*this)); } }; - var_eqs_merge_handler* m_merge_handler; + T* m_merge_handler; union_find m_uf; svector> m_trail; unsigned_vector m_trail_lim; @@ -83,30 +77,61 @@ class var_eqs { mutable svector m_justtrail; mutable stats m_stats; -public: - var_eqs(); - +public: + var_eqs(): m_merge_handler(nullptr), m_uf(*this), m_stack(*this) {} /** - \brief push a scope - */ - void push(); + \brief push a scope */ + void push() { + m_trail_lim.push_back(m_trail.size()); + m_stack.push_scope(); + } /** \brief pop n scopes */ - void pop(unsigned n); + void pop(unsigned n) { + unsigned old_sz = m_trail_lim[m_trail_lim.size() - n]; + for (unsigned i = m_trail.size(); i-- > old_sz; ) { + auto const& sv = m_trail[i]; + m_eqs[sv.first.index()].pop_back(); + m_eqs[sv.second.index()].pop_back(); + m_eqs[(~sv.first).index()].pop_back(); + m_eqs[(~sv.second).index()].pop_back(); + } + m_trail_lim.shrink(m_trail_lim.size() - n); + m_trail.shrink(old_sz); + m_stack.pop_scope(n); + } /** \brief merge equivalence classes for v1, v2 with justification j */ - void merge(signed_var v1, signed_var v2, eq_justification const& j); + void merge(signed_var v1, signed_var v2, eq_justification const& j) { + unsigned max_i = std::max(v1.index(), v2.index()) + 2; + m_eqs.reserve(max_i); + while (m_uf.get_num_vars() <= max_i) m_uf.mk_var(); + m_trail.push_back(std::make_pair(v1, v2)); + m_uf.merge(v1.index(), v2.index()); + m_uf.merge((~v1).index(), (~v2).index()); + m_eqs[v1.index()].push_back(eq_edge(v2, j)); + m_eqs[v2.index()].push_back(eq_edge(v1, j)); + m_eqs[(~v1).index()].push_back(eq_edge(~v2, j)); + m_eqs[(~v2).index()].push_back(eq_edge(~v1, j)); + } + void merge_plus(lpvar v1, lpvar v2, eq_justification const& j) { merge(signed_var(v1, false), signed_var(v2, false), j); } void merge_minus(lpvar v1, lpvar v2, eq_justification const& j) { merge(signed_var(v1, false), signed_var(v2, true), j); } /** \brief find equivalence class representative for v */ - signed_var find(signed_var v) const; + signed_var find(signed_var v) const { + if (v.index() >= m_uf.get_num_vars()) { + return v; + } + unsigned idx = m_uf.find(v.index()); + return signed_var(idx); + } inline signed_var find(lpvar j) const { return find(signed_var(j, false)); @@ -132,8 +157,109 @@ public: \brief Returns eq_justifications for \pre find(v1) == find(v2) */ - void explain_dfs(signed_var v1, signed_var v2, lp::explanation& e) const; - void explain_bfs(signed_var v1, signed_var v2, lp::explanation& e) const; + void explain_dfs(signed_var v1, signed_var v2, lp::explanation& e) const { + SASSERT(find(v1) == find(v2)); + if (v1 == v2) { + return; + } + m_todo.push_back(var_frame(v1, 0)); + m_justtrail.reset(); + m_marked.reserve(m_eqs.size(), false); + SASSERT(m_marked_trail.empty()); + m_marked[v1.index()] = true; + m_marked_trail.push_back(v1.index()); + while (true) { + SASSERT(!m_todo.empty()); + var_frame& f = m_todo.back(); + signed_var v = f.m_var; + if (v == v2) { + break; + } + auto const& next = m_eqs[v.index()]; + bool seen_all = true; + unsigned sz = next.size(); + for (unsigned i = f.m_index; seen_all && i < sz; ++i) { + eq_edge const& jv = next[i]; + signed_var v3 = jv.m_var; + if (!m_marked[v3.index()]) { + seen_all = false; + f.m_index = i + 1; + m_todo.push_back(var_frame(v3, 0)); + m_justtrail.push_back(jv.m_just); + m_marked_trail.push_back(v3.index()); + m_marked[v3.index()] = true; + } + } + if (seen_all) { + m_todo.pop_back(); + m_justtrail.pop_back(); + } + } + + for (eq_justification const& j : m_justtrail) { + j.explain(e); + } + m_stats.m_num_explains += m_justtrail.size(); + m_stats.m_num_explain_calls++; + m_todo.reset(); + m_justtrail.reset(); + for (unsigned idx : m_marked_trail) { + m_marked[idx] = false; + } + m_marked_trail.reset(); + + // IF_VERBOSE(2, verbose_stream() << (double)m_stats.m_num_explains / m_stats.m_num_explain_calls << "\n"); + } + + void explain_bfs(signed_var v1, signed_var v2, lp::explanation& e) const { + SASSERT(find(v1) == find(v2)); + if (v1 == v2) { + return; + } + m_todo.push_back(var_frame(v1, 0)); + m_justtrail.push_back(eq_justification({})); + m_marked.reserve(m_eqs.size(), false); + SASSERT(m_marked_trail.empty()); + m_marked[v1.index()] = true; + m_marked_trail.push_back(v1.index()); + unsigned head = 0; + for (; ; ++head) { + var_frame& f = m_todo[head]; + signed_var v = f.m_var; + if (v == v2) { + break; + } + auto const& next = m_eqs[v.index()]; + unsigned sz = next.size(); + for (unsigned i = sz; i-- > 0; ) { + eq_edge const& jv = next[i]; + signed_var v3 = jv.m_var; + if (!m_marked[v3.index()]) { + m_todo.push_back(var_frame(v3, head)); + m_justtrail.push_back(jv.m_just); + m_marked_trail.push_back(v3.index()); + m_marked[v3.index()] = true; + } + } + } + + while (head != 0) { + m_justtrail[head].explain(e); + head = m_todo[head].m_index; + ++m_stats.m_num_explains; + } + ++m_stats.m_num_explain_calls; + + m_todo.reset(); + m_justtrail.reset(); + for (unsigned idx : m_marked_trail) { + m_marked[idx] = false; + } + m_marked_trail.reset(); + + // IF_VERBOSE(2, verbose_stream() << (double)m_stats.m_num_explains / m_stats.m_num_explain_calls << "\n"); + } + inline void explain(signed_var v1, signed_var v2, lp::explanation& e) const { explain_bfs(v1, v2, e); @@ -176,10 +302,25 @@ public: eq_class equiv_class(lpvar v) { return equiv_class(signed_var(v, false)); } - std::ostream& display(std::ostream& out) const; + std::ostream& display(std::ostream& out) const { + m_uf.display(out); + unsigned idx = 0; + for (auto const& edges : m_eqs) { + if (!edges.empty()) { + auto v = signed_var(idx); + out << v << " root: " << find(v) << " : "; + for (auto const& jv : edges) { + out << jv.m_var << " "; + } + out << "\n"; + } + ++idx; + } + return out; + } // union find event handlers - void set_merge_handler(var_eqs_merge_handler* mh) { m_merge_handler = mh; } + void set_merge_handler(T* mh) { m_merge_handler = mh; } // this method is required by union_find trail_stack & get_trail_stack() { return m_stack; } @@ -203,6 +344,7 @@ public: } }; // end of var_eqs -inline std::ostream& operator<<(var_eqs const& ve, std::ostream& out) { return ve.display(out); } +template +std::ostream& operator<<(var_eqs const& ve, std::ostream& out) { return ve.display(out); } }