1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3
4 Module Name:
5
6 model.cpp
7
8 Abstract:
9
10 <abstract>
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2011-04-30.
15
16 Revision History:
17
18 --*/
19 #include "ast/ast.h"
20 #include "util/top_sort.h"
21 #include "ast/ast_pp.h"
22 #include "ast/ast_ll_pp.h"
23 #include "ast/rewriter/var_subst.h"
24 #include "ast/rewriter/th_rewriter.h"
25 #include "ast/array_decl_plugin.h"
26 #include "ast/bv_decl_plugin.h"
27 #include "ast/well_sorted.h"
28 #include "ast/used_symbols.h"
29 #include "ast/for_each_expr.h"
30 #include "ast/for_each_ast.h"
31 #include "model/model.h"
32 #include "model/model_params.hpp"
33 #include "model/model_evaluator.h"
34 #include "model/array_factory.h"
35 #include "model/value_factory.h"
36 #include "model/seq_factory.h"
37 #include "model/datatype_factory.h"
38 #include "model/numeral_factory.h"
39 #include "model/fpa_factory.h"
40
41
model(ast_manager & m)42 model::model(ast_manager & m):
43 model_core(m),
44 m_mev(*this),
45 m_cleaned(false),
46 m_inline(false) {
47 }
48
~model()49 model::~model() {
50 for (auto & kv : m_usort2universe) {
51 m.dec_ref(kv.m_key);
52 m.dec_array_ref(kv.m_value->size(), kv.m_value->c_ptr());
53 dealloc(kv.m_value);
54 }
55 }
56
updt_params(params_ref const & p)57 void model::updt_params(params_ref const & p) {
58 model_params mp(p);
59 m_inline = mp.inline_def();
60 m_mev.updt_params(p);
61 }
62
63
copy_const_interps(model const & source)64 void model::copy_const_interps(model const & source) {
65 for (auto const& kv : source.m_interp)
66 register_decl(kv.m_key, kv.m_value.second);
67 }
68
copy_func_interps(model const & source)69 void model::copy_func_interps(model const & source) {
70 for (auto const& kv : source.m_finterp)
71 register_decl(kv.m_key, kv.m_value->copy());
72 }
73
copy_usort_interps(model const & source)74 void model::copy_usort_interps(model const & source) {
75 for (auto const& kv : source.m_usort2universe)
76 register_usort(kv.m_key, kv.m_value->size(), kv.m_value->c_ptr());
77 }
78
copy() const79 model * model::copy() const {
80 model * mdl = alloc(model, m);
81 mdl->copy_const_interps(*this);
82 mdl->copy_func_interps(*this);
83 mdl->copy_usort_interps(*this);
84 return mdl;
85 }
86
eval_expr(expr * e,expr_ref & result,bool model_completion)87 bool model::eval_expr(expr * e, expr_ref & result, bool model_completion) {
88 scoped_model_completion _smc(*this, model_completion);
89 try {
90 result = (*this)(e);
91 return true;
92 }
93 catch (model_evaluator_exception & ex) {
94 (void)ex;
95 TRACE("model_evaluator", tout << ex.msg() << "\n";);
96 return false;
97 }
98 }
99
get_factory(sort * s)100 value_factory* model::get_factory(sort* s) {
101 if (m_factories.plugins().empty()) {
102 seq_util su(m);
103 fpa_util fu(m);
104 m_factories.register_plugin(alloc(array_factory, m, *this));
105 m_factories.register_plugin(alloc(datatype_factory, m, *this));
106 m_factories.register_plugin(alloc(bv_factory, m));
107 m_factories.register_plugin(alloc(arith_factory, m));
108 m_factories.register_plugin(alloc(seq_factory, m, su.get_family_id(), *this));
109 m_factories.register_plugin(alloc(fpa_value_factory, m, fu.get_family_id()));
110 }
111 family_id fid = s->get_family_id();
112 return m_factories.get_plugin(fid);
113 }
114
get_some_value(sort * s)115 expr * model::get_some_value(sort * s) {
116 ptr_vector<expr> * u = nullptr;
117 if (m_usort2universe.find(s, u)) {
118 if (!u->empty())
119 return u->get(0);
120 }
121 return m.get_some_value(s);
122 }
123
get_fresh_value(sort * s)124 expr * model::get_fresh_value(sort * s) {
125 return get_factory(s)->get_fresh_value(s);
126 }
127
get_some_values(sort * s,expr_ref & v1,expr_ref & v2)128 bool model::get_some_values(sort * s, expr_ref& v1, expr_ref& v2) {
129 return get_factory(s)->get_some_values(s, v1, v2);
130 }
131
get_universe(sort * s) const132 ptr_vector<expr> const & model::get_universe(sort * s) const {
133 return *m_usort2universe[s];
134 }
135
has_uninterpreted_sort(sort * s) const136 bool model::has_uninterpreted_sort(sort * s) const {
137 ptr_vector<expr> * u = nullptr;
138 m_usort2universe.find(s, u);
139 return u != nullptr;
140 }
141
get_num_uninterpreted_sorts() const142 unsigned model::get_num_uninterpreted_sorts() const {
143 return m_usorts.size();
144 }
145
get_uninterpreted_sort(unsigned idx) const146 sort * model::get_uninterpreted_sort(unsigned idx) const {
147 return m_usorts[idx];
148 }
149
register_usort(sort * s,unsigned usize,expr * const * universe)150 void model::register_usort(sort * s, unsigned usize, expr * const * universe) {
151 ptr_vector<expr>* & u = m_usort2universe.insert_if_not_there(s, nullptr);
152 m.inc_array_ref(usize, universe);
153 if (!u) {
154 m_usorts.push_back(s);
155 m.inc_ref(s);
156 u = alloc(ptr_vector<expr>);
157 u->append(usize, universe);
158 }
159 else {
160 m.dec_array_ref(u->size(), u->c_ptr());
161 u->reset();
162 u->append(usize, universe);
163 }
164 }
165
translate(ast_translation & translator) const166 model * model::translate(ast_translation & translator) const {
167 model * res = alloc(model, translator.to());
168
169 // Translate const interps
170 for (auto const& kv : m_interp) {
171 func_decl_ref d(translator(kv.m_key), translator.to());
172 expr_ref v(translator(kv.m_value.second), translator.to());
173 res->register_decl(d, v);
174 }
175 // Translate func interps
176 for (auto const& kv : m_finterp) {
177 func_interp* fi = kv.m_value->translate(translator);
178 res->register_decl(translator(kv.m_key), fi);
179 }
180
181 // Translate usort interps
182 for (auto const& kv : m_usort2universe) {
183 ptr_vector<expr> new_universe;
184 for (expr* e : *kv.m_value) {
185 new_universe.push_back(translator(e));
186 }
187 res->register_usort(translator(kv.m_key),
188 new_universe.size(),
189 new_universe.c_ptr());
190 }
191
192 return res;
193 }
194
195 struct model::top_sort : public ::top_sort<func_decl> {
196 func_decl_ref_vector m_pinned; // protect keys in m_occur_count
197 th_rewriter m_rewrite;
198 obj_map<func_decl, unsigned> m_occur_count;
199
200
top_sortmodel::top_sort201 top_sort(ast_manager& m):
202 m_pinned(m), m_rewrite(m)
203 {
204 params_ref p;
205 p.set_bool("elim_ite", false);
206 p.set_bool("ite_extra_rules", true);
207 m_rewrite.updt_params(p);
208 }
209
add_occursmodel::top_sort210 void add_occurs(func_decl* f) {
211 m_pinned.push_back(f);
212 m_occur_count.insert(f, occur_count(f) + 1);
213 }
214
occur_countmodel::top_sort215 unsigned occur_count(func_decl* f) const {
216 unsigned count = 0;
217 m_occur_count.find(f, count);
218 return count;
219 }
220
~top_sortmodel::top_sort221 ~top_sort() override {}
222 };
223
compress()224 void model::compress() {
225 if (m_cleaned) return;
226
227 // stratify m_finterp and m_decls in a topological sort
228 // such that functions f1 < f2 then f1 does not use f2.
229 // then for each function in order clean-up the interpretations
230 // by substituting in auxiliary definitions that can be eliminated.
231
232 func_decl_ref_vector pinned(m);
233 while (true) {
234 top_sort ts(m);
235 collect_deps(ts);
236 ts.topological_sort();
237 for (func_decl * f : ts.top_sorted()) {
238 cleanup_interp(ts, f);
239 }
240
241 func_decl_set removed;
242 ts.m_occur_count.reset();
243 for (func_decl * f : ts.top_sorted()) {
244 collect_occs(ts, f);
245 }
246
247 // remove auxiliary declarations that are not used.
248 for (func_decl * f : ts.top_sorted()) {
249 if (f->is_skolem() && ts.occur_count(f) == 0) {
250 pinned.push_back(f);
251 unregister_decl(f);
252 removed.insert(f);
253 }
254 }
255 if (removed.empty()) break;
256 TRACE("model", tout << "remove\n"; for (func_decl* f : removed) tout << f->get_name() << "\n";);
257 remove_decls(m_decls, removed);
258 remove_decls(m_func_decls, removed);
259 remove_decls(m_const_decls, removed);
260 }
261 m_cleaned = true;
262 reset_eval_cache();
263 }
264
265
collect_deps(top_sort & ts)266 void model::collect_deps(top_sort& ts) {
267 for (auto const& kv : m_finterp) {
268 ts.insert(kv.m_key, collect_deps(ts, kv.m_value));
269 }
270 for (auto const& kv : m_interp) {
271 ts.insert(kv.m_key, collect_deps(ts, kv.m_value.second));
272 }
273 }
274
275 struct model::deps_collector {
276 model& m;
277 top_sort& ts;
278 func_decl_set& s;
279 array_util autil;
deps_collectormodel::deps_collector280 deps_collector(model& m, top_sort& ts, func_decl_set& s): m(m), ts(ts), s(s), autil(m.get_manager()) {}
operator ()model::deps_collector281 void operator()(app* a) {
282 func_decl* f = a->get_decl();
283 if (autil.is_as_array(f)) {
284 f = autil.get_as_array_func_decl(a);
285 }
286 if (m.has_interpretation(f)) {
287 s.insert(f);
288 ts.add_occurs(f);
289 }
290 }
operator ()model::deps_collector291 void operator()(expr* ) {}
292 };
293
294 struct model::occs_collector {
295 top_sort& ts;
occs_collectormodel::occs_collector296 occs_collector(top_sort& ts): ts(ts) {}
operator ()model::occs_collector297 void operator()(func_decl* f) {
298 ts.add_occurs(f);
299 }
operator ()model::occs_collector300 void operator()(ast*) {}
301 };
302
303
collect_deps(top_sort & ts,expr * e)304 model::func_decl_set* model::collect_deps(top_sort& ts, expr * e) {
305 func_decl_set* s = alloc(func_decl_set);
306 deps_collector collector(*this, ts, *s);
307 if (e) for_each_expr(collector, e);
308 return s;
309 }
310
collect_deps(top_sort & ts,func_interp * fi)311 model::func_decl_set* model::collect_deps(top_sort& ts, func_interp * fi) {
312 func_decl_set* s = alloc(func_decl_set);
313 deps_collector collector(*this, ts, *s);
314 fi->compress();
315 expr* e = fi->get_else();
316 if (e) for_each_expr(collector, e);
317 unsigned num_args = fi->get_arity();
318 for (func_entry* fe : *fi) {
319 for (unsigned i = 0; i < num_args; ++i) {
320 for_each_expr(collector, fe->get_arg(i));
321 }
322 for_each_expr(collector, fe->get_result());
323 }
324 return s;
325 }
326
327
328 /**
329 \brief Inline interpretations of skolem functions
330 */
331
cleanup_interp(top_sort & ts,func_decl * f)332 void model::cleanup_interp(top_sort& ts, func_decl* f) {
333 unsigned pid = ts.partition_id(f);
334 expr * e1 = get_const_interp(f);
335 if (e1) {
336 expr_ref e2 = cleanup_expr(ts, e1, pid);
337 if (e2 != e1)
338 register_decl(f, e2);
339 return;
340 }
341 func_interp* fi = get_func_interp(f);
342 if (fi) {
343 e1 = fi->get_else();
344 expr_ref e2 = cleanup_expr(ts, e1, pid);
345 if (e1 != e2)
346 fi->set_else(e2);
347 for (auto& fe : *fi) {
348 e2 = cleanup_expr(ts, fe->get_result(), pid);
349 if (e2 != fe->get_result()) {
350 fi->insert_entry(fe->get_args(), e2);
351 }
352 }
353 }
354 }
355
collect_occs(top_sort & ts,func_decl * f)356 void model::collect_occs(top_sort& ts, func_decl* f) {
357 expr * e = get_const_interp(f);
358 if (e) {
359 collect_occs(ts, e);
360 }
361 else {
362 func_interp* fi = get_func_interp(f);
363 if (fi) {
364 e = fi->get_else();
365 if (e != nullptr)
366 collect_occs(ts, e);
367 for (auto const& fe : *fi) {
368 collect_occs(ts, fe->get_result());
369 for (unsigned i = 0; i < fi->get_arity(); ++i) {
370 collect_occs(ts, fe->get_arg(i));
371 }
372 }
373 }
374 }
375 }
376
collect_occs(top_sort & ts,expr * e)377 void model::collect_occs(top_sort& ts, expr* e) {
378 occs_collector collector(ts);
379 for_each_ast(collector, e, true);
380 }
381
can_inline_def(top_sort & ts,func_decl * f)382 bool model::can_inline_def(top_sort& ts, func_decl* f) {
383 if (ts.occur_count(f) <= 1) return true;
384 func_interp* fi = get_func_interp(f);
385 if (!fi) return false;
386 if (fi->get_else() == nullptr) return false;
387 if (m_inline) return true;
388 expr* e = fi->get_else();
389 obj_hashtable<expr> subs;
390 ptr_buffer<expr> todo;
391 todo.push_back(e);
392 while (!todo.empty()) {
393 if (fi->num_entries() + subs.size() > 8) return false;
394 expr* e = todo.back();
395 todo.pop_back();
396 if (subs.contains(e)) continue;
397 subs.insert(e);
398 if (is_app(e)) {
399 for (expr* arg : *to_app(e)) {
400 todo.push_back(arg);
401 }
402 }
403 else if (is_quantifier(e)) {
404 todo.push_back(to_quantifier(e)->get_expr());
405 }
406 }
407 return true;
408 }
409
410
cleanup_expr(top_sort & ts,expr * e,unsigned current_partition)411 expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition) {
412 if (!e) return expr_ref(nullptr, m);
413
414 TRACE("model", tout << "cleaning up:\n" << mk_pp(e, m) << "\n";);
415
416 obj_map<expr, expr*> cache;
417 expr_ref_vector trail(m);
418 ptr_buffer<expr, 128> todo;
419 ptr_buffer<expr> args;
420 todo.push_back(e);
421 array_util autil(m);
422 bv_util bv(m);
423 func_interp* fi = nullptr;
424 unsigned pid = 0;
425 expr_ref new_t(m);
426
427 while (!todo.empty()) {
428 expr* a = todo.back();
429 switch(a->get_kind()) {
430 case AST_APP: {
431 app * t = to_app(a);
432 func_decl* f = t->get_decl();
433 bool visited = true;
434
435 args.reset();
436 for (expr* t_arg : *t) {
437 expr * arg = nullptr;
438 if (!cache.find(t_arg, arg)) {
439 visited = false;
440 todo.push_back(t_arg);
441 }
442 else {
443 args.push_back(arg);
444 }
445 }
446 if (!visited) {
447 continue;
448 }
449 fi = nullptr;
450 new_t = nullptr;
451 sort_ref_vector domain(m);
452 if (autil.is_as_array(a)) {
453 func_decl* f = autil.get_as_array_func_decl(a);
454 // only expand auxiliary definitions that occur once.
455 if (can_inline_def(ts, f)) {
456 fi = get_func_interp(f);
457 if (fi) {
458 new_t = fi->get_array_interp(f);
459 TRACE("model", tout << "array interpretation:" << new_t << "\n";);
460 }
461 }
462 }
463
464 if (new_t) {
465 // noop
466 }
467 else if (f->is_skolem() && can_inline_def(ts, f) && (fi = get_func_interp(f)) &&
468 fi->get_interp() && (!ts.partition_ids().find(f, pid) || pid != current_partition)) {
469 var_subst vs(m, false);
470 new_t = vs(fi->get_interp(), args.size(), args.c_ptr());
471 }
472 else if (bv.is_bit2bool(t)) {
473 unsigned idx = f->get_parameter(0).get_int();
474 new_t = m.mk_eq(bv.mk_extract(idx, idx, args[0]), bv.mk_numeral(1, 1));
475 }
476 #if 0
477 else if (is_uninterp_const(a) && !get_const_interp(f)) {
478 new_t = get_some_value(f->get_range());
479 register_decl(f, new_t);
480 }
481 #endif
482 else {
483 new_t = ts.m_rewrite.mk_app(f, args.size(), args.c_ptr());
484 }
485
486 if (t != new_t.get()) trail.push_back(new_t);
487 CTRACE("model", (t != new_t.get()), tout << mk_bounded_pp(t, m) << " " << new_t << "\n";);
488 todo.pop_back();
489 cache.insert(t, new_t);
490 break;
491 }
492 default:
493 SASSERT(a != nullptr);
494 cache.insert(a, a);
495 todo.pop_back();
496 break;
497 }
498 }
499
500 ts.m_rewrite(cache[e], new_t);
501 return new_t;
502 }
503
remove_decls(ptr_vector<func_decl> & decls,func_decl_set const & s)504 void model::remove_decls(ptr_vector<func_decl> & decls, func_decl_set const & s) {
505 unsigned j = 0;
506 for (func_decl* f : decls) {
507 if (!s.contains(f)) {
508 decls[j++] = f;
509 }
510 }
511 decls.shrink(j);
512 }
513
unfold_as_array(expr * e)514 expr_ref model::unfold_as_array(expr* e) {
515 func_decl* f = nullptr;
516 array_util autil(m);
517 if (!autil.is_as_array(e, f))
518 return expr_ref(e, m);
519 auto* fi = get_func_interp(f);
520 if (!fi)
521 return expr_ref(e, m);
522 return fi->get_array_interp(f);
523 }
524
525
get_inlined_const_interp(func_decl * f)526 expr_ref model::get_inlined_const_interp(func_decl* f) {
527 expr* v = get_const_interp(f);
528 if (!v) return expr_ref(nullptr, m);
529 top_sort st(m);
530 expr_ref result1(v, m);
531 expr_ref result2 = cleanup_expr(st, v, UINT_MAX);
532 while (result1 != result2) {
533 result1 = result2;
534 result2 = cleanup_expr(st, result1, UINT_MAX);
535 }
536 return result2;
537 }
538
operator ()(expr * t)539 expr_ref model::operator()(expr* t) {
540 return m_mev(t);
541 }
542
set_solver(expr_solver * s)543 void model::set_solver(expr_solver* s) {
544 m_mev.set_solver(s);
545 }
546
has_solver()547 bool model::has_solver() {
548 return m_mev.has_solver();
549 }
550
operator ()(expr_ref_vector const & ts)551 expr_ref_vector model::operator()(expr_ref_vector const& ts) {
552 expr_ref_vector rs(m);
553 for (expr* t : ts) rs.push_back((*this)(t));
554 return rs;
555 }
556
is_true(expr * t)557 bool model::is_true(expr* t) {
558 return m.is_true((*this)(t));
559 }
560
is_false(expr * t)561 bool model::is_false(expr* t) {
562 return m.is_false((*this)(t));
563 }
564
is_true(expr_ref_vector const & ts)565 bool model::is_true(expr_ref_vector const& ts) {
566 for (expr* t : ts) if (!is_true(t)) return false;
567 return true;
568 }
569
is_false(expr_ref_vector const & ts)570 bool model::is_false(expr_ref_vector const& ts) {
571 for (expr* t : ts) if (is_false(t)) return true;
572 return false;
573 }
574
are_equal(expr * s,expr * t)575 bool model::are_equal(expr* s, expr* t) {
576 return m_mev.are_equal(s, t);
577 }
578
reset_eval_cache()579 void model::reset_eval_cache() {
580 m_mev.reset();
581 }
582
583