mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

debug refactor of smon

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-04-23 16:07:16 -07:00
parent 9411911cf3
commit 11e3e1b463
3 changed files with 42 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/util/lp/emonomials.cpp
View file

@ -311,23 +311,23 @@ namespace nla {
// yes, assume that monomials are non-empty. // yes, assume that monomials are non-empty.
emonomials::pf_iterator::pf_iterator(emonomials const& m, monomial & mon, bool at_end): 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(); fast_forward();
} }
emonomials::pf_iterator::pf_iterator(emonomials const& m, lpvar v, bool at_end): 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(); fast_forward();
} }
void emonomials::pf_iterator::fast_forward() { void emonomials::pf_iterator::fast_forward() {
for (; m_it != m_end; ++m_it) { 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)) { if (m_mon && m_mon->var() != (*m_it).var() && m_em.canonize_divides(*m_mon, *m_it) && !m_em.is_visited(*m_it)) {
m.set_visited(*m_it); m_em.set_visited(*m_it);
break; break;
} }
if (!m_mon && !m.is_visited(*m_it)) { if (!m_mon && !m_em.is_visited(*m_it)) {
m.set_visited(*m_it); m_em.set_visited(*m_it);
break; break;
} }
} }

16
src/util/lp/emonomials.h
View file

@ -141,7 +141,7 @@ public:
monomial & operator[](lpvar v) { return m_monomials[m_var2index[v]]; } 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 { 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. \brief retrieve monomials m' where m is a proper factor of modulo current equalities.
*/ */
class pf_iterator { class pf_iterator {
emonomials const& m; emonomials const& m_em;
monomial * m_mon; // monomial 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; iterator m_end;
void fast_forward(); void fast_forward();
@ -209,19 +209,19 @@ public:
bool operator!=(pf_iterator const& other) const { return m_it != other.m_it; } bool operator!=(pf_iterator const& other) const { return m_it != other.m_it; }
}; };
class factors_of { class products_of {
emonomials const& m; emonomials const& m;
monomial * mon; monomial * mon;
lpvar m_var; lpvar m_var;
public: public:
factors_of(emonomials const& m, monomial & mon): m(m), mon(&mon), m_var(UINT_MAX) {} products_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, 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 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); } 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); } products_of get_products_of(monomial& m) const { inc_visited(); return products_of(*this, m); }
factors_of get_factors_of(lpvar v) const { inc_visited(); return factors_of(*this, v); } products_of get_products_of(lpvar v) const { inc_visited(); return products_of(*this, v); }
monomial const* find_canonical(svector<lpvar> const& vars) const; monomial const* find_canonical(svector<lpvar> const& vars) const;

42
src/util/lp/nla_order_lemmas.cpp
View file

@ -24,9 +24,11 @@
namespace nla { namespace nla {
// The order lemma is
// a > b && c > 0 => ac > bc
void order::order_lemma() { void order::order_lemma() {
TRACE("nla_solver", ); 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 start = random();
unsigned sz = rm_ref.size(); unsigned sz = rm_ref.size();
for (unsigned i = 0; i < sz && !done(); ++i) { 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) { void order::order_lemma_on_rmonomial(const monomial& m) {
TRACE("nla_solver_details", TRACE("nla_solver_details",
tout << "m = " << pp_mon(c(), m);); 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) if (ac.size() != 2)
continue; continue;
if (ac.is_mon()) if (ac.is_mon())
@ -50,17 +56,22 @@ void order::order_lemma_on_rmonomial(const monomial& m) {
break; 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) { void order::order_lemma_on_binomial(const monomial& ac) {
TRACE("nla_solver", tout << pp_mon(c(), ac);); TRACE("nla_solver", tout << pp_mon(c(), ac););
SASSERT(!check_monomial(ac) && ac.size() == 2); SASSERT(!check_monomial(ac) && ac.size() == 2);
const rational mult_val = vvr(ac.vars()[0]) * vvr(ac.vars()[1]); const rational mult_val = vvr(ac.vars()[0]) * vvr(ac.vars()[1]);
const rational acv = vvr(ac); const rational acv = vvr(ac);
bool gt = acv > mult_val; bool gt = acv > mult_val;
for (unsigned k = 0; k < 2; k++) { bool k = false;
order_lemma_on_binomial_k(ac, k == 1, gt); do {
order_lemma_on_factor_binomial_explore(ac, k == 1); 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) { 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); mk_ineq(xy.var(), - vvr(x), y, sign == 1 ? llc::LE : llc::GE);
TRACE("nla_solver", print_lemma(tout);); TRACE("nla_solver", print_lemma(tout););
} }
// 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
void order::order_lemma_on_factor_binomial_explore(const monomial& m1, bool k) { // We look for monomials of form m[k]d and see if we can create an order lemma for
SASSERT(m1.size() == 2); // m and m[k]d
lpvar c = m1.vars()[k]; void order::order_lemma_on_factor_binomial_explore(const monomial& m, bool k) {
for (monomial const& m2 : _().m_emons.get_factors_of(c)) { SASSERT(m.size() == 2);
order_lemma_on_factor_binomial_rm(m1, k, m2); 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()) { if (done()) {
break; 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) { 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 d(_().m_evars.find(ac.vars()[k]).var(), factor_type::VAR);
factor b; factor b;
if (c().divide(bd, d, 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 { 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)) { if (order_lemma_on_ac_and_bc(rm , ac, k, bc)) {
return true; return true;
} }