1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3
4 Module Name:
5
6 elim_uncnstr_vars.cpp
7
8 Abstract:
9
10 Eliminated unconstrained variables.
11
12 Author:
13
14 Leonardo (leonardo) 2011-10-22
15
16 Notes:
17
18 --*/
19 #include "tactic/tactical.h"
20 #include "tactic/generic_model_converter.h"
21 #include "ast/rewriter/rewriter_def.h"
22 #include "ast/arith_decl_plugin.h"
23 #include "ast/bv_decl_plugin.h"
24 #include "ast/recfun_decl_plugin.h"
25 #include "ast/array_decl_plugin.h"
26 #include "ast/datatype_decl_plugin.h"
27 #include "tactic/core/collect_occs.h"
28 #include "ast/ast_smt2_pp.h"
29 #include "ast/ast_ll_pp.h"
30
31 namespace {
32 class elim_uncnstr_tactic : public tactic {
33
34 // unconstrained vars collector
35
36 typedef generic_model_converter mc;
37
38 struct rw_cfg : public default_rewriter_cfg {
39 bool m_produce_proofs;
40 obj_hashtable<expr> & m_vars;
41 ref<mc> m_mc;
42 arith_util m_a_util;
43 bv_util m_bv_util;
44 array_util m_ar_util;
45 datatype_util m_dt_util;
46 app_ref_vector m_fresh_vars;
47 obj_map<app, app*> m_cache;
48 app_ref_vector m_cache_domain;
49 unsigned long long m_max_memory;
50 unsigned m_max_steps;
51
rw_cfg__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg52 rw_cfg(ast_manager & m, bool produce_proofs, obj_hashtable<expr> & vars, mc * _m,
53 unsigned long long max_memory, unsigned max_steps):
54 m_produce_proofs(produce_proofs),
55 m_vars(vars),
56 m_mc(_m),
57 m_a_util(m),
58 m_bv_util(m),
59 m_ar_util(m),
60 m_dt_util(m),
61 m_fresh_vars(m),
62 m_cache_domain(m),
63 m_max_memory(max_memory),
64 m_max_steps(max_steps) {
65 }
66
m__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg67 ast_manager & m() const { return m_a_util.get_manager(); }
68
max_steps_exceeded__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg69 bool max_steps_exceeded(unsigned num_steps) const {
70 if (memory::get_allocation_size() > m_max_memory)
71 throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
72 return num_steps > m_max_steps;
73 }
74
uncnstr__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg75 bool uncnstr(expr * arg) const {
76 return m_vars.contains(arg);
77 }
78
uncnstr__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg79 bool uncnstr(unsigned num, expr * const * args) const {
80 for (unsigned i = 0; i < num; i++)
81 if (!uncnstr(args[i]))
82 return false;
83 return true;
84 }
85
86 /**
87 \brief Create a fresh variable for abstracting (f args[0] ... args[num-1])
88 Return true if it a new variable was created, and false if the variable already existed for this
89 application. Store the variable in v
90 */
mk_fresh_uncnstr_var_for__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg91 bool mk_fresh_uncnstr_var_for(app * t, app * & v) {
92 if (m_cache.find(t, v)) {
93 return false; // variable already existed for this application
94 }
95
96 v = m().mk_fresh_const(nullptr, t->get_sort());
97 TRACE("elim_uncnstr_bug", tout << "eliminating:\n" << mk_ismt2_pp(t, m()) << "\n";);
98 TRACE("elim_uncnstr_bug_ll", tout << "eliminating:\n" << mk_bounded_pp(t, m()) << "\n";);
99 m_fresh_vars.push_back(v);
100 if (m_mc) m_mc->hide(v);
101 m_cache_domain.push_back(t);
102 m_cache.insert(t, v);
103 return true;
104 }
105
mk_fresh_uncnstr_var_for__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg106 bool mk_fresh_uncnstr_var_for(func_decl * f, unsigned num, expr * const * args, app * & v) {
107 return mk_fresh_uncnstr_var_for(m().mk_app(f, num, args), v);
108 }
109
mk_fresh_uncnstr_var_for__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg110 bool mk_fresh_uncnstr_var_for(func_decl * f, expr * arg1, expr * arg2, app * & v) {
111 return mk_fresh_uncnstr_var_for(m().mk_app(f, arg1, arg2), v);
112 }
113
mk_fresh_uncnstr_var_for__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg114 bool mk_fresh_uncnstr_var_for(func_decl * f, expr * arg, app * & v) {
115 return mk_fresh_uncnstr_var_for(m().mk_app(f, arg), v);
116 }
117
add_def__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg118 void add_def(expr * v, expr * def) {
119 SASSERT(uncnstr(v));
120 SASSERT(to_app(v)->get_num_args() == 0);
121 if (m_mc)
122 m_mc->add(to_app(v)->get_decl(), def);
123 }
124
add_defs__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg125 void add_defs(unsigned num, expr * const * args, expr * u, expr * identity) {
126 if (m_mc) {
127 add_def(args[0], u);
128 for (unsigned i = 1; i < num; i++)
129 add_def(args[i], identity);
130 }
131 }
132
133 // return a term that is different from t.
mk_diff__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg134 bool mk_diff(expr * t, expr_ref & r) {
135 sort * s = t->get_sort();
136 if (m().is_bool(s)) {
137 r = m().mk_not(t);
138 return true;
139 }
140 family_id fid = s->get_family_id();
141 if (fid == m_a_util.get_family_id()) {
142 r = m_a_util.mk_add(t, m_a_util.mk_numeral(rational(1), s));
143 return true;
144 }
145 if (fid == m_bv_util.get_family_id()) {
146 r = m().mk_app(m_bv_util.get_family_id(), OP_BNOT, t);
147 return true;
148 }
149 if (fid == m_ar_util.get_family_id()) {
150 if (m().is_uninterp(get_array_range(s)))
151 return false;
152 unsigned arity = get_array_arity(s);
153 for (unsigned i = 0; i < arity; i++)
154 if (m().is_uninterp(get_array_domain(s, i)))
155 return false;
156 // building
157 // r = (store t i1 ... in d)
158 // where i1 ... in are arbitrary values
159 // and d is a term different from (select t i1 ... in)
160 ptr_buffer<expr> new_args;
161 new_args.push_back(t);
162 for (unsigned i = 0; i < arity; i++)
163 new_args.push_back(m().get_some_value(get_array_domain(s, i)));
164 expr_ref sel(m());
165 sel = m().mk_app(fid, OP_SELECT, new_args.size(), new_args.data());
166 expr_ref diff_sel(m());
167 if (!mk_diff(sel, diff_sel))
168 return false;
169 new_args.push_back(diff_sel);
170 r = m().mk_app(fid, OP_STORE, new_args.size(), new_args.data());
171 return true;
172 }
173 if (fid == m_dt_util.get_family_id()) {
174 // In the current implementation, I only handle the case where
175 // the datatype has a recursive constructor.
176 ptr_vector<func_decl> const & constructors = *m_dt_util.get_datatype_constructors(s);
177 for (func_decl * constructor : constructors) {
178 unsigned num = constructor->get_arity();
179 unsigned target = UINT_MAX;
180 for (unsigned i = 0; i < num; i++) {
181 sort * s_arg = constructor->get_domain(i);
182 if (s == s_arg) {
183 target = i;
184 continue;
185 }
186 if (m().is_uninterp(s_arg))
187 break;
188 }
189 if (target == UINT_MAX)
190 continue;
191 // use the constructor the distinct term constructor(...,t,...)
192 ptr_buffer<expr> new_args;
193 for (unsigned i = 0; i < num; i++) {
194 if (i == target) {
195 new_args.push_back(t);
196 }
197 else {
198 new_args.push_back(m().get_some_value(constructor->get_domain(i)));
199 }
200 }
201 r = m().mk_app(constructor, new_args.size(), new_args.data());
202 return true;
203 }
204 // TODO: handle more cases.
205 return false;
206 }
207 return false;
208 }
209
process_eq__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg210 app * process_eq(func_decl * f, expr * arg1, expr * arg2) {
211 expr * v;
212 expr * t;
213 if (uncnstr(arg1)) {
214 v = arg1;
215 t = arg2;
216 }
217 else if (uncnstr(arg2)) {
218 v = arg2;
219 t = arg1;
220 }
221 else {
222 return nullptr;
223 }
224
225 sort * s = arg1->get_sort();
226
227 // Remark:
228 // I currently do not support unconstrained vars that have
229 // uninterpreted sorts, for the following reasons:
230 // - Soundness
231 // (forall ((x S) (y S)) (= x y))
232 // (not (= c1 c2))
233 //
234 // The constants c1 and c2 have only one occurrence in
235 // the formula above, but they are not really unconstrained.
236 // The quantifier forces S to have interpretations of size 1.
237 // If we replace (= c1 c2) with fresh k. The formula will
238 // become satisfiable.
239 //
240 // - Even if the formula is quantifier free, I would still
241 // have to build an interpretation for the eliminated
242 // variables.
243 //
244 if (!m().is_fully_interp(s))
245 return nullptr;
246
247 // If the interpreted sort has only one element,
248 // then it is unsound to eliminate the unconstrained variable in the equality
249 sort_size sz = s->get_num_elements();
250
251 if (sz.is_finite() && sz.size() <= 1)
252 return nullptr;
253
254 if (!m_mc) {
255 // easy case, model generation is disabled.
256 app * u;
257 mk_fresh_uncnstr_var_for(f, arg1, arg2, u);
258 return u;
259 }
260
261 expr_ref d(m());
262 if (mk_diff(t, d)) {
263 app * u;
264 if (!mk_fresh_uncnstr_var_for(f, arg1, arg2, u))
265 return u;
266 add_def(v, m().mk_ite(u, t, d));
267 return u;
268 }
269 return nullptr;
270 }
271
process_basic_app__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg272 app * process_basic_app(func_decl * f, unsigned num, expr * const * args) {
273 SASSERT(f->get_family_id() == m().get_basic_family_id());
274 switch (f->get_decl_kind()) {
275 case OP_ITE:
276 SASSERT(num == 3);
277 if (uncnstr(args[1]) && uncnstr(args[2])) {
278 app * r;
279 if (!mk_fresh_uncnstr_var_for(f, num, args, r))
280 return r;
281 add_def(args[1], r);
282 add_def(args[2], r);
283 return r;
284 }
285 if (uncnstr(args[0]) && uncnstr(args[1])) {
286 app * r;
287 if (!mk_fresh_uncnstr_var_for(f, num, args, r))
288 return r;
289 add_def(args[0], m().mk_true());
290 add_def(args[1], r);
291 return r;
292 }
293 if (uncnstr(args[0]) && uncnstr(args[2])) {
294 app * r;
295 if (!mk_fresh_uncnstr_var_for(f, num, args, r))
296 return r;
297 add_def(args[0], m().mk_false());
298 add_def(args[2], r);
299 return r;
300 }
301 return nullptr;
302 case OP_NOT:
303 SASSERT(num == 1);
304 if (uncnstr(args[0])) {
305 app * r;
306 if (!mk_fresh_uncnstr_var_for(f, num, args, r))
307 return r;
308 if (m_mc)
309 add_def(args[0], m().mk_not(r));
310 return r;
311 }
312 return nullptr;
313 case OP_AND:
314 if (num > 0 && uncnstr(num, args)) {
315 app * r;
316 if (!mk_fresh_uncnstr_var_for(f, num, args, r))
317 return r;
318 if (m_mc)
319 add_defs(num, args, r, m().mk_true());
320 return r;
321 }
322 return nullptr;
323 case OP_OR:
324 if (num > 0 && uncnstr(num, args)) {
325 app * r;
326 if (!mk_fresh_uncnstr_var_for(f, num, args, r))
327 return r;
328 if (m_mc)
329 add_defs(num, args, r, m().mk_false());
330 return r;
331 }
332 return nullptr;
333 case OP_EQ:
334 SASSERT(num == 2);
335 return process_eq(f, args[0], args[1]);
336 default:
337 return nullptr;
338 }
339 }
340
process_le_ge__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg341 app * process_le_ge(func_decl * f, expr * arg1, expr * arg2, bool le) {
342 expr * v;
343 expr * t;
344 if (uncnstr(arg1)) {
345 v = arg1;
346 t = arg2;
347 }
348 else if (uncnstr(arg2)) {
349 v = arg2;
350 t = arg1;
351 le = !le;
352 }
353 else {
354 return nullptr;
355 }
356 app * u;
357 if (!mk_fresh_uncnstr_var_for(f, arg1, arg2, u))
358 return u;
359 if (!m_mc)
360 return u;
361 // v = ite(u, t, t + 1) if le
362 // v = ite(u, t, t - 1) if !le
363 add_def(v, m().mk_ite(u, t, m_a_util.mk_add(t, m_a_util.mk_numeral(rational(le ? 1 : -1), arg1->get_sort()))));
364 return u;
365 }
366
process_add__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg367 app * process_add(family_id fid, decl_kind add_k, decl_kind sub_k, unsigned num, expr * const * args) {
368 if (num == 0)
369 return nullptr;
370 unsigned i;
371 expr * v = nullptr;
372 for (i = 0; i < num; i++) {
373 expr * arg = args[i];
374 if (uncnstr(arg)) {
375 v = arg;
376 break;
377 }
378 }
379 if (v == nullptr)
380 return nullptr;
381 app * u;
382 if (!mk_fresh_uncnstr_var_for(m().mk_app(fid, add_k, num, args), u))
383 return u;
384 if (!m_mc)
385 return u;
386 ptr_buffer<expr> new_args;
387 for (unsigned j = 0; j < num; j++) {
388 if (j == i)
389 continue;
390 new_args.push_back(args[j]);
391 }
392 if (new_args.empty()) {
393 add_def(v, u);
394 }
395 else {
396 expr * rest;
397 if (new_args.size() == 1)
398 rest = new_args[0];
399 else
400 rest = m().mk_app(fid, add_k, new_args.size(), new_args.data());
401 add_def(v, m().mk_app(fid, sub_k, u, rest));
402 }
403 return u;
404 }
405
process_arith_mul__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg406 app * process_arith_mul(func_decl * f, unsigned num, expr * const * args) {
407 if (num == 0)
408 return nullptr;
409 sort * s = args[0]->get_sort();
410 if (uncnstr(num, args)) {
411 app * r;
412 if (!mk_fresh_uncnstr_var_for(f, num, args, r))
413 return r;
414 if (m_mc)
415 add_defs(num, args, r, m_a_util.mk_numeral(rational(1), s));
416 return r;
417 }
418 // c * v case for reals
419 bool is_int;
420 rational val;
421 if (num == 2 && uncnstr(args[1]) && m_a_util.is_numeral(args[0], val, is_int) && !is_int) {
422 if (val.is_zero())
423 return nullptr;
424 app * r;
425 if (!mk_fresh_uncnstr_var_for(f, num, args, r))
426 return r;
427 if (m_mc) {
428 val = rational(1) / val;
429 add_def(args[1], m_a_util.mk_mul(m_a_util.mk_numeral(val, false), r));
430 }
431 return r;
432 }
433 return nullptr;
434 }
435
process_arith_app__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg436 app * process_arith_app(func_decl * f, unsigned num, expr * const * args) {
437
438 SASSERT(f->get_family_id() == m_a_util.get_family_id());
439 switch (f->get_decl_kind()) {
440 case OP_ADD:
441 return process_add(f->get_family_id(), OP_ADD, OP_SUB, num, args);
442 case OP_MUL:
443 return process_arith_mul(f, num, args);
444 case OP_LE:
445 SASSERT(num == 2);
446 return process_le_ge(f, args[0], args[1], true);
447 case OP_GE:
448 SASSERT(num == 2);
449 return process_le_ge(f, args[0], args[1], false);
450 default:
451 return nullptr;
452 }
453 }
454
process_bv_mul__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg455 app * process_bv_mul(func_decl * f, unsigned num, expr * const * args) {
456 if (num == 0)
457 return nullptr;
458 if (uncnstr(num, args)) {
459 sort * s = args[0]->get_sort();
460 app * r;
461 if (!mk_fresh_uncnstr_var_for(f, num, args, r))
462 return r;
463 if (m_mc)
464 add_defs(num, args, r, m_bv_util.mk_numeral(rational(1), s));
465 return r;
466 }
467 // c * v (c is even) case
468 unsigned bv_size;
469 rational val;
470 rational inv;
471 if (num == 2 &&
472 uncnstr(args[1]) &&
473 m_bv_util.is_numeral(args[0], val, bv_size) &&
474 val.mult_inverse(bv_size, inv)) {
475 app * r;
476 if (!mk_fresh_uncnstr_var_for(f, num, args, r))
477 return r;
478 sort * s = args[1]->get_sort();
479 if (m_mc)
480 add_def(args[1], m_bv_util.mk_bv_mul(m_bv_util.mk_numeral(inv, s), r));
481 return r;
482 }
483 return nullptr;
484 }
485
process_extract__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg486 app * process_extract(func_decl * f, expr * arg) {
487 if (!uncnstr(arg))
488 return nullptr;
489 app * r;
490 if (!mk_fresh_uncnstr_var_for(f, arg, r))
491 return r;
492 if (!m_mc)
493 return r;
494 unsigned high = m_bv_util.get_extract_high(f);
495 unsigned low = m_bv_util.get_extract_low(f);
496 unsigned bv_size = m_bv_util.get_bv_size(arg->get_sort());
497 if (bv_size == high - low + 1) {
498 add_def(arg, r);
499 }
500 else {
501 ptr_buffer<expr> args;
502 if (high < bv_size - 1)
503 args.push_back(m_bv_util.mk_numeral(rational(0), bv_size - high - 1));
504 args.push_back(r);
505 if (low > 0)
506 args.push_back(m_bv_util.mk_numeral(rational(0), low));
507 add_def(arg, m_bv_util.mk_concat(args.size(), args.data()));
508 }
509 return r;
510 }
511
process_bv_div__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg512 app * process_bv_div(func_decl * f, expr * arg1, expr * arg2) {
513 if (uncnstr(arg1) && uncnstr(arg2)) {
514 sort * s = arg1->get_sort();
515 app * r;
516 if (!mk_fresh_uncnstr_var_for(f, arg1, arg2, r))
517 return r;
518 if (!m_mc)
519 return r;
520 add_def(arg1, r);
521 add_def(arg2, m_bv_util.mk_numeral(rational(1), s));
522 return r;
523 }
524 return nullptr;
525 }
526
process_concat__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg527 app * process_concat(func_decl * f, unsigned num, expr * const * args) {
528 if (num == 0)
529 return nullptr;
530 if (!uncnstr(num, args))
531 return nullptr;
532 app * r;
533 if (!mk_fresh_uncnstr_var_for(f, num, args, r))
534 return r;
535 if (m_mc) {
536 unsigned i = num;
537 unsigned low = 0;
538 while (i > 0) {
539 --i;
540 expr * arg = args[i];
541 unsigned sz = m_bv_util.get_bv_size(arg);
542 add_def(arg, m_bv_util.mk_extract(low + sz - 1, low, r));
543 low += sz;
544 }
545 }
546 return r;
547 }
548
process_bv_le__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg549 app * process_bv_le(func_decl * f, expr * arg1, expr * arg2, bool is_signed) {
550 if (m_produce_proofs) {
551 // The result of bv_le is not just introducing a new fresh name,
552 // we need a side condition.
553 // TODO: the correct proof step
554 return nullptr;
555 }
556 if (uncnstr(arg1)) {
557 // v <= t
558 expr * v = arg1;
559 expr * t = arg2;
560 // v <= t ---> (u or t == MAX) u is fresh
561 // add definition v = ite(u or t == MAX, t, t+1)
562 unsigned bv_sz = m_bv_util.get_bv_size(arg1);
563 rational MAX;
564 if (is_signed)
565 MAX = rational::power_of_two(bv_sz - 1) - rational(1);
566 else
567 MAX = rational::power_of_two(bv_sz) - rational(1);
568 app * u;
569 bool is_new = mk_fresh_uncnstr_var_for(f, arg1, arg2, u);
570 app * r = m().mk_or(u, m().mk_eq(t, m_bv_util.mk_numeral(MAX, bv_sz)));
571 if (m_mc && is_new)
572 add_def(v, m().mk_ite(r, t, m_bv_util.mk_bv_add(t, m_bv_util.mk_numeral(rational(1), bv_sz))));
573 return r;
574 }
575 if (uncnstr(arg2)) {
576 // v >= t
577 expr * v = arg2;
578 expr * t = arg1;
579 // v >= t ---> (u ot t == MIN) u is fresh
580 // add definition v = ite(u or t == MIN, t, t-1)
581 unsigned bv_sz = m_bv_util.get_bv_size(arg1);
582 rational MIN;
583 if (is_signed)
584 MIN = -rational::power_of_two(bv_sz - 1);
585 else
586 MIN = rational(0);
587 app * u;
588 bool is_new = mk_fresh_uncnstr_var_for(f, arg1, arg2, u);
589 app * r = m().mk_or(u, m().mk_eq(t, m_bv_util.mk_numeral(MIN, bv_sz)));
590 if (m_mc && is_new)
591 add_def(v, m().mk_ite(r, t, m_bv_util.mk_bv_sub(t, m_bv_util.mk_numeral(rational(1), bv_sz))));
592 return r;
593 }
594 return nullptr;
595 }
596
process_bv_app__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg597 app * process_bv_app(func_decl * f, unsigned num, expr * const * args) {
598 SASSERT(f->get_family_id() == m_bv_util.get_family_id());
599 switch (f->get_decl_kind()) {
600 case OP_BADD:
601 return process_add(f->get_family_id(), OP_BADD, OP_BSUB, num, args);
602 case OP_BMUL:
603 return process_bv_mul(f, num, args);
604 case OP_BSDIV:
605 case OP_BUDIV:
606 case OP_BSDIV_I:
607 case OP_BUDIV_I:
608 SASSERT(num == 2);
609 return process_bv_div(f, args[0], args[1]);
610 case OP_SLEQ:
611 SASSERT(num == 2);
612 return process_bv_le(f, args[0], args[1], true);
613 case OP_ULEQ:
614 SASSERT(num == 2);
615 return process_bv_le(f, args[0], args[1], false);
616 case OP_CONCAT:
617 return process_concat(f, num, args);
618 case OP_EXTRACT:
619 SASSERT(num == 1);
620 return process_extract(f, args[0]);
621 case OP_BNOT:
622 SASSERT(num == 1);
623 if (uncnstr(args[0])) {
624 app * r;
625 if (!mk_fresh_uncnstr_var_for(f, num, args, r))
626 return r;
627 if (m_mc)
628 add_def(args[0], m().mk_app(f, r));
629 return r;
630 }
631 return nullptr;
632 case OP_BOR:
633 if (num > 0 && uncnstr(num, args)) {
634 sort * s = args[0]->get_sort();
635 app * r;
636 if (!mk_fresh_uncnstr_var_for(f, num, args, r))
637 return r;
638 if (m_mc)
639 add_defs(num, args, r, m_bv_util.mk_numeral(rational(0), s));
640 return r;
641 }
642 return nullptr;
643 default:
644 return nullptr;
645 }
646 }
647
process_array_app__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg648 app * process_array_app(func_decl * f, unsigned num, expr * const * args) {
649 SASSERT(f->get_family_id() == m_ar_util.get_family_id());
650 switch (f->get_decl_kind()) {
651 case OP_SELECT:
652 if (uncnstr(args[0])) {
653 app * r;
654 if (!mk_fresh_uncnstr_var_for(f, num, args, r))
655 return r;
656 sort * s = args[0]->get_sort();
657 if (m_mc)
658 add_def(args[0], m_ar_util.mk_const_array(s, r));
659 return r;
660 }
661 return nullptr;
662 case OP_STORE:
663 if (uncnstr(args[0]) && uncnstr(args[num-1])) {
664 app * r;
665 if (!mk_fresh_uncnstr_var_for(f, num, args, r))
666 return r;
667 if (m_mc) {
668 add_def(args[num-1], m().mk_app(m_ar_util.get_family_id(), OP_SELECT, num-1, args));
669 add_def(args[0], r);
670 }
671 return r;
672 }
673 default:
674 return nullptr;
675 }
676 }
677
process_datatype_app__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg678 app * process_datatype_app(func_decl * f, unsigned num, expr * const * args) {
679 if (m_dt_util.is_accessor(f)) {
680 SASSERT(num == 1);
681 if (uncnstr(args[0])) {
682 if (!m_mc) {
683 app * r;
684 mk_fresh_uncnstr_var_for(f, num, args, r);
685 return r;
686 }
687 func_decl * c = m_dt_util.get_accessor_constructor(f);
688 for (unsigned i = 0; i < c->get_arity(); i++)
689 if (!m().is_fully_interp(c->get_domain(i)))
690 return nullptr;
691 app * u;
692 if (!mk_fresh_uncnstr_var_for(f, num, args, u))
693 return u;
694 ptr_vector<func_decl> const & accs = *m_dt_util.get_constructor_accessors(c);
695 ptr_buffer<expr> new_args;
696 for (unsigned i = 0; i < accs.size(); i++) {
697 if (accs[i] == f)
698 new_args.push_back(u);
699 else
700 new_args.push_back(m().get_some_value(c->get_domain(i)));
701 }
702 add_def(args[0], m().mk_app(c, new_args.size(), new_args.data()));
703 return u;
704 }
705 }
706 return nullptr;
707 }
708
reduce_app__anon2f1f399f0111::elim_uncnstr_tactic::rw_cfg709 br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
710 if (num == 0)
711 return BR_FAILED;
712 family_id fid = f->get_family_id();
713 if (fid == null_family_id)
714 return BR_FAILED;
715
716 for (unsigned i = 0; i < num; i++) {
717 if (!is_ground(args[i]))
718 return BR_FAILED; // non-ground terms are not handled.
719 }
720
721 app * u = nullptr;
722
723 if (fid == m().get_basic_family_id())
724 u = process_basic_app(f, num, args);
725 else if (fid == m_a_util.get_family_id())
726 u = process_arith_app(f, num, args);
727 else if (fid == m_bv_util.get_family_id())
728 u = process_bv_app(f, num, args);
729 else if (fid == m_ar_util.get_family_id())
730 u = process_array_app(f, num, args);
731 else if (fid == m_dt_util.get_family_id())
732 u = process_datatype_app(f, num, args);
733
734 if (u == nullptr)
735 return BR_FAILED;
736
737 result = u;
738 if (m_produce_proofs) {
739 expr * s = m().mk_app(f, num, args);
740 expr * eq = m().mk_eq(s, u);
741 proof * pr1 = m().mk_def_intro(eq);
742 result_pr = m().mk_apply_def(s, u, pr1);
743 }
744
745 return BR_DONE;
746 }
747 };
748
749 class rw : public rewriter_tpl<rw_cfg> {
750 rw_cfg m_cfg;
751 public:
rw(ast_manager & m,bool produce_proofs,obj_hashtable<expr> & vars,mc * _m,unsigned long long max_memory,unsigned max_steps)752 rw(ast_manager & m, bool produce_proofs, obj_hashtable<expr> & vars, mc * _m,
753 unsigned long long max_memory, unsigned max_steps):
754 rewriter_tpl<rw_cfg>(m, produce_proofs, m_cfg),
755 m_cfg(m, produce_proofs, vars, _m, max_memory, max_steps) {
756 }
757 };
758
759 ast_manager & m_manager;
760 ref<mc> m_mc;
761 obj_hashtable<expr> m_vars;
762 scoped_ptr<rw> m_rw;
763 unsigned m_num_elim_apps = 0;
764 unsigned long long m_max_memory;
765 unsigned m_max_steps;
766
m()767 ast_manager & m() { return m_manager; }
768
init_mc(bool produce_models)769 void init_mc(bool produce_models) {
770 m_mc = nullptr;
771 if (produce_models) {
772 m_mc = alloc(mc, m(), "elim_uncstr");
773 }
774 }
775
init_rw(bool produce_proofs)776 void init_rw(bool produce_proofs) {
777 m_rw = alloc(rw, m(), produce_proofs, m_vars, m_mc.get(), m_max_memory, m_max_steps);
778 }
779
run(goal_ref const & g,goal_ref_buffer & result)780 void run(goal_ref const & g, goal_ref_buffer & result) {
781 bool produce_proofs = g->proofs_enabled();
782
783 TRACE("goal", g->display(tout););
784 tactic_report report("elim-uncnstr", *g);
785 m_vars.reset();
786 collect_occs p;
787 p(*g, m_vars);
788 if (m_vars.empty() || recfun::util(m()).has_defs()) {
789 result.push_back(g.get());
790 // did not increase depth since it didn't do anything.
791 return;
792 }
793 bool modified = true;
794 TRACE("elim_uncnstr", tout << "unconstrained variables...\n";
795 for (expr * v : m_vars) tout << mk_ismt2_pp(v, m()) << " ";
796 tout << "\n";);
797 init_mc(g->models_enabled());
798 init_rw(produce_proofs);
799
800 expr_ref new_f(m());
801 proof_ref new_pr(m());
802 unsigned round = 0;
803 unsigned size = g->size();
804 unsigned idx = 0;
805 while (true) {
806 for (; idx < size; idx++) {
807 expr * f = g->form(idx);
808 m_rw->operator()(f, new_f, new_pr);
809 if (f == new_f)
810 continue;
811 modified = true;
812 if (produce_proofs) {
813 proof * pr = g->pr(idx);
814 new_pr = m().mk_modus_ponens(pr, new_pr);
815 }
816 g->update(idx, new_f, new_pr, g->dep(idx));
817 }
818 if (!modified) {
819 if (round == 0) {
820 }
821 else {
822 m_num_elim_apps = m_rw->cfg().m_fresh_vars.size();
823 g->add(m_mc.get());
824 }
825 TRACE("elim_uncnstr", if (m_mc) m_mc->display(tout); else tout << "no mc\n";);
826 m_mc = nullptr;
827 m_rw = nullptr;
828 result.push_back(g.get());
829 g->inc_depth();
830 TRACE("goal", g->display(tout););
831 return;
832 }
833 modified = false;
834 round ++;
835 size = g->size();
836 m_rw->reset(); // reset cache
837 m_vars.reset();
838 {
839 collect_occs p;
840 p(*g, m_vars);
841 }
842 if (m_vars.empty())
843 idx = size; // force to finish
844 else
845 idx = 0;
846 }
847 }
848
849 params_ref m_params;
850 public:
elim_uncnstr_tactic(ast_manager & m,params_ref const & p)851 elim_uncnstr_tactic(ast_manager & m, params_ref const & p):
852 m_manager(m), m_params(p) {
853 updt_params(p);
854 }
855
translate(ast_manager & m)856 tactic * translate(ast_manager & m) override {
857 return alloc(elim_uncnstr_tactic, m, m_params);
858 }
859
updt_params(params_ref const & p)860 void updt_params(params_ref const & p) override {
861 m_params = p;
862 m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
863 m_max_steps = p.get_uint("max_steps", UINT_MAX);
864 }
865
collect_param_descrs(param_descrs & r)866 void collect_param_descrs(param_descrs & r) override {
867 insert_max_memory(r);
868 insert_max_steps(r);
869 }
870
operator ()(goal_ref const & g,goal_ref_buffer & result)871 void operator()(goal_ref const & g,
872 goal_ref_buffer & result) override {
873 run(g, result);
874 report_tactic_progress(":num-elim-apps", m_num_elim_apps);
875 }
876
cleanup()877 void cleanup() override {
878 m_mc = nullptr;
879 m_rw = nullptr;
880 m_vars.reset();
881 }
882
collect_statistics(statistics & st) const883 void collect_statistics(statistics & st) const override {
884 st.update("eliminated applications", m_num_elim_apps);
885 }
886
reset_statistics()887 void reset_statistics() override {
888 m_num_elim_apps = 0;
889 }
890
891 };
892 }
893
mk_elim_uncnstr_tactic(ast_manager & m,params_ref const & p)894 tactic * mk_elim_uncnstr_tactic(ast_manager & m, params_ref const & p) {
895 return clean(alloc(elim_uncnstr_tactic, m, p));
896 }
897