1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3
4 Module Name:
5
6 th_rewriter.h
7
8 Abstract:
9
10 Rewriter for applying all builtin (cheap) theory rewrite rules.
11
12 Author:
13
14 Leonardo (leonardo) 2011-04-07
15
16 Notes:
17
18 --*/
19 #include "params/rewriter_params.hpp"
20 #include "ast/rewriter/th_rewriter.h"
21 #include "ast/rewriter/bool_rewriter.h"
22 #include "ast/rewriter/arith_rewriter.h"
23 #include "ast/rewriter/bv_rewriter.h"
24 #include "ast/rewriter/datatype_rewriter.h"
25 #include "ast/rewriter/array_rewriter.h"
26 #include "ast/rewriter/fpa_rewriter.h"
27 #include "ast/rewriter/dl_rewriter.h"
28 #include "ast/rewriter/pb_rewriter.h"
29 #include "ast/rewriter/recfun_rewriter.h"
30 #include "ast/rewriter/seq_rewriter.h"
31 #include "ast/rewriter/rewriter_def.h"
32 #include "ast/rewriter/var_subst.h"
33 #include "ast/rewriter/expr_safe_replace.h"
34 #include "ast/expr_substitution.h"
35 #include "ast/ast_smt2_pp.h"
36 #include "ast/ast_pp.h"
37 #include "ast/ast_util.h"
38 #include "ast/well_sorted.h"
39
40 namespace {
41 struct th_rewriter_cfg : public default_rewriter_cfg {
42 bool_rewriter m_b_rw;
43 arith_rewriter m_a_rw;
44 bv_rewriter m_bv_rw;
45 array_rewriter m_ar_rw;
46 datatype_rewriter m_dt_rw;
47 fpa_rewriter m_f_rw;
48 dl_rewriter m_dl_rw;
49 pb_rewriter m_pb_rw;
50 seq_rewriter m_seq_rw;
51 recfun_rewriter m_rec_rw;
52 arith_util m_a_util;
53 bv_util m_bv_util;
54 expr_safe_replace m_rep;
55 expr_ref_vector m_pinned;
56 // substitution support
57 expr_dependency_ref m_used_dependencies; // set of dependencies of used substitutions
58 expr_substitution * m_subst = nullptr;
59 unsigned long long m_max_memory; // in bytes
60 bool m_new_subst = false;
61 unsigned m_max_steps = UINT_MAX;
62 bool m_pull_cheap_ite = true;
63 bool m_flat = true;
64 bool m_cache_all = false;
65 bool m_push_ite_arith = true;
66 bool m_push_ite_bv = true;
67 bool m_ignore_patterns_on_ground_qbody = true;
68 bool m_rewrite_patterns = true;
69
70
m__anon2045c6df0111::th_rewriter_cfg71 ast_manager & m() const { return m_b_rw.m(); }
72
updt_local_params__anon2045c6df0111::th_rewriter_cfg73 void updt_local_params(params_ref const & _p) {
74 rewriter_params p(_p);
75 m_flat = p.flat();
76 m_max_memory = megabytes_to_bytes(p.max_memory());
77 m_max_steps = p.max_steps();
78 m_pull_cheap_ite = p.pull_cheap_ite();
79 m_cache_all = p.cache_all();
80 m_push_ite_arith = p.push_ite_arith();
81 m_push_ite_bv = p.push_ite_bv();
82 m_ignore_patterns_on_ground_qbody = p.ignore_patterns_on_ground_qbody();
83 m_rewrite_patterns = p.rewrite_patterns();
84 }
85
updt_params__anon2045c6df0111::th_rewriter_cfg86 void updt_params(params_ref const & p) {
87 m_b_rw.updt_params(p);
88 m_a_rw.updt_params(p);
89 m_bv_rw.updt_params(p);
90 m_ar_rw.updt_params(p);
91 m_f_rw.updt_params(p);
92 m_seq_rw.updt_params(p);
93 updt_local_params(p);
94 }
95
flat_assoc__anon2045c6df0111::th_rewriter_cfg96 bool flat_assoc(func_decl * f) const {
97 if (!m_flat) return false;
98 family_id fid = f->get_family_id();
99 if (fid == null_family_id)
100 return false;
101 decl_kind k = f->get_decl_kind();
102 if (fid == m_b_rw.get_fid())
103 return k == OP_AND || k == OP_OR;
104 if (fid == m_a_rw.get_fid())
105 return k == OP_ADD;
106 if (fid == m_bv_rw.get_fid())
107 return k == OP_BADD || k == OP_BOR || k == OP_BAND || k == OP_BXOR;
108 return false;
109 }
110
rewrite_patterns__anon2045c6df0111::th_rewriter_cfg111 bool rewrite_patterns() const { return m_rewrite_patterns; }
112
cache_all_results__anon2045c6df0111::th_rewriter_cfg113 bool cache_all_results() const { return m_cache_all; }
114
max_steps_exceeded__anon2045c6df0111::th_rewriter_cfg115 bool max_steps_exceeded(unsigned num_steps) const {
116 if (m_max_memory != SIZE_MAX &&
117 memory::get_allocation_size() > m_max_memory)
118 throw rewriter_exception(Z3_MAX_MEMORY_MSG);
119 return num_steps > m_max_steps;
120 }
121
122 // Return true if t is of the form
123 // (= t #b0)
124 // (= t #b1)
125 // (= #b0 t)
126 // (= #b1 t)
is_eq_bit__anon2045c6df0111::th_rewriter_cfg127 bool is_eq_bit(expr * t, expr * & x, unsigned & val) {
128 if (!m().is_eq(t))
129 return false;
130 expr * lhs = to_app(t)->get_arg(0);
131 if (!m_bv_rw.is_bv(lhs))
132 return false;
133 if (m_bv_rw.get_bv_size(lhs) != 1)
134 return false;
135 expr * rhs = to_app(t)->get_arg(1);
136 rational v;
137 unsigned sz;
138 if (m_bv_rw.is_numeral(lhs, v, sz)) {
139 x = rhs;
140 val = v.get_unsigned();
141 SASSERT(val == 0 || val == 1);
142 return true;
143 }
144 if (m_bv_rw.is_numeral(rhs, v, sz)) {
145 x = lhs;
146 val = v.get_unsigned();
147 SASSERT(val == 0 || val == 1);
148 return true;
149 }
150 return false;
151 }
152
153 // (iff (= x bit1) A)
154 // --->
155 // (= x (ite A bit1 bit0))
apply_tamagotchi__anon2045c6df0111::th_rewriter_cfg156 br_status apply_tamagotchi(expr * lhs, expr * rhs, expr_ref & result) {
157 expr * x;
158 unsigned val;
159 if (is_eq_bit(lhs, x, val)) {
160 result = m().mk_eq(x, m().mk_ite(rhs, m_bv_rw.mk_numeral(val, 1), m_bv_rw.mk_numeral(1-val, 1)));
161 return BR_REWRITE2;
162 }
163 if (is_eq_bit(rhs, x, val)) {
164 result = m().mk_eq(x, m().mk_ite(lhs, m_bv_rw.mk_numeral(val, 1), m_bv_rw.mk_numeral(1-val, 1)));
165 return BR_REWRITE2;
166 }
167 return BR_FAILED;
168 }
169
reduce_app_core__anon2045c6df0111::th_rewriter_cfg170 br_status reduce_app_core(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
171 family_id fid = f->get_family_id();
172 if (fid == null_family_id)
173 return BR_FAILED;
174 br_status st = BR_FAILED;
175 if (fid == m_b_rw.get_fid()) {
176 decl_kind k = f->get_decl_kind();
177 if (k == OP_EQ) {
178 // theory dispatch for =
179 SASSERT(num == 2);
180 family_id s_fid = args[0]->get_sort()->get_family_id();
181 if (s_fid == m_a_rw.get_fid())
182 st = m_a_rw.mk_eq_core(args[0], args[1], result);
183 else if (s_fid == m_bv_rw.get_fid())
184 st = m_bv_rw.mk_eq_core(args[0], args[1], result);
185 else if (s_fid == m_dt_rw.get_fid())
186 st = m_dt_rw.mk_eq_core(args[0], args[1], result);
187 else if (s_fid == m_f_rw.get_fid())
188 st = m_f_rw.mk_eq_core(args[0], args[1], result);
189 else if (s_fid == m_ar_rw.get_fid())
190 st = m_ar_rw.mk_eq_core(args[0], args[1], result);
191 else if (s_fid == m_seq_rw.get_fid())
192 st = m_seq_rw.mk_eq_core(args[0], args[1], result);
193 if (st != BR_FAILED)
194 return st;
195 }
196 if (k == OP_EQ) {
197 SASSERT(num == 2);
198 st = apply_tamagotchi(args[0], args[1], result);
199 if (st != BR_FAILED)
200 return st;
201 }
202 if (k == OP_ITE) {
203 SASSERT(num == 3);
204 family_id s_fid = args[1]->get_sort()->get_family_id();
205 if (s_fid == m_bv_rw.get_fid())
206 st = m_bv_rw.mk_ite_core(args[0], args[1], args[2], result);
207 if (st != BR_FAILED)
208 return st;
209 }
210 if ((k == OP_AND || k == OP_OR) && m_seq_rw.u().has_re()) {
211 st = m_seq_rw.mk_bool_app(f, num, args, result);
212 if (st != BR_FAILED)
213 return st;
214 }
215 if (k == OP_EQ && m_seq_rw.u().has_seq() && is_app(args[0]) &&
216 to_app(args[0])->get_family_id() == m_seq_rw.get_fid()) {
217 st = m_seq_rw.mk_eq_core(args[0], args[1], result);
218 if (st != BR_FAILED)
219 return st;
220 }
221
222 return m_b_rw.mk_app_core(f, num, args, result);
223 }
224 if (fid == m_a_rw.get_fid() && OP_LE == f->get_decl_kind() && m_seq_rw.u().has_seq()) {
225 st = m_seq_rw.mk_le_core(args[0], args[1], result);
226 if (st != BR_FAILED)
227 return st;
228 }
229 if (fid == m_a_rw.get_fid() && OP_GE == f->get_decl_kind() && m_seq_rw.u().has_seq()) {
230 st = m_seq_rw.mk_le_core(args[1], args[0], result);
231 if (st != BR_FAILED)
232 return st;
233 }
234 if (fid == m_a_rw.get_fid())
235 return m_a_rw.mk_app_core(f, num, args, result);
236 if (fid == m_bv_rw.get_fid())
237 return m_bv_rw.mk_app_core(f, num, args, result);
238 if (fid == m_ar_rw.get_fid())
239 return m_ar_rw.mk_app_core(f, num, args, result);
240 if (fid == m_dt_rw.get_fid())
241 return m_dt_rw.mk_app_core(f, num, args, result);
242 if (fid == m_f_rw.get_fid())
243 return m_f_rw.mk_app_core(f, num, args, result);
244 if (fid == m_dl_rw.get_fid())
245 return m_dl_rw.mk_app_core(f, num, args, result);
246 if (fid == m_pb_rw.get_fid())
247 return m_pb_rw.mk_app_core(f, num, args, result);
248 if (fid == m_seq_rw.get_fid())
249 return m_seq_rw.mk_app_core(f, num, args, result);
250 if (fid == m_rec_rw.get_fid())
251 return m_rec_rw.mk_app_core(f, num, args, result);
252 return BR_FAILED;
253 }
254
255 // auxiliary function for pull_ite_core
mk_eq_value__anon2045c6df0111::th_rewriter_cfg256 expr * mk_eq_value(expr * lhs, expr * value) {
257 if (m().are_equal(lhs, value)) {
258 return m().mk_true();
259 }
260 else if (m().are_distinct(lhs, value)) {
261 return m().mk_false();
262 }
263 return m().mk_eq(lhs, value);
264 }
265
266 template<bool SWAP>
pull_ite_core__anon2045c6df0111::th_rewriter_cfg267 br_status pull_ite_core(func_decl * p, app * ite, app * value, expr_ref & result) {
268 if (m().is_eq(p)) {
269 result = m().mk_ite(ite->get_arg(0),
270 mk_eq_value(ite->get_arg(1), value),
271 mk_eq_value(ite->get_arg(2), value));
272 return BR_REWRITE2;
273 }
274 else {
275 if (SWAP) {
276 result = m().mk_ite(ite->get_arg(0),
277 m().mk_app(p, value, ite->get_arg(1)),
278 m().mk_app(p, value, ite->get_arg(2)));
279 return BR_REWRITE2;
280 }
281 else {
282 result = m().mk_ite(ite->get_arg(0),
283 m().mk_app(p, ite->get_arg(1), value),
284 m().mk_app(p, ite->get_arg(2), value));
285 return BR_REWRITE2;
286 }
287 }
288 }
289
290 // Return true if t is an ite-value-tree form defined as:
291 // ite-value-tree := (ite c <subtree> <subtree>)
292 // subtree := value
293 // | (ite c <subtree> <subtree>)
294 //
is_ite_value_tree__anon2045c6df0111::th_rewriter_cfg295 bool is_ite_value_tree(expr * t) {
296 if (!m().is_ite(t))
297 return false;
298 ptr_buffer<app> todo;
299 todo.push_back(to_app(t));
300 while (!todo.empty()) {
301 app * ite = todo.back();
302 todo.pop_back();
303 expr * arg1 = ite->get_arg(1);
304 expr * arg2 = ite->get_arg(2);
305
306 if (m().is_ite(arg1) && arg1->get_ref_count() == 1) // do not apply on shared terms, since it may blowup
307 todo.push_back(to_app(arg1));
308 else if (!m().is_value(arg1))
309 return false;
310
311 if (m().is_ite(arg2) && arg2->get_ref_count() == 1) // do not apply on shared terms, since it may blowup
312 todo.push_back(to_app(arg2));
313 else if (!m().is_value(arg2))
314 return false;
315 }
316 return true;
317 }
318
pull_ite__anon2045c6df0111::th_rewriter_cfg319 br_status pull_ite(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
320 if (num == 2 && m().is_bool(f->get_range()) && !m().is_bool(args[0])) {
321 if (m().is_ite(args[0])) {
322 if (m().is_value(args[1]))
323 return pull_ite_core<false>(f, to_app(args[0]), to_app(args[1]), result);
324 if (m().is_ite(args[1]) && to_app(args[0])->get_arg(0) == to_app(args[1])->get_arg(0)) {
325 // (p (ite C A1 B1) (ite C A2 B2)) --> (ite (p A1 A2) (p B1 B2))
326 result = m().mk_ite(to_app(args[0])->get_arg(0),
327 m().mk_app(f, to_app(args[0])->get_arg(1), to_app(args[1])->get_arg(1)),
328 m().mk_app(f, to_app(args[0])->get_arg(2), to_app(args[1])->get_arg(2)));
329 return BR_REWRITE2;
330 }
331 }
332 if (m().is_ite(args[1]) && m().is_value(args[0]))
333 return pull_ite_core<true>(f, to_app(args[1]), to_app(args[0]), result);
334 }
335 family_id fid = f->get_family_id();
336 if (num == 2 && (fid == m().get_basic_family_id() || fid == m_a_rw.get_fid() || fid == m_bv_rw.get_fid())) {
337 // (f v3 (ite c v1 v2)) --> (ite v (f v3 v1) (f v3 v2))
338 if (m().is_value(args[0]) && is_ite_value_tree(args[1]))
339 return pull_ite_core<true>(f, to_app(args[1]), to_app(args[0]), result);
340
341 // (f (ite c v1 v2) v3) --> (ite v (f v1 v3) (f v2 v3))
342 if (m().is_value(args[1]) && is_ite_value_tree(args[0]))
343 return pull_ite_core<false>(f, to_app(args[0]), to_app(args[1]), result);
344 }
345 return BR_FAILED;
346 }
347
pull_ite__anon2045c6df0111::th_rewriter_cfg348 br_status pull_ite(expr_ref & result) {
349 expr * t = result.get();
350 if (is_app(t)) {
351 br_status st = pull_ite(to_app(t)->get_decl(), to_app(t)->get_num_args(), to_app(t)->get_args(), result);
352 if (st != BR_FAILED)
353 return st;
354 }
355 return BR_DONE;
356 }
357
is_arith_bv_app__anon2045c6df0111::th_rewriter_cfg358 bool is_arith_bv_app(expr * t) const {
359 if (!is_app(t))
360 return false;
361 family_id fid = to_app(t)->get_family_id();
362 return ((fid == m_a_rw.get_fid() && m_push_ite_arith) ||
363 (fid == m_bv_rw.get_fid() && m_push_ite_bv));
364 }
365
get_neutral_elem__anon2045c6df0111::th_rewriter_cfg366 bool get_neutral_elem(app * t, expr_ref & n) {
367 family_id fid = t->get_family_id();
368 if (fid == m_a_rw.get_fid()) {
369 switch (t->get_decl_kind()) {
370 case OP_ADD: n = m_a_util.mk_numeral(rational::zero(), t->get_sort()); return true;
371 case OP_MUL: n = m_a_util.mk_numeral(rational::one(), t->get_sort()); return true;
372 default:
373 return false;
374 }
375 }
376 if (fid == m_bv_rw.get_fid()) {
377 switch (t->get_decl_kind()) {
378 case OP_BADD: n = m_bv_util.mk_numeral(rational::zero(), t->get_sort()); return true;
379 case OP_BMUL: n = m_bv_util.mk_numeral(rational::one(), t->get_sort()); return true;
380 default:
381 return false;
382 }
383 }
384 return false;
385 }
386
387 /**
388 \brief Try to "unify" t1 and t2
389 Examples
390 (+ 2 a) (+ 3 a) --> 2, 3, a
391 (+ 2 a) a --> 2, 0, a
392 ...
393 */
unify_core__anon2045c6df0111::th_rewriter_cfg394 bool unify_core(app * t1, expr * t2, expr_ref & new_t1, expr_ref & new_t2, expr_ref & c, bool & first) {
395 if (t1->get_num_args() != 2)
396 return false;
397 expr * a1 = t1->get_arg(0);
398 expr * b1 = t1->get_arg(1);
399 if (t2 == b1) {
400 if (get_neutral_elem(t1, new_t2)) {
401 new_t1 = a1;
402 c = b1;
403 first = false;
404 return true;
405 }
406 }
407 else if (t2 == a1) {
408 if (get_neutral_elem(t1, new_t2)) {
409 new_t1 = b1;
410 c = a1;
411 first = true;
412 return true;
413 }
414 }
415 else if (is_app_of(t2, t1->get_decl()) && to_app(t2)->get_num_args() == 2) {
416 expr * a2 = to_app(t2)->get_arg(0);
417 expr * b2 = to_app(t2)->get_arg(1);
418 if (b1 == b2) {
419 new_t1 = a1;
420 new_t2 = a2;
421 c = b2;
422 first = false;
423 return true;
424 }
425 if (a1 == a2) {
426 new_t1 = b1;
427 new_t2 = b2;
428 c = a1;
429 first = true;
430 return true;
431 }
432 if (t1->get_decl()->is_commutative()) {
433 if (a1 == b2) {
434 new_t1 = b1;
435 new_t2 = a2;
436 c = a1;
437 first = true; // doesn't really matter for commutative ops.
438 return true;
439 }
440 if (b1 == a2) {
441 new_t1 = a1;
442 new_t2 = b2;
443 c = b1;
444 first = false; // doesn't really matter for commutative ops.
445 return true;
446 }
447 }
448 }
449 return false;
450 }
451
452 // Return true if t1 and t2 are of the form:
453 // t + a1*x1 + ... + an*xn
454 // t' + a1*x1 + ... + an*xn
455 // Store t in new_t1, t' in new_t2 and (a1*x1 + ... + an*xn) in c.
unify_add__anon2045c6df0111::th_rewriter_cfg456 bool unify_add(app * t1, expr * t2, expr_ref & new_t1, expr_ref & new_t2, expr_ref & c) {
457 unsigned num1 = t1->get_num_args();
458 expr * const * ms1 = t1->get_args();
459 if (num1 < 2)
460 return false;
461 unsigned num2;
462 expr * const * ms2;
463 if (m_a_util.is_add(t2)) {
464 num2 = to_app(t2)->get_num_args();
465 ms2 = to_app(t2)->get_args();
466 }
467 else {
468 num2 = 1;
469 ms2 = &t2;
470 }
471 if (num1 != num2 && num1 != num2 + 1 && num1 != num2 - 1)
472 return false;
473 new_t1 = nullptr;
474 new_t2 = nullptr;
475 expr_fast_mark1 visited1;
476 expr_fast_mark2 visited2;
477 for (unsigned i = 0; i < num1; i++) {
478 expr * arg = ms1[i];
479 visited1.mark(arg);
480 }
481 for (unsigned i = 0; i < num2; i++) {
482 expr * arg = ms2[i];
483 visited2.mark(arg);
484 if (visited1.is_marked(arg))
485 continue;
486 if (new_t2)
487 return false; // more than one missing term
488 new_t2 = arg;
489 }
490 for (unsigned i = 0; i < num1; i++) {
491 expr * arg = ms1[i];
492 if (visited2.is_marked(arg))
493 continue;
494 if (new_t1)
495 return false; // more than one missing term
496 new_t1 = arg;
497 }
498 // terms matched...
499 bool is_int = m_a_util.is_int(t1);
500 if (!new_t1)
501 new_t1 = m_a_util.mk_numeral(rational::zero(), is_int);
502 if (!new_t2)
503 new_t2 = m_a_util.mk_numeral(rational::zero(), is_int);
504 // mk common part
505 ptr_buffer<expr> args;
506 for (unsigned i = 0; i < num1; i++) {
507 expr * arg = ms1[i];
508 if (arg == new_t1.get())
509 continue;
510 args.push_back(arg);
511 }
512 SASSERT(!args.empty());
513 if (args.size() == 1)
514 c = args[0];
515 else
516 c = m_a_util.mk_add(args.size(), args.data());
517 return true;
518 }
519
unify__anon2045c6df0111::th_rewriter_cfg520 bool unify(expr * t1, expr * t2, func_decl * & f, expr_ref & new_t1, expr_ref & new_t2, expr_ref & c, bool & first) {
521 #if 0
522 // Did not work for ring benchmarks
523
524 // Hack for handling more complex cases of + apps
525 // such as (+ 2 t1 t2 t3) and (+ 3 t3 t2 t1)
526 if (m_a_util.is_add(t1)) {
527 first = true; // doesn't matter for AC ops
528 f = to_app(t1)->get_decl();
529 if (unify_add(to_app(t1), t2, new_t1, new_t2, c))
530 return true;
531 }
532 if (m_a_util.is_add(t2)) {
533 first = true; // doesn't matter for AC ops
534 f = to_app(t2)->get_decl();
535 if (unify_add(to_app(t2), t1, new_t2, new_t1, c))
536 return true;
537 }
538 #endif
539
540 if (is_arith_bv_app(t1)) {
541 f = to_app(t1)->get_decl();
542 return unify_core(to_app(t1), t2, new_t1, new_t2, c, first);
543 }
544 else if (is_arith_bv_app(t2)) {
545 f = to_app(t2)->get_decl();
546 return unify_core(to_app(t2), t1, new_t2, new_t1, c, first);
547 }
548 else {
549 return false;
550 }
551 }
552
553 // Apply transformations of the form
554 //
555 // (ite c (+ k1 a) (+ k2 a)) --> (+ (ite c k1 k2) a)
556 // (ite c (* k1 a) (* k2 a)) --> (* (ite c k1 k2) a)
557 //
558 // These transformations are useful for bit-vector problems, since
559 // they will minimize the number of adders/multipliers/etc
push_ite__anon2045c6df0111::th_rewriter_cfg560 br_status push_ite(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
561 if (!m().is_ite(f))
562 return BR_FAILED;
563 expr * c = args[0];
564 expr * t = args[1];
565 expr * e = args[2];
566 func_decl * f_prime = nullptr;
567 expr_ref new_t(m()), new_e(m()), common(m());
568 bool first;
569 TRACE("push_ite", tout << "unifying:\n" << mk_ismt2_pp(t, m()) << "\n" << mk_ismt2_pp(e, m()) << "\n";);
570 if (unify(t, e, f_prime, new_t, new_e, common, first)) {
571 if (first)
572 result = m().mk_app(f_prime, common, m().mk_ite(c, new_t, new_e));
573 else
574 result = m().mk_app(f_prime, m().mk_ite(c, new_t, new_e), common);
575 return BR_DONE;
576 }
577 TRACE("push_ite", tout << "failed\n";);
578 return BR_FAILED;
579 }
580
push_ite__anon2045c6df0111::th_rewriter_cfg581 br_status push_ite(expr_ref & result) {
582 expr * t = result.get();
583 if (m().is_ite(t)) {
584 br_status st = push_ite(to_app(t)->get_decl(), to_app(t)->get_num_args(), to_app(t)->get_args(), result);
585 if (st != BR_FAILED)
586 return st;
587 }
588 return BR_DONE;
589 }
590
count_down_subterm_references__anon2045c6df0111::th_rewriter_cfg591 void count_down_subterm_references(expr * e, map<expr *, unsigned, ptr_hash<expr>, ptr_eq<expr>> & reference_map) {
592 if (is_app(e)) {
593 app * a = to_app(e);
594 for (unsigned i = 0; i < a->get_num_args(); ++i) {
595 expr * child = a->get_arg(i);
596 unsigned countdown = reference_map.get(child, child->get_ref_count()) - 1;
597 reference_map.insert(child, countdown);
598 if (countdown == 0)
599 count_down_subterm_references(child, reference_map);
600 }
601 }
602 }
603
log_rewrite_axiom_instantiation__anon2045c6df0111::th_rewriter_cfg604 void log_rewrite_axiom_instantiation(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
605 family_id fid = f->get_family_id();
606 if (fid == m_b_rw.get_fid()) {
607 decl_kind k = f->get_decl_kind();
608 if (k == OP_EQ) {
609 SASSERT(num == 2);
610 fid = args[0]->get_sort()->get_family_id();
611 }
612 else if (k == OP_ITE) {
613 SASSERT(num == 3);
614 fid = args[1]->get_sort()->get_family_id();
615 }
616 }
617 app_ref tmp(m());
618 tmp = m().mk_app(f, num, args);
619 m().trace_stream() << "[inst-discovered] theory-solving " << static_cast<void *>(nullptr) << " " << m().get_family_name(fid) << "# ; #" << tmp->get_id() << "\n";
620 tmp = m().mk_eq(tmp, result);
621 m().trace_stream() << "[instance] " << static_cast<void *>(nullptr) << " #" << tmp->get_id() << "\n";
622
623 // Make sure that both the result term and equality were newly introduced.
624 if (tmp->get_ref_count() == 1) {
625 if (result->get_ref_count() == 1) {
626 map<expr *, unsigned, ptr_hash<expr>, ptr_eq<expr>> reference_map;
627 count_down_subterm_references(result, reference_map);
628
629 // Any term that was newly introduced by the rewrite step is only referenced within / reachable from the result term.
630 for (auto kv : reference_map) {
631 if (kv.m_value == 0) {
632 m().trace_stream() << "[attach-enode] #" << kv.m_key->get_id() << " 0\n";
633 }
634 }
635
636 m().trace_stream() << "[attach-enode] #" << result->get_id() << " 0\n";
637 }
638 m().trace_stream() << "[attach-enode] #" << tmp->get_id() << " 0\n";
639 }
640 m().trace_stream() << "[end-of-instance]\n";
641 m().trace_stream().flush();
642 }
643
reduce_app__anon2045c6df0111::th_rewriter_cfg644 br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
645 result_pr = nullptr;
646 br_status st = reduce_app_core(f, num, args, result);
647
648 if (st != BR_FAILED && m().has_trace_stream()) {
649 log_rewrite_axiom_instantiation(f, num, args, result);
650 }
651
652 if (st != BR_DONE && st != BR_FAILED) {
653 CTRACE("th_rewriter_step", st != BR_FAILED,
654 tout << f->get_name() << "\n";
655 for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n";
656 tout << "---------->\n" << mk_ismt2_pp(result, m()) << "\n";);
657 return st;
658 }
659 if (m_push_ite_bv || m_push_ite_arith) {
660 if (st == BR_FAILED)
661 st = push_ite(f, num, args, result);
662 else
663 st = push_ite(result);
664 }
665 if (m_pull_cheap_ite) {
666 if (st == BR_FAILED)
667 st = pull_ite(f, num, args, result);
668 else
669 st = pull_ite(result);
670 }
671 CTRACE("th_rewriter_step", st != BR_FAILED,
672 tout << f->get_name() << "\n";
673 for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n";
674 tout << "---------->\n" << mk_ismt2_pp(result, m()) << "\n";);
675 return st;
676 }
677
mk_app__anon2045c6df0111::th_rewriter_cfg678 expr_ref mk_app(func_decl* f, unsigned num_args, expr* const* args) {
679 expr_ref result(m());
680 proof_ref pr(m());
681 if (BR_FAILED == reduce_app(f, num_args, args, result, pr)) {
682 result = m().mk_app(f, num_args, args);
683 }
684 return result;
685 }
686
apply_subst__anon2045c6df0111::th_rewriter_cfg687 void apply_subst(ptr_buffer<expr>& patterns) {
688 if (!m_subst)
689 return;
690 if (patterns.empty())
691 return;
692 if (m_new_subst) {
693 m_rep.reset();
694 for (auto kv : m_subst->sub())
695 m_rep.insert(kv.m_key, kv.m_value);
696 m_new_subst = false;
697 }
698 expr_ref tmp(m());
699 for (unsigned i = 0; i < patterns.size(); ++i) {
700 m_rep(patterns[i], tmp);
701 m_pinned.push_back(tmp);
702 patterns[i] = tmp;
703 }
704 }
705
706
reduce_quantifier__anon2045c6df0111::th_rewriter_cfg707 bool reduce_quantifier(quantifier * old_q,
708 expr * new_body,
709 expr * const * new_patterns,
710 expr * const * new_no_patterns,
711 expr_ref & result,
712 proof_ref & result_pr) {
713 quantifier_ref q1(m());
714 proof_ref p1(m());
715 if (is_quantifier(new_body) &&
716 to_quantifier(new_body)->get_kind() == old_q->get_kind() &&
717 to_quantifier(new_body)->get_kind() != lambda_k &&
718 !old_q->has_patterns() &&
719 !to_quantifier(new_body)->has_patterns()) {
720
721 quantifier * nested_q = to_quantifier(new_body);
722
723 ptr_buffer<sort> sorts;
724 buffer<symbol> names;
725 sorts.append(old_q->get_num_decls(), old_q->get_decl_sorts());
726 names.append(old_q->get_num_decls(), old_q->get_decl_names());
727 sorts.append(nested_q->get_num_decls(), nested_q->get_decl_sorts());
728 names.append(nested_q->get_num_decls(), nested_q->get_decl_names());
729
730 q1 = m().mk_quantifier(old_q->get_kind(),
731 sorts.size(),
732 sorts.data(),
733 names.data(),
734 nested_q->get_expr(),
735 std::min(old_q->get_weight(), nested_q->get_weight()),
736 old_q->get_qid(),
737 old_q->get_skid(),
738 0, nullptr, 0, nullptr);
739
740 SASSERT(is_well_sorted(m(), q1));
741
742 if (m().proofs_enabled()) {
743 p1 = m().mk_pull_quant(old_q, q1);
744 }
745 }
746 else if (old_q->get_kind() == lambda_k &&
747 is_ground(new_body)) {
748 result = m_ar_rw.util().mk_const_array(old_q->get_sort(), new_body);
749 if (m().proofs_enabled()) {
750 result_pr = m().mk_rewrite(old_q, result);
751 }
752 return true;
753 }
754 else {
755 ptr_buffer<expr> new_patterns_buf;
756 ptr_buffer<expr> new_no_patterns_buf;
757
758 new_patterns_buf.append(old_q->get_num_patterns(), new_patterns);
759 new_no_patterns_buf.append(old_q->get_num_no_patterns(), new_no_patterns);
760
761 remove_duplicates(new_patterns_buf);
762 remove_duplicates(new_no_patterns_buf);
763
764 apply_subst(new_patterns_buf);
765
766 q1 = m().update_quantifier(old_q,
767 new_patterns_buf.size(), new_patterns_buf.data(), new_no_patterns_buf.size(), new_no_patterns_buf.data(),
768 new_body);
769 m_pinned.reset();
770 TRACE("reduce_quantifier", tout << mk_ismt2_pp(old_q, m()) << "\n----->\n" << mk_ismt2_pp(q1, m()) << "\n";);
771 SASSERT(is_well_sorted(m(), q1));
772 if (m().proofs_enabled() && q1 != old_q) {
773 p1 = m().mk_rewrite(old_q, q1);
774 }
775 }
776 SASSERT(old_q->get_sort() == q1->get_sort());
777 result = elim_unused_vars(m(), q1, params_ref());
778
779
780 TRACE("reduce_quantifier", tout << "after elim_unused_vars:\n" << result << "\n";);
781
782 result_pr = nullptr;
783 if (m().proofs_enabled()) {
784 proof_ref p2(m());
785 if (q1.get() != result.get() && q1->get_kind() != lambda_k)
786 p2 = m().mk_elim_unused_vars(q1, result);
787 result_pr = m().mk_transitivity(p1, p2);
788 }
789 SASSERT(old_q->get_sort() == result->get_sort());
790 return true;
791 }
792
th_rewriter_cfg__anon2045c6df0111::th_rewriter_cfg793 th_rewriter_cfg(ast_manager & m, params_ref const & p):
794 m_b_rw(m, p),
795 m_a_rw(m, p),
796 m_bv_rw(m, p),
797 m_ar_rw(m, p),
798 m_dt_rw(m),
799 m_f_rw(m, p),
800 m_dl_rw(m),
801 m_pb_rw(m),
802 m_seq_rw(m),
803 m_rec_rw(m),
804 m_a_util(m),
805 m_bv_util(m),
806 m_rep(m),
807 m_pinned(m),
808 m_used_dependencies(m) {
809 updt_local_params(p);
810 }
811
set_substitution__anon2045c6df0111::th_rewriter_cfg812 void set_substitution(expr_substitution * s) {
813 reset();
814 m_subst = s;
815 m_new_subst = true;
816 }
817
reset__anon2045c6df0111::th_rewriter_cfg818 void reset() {
819 m_subst = nullptr;
820 }
821
get_subst__anon2045c6df0111::th_rewriter_cfg822 bool get_subst(expr * s, expr * & t, proof * & pr) {
823 if (m_subst == nullptr)
824 return false;
825 expr_dependency * d = nullptr;
826 if (m_subst->find(s, t, pr, d)) {
827 m_used_dependencies = m().mk_join(m_used_dependencies, d);
828 return true;
829 }
830 return false;
831 }
832
833
834 };
835 }
836
837 struct th_rewriter::imp : public rewriter_tpl<th_rewriter_cfg> {
838 th_rewriter_cfg m_cfg;
impth_rewriter::imp839 imp(ast_manager & m, params_ref const & p):
840 rewriter_tpl<th_rewriter_cfg>(m, m.proofs_enabled(), m_cfg),
841 m_cfg(m, p) {
842 }
mk_appth_rewriter::imp843 expr_ref mk_app(func_decl* f, unsigned sz, expr* const* args) {
844 return m_cfg.mk_app(f, sz, args);
845 }
846
set_solverth_rewriter::imp847 void set_solver(expr_solver* solver) {
848 m_cfg.m_seq_rw.set_solver(solver);
849 }
850 };
851
th_rewriter(ast_manager & m,params_ref const & p)852 th_rewriter::th_rewriter(ast_manager & m, params_ref const & p):
853 m_params(p) {
854 m_imp = alloc(imp, m, p);
855 }
856
m() const857 ast_manager & th_rewriter::m() const {
858 return m_imp->m();
859 }
860
updt_params(params_ref const & p)861 void th_rewriter::updt_params(params_ref const & p) {
862 m_params = p;
863 m_imp->cfg().updt_params(p);
864 }
865
get_param_descrs(param_descrs & r)866 void th_rewriter::get_param_descrs(param_descrs & r) {
867 bool_rewriter::get_param_descrs(r);
868 arith_rewriter::get_param_descrs(r);
869 bv_rewriter::get_param_descrs(r);
870 array_rewriter::get_param_descrs(r);
871 rewriter_params::collect_param_descrs(r);
872 }
873
~th_rewriter()874 th_rewriter::~th_rewriter() {
875 dealloc(m_imp);
876 }
877
get_cache_size() const878 unsigned th_rewriter::get_cache_size() const {
879 return m_imp->get_cache_size();
880 }
881
get_num_steps() const882 unsigned th_rewriter::get_num_steps() const {
883 return m_imp->get_num_steps();
884 }
885
886
cleanup()887 void th_rewriter::cleanup() {
888 ast_manager & m = m_imp->m();
889 m_imp->~imp();
890 new (m_imp) imp(m, m_params);
891 }
892
reset()893 void th_rewriter::reset() {
894 m_imp->reset();
895 m_imp->cfg().reset();
896 }
897
operator ()(expr_ref & term)898 void th_rewriter::operator()(expr_ref & term) {
899 expr_ref result(term.get_manager());
900 m_imp->operator()(term, result);
901 term = std::move(result);
902 }
903
operator ()(expr * t,expr_ref & result)904 void th_rewriter::operator()(expr * t, expr_ref & result) {
905 m_imp->operator()(t, result);
906 }
907
operator ()(expr * t,expr_ref & result,proof_ref & result_pr)908 void th_rewriter::operator()(expr * t, expr_ref & result, proof_ref & result_pr) {
909 m_imp->operator()(t, result, result_pr);
910 }
911
operator ()(expr * n,unsigned num_bindings,expr * const * bindings)912 expr_ref th_rewriter::operator()(expr * n, unsigned num_bindings, expr * const * bindings) {
913 return m_imp->operator()(n, num_bindings, bindings);
914 }
915
set_substitution(expr_substitution * s)916 void th_rewriter::set_substitution(expr_substitution * s) {
917 m_imp->reset(); // reset the cache
918 m_imp->cfg().set_substitution(s);
919 }
920
get_used_dependencies()921 expr_dependency * th_rewriter::get_used_dependencies() {
922 return m_imp->cfg().m_used_dependencies;
923 }
924
reset_used_dependencies()925 void th_rewriter::reset_used_dependencies() {
926 if (get_used_dependencies() != nullptr) {
927 set_substitution(m_imp->cfg().m_subst); // reset cache preserving subst
928 m_imp->cfg().m_used_dependencies = nullptr;
929 }
930 }
931
mk_app(func_decl * f,unsigned num_args,expr * const * args)932 expr_ref th_rewriter::mk_app(func_decl* f, unsigned num_args, expr* const* args) {
933 return m_imp->mk_app(f, num_args, args);
934 }
935
set_solver(expr_solver * solver)936 void th_rewriter::set_solver(expr_solver* solver) {
937 m_imp->set_solver(solver);
938 }
939
940
reduce_quantifier(quantifier * old_q,expr * new_body,expr * const * new_patterns,expr * const * new_no_patterns,expr_ref & result,proof_ref & result_pr)941 bool th_rewriter::reduce_quantifier(quantifier * old_q,
942 expr * new_body,
943 expr * const * new_patterns,
944 expr * const * new_no_patterns,
945 expr_ref & result,
946 proof_ref & result_pr) {
947 return m_imp->cfg().reduce_quantifier(old_q, new_body, new_patterns, new_no_patterns, result, result_pr);
948 }
949