From 45b72d77903f29819c04bd57260251b3c83591a6 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 14 May 2019 17:20:08 -0700 Subject: [PATCH] use union_find in emonomials Signed-off-by: Lev Nachmanson --- src/util/lp/emonomials.cpp | 99 ++++++++++++++++++++++++++------------ src/util/lp/emonomials.h | 54 +++++++++++++++++---- src/util/lp/monomial.h | 8 +-- src/util/lp/nla_core.cpp | 44 ++++------------- src/util/lp/nla_core.h | 2 +- 5 files changed, 123 insertions(+), 84 deletions(-) diff --git a/src/util/lp/emonomials.cpp b/src/util/lp/emonomials.cpp index c6bcf89fe..659d9f141 100644 --- a/src/util/lp/emonomials.cpp +++ b/src/util/lp/emonomials.cpp @@ -36,7 +36,8 @@ void emonomials::inc_visited() const { } } -void emonomials::push() { +void emonomials::push() { + m_u_f_stack.push_scope(); m_lim.push_back(m_monomials.size()); m_region.push_scope(); m_ve.push(); @@ -48,7 +49,7 @@ void emonomials::pop(unsigned n) { unsigned old_sz = m_lim[m_lim.size() - n]; for (unsigned i = m_monomials.size(); i-- > old_sz; ) { monomial & m = m_monomials[i]; - remove_cg(i, m); + remove_cg_mon(m); m_var2index[m.var()] = UINT_MAX; lpvar last_var = UINT_MAX; for (lpvar v : m.vars()) { @@ -63,6 +64,12 @@ void emonomials::pop(unsigned n) { m_region.pop_scope(n); m_lim.shrink(m_lim.size() - n); SASSERT(monomials_are_canonized()); + m_mons_to_rehash.clear(); + m_u_f_stack.pop_scope(n); + for (unsigned j : m_mons_to_rehash) { + remove_cg_mon(m_monomials[j]); + insert_cg_mon(m_monomials[j]); + } } void emonomials::remove_cell(head_tail& v, unsigned mIndex) { @@ -161,32 +168,18 @@ void emonomials::remove_cg(lpvar v) { monomial & m = m_monomials[idx]; if (!is_visited(m)) { set_visited(m); - remove_cg(idx, m); + remove_cg_mon(m); } } while (c != first); } -void emonomials::remove_cg(unsigned idx, monomial& m) { - monomial& sv = m_monomials[idx]; - unsigned next = sv.next(); - unsigned prev = sv.prev(); - - +void emonomials::remove_cg_mon(const monomial& m) { lpvar u = m.var(), w; // equivalence class of u: - if (m_cg_table.find(u, w) && w == u) { + if (m_cg_table.find(u, w)) { + TRACE("nla_solver", tout << "erase << " << m << "\n";); m_cg_table.erase(u); - // insert other representative: - if (prev != idx) { - m_cg_table.insert(m_monomials[prev].var()); - } - } - if (prev != idx) { - m_monomials[next].prev() = prev; - m_monomials[prev].next() = next; - sv.next() = idx; - sv.prev() = idx; } } @@ -212,28 +205,69 @@ void emonomials::insert_cg(lpvar v) { monomial & m = m_monomials[idx]; if (!is_visited(m)) { set_visited(m); - insert_cg(idx, m); + insert_cg_mon(m); } } while (c != first); } -void emonomials::insert_cg(unsigned idx, monomial & m) { +bool emonomials::elists_are_consistent(std::unordered_map, hash_svector>& lists) const { + for (auto const & m : m_monomials) { + auto it = lists.find(m.rvars()); + if (it == lists.end()) { + std::unordered_set v; + v.insert(m.var()); + lists[m.rvars()] = v; + } else { + it->second.insert(m.var()); + } + } + for (auto const & m : m_monomials) { + SASSERT(is_canonized(m)); + if (!is_canonical_monomial(m.var())) + continue; + std::unordered_set c; + for (const monomial& e : enum_sign_equiv_monomials(m)) + c.insert(e.var()); + auto it = lists.find(m.rvars()); + + CTRACE("nla_solver", it->second != c, + tout << "m = " << m << "\n"; + tout << "c = " ; print_vector(c, tout); tout << "\n"; + if (it == lists.end()) { + tout << "m.rvars are not found\n"; + } + else { + tout << "it->second = "; print_vector(it->second, tout); tout << "\n"; + for (unsigned j : it->second) { + tout << (*this)[j] << "\n"; + } + }); + SASSERT(c == it->second); + } + return true; +} + + +void emonomials::insert_cg_mon(monomial & m) { do_canonize(m); lpvar v = m.var(), w; if (m_cg_table.find(v, w)) { - SASSERT(w != v); - unsigned idxr = m_var2index[w]; - unsigned idxl = m_monomials[idxr].prev(); - m_monomials[idx].next() = idxr; - m_monomials[idx].prev() = idxl; - m_monomials[idxr].prev() = idx; - m_monomials[idxl].next() = idx; + if (v == w) { + TRACE("nla_solver", tout << "found " << v << "\n";); + return; + } + unsigned v_idx = m_var2index[v]; + unsigned w_idx = m_var2index[w]; + unsigned max_i = std::max(v_idx, w_idx); + while (m_u_f.get_num_vars() <= max_i) + m_u_f.mk_var(); + TRACE("nla_solver", tout << "merge " << v << " idx " << v_idx << ", and " << w << " idx " << w_idx << "\n";); + m_u_f.merge(v_idx, w_idx); } else { + TRACE("nla_solver", tout << "insert " << m << "\n";); m_cg_table.insert(v); - SASSERT(m_monomials[idx].next() == idx); - SASSERT(m_monomials[idx].prev() == idx); } } @@ -267,7 +301,7 @@ void emonomials::add(lpvar v, unsigned sz, lpvar const* vs) { } SASSERT(m_ve.is_root(v)); m_var2index.setx(v, idx, UINT_MAX); - insert_cg(idx, m_monomials[idx]); + insert_cg_mon(m_monomials[idx]); } void emonomials::do_canonize(monomial & m) const { @@ -349,6 +383,7 @@ void emonomials::after_merge_eh(signed_var r2, signed_var r1, signed_var v2, sig TRACE("nla_solver", tout << r2 << " <- " << r1 << "\n";); if (m_ve.find(~r1) == m_ve.find(~r2)) { // the other sign has also been merged m_use_lists.reserve(std::max(r2.var(), r1.var()) + 1); + TRACE("nla_solver", tout << "rehasing " << r1.var() << "\n";); rehash_cg(r1.var()); merge_cells(m_use_lists[r2.var()], m_use_lists[r1.var()]); } diff --git a/src/util/lp/emonomials.h b/src/util/lp/emonomials.h index 76ae6f5a2..23611da45 100644 --- a/src/util/lp/emonomials.h +++ b/src/util/lp/emonomials.h @@ -27,6 +27,12 @@ namespace nla { +struct hash_svector { + size_t operator()(const unsigned_vector & v) const { + return svector_hash()(v); + } +}; + class core; class emonomials { @@ -73,9 +79,12 @@ class emonomials { return uvec == vvec; } }; - - mutable svector m_find_key; // the key used when looking for a monomial with the specific variables - var_eqs& m_ve; + + union_find m_u_f; + trail_stack m_u_f_stack; + std::unordered_set m_mons_to_rehash; + mutable svector m_find_key; // the key used when looking for a monomial with the specific variables + 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 @@ -86,6 +95,7 @@ class emonomials { eq_canonical m_cg_eq; hashtable m_cg_table; // congruence (canonical) table. + void inc_visited() const; void remove_cell(head_tail& v, unsigned mIndex); @@ -95,8 +105,8 @@ class emonomials { void remove_cg(lpvar v); void insert_cg(lpvar v); - void insert_cg(unsigned idx, monomial & m); - void remove_cg(unsigned idx, monomial & m); + void insert_cg_mon(monomial & m); + void remove_cg_mon(const monomial & m); void rehash_cg(lpvar v) { remove_cg(v); insert_cg(v); } void do_canonize(monomial& m) const; @@ -110,7 +120,9 @@ 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_u_f(*this), + m_u_f_stack(*this), m_ve(ve), m_visited(0), m_cg_hash(*this), @@ -119,6 +131,18 @@ public: m_ve.set_merge_handler(this); } + void unmerge_eh(unsigned i, unsigned j) { + TRACE("nla_solver", tout << "unmerged " << i << " and " << j << "\n";); + m_mons_to_rehash.insert(i); + m_mons_to_rehash.insert(j); + } + + void merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) {} + void after_merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) {} + + // this method is required by union_find + trail_stack & get_trail_stack() { return m_u_f_stack; } + /** \brief push/pop scopes. The life-time of a merge is local within a scope. @@ -229,7 +253,13 @@ public: products_of get_products_of(lpvar v) const { inc_visited(); return products_of(*this, v); } monomial const* find_canonical(svector const& vars) const; - + bool is_canonical_monomial(lpvar j) const { + SASSERT(is_monomial_var(j)); + unsigned idx = m_var2index[j]; + if (idx >= m_u_f.get_num_vars()) + return true; + return m_u_f.find(idx) == idx; + } /** \brief iterator over sign equivalent monomials. These are monomials that are equivalent modulo m_var_eqs amd modulo signs. @@ -245,8 +275,9 @@ public: monomial const& operator*() { return m.m_monomials[m_index]; } sign_equiv_monomials_it& operator++() { - m_touched = true; - m_index = m.m_monomials[m_index].next(); + m_touched = true; + if (m_index < m.m_u_f.get_num_vars()) + m_index = m.m_u_f.next(m_index); return *this; } @@ -295,7 +326,10 @@ public: 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; } -}; + + bool elists_are_consistent(std::unordered_map, hash_svector> &lists) const; + +}; // end of emonomials struct pp_emons { const core& m_c; diff --git a/src/util/lp/monomial.h b/src/util/lp/monomial.h index 48e2f4a35..e6b8c8930 100644 --- a/src/util/lp/monomial.h +++ b/src/util/lp/monomial.h @@ -43,21 +43,15 @@ class monomial: public mon_eq { // fields svector m_rvars; bool m_rsign; - unsigned m_next; // next congruent node. - unsigned m_prev; // previous congruent node mutable unsigned m_visited; public: // constructors monomial(lpvar v, unsigned sz, lpvar const* vs, unsigned idx): monomial(v, svector(sz, vs), idx) { } - monomial(lpvar v, const svector &vs, unsigned idx) : mon_eq(v, vs), m_rsign(false), m_next(idx), m_prev(idx), m_visited(0) { + monomial(lpvar v, const svector &vs, unsigned idx) : mon_eq(v, vs), m_rsign(false), m_visited(0) { std::sort(vars().begin(), vars().end()); } - 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& rvars() const { return m_rvars; } diff --git a/src/util/lp/nla_core.cpp b/src/util/lp/nla_core.cpp index aeee919da..7f659660d 100644 --- a/src/util/lp/nla_core.cpp +++ b/src/util/lp/nla_core.cpp @@ -133,7 +133,8 @@ void core::push() { void core::pop(unsigned n) { TRACE("nla_solver", tout << "n = " << n << "\n";); - m_emons.pop(n); + m_emons.pop(n); + SASSERT(elists_are_consistent(false)); } rational core::product_value(const unsigned_vector & m) const { @@ -811,11 +812,7 @@ bool core::find_canonical_monomial_of_vars(const svector& vars, lpvar & i } bool core::is_canonical_monomial(lpvar j) const { - const monomial & m = m_emons[j]; - unsigned k; - SASSERT(find_canonical_monomial_of_vars(m.rvars(), k)); - find_canonical_monomial_of_vars(m.rvars(), k); - return j == k; + return m_emons.is_canonical_monomial(j); } @@ -1366,6 +1363,7 @@ void core::clear() { void core::init_search() { clear(); init_vars_equivalence(); + SASSERT(elists_are_consistent(false)); } void core::init_to_refine() { @@ -1866,7 +1864,7 @@ lbool core:: inner_check(bool derived) { } if (derived) continue; TRACE("nla_solver", tout << "passed derived and basic lemmas\n";); - SASSERT(elists_are_consistent()); + SASSERT(elists_are_consistent(true)); if (search_level == 1) { m_order.order_lemma(); } else { // search_level == 2 @@ -1877,12 +1875,6 @@ lbool core:: inner_check(bool derived) { return m_lemma_vec->empty()? l_undef : l_false; } -struct hash_svector { - size_t operator()(const unsigned_vector & v) const { - return svector_hash()(v); - } -}; - bool core::elist_is_consistent(const std::unordered_set & list) const { bool first = true; bool p; @@ -1897,29 +1889,13 @@ bool core::elist_is_consistent(const std::unordered_set & list) const { return true; } -bool core::elists_are_consistent() const { - +bool core::elists_are_consistent(bool check_in_model) const { std::unordered_map, hash_svector> lists; - for (auto const & m : m_emons) { - auto it = lists.find(m.rvars()); - if (it == lists.end()) { - std::unordered_set v; - v.insert(m.var()); - lists[m.rvars()] = v; - } else { - it->second.insert(m.var()); - } - } - for (auto const & m : m_emons) { - if (!is_canonical_monomial(m.var())) - continue; - std::unordered_set c; - for (const monomial& e : m_emons.enum_sign_equiv_monomials(m)) - c.insert(e.var()); - auto it = lists.find(m.rvars()); - SASSERT(it->second == c); - } + if (!m_emons.elists_are_consistent(lists)) + return false; + if (!check_in_model) + return true; for (const auto & p : lists) { if (! elist_is_consistent(p.second)) return false; diff --git a/src/util/lp/nla_core.h b/src/util/lp/nla_core.h index 75b5c4173..f369b07e8 100644 --- a/src/util/lp/nla_core.h +++ b/src/util/lp/nla_core.h @@ -241,7 +241,7 @@ public: bool find_canonical_monomial_of_vars(const svector& vars, lpvar & i) const; bool is_canonical_monomial(lpvar) const; - bool elists_are_consistent() const; + bool elists_are_consistent(bool check_in_model) const; bool elist_is_consistent(const std::unordered_set&) const; bool var_has_positive_lower_bound(lpvar j) const;