mirror of
https://github.com/Z3Prover/z3
synced 2025-07-24 13:18:55 +00:00
code reviewing order lemmas (#93)
* code reviewing order lemmas Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * code review monotonity Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
Lev Nachmanson
parent
1ab3957eea
commit
ed3bfcdea9
7 changed files with 233 additions and 204 deletions
|
|
@ -15,7 +15,6 @@
|
|||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
#include "util/lp/nla_order_lemmas.h"
|
||||
|
|
@ -25,13 +24,144 @@
|
|||
|
||||
namespace nla {
|
||||
|
||||
// a >< b && c > 0 => ac >< bc
|
||||
// a >< b && c < 0 => ac <> bc
|
||||
void order::order_lemma() {
|
||||
TRACE("nla_solver", );
|
||||
const auto& rm_ref = c().m_to_refine;
|
||||
unsigned start = random();
|
||||
unsigned sz = rm_ref.size();
|
||||
for (unsigned i = 0; i < sz && !done(); ++i) {
|
||||
const smon& rm = c().m_emons.canonical[rm_ref[(i + start) % sz]];
|
||||
order_lemma_on_rmonomial(rm);
|
||||
}
|
||||
}
|
||||
|
||||
void order::order_lemma_on_rmonomial(const smon& rm) {
|
||||
TRACE("nla_solver_details",
|
||||
tout << "rm = " << rm << ", orig = " << c().m_emons[rm];);
|
||||
|
||||
for (auto ac : factorization_factory_imp(rm, c())) {
|
||||
if (ac.size() != 2)
|
||||
continue;
|
||||
if (ac.is_mon())
|
||||
order_lemma_on_binomial(*ac.mon());
|
||||
else
|
||||
order_lemma_on_factorization(rm, ac);
|
||||
if (done())
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
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[0]) * vvr(ac[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);
|
||||
}
|
||||
}
|
||||
|
||||
void order::order_lemma_on_binomial_k(const monomial& m, bool k, bool gt) {
|
||||
SASSERT(gt == (vvr(m) > vvr(m[0]) * vvr(m[1])));
|
||||
order_lemma_on_binomial_sign(m, m[k], m[!k], gt ? 1: -1);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief
|
||||
sign = the sign of vvr(xy) - vvr(x) * vvr(y) != 0
|
||||
y <= 0 or x < a or xy >= ay
|
||||
y <= 0 or x > a or xy <= ay
|
||||
y >= 0 or x < a or xy <= ay
|
||||
y >= 0 or x > a or xy >= ay
|
||||
|
||||
*/
|
||||
void order::order_lemma_on_binomial_sign(const monomial& xy, lpvar x, lpvar y, int sign) {
|
||||
SASSERT(!_().mon_has_zero(xy));
|
||||
int sy = rat_sign(vvr(y));
|
||||
add_empty_lemma();
|
||||
mk_ineq(y, sy == 1 ? llc::LE : llc::GE); // negate sy
|
||||
mk_ineq(x, sy*sign == 1 ? llc::GT : llc::LT , vvr(x));
|
||||
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[k];
|
||||
for (monomial const& m2 : _().m_emons.get_factors_of(c)) {
|
||||
order_lemma_on_factor_binomial_rm(m1, k, m2);
|
||||
if (done()) {
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void order::order_lemma_on_factor_binomial_rm(const monomial& ac, bool k, const monomial& bd) {
|
||||
smon const& rm_bd = _().m_emons.canonical[bd];
|
||||
factor d(_().m_evars.find(ac[k]).var(), factor_type::VAR);
|
||||
factor b;
|
||||
if (c().divide(rm_bd, d, b)) {
|
||||
order_lemma_on_binomial_ac_bd(ac, k, rm_bd, b, d.var());
|
||||
}
|
||||
}
|
||||
|
||||
void order::order_lemma_on_binomial_ac_bd(const monomial& ac, bool k, const smon& bd, const factor& b, lpvar d) {
|
||||
TRACE("nla_solver",
|
||||
tout << "ac=" << pp_mon(c(), ac) << "\nrm= " << bd << ", b= " << pp_fac(c(), b) << ", d= " << pp_var(c(), d) << "\n";);
|
||||
bool p = !k;
|
||||
lpvar a = ac[p];
|
||||
lpvar c = ac[k];
|
||||
SASSERT(_().m_evars.find(c).var() == d);
|
||||
rational acv = vvr(ac);
|
||||
rational av = vvr(a);
|
||||
rational c_sign = rrat_sign(vvr(c));
|
||||
rational d_sign = rrat_sign(vvr(d));
|
||||
rational bdv = vvr(bd);
|
||||
rational bv = vvr(b);
|
||||
auto av_c_s = av*c_sign; auto bv_d_s = bv*d_sign;
|
||||
|
||||
// suppose ac >= bd, then ac/|c| >= bd/|d|.
|
||||
// Notice that ac/|c| = a*c_sign , and bd/|d| = b*d_sign
|
||||
if (acv >= bdv && av_c_s < bv_d_s)
|
||||
generate_mon_ol(ac, a, c_sign, c, bd, b, d_sign, d, llc::LT);
|
||||
else if (acv <= bdv && av_c_s > bv_d_s)
|
||||
generate_mon_ol(ac, a, c_sign, c, bd, b, d_sign, d, llc::GT);
|
||||
|
||||
}
|
||||
|
||||
// TBD: document what lemma is created here.
|
||||
|
||||
void order::generate_mon_ol(const monomial& ac,
|
||||
lpvar a,
|
||||
const rational& c_sign,
|
||||
lpvar c,
|
||||
const smon& bd,
|
||||
const factor& b,
|
||||
const rational& d_sign,
|
||||
lpvar d,
|
||||
llc ab_cmp) {
|
||||
add_empty_lemma();
|
||||
mk_ineq(c_sign, c, llc::LE);
|
||||
explain(c); // this explains c == +- d
|
||||
negate_var_factor_relation(c_sign, a, d_sign, b);
|
||||
mk_ineq(ac.var(), -canonize_sign(bd), var(bd), ab_cmp);
|
||||
explain(bd);
|
||||
explain(b);
|
||||
explain(d);
|
||||
TRACE("nla_solver", print_lemma(tout););
|
||||
}
|
||||
|
||||
|
||||
// a > b && c > 0 => ac > bc
|
||||
// a >< b && c > 0 => ac >< bc
|
||||
// a >< b && c < 0 => ac <> bc
|
||||
// ac[k] plays the role of c
|
||||
|
||||
bool order::order_lemma_on_ac_and_bc(const smon& rm_ac,
|
||||
const factorization& ac_f,
|
||||
unsigned k,
|
||||
bool k,
|
||||
const smon& rm_bd) {
|
||||
TRACE("nla_solver",
|
||||
tout << "rm_ac = " << rm_ac << "\n";
|
||||
|
|
@ -41,10 +171,36 @@ bool order::order_lemma_on_ac_and_bc(const smon& rm_ac,
|
|||
factor b;
|
||||
return
|
||||
c().divide(rm_bd, ac_f[k], b) &&
|
||||
order_lemma_on_ac_and_bc_and_factors(rm_ac, ac_f[(k + 1) % 2], ac_f[k], rm_bd, b);
|
||||
order_lemma_on_ac_and_bc_and_factors(rm_ac, ac_f[!k], ac_f[k], rm_bd, b);
|
||||
}
|
||||
|
||||
bool order::order_lemma_on_ac_explore(const smon& rm, const factorization& ac, unsigned k) {
|
||||
// TBD: document what lemma is created here.
|
||||
|
||||
void order::order_lemma_on_factorization(const smon& rm, const factorization& ab) {
|
||||
const monomial& m = _().m_emons[rm];
|
||||
TRACE("nla_solver", tout << "orig_sign = " << _().m_emons.orig_sign(rm) << "\n";);
|
||||
rational sign = _().m_emons.orig_sign(rm);
|
||||
for (factor f: ab)
|
||||
sign *= _().canonize_sign(f);
|
||||
const rational & fv = vvr(ab[0]) * vvr(ab[1]);
|
||||
const rational mv = sign * vvr(m);
|
||||
TRACE("nla_solver",
|
||||
tout << "ab.size()=" << ab.size() << "\n";
|
||||
tout << "we should have sign*vvr(m):" << mv << "=(" << sign << ")*(" << vvr(m) <<") to be equal to " << " vvr(ab[0])*vvr(ab[1]):" << fv << "\n";);
|
||||
if (mv == fv)
|
||||
return;
|
||||
bool gt = mv > fv;
|
||||
TRACE("nla_solver_f", tout << "m="; _().print_monomial_with_vars(m, tout); tout << "\nfactorization="; _().print_factorization(ab, tout););
|
||||
for (unsigned j = 0, k = 1; j < 2; j++, k--) {
|
||||
order_lemma_on_ab(m, sign, var(ab[k]), var(ab[j]), gt);
|
||||
explain(ab); explain(m);
|
||||
explain(rm);
|
||||
TRACE("nla_solver", _().print_lemma(tout););
|
||||
order_lemma_on_ac_explore(rm, ab, j == 1);
|
||||
}
|
||||
}
|
||||
|
||||
bool order::order_lemma_on_ac_explore(const smon& rm, const factorization& ac, bool k) {
|
||||
const factor c = ac[k];
|
||||
TRACE("nla_solver", tout << "c = "; _().print_factor_with_vars(c, tout); );
|
||||
if (c.is_var()) {
|
||||
|
|
@ -65,29 +221,6 @@ bool order::order_lemma_on_ac_explore(const smon& rm, const factorization& ac, u
|
|||
return false;
|
||||
}
|
||||
|
||||
void order::order_lemma_on_factorization(const smon& rm, const factorization& ab) {
|
||||
const monomial& m = _().m_emons[rm.var()];
|
||||
TRACE("nla_solver", tout << "orig_sign = " << _().m_emons.orig_sign(rm) << "\n";);
|
||||
rational sign = _().m_emons.orig_sign(rm);
|
||||
for (factor f: ab)
|
||||
sign *= _().canonize_sign(f);
|
||||
const rational & fv = vvr(ab[0]) * vvr(ab[1]);
|
||||
const rational mv = sign * vvr(m);
|
||||
TRACE("nla_solver",
|
||||
tout << "ab.size()=" << ab.size() << "\n";
|
||||
tout << "we should have sign*vvr(m):" << mv << "=(" << sign << ")*(" << vvr(m) <<") to be equal to " << " vvr(ab[0])*vvr(ab[1]):" << fv << "\n";);
|
||||
if (mv == fv)
|
||||
return;
|
||||
bool gt = mv > fv;
|
||||
TRACE("nla_solver_f", tout << "m="; _().print_monomial_with_vars(m, tout); tout << "\nfactorization="; _().print_factorization(ab, tout););
|
||||
for (unsigned j = 0, k = 1; j < 2; j++, k--) {
|
||||
order_lemma_on_ab(m, sign, var(ab[k]), var(ab[j]), gt);
|
||||
explain(ab); explain(m);
|
||||
explain(rm);
|
||||
TRACE("nla_solver", _().print_lemma(tout););
|
||||
order_lemma_on_ac_explore(rm, ab, j);
|
||||
}
|
||||
}
|
||||
// |c_sign| = 1, and c*c_sign > 0
|
||||
// ac > bc => ac/|c| > bc/|c| => a*c_sign > b*c_sign
|
||||
void order::generate_ol(const smon& ac,
|
||||
|
|
@ -110,25 +243,6 @@ void order::generate_ol(const smon& ac,
|
|||
TRACE("nla_solver", _().print_lemma(tout););
|
||||
}
|
||||
|
||||
void order::generate_mon_ol(const monomial& ac,
|
||||
lpvar a,
|
||||
const rational& c_sign,
|
||||
lpvar c,
|
||||
const smon& bd,
|
||||
const factor& b,
|
||||
const rational& d_sign,
|
||||
lpvar d,
|
||||
llc ab_cmp) {
|
||||
add_empty_lemma();
|
||||
mk_ineq(c_sign, c, llc::LE);
|
||||
explain(c); // this explains c == +- d
|
||||
negate_var_factor_relation(c_sign, a, d_sign, b);
|
||||
mk_ineq(ac.var(), -canonize_sign(bd), var(bd), ab_cmp);
|
||||
explain(bd);
|
||||
explain(b);
|
||||
explain(d);
|
||||
TRACE("nla_solver", print_lemma(tout););
|
||||
}
|
||||
|
||||
void order::negate_var_factor_relation(const rational& a_sign, lpvar a, const rational& b_sign, const factor& b) {
|
||||
rational b_fs = canonize_sign(b);
|
||||
|
|
@ -136,16 +250,6 @@ void order::negate_var_factor_relation(const rational& a_sign, lpvar a, const ra
|
|||
mk_ineq(a_sign, a, - b_fs*b_sign, var(b), cmp);
|
||||
}
|
||||
|
||||
void order::order_lemma() {
|
||||
TRACE("nla_solver", );
|
||||
const auto& rm_ref = c().m_to_refine;
|
||||
unsigned start = random();
|
||||
unsigned sz = rm_ref.size();
|
||||
for (unsigned i = sz; i-- > 0 && !done(); ) {
|
||||
const smon& rm = c().m_emons.canonical[rm_ref[(i + start) % sz]];
|
||||
order_lemma_on_rmonomial(rm);
|
||||
}
|
||||
}
|
||||
|
||||
bool order::order_lemma_on_ac_and_bc_and_factors(const smon& ac,
|
||||
const factor& a,
|
||||
|
|
@ -231,95 +335,5 @@ void order::order_lemma_on_ab(const monomial& m, const rational& sign, lpvar a,
|
|||
else
|
||||
order_lemma_on_ab_lt(m, sign, a, b);
|
||||
}
|
||||
// a > b && c > 0 => ac > bc
|
||||
void order::order_lemma_on_rmonomial(const smon& rm) {
|
||||
TRACE("nla_solver_details",
|
||||
tout << "rm = "; print_product(rm, tout);
|
||||
tout << ", orig = " << pp_mon(c(), c().m_emons[rm.var()]);
|
||||
);
|
||||
for (auto ac : factorization_factory_imp(rm, c())) {
|
||||
if (ac.size() != 2)
|
||||
continue;
|
||||
if (ac.is_mon())
|
||||
order_lemma_on_binomial(*ac.mon());
|
||||
else
|
||||
order_lemma_on_factorization(rm, ac);
|
||||
if (done())
|
||||
break;
|
||||
}
|
||||
}
|
||||
void order::order_lemma_on_binomial_k(const monomial& m, lpvar k, bool gt) {
|
||||
SASSERT(gt == (vvr(m) > vvr(m[0]) * vvr(m[1])));
|
||||
unsigned p = (k + 1) % 2;
|
||||
order_lemma_on_binomial_sign(m, m[k], m[p], gt? 1: -1);
|
||||
}
|
||||
// sign it the sign of vvr(m) - vvr(m[0]) * vvr(m[1])
|
||||
// m = xy
|
||||
// and val(m) != val(x)*val(y)
|
||||
// y > 0 and x = a, then xy >= ay
|
||||
void order::order_lemma_on_binomial_sign(const monomial& ac, lpvar x, lpvar y, int sign) {
|
||||
SASSERT(!_().mon_has_zero(ac));
|
||||
int sy = rat_sign(vvr(y));
|
||||
add_empty_lemma();
|
||||
mk_ineq(y, sy == 1? llc::LE : llc::GE); // negate sy
|
||||
mk_ineq(x, sy*sign == 1? llc::GT:llc::LT , vvr(x)); // assert x <= vvr(x) if x > 0
|
||||
mk_ineq(ac.var(), - vvr(x), y, sign == 1?llc::LE:llc::GE);
|
||||
TRACE("nla_solver", print_lemma(tout););
|
||||
}
|
||||
void order::order_lemma_on_factor_binomial_rm(const monomial& ac, unsigned k, const monomial& bd) {
|
||||
smon const& rm_bd = _().m_emons.canonical[bd];
|
||||
factor d(_().m_evars.find(ac[k]).var(), factor_type::VAR);
|
||||
factor b;
|
||||
if (_().divide(rm_bd, d, b)) {
|
||||
order_lemma_on_binomial_ac_bd(ac, k, rm_bd, b, d.var());
|
||||
}
|
||||
}
|
||||
|
||||
void order::order_lemma_on_binomial_ac_bd(const monomial& ac, unsigned k, const smon& bd, const factor& b, lpvar d) {
|
||||
TRACE("nla_solver", tout << "ac=" << pp_mon(c(), ac);
|
||||
tout << "\nrm=" << bd;
|
||||
print_factor(b, tout << ", b="); print_var(d, tout << ", d=") << "\n";);
|
||||
int p = (k + 1) % 2;
|
||||
lpvar a = ac[p];
|
||||
lpvar c = ac[k];
|
||||
SASSERT(_().m_evars.find(c).var() == d);
|
||||
rational acv = vvr(ac);
|
||||
rational av = vvr(a);
|
||||
rational c_sign = rrat_sign(vvr(c));
|
||||
rational d_sign = rrat_sign(vvr(d));
|
||||
rational bdv = vvr(bd);
|
||||
rational bv = vvr(b);
|
||||
auto av_c_s = av*c_sign; auto bv_d_s = bv*d_sign;
|
||||
|
||||
// suppose ac >= bd, then ac/|c| >= bd/|d|.
|
||||
// Notice that ac/|c| = a*c_sign , and bd/|d| = b*d_sign
|
||||
if (acv >= bdv && av_c_s < bv_d_s)
|
||||
generate_mon_ol(ac, a, c_sign, c, bd, b, d_sign, d, llc::LT);
|
||||
else if (acv <= bdv && av_c_s > bv_d_s)
|
||||
generate_mon_ol(ac, a, c_sign, c, bd, b, d_sign, d, llc::GT);
|
||||
|
||||
}
|
||||
|
||||
void order::order_lemma_on_factor_binomial_explore(const monomial& m, unsigned k) {
|
||||
SASSERT(m.size() == 2);
|
||||
lpvar c = m[k];
|
||||
for (monomial const& m2 : _().m_emons.get_factors_of(c)) {
|
||||
order_lemma_on_factor_binomial_rm(m, k, m2);
|
||||
if (done()) {
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
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[0]) * vvr(ac[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, gt);
|
||||
order_lemma_on_factor_binomial_explore(ac, k);
|
||||
}
|
||||
}
|
||||
} // end of namespace nla
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue