From 0d5ca4edfee493a9ca89e627ff44088c306f95ce Mon Sep 17 00:00:00 2001 From: Lev Date: Tue, 8 Jan 2019 23:16:33 -0800 Subject: [PATCH] more efficient sign lemma Signed-off-by: Lev --- src/smt/theory_lra.cpp | 4 +- src/util/lp/monomial.h | 8 +- src/util/lp/nla_solver.cpp | 250 +++++++++++++++++++++++++++------ src/util/lp/vars_equivalence.h | 57 +------- 4 files changed, 221 insertions(+), 98 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index c5dff1835..7151662a5 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -267,8 +267,8 @@ class theory_lra::imp { struct switcher { theory_lra::imp& m_th_imp; scoped_ptr* m_nra; - scoped_ptr* m_nla; - bool m_use_nla; + scoped_ptr* m_nla; + bool m_use_nla; switcher(theory_lra::imp& i): m_th_imp(i), m_nra(nullptr), m_nla(nullptr) { } diff --git a/src/util/lp/monomial.h b/src/util/lp/monomial.h index 1a8ae936d..548062f68 100644 --- a/src/util/lp/monomial.h +++ b/src/util/lp/monomial.h @@ -20,9 +20,13 @@ namespace nla { public: // constructors monomial(lp::var_index v, unsigned sz, lp::var_index const* vs): - m_v(v), m_vs(sz, vs) {} + m_v(v), m_vs(sz, vs) { + std::sort(m_vs.begin(), m_vs.end()); + } monomial(lp::var_index v, const svector &vs): - m_v(v), m_vs(vs) {} + m_v(v), m_vs(vs) { + std::sort(m_vs.begin(), m_vs.end()); + } monomial() {} unsigned var() const { return m_v; } diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index 827b9c2b5..357c947dd 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -29,6 +29,7 @@ namespace nla { typedef lp::lconstraint_kind llc; struct solver::imp { + typedef lp::lar_base_constraint lpcon; //fields @@ -39,12 +40,133 @@ struct solver::imp { // this field is used for the push/pop operations unsigned_vector m_monomials_counts; lp::lar_solver& m_lar_solver; + std::unordered_map> m_monomials_containing_var; // m_var_to_its_monomial[m_monomials[i].var()] = i std::unordered_map m_var_to_its_monomial; lp::explanation * m_expl; lemma * m_lemma; + unsigned_vector m_to_refine; + std::unordered_map m_mkeys; // the key is the sorted vars of a monomial + struct const_iterator_equiv_mon { + // fields + const unsigned_vector m_vars; + vector m_offsets; + const imp& m_imp; + bool m_done; + // constructor for begin() + const_iterator_equiv_mon(const unsigned_vector& vars, + vector offsets, + const imp& i) : m_vars(vars), + m_offsets(offsets), + m_imp(i), + m_done(false) {} + // constructor for end() + const_iterator_equiv_mon( const imp& i) :m_imp(i), + m_done(true) {} + + //typedefs + typedef const_iterator_equiv_mon self_type; + typedef unsigned value_type; + typedef unsigned reference; + typedef int difference_type; + typedef std::forward_iterator_tag iterator_category; + + void advance() { + if (m_done) + return; + unsigned k = 0; + for (; k < m_offsets.size(); k++) { + auto & it = m_offsets[k]; + it++; + const auto & evars = m_imp.abs_eq_vars(m_vars[k]); + if (it == evars.end()) { + it = evars.begin(); + } else { + break; + } + } + + if (k == m_vars.size()) { + m_done = true; + } + } + + unsigned_vector get_key() const { + unsigned_vector r; + for(const auto& it : m_offsets){ + r.push_back(*it); + } + std::sort(r.begin(), r.end()); + TRACE("nla_solver", tout << "r = "; m_imp.print_product_with_vars(r, tout);); + return r; + } + + unsigned get_monomial() const { + unsigned_vector key = get_key(); + return m_imp.find_monomial(key); + } + + self_type operator++() {self_type i = *this; operator++(1); return i;} + self_type operator++(int) { advance(); return *this; } + + bool operator==(const self_type &other) const { return m_done == other.m_done;} + bool operator!=(const self_type &other) const { return ! (*this == other); } + reference operator*() const { + unsigned i = get_monomial(); + TRACE("nla_solver", + if (static_cast(i) != -1) + m_imp.print_monomial_with_vars(m_imp.m_monomials[i], tout); + else + tout << "not found";); + return i; + } + }; + + struct equiv_monomials { + const monomial & m_mon; + const imp& m_imp; + equiv_monomials(const monomial & m, const imp& i) : m_mon(m), m_imp(i) {} + + const_iterator_equiv_mon begin() { + return const_iterator_equiv_mon(m_mon.vars(), vars_eq_offsets_begin(), m_imp); + } + + const_iterator_equiv_mon end() { + return const_iterator_equiv_mon(m_imp); + } + vector vars_eq_offsets_end() const { + vector r; + for(lpvar j : m_mon.vars()) { + r.push_back(m_imp.abs_eq_vars(j).end()); + } + return r; + } + vector vars_eq_offsets_begin() const { + vector r; + for(lpvar j : m_mon.vars()) { + r.push_back(m_imp.abs_eq_vars(j).begin()); + } + return r; + } + }; + + unsigned find_monomial(const unsigned_vector& k) const { + TRACE("nla_solver", tout << "k = "; print_product_with_vars(k, tout);); + auto it = m_mkeys.find(k); + if (it == m_mkeys.end()) { + TRACE("nla_solver", tout << "not found";); + return -1; + } + TRACE("nla_solver", tout << "found " << it->second << ", mon = "; print_monomial_with_vars(m_monomials[it->second], tout);); + return it->second; + } + + const unsigned_vector& abs_eq_vars(lpvar j) const { + rational v = abs(vvr(j)); + return m_vars_equivalence.get_vars_with_the_same_abs_val(v); + } imp(lp::lar_solver& s, reslimit& lim, params_ref const& p) : @@ -133,7 +255,9 @@ struct solver::imp { unsigned add(lpvar v, unsigned sz, lpvar const* vs) { m_monomials.push_back(monomial(v, sz, vs)); TRACE("nla_solver", print_monomial(m_monomials.back(), tout);); - return m_monomials.size() - 1; + const auto & m = m_monomials.back(); + SASSERT(m_mkeys.find(m.vars()) == m_mkeys.end()); + return m_mkeys[m.vars()] = m_monomials.size() - 1; } void push() { @@ -149,7 +273,8 @@ struct solver::imp { } void deregister_monomial_from_tables(const monomial & m, unsigned i){ - m_vars_equivalence.deregister_monomial_from_abs_vals(m, i); + TRACE("nla_solver", tout << "m = "; print_monomial(m, tout);); + m_mkeys.erase(m.vars()); deregister_monomial_from_rooted_monomials(m, i); } @@ -491,14 +616,11 @@ struct solver::imp { // the value of the i-th monomial has to be equal to the value of the k-th monomial modulo sign // but it is not the case in the model - void generate_sign_lemma(const vector& abs_vals, unsigned i, unsigned k, const rational& sign) { - SASSERT(sign == rational(1) || sign == rational(-1)); + void generate_sign_lemma(const vector& abs_vals, const monomial& m, const monomial& n, const rational& sign) { SASSERT(m_lemma->empty()); TRACE("nla_solver", - tout << "mon i=" << i << " = "; print_monomial_with_vars(m_monomials[i],tout); - tout << '\n'; - tout << "mon k=" << k << " = "; print_monomial_with_vars(m_monomials[k],tout); - tout << '\n'; + tout << "m = "; print_monomial_with_vars(m, tout); + tout << "n = "; print_monomial_with_vars(n, tout); tout << "abs_vals="; print_vector(abs_vals, tout); ); std::unordered_map> map; @@ -506,7 +628,7 @@ struct solver::imp { map[v] = vector(); } - for (unsigned j : m_monomials[i]) { + for (unsigned j : m) { rational v = vvr(j); int s; if (v.is_pos()) { @@ -521,7 +643,7 @@ struct solver::imp { it->second.push_back(index_with_sign(j, rational(s))); } - for (unsigned j : m_monomials[k]) { + for (unsigned j : n) { rational v = vvr(j); rational s; if (v.is_pos()) { @@ -541,7 +663,7 @@ struct solver::imp { it->second.pop_back(); } - mk_ineq(m_monomials[i].var(), -sign, m_monomials[k].var(), llc::EQ); + mk_ineq(m.var(), -sign, n.var(), llc::EQ); TRACE("nla_solver", print_lemma(tout);); } @@ -584,29 +706,58 @@ struct solver::imp { } return false; } - - bool basic_sign_lemma_on_a_bucket_of_abs_vals(const vector& abs_vals, const unsigned_vector& list){ - TRACE("nla_solver", - tout << "key = "; - print_vector(abs_vals, tout); - tout << "m0 = "; - print_monomial_with_vars(m_monomials[list[0]], tout); - ); - rational val = vvr(m_monomials[list[0]].var()); - int sign = vars_sign(m_monomials[list[0]].vars()); - if (sign == 0) { - return sign_lemma_for_zero_on_list(list); - } - - for (unsigned i = 1; i < list.size(); i++) { - rational rsign = rational(vars_sign(m_monomials[list[i]].vars()) * sign); - SASSERT(!rsign.is_zero()); - rational other_val = vvr(m_monomials[list[i]].var()); - if (val * rsign != other_val) { - generate_sign_lemma(abs_vals, list[0], list[i], rsign); - return true; + + rational rat_sign(const monomial& m) const { + int sign = 1; + for (lpvar j : m) { + auto v = vvr(j); + if (v.is_neg()) { + sign = - sign; + continue; } + if (v.is_pos()) { + continue; + } + sign = 0; + break; } + return rational(sign); + } + + bool sign_contradiction(const monomial& m, const monomial& n, rational & sign) const { + sign = rat_sign(m) * rat_sign(n); + return vvr(m) != sign * vvr(n) ; + } + + vector abs_vals(const monomial& m) const { + vector r; + for(unsigned j : m){ + r.push_back(abs(vvr(j))); + } + return r; + } + + + + bool basic_sign_lemma_on_two_monomials(const monomial& m, const monomial& n) { + TRACE("nla_solver", tout << "m = "; print_monomial_with_vars(m, tout); tout << "n= "; print_monomial_with_vars(n, tout); ); + rational sign; + if (sign_contradiction(m, n, sign)) { + generate_sign_lemma(abs_vals(m) ,m, n, sign); + return true; + } + return false; + } + + bool basic_sign_lemma_on_mon(unsigned i){ + TRACE("nla_solver", tout << "i = " << i << ", mon = "; print_monomial_with_vars(m_monomials[i], tout);); + const monomial& m = m_monomials[i]; + for (unsigned n : equiv_monomials(m, *this)) { + if (n == static_cast(-1) || n == i) continue; + if (basic_sign_lemma_on_two_monomials(m_monomials[i], m_monomials[n])) + return true; + } + TRACE("nla_solver",); return false; } @@ -626,8 +777,8 @@ struct solver::imp { -ab = a(-b) */ bool basic_sign_lemma() { - 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)) + for (unsigned i : m_to_refine){ + if (basic_sign_lemma_on_mon(i)) return true; } return false; @@ -998,12 +1149,28 @@ struct solver::imp { return false; } + void map_monomial_vars_to_monomial_indices(unsigned i) { + const monomial& m = m_monomials[i]; + for (lpvar j : m.vars()) { + auto it = m_monomials_containing_var.find(j); + if (it == m_monomials_containing_var.end()) { + unsigned_vector ms; + ms.push_back(i); + m_monomials_containing_var[j] = ms; + } + else { + it->second.push_back(i); + } + } + } + void map_vars_to_monomials() { for (unsigned i = 0; i < m_monomials.size(); i++) { const monomial& m = m_monomials[i]; lpvar v = m.var(); SASSERT(m_var_to_its_monomial.find(v) == m_var_to_its_monomial.end()); m_var_to_its_monomial[v] = i; + map_monomial_vars_to_monomial_indices(i); } } @@ -1133,9 +1300,9 @@ struct solver::imp { void register_monomial_in_tables(unsigned i_mon) { - m_vars_equivalence.register_monomial_in_abs_vals(i_mon, m_monomials[i_mon]); - monomial_coeff mc = canonize_monomial(m_monomials[i_mon]); - TRACE("nla_solver", tout << "mon = "; + const monomial& m = m_monomials[i_mon]; + monomial_coeff mc = canonize_monomial(m); + TRACE("nla_solver", tout << "i_mon = " << i_mon << ", mon = "; print_monomial(m_monomials[i_mon], tout); tout << "\nmc = "; print_product(mc.vars(), tout); @@ -1166,6 +1333,7 @@ struct solver::imp { m_var_to_its_monomial.clear(); m_vars_equivalence.clear(); m_rm_table.clear(); + m_monomials_containing_var.clear(); m_expl->clear(); m_lemma->clear(); } @@ -1741,13 +1909,12 @@ struct solver::imp { return l_undef; } - bool to_refine = false; - for (unsigned i = 0; i < m_monomials.size() && !to_refine; i++) { + for (unsigned i = 0; i < m_monomials.size(); i++) { if (!check_monomial(m_monomials[i])) - to_refine = true; + m_to_refine.push_back(i); } - if (!to_refine) { + if (m_to_refine.empty()) { return l_true; } @@ -2277,6 +2444,7 @@ void solver::test_basic_lemma_for_mon_neutral_from_monomial_to_factors() { } void solver::test_basic_sign_lemma() { + enable_trace("nla_solver"); lp::lar_solver s; unsigned a = 0, b = 1, c = 2, d = 3, e = 4, bde = 7, acd = 8; diff --git a/src/util/lp/vars_equivalence.h b/src/util/lp/vars_equivalence.h index 187d396fa..f7dee5a5a 100644 --- a/src/util/lp/vars_equivalence.h +++ b/src/util/lp/vars_equivalence.h @@ -41,17 +41,6 @@ struct index_with_sign { const rational& sign() const { return m_sign; } }; -struct rat_hash { - typedef rational data; - unsigned operator()(const rational& x) const { return x.hash(); } -}; - - -struct hash_vector { - size_t operator()(const vector & v) const { - return vector_hash()(v); - } -}; struct vars_equivalence { @@ -82,36 +71,21 @@ 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, - unsigned_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, - unsigned_vector, - hash_vector>& monomials_by_abs_values() const { - return m_monomials_by_abs_vals; - } - - void clear() { m_equivs.clear(); m_tree.clear(); - m_vars_by_abs_values.clear(); - m_monomials_by_abs_vals.clear(); + m_vars_by_abs_values.clear(); } - svector get_vars_with_the_same_abs_val(const rational& v) const { - svector ret; + const svector& get_vars_with_the_same_abs_val(const rational& v) const { auto it = m_vars_by_abs_values.find(abs(v)); - if (it == m_vars_by_abs_values.end()) - return ret; - + SASSERT (it != m_vars_by_abs_values.end()); return it->second; } @@ -242,13 +216,6 @@ struct vars_equivalence { } } - 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() == i); - 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; @@ -262,21 +229,5 @@ struct vars_equivalence { 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); - auto it = m_monomials_by_abs_vals.find(abs_vals); - if (it == m_monomials_by_abs_vals.end()) { - unsigned_vector v; - v.push_back(i); - // v is a vector containing a single index_with_sign - m_monomials_by_abs_vals.emplace(abs_vals, v); - } - else { - it->second.push_back(i); - } - - } }; // end of vars_equivalence }