Skip to content

Commit 991cffb

Browse files
handle multi-arity arrays
1 parent 674e1b8 commit 991cffb

File tree

1 file changed

+52
-37
lines changed

1 file changed

+52
-37
lines changed

src/qe/mbp/mbp_arrays_tg.cpp

+52-37
Original file line numberDiff line numberDiff line change
@@ -13,14 +13,12 @@ Module Name:
1313
1414
Hari Govind V K (hgvk94) 2023-03-07
1515
16-
Revision History:
17-
1816
--*/
1917

20-
#include "qe/mbp/mbp_arrays_tg.h"
2118
#include "ast/array_decl_plugin.h"
2219
#include "ast/array_peq.h"
2320
#include "qe/mbp/mbp_qel_util.h"
21+
#include "qe/mbp/mbp_arrays_tg.h"
2422
#include "util/obj_hashtable.h"
2523
#include "util/obj_pair_hashtable.h"
2624

@@ -83,8 +81,10 @@ struct mbp_array_tg::impl {
8381
// Returns true if e has a subterm store(v) where v is a variable to be
8482
// eliminated. Recurses on subexpressions of ee
8583
bool has_stores(expr *e) {
86-
if (m_has_stores.is_marked(e)) return true;
87-
if (!is_app(e)) return false;
84+
if (m_has_stores.is_marked(e))
85+
return true;
86+
if (!is_app(e))
87+
return false;
8888
if (m_array_util.is_store(e) && is_var(to_app(e)->get_arg(0))) {
8989
m_has_stores.mark(e, true);
9090
return true;
@@ -94,7 +94,7 @@ struct mbp_array_tg::impl {
9494
return true;
9595
}
9696
//recurse
97-
for(auto c : *(to_app(e))) {
97+
for (auto c : *(to_app(e))) {
9898
if (has_stores(c)) {
9999
m_has_stores.mark(e, true);
100100
return true;
@@ -166,56 +166,73 @@ struct mbp_array_tg::impl {
166166
}
167167

168168
// rewrite store(x, j, elem) \peq_{indices} y
169-
// into either j = i && x \peq_{indices} y (for some i in
170-
// indices) or &&_{i \in indices} j \neq i &&
169+
// into either j = i && x \peq_{indices} y (for some i in indices)
170+
// or &&_{i \in indices} j \neq i &&
171171
// x \peq_{indices, j} y &&
172172
// select(y, j) = elem
173173
// rewrite negation !(store(x, j, elem) \peq_{indices} y) into
174-
// into either j = i && !(x \peq_{indices} y) (for some i in
175-
// indices) or &&_{i \in indices} j \neq i &&
174+
// into either j = i && !(x \peq_{indices} y) (for some i in indices)
175+
// or &&_{i \in indices} j \neq i &&
176176
// !(x \peq_{indices, j} y) &&
177-
// or &&_{i \in indices} j \neq i &&
177+
// or &&_{i \in indices} j \neq i &&
178178
// !(select(y, j) = elem)
179179
void elimwreq(peq p, bool is_neg) {
180-
expr* a = nullptr, *j = nullptr, *elem = nullptr;
181-
VERIFY(is_arr_write(p.lhs(), a, j, elem)); // TDOO: make this work with multi-arity arrays
180+
181+
SASSERT(m_array_util.is_store(p.lhs()));
182+
expr* a = to_app(p.lhs())->get_arg(0);
183+
auto js = array_store_indices(to_app(p.lhs()));
184+
auto elem = array_store_elem(to_app(p.lhs()));
185+
182186
TRACE("mbp_tg",
183187
tout << "applying elimwreq on " << expr_ref(p.mk_peq(), m) << " is neg: " << is_neg << "\n");
184188
vector<expr_ref_vector> indices;
185189
bool in = false;
186-
p.get_diff_indices(indices);
187-
expr_ref eq_index(m);
188-
expr_ref_vector deq(m);
190+
p.get_diff_indices(indices);
191+
unsigned eq_index = UINT_MAX, idx = 0;
192+
svector<std::pair<expr*, expr*>> deq;
189193
for (expr_ref_vector &e : indices) {
190-
for (expr *i : e) {
191-
if (m_mdl.are_equal(j, i)) {
192-
in = true;
193-
// save for later
194-
eq_index = i;
195-
break;
196-
}
197-
else
198-
deq.push_back(i);
194+
auto jit = js.begin();
195+
bool is_eq = true;
196+
for (expr* i : e) {
197+
if (!m_mdl.are_equal(*jit, i)) {
198+
if (is_eq)
199+
deq.push_back({ *jit, i });
200+
is_eq = false;
201+
}
202+
++jit;
199203
}
204+
if (is_eq) {
205+
in = true;
206+
eq_index = idx;
207+
break;
208+
}
200209
}
201210
if (in) {
202-
SASSERT(m_mdl.are_equal(j, eq_index));
203-
peq p_new =
204-
mk_wr_peq(a, p.rhs(), indices);
205-
m_tg.add_eq(j, eq_index);
211+
peq p_new = mk_wr_peq(a, p.rhs(), indices);
212+
auto jit = js.begin();
213+
for (expr* i : indices[eq_index]) {
214+
m_tg.add_eq(*jit, i);
215+
++jit;
216+
}
206217
expr_ref p_new_expr(m);
207218
p_new_expr = is_neg ? m.mk_not(p_new.mk_peq()) : p_new.mk_peq();
208219
m_tg.add_lit(p_new_expr);
209220
m_tg.add_eq(p_new.mk_peq(), p.mk_peq());
210221
return;
211222
}
212-
for (expr *d : deq)
213-
m_tg.add_deq(j, d);
223+
for (auto [i, j] : deq)
224+
m_tg.add_deq(i, j);
225+
214226
expr_ref_vector setOne(m);
215-
setOne.push_back(j);
227+
for (auto j : js)
228+
setOne.push_back(j);
216229
indices.push_back(setOne);
217230
peq p_new = mk_wr_peq(a, p.rhs(), indices);
218-
expr_ref rd(m_array_util.mk_select(p.rhs(), j), m);
231+
ptr_buffer<expr> args;
232+
args.push_back(p.rhs());
233+
for (auto j : js)
234+
args.push_back(j);
235+
expr_ref rd(m_array_util.mk_select(args), m);
219236
if (!is_neg) {
220237
m_tg.add_lit(p_new.mk_peq());
221238
m_tg.add_eq(rd, elem);
@@ -273,8 +290,7 @@ struct mbp_array_tg::impl {
273290
}
274291

275292
// rewrite select(store(a, i, k), j) into either select(a, j) or k
276-
void elimrdwr(expr *_term) {
277-
app* term = to_app(_term);
293+
void elimrdwr(app *term) {
278294
TRACE("mbp_tg", tout << "applying elimrdwr on " << expr_ref(term, m););
279295
auto rd_indices = array_select_indices(term);
280296
auto store_term = to_app(term->get_arg(0));
@@ -370,11 +386,10 @@ struct mbp_array_tg::impl {
370386
continue;
371387
}
372388
}
373-
TRACE("mbp_tg", tout << "not applying any rules on " << expr_ref(nt, m) << " " << is_rd_wr(nt) << " " << m_use_mdl << "\n";);
374389
if (m_use_mdl && is_rd_wr(nt)) {
375390
mark_seen(term);
376391
progress = true;
377-
elimrdwr(nt);
392+
elimrdwr(to_app(nt));
378393
continue;
379394
}
380395
}

0 commit comments

Comments
 (0)