1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3
4 Module Name:
5
6 model_evaluator.cpp
7
8 Abstract:
9
10 Evaluate expressions in a given model.
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2011-04-30.
15
16 Revision History:
17
18 --*/
19 #include "ast/ast_pp.h"
20 #include "ast/ast_util.h"
21 #include "ast/for_each_expr.h"
22 #include "ast/recfun_decl_plugin.h"
23 #include "ast/rewriter/rewriter_types.h"
24 #include "ast/rewriter/bool_rewriter.h"
25 #include "ast/rewriter/arith_rewriter.h"
26 #include "ast/rewriter/bv_rewriter.h"
27 #include "ast/rewriter/pb_rewriter.h"
28 #include "ast/rewriter/seq_rewriter.h"
29 #include "ast/rewriter/datatype_rewriter.h"
30 #include "ast/rewriter/array_rewriter.h"
31 #include "ast/rewriter/fpa_rewriter.h"
32 #include "ast/rewriter/th_rewriter.h"
33 #include "ast/rewriter/rewriter_def.h"
34 #include "ast/rewriter/var_subst.h"
35 #include "model/model_smt2_pp.h"
36 #include "model/model.h"
37 #include "model/model_evaluator_params.hpp"
38 #include "model/model_evaluator.h"
39 #include "model/model_v2_pp.h"
40
41
42 namespace mev {
43
44 struct evaluator_cfg : public default_rewriter_cfg {
45 ast_manager & m;
46 model_core & m_model;
47 params_ref m_params;
48 bool_rewriter m_b_rw;
49 arith_rewriter m_a_rw;
50 bv_rewriter m_bv_rw;
51 array_rewriter m_ar_rw;
52 datatype_rewriter m_dt_rw;
53 pb_rewriter m_pb_rw;
54 fpa_rewriter m_f_rw;
55 seq_rewriter m_seq_rw;
56 array_util m_ar;
57 arith_util m_au;
58 fpa_util m_fpau;
59 datatype::util m_dt;
60 unsigned long long m_max_memory;
61 unsigned m_max_steps;
62 bool m_model_completion;
63 bool m_array_equalities;
64 bool m_array_as_stores;
65 obj_map<func_decl, expr*> m_def_cache;
66 expr_ref_vector m_pinned;
67
evaluator_cfgmev::evaluator_cfg68 evaluator_cfg(ast_manager & m, model_core & md, params_ref const & p):
69 m(m),
70 m_model(md),
71 m_params(p),
72 m_b_rw(m),
73 // We must allow customers to set parameters for arithmetic rewriter/evaluator.
74 // In particular, the maximum degree of algebraic numbers that will be evaluated.
75 m_a_rw(m, p),
76 m_bv_rw(m),
77 // See comment above. We want to allow customers to set :sort-store
78 m_ar_rw(m, p),
79 m_dt_rw(m),
80 m_pb_rw(m),
81 m_f_rw(m),
82 m_seq_rw(m),
83 m_ar(m),
84 m_au(m),
85 m_fpau(m),
86 m_dt(m),
87 m_pinned(m) {
88 bool flat = true;
89 m_b_rw.set_flat(flat);
90 m_a_rw.set_flat(flat);
91 m_bv_rw.set_flat(flat);
92 m_bv_rw.set_mkbv2num(true);
93 m_ar_rw.set_expand_select_store(true);
94 m_ar_rw.set_expand_select_ite(true);
95 updt_params(p);
96 //add_unspecified_function_models(md);
97 }
98
updt_paramsmev::evaluator_cfg99 void updt_params(params_ref const & _p) {
100 model_evaluator_params p(_p);
101 m_max_memory = megabytes_to_bytes(p.max_memory());
102 m_max_steps = p.max_steps();
103 m_model_completion = p.completion();
104 m_array_equalities = p.array_equalities();
105 m_array_as_stores = p.array_as_stores();
106 }
107
evaluatemev::evaluator_cfg108 bool evaluate(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
109 func_interp * fi = m_model.get_func_interp(f);
110 bool r = (fi != nullptr) && eval_fi(fi, num, args, result);
111 CTRACE("model_evaluator", r, tout << "reduce_app " << f->get_name() << "\n";
112 for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m) << "\n";
113 tout << "---->\n" << mk_ismt2_pp(result, m) << "\n";);
114 return r;
115 }
116
117 // Try to use the entries to quickly evaluate the fi
eval_fimev::evaluator_cfg118 bool eval_fi(func_interp * fi, unsigned num, expr * const * args, expr_ref & result) {
119 if (fi->num_entries() == 0)
120 return false; // let get_macro handle it.
121
122 SASSERT(fi->get_arity() == num);
123
124 bool actuals_are_values = true;
125
126 for (unsigned i = 0; actuals_are_values && i < num; i++)
127 actuals_are_values = m.is_value(args[i]);
128
129 if (!actuals_are_values)
130 return false; // let get_macro handle it
131
132 func_entry * entry = fi->get_entry(args);
133 if (entry != nullptr) {
134 result = entry->get_result();
135 return true;
136 }
137
138 return false;
139 }
140
reduce_quantifiermev::evaluator_cfg141 bool reduce_quantifier(quantifier * old_q,
142 expr * new_body,
143 expr * const * new_patterns,
144 expr * const * new_no_patterns,
145 expr_ref & result,
146 proof_ref & result_pr) {
147 th_rewriter th(m);
148 return th.reduce_quantifier(old_q, new_body, new_patterns, new_no_patterns, result, result_pr);
149 }
150
reduce_appmev::evaluator_cfg151 br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
152 auto st = reduce_app_core(f, num, args, result, result_pr);
153 CTRACE("model_evaluator", st != BR_FAILED,
154 tout << st << " " << mk_pp(f, m) << " ";
155 for (unsigned i = 0; i < num; ++i) tout << mk_pp(args[i], m) << " ";
156 tout << "\n--> " << result << "\n";);
157
158 return st;
159 }
160
reduce_app_coremev::evaluator_cfg161 br_status reduce_app_core(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
162 result_pr = nullptr;
163 family_id fid = f->get_family_id();
164 bool _is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f);
165 br_status st = BR_FAILED;
166 #if 0
167 struct pp {
168 func_decl* f;
169 expr_ref& r;
170 pp(func_decl* f, expr_ref& r) :f(f), r(r) {}
171 ~pp() { TRACE("model_evaluator", tout << mk_pp(f, r.m()) << " " << r << "\n";); }
172 };
173 pp _pp(f, result);
174 #endif
175
176
177 if (num == 0 && (fid == null_family_id || _is_uninterp || m_ar.is_as_array(f))) {
178 expr * val = m_model.get_const_interp(f);
179 if (val != nullptr) {
180 result = val;
181 st = m_ar.is_as_array(val) ? BR_REWRITE1 : BR_DONE;
182 TRACE("model_evaluator", tout << result << "\n";);
183 return st;
184 }
185 if (!m_model_completion)
186 return BR_FAILED;
187
188 if (!m_ar.is_as_array(f)) {
189 sort * s = f->get_range();
190 expr * val = m_model.get_some_value(s);
191 m_model.register_decl(f, val);
192 result = val;
193 return BR_DONE;
194 }
195 // fall through
196 }
197
198
199 if (fid == m_b_rw.get_fid()) {
200 decl_kind k = f->get_decl_kind();
201 if (k == OP_EQ) {
202 // theory dispatch for =
203 SASSERT(num == 2);
204 sort* s = args[0]->get_sort();
205 family_id s_fid = s->get_family_id();
206 if (s_fid == m_a_rw.get_fid())
207 st = m_a_rw.mk_eq_core(args[0], args[1], result);
208 else if (s_fid == m_bv_rw.get_fid())
209 st = m_bv_rw.mk_eq_core(args[0], args[1], result);
210 else if (s_fid == m_dt_rw.get_fid())
211 st = m_dt_rw.mk_eq_core(args[0], args[1], result);
212 else if (s_fid == m_f_rw.get_fid())
213 st = m_f_rw.mk_eq_core(args[0], args[1], result);
214 else if (s_fid == m_seq_rw.get_fid())
215 st = m_seq_rw.mk_eq_core(args[0], args[1], result);
216 else if (s_fid == m_ar_rw.get_fid())
217 st = mk_array_eq(args[0], args[1], result);
218 else if (m.are_equal(args[0], args[1])) {
219 result = m.mk_true();
220 st = BR_DONE;
221 }
222 else if (m.are_distinct(args[0], args[1])) {
223 result = m.mk_false();
224 st = BR_DONE;
225 }
226 if (st != BR_FAILED)
227 return st;
228 }
229 return m_b_rw.mk_app_core(f, num, args, result);
230 }
231 if (fid == m_a_rw.get_fid())
232 st = m_a_rw.mk_app_core(f, num, args, result);
233 else if (fid == m_bv_rw.get_fid())
234 st = m_bv_rw.mk_app_core(f, num, args, result);
235 else if (fid == m_ar_rw.get_fid())
236 st = m_ar_rw.mk_app_core(f, num, args, result);
237 else if (fid == m_dt_rw.get_fid())
238 st = m_dt_rw.mk_app_core(f, num, args, result);
239 else if (fid == m_pb_rw.get_fid())
240 st = m_pb_rw.mk_app_core(f, num, args, result);
241 else if (fid == m_f_rw.get_fid())
242 st = m_f_rw.mk_app_core(f, num, args, result);
243 else if (fid == m_seq_rw.get_fid())
244 st = m_seq_rw.mk_app_core(f, num, args, result);
245 else if (fid == m.get_label_family_id() && num == 1) {
246 result = args[0];
247 st = BR_DONE;
248 }
249 else if (evaluate(f, num, args, result))
250 st = BR_REWRITE1;
251 if (st == BR_FAILED && !m.is_builtin_family_id(fid))
252 st = evaluate_partial_theory_func(f, num, args, result, result_pr);
253 if (st == BR_DONE && is_app(result)) {
254 app* a = to_app(result);
255 if (evaluate(a->get_decl(), a->get_num_args(), a->get_args(), result))
256 st = BR_REWRITE1;
257 }
258
259 if (st == BR_DONE && is_app(result) && expand_as_array(to_app(result)->get_decl(), result))
260 return BR_REWRITE_FULL;
261
262 if (st == BR_FAILED && expand_as_array(f, result))
263 return BR_REWRITE_FULL;
264 return st;
265 }
266
expand_as_arraymev::evaluator_cfg267 bool expand_as_array(func_decl* f, expr_ref& result) {
268 if (!m_model_completion)
269 return false;
270 func_decl* g = nullptr;
271 if (!m_ar.is_as_array(f, g))
272 return false;
273 expr* def = nullptr;
274 if (m_def_cache.find(g, def)) {
275 result = def;
276 TRACE("model_evaluator", tout << result << "\n";);
277 return true;
278 }
279 expr_ref tmp(m);
280 func_interp* fi = m_model.get_func_interp(g);
281 if (fi && !fi->get_else()) {
282 fi->set_else(m_model.get_some_value(g->get_range()));
283 }
284 if (fi && (tmp = fi->get_array_interp(g))) {
285 model_evaluator ev(m_model, m_params);
286 ev.set_model_completion(false);
287 result = ev(tmp);
288 m_pinned.push_back(result);
289 m_def_cache.insert(g, result);
290 TRACE("model_evaluator", tout << mk_pp(g, m) << " " << result << "\n";);
291 return true;
292 }
293
294 TRACE("model_evaluator",
295 tout << "could not get array interpretation " << mk_pp(g, m) << " " << fi << "\n";
296 tout << m_model << "\n";);
297
298 return false;
299 }
300
expand_storesmev::evaluator_cfg301 void expand_stores(expr_ref& val) {
302 TRACE("model_evaluator", tout << val << "\n";);
303 vector<expr_ref_vector> stores;
304 expr_ref else_case(m);
305 bool _unused;
306 if (m_array_as_stores &&
307 m_ar.is_array(val) &&
308 extract_array_func_interp(val, stores, else_case, _unused)) {
309 sort* srt = val->get_sort();
310 val = m_ar.mk_const_array(srt, else_case);
311 for (unsigned i = stores.size(); i-- > 0; ) {
312 expr_ref_vector args(m);
313 args.push_back(val);
314 args.append(stores[i].size(), stores[i].data());
315 val = m_ar.mk_store(args);
316 }
317 TRACE("model_evaluator", tout << val << "\n";);
318 }
319 }
320
reduce_macromev::evaluator_cfg321 bool reduce_macro() { return true; }
322
get_macromev::evaluator_cfg323 bool get_macro(func_decl * f, expr * & def, quantifier * & , proof * &) {
324 func_interp * fi = m_model.get_func_interp(f);
325 def = nullptr;
326 if (fi != nullptr) {
327 if (fi->is_partial()) {
328 if (m_model_completion) {
329 sort * s = f->get_range();
330 expr * val = m_model.get_some_value(s);
331 fi->set_else(val);
332 }
333 else
334 return false;
335 }
336 def = fi->get_interp();
337 SASSERT(def != nullptr);
338 }
339 else if (m_model_completion &&
340 (f->get_family_id() == null_family_id ||
341 m.get_plugin(f->get_family_id())->is_considered_uninterpreted(f))) {
342 sort * s = f->get_range();
343 expr * val = m_model.get_some_value(s);
344 func_interp * new_fi = alloc(func_interp, m, f->get_arity());
345 new_fi->set_else(val);
346 m_model.register_decl(f, new_fi);
347 def = val;
348 SASSERT(def != nullptr);
349 }
350
351 CTRACE("model_evaluator", def != nullptr, tout << "get_macro for " << f->get_name() << " (model completion: " << m_model_completion << ") " << mk_pp(def, m) << "\n";);
352
353 return def != nullptr;
354 }
355
evaluate_partial_theory_funcmev::evaluator_cfg356 br_status evaluate_partial_theory_func(func_decl * f,
357 unsigned num, expr * const * args,
358 expr_ref & result, proof_ref & result_pr) {
359 SASSERT(f != nullptr);
360 SASSERT(!m.is_builtin_family_id(f->get_family_id()));
361 result = nullptr;
362 result_pr = nullptr;
363
364 if (f->get_family_id() == m_fpau.get_family_id() &&
365 !m_fpau.is_considered_uninterpreted(f, num, args)) {
366 // cwinter: should this be unreachable?
367 return BR_FAILED;
368 }
369
370 func_interp * fi = m_model.get_func_interp(f);
371
372 func_decl_ref f_ui(m);
373 if (!fi && m_au.is_considered_uninterpreted(f, num, args, f_ui)) {
374 if (f_ui) {
375 fi = m_model.get_func_interp(f_ui);
376 }
377
378 if (!fi) {
379 result = m_au.mk_numeral(rational(0), f->get_range());
380 return BR_DONE;
381 }
382 }
383 else if (!fi && m_fpau.is_considered_uninterpreted(f, num, args)) {
384 result = m.get_some_value(f->get_range());
385 return BR_DONE;
386 }
387 else if (m_dt.is_accessor(f) && !is_ground(args[0])) {
388 result = m.mk_app(f, num, args);
389 return BR_DONE;
390 }
391 if (fi) {
392 if (fi->is_partial())
393 fi->set_else(m.get_some_value(f->get_range()));
394
395 var_subst vs(m, false);
396 result = vs(fi->get_interp(), num, args);
397 if (!is_ground(result.get()) && recfun::util(m).is_defined(f))
398 return BR_DONE;
399 return BR_REWRITE_FULL;
400 }
401
402 return BR_FAILED;
403 }
404
405
max_steps_exceededmev::evaluator_cfg406 bool max_steps_exceeded(unsigned num_steps) const {
407 if (memory::get_allocation_size() > m_max_memory)
408 throw rewriter_exception(Z3_MAX_MEMORY_MSG);
409 return num_steps > m_max_steps;
410 }
411
mk_array_eqmev::evaluator_cfg412 br_status mk_array_eq(expr* a, expr* b, expr_ref& result) {
413
414 if (a == b) {
415 result = m.mk_true();
416 return BR_DONE;
417 }
418 if (!m_array_equalities) {
419 return m_ar_rw.mk_eq_core(a, b, result);
420 }
421 TRACE("model_evaluator", tout << "mk_array_eq " << m_array_equalities << " "
422 << mk_pp(a, m) << " " << mk_pp(b, m) << "\n";);
423
424 vector<expr_ref_vector> stores1, stores2;
425 bool args_are_unique1, args_are_unique2;
426 expr_ref else1(m), else2(m);
427 if (extract_array_func_interp(a, stores1, else1, args_are_unique1) &&
428 extract_array_func_interp(b, stores2, else2, args_are_unique2)) {
429 expr_ref_vector conj(m), args1(m), args2(m);
430 if (m.are_equal(else1, else2)) {
431 // no op
432 }
433 else if (m.are_distinct(else1, else2) && !(else1->get_sort()->get_info()->get_num_elements().is_finite())) {
434 result = m.mk_false();
435 return BR_DONE;
436 }
437 else {
438 conj.push_back(m.mk_eq(else1, else2));
439 }
440 if (args_are_unique1 && args_are_unique2 && !stores1.empty()) {
441 TRACE("model_evaluator", tout << "args are unique " << conj << "\n";);
442 return mk_array_eq_core(stores1, else1, stores2, else2, conj, result);
443 }
444
445 // TBD: this is too inefficient.
446 args1.push_back(a);
447 args2.push_back(b);
448 stores1.append(stores2);
449 for (unsigned i = 0; i < stores1.size(); ++i) {
450 args1.resize(1); args1.append(stores1[i].size() - 1, stores1[i].data());
451 args2.resize(1); args2.append(stores1[i].size() - 1, stores1[i].data());
452 expr_ref s1(m_ar.mk_select(args1.size(), args1.data()), m);
453 expr_ref s2(m_ar.mk_select(args2.size(), args2.data()), m);
454 conj.push_back(m.mk_eq(s1, s2));
455 }
456 result = mk_and(conj);
457 TRACE("model_evaluator", tout << mk_pp(a, m) << " == " << mk_pp(b, m) << " -> " << conj << "\n";
458 for (auto& s : stores1) tout << "store: " << s << "\n"; );
459 return BR_REWRITE_FULL;
460 }
461 return m_ar_rw.mk_eq_core(a, b, result);
462 }
463
464 struct args_eq {
465 unsigned m_arity;
args_eqmev::evaluator_cfg::args_eq466 args_eq(unsigned arity): m_arity(arity) {}
operator ()mev::evaluator_cfg::args_eq467 bool operator()(expr * const* args1, expr* const* args2) const {
468 for (unsigned i = 0; i < m_arity; ++i) {
469 if (args1[i] != args2[i]) {
470 return false;
471 }
472 }
473 return true;
474 }
475 };
476
477 struct args_hash {
478 unsigned m_arity;
args_hashmev::evaluator_cfg::args_hash479 args_hash(unsigned arity): m_arity(arity) {}
operator ()mev::evaluator_cfg::args_hash480 unsigned operator()(expr * const* args) const {
481 return get_composite_hash(args, m_arity, default_kind_hash_proc<expr*const*>(), *this);
482 }
operator ()mev::evaluator_cfg::args_hash483 unsigned operator()(expr* const* args, unsigned idx) const {
484 return args[idx]->hash();
485 }
486 };
487
488 typedef hashtable<expr*const*, args_hash, args_eq> args_table;
489
mk_array_eq_coremev::evaluator_cfg490 br_status mk_array_eq_core(vector<expr_ref_vector> const& stores1, expr* else1,
491 vector<expr_ref_vector> const& stores2, expr* else2,
492 expr_ref_vector& conj, expr_ref& result) {
493 unsigned arity = stores1[0].size()-1; // TBD: fix arity.
494 args_hash ah(arity);
495 args_eq ae(arity);
496 args_table table1(DEFAULT_HASHTABLE_INITIAL_CAPACITY, ah, ae);
497 args_table table2(DEFAULT_HASHTABLE_INITIAL_CAPACITY, ah, ae);
498 TRACE("model_evaluator",
499 tout << "arity " << arity << "\n";
500 for (auto& v : stores1) tout << "stores1: " << v << "\n";
501 for (auto& v : stores2) tout << "stores2: " << v << "\n";
502 tout << "else1: " << mk_pp(else1, m) << "\n";
503 tout << "else2: " << mk_pp(else2, m) << "\n";
504 tout << "conj: " << conj << "\n";);
505
506 // stores with smaller index take precedence
507 for (unsigned i = stores1.size(); i-- > 0; ) {
508 table1.insert(stores1[i].data());
509 }
510
511 for (unsigned i = 0, sz = stores2.size(); i < sz; ++i) {
512 if (table2.contains(stores2[i].data())) {
513 // first insertion takes precedence.
514 TRACE("model_evaluator", tout << "duplicate " << stores2[i] << "\n";);
515 continue;
516 }
517 table2.insert(stores2[i].data());
518 expr * const* args = nullptr;
519 expr* val = stores2[i][arity];
520 if (table1.find(stores2[i].data(), args)) {
521 TRACE("model_evaluator", tout << "found value " << stores2[i] << "\n";);
522 table1.remove(args);
523 switch (compare(args[arity], val)) {
524 case l_true: break;
525 case l_false: result = m.mk_false(); return BR_DONE;
526 default: conj.push_back(m.mk_eq(val, args[arity])); break;
527 }
528 }
529 else {
530 TRACE("model_evaluator", tout << "not found value " << stores2[i] << "\n";);
531 switch (compare(else1, val)) {
532 case l_true: break;
533 case l_false: result = m.mk_false(); return BR_DONE;
534 default: conj.push_back(m.mk_eq(else1, val)); break;
535 }
536 }
537 }
538 for (auto const& t : table1) {
539 switch (compare((t)[arity], else2)) {
540 case l_true: break;
541 case l_false: result = m.mk_false(); return BR_DONE;
542 default: conj.push_back(m.mk_eq((t)[arity], else2)); break;
543 }
544 }
545 result = mk_and(conj);
546 return BR_REWRITE_FULL;
547 }
548
comparemev::evaluator_cfg549 lbool compare(expr* a, expr* b) {
550 if (m.are_equal(a, b)) return l_true;
551 if (m.are_distinct(a, b)) return l_false;
552 return l_undef;
553 }
554
555
args_are_valuesmev::evaluator_cfg556 bool args_are_values(expr_ref_vector const& store, bool& are_unique) {
557 bool are_values = true;
558 for (unsigned j = 0; are_values && j + 1 < store.size(); ++j) {
559 are_values = m.is_value(store[j]);
560 are_unique &= m.is_unique_value(store[j]);
561 }
562 SASSERT(!are_unique || are_values);
563 return are_values;
564 }
565
566
extract_array_func_interpmev::evaluator_cfg567 bool extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref& else_case, bool& are_unique) {
568 SASSERT(m_ar.is_array(a));
569 bool are_values = true;
570 are_unique = true;
571 TRACE("model_evaluator", tout << mk_pp(a, m) << "\n";);
572
573 while (m_ar.is_store(a)) {
574 expr_ref_vector store(m);
575 store.append(to_app(a)->get_num_args()-1, to_app(a)->get_args()+1);
576 are_values &= args_are_values(store, are_unique);
577 stores.push_back(store);
578 a = to_app(a)->get_arg(0);
579 }
580
581 if (m_ar.is_const(a)) {
582 else_case = to_app(a)->get_arg(0);
583 return true;
584 }
585
586 if (m_ar_rw.has_index_set(a, else_case, stores)) {
587 for (auto const& store : stores) {
588 are_values &= args_are_values(store, are_unique);
589 }
590 return true;
591 }
592 if (!m_ar.is_as_array(a)) {
593 TRACE("model_evaluator", tout << "no translation: " << mk_pp(a, m) << "\n";);
594 TRACE("model_evaluator", tout << m_model << "\n";);
595 return false;
596 }
597
598 func_decl* f = m_ar.get_as_array_func_decl(to_app(a));
599 func_interp* g = m_model.get_func_interp(f);
600 if (!g) {
601 TRACE("model_evaluator", tout << "no interpretation for " << mk_pp(f, m) << "\n";);
602 return false;
603 }
604 else_case = g->get_else();
605 if (!else_case) {
606 TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m) << "\n";);
607 return false;
608 }
609 bool ground = is_ground(else_case);
610 unsigned sz = g->num_entries();
611 expr_ref_vector store(m);
612 for (unsigned i = 0; i < sz; ++i) {
613 store.reset();
614 func_entry const* fe = g->get_entry(i);
615 expr* res = fe->get_result();
616 if (m.are_equal(else_case, res)) {
617 continue;
618 }
619 ground &= is_ground(res);
620 store.append(g->get_arity(), fe->get_args());
621 store.push_back(res);
622 for (expr* arg : store) {
623 ground &= is_ground(arg);
624 }
625 stores.push_back(store);
626 }
627 if (!ground) {
628 TRACE("model_evaluator", tout << "could not extract ground array interpretation: " << mk_pp(a, m) << "\n";);
629 return false;
630 }
631 return true;
632 }
633 };
634 }
635
636 struct model_evaluator::imp : public rewriter_tpl<mev::evaluator_cfg> {
637 mev::evaluator_cfg m_cfg;
impmodel_evaluator::imp638 imp(model_core & md, params_ref const & p):
639 rewriter_tpl<mev::evaluator_cfg>(md.get_manager(),
640 false, // no proofs for evaluator
641 m_cfg),
642 m_cfg(md.get_manager(), md, p) {
643 }
expand_storesmodel_evaluator::imp644 void expand_stores(expr_ref &val) {m_cfg.expand_stores(val);}
resetmodel_evaluator::imp645 void reset() {
646 rewriter_tpl<mev::evaluator_cfg>::reset();
647 m_cfg.reset();
648 m_cfg.m_def_cache.reset();
649 }
650 };
651
model_evaluator(model_core & md,params_ref const & p)652 model_evaluator::model_evaluator(model_core & md, params_ref const & p) {
653 m_imp = alloc(imp, md, p);
654 }
655
m() const656 ast_manager & model_evaluator::m() const {
657 return m_imp->m();
658 }
659
~model_evaluator()660 model_evaluator::~model_evaluator() {
661 dealloc(m_imp);
662 }
663
updt_params(params_ref const & p)664 void model_evaluator::updt_params(params_ref const & p) {
665 m_imp->cfg().updt_params(p);
666 }
667
get_param_descrs(param_descrs & r)668 void model_evaluator::get_param_descrs(param_descrs & r) {
669 model_evaluator_params::collect_param_descrs(r);
670 }
671
set_model_completion(bool f)672 void model_evaluator::set_model_completion(bool f) {
673 if (m_imp->cfg().m_model_completion != f) {
674 reset();
675 m_imp->cfg().m_model_completion = f;
676 }
677 }
678
get_model_completion() const679 bool model_evaluator::get_model_completion() const {
680 return m_imp->cfg().m_model_completion;
681 }
682
set_expand_array_equalities(bool f)683 void model_evaluator::set_expand_array_equalities(bool f) {
684 m_imp->cfg().m_array_equalities = f;
685 }
686
get_num_steps() const687 unsigned model_evaluator::get_num_steps() const {
688 return m_imp->get_num_steps();
689 }
690
cleanup(params_ref const & p)691 void model_evaluator::cleanup(params_ref const & p) {
692 model_core & md = m_imp->cfg().m_model;
693 m_imp->~imp();
694 new (m_imp) imp(md, p);
695 }
696
reset(params_ref const & p)697 void model_evaluator::reset(params_ref const & p) {
698 m_imp->reset();
699 updt_params(p);
700 }
701
reset(model_core & model,params_ref const & p)702 void model_evaluator::reset(model_core &model, params_ref const& p) {
703 m_imp->~imp();
704 new (m_imp) imp(model, p);
705 }
706
707
operator ()(expr * t,expr_ref & result)708 void model_evaluator::operator()(expr * t, expr_ref & result) {
709 TRACE("model_evaluator", tout << mk_ismt2_pp(t, m()) << "\n";);
710 m_imp->operator()(t, result);
711 m_imp->expand_stores(result);
712 TRACE("model_evaluator", tout << "eval: " << mk_ismt2_pp(t, m()) << " --> " << result << "\n";);
713 }
714
operator ()(expr * t)715 expr_ref model_evaluator::operator()(expr * t) {
716 expr_ref result(m());
717 this->operator()(t, result);
718 return result;
719 }
720
operator ()(expr_ref_vector const & ts)721 expr_ref_vector model_evaluator::operator()(expr_ref_vector const& ts) {
722 expr_ref_vector rs(m());
723 for (expr* t : ts) rs.push_back((*this)(t));
724 return rs;
725 }
726
727
is_true(expr * t)728 bool model_evaluator::is_true(expr* t) {
729 expr_ref tmp(m());
730 return eval(t, tmp, true) && m().is_true(tmp);
731 }
732
is_false(expr * t)733 bool model_evaluator::is_false(expr* t) {
734 expr_ref tmp(m());
735 return eval(t, tmp, true) && m().is_false(tmp);
736 }
737
is_true(expr_ref_vector const & ts)738 bool model_evaluator::is_true(expr_ref_vector const& ts) {
739 for (expr* t : ts) if (!is_true(t)) return false;
740 return true;
741 }
742
are_equal(expr * s,expr * t)743 bool model_evaluator::are_equal(expr* s, expr* t) {
744 if (m().are_equal(s, t)) return true;
745 if (m().are_distinct(s, t)) return false;
746 expr_ref t1(m()), t2(m());
747 eval(t, t1, true);
748 eval(s, t2, true);
749 return m().are_equal(t1, t2);
750 }
751
eval(expr * t,expr_ref & r,bool model_completion)752 bool model_evaluator::eval(expr* t, expr_ref& r, bool model_completion) {
753 set_model_completion(model_completion);
754 try {
755 r = (*this)(t);
756 return true;
757 }
758 catch (model_evaluator_exception &ex) {
759 (void)ex;
760 TRACE("model_evaluator", tout << ex.msg () << "\n";);
761 return false;
762 }
763 }
764
eval(expr_ref_vector const & ts,expr_ref & r,bool model_completion)765 bool model_evaluator::eval(expr_ref_vector const& ts, expr_ref& r, bool model_completion) {
766 expr_ref tmp(m());
767 tmp = mk_and(ts);
768 return eval(tmp, r, model_completion);
769 }
770
set_solver(expr_solver * solver)771 void model_evaluator::set_solver(expr_solver* solver) {
772 m_imp->m_cfg.m_seq_rw.set_solver(solver);
773 }
774
has_solver()775 bool model_evaluator::has_solver() {
776 return m_imp->m_cfg.m_seq_rw.has_solver();
777 }
778
get_model() const779 model_core const & model_evaluator::get_model() const {
780 return m_imp->cfg().m_model;
781 }
782