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

#5604

Browse source 
retain array interpretation when available
This commit is contained in:
Nikolaj Bjorner 2021-10-17 20:24:12 -07:00
parent 115203e87c
commit bc2020a39b
2 changed files with 62 additions and 53 deletions
Download patch file Download diff file Expand all files Collapse all files

99
src/ast/rewriter/array_rewriter.cpp
View file

@ -703,8 +703,60 @@ br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result)
result = m().update_quantifier(lam, quantifier_kind::forall_k, e);
return BR_REWRITE2;
}
expr_ref lh1(m()), rh1(m());
expr_ref_vector fmls(m());
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_expand_store_eq) {
expr* lhs1 = lhs;
expr* rhs1 = rhs;
unsigned num_lhs = 0, num_rhs = 0;
while (m_util.is_store(lhs1)) {
lhs1 = to_app(lhs1)->get_arg(0);
++num_lhs;
}
while (m_util.is_store(rhs1)) {
rhs1 = to_app(rhs1)->get_arg(0);
++num_rhs;
}
if (lhs1 == rhs1) {
mk_eq(lhs, lhs, rhs, fmls);
mk_eq(rhs, lhs, rhs, fmls);
result = m().mk_and(fmls);
return BR_REWRITE_FULL;
}
if (m_util.is_const(lhs1, v) && m_util.is_const(rhs1, w) &&
has_large_domain(lhs->get_sort(), 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;
}
}
if (m_expand_nested_stores) {
expr_ref lh1(m()), rh1(m());
if (is_expandable_store(lhs)) {
lh1 = expand_store(lhs);
}
@ -719,10 +771,6 @@ br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result)
}
}
if (!m_expand_store_eq) {
return BR_FAILED;
}
expr_ref_vector fmls(m());
#if 0
// lambda friendly version of array equality rewriting.
@ -744,46 +792,5 @@ 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) {
mk_eq(lhs, lhs, rhs, fmls);
mk_eq(rhs, lhs, rhs, fmls);
result = m().mk_and(fmls);
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(lhs->get_sort(), 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;
}

16
src/model/func_interp.cpp
View file

@ -280,6 +280,9 @@ void func_interp::compress() {
}
// other compression, if else is a default branch.
// or function encode identity.
#if 0
// breaks array interpretations
// #5604
if (m().is_false(m_else)) {
expr_ref new_else(get_interp(), m());
for (func_entry * curr : m_entries) {
@ -291,7 +294,9 @@ void func_interp::compress() {
m().dec_ref(m_else);
m_else = new_else;
}
else if (!m_entries.empty() && is_identity()) {
else
#endif
if (!m_entries.empty() && is_identity()) {
for (func_entry * curr : m_entries) {
curr->deallocate(m(), m_arity);
}
@ -335,14 +340,11 @@ expr * func_interp::get_interp_core() const {
expr * r = m_else;
ptr_buffer<expr> vars;
for (func_entry * curr : m_entries) {
if (m_else == curr->get_result()) {
if (m_else == curr->get_result())
continue;
}
if (vars.empty()) {
for (unsigned i = 0; i < m_arity; i++) {
if (vars.empty())
for (unsigned i = 0; i < m_arity; i++)
vars.push_back(m().mk_var(i, curr->get_arg(i)->get_sort()));
}
}
ptr_buffer<expr> eqs;
for (unsigned i = 0; i < m_arity; i++) {
eqs.push_back(m().mk_eq(vars[i], curr->get_arg(i)));