From 50db22b2b2afe7afdb38ce148dec26b9beda4165 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 24 Mar 2020 00:00:42 -0700 Subject: [PATCH] fix #3407 Signed-off-by: Nikolaj Bjorner --- src/math/lp/emonics.cpp | 20 +++++++++----------- src/math/lp/nla_core.cpp | 2 +- src/math/lp/var_eqs.h | 9 ++++++--- 3 files changed, 16 insertions(+), 15 deletions(-) diff --git a/src/math/lp/emonics.cpp b/src/math/lp/emonics.cpp index e691480e3..7c8435bcf 100644 --- a/src/math/lp/emonics.cpp +++ b/src/math/lp/emonics.cpp @@ -349,11 +349,13 @@ void emonics::add(lpvar v, unsigned sz, lpvar const* vs) { } void emonics::do_canonize(monic & m) const { + TRACE("nla_solver_mons", tout << m << "\n";); m.reset_rfields(); for (lpvar v : m.vars()) { m.push_rvar(m_ve.find(v)); } m.sort_rvars(); + TRACE("nla_solver_mons", tout << m << "\n";); } bool emonics::is_canonized(const monic & m) const { @@ -431,17 +433,19 @@ void emonics::merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v } void emonics::after_merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1) { - if (m_ve.find(~r1) == m_ve.find(~r2)) { // the other sign has also been merged - TRACE("nla_solver_mons", tout << r2 << " <- " << r1 << "\n";); + TRACE("nla_solver_mons", tout << v2 << " <- " << v1 << " : " << r2 << " <- " << r1 << "\n";); + if (r1.var() == r2.var() || m_ve.find(~r1) == m_ve.find(~r2)) { // the other sign has also been merged + TRACE("nla_solver_mons", + display_uf(tout << r2 << " <- " << r1 << "\n"); + tout << "rehashing " << r1.var() << "\n";); m_use_lists.reserve(std::max(r2.var(), r1.var()) + 1); - TRACE("nla_solver_mons", tout << "rehashing " << r1.var() << "\n";); rehash_cg(r1.var()); merge_cells(m_use_lists[r2.var()], m_use_lists[r1.var()]); } } void emonics::unmerge_eh(signed_var r2, signed_var r1) { - if (m_ve.find(~r1) != m_ve.find(~r2)) { // the other sign has also been unmerged + if (r1.var() == r2.var() || m_ve.find(~r1) != m_ve.find(~r2)) { // the other sign has also been unmerged TRACE("nla_solver_mons", tout << r2 << " -> " << r1 << "\n";); unmerge_cells(m_use_lists[r2.var()], m_use_lists[r1.var()]); rehash_cg(r1.var()); @@ -536,12 +540,6 @@ bool emonics::invariant() const { do { auto const& m = m_monics[c->m_index]; bool found = false; -#if 0 - for (lp::var_index w : m.vars()) { - auto w1 = m_ve.find(w); - found |= v1.var() == w1.var(); - } -#endif for (lp::var_index w : m.rvars()) { auto w1 = m_ve.find(w); found |= v1.var() == w1.var(); @@ -573,7 +571,7 @@ bool emonics::invariant() const { }; unsigned idx = 0; for (auto const& m : m_monics) { - CTRACE("nla_solver_mons", !m_cg_table.contains(m.var()), tout << "removed " << m << "\n";); + CTRACE("nla_solver_mons", !m_cg_table.contains(m.var()), tout << "removed " << m << "\n"; ); SASSERT(m_cg_table.contains(m.var())); SASSERT(m_cg_table[m.var()].contains(m.var())); // same with rooted variables diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 4f25f5648..ebc18ec01 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -838,7 +838,7 @@ void core::collect_equivs() { continue; lpvar j = s.external_to_local(lp::tv::mask_term(i)); if (var_is_fixed_to_zero(j)) { - TRACE("nla_solver_eq", tout << "term = "; s.print_term_as_indices(*s.terms()[i], tout);); + TRACE("nla_solver_mons", s.print_term_as_indices(*s.terms()[i], tout << "term = ") << "\n";); add_equivalence_maybe(s.terms()[i], s.get_column_upper_bound_witness(j), s.get_column_lower_bound_witness(j)); } } diff --git a/src/math/lp/var_eqs.h b/src/math/lp/var_eqs.h index 46c6c3f7b..09c00ef36 100644 --- a/src/math/lp/var_eqs.h +++ b/src/math/lp/var_eqs.h @@ -98,7 +98,7 @@ public: 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_eqs[(~sv.second).index()].pop_back(); } m_trail.pop_scope(n); m_stack.pop_scope(n); // this cass takes care of unmerging through union_find m_uf @@ -110,12 +110,15 @@ public: void merge(signed_var v1, signed_var v2, eq_justification const& j) { if (v1 == v2) return; + if (find(v1).var() == find(v2).var()) + return; 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(); + TRACE("nla_solver_mons", tout << v1 << " == " << v2 << " " << m_uf.find(v1.index()) << " == " << m_uf.find(v2.index()) << "\n";); m_trail.push_back(std::make_pair(v1, v2)); m_uf.merge(v1.index(), v2.index()); - 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)); @@ -146,7 +149,7 @@ public: } inline bool is_root(svector v) const { for (lpvar j : v) - if (! is_root(j)) + if (!is_root(j)) return false; return true; }