From 6a1c2e4766fa47c268087f2034f3a5a0c85f8c19 Mon Sep 17 00:00:00 2001 From: Lev Date: Wed, 14 Nov 2018 15:17:16 -0800 Subject: [PATCH] work on order lemma Signed-off-by: Lev --- src/util/lp/nla_solver.cpp | 63 +++++--------------------------- src/util/lp/vars_equivalence.h | 65 ++++++++++++++++++++++++++++++++-- 2 files changed, 71 insertions(+), 57 deletions(-) diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index 646bbc07d..b31efbc52 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -41,10 +41,6 @@ struct solver::imp { hash_svector> m_rooted_monomials; - std::unordered_map, - vector, - hash_vector> - m_abs_vals_to_monomials; // this field is used for the push/pop operations unsigned_vector m_monomials_counts; lp::lar_solver& m_lar_solver; @@ -55,7 +51,9 @@ struct solver::imp { lp::explanation * m_expl; lemma * m_lemma; imp(lp::lar_solver& s, reslimit& lim, params_ref const& p) - : m_lar_solver(s) + : + m_vars_equivalence([this](unsigned h){return vvr(h);}), + m_lar_solver(s) // m_limit(lim), // m_params(p) { @@ -76,12 +74,6 @@ struct solver::imp { m_monomials_counts.push_back(m_monomials.size()); } - void deregister_monomial_from_abs_vals(const monomial & m, unsigned i){ - int sign; - auto key = get_sorted_abs_vals_from_mon(m, sign); - SASSERT(m_abs_vals_to_monomials.find(key)->second.back() == index_with_sign(i, rational(sign))); - m_abs_vals_to_monomials.find(key)->second.pop_back(); - } void deregister_monomial_from_rooted_monomials (const monomial & m, unsigned i){ rational sign = rational(1); @@ -90,7 +82,7 @@ struct solver::imp { } void deregister_monomial_from_tables(const monomial & m, unsigned i){ - deregister_monomial_from_abs_vals(m, i); + m_vars_equivalence.deregister_monomial_from_abs_vals(m, i); deregister_monomial_from_rooted_monomials(m, i); } @@ -355,7 +347,7 @@ struct solver::imp { -ab = a(-b) */ bool basic_sign_lemma() { - for (const auto & p : m_abs_vals_to_monomials){ + for (const auto & p : m_vars_equivalence.monomials_by_abs_values()){ if (basic_sign_lemma_on_a_bucket_of_abs_vals(p.first, p.second)) return true; } @@ -775,53 +767,14 @@ struct solver::imp { } } - vector get_sorted_abs_vals_from_mon(const monomial& m, int & sign) { - sign = 1; - vector abs_vals; - for (lpvar j : m) { - const rational v = vvr(j); - abs_vals.push_back(abs(v)); - if (v.is_neg()) { - sign = -sign; - } - } - std::sort(abs_vals.begin(), abs_vals.end()); - return abs_vals; - } - - void register_monomial_in_abs_vals(unsigned i) { - const monomial & m = m_monomials[i]; - int sign; - vector abs_vals = get_sorted_abs_vals_from_mon(m, sign); - index_with_sign ms(i, rational(sign)); - auto it = m_abs_vals_to_monomials.find(abs_vals); - - if (it == m_abs_vals_to_monomials.end()) { - - TRACE("nla_solver", - print_monomial_with_vars(m, tout);); - vector v; - v.push_back(ms); - // v is a vector containing a single index_with_sign - m_abs_vals_to_monomials.emplace(abs_vals, v); - } - else { - TRACE("nla_solver", - tout << "key="; print_vector(it->first, tout); - print_monomial_with_vars(m, tout);); - it->second.push_back(ms); - } - - } - void register_monomial_in_tables(unsigned i) { - register_monomial_in_abs_vals(i); + m_vars_equivalence.register_monomial_in_abs_vals(i, m_monomials[i]); monomial_coeff mc = canonize_monomial(m_monomials[i]); register_key_mono_in_rooted_monomials(mc, i); } void register_monomials_in_tables() { - m_abs_vals_to_monomials.clear(); + m_vars_equivalence.clear_monomials_by_abs_vals(); for (unsigned i = 0; i < m_monomials.size(); i++) register_monomial_in_tables(i); } @@ -877,7 +830,7 @@ struct solver::imp { bool order_lemma_on_factor(unsigned i_mon, const factorization& f, unsigned k, int sign) { lpvar j = f[k]; TRACE("nla_solver", tout << "k = " << k << ", j = " << j; ); - for (const index_with_sign& p : m_vars_equivalence.get_equivalent_vars(j, [this](unsigned h) {return vvr(h);})) { + for (const index_with_sign& p : m_vars_equivalence.get_equivalent_vars(j)) { TRACE("nla_solver", tout << "p.var() = " << p.var() << ", p.sign() = " << p.sign(); ); if (order_lemma_on_factor_and_equiv(p.m_i, i_mon, f, k, sign * p.m_sign)) { return true; diff --git a/src/util/lp/vars_equivalence.h b/src/util/lp/vars_equivalence.h index ec73cf78d..54f8e825d 100644 --- a/src/util/lp/vars_equivalence.h +++ b/src/util/lp/vars_equivalence.h @@ -81,16 +81,33 @@ struct vars_equivalence { // if m_tree[v] is not equal to -1 then m_equivs[m_tree[v]] = (k, v) or (v, k), that k is the parent of v vector m_equivs; // all equivalences extracted from constraints std::unordered_map m_vars_by_abs_values; + std::unordered_map, + vector, + hash_vector> + m_monomials_by_abs_vals; + std::function m_vvr; + + + // constructor + vars_equivalence(std::function vvr) : m_vvr(vvr) {} + + const std::unordered_map, + vector, + hash_vector>& monomials_by_abs_values() const { + return m_monomials_by_abs_vals; + } + + void clear() { m_equivs.clear(); m_tree.clear(); } // it also returns (j, 1) - vector get_equivalent_vars(lpvar j, std::function vvr) const { + vector get_equivalent_vars(lpvar j) const { vector ret; - rational val = vvr(j); + rational val = m_vvr(j); for (lpvar j : m_vars_by_abs_values.find(abs(val))->second) { if (val.is_pos()) ret.push_back(index_with_sign(j, rational(1))); @@ -202,5 +219,49 @@ struct vars_equivalence { it->second.push_back(j); } } + + void deregister_monomial_from_abs_vals(const monomial & m, unsigned i){ + int sign; + auto key = get_sorted_abs_vals_from_mon(m, sign); + SASSERT(m_monomials_by_abs_vals.find(key)->second.back() == index_with_sign(i, rational(sign))); + m_monomials_by_abs_vals.find(key)->second.pop_back(); + } + + vector get_sorted_abs_vals_from_mon(const monomial& m, int & sign) { + sign = 1; + vector abs_vals; + for (lpvar j : m) { + const rational v = m_vvr(j); + abs_vals.push_back(abs(v)); + if (v.is_neg()) { + sign = -sign; + } + } + std::sort(abs_vals.begin(), abs_vals.end()); + return abs_vals; + } + + void register_monomial_in_abs_vals(unsigned i, const monomial & m ) { + int sign; + vector abs_vals = get_sorted_abs_vals_from_mon(m, sign); + index_with_sign ms(i, rational(sign)); + auto it = m_monomials_by_abs_vals.find(abs_vals); + + if (it == m_monomials_by_abs_vals.end()) { + vector v; + v.push_back(ms); + // v is a vector containing a single index_with_sign + m_monomials_by_abs_vals.emplace(abs_vals, v); + } + else { + it->second.push_back(ms); + } + + } + + void clear_monomials_by_abs_vals() { + m_monomials_by_abs_vals.clear(); + } + }; // end of vars_equivalence }