From c5c89704a62aa1a4982b8ff96b6771d284b250f7 Mon Sep 17 00:00:00 2001 From: Lev Date: Tue, 27 Nov 2018 12:09:45 -0800 Subject: [PATCH] remove sign from factorization Signed-off-by: Lev --- src/util/lp/factorization.cpp | 10 ++- src/util/lp/factorization.h | 5 +- src/util/lp/nla_solver.cpp | 127 ++++++++-------------------------- 3 files changed, 32 insertions(+), 110 deletions(-) diff --git a/src/util/lp/factorization.cpp b/src/util/lp/factorization.cpp index 8522e7caf..aaf66979b 100644 --- a/src/util/lp/factorization.cpp +++ b/src/util/lp/factorization.cpp @@ -54,7 +54,7 @@ const_iterator_mon::reference const_iterator_mon::operator*() const { unsigned j, k; rational sign; if (!get_factors(j, k, sign)) return factorization(); - return create_binary_factorization(j, k, sign); + return create_binary_factorization(j, k); } void const_iterator_mon::advance_mask() { @@ -90,7 +90,7 @@ bool const_iterator_mon::operator==(const const_iterator_mon::self_type &other) } bool const_iterator_mon::operator!=(const const_iterator_mon::self_type &other) const { return !(*this == other); } -factorization const_iterator_mon::create_binary_factorization(lpvar j, lpvar k, rational const& sign) const { +factorization const_iterator_mon::create_binary_factorization(lpvar j, lpvar k) const { // todo : the current explanation is an overkill // std::function explain = [&](expl_set& exp){ // const imp & impl = m_ff->m_impf; @@ -106,15 +106,13 @@ factorization const_iterator_mon::create_binary_factorization(lpvar j, lpvar k, // }; factorization f; f.vars().push_back(j); - f.vars().push_back(k); - f.sign() = sign; + f.vars().push_back(k); return f; } factorization const_iterator_mon::create_full_factorization() const { factorization f; - f.vars() = m_ff->m_vars; - f.sign() = rational(1); + f.vars() = m_ff->m_vars; return f; } } diff --git a/src/util/lp/factorization.h b/src/util/lp/factorization.h index 0b2898a83..59c9c2bcf 100644 --- a/src/util/lp/factorization.h +++ b/src/util/lp/factorization.h @@ -28,13 +28,10 @@ typedef unsigned lpvar; class factorization { svector m_vars; - rational m_sign; public: bool is_empty() const { return m_vars.empty(); } svector & vars() { return m_vars; } const svector & vars() const { return m_vars; } - rational const& sign() const { return m_sign; } - rational& sign() { return m_sign; } // the setter unsigned operator[](unsigned k) const { return m_vars[k]; } size_t size() const { return m_vars.size(); } const lpvar* begin() const { return m_vars.begin(); } @@ -69,7 +66,7 @@ struct const_iterator_mon { bool operator==(const self_type &other) const; bool operator!=(const self_type &other) const; - factorization create_binary_factorization(lpvar j, lpvar k, rational const& sign) const; + factorization create_binary_factorization(lpvar j, lpvar k) const; factorization create_full_factorization() const; }; diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index 7a58b8358..190e9bcbd 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -35,6 +35,7 @@ struct solver::imp { lpvar operator[](unsigned k) const { return m_vars[k];} unsigned size() const { return m_vars.size(); } unsigned orig_index() const { return m_orig.m_i; } + const svector & vars() const {return m_vars;} }; @@ -485,7 +486,7 @@ struct solver::imp { if (k < f.size() - 1) out << "*"; } - return out << ", sign = " << f.sign(); + return out; } struct factorization_factory_imp: factorization_factory { @@ -587,7 +588,6 @@ struct solver::imp { bool basic_lemma_for_mon_neutral_monomial_to_factor(const rooted_mon& rm, const factorization& f) { TRACE("nla_solver", trace_print_monomial_and_factorization(rm, f, tout);); - // todo : consider the case of just two factors lpvar mon_var = m_monomials[rm.orig_index()].var(); const auto & mv = vvr(mon_var); const auto abs_mv = abs(mv); @@ -717,7 +717,7 @@ struct solver::imp { return true; for (const rooted_mon& r : m_vector_of_rooted_monomials) { - if (check_monomial(m_monomials[r.m_orig.m_i])) + if (check_monomial(m_monomials[r.orig_index()])) continue; if (basic_lemma_for_mon(r)) { return true; @@ -922,96 +922,19 @@ struct solver::imp { return ret; } - // a > b && c == d => ac > bd - // ac is a factorization of m_monomials[i_mon] - // ac[k] plays the role of c - // d = +-c - // i_bd_equiv is a candidate for bd - bool order_lemma_on_factor_equiv_and_other_mon_eq(unsigned b, - unsigned i_bd_equiv, - unsigned i_bd, - unsigned d, unsigned i_ac, const factorization& ac, unsigned k) { - return false; - } - - - // a > b && c == d => ac > bd - // ac is a factorization of m_monomials[i_mon] - // ac[k] plays the role of c - // d = +-c - // i_bd_equiv is a candidate for bd - bool order_lemma_on_factor_equiv_and_other_mon_eq(unsigned i_bd_equiv, - unsigned i_bd, - unsigned d, unsigned i_ac, const factorization& ac, unsigned k) { - return false; - /* - TRACE("nla_solver", tout << "i_bd_equiv = "; print_monomial_with_vars(i_bd_equiv, tout); ); - rational abs_d = abs(vvr(d)); - for (unsigned k = 0; k < m_monomials[i_bd_equiv].size(); k++) { - if (abs(vvr(m_monomials[i_bd_equiv][k])) != abs_d) - continue; - svector b = extract_all_but(m_monomials[i_bd_equiv].vars(), k); - std::sort(b.begin(), b.end()); - auto it = m_rooted_monomials_map.find(b); - if (it == m_rooted_monomials_map.end()) - return false; - - for (const index_with_sign& s : it->second) { - if (order_lemma_on_factor_equiv_and_other_mon_eq_b(s.var(), i_bd, d, i_bd, d, i_ac, ac, k)) - return true; - } - } - return false;*/ - } - - - // a > b && c == d => ac > bd - // ac is a factorization of m_monomials[i_mon] - // ac[k] plays the role of c - // d = +-c - bool order_lemma_on_factor_equiv_and_other_mon(unsigned i_bd, unsigned d, unsigned i_ac, const factorization& ac, unsigned k) { - if (i_bd == i_ac) { - return false; - } - - const monomial & m_bd = m_monomials[i_bd]; - monomial_coeff m_bd_rooted = canonize_monomial(m_bd); - TRACE("nla_solver", tout << "i_bd monomial = "; print_monomial(m_bd, tout); ); - auto it = m_rooted_monomials_map.find(m_bd_rooted.vars()); - if (it == m_rooted_monomials_map.end()) - return false; - for (const index_with_sign& s : it->second) { - if (order_lemma_on_factor_equiv_and_other_mon_eq(s.var(), i_bd, d, i_ac, ac, k)) - return true; - } + bool order_lemma_on_ac_and_bc(const rooted_mon& rm, const factorization& ac, unsigned k, const rooted_mon& rm_bc) { return false; } - // a > b && c == d => ac > bd - // ac is a factorization of m_monomials[i_mon] - // ac[k] plays the role of c - // d = +-c - bool order_lemma_on_factor_and_equiv(unsigned d, unsigned i_mon, const factorization& ac, unsigned k) { - TRACE("nla_solver", tout << "d = " << d << ", k = " << k << ", ac[k] = " << ac[k] << std::endl; ); - SASSERT(abs(vvr(d)) == abs(vvr(ac[k]))); - lpvar j = ac[k]; - for (unsigned i : m_monomials_containing_var[j]) { - if (order_lemma_on_factor_equiv_and_other_mon(i, d, i_mon, ac, k)) { - return true; - } - } - return false; - } - - // a > b && c == d => ac > bd + // a > b && c > 0 => ac > bc // ac is a factorization of m_monomials[i_mon] // ac[k] plays the role of c - bool order_lemma_on_factor(unsigned i_mon, const factorization& ac, unsigned k) { + bool order_lemma_on_factor(const rooted_mon& rm, const factorization& ac, unsigned k) { lpvar c = ac[k]; TRACE("nla_solver", tout << "k = " << k << ", c = " << c; ); - for (const index_with_sign& d : m_vars_equivalence.get_equivalent_vars(c)) { - TRACE("nla_solver", tout << "d.var() = " << d.var() << ", d.sign() = " << d.sign(); ); - if (order_lemma_on_factor_and_equiv(d.m_i, i_mon, ac, k)) { + SASSERT(m_rooted_monomials_containing_var.find(c) != m_rooted_monomials_containing_var.end()); + for (unsigned rm_bc : m_rooted_monomials_containing_var[c]) { + if (order_lemma_on_ac_and_bc(rm , ac, k, m_vector_of_rooted_monomials[rm_bc])) { return true; } } @@ -1020,39 +943,43 @@ struct solver::imp { // a > b && c == d => ac > bd // ac is a factorization of m_monomials[i_mon] - bool order_lemma_on_factorization(unsigned i_mon, const factorization& ac) { + bool order_lemma_on_factorization(const rooted_mon& rm, const factorization& ac) { TRACE("nla_solver", tout << "factorization = "; print_factorization(ac, tout);); for (unsigned k = 0; k < ac.size(); k++) { const rational & v = vvr(ac[k]); if (v.is_zero()) continue; - if (order_lemma_on_factor(i_mon, ac, k)) { + if (order_lemma_on_factor(rm, ac, k)) { return true; } } return false; } - // a > b && c == d => ac > bd + // a > b && c > 0 => ac > bc bool order_lemma_on_monomial(const rooted_mon& rm) { - /* - TRACE("nla_solver", print_monomial_with_vars(i_mon, tout);); - for (auto ac : factorization_factory_imp(i_mon, *this)) { + TRACE("nla_solver", + tout << "rm = "; print_product(rm, tout); + tout << ", orig = "; print_monomial(m_monomials[rm.orig_index()], tout); + ); + for (auto ac : factorization_factory_imp(rm.vars(), *this)) { if (ac.is_empty()) continue; - if (order_lemma_on_factorization(i_mon, ac)) + if (order_lemma_on_factorization(rm, ac)) return true; - }*/ + } return false; } bool order_lemma() { - // for (unsigned i_mon : to_refine) { - // if (order_lemma_on_monomial(i_mon)) { - // return true; - // } - // } + for (const auto& rm : m_vector_of_rooted_monomials) { + if (check_monomial(m_monomials[rm.orig_index()])) + continue; + if (order_lemma_on_monomial(rm)) { + return true; + } + } return false; } @@ -1148,7 +1075,7 @@ struct solver::imp { for (lpvar j : f) { std::cout << "j = "; print_var(j, std::cout); } - std::cout << "sign = " << f.sign() << std::endl; + std::cout << std::endl; } SASSERT(found_factorizations == number_of_factorizations); }