mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 11:22:04 +00:00
Code Activity

treat monomial factorization in a special way in generate_pl()

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-04-01 14:06:12 -07:00
parent e32c1bdee8
commit f828dc9451
1 changed files with 32 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

37
src/util/lp/nla_solver.cpp
View file

@ -1595,12 +1595,39 @@ struct solver::imp {
return false; return false;
} }
// none of the factors is zero -> |fc[factor_index]| <= |rm| // if there are no zero factors then |m| >= |m[factor_index]|
void generate_pl_on_mon(const monomial& m, unsigned factor_index) {
add_empty_lemma();
unsigned mon_var = m.var();
rational mv = vvr(mon_var);
rational sm = rational(rat_sign(mv));
mk_ineq(sm, mon_var, llc::LT);
for (unsigned fi = 0; fi < m.size(); fi ++) {
lpvar j = m[fi];
if (fi != factor_index) {
mk_ineq(j, llc::EQ);
} else {
rational jv = vvr(j);
rational sj = rational(rat_sign(jv));
SASSERT(sm*mv < sj*jv);
mk_ineq(sj, j, llc::LT);
mk_ineq(sm, mon_var, -sj, j, llc::GE );
}
}
TRACE("nla_solver", print_lemma(tout); );
}
// none of the factors is zero and the product is not zero
// -> |fc[factor_index]| <= |rm|
void generate_pl(const rooted_mon& rm, const factorization& fc, int factor_index) { void generate_pl(const rooted_mon& rm, const factorization& fc, int factor_index) {
TRACE("nla_solver", tout << "factor_index = " << factor_index << ", rm = "; TRACE("nla_solver", tout << "factor_index = " << factor_index << ", rm = ";
print_rooted_monomial_with_vars(rm, tout); print_rooted_monomial_with_vars(rm, tout);
tout << "fc = "; print_factorization(fc, tout); tout << "fc = "; print_factorization(fc, tout);
tout << "orig mon = "; print_monomial(m_monomials[rm.orig_index()], tout);); tout << "orig mon = "; print_monomial(m_monomials[rm.orig_index()], tout););
if (fc.is_mon()) {
generate_pl_on_mon(*fc.mon(), factor_index);
return;
}
add_empty_lemma(); add_empty_lemma();
int fi = 0; int fi = 0;
rational rmv = vvr(rm); rational rmv = vvr(rm);
@ -1616,7 +1643,7 @@ struct solver::imp {
rational sj = rational(rat_sign(jv)); rational sj = rational(rat_sign(jv));
SASSERT(sm*rmv < sj*jv); SASSERT(sm*rmv < sj*jv);
mk_ineq(sj, j, llc::LT); mk_ineq(sj, j, llc::LT);
mk_ineq(sm, mon_var, -sj, j, llc::GE); mk_ineq(sm, mon_var, -sj, j, llc::GE );
} }
} }
if (!fc.is_mon()) { if (!fc.is_mon()) {
@ -1645,21 +1672,19 @@ struct solver::imp {
} }
// x != 0 or y = 0 => |xy| >= |y| // x != 0 or y = 0 => |xy| >= |y|
bool proportion_lemma_model_based(const rooted_mon& rm, const factorization& factorization) { void proportion_lemma_model_based(const rooted_mon& rm, const factorization& factorization) {
rational rmv = abs(vvr(rm)); rational rmv = abs(vvr(rm));
if (rmv.is_zero()) { if (rmv.is_zero()) {
SASSERT(has_zero_factor(factorization)); SASSERT(has_zero_factor(factorization));
return false; return;
} }
int factor_index = 0; int factor_index = 0;
for (factor f : factorization) { for (factor f : factorization) {
if (abs(vvr(f)) > rmv) { if (abs(vvr(f)) > rmv) {
generate_pl(rm, factorization, factor_index); generate_pl(rm, factorization, factor_index);
return true;
} }
factor_index++; factor_index++;
} }
return false;
} }
// x != 0 or y = 0 => |xy| >= |y| // x != 0 or y = 0 => |xy| >= |y|
bool proportion_lemma_derived(const rooted_mon& rm, const factorization& factorization) { bool proportion_lemma_derived(const rooted_mon& rm, const factorization& factorization) {