mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
for #4588
This commit is contained in:
parent
8857a67e4f
commit
f7b2407a11
|
@ -196,7 +196,7 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args,
|
|||
return BR_REWRITE2;
|
||||
}
|
||||
else {
|
||||
result = m().mk_ite(m().mk_and(eqs.size(), eqs.c_ptr()), v, sel_a_j);
|
||||
result = m().mk_ite(m().mk_and(eqs), v, sel_a_j);
|
||||
return BR_REWRITE3;
|
||||
}
|
||||
}
|
||||
|
@ -756,19 +756,45 @@ br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result)
|
|||
#endif
|
||||
|
||||
expr* lhs1 = lhs;
|
||||
unsigned num_lhs = 0, num_rhs = 0;
|
||||
while (m_util.is_store(lhs1)) {
|
||||
lhs1 = to_app(lhs1)->get_arg(0);
|
||||
++num_lhs;
|
||||
}
|
||||
expr* rhs1 = rhs;
|
||||
while (m_util.is_store(rhs1)) {
|
||||
rhs1 = to_app(rhs1)->get_arg(0);
|
||||
++num_rhs;
|
||||
}
|
||||
if (lhs1 != rhs1) {
|
||||
return BR_FAILED;
|
||||
if (lhs1 == rhs1) {
|
||||
mk_eq(lhs, lhs, rhs, fmls);
|
||||
mk_eq(rhs, lhs, rhs, fmls);
|
||||
result = m().mk_and(fmls);
|
||||
return BR_REWRITE_FULL;
|
||||
}
|
||||
|
||||
mk_eq(lhs, lhs, rhs, fmls);
|
||||
mk_eq(rhs, lhs, rhs, fmls);
|
||||
result = m().mk_and(fmls.size(), fmls.c_ptr());
|
||||
return BR_REWRITE_FULL;
|
||||
auto has_large_domain = [&](sort* s, unsigned num_stores) {
|
||||
unsigned sz = get_array_arity(s);
|
||||
uint64_t dsz = 1;
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
sort* d = get_array_domain(s, i);
|
||||
if (d->is_infinite() || d->is_very_big())
|
||||
return true;
|
||||
auto const& n = d->get_num_elements();
|
||||
if (n.size() > num_stores)
|
||||
return true;
|
||||
dsz *= n.size();
|
||||
if (dsz > num_stores)
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
};
|
||||
if (m_util.is_const(lhs1, v) && m_util.is_const(rhs1, w) &&
|
||||
has_large_domain(m().get_sort(lhs), std::max(num_lhs, num_rhs))) {
|
||||
mk_eq(lhs, lhs, rhs, fmls);
|
||||
mk_eq(rhs, lhs, rhs, fmls);
|
||||
fmls.push_back(m().mk_eq(v, w));
|
||||
result = m().mk_and(fmls);
|
||||
return BR_REWRITE_FULL;
|
||||
}
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue