mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix nex division

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-10-04 10:39:22 -07:00
parent f8a45d2fb3
commit 08de9ecbd1
2 changed files with 35 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

64
src/math/lp/nex_creator.cpp
View file

@ -554,25 +554,15 @@ nex * nex_creator::mk_div_sum_by_mul(const nex_sum* m, const nex_mul* b) {
return r; return r;
} }
nex * nex_creator::mk_div_by_mul(const nex* a, const nex_mul* b) { nex * nex_creator::mk_div_mul_by_mul(const nex_mul *a, const nex_mul* b) {
if (a->is_sum()) { SASSERT(all_factors_are_elementary(a) && all_factors_are_elementary(b));
return mk_div_sum_by_mul(to_sum(a), b);
}
if (a->is_var()) {
SASSERT(b->get_degree() == 1 && !b->has_a_coeff() && get_vars_of_expr(a) == get_vars_of_expr(b));
return mk_scalar(rational(1));
}
const nex_mul* am = to_mul(a);
SASSERT(all_factors_are_elementary(am) && all_factors_are_elementary(b) && have_no_scalars(b));
b->get_powers_from_mul(m_powers); b->get_powers_from_mul(m_powers);
nex_mul* ret = new nex_mul(); nex_mul* ret = new nex_mul();
for (auto& p : *am) { for (auto& p_from_a : *a) {
TRACE("nla_cn_details", tout << "p = " << p << "\n";); TRACE("nla_cn_details", tout << "p_from_a = " << p_from_a << "\n";);
const nex* e = p.e(); const nex* e = p_from_a.e();
if (!e->is_var()) { if (e->is_scalar()) {
SASSERT(e->is_scalar()); ret->add_child_in_power(clone(e), p_from_a.pow());
ret->add_child_in_power(clone(e), p.pow());
TRACE("nla_cn_details", tout << "processed scalar\n";); TRACE("nla_cn_details", tout << "processed scalar\n";);
continue; continue;
} }
@ -580,20 +570,21 @@ nex * nex_creator::mk_div_by_mul(const nex* a, const nex_mul* b) {
lpvar j = to_var(e)->var(); lpvar j = to_var(e)->var();
auto it = m_powers.find(j); auto it = m_powers.find(j);
if (it == m_powers.end()) { if (it == m_powers.end()) {
ret->add_child_in_power(clone(e), p.pow()); ret->add_child_in_power(clone(e), p_from_a.pow());
} else { } else {
unsigned pw = p.pow(); unsigned pa = p_from_a.pow();
SASSERT(pw); unsigned& pb = it->second;
while (pw--) { SASSERT(pa);
SASSERT(it->second); if (pa > pb) {
it->second --; ret->add_child_in_power(mk_var(j), pa - pb);
if (it->second == 0) { m_powers.erase(it);
m_powers.erase(it); } else if (pa == pb) {
break; m_powers.erase(it);
} } else {
} SASSERT(pa < pb);
if (pw) { // not adding the factor here, it was eaten by b,
ret->add_child_in_power(clone(e), pw); // but the key j in m_powers remains
pb -= pa;
} }
} }
TRACE("nla_cn_details", tout << *ret << "\n";); TRACE("nla_cn_details", tout << *ret << "\n";);
@ -609,6 +600,19 @@ nex * nex_creator::mk_div_by_mul(const nex* a, const nex_mul* b) {
return ret; return ret;
} }
nex * nex_creator::mk_div_by_mul(const nex* a, const nex_mul* b) {
SASSERT(have_no_scalars(b));
if (a->is_sum()) {
return mk_div_sum_by_mul(to_sum(a), b);
}
if (a->is_var()) {
SASSERT(b->get_degree() == 1 && get_vars_of_expr(a) == get_vars_of_expr(b));
return mk_scalar(rational(1));
}
return mk_div_mul_by_mul(to_mul(a), b);
}
nex * nex_creator::mk_div(const nex* a, const nex* b) { nex * nex_creator::mk_div(const nex* a, const nex* b) {
TRACE("nla_cn_details", tout << *a <<" / " << *b << "\n";); TRACE("nla_cn_details", tout << *a <<" / " << *b << "\n";);
if (b->is_var()) { if (b->is_var()) {

1
src/math/lp/nex_creator.h
View file

@ -204,6 +204,7 @@ public:
nex * mk_div(const nex* a, const nex* b); nex * mk_div(const nex* a, const nex* b);
nex * mk_div_by_mul(const nex* a, const nex_mul* b); nex * mk_div_by_mul(const nex* a, const nex_mul* b);
nex * mk_div_sum_by_mul(const nex_sum* a, const nex_mul* b); nex * mk_div_sum_by_mul(const nex_sum* a, const nex_mul* b);
nex * mk_div_mul_by_mul(const nex_mul* a, const nex_mul* b);
nex * simplify_mul(nex_mul *e); nex * simplify_mul(nex_mul *e);
bool is_sorted(const nex_mul * e) const; bool is_sorted(const nex_mul * e) const;