From 7a3a696b6f69d367ba839a685a9da45d1e6dcf68 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 3 Apr 2019 15:24:55 -0700 Subject: [PATCH] debugging var_eqs --- src/util/lp/nla_solver.cpp | 60 ++++---- src/util/lp/var_eqs.cpp | 10 +- src/util/lp/var_eqs.h | 285 ++++++++++++++++++------------------- 3 files changed, 179 insertions(+), 176 deletions(-) diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index 40d674231..5238c7e8a 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -34,9 +34,11 @@ bool try_insert(const A& elem, B& collection) { collection.insert(elem); return true; } + typedef lp::constraint_index lpci; typedef lp::lconstraint_kind llc; + struct point { rational x; rational y; @@ -86,7 +88,7 @@ struct solver::imp { }; //fields - var_eqs m_vars_equivalence; + var_eqs m_evars; vector m_monomials; rooted_mon_table m_rm_table; @@ -114,7 +116,7 @@ struct solver::imp { imp(lp::lar_solver& s, reslimit& lim, params_ref const& p) : - m_vars_equivalence(), + m_evars(), m_lar_solver(s) // m_limit(lim), // m_params(p) @@ -201,7 +203,7 @@ struct solver::imp { } rational canonize_sign_of_var(lpvar j) const { - return m_vars_equivalence.find_sign(j); + return m_evars.find(j).rsign(); } // the value of the rooted monomias is equal to the value of the variable multiplied @@ -222,6 +224,7 @@ struct solver::imp { void push() { TRACE("nla_solver",); m_monomials_counts.push_back(m_monomials.size()); + m_evars.push(); } void deregister_monomial_from_rooted_monomials (const monomial & m, unsigned i){ @@ -247,7 +250,8 @@ struct solver::imp { deregister_monomial_from_tables(m_monomials[i], i); } m_monomials.shrink(new_size); - m_monomials_counts.shrink(m_monomials_counts.size() - n); + m_monomials_counts.shrink(m_monomials_counts.size() - n); + m_evars.pop(n); } rational mon_value_by_vars(unsigned i) const { @@ -287,7 +291,7 @@ struct solver::imp { } void explain(lpvar j, lp::explanation& exp) const { - m_vars_equivalence.explain(j, exp); + m_evars.explain(j, exp); } template @@ -616,17 +620,17 @@ struct solver::imp { // svector reduce_monomial_to_rooted(const svector & vars, rational & sign) const { svector ret; - sign = 1; + bool s = false; for (lpvar v : vars) { - unsigned root = m_vars_equivalence.find(v, sign); - SASSERT(m_vars_equivalence.is_root(root)); + auto root = m_evars.find(v); + s ^= root.sign(); TRACE("nla_solver_eq", print_var(v,tout); tout << " mapped to "; - - print_var(root, tout);); - ret.push_back(root); + print_var(root.var(), tout);); + ret.push_back(root.var()); } + sign = rational(s? -1: 1); std::sort(ret.begin(), ret.end()); return ret; } @@ -844,10 +848,10 @@ struct solver::imp { /* unsigned_vector eq_vars(lpvar j) const { TRACE("nla_solver_eq", tout << "j = "; print_var(j, tout); tout << "eqs = "; - for(auto jj : m_vars_equivalence.eq_vars(j)) { + for(auto jj : m_evars.eq_vars(j)) { print_var(jj, tout); }); - return m_vars_equivalence.eq_vars(j); + return m_evars.eq_vars(j); } */ // Monomials m and n vars have the same values, up to "sign" @@ -1091,7 +1095,7 @@ struct solver::imp { if (!(var_has_positive_lower_bound(j) || var_has_negative_upper_bound(j))) { return 0; } - sign *= m_vars_equivalence.find_sign(j); + sign *= m_evars.find(j).rsign(); } return rat_sign(sign); } @@ -1339,13 +1343,13 @@ struct solver::imp { bool vars_are_equiv(lpvar a, lpvar b) const { SASSERT(abs(vvr(a)) == abs(vvr(b))); - return m_vars_equivalence.vars_are_equiv(a, b); + return m_evars.vars_are_equiv(a, b); } void explain_equiv_vars(lpvar a, lpvar b) { SASSERT(abs(vvr(a)) == abs(vvr(b))); - if (m_vars_equivalence.vars_are_equiv(a, b)) { + if (m_evars.vars_are_equiv(a, b)) { explain(a, current_expl()); explain(b, current_expl()); } else { @@ -1864,9 +1868,9 @@ struct solver::imp { auto c2 = m_lar_solver.get_column_upper_bound_witness(v[k]); auto c3 = m_lar_solver.get_column_lower_bound_witness(v[k]); if (vvr(head) == vvr(v[k])) - m_vars_equivalence.merge_plus(head, v[k], eq_justification({c0, c1, c2, c3})); + m_evars.merge_plus(head, v[k], eq_justification({c0, c1, c2, c3})); else - m_vars_equivalence.merge_minus(head, v[k], eq_justification({c0, c1, c2, c3})); + m_evars.merge_minus(head, v[k], eq_justification({c0, c1, c2, c3})); } } } @@ -1895,16 +1899,16 @@ struct solver::imp { SASSERT(j != static_cast(-1)); bool sign = (seen_minus && seen_plus)? false : true; if (sign) - m_vars_equivalence.merge_minus(i, j, eq_justification({c0, c1})); + m_evars.merge_minus(i, j, eq_justification({c0, c1})); else - m_vars_equivalence.merge_plus(i, j, eq_justification({c0, c1})); + m_evars.merge_plus(i, j, eq_justification({c0, c1})); } // x is equivalent to y if x = +- y void init_vars_equivalence() { - /* SASSERT(m_vars_equivalence.empty());*/ + /* SASSERT(m_evars.empty());*/ collect_equivs(); - /* TRACE("nla_solver_details", tout << "number of equivs = " << m_vars_equivalence.size(););*/ + /* TRACE("nla_solver_details", tout << "number of equivs = " << m_evars.size(););*/ SASSERT((settings().random_next() % 100) || tables_are_ok()); } @@ -1932,7 +1936,7 @@ struct solver::imp { bool rm_table_is_ok() const { for (const auto & rm : m_rm_table.rms()) { for (lpvar j : rm.vars()) { - if (!m_vars_equivalence.is_root(j)){ + if (!m_evars.is_root(j)){ TRACE("nla_solver", print_var(j, tout);); return false; } @@ -1945,7 +1949,7 @@ struct solver::imp { return vars_table_is_ok() && rm_table_is_ok(); } - bool var_is_a_root(lpvar j) const { return m_vars_equivalence.is_root(j); } + bool var_is_a_root(lpvar j) const { return m_evars.is_root(j); } template bool vars_are_roots(const T& v) const { @@ -2244,7 +2248,7 @@ struct solver::imp { SASSERT(abs(vvr(i)) == abs(vvr(c))); auto it = m_var_to_its_monomial.find(i); if (it == m_var_to_its_monomial.end()) { - i = m_vars_equivalence.find(i); + i = m_evars.find(i).var(); if (try_insert(i, found_vars)) { r.push_back(factor(i, factor_type::VAR)); } @@ -2382,7 +2386,7 @@ struct solver::imp { void order_lemma_on_factor_binomial_explore(const monomial& m, unsigned k) { SASSERT(m.size() == 2); lpvar c = m[k]; - lpvar d = m_vars_equivalence.find(c); + lpvar d = m_evars.find(c).var(); auto it = m_rm_table.var_map().find(d); SASSERT(it != m_rm_table.var_map().end()); for (unsigned bd_i : it->second) { @@ -2393,7 +2397,7 @@ struct solver::imp { } void order_lemma_on_factor_binomial_rm(const monomial& ac, unsigned k, const rooted_mon& rm_bd) { - factor d(m_vars_equivalence.find(ac[k]), factor_type::VAR); + factor d(m_evars.find(ac[k]).var(), factor_type::VAR); factor b; if (!divide(rm_bd, d, b)) return; @@ -2407,7 +2411,7 @@ struct solver::imp { int p = (k + 1) % 2; lpvar a = ac[p]; lpvar c = ac[k]; - SASSERT(m_vars_equivalence.find(c) == d); + SASSERT(m_evars.find(c).var() == d); rational acv = vvr(ac); rational av = vvr(a); rational c_sign = rrat_sign(vvr(c)); diff --git a/src/util/lp/var_eqs.cpp b/src/util/lp/var_eqs.cpp index bd120cf17..273e47b3b 100644 --- a/src/util/lp/var_eqs.cpp +++ b/src/util/lp/var_eqs.cpp @@ -20,7 +20,6 @@ #include "util/lp/var_eqs.h" - namespace nla { @@ -40,13 +39,13 @@ namespace nla { m_eqs[(~sv.first).index()].pop_back(); m_eqs[(~sv.second).index()].pop_back(); } - m_trail_lim.shrink(n); + m_trail_lim.shrink(m_trail_lim.size() - n); m_trail.shrink(old_sz); m_ufctx.get_trail_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()) + 1; + 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_uf.merge(v1.index(), v2.index()); @@ -62,7 +61,7 @@ namespace nla { return v; } unsigned idx = m_uf.find(v.index()); - return signed_var(idx); + return signed_var(idx, from_index()); // 0 is needed to call the right constructor } void var_eqs::explain(signed_var v1, signed_var v2, lp::explanation& e) const { @@ -85,7 +84,7 @@ namespace nla { auto const& next = m_eqs[v.index()]; unsigned sz = next.size(); bool seen_all = true; - for (unsigned i = f.m_index; !seen_all && i < sz; ++i) { + for (unsigned i = f.m_index; seen_all && i < sz; ++i) { justified_var const& jv = next[i]; if (!m_marked[jv.m_var.index()]) { seen_all = false; @@ -104,6 +103,7 @@ namespace nla { for (eq_justification const& j : m_dfs_trail) { j.explain(e); } + m_todo.reset(); m_dfs_trail.reset(); for (unsigned idx : m_marked_trail) { m_marked[idx] = false; diff --git a/src/util/lp/var_eqs.h b/src/util/lp/var_eqs.h index aff7ec9c6..32cc45cd0 100644 --- a/src/util/lp/var_eqs.h +++ b/src/util/lp/var_eqs.h @@ -26,157 +26,156 @@ namespace nla { typedef lp::var_index lpvar; -typedef lp::constraint_index lpcindex; +typedef lp::constraint_index lpci; +struct from_index{}; - class signed_var { - unsigned m_sv; - public: - // constructor, sign = true means minus - signed_var(lpvar v, bool sign): m_sv((v << 1) + (sign ? 1 : 0)) {} - // constructor - explicit signed_var(unsigned sv): m_sv(sv) {} - bool sign() const { return 0 != (m_sv & 0x1); } - lpvar var() const { return m_sv >> 1; } - unsigned index() const { return m_sv; } - void neg() { m_sv = m_sv ^ 1; } - friend signed_var operator~(signed_var const& sv) { - return signed_var(sv.var(), !sv.sign()); - } - bool operator==(signed_var const& other) const { - return m_sv == other.m_sv; - } - bool operator!=(signed_var const& other) const { - return m_sv != other.m_sv; - } - }; +class signed_var { + unsigned m_sv; +public: + // constructor, sign = true means minus + signed_var(lpvar v, bool sign): m_sv((v << 1) + (sign ? 1 : 0)) {} + // constructor + signed_var(unsigned sv, from_index): m_sv(sv) {} + bool sign() const { return 0 != (m_sv & 0x1); } + lpvar var() const { return m_sv >> 1; } + unsigned index() const { return m_sv; } + void neg() { m_sv = m_sv ^ 1; } + friend signed_var operator~(signed_var const& sv) { + return signed_var(sv.var(), !sv.sign()); + } + bool operator==(signed_var const& other) const { + return m_sv == other.m_sv; + } + bool operator!=(signed_var const& other) const { + return m_sv != other.m_sv; + } + rational rsign() const { return sign() ? rational::minus_one() : rational::one(); } +}; - - class eq_justification { - svector m_cs; - public: - eq_justification(std::initializer_list cs) { - for (lpcindex c: cs) - m_cs.push_back(c); +class eq_justification { + lpci m_cs[4]; +public: + eq_justification(std::initializer_list cs) { + int i = 0; + for (lpci c: cs) { + m_cs[i++] = c; } - void explain(lp::explanation& e) const { - for (lpcindex c : m_cs) + for (; i < 4; i++) { + m_cs[i] = -1; + } + } + + void explain(lp::explanation& e) const { + for (lpci c : m_cs) + if (c + 1 != 0) // c != -1 e.add(c); + } +}; + +class var_eqs { + struct justified_var { + signed_var m_var; + eq_justification m_j; + justified_var(signed_var v, eq_justification const& j): m_var(v), m_j(j) {} + }; + typedef svector justified_vars; + + struct dfs_frame { + signed_var m_var; + unsigned m_index; + dfs_frame(signed_var v, unsigned i): m_var(v), m_index(i) {} + }; + typedef std::pair signed_var_pair; + + union_find_default_ctx m_ufctx; + union_find<> m_uf; + svector m_trail; + unsigned_vector m_trail_lim; + vector m_eqs; // signed_var-index -> justified_var corresponding to edges in a graph used to extract justifications. + + mutable svector m_todo; + mutable svector m_marked; + mutable unsigned_vector m_marked_trail; + mutable svector m_dfs_trail; + +public: + var_eqs(); + + /** + \brief push a scope + */ + void push(); + + /** + \brief pop n scopes + */ + void pop(unsigned 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_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; + + inline signed_var find(lpvar j) const { + return find(signed_var(j, false)); + } + + inline bool is_root(lpvar j) const { + signed_var sv = find(signed_var(j, false)); + return sv.var() == j; + } + bool vars_are_equiv(lpvar j, lpvar k) const { + signed_var sj = find(signed_var(j, false)); + signed_var sk = find(signed_var(k, false)); + return sj.var() == sk.var(); + } + /** + \brief Returns eq_justifications for + \pre find(v1) == find(v2) + */ + void explain(signed_var v1, signed_var v2, lp::explanation& e) const; + inline + void explain(lpvar v1, lpvar v2, lp::explanation & e) const { + return explain(signed_var(v1, false), signed_var(v2, false), e); + } + + inline void explain(lpvar j, lp::explanation& e) const { + signed_var s(j, false); + return explain(find(s), s, e); + } + + class iterator { + var_eqs& m_ve; // context. + unsigned m_idx; // index into a signed variable, same as union-find index + bool m_touched; // toggle between initial and final state + public: + iterator(var_eqs& ve, unsigned idx, bool t) : m_ve(ve), m_idx(idx), m_touched(t) {} + signed_var operator*() const { + return signed_var(m_idx, from_index()); // 0 is needed to call the right constructor } + iterator& operator++() { m_idx = m_ve.m_uf.next(m_idx); m_touched = true; return *this; } + bool operator==(iterator const& other) const { return m_idx == other.m_idx && m_touched == other.m_touched; } + bool operator!=(iterator const& other) const { return m_idx != other.m_idx || m_touched != other.m_touched; } }; - class var_eqs { - struct justified_var { - signed_var m_var; - eq_justification m_j; - justified_var(signed_var v, eq_justification const& j): m_var(v), m_j(j) {} - }; - typedef svector justified_vars; - - struct dfs_frame { - signed_var m_var; - unsigned m_index; - dfs_frame(signed_var v, unsigned i): m_var(v), m_index(i) {} - }; - typedef std::pair signed_var_pair; - - union_find_default_ctx m_ufctx; - union_find<> m_uf; - svector m_trail; - unsigned_vector m_trail_lim; - vector m_eqs; // signed_var-index -> justified_var corresponding to edges in a graph used to extract justifications. - - mutable svector m_todo; - mutable svector m_marked; - mutable unsigned_vector m_marked_trail; - mutable svector m_dfs_trail; - + class eq_class { + var_eqs& m_ve; + signed_var m_v; public: - var_eqs(); + eq_class(var_eqs& ve, signed_var v) : m_ve(ve), m_v(v) {} + iterator begin() { return iterator(m_ve, m_v.index(), false); } + iterator end() { return iterator(m_ve, m_v.index(), true); } + }; - /** - \brief push a scope - */ - void push(); + eq_class equiv_class(signed_var v) { return eq_class(*this, v); } - /** - \brief pop n scopes - */ - void pop(unsigned 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_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; - inline lpvar find(lpvar j, rational& sign) const { - signed_var sv = find(signed_var(j, false)); - sign = sv.sign()? rational(-1) : rational(1); - return sv.var(); - } - - inline rational find_sign(lpvar j) const { - signed_var sv = find(signed_var(j, false)); - return sv.sign()? rational(-1) : rational(1); - } - - inline lpvar find(lpvar j) const { - signed_var sv = find(signed_var(j, false)); - return sv.var(); - } - - inline bool is_root(lpvar j) const { - signed_var sv = find(signed_var(j, false)); - return sv.var() == j; - } - bool vars_are_equiv(lpvar j, lpvar k) const { - signed_var sj = find(signed_var(j, false)); - signed_var sk = find(signed_var(k, false)); - return sj.var() == sk.var(); - } - /** - \brief Returns eq_justifications for - \pre find(v1) == find(v2) - */ - void explain(signed_var v1, signed_var v2, lp::explanation& e) const; - inline - void explain(lpvar v1, lpvar v2, lp::explanation & e) const { - return explain(signed_var(v1), signed_var(v2), e); - } - - inline void explain(lpvar j, lp::explanation& e) const { - signed_var s(j, false); - return explain(find(s), s, e); - } - - class iterator { - var_eqs& m_ve; // context. - unsigned m_idx; // index into a signed variable, same as union-find index - bool m_touched; // toggle between initial and final state - public: - iterator(var_eqs& ve, unsigned idx, bool t) : m_ve(ve), m_idx(idx), m_touched(t) {} - signed_var operator*() const { return signed_var(m_idx); } - iterator& operator++() { m_idx = m_ve.m_uf.next(m_idx); m_touched = true; return *this; } - bool operator==(iterator const& other) const { return m_idx == other.m_idx && m_touched == other.m_touched; } - bool operator!=(iterator const& other) const { return m_idx != other.m_idx || m_touched != other.m_touched; } - }; - - class eq_class { - var_eqs& m_ve; - signed_var m_v; - public: - eq_class(var_eqs& ve, signed_var v) : m_ve(ve), m_v(v) {} - iterator begin() { return iterator(m_ve, m_v.index(), false); } - iterator end() { return iterator(m_ve, m_v.index(), true); } - }; - - eq_class equiv_class(signed_var v) { return eq_class(*this, v); } - - eq_class equiv_class(lpvar v) { return equiv_class(signed_var(v, false)); } - }; + eq_class equiv_class(lpvar v) { return equiv_class(signed_var(v, false)); } +}; }