mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 01:24:08 +00:00
#6999 deal with implicit assumptions, more robust pattern matching
The code is making some assumptions that arrays are 1-dimensional. This is not generally true. Introducing pattern matching to ensure the assumption is met. Avoid get_arg(..) especially when there is an approach based on pattern matching recognizers.
This commit is contained in:
parent
6d6d6b8ed0
commit
b9455c3692
|
@ -186,6 +186,21 @@ public:
|
|||
|
||||
bool is_store_ext(expr* e, expr_ref& a, expr_ref_vector& args, expr_ref& value);
|
||||
|
||||
|
||||
bool is_select1(expr* n) const { return is_select(n) && to_app(n)->get_num_args() == 2; }
|
||||
|
||||
bool is_select1(expr* n, expr*& a, expr*& i) const {
|
||||
return is_select1(n) && (a = to_app(n)->get_arg(0), i = to_app(n)->get_arg(1), true);
|
||||
}
|
||||
|
||||
bool is_store1(expr* n) const { return is_store(n) && to_app(n)->get_num_args() == 3; }
|
||||
|
||||
bool is_store1(expr* n, expr*& a, expr*& i, expr*& v) const {
|
||||
app* _n;
|
||||
return is_store1(n) && (_n = to_app(n), a = _n->get_arg(0), i = _n->get_arg(1), v = _n->get_arg(2), true);
|
||||
}
|
||||
|
||||
|
||||
MATCH_BINARY(is_subset);
|
||||
};
|
||||
|
||||
|
@ -213,6 +228,11 @@ public:
|
|||
return mk_store(args.size(), args.data());
|
||||
}
|
||||
|
||||
app * mk_select(expr* a, expr* i) const {
|
||||
expr* args[2] = { a, i };
|
||||
return mk_select(2, args);
|
||||
}
|
||||
|
||||
app * mk_select(unsigned num_args, expr * const * args) const {
|
||||
return m_manager.mk_app(m_fid, OP_SELECT, 0, nullptr, num_args, args);
|
||||
}
|
||||
|
|
|
@ -72,8 +72,11 @@ struct mbp_array_tg::impl {
|
|||
}
|
||||
|
||||
bool is_arr_write(expr *t) {
|
||||
if (!m_array_util.is_store(t)) return false;
|
||||
return has_var(to_app(t));
|
||||
return m_array_util.is_store1(t) && has_var(to_app(t));
|
||||
}
|
||||
|
||||
bool is_arr_write(expr *t, expr*& a, expr*& i, expr*& v) {
|
||||
return m_array_util.is_store1(t, a, i, v) && has_var(to_app(t));
|
||||
}
|
||||
|
||||
// Returns true if e has a subterm store(v) where v is a variable to be
|
||||
|
@ -99,25 +102,50 @@ struct mbp_array_tg::impl {
|
|||
return false;
|
||||
}
|
||||
|
||||
//
|
||||
// the code that uses this assumes that select takes only two arguments.
|
||||
// Note that select may take more than two arguments in general.
|
||||
//
|
||||
bool is_rd_wr(expr *t) {
|
||||
if (!m_array_util.is_select(t)) return false;
|
||||
return m_array_util.is_store(to_app(t)->get_arg(0)) &&
|
||||
has_stores(to_app(t)->get_arg(0));
|
||||
expr* a, *idx;
|
||||
return m_array_util.is_select1(t, a, idx) &&
|
||||
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;
|
||||
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) {
|
||||
return m.is_eq(e) &&
|
||||
is_implicit_peq(to_app(e)->get_arg(0), to_app(e)->get_arg(1));
|
||||
expr* a, *b;
|
||||
return is_implicit_peq(e, a, b);
|
||||
}
|
||||
|
||||
bool is_implicit_peq(expr *e, expr*& a, expr*& b) {
|
||||
return m.is_eq(e, a, b) && is_implicit_peq(a, b);
|
||||
}
|
||||
|
||||
bool is_implicit_peq(expr *lhs, expr *rhs) {
|
||||
return m_array_util.is_array(lhs) && m_array_util.is_array(rhs) &&
|
||||
(has_var(lhs) || has_var(rhs));
|
||||
}
|
||||
|
||||
bool is_neg_peq(expr *e, expr*& a, expr*& b) {
|
||||
expr* ne;
|
||||
return m.is_not(e, ne) && is_implicit_peq(ne, a, b);
|
||||
}
|
||||
|
||||
bool is_neg_peq(expr *e) {
|
||||
expr* ne;
|
||||
return m.is_not(e, ne) && is_implicit_peq(ne);
|
||||
}
|
||||
|
||||
void mark_seen(expr *t) { m_seen.mark(t); }
|
||||
bool is_seen(expr *t) { return m_seen.is_marked(t); }
|
||||
void mark_seen(expr *t1, expr *t2) { m_seenp.insert(expr_pair(t1, t2)); }
|
||||
|
@ -140,7 +168,8 @@ struct mbp_array_tg::impl {
|
|||
// create a peq where write terms are preferred on the left hand side
|
||||
peq mk_wr_peq(expr *e1, expr *e2, vector<expr_ref_vector> &indices) {
|
||||
expr *n_lhs = e1, *n_rhs = e2;
|
||||
if (is_wr_on_rhs(e1, e2)) std::swap(n_lhs, n_rhs);
|
||||
if (is_wr_on_rhs(e1, e2))
|
||||
std::swap(n_lhs, n_rhs);
|
||||
return peq(n_lhs, n_rhs, indices, m);
|
||||
}
|
||||
|
||||
|
@ -156,12 +185,11 @@ struct mbp_array_tg::impl {
|
|||
// or &&_{i \in indices} j \neq i &&
|
||||
// !(select(y, j) = elem)
|
||||
void elimwreq(peq p, bool is_neg) {
|
||||
SASSERT(is_arr_write(p.lhs()));
|
||||
expr* a, *j, *elem;
|
||||
VERIFY(is_arr_write(p.lhs(), a, j, elem));
|
||||
TRACE("mbp_tg",
|
||||
tout << "applying elimwreq on " << expr_ref(p.mk_peq(), m) << " is neg: " << is_neg;);
|
||||
vector<expr_ref_vector> indices;
|
||||
expr *j = to_app(p.lhs())->get_arg(1);
|
||||
expr *elem = to_app(p.lhs())->get_arg(2);
|
||||
bool in = false;
|
||||
p.get_diff_indices(indices);
|
||||
expr_ref eq_index(m);
|
||||
|
@ -180,7 +208,7 @@ struct mbp_array_tg::impl {
|
|||
if (in) {
|
||||
SASSERT(m_mdl.are_equal(j, eq_index));
|
||||
peq p_new =
|
||||
mk_wr_peq(to_app(p.lhs())->get_arg(0), p.rhs(), indices);
|
||||
mk_wr_peq(to_app(a, p.rhs(), indices);
|
||||
m_tg.add_eq(j, eq_index);
|
||||
expr_ref p_new_expr(m);
|
||||
p_new_expr = is_neg ? m.mk_not(p_new.mk_peq()) : p_new.mk_peq();
|
||||
|
@ -192,9 +220,8 @@ struct mbp_array_tg::impl {
|
|||
expr_ref_vector setOne(m);
|
||||
setOne.push_back(j);
|
||||
indices.push_back(setOne);
|
||||
peq p_new = mk_wr_peq(to_app(p.lhs())->get_arg(0), p.rhs(), indices);
|
||||
expr *args[2] = {p.rhs(), j};
|
||||
expr_ref rd(m_array_util.mk_select(2, args), m);
|
||||
peq p_new = mk_wr_peq(a, p.rhs(), indices);
|
||||
expr_ref rd(m_array_util.mk_select(p.rhs(), j), m);
|
||||
if (!is_neg) {
|
||||
m_tg.add_lit(p_new.mk_peq());
|
||||
m_tg.add_eq(rd, elem);
|
||||
|
@ -240,8 +267,7 @@ struct mbp_array_tg::impl {
|
|||
m_tg.add_var(a);
|
||||
auto const &indx = std::next(itr, i);
|
||||
SASSERT(indx->size() == 1);
|
||||
expr *args[2] = {to_app(p.lhs()), to_app(indx->get(0))};
|
||||
sel = m_array_util.mk_select(2, args);
|
||||
sel = m_array_util.mk_select(p.lhs(), indx->get(0));
|
||||
m_mdl.register_decl(a->get_decl(), m_mdl(sel));
|
||||
i++;
|
||||
}
|
||||
|
@ -252,21 +278,16 @@ struct mbp_array_tg::impl {
|
|||
|
||||
// rewrite select(store(a, i, k), j) into either select(a, j) or k
|
||||
void elimrdwr(expr *term) {
|
||||
SASSERT(is_rd_wr(term));
|
||||
TRACE("mbp_tg", tout << "applying elimrdwr on " << expr_ref(term, m););
|
||||
expr *wr_ind = to_app(to_app(term)->get_arg(0))->get_arg(1);
|
||||
expr *rd_ind = to_app(term)->get_arg(1);
|
||||
expr *e;
|
||||
if (m_mdl.are_equal(wr_ind, rd_ind)) {
|
||||
expr* wr_ind, *rd_ind, *b, *v;
|
||||
VERIFY(is_rd_wr(term, wr_ind, rd_ind, b, v));
|
||||
if (m_mdl.are_equal(wr_ind, rd_ind))
|
||||
m_tg.add_eq(wr_ind, rd_ind);
|
||||
e = to_app(to_app(term)->get_arg(0))->get_arg(2);
|
||||
} else {
|
||||
else {
|
||||
m_tg.add_deq(wr_ind, rd_ind);
|
||||
expr *args[2] = {to_app(to_app(term)->get_arg(0))->get_arg(0),
|
||||
to_app(term)->get_arg(1)};
|
||||
e = m_array_util.mk_select(2, args);
|
||||
v = m_array_util.mk_select(b, rd_ind);
|
||||
}
|
||||
m_tg.add_eq(term, e);
|
||||
m_tg.add_eq(term, v);
|
||||
}
|
||||
|
||||
// iterate through all terms in m_tg and apply all array MBP rules once
|
||||
|
@ -284,18 +305,19 @@ struct mbp_array_tg::impl {
|
|||
m_tg.get_terms(terms, false);
|
||||
for (unsigned i = 0; i < terms.size(); i++) {
|
||||
term = terms.get(i);
|
||||
if (m_seen.is_marked(term)) continue;
|
||||
if (m_tg.is_cgr(term)) continue;
|
||||
if (m_seen.is_marked(term))
|
||||
continue;
|
||||
if (m_tg.is_cgr(term))
|
||||
continue;
|
||||
TRACE("mbp_tg", tout << "processing " << expr_ref(term, m););
|
||||
if (is_implicit_peq(term) || is_neg_peq(term)) {
|
||||
expr* a, *b;
|
||||
if (is_implicit_peq(term, a, b) || is_neg_peq(term, a, b)) {
|
||||
// rewrite array eq as peq
|
||||
mark_seen(term);
|
||||
progress = true;
|
||||
nt = term;
|
||||
bool is_not = m.is_not(term, nt);
|
||||
e = mk_wr_peq(to_app(nt)->get_arg(0),
|
||||
to_app(nt)->get_arg(1))
|
||||
.mk_peq();
|
||||
e = mk_wr_peq(a, b).mk_peq();
|
||||
e = is_not ? m.mk_not(e) : e.get();
|
||||
m_tg.add_lit(e);
|
||||
m_tg.add_eq(term, e);
|
||||
|
|
Loading…
Reference in a new issue