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