From 34262ae02c5226c89483e8c643bf7b2f06c0a2e6 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 28 Feb 2019 18:30:23 +1400 Subject: [PATCH] rollback but leave the change with llc::NE Signed-off-by: Lev Nachmanson --- src/util/lp/nla_solver.cpp | 80 ++++++++++++---------------------- src/util/lp/vars_equivalence.h | 35 +++------------ 2 files changed, 36 insertions(+), 79 deletions(-) diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index 1c0975f40..839d03d16 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -101,7 +101,7 @@ struct solver::imp { std::unordered_map m_mkeys; // the key is the sorted vars of a monomial unsigned find_monomial(const unsigned_vector& k) const { - TRACE("nla_solver", tout << "k = "; print_product_with_vars(k, tout);); + TRACE("nla_solver_find", 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";); @@ -259,8 +259,7 @@ struct solver::imp { // return true iff the monomial value is equal to the product of the values of the factors bool check_monomial(const monomial& m) const { - SASSERT(m_lar_solver.get_column_value(m.var()).is_int()); - TRACE("nla_solver_check", tout << "m = "; print_monomial_with_vars(m, tout);); + SASSERT(m_lar_solver.get_column_value(m.var()).is_int()); return product_value(m) == m_lar_solver.get_column_value_rational(m.var()); } @@ -354,7 +353,6 @@ struct solver::imp { print_var(m[k], out); } return out; - } std::ostream& print_monomial_with_vars(const monomial& m, std::ostream& out) const { @@ -792,6 +790,10 @@ struct solver::imp { return zero_j; } + static bool is_set(unsigned j) { + return static_cast(j) != -1; + } + bool try_get_non_strict_sign_from_bounds(lpvar j, int& sign) const { SASSERT(sign); if (has_lower_bound(j) && get_lower_bound(j) >= rational(0)) @@ -886,12 +888,14 @@ struct solver::imp { return m_vars_equivalence.eq_vars(j); } - void basic_sign_lemma_on_two_monomials(const monomial& m, const monomial& n, const rational& sign) { + bool basic_sign_lemma_on_two_monomials(const monomial& m, const monomial& n, const rational& sign) { TRACE("nla_solver", tout << "m = "; print_monomial_with_vars(m, tout); tout << "n= "; print_monomial_with_vars(n, tout); ); rational contr_sign; if (sign_contradiction(m, n, contr_sign)) { generate_sign_lemma(m, n, sign); + return true; } + return false; } void init_abs_val_table() { @@ -967,9 +971,9 @@ struct solver::imp { for (index_with_sign i_s : mons_to_explore) { unsigned n = i_s.index(); if (n == i) continue; - basic_sign_lemma_on_two_monomials(m, m_monomials[n], rm_i_s.sign()*i_s.sign()); - if(done()) - return true; + if (basic_sign_lemma_on_two_monomials(m, m_monomials[n], rm_i_s.sign()*i_s.sign())) + if(done()) + return true; } TRACE("nla_solver",); return false; @@ -979,18 +983,16 @@ struct solver::imp { * \brief explored; - for (unsigned i : m_to_refine){ - basic_sign_lemma_on_mon(i, explored); - if (done()) - return; - - } + bool basic_sign_lemma(bool derived) { + if (!derived) + return basic_sign_lemma_model_based(); + + std::unordered_set explored; + for (unsigned i : m_to_refine){ + if (basic_sign_lemma_on_mon(i, explored)) + return true; } + return false; } bool var_is_fixed_to_zero(lpvar j) const { @@ -1660,10 +1662,11 @@ struct solver::imp { unsigned random() {return settings().random_next();} // use basic multiplication properties to create a lemma - void basic_lemma(bool derived) { - basic_sign_lemma(derived); + bool basic_lemma(bool derived) { + if (basic_sign_lemma(derived)) + return true; if (derived) - return; + return false; init_rm_to_refine(); const auto& rm_ref = m_rm_table.to_refine(); TRACE("nla_solver", tout << "rm_ref = "; print_vector(rm_ref, tout);); @@ -1677,6 +1680,8 @@ struct solver::imp { i = 0; } } while(i != start && !done()); + + return false; } void map_monomial_vars_to_monomial_indices(unsigned i) { @@ -1707,8 +1712,7 @@ struct solver::imp { // we look for octagon constraints here, with a left part +-x +- y void collect_equivs() { const lp::lar_solver& s = m_lar_solver; - - + for (unsigned i = 0; i < s.terms().size(); i++) { unsigned ti = i + s.terms_start_index(); if (!s.term_is_used_as_row(ti)) @@ -1719,27 +1723,6 @@ struct solver::imp { add_equivalence_maybe(s.terms()[i], s.get_column_upper_bound_witness(j), s.get_column_lower_bound_witness(j)); } } - - std::unordered_map fixed_vars; - for (unsigned j = 0; j < s.number_of_vars(); j++) { - if (!var_is_fixed_to_zero(j)) continue; - rational v = abs(vvr(j)); - auto it = fixed_vars.find(v); - if (it == fixed_vars.end()){ - fixed_vars[v] = j; - } else { - lpvar k = it->second; - TRACE("nla_solver", tout << "fixed vars eq: " << k << ", " << j << ", fixed to " << vvr(j) << "\n";); - add_equivalence_of_two_vars(k, j, - s.get_column_upper_bound_witness(k), - s.get_column_lower_bound_witness(k), - s.get_column_upper_bound_witness(j), - s.get_column_lower_bound_witness(j)); - } - } - - - } void add_equivalence_maybe(const lp::lar_term *t, lpci c0, lpci c1) { @@ -1766,11 +1749,6 @@ struct solver::imp { rational sign((seen_minus && seen_plus)? 1 : -1); m_vars_equivalence.add_equiv(i, j, sign, c0, c1); } - void add_equivalence_of_two_vars(lpvar k, lpvar j, lpci c0, lpci c1, lpci c2, lpci c3) { - SASSERT(abs(vvr(k)) == abs(vvr(j))); - rational sign(vvr(k) == vvr(j)? 1 : -1); - m_vars_equivalence.add_equiv(k, j, sign, c0, c1, c2, c3); - } // x is equivalent to y if x = +- y void init_vars_equivalence() { @@ -2794,7 +2772,7 @@ struct solver::imp { if (search_level == 0) { basic_lemma(derived); if (!m_lemma_vec->empty()) - return l_false; + return l_false; } else if (search_level == 1) { order_lemma(derived); } else { // search_level == 2 diff --git a/src/util/lp/vars_equivalence.h b/src/util/lp/vars_equivalence.h index 459be11c6..f51004a04 100644 --- a/src/util/lp/vars_equivalence.h +++ b/src/util/lp/vars_equivalence.h @@ -19,8 +19,6 @@ --*/ namespace nla { - bool is_set(unsigned j) { return static_cast(j) != -1; } - typedef lp::constraint_index lpci; typedef lp::explanation expl_set; @@ -41,24 +39,15 @@ struct vars_equivalence { rational m_sign; lpci m_c0; lpci m_c1; - lpci m_c2; - lpci m_c3; - equiv(lpvar i, lpvar j, rational const& sign, - lpci c0, - lpci c1, - lpci c2, - lpci c3 - ) : + + equiv(lpvar i, lpvar j, rational const& sign, lpci c0, lpci c1) : m_i(i), m_j(j), m_sign(sign), m_c0(c0), - m_c1(c1), - m_c2(c2), - m_c3(c3) { + m_c1(c1) { SASSERT(m_i != m_j); } - }; struct node { @@ -150,13 +139,9 @@ struct vars_equivalence { } void add_equiv(lpvar i, lpvar j, rational const& sign, lpci c0, lpci c1) { - m_equivs.push_back(equiv(i, j, sign, c0, c1, -1, -1)); + m_equivs.push_back(equiv(i, j, sign, c0, c1)); } - - void add_equiv(lpvar i, lpvar j, rational const& sign, lpci c0, lpci c1, lpci c2, lpci c3) { - m_equivs.push_back(equiv(i, j, sign, c0, c1, c2, c3)); - } - + void connect_equiv_to_tree(unsigned k) { // m_tree is the tree with the edges formed by m_equivs const equiv &e = m_equivs[k]; @@ -262,14 +247,8 @@ struct vars_equivalence { if (it->second.m_parent == static_cast(-1)) return; const equiv & e = m_equivs[it->second.m_parent]; - if (is_set(e.m_c0)) - exp.add(e.m_c0); - if (is_set(e.m_c1)) - exp.add(e.m_c1); - if (is_set(e.m_c2)) - exp.add(e.m_c2); - if (is_set(e.m_c3)) - exp.add(e.m_c3); + exp.add(e.m_c0); + exp.add(e.m_c1); j = get_parent_node(j, e); } }