1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3
4 Module Name:
5
6 array_rewriter.cpp
7
8 Abstract:
9
10 Basic rewriting rules for Arrays.
11
12 Author:
13
14 Leonardo (leonardo) 2011-04-06
15
16 Notes:
17
18 --*/
19 #include "ast/rewriter/array_rewriter.h"
20 #include "ast/ast_lt.h"
21 #include "ast/ast_util.h"
22 #include "ast/ast_pp.h"
23 #include "ast/ast_ll_pp.h"
24 #include "ast/rewriter/var_subst.h"
25 #include "params/array_rewriter_params.hpp"
26
updt_params(params_ref const & _p)27 void array_rewriter::updt_params(params_ref const & _p) {
28 array_rewriter_params p(_p);
29 m_sort_store = p.sort_store();
30 m_expand_select_store = p.expand_select_store();
31 m_expand_store_eq = p.expand_store_eq();
32 m_expand_nested_stores = p.expand_nested_stores();
33 m_blast_select_store = p.blast_select_store();
34 m_expand_select_ite = p.expand_select_ite();
35 }
36
get_param_descrs(param_descrs & r)37 void array_rewriter::get_param_descrs(param_descrs & r) {
38 array_rewriter_params::collect_param_descrs(r);
39 }
40
mk_app_core(func_decl * f,unsigned num_args,expr * const * args,expr_ref & result)41 br_status array_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
42 SASSERT(f->get_family_id() == get_fid());
43 br_status st;
44 switch (f->get_decl_kind()) {
45 case OP_SELECT:
46 st = mk_select_core(num_args, args, result);
47 break;
48 case OP_STORE:
49 st = mk_store_core(num_args, args, result);
50 break;
51 case OP_ARRAY_MAP:
52 st = mk_map_core(m_util.get_map_func_decl(f), num_args, args, result);
53 break;
54 case OP_SET_UNION:
55 st = mk_set_union(num_args, args, result);
56 break;
57 case OP_SET_INTERSECT:
58 st = mk_set_intersect(num_args, args, result);
59 break;
60 case OP_SET_SUBSET:
61 SASSERT(num_args == 2);
62 st = mk_set_subset(args[0], args[1], result);
63 break;
64 case OP_SET_COMPLEMENT:
65 SASSERT(num_args == 1);
66 st = mk_set_complement(args[0], result);
67 break;
68 case OP_SET_DIFFERENCE:
69 SASSERT(num_args == 2);
70 st = mk_set_difference(args[0], args[1], result);
71 break;
72 default:
73 st = BR_FAILED;
74 break;
75 }
76 CTRACE("array_rewriter", st != BR_FAILED,
77 tout << mk_pp(f, m()) << "\n";
78 for (unsigned i = 0; i < num_args; ++i) {
79 tout << mk_bounded_pp(args[i], m(), 2) << "\n";
80 }
81 tout << "\n --> " << mk_bounded_pp(result, m(), 2) << "\n";);
82 return st;
83 }
84
85 // l_true -- all equal
86 // l_false -- at least one disequal
87 // l_undef -- don't know
88 template<bool CHECK_DISEQ>
compare_args(unsigned num_args,expr * const * args1,expr * const * args2)89 lbool array_rewriter::compare_args(unsigned num_args, expr * const * args1, expr * const * args2) {
90 for (unsigned i = 0; i < num_args; i++) {
91 if (args1[i] == args2[i])
92 continue;
93 if (CHECK_DISEQ && m().are_distinct(args1[i], args2[i]))
94 return l_false;
95 return l_undef;
96 }
97 return l_true;
98 }
99
mk_store_core(unsigned num_args,expr * const * args,expr_ref & result)100 br_status array_rewriter::mk_store_core(unsigned num_args, expr * const * args, expr_ref & result) {
101 SASSERT(num_args >= 3);
102
103 if (m_util.is_store(args[0])) {
104 lbool r = m_sort_store ?
105 compare_args<true>(num_args - 2, args + 1, to_app(args[0])->get_args() + 1) :
106 compare_args<false>(num_args - 2, args + 1, to_app(args[0])->get_args() + 1);
107 switch (r) {
108 case l_true: {
109 //
110 // store(store(a,i,v),i,w) --> store(a,i,w)
111 //
112 ptr_buffer<expr> new_args;
113 new_args.push_back(to_app(args[0])->get_arg(0));
114 new_args.append(num_args-1, args+1);
115 SASSERT(new_args.size() == num_args);
116 result = m().mk_app(get_fid(), OP_STORE, num_args, new_args.data());
117 return BR_DONE;
118 }
119 case l_false:
120 SASSERT(m_sort_store);
121 //
122 // store(store(a,i,v),j,w) -> store(store(a,j,w),i,v)
123 // if i, j are different, lt(i,j)
124 //
125 if (lex_lt(num_args-2, args+1, to_app(args[0])->get_args() + 1)) {
126 ptr_buffer<expr> new_args;
127 new_args.push_back(to_app(args[0])->get_arg(0));
128 new_args.append(num_args-1, args+1);
129 expr * nested_store = m().mk_app(get_fid(), OP_STORE, num_args, new_args.data());
130 new_args.reset();
131 new_args.push_back(nested_store);
132 new_args.append(num_args - 1, to_app(args[0])->get_args() + 1);
133 result = m().mk_app(get_fid(), OP_STORE, num_args, new_args.data());
134 return BR_REWRITE2;
135 }
136 break;
137 case l_undef:
138 break;
139 }
140 }
141
142 //
143 // store(const(v),i,v) --> const(v)
144 //
145 if (m_util.is_const(args[0]) &&
146 to_app(args[0])->get_arg(0) == args[num_args-1]) {
147 result = args[0];
148 return BR_DONE;
149 }
150
151 expr * v = args[num_args-1];
152
153 //
154 // store(a, i, select(a, i)) --> a
155 //
156 if (m_util.is_select(v) &&
157 compare_args<false>(num_args-1, args, to_app(v)->get_args())) {
158 result = args[0];
159 return BR_DONE;
160 }
161
162 return BR_FAILED;
163 }
164
mk_select_core(unsigned num_args,expr * const * args,expr_ref & result)165 br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args, expr_ref & result) {
166 SASSERT(num_args >= 2);
167 if (m_util.is_store(args[0])) {
168 SASSERT(to_app(args[0])->get_num_args() == num_args+1);
169 switch (compare_args<true>(num_args - 1, args+1, to_app(args[0])->get_args()+1)) {
170 case l_true:
171 // select(store(a, I, v), I) --> v
172 result = to_app(args[0])->get_arg(num_args);
173 return BR_DONE;
174 case l_false: {
175 // select(store(a, I, v), J) --> select(a, J) if I != J
176 ptr_buffer<expr> new_args;
177 new_args.push_back(to_app(args[0])->get_arg(0));
178 new_args.append(num_args-1, args+1);
179 result = m().mk_app(get_fid(), OP_SELECT, num_args, new_args.data());
180 return BR_REWRITE1;
181 }
182 default:
183 if (m_blast_select_store || (m_expand_select_store && to_app(args[0])->get_arg(0)->get_ref_count() == 1)) {
184 // select(store(a, I, v), J) --> ite(I=J, v, select(a, J))
185 ptr_buffer<expr> new_args;
186 new_args.push_back(to_app(args[0])->get_arg(0));
187 new_args.append(num_args-1, args+1);
188 expr * sel_a_j = m().mk_app(get_fid(), OP_SELECT, num_args, new_args.data());
189 expr * v = to_app(args[0])->get_arg(num_args);
190 ptr_buffer<expr> eqs;
191 unsigned num_indices = num_args-1;
192 for (unsigned i = 0; i < num_indices; i++) {
193 eqs.push_back(m().mk_eq(to_app(args[0])->get_arg(i+1), args[i+1]));
194 }
195 if (num_indices == 1) {
196 result = m().mk_ite(eqs[0], v, sel_a_j);
197 return BR_REWRITE2;
198 }
199 else {
200 result = m().mk_ite(m().mk_and(eqs), v, sel_a_j);
201 return BR_REWRITE3;
202 }
203 }
204 return BR_FAILED;
205 }
206 }
207
208 if (m_util.is_const(args[0])) {
209 // select(const(v), I) --> v
210 result = to_app(args[0])->get_arg(0);
211 return BR_DONE;
212 }
213
214 if (is_lambda(args[0])) {
215 // anywhere lambda reduction as opposed to whnf
216 // select(lambda(X) M, N) -> M[N/X]
217 quantifier* q = to_quantifier(args[0]);
218 SASSERT(q->get_num_decls() == num_args - 1);
219 var_subst subst(m());
220 expr_ref_vector _args(m());
221 var_shifter sh(m());
222 for (unsigned i = 1; i < num_args; ++i) {
223 sh(args[i], num_args-1, result);
224 _args.push_back(result);
225 }
226 result = subst(q->get_expr(), _args.size(), _args.data());
227 inv_var_shifter invsh(m());
228 invsh(result, _args.size(), result);
229 return BR_REWRITE_FULL;
230 }
231
232 if (m_util.is_map(args[0])) {
233 app* a = to_app(args[0]);
234 func_decl* f0 = m_util.get_map_func_decl(a);
235 expr_ref_vector args0(m());
236 for (expr* arg : *a) {
237 ptr_vector<expr> args1;
238 args1.push_back(arg);
239 args1.append(num_args-1, args + 1);
240 args0.push_back(m_util.mk_select(args1.size(), args1.data()));
241 }
242 result = m().mk_app(f0, args0.size(), args0.data());
243 return BR_REWRITE2;
244 }
245
246 if (m_util.is_as_array(args[0])) {
247 // select(as-array[f], I) --> f(I)
248 func_decl * f = m_util.get_as_array_func_decl(to_app(args[0]));
249 result = m().mk_app(f, num_args - 1, args + 1);
250 return BR_REWRITE1;
251 }
252
253 expr* c, *th, *el;
254 if (m().is_ite(args[0], c, th, el) && (m_expand_select_ite || (th->get_ref_count() == 1 || el->get_ref_count() == 1))) {
255 ptr_vector<expr> args1, args2;
256 args1.push_back(th);
257 args1.append(num_args-1, args + 1);
258 args2.push_back(el);
259 args2.append(num_args-1, args + 1);
260 result = m().mk_ite(c, m_util.mk_select(num_args, args1.data()), m_util.mk_select(num_args, args2.data()));
261 return BR_REWRITE2;
262 }
263
264 return BR_FAILED;
265 }
266
get_map_array_sort(func_decl * f,unsigned num_args,expr * const * args)267 sort_ref array_rewriter::get_map_array_sort(func_decl* f, unsigned num_args, expr* const* args) {
268 sort* s0 = args[0]->get_sort();
269 unsigned sz = get_array_arity(s0);
270 ptr_vector<sort> domain;
271 for (unsigned i = 0; i < sz; ++i) domain.push_back(get_array_domain(s0, i));
272 return sort_ref(m_util.mk_array_sort(sz, domain.data(), f->get_range()), m());
273 }
274
mk_map_core(func_decl * f,unsigned num_args,expr * const * args,expr_ref & result)275 br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
276
277 app* store_expr = nullptr;
278 unsigned num_indices = 0;
279 bool same_store = true;
280 for (unsigned i = 0; same_store && i < num_args; i++) {
281 expr* a = args[i];
282 if (m_util.is_const(a)) {
283 continue;
284 }
285 else if (!m_util.is_store(a)) {
286 same_store = false;
287 }
288 else if (!store_expr) {
289 num_indices = to_app(a)->get_num_args() - 2;
290 store_expr = to_app(a);
291 }
292 else {
293 for (unsigned j = 1; same_store && j < num_indices + 1; j++) {
294 same_store = (store_expr->get_arg(j) == to_app(a)->get_arg(j));
295 }
296 }
297 }
298
299 //
300 // map_f (store a_1 j v_1) ... (store a_n j v_n) --> (store (map_f a_1 ... a_n) j (f v_1 ... v_n))
301 //
302 if (same_store) {
303 ptr_buffer<expr> arrays;
304 ptr_buffer<expr> values;
305 for (unsigned i = 0; i < num_args; i++) {
306 expr* a = args[i];
307 if (m_util.is_const(a)) {
308 arrays.push_back(a);
309 values.push_back(to_app(a)->get_arg(0));
310 }
311 else {
312 arrays.push_back(to_app(a)->get_arg(0));
313 values.push_back(to_app(a)->get_arg(num_indices+1));
314 }
315 }
316 if (store_expr) {
317 ptr_buffer<expr> new_args;
318 new_args.push_back(m_util.mk_map(f, arrays.size(), arrays.data()));
319 new_args.append(num_indices, store_expr->get_args() + 1);
320 new_args.push_back(m().mk_app(f, values.size(), values.data()));
321 result = m().mk_app(get_fid(), OP_STORE, new_args.size(), new_args.data());
322 }
323 else {
324 expr_ref value(m().mk_app(f, values.size(), values.data()), m());
325 sort_ref s = get_map_array_sort(f, num_args, args);
326 result = m_util.mk_const_array(s, value);
327 }
328 TRACE("array", tout << result << "\n";);
329 return BR_REWRITE2;
330 }
331
332 //
333 // map_f (lambda x1 b1) ... (lambda x1 bn) -> lambda x1 (f b1 .. bn)
334 //
335 quantifier* lam = nullptr;
336 for (unsigned i = 0; i < num_args; ++i) {
337 if (is_lambda(args[i]))
338 lam = to_quantifier(args[i]);
339 else if (m_util.is_const(args[i]))
340 continue;
341 else {
342 lam = nullptr;
343 break;
344 }
345 }
346 if (lam) {
347 expr_ref_vector args1(m());
348 for (unsigned i = 0; i < num_args; ++i) {
349 expr* a = args[i];
350 if (m_util.is_const(a)) {
351 args1.push_back(to_app(a)->get_arg(0));
352 }
353 else if (is_lambda(a)) {
354 lam = to_quantifier(a);
355 args1.push_back(lam->get_expr());
356 }
357 }
358 result = m().mk_app(f, args1.size(), args1.data());
359 result = m().update_quantifier(lam, result);
360 return BR_REWRITE3;
361 }
362
363 if (m().is_not(f) && m_util.is_map(args[0]) && m().is_not(m_util.get_map_func_decl(args[0]))) {
364 result = to_app(args[0])->get_arg(0);
365 return BR_DONE;
366 }
367
368 if (m().is_and(f)) {
369 ast_mark mark;
370 ptr_buffer<expr> es;
371 bool change = false;
372 unsigned j = 0;
373 es.append(num_args, args);
374 for (unsigned i = 0; i < es.size(); ++i) {
375 expr* e = es[i];
376 if (mark.is_marked(e)) {
377 change = true;
378 }
379 else if (m_util.is_map(e) && m().is_and(m_util.get_map_func_decl(e))) {
380 mark.mark(e, true);
381 es.append(to_app(e)->get_num_args(), to_app(e)->get_args());
382 }
383 else {
384 mark.mark(e, true);
385 es[j++] = es[i];
386 }
387 }
388 es.shrink(j);
389 j = 0;
390 for (expr* e : es) {
391 if (m_util.is_map(e) && m().is_not(m_util.get_map_func_decl(e))) {
392 expr * arg = to_app(e)->get_arg(0);
393 if (mark.is_marked(arg)) {
394 sort_ref s = get_map_array_sort(f, num_args, args);
395 result = m_util.mk_const_array(s, m().mk_false());
396 return BR_DONE;
397 }
398 // a & (!a & b & c) -> a & !(b & c)
399 if (m_util.is_map(arg) && m().is_and(m_util.get_map_func_decl(arg))) {
400 unsigned k = 0;
401 ptr_buffer<expr> gs;
402 bool and_change = false;
403 gs.append(to_app(arg)->get_num_args(), to_app(arg)->get_args());
404 for (unsigned i = 0; i < gs.size(); ++i) {
405 expr* g = gs[i];
406 if (mark.is_marked(g)) {
407 change = true;
408 and_change = true;
409 }
410 else if (m_util.is_map(g) && m().is_and(m_util.get_map_func_decl(g))) {
411 gs.append(to_app(g)->get_num_args(), to_app(g)->get_args());
412 }
413 else {
414 gs[k++] = gs[i];
415 }
416 }
417 gs.shrink(k);
418 if (and_change) {
419 std::sort(gs.begin(), gs.end(), [](expr* a, expr* b) { return a->get_id() < b->get_id(); });
420 expr* arg = m_util.mk_map_assoc(f, gs.size(), gs.data());
421 es[j] = m_util.mk_map(m().mk_not_decl(), 1, &arg);
422 }
423 }
424 }
425 ++j;
426 }
427 if (change) {
428 std::sort(es.begin(), es.end(), [](expr* a, expr* b) { return a->get_id() < b->get_id(); });
429 result = m_util.mk_map_assoc(f, es.size(), es.data());
430 return BR_REWRITE2;
431 }
432 }
433
434 if (m().is_or(f)) {
435 ast_mark mark;
436 ptr_buffer<expr> es;
437 es.append(num_args, args);
438 unsigned j = 0;
439 bool change = false;
440 for (unsigned i = 0; i < es.size(); ++i) {
441 expr* e = es[i];
442 if (mark.is_marked(e)) {
443 change = true;
444 }
445 else if (m_util.is_map(e) && m().is_or(m_util.get_map_func_decl(e))) {
446 mark.mark(e, true);
447 es.append(to_app(e)->get_num_args(), to_app(e)->get_args());
448 }
449 else {
450 mark.mark(e, true);
451 es[j++] = es[i];
452 }
453 }
454 es.shrink(j);
455 for (expr* e : es) {
456 if (m_util.is_map(e) && m().is_not(m_util.get_map_func_decl(e)) && mark.is_marked(to_app(e)->get_arg(0))) {
457 sort_ref s = get_map_array_sort(f, num_args, args);
458 result = m_util.mk_const_array(s, m().mk_true());
459 return BR_DONE;
460 }
461 }
462 if (change) {
463 result = m_util.mk_map_assoc(f, es.size(), es.data());
464 return BR_REWRITE1;
465 }
466 }
467
468
469 return BR_FAILED;
470 }
471
mk_store(unsigned num_args,expr * const * args,expr_ref & result)472 void array_rewriter::mk_store(unsigned num_args, expr * const * args, expr_ref & result) {
473 if (mk_store_core(num_args, args, result) == BR_FAILED)
474 result = m().mk_app(get_fid(), OP_STORE, num_args, args);
475 }
476
mk_select(unsigned num_args,expr * const * args,expr_ref & result)477 void array_rewriter::mk_select(unsigned num_args, expr * const * args, expr_ref & result) {
478 if (mk_select_core(num_args, args, result) == BR_FAILED)
479 result = m().mk_app(get_fid(), OP_SELECT, num_args, args);
480 }
481
mk_map(func_decl * f,unsigned num_args,expr * const * args,expr_ref & result)482 void array_rewriter::mk_map(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
483 if (mk_map_core(f, num_args, args, result) == BR_FAILED)
484 result = m_util.mk_map(f, num_args, args);
485 }
486
mk_set_union(unsigned num_args,expr * const * args,expr_ref & result)487 br_status array_rewriter::mk_set_union(unsigned num_args, expr * const * args, expr_ref & result) {
488 SASSERT(num_args > 0);
489 if (num_args == 1) {
490 result = args[0];
491 return BR_DONE;
492 }
493 SASSERT(num_args >= 2);
494 br_status r = unsigned2br_status(num_args - 2);
495 result = m_util.mk_map(m().mk_or_decl(), num_args, args);
496 return r;
497 }
498
mk_set_intersect(unsigned num_args,expr * const * args,expr_ref & result)499 br_status array_rewriter::mk_set_intersect(unsigned num_args, expr * const * args, expr_ref & result) {
500 SASSERT(num_args > 0);
501 if (num_args == 1) {
502 result = args[0];
503 return BR_DONE;
504 }
505 SASSERT(num_args >= 2);
506 br_status r = unsigned2br_status(num_args - 2);
507 result = m_util.mk_map(m().mk_and_decl(), num_args, args);
508 return r;
509 }
510
511
mk_set_complement(expr * arg,expr_ref & result)512 br_status array_rewriter::mk_set_complement(expr * arg, expr_ref & result) {
513 func_decl* fnot = m().mk_not_decl();
514 br_status st = mk_map_core(fnot, 1, &arg, result);
515 if (BR_FAILED == st) {
516 result = m_util.mk_map(fnot, 1, &arg);
517 st = BR_DONE;
518 }
519 return st;
520 }
521
mk_set_difference(expr * arg1,expr * arg2,expr_ref & result)522 br_status array_rewriter::mk_set_difference(expr * arg1, expr * arg2, expr_ref & result) {
523 expr * args[2] = { arg1, m_util.mk_map(m().mk_not_decl(), 1, &arg2) };
524 result = m_util.mk_map(m().mk_and_decl(), 2, args);
525 return BR_REWRITE2;
526 }
527
mk_set_subset(expr * arg1,expr * arg2,expr_ref & result)528 br_status array_rewriter::mk_set_subset(expr * arg1, expr * arg2, expr_ref & result) {
529 mk_set_difference(arg1, arg2, result);
530 result = m().mk_eq(result.get(), m_util.mk_empty_set(arg1->get_sort()));
531 return BR_REWRITE3;
532 }
533
mk_eq(expr * e,expr * lhs,expr * rhs,expr_ref_vector & fmls)534 void array_rewriter::mk_eq(expr* e, expr* lhs, expr* rhs, expr_ref_vector& fmls) {
535 expr_ref tmp1(m()), tmp2(m());
536 expr_ref a(m()), v(m());
537 expr_ref_vector args0(m()), args(m());
538 while (m_util.is_store_ext(e, a, args0, v)) {
539 args.reset();
540 args.push_back(lhs);
541 args.append(args0);
542 mk_select(args.size(), args.data(), tmp1);
543 args[0] = rhs;
544 mk_select(args.size(), args.data(), tmp2);
545 fmls.push_back(m().mk_eq(tmp1, tmp2));
546 e = a;
547 }
548 }
549
has_index_set(expr * e,expr_ref & else_case,vector<expr_ref_vector> & stores)550 bool array_rewriter::has_index_set(expr* e, expr_ref& else_case, vector<expr_ref_vector>& stores) {
551 expr_ref_vector args(m());
552 expr_ref a(m()), v(m());
553 a = e;
554 while (m_util.is_store_ext(e, a, args, v)) {
555 args.push_back(v);
556 stores.push_back(args);
557 e = a;
558 }
559 if (m_util.is_const(e, e)) {
560 else_case = e;
561 return true;
562 }
563 if (is_lambda(e)) {
564 quantifier* q = to_quantifier(e);
565 e = q->get_expr();
566 unsigned num_idxs = q->get_num_decls();
567 expr* e1, *e3, *store_val;
568 if (!is_ground(e) && m().is_or(e)) {
569 for (expr* arg : *to_app(e)) {
570 if (!add_store(args, num_idxs, arg, m().mk_true(), stores)) {
571 return false;
572 }
573 }
574 else_case = m().mk_false();
575 return true;
576 }
577 if (!is_ground(e) && m().is_and(e)) {
578 for (expr* arg : *to_app(e)) {
579 if (!add_store(args, num_idxs, arg, m().mk_true(), stores)) {
580 return false;
581 }
582 }
583 else_case = m().mk_true();
584 return true;
585 }
586 while (!is_ground(e) && m().is_ite(e, e1, store_val, e3) && is_ground(store_val)) {
587 if (!add_store(args, num_idxs, e1, store_val, stores)) {
588 return false;
589 }
590 e = e3;
591 }
592 else_case = e;
593 return is_ground(e);
594 }
595 return false;
596 }
597
add_store(expr_ref_vector & args,unsigned num_idxs,expr * e,expr * store_val,vector<expr_ref_vector> & stores)598 bool array_rewriter::add_store(expr_ref_vector& args, unsigned num_idxs, expr* e, expr* store_val, vector<expr_ref_vector>& stores) {
599
600 expr* e1, *e2;
601 ptr_vector<expr> eqs;
602 args.reset();
603 args.resize(num_idxs + 1, nullptr);
604 bool is_not = m().is_bool(store_val) && m().is_not(e, e);
605
606 eqs.push_back(e);
607 for (unsigned i = 0; i < eqs.size(); ++i) {
608 e = eqs[i];
609 if (m().is_and(e)) {
610 eqs.append(to_app(e)->get_num_args(), to_app(e)->get_args());
611 continue;
612 }
613 if (m().is_eq(e, e1, e2)) {
614 if (is_var(e2)) {
615 std::swap(e1, e2);
616 }
617 if (is_var(e1) && is_ground(e2)) {
618 unsigned idx = to_var(e1)->get_idx();
619 args[num_idxs - idx - 1] = e2;
620 }
621 else {
622 return false;
623 }
624 continue;
625 }
626 return false;
627 }
628 for (unsigned i = 0; i < num_idxs; ++i) {
629 if (!args.get(i)) return false;
630 }
631 if (is_not) {
632 store_val = mk_not(m(), store_val);
633 }
634 args[num_idxs] = store_val;
635 stores.push_back(args);
636 return true;
637 }
638
is_expandable_store(expr * s)639 bool array_rewriter::is_expandable_store(expr* s) {
640 unsigned count = 0;
641 unsigned depth = 0;
642 while (m_util.is_store(s)) {
643 s = to_app(s)->get_arg(0);
644 count += s->get_ref_count();
645 depth++;
646 }
647 return (depth >= 3 && count <= depth*2);
648 }
649
expand_store(expr * s)650 expr_ref array_rewriter::expand_store(expr* s) {
651 sort* srt = s->get_sort();
652 unsigned arity = get_array_arity(srt);
653 ptr_vector<app> stores;
654 expr_ref result(m()), tmp(m());
655 var_shifter sh(m());
656 while (m_util.is_store(s)) {
657 stores.push_back(to_app(s));
658 s = to_app(s)->get_arg(0);
659 }
660 stores.reverse();
661 expr_ref_vector args(m()), eqs(m());
662 ptr_vector<sort> sorts;
663 svector<symbol> names;
664 sh(s, arity, tmp);
665 args.push_back(tmp);
666 for (unsigned i = arity; i-- > 0; ) {
667 args.push_back(m().mk_var(i, get_array_domain(srt, i)));
668 sorts.push_back(get_array_domain(srt, i));
669 names.push_back(symbol(i));
670 }
671 names.reverse();
672 sorts.reverse();
673 result = m_util.mk_select(args);
674 for (app* st : stores) {
675 eqs.reset();
676 for (unsigned i = 1; i < args.size(); ++i) {
677 sh(st->get_arg(i), arity, tmp);
678 eqs.push_back(m().mk_eq(args.get(i), tmp));
679 }
680 sh(st->get_arg(args.size()), arity, tmp);
681 result = m().mk_ite(mk_and(eqs), tmp, result);
682 }
683 result = m().mk_lambda(sorts.size(), sorts.data(), names.data(), result);
684 return result;
685 }
686
mk_eq_core(expr * lhs,expr * rhs,expr_ref & result)687 br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
688 TRACE("array_rewriter", tout << mk_bounded_pp(lhs, m(), 2) << " " << mk_bounded_pp(rhs, m(), 2) << "\n";);
689 expr* v = nullptr, *w = nullptr;
690 if (m_util.is_const(rhs) && is_lambda(lhs)) {
691 std::swap(lhs, rhs);
692 }
693 if (m_util.is_const(rhs) && m_util.is_store(lhs)) {
694 std::swap(lhs, rhs);
695 }
696 if (m_util.is_const(lhs, v) && m_util.is_const(rhs, w)) {
697 result = m().mk_eq(v, w);
698 return BR_REWRITE1;
699 }
700 if (m_util.is_const(lhs, v) && is_lambda(rhs)) {
701 quantifier* lam = to_quantifier(rhs);
702 expr_ref e(m().mk_eq(lam->get_expr(), v), m());
703 result = m().update_quantifier(lam, quantifier_kind::forall_k, e);
704 return BR_REWRITE2;
705 }
706
707 expr_ref_vector fmls(m());
708
709
710 auto has_large_domain = [&](sort* s, unsigned num_stores) {
711 unsigned sz = get_array_arity(s);
712 uint64_t dsz = 1;
713 for (unsigned i = 0; i < sz; ++i) {
714 sort* d = get_array_domain(s, i);
715 if (d->is_infinite() || d->is_very_big())
716 return true;
717 auto const& n = d->get_num_elements();
718 if (n.size() > num_stores)
719 return true;
720 dsz *= n.size();
721 if (dsz > num_stores)
722 return true;
723 }
724 return false;
725 };
726
727
728 if (m_expand_store_eq) {
729 expr* lhs1 = lhs;
730 expr* rhs1 = rhs;
731 unsigned num_lhs = 0, num_rhs = 0;
732 while (m_util.is_store(lhs1)) {
733 lhs1 = to_app(lhs1)->get_arg(0);
734 ++num_lhs;
735 }
736 while (m_util.is_store(rhs1)) {
737 rhs1 = to_app(rhs1)->get_arg(0);
738 ++num_rhs;
739 }
740 if (lhs1 == rhs1) {
741 mk_eq(lhs, lhs, rhs, fmls);
742 mk_eq(rhs, lhs, rhs, fmls);
743 result = m().mk_and(fmls);
744 return BR_REWRITE_FULL;
745 }
746
747 if (m_util.is_const(lhs1, v) && m_util.is_const(rhs1, w) &&
748 has_large_domain(lhs->get_sort(), std::max(num_lhs, num_rhs))) {
749 mk_eq(lhs, lhs, rhs, fmls);
750 mk_eq(rhs, lhs, rhs, fmls);
751 fmls.push_back(m().mk_eq(v, w));
752 result = m().mk_and(fmls);
753 return BR_REWRITE_FULL;
754 }
755 }
756
757
758 if (m_expand_nested_stores) {
759 expr_ref lh1(m()), rh1(m());
760 if (is_expandable_store(lhs)) {
761 lh1 = expand_store(lhs);
762 }
763 if (is_expandable_store(rhs)) {
764 rh1 = expand_store(rhs);
765 }
766 if (lh1 || rh1) {
767 if (!lh1) lh1 = lhs;
768 if (!rh1) rh1 = rhs;
769 result = m().mk_eq(lh1, rh1);
770 return BR_REWRITE_FULL;
771 }
772 }
773
774
775 #if 0
776 // lambda friendly version of array equality rewriting.
777 vector<expr_ref_vector> indices;
778 expr_ref lhs0(m()), rhs0(m());
779 expr_ref tmp1(m()), tmp2(m());
780 if (has_index_set(lhs, lhs0, indices) && has_index_set(rhs, rhs0, indices) && lhs0 == rhs0) {
781 expr_ref_vector args(m());
782 for (auto const& idxs : indices) {
783 args.reset();
784 args.push_back(lhs);
785 idxs.pop_back();
786 args.append(idxs);
787 mk_select(args.size(), args.c_ptr(), tmp1);
788 args[0] = rhs;
789 mk_select(args.size(), args.c_ptr(), tmp2);
790 fmls.push_back(m().mk_eq(tmp1, tmp2));
791 }
792 }
793 #endif
794
795 return BR_FAILED;
796 }
797