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