From 11e3e1b463d5965f56cad616538324e894ad6e39 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 23 Apr 2019 16:07:16 -0700 Subject: [PATCH] debug refactor of smon Signed-off-by: Lev Nachmanson --- src/util/lp/emonomials.cpp | 12 ++++----- src/util/lp/emonomials.h | 16 ++++++------ src/util/lp/nla_order_lemmas.cpp | 42 +++++++++++++++++++++----------- 3 files changed, 42 insertions(+), 28 deletions(-) diff --git a/src/util/lp/emonomials.cpp b/src/util/lp/emonomials.cpp index f5bbc1832..4b77fd6a9 100644 --- a/src/util/lp/emonomials.cpp +++ b/src/util/lp/emonomials.cpp @@ -311,23 +311,23 @@ namespace nla { // yes, assume that monomials are non-empty. emonomials::pf_iterator::pf_iterator(emonomials const& m, monomial & mon, bool at_end): - m(m), m_mon(&mon), m_it(iterator(m, m.head(mon.vars()[0]), at_end)), m_end(iterator(m, m.head(mon.vars()[0]), true)) { + m_em(m), m_mon(&mon), m_it(iterator(m, m.head(mon.vars()[0]), at_end)), m_end(iterator(m, m.head(mon.vars()[0]), true)) { fast_forward(); } emonomials::pf_iterator::pf_iterator(emonomials const& m, lpvar v, bool at_end): - m(m), m_mon(nullptr), m_it(iterator(m, m.head(v), at_end)), m_end(iterator(m, m.head(v), true)) { + m_em(m), m_mon(nullptr), m_it(iterator(m, m.head(v), at_end)), m_end(iterator(m, m.head(v), true)) { fast_forward(); } void emonomials::pf_iterator::fast_forward() { for (; m_it != m_end; ++m_it) { - if (m_mon && m_mon->var() != (*m_it).var() && m.canonize_divides(*m_mon, *m_it) && !m.is_visited(*m_it)) { - m.set_visited(*m_it); + if (m_mon && m_mon->var() != (*m_it).var() && m_em.canonize_divides(*m_mon, *m_it) && !m_em.is_visited(*m_it)) { + m_em.set_visited(*m_it); break; } - if (!m_mon && !m.is_visited(*m_it)) { - m.set_visited(*m_it); + if (!m_mon && !m_em.is_visited(*m_it)) { + m_em.set_visited(*m_it); break; } } diff --git a/src/util/lp/emonomials.h b/src/util/lp/emonomials.h index 7d638c8e7..c2ab6f4f6 100644 --- a/src/util/lp/emonomials.h +++ b/src/util/lp/emonomials.h @@ -141,7 +141,7 @@ public: monomial & operator[](lpvar v) { return m_monomials[m_var2index[v]]; } /** - \brief obtain the representative canonized monomial up to sign. + \brief obtain the representative canonized monomial */ monomial const& rep(monomial const& sv) const { @@ -193,9 +193,9 @@ public: \brief retrieve monomials m' where m is a proper factor of modulo current equalities. */ class pf_iterator { - emonomials const& m; + emonomials const& m_em; monomial * m_mon; // monomial - iterator m_it; // iterator over the first variable occurs list, ++ filters out elements that are not factors. + iterator m_it; // iterator over the first variable occurs list, ++ filters out elements that do not have m as a factor iterator m_end; void fast_forward(); @@ -209,19 +209,19 @@ public: bool operator!=(pf_iterator const& other) const { return m_it != other.m_it; } }; - class factors_of { + class products_of { emonomials const& m; monomial * mon; lpvar m_var; public: - factors_of(emonomials const& m, monomial & mon): m(m), mon(&mon), m_var(UINT_MAX) {} - factors_of(emonomials const& m, lpvar v): m(m), mon(nullptr), m_var(v) {} + products_of(emonomials const& m, monomial & mon): m(m), mon(&mon), m_var(UINT_MAX) {} + products_of(emonomials const& m, lpvar v): m(m), mon(nullptr), m_var(v) {} pf_iterator begin() { if (mon) return pf_iterator(m, *mon, false); return pf_iterator(m, m_var, false); } pf_iterator end() { if (mon) return pf_iterator(m, *mon, true); return pf_iterator(m, m_var, true); } }; - factors_of get_factors_of(monomial& m) const { inc_visited(); return factors_of(*this, m); } - factors_of get_factors_of(lpvar v) const { inc_visited(); return factors_of(*this, v); } + products_of get_products_of(monomial& m) const { inc_visited(); return products_of(*this, m); } + products_of get_products_of(lpvar v) const { inc_visited(); return products_of(*this, v); } monomial const* find_canonical(svector const& vars) const; diff --git a/src/util/lp/nla_order_lemmas.cpp b/src/util/lp/nla_order_lemmas.cpp index 829f09096..e8101fcc3 100644 --- a/src/util/lp/nla_order_lemmas.cpp +++ b/src/util/lp/nla_order_lemmas.cpp @@ -24,9 +24,11 @@ namespace nla { +// The order lemma is +// a > b && c > 0 => ac > bc void order::order_lemma() { TRACE("nla_solver", ); - const auto& rm_ref = c().m_to_refine; + const auto& rm_ref = c().m_to_refine; // todo : run on the rooted subset or m_to_refine unsigned start = random(); unsigned sz = rm_ref.size(); for (unsigned i = 0; i < sz && !done(); ++i) { @@ -35,11 +37,15 @@ void order::order_lemma() { } } +// The order lemma is +// a > b && c > 0 => ac > bc +// Consider here some binary factorizations of m=ac and +// try create order lemmas with either factor playing the role of c. void order::order_lemma_on_rmonomial(const monomial& m) { TRACE("nla_solver_details", tout << "m = " << pp_mon(c(), m);); - for (auto ac : factorization_factory_imp(m, c())) { + for (auto ac : factorization_factory_imp(m, _())) { if (ac.size() != 2) continue; if (ac.is_mon()) @@ -50,17 +56,22 @@ void order::order_lemma_on_rmonomial(const monomial& m) { break; } } - +// Here ac is a monomial of size 2 +// Trying to get an order lemma is +// a > b && c > 0 => ac > bc, +// with either variable of ac playing the role of c void order::order_lemma_on_binomial(const monomial& ac) { TRACE("nla_solver", tout << pp_mon(c(), ac);); SASSERT(!check_monomial(ac) && ac.size() == 2); const rational mult_val = vvr(ac.vars()[0]) * vvr(ac.vars()[1]); const rational acv = vvr(ac); bool gt = acv > mult_val; - for (unsigned k = 0; k < 2; k++) { - order_lemma_on_binomial_k(ac, k == 1, gt); - order_lemma_on_factor_binomial_explore(ac, k == 1); - } + bool k = false; + do { + order_lemma_on_binomial_k(ac, k, gt); + order_lemma_on_factor_binomial_explore(ac, k); + k = !k; + } while (k); } void order::order_lemma_on_binomial_k(const monomial& m, bool k, bool gt) { @@ -86,12 +97,14 @@ void order::order_lemma_on_binomial_sign(const monomial& xy, lpvar x, lpvar y, i mk_ineq(xy.var(), - vvr(x), y, sign == 1 ? llc::LE : llc::GE); TRACE("nla_solver", print_lemma(tout);); } - -void order::order_lemma_on_factor_binomial_explore(const monomial& m1, bool k) { - SASSERT(m1.size() == 2); - lpvar c = m1.vars()[k]; - for (monomial const& m2 : _().m_emons.get_factors_of(c)) { - order_lemma_on_factor_binomial_rm(m1, k, m2); +// m's size is 2 and m = m[k]a[!k] if k is false and m = m[!k]a[k] if k is true +// We look for monomials of form m[k]d and see if we can create an order lemma for +// m and m[k]d +void order::order_lemma_on_factor_binomial_explore(const monomial& m, bool k) { + SASSERT(m.size() == 2); + lpvar c = m.vars()[k]; + for (monomial const& m2 : _().m_emons.get_products_of(c)) { + order_lemma_on_factor_binomial_rm(m, k, m2); if (done()) { break; } @@ -99,6 +112,7 @@ void order::order_lemma_on_factor_binomial_explore(const monomial& m1, bool k) { } void order::order_lemma_on_factor_binomial_rm(const monomial& ac, bool k, const monomial& bd) { + TRACE("nla_solver", tout << "bd=" << pp_mon(_(), bd) << "\n";); factor d(_().m_evars.find(ac.vars()[k]).var(), factor_type::VAR); factor b; if (c().divide(bd, d, b)) { @@ -208,7 +222,7 @@ bool order::order_lemma_on_ac_explore(const monomial& rm, const factorization& a } } else { - for (monomial const& bc : _().m_emons.get_factors_of(c.var())) { + for (monomial const& bc : _().m_emons.get_products_of(c.var())) { if (order_lemma_on_ac_and_bc(rm , ac, k, bc)) { return true; }