mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

adjust select/store rule for n-ary arrays

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-02-18 20:08:56 -08:00
parent 42f6e1300a
commit ce69b54b5f
1 changed files with 32 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

54
src/qe/mbp/mbp_arrays_tg.cpp
View file

@ -108,19 +108,10 @@ struct mbp_array_tg::impl {
// Note that select may take more than two arguments in general. // Note that select may take more than two arguments in general.
// //
bool is_rd_wr(expr *t) { bool is_rd_wr(expr *t) {
expr* a, *idx; expr* a;
return m_array_util.is_select1(t, a, idx) && return
m_array_util.is_store(a) && m_array_util.is_select(t) &&
has_stores(a); (a = to_app(t)->get_arg(0), m_array_util.is_store(a) && has_stores(a));
}
bool is_rd_wr(expr* t, expr*& wr_ind, expr*& rd_ind, expr*& b, expr*& v) {
if (!is_rd_wr(t))
return false;
expr* a = nullptr;
VERIFY(m_array_util.is_select1(t, a, rd_ind));
VERIFY(m_array_util.is_store1(a, b, wr_ind, v));
return true;
} }
bool is_implicit_peq(expr *e) { bool is_implicit_peq(expr *e) {
@ -282,17 +273,36 @@ struct mbp_array_tg::impl {
} }
// rewrite select(store(a, i, k), j) into either select(a, j) or k // rewrite select(store(a, i, k), j) into either select(a, j) or k
void elimrdwr(expr *term) { void elimrdwr(expr *_term) {
app* term = to_app(_term);
TRACE("mbp_tg", tout << "applying elimrdwr on " << expr_ref(term, m);); TRACE("mbp_tg", tout << "applying elimrdwr on " << expr_ref(term, m););
expr* wr_ind = nullptr, *rd_ind = nullptr, *b = nullptr, *v = nullptr; auto rd_indices = array_select_indices(term);
VERIFY(is_rd_wr(term, wr_ind, rd_ind, b, v)); auto store_term = to_app(term->get_arg(0));
if (m_mdl.are_equal(wr_ind, rd_ind)) auto wr_indices = array_store_indices(store_term);
m_tg.add_eq(wr_ind, rd_ind); auto store_elem = array_store_elem(store_term);
else { auto store_array = store_term->get_arg(0);
m_tg.add_deq(wr_ind, rd_ind); bool all_eq = true;
v = m_array_util.mk_select(b, rd_ind); for (auto rd_idx : rd_indices) {
auto wr_idx = *wr_indices;
if (m_mdl.are_equal(rd_idx, wr_idx))
m_tg.add_eq(rd_idx, wr_idx);
else {
m_tg.add_deq(rd_idx, wr_idx);
all_eq = false;
}
++wr_indices;
} }
m_tg.add_eq(term, v); expr* v;
if (all_eq)
v = store_elem;
else {
ptr_buffer<expr> args;
args.push_back(store_array);
for (auto rd_idx : rd_indices)
args.push_back(rd_idx);
v = m_array_util.mk_select(args);
}
m_tg.add_eq(term, v);
} }
// iterate through all terms in m_tg and apply all array MBP rules once // iterate through all terms in m_tg and apply all array MBP rules once