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

handle multi-arity arrays

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-02-18 20:38:45 -08:00
parent 674e1b8f98
commit 991cffb519
1 changed files with 52 additions and 37 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -13,14 +13,12 @@ Author:
Hari Govind V K (hgvk94) 2023-03-07 Hari Govind V K (hgvk94) 2023-03-07
Revision History:
--*/ --*/
#include "qe/mbp/mbp_arrays_tg.h"
#include "ast/array_decl_plugin.h" #include "ast/array_decl_plugin.h"
#include "ast/array_peq.h" #include "ast/array_peq.h"
#include "qe/mbp/mbp_qel_util.h" #include "qe/mbp/mbp_qel_util.h"
#include "qe/mbp/mbp_arrays_tg.h"
#include "util/obj_hashtable.h" #include "util/obj_hashtable.h"
#include "util/obj_pair_hashtable.h" #include "util/obj_pair_hashtable.h"
@ -83,8 +81,10 @@ struct mbp_array_tg::impl {
// Returns true if e has a subterm store(v) where v is a variable to be // Returns true if e has a subterm store(v) where v is a variable to be
// eliminated. Recurses on subexpressions of ee // eliminated. Recurses on subexpressions of ee
bool has_stores(expr *e) { bool has_stores(expr *e) {
if (m_has_stores.is_marked(e)) return true; if (m_has_stores.is_marked(e))
if (!is_app(e)) return false; return true;
if (!is_app(e))
return false;
if (m_array_util.is_store(e) && is_var(to_app(e)->get_arg(0))) { if (m_array_util.is_store(e) && is_var(to_app(e)->get_arg(0))) {
m_has_stores.mark(e, true); m_has_stores.mark(e, true);
return true; return true;
@ -94,7 +94,7 @@ struct mbp_array_tg::impl {
return true; return true;
} }
//recurse //recurse
for(auto c : *(to_app(e))) { for (auto c : *(to_app(e))) {
if (has_stores(c)) { if (has_stores(c)) {
m_has_stores.mark(e, true); m_has_stores.mark(e, true);
return true; return true;
@ -166,56 +166,73 @@ struct mbp_array_tg::impl {
} }
// rewrite store(x, j, elem) \peq_{indices} y // rewrite store(x, j, elem) \peq_{indices} y
// into either j = i && x \peq_{indices} y (for some i in // into either j = i && x \peq_{indices} y (for some i in indices)
// indices) or &&_{i \in indices} j \neq i && // or &&_{i \in indices} j \neq i &&
// x \peq_{indices, j} y && // x \peq_{indices, j} y &&
// select(y, j) = elem // select(y, j) = elem
// rewrite negation !(store(x, j, elem) \peq_{indices} y) into // rewrite negation !(store(x, j, elem) \peq_{indices} y) into
// into either j = i && !(x \peq_{indices} y) (for some i in // into either j = i && !(x \peq_{indices} y) (for some i in indices)
// indices) or &&_{i \in indices} j \neq i && // or &&_{i \in indices} j \neq i &&
// !(x \peq_{indices, j} y) && // !(x \peq_{indices, j} y) &&
// or &&_{i \in indices} j \neq i && // or &&_{i \in indices} j \neq i &&
// !(select(y, j) = elem) // !(select(y, j) = elem)
void elimwreq(peq p, bool is_neg) { void elimwreq(peq p, bool is_neg) {
expr* a = nullptr, *j = nullptr, *elem = nullptr;
VERIFY(is_arr_write(p.lhs(), a, j, elem)); // TDOO: make this work with multi-arity arrays SASSERT(m_array_util.is_store(p.lhs()));
expr* a = to_app(p.lhs())->get_arg(0);
auto js = array_store_indices(to_app(p.lhs()));
auto elem = array_store_elem(to_app(p.lhs()));
TRACE("mbp_tg", TRACE("mbp_tg",
tout << "applying elimwreq on " << expr_ref(p.mk_peq(), m) << " is neg: " << is_neg << "\n"); tout << "applying elimwreq on " << expr_ref(p.mk_peq(), m) << " is neg: " << is_neg << "\n");
vector<expr_ref_vector> indices; vector<expr_ref_vector> indices;
bool in = false; bool in = false;
p.get_diff_indices(indices); p.get_diff_indices(indices);
expr_ref eq_index(m); unsigned eq_index = UINT_MAX, idx = 0;
expr_ref_vector deq(m); svector<std::pair<expr*, expr*>> deq;
for (expr_ref_vector &e : indices) { for (expr_ref_vector &e : indices) {
for (expr *i : e) { auto jit = js.begin();
if (m_mdl.are_equal(j, i)) { bool is_eq = true;
in = true; for (expr* i : e) {
// save for later if (!m_mdl.are_equal(*jit, i)) {
eq_index = i; if (is_eq)
break; deq.push_back({ *jit, i });
} is_eq = false;
else }
deq.push_back(i); ++jit;
} }
if (is_eq) {
in = true;
eq_index = idx;
break;
}
} }
if (in) { if (in) {
SASSERT(m_mdl.are_equal(j, eq_index)); peq p_new = mk_wr_peq(a, p.rhs(), indices);
peq p_new = auto jit = js.begin();
mk_wr_peq(a, p.rhs(), indices); for (expr* i : indices[eq_index]) {
m_tg.add_eq(j, eq_index); m_tg.add_eq(*jit, i);
++jit;
}
expr_ref p_new_expr(m); expr_ref p_new_expr(m);
p_new_expr = is_neg ? m.mk_not(p_new.mk_peq()) : p_new.mk_peq(); p_new_expr = is_neg ? m.mk_not(p_new.mk_peq()) : p_new.mk_peq();
m_tg.add_lit(p_new_expr); m_tg.add_lit(p_new_expr);
m_tg.add_eq(p_new.mk_peq(), p.mk_peq()); m_tg.add_eq(p_new.mk_peq(), p.mk_peq());
return; return;
} }
for (expr *d : deq) for (auto [i, j] : deq)
m_tg.add_deq(j, d); m_tg.add_deq(i, j);
expr_ref_vector setOne(m); expr_ref_vector setOne(m);
setOne.push_back(j); for (auto j : js)
setOne.push_back(j);
indices.push_back(setOne); indices.push_back(setOne);
peq p_new = mk_wr_peq(a, p.rhs(), indices); peq p_new = mk_wr_peq(a, p.rhs(), indices);
expr_ref rd(m_array_util.mk_select(p.rhs(), j), m); ptr_buffer<expr> args;
args.push_back(p.rhs());
for (auto j : js)
args.push_back(j);
expr_ref rd(m_array_util.mk_select(args), m);
if (!is_neg) { if (!is_neg) {
m_tg.add_lit(p_new.mk_peq()); m_tg.add_lit(p_new.mk_peq());
m_tg.add_eq(rd, elem); m_tg.add_eq(rd, elem);
@ -273,8 +290,7 @@ 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(app *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););
auto rd_indices = array_select_indices(term); auto rd_indices = array_select_indices(term);
auto store_term = to_app(term->get_arg(0)); auto store_term = to_app(term->get_arg(0));
@ -370,11 +386,10 @@ struct mbp_array_tg::impl {
continue; continue;
} }
} }
TRACE("mbp_tg", tout << "not applying any rules on " << expr_ref(nt, m) << " " << is_rd_wr(nt) << " " << m_use_mdl << "\n";);
if (m_use_mdl && is_rd_wr(nt)) { if (m_use_mdl && is_rd_wr(nt)) {
mark_seen(term); mark_seen(term);
progress = true; progress = true;
elimrdwr(nt); elimrdwr(to_app(nt));
continue; continue;
} }
} }