1 /**
2 Copyright (c) 2017 Arie Gurfinkel
3 
4  Deprecated implementation of model evaluator. To be removed.
5 */
6 
7 #include <sstream>
8 #include "ast/array_decl_plugin.h"
9 #include "ast/ast_pp.h"
10 #include "ast/rewriter/bool_rewriter.h"
11 #include "muz/base/dl_util.h"
12 #include "ast/for_each_expr.h"
13 #include "smt/params/smt_params.h"
14 #include "model/model.h"
15 #include "util/ref_vector.h"
16 #include "ast/rewriter/rewriter.h"
17 #include "ast/rewriter/rewriter_def.h"
18 #include "util/util.h"
19 #include "muz/spacer/spacer_manager.h"
20 #include "muz/spacer/spacer_legacy_mev.h"
21 #include "muz/spacer/spacer_util.h"
22 #include "ast/arith_decl_plugin.h"
23 #include "ast/rewriter/expr_replacer.h"
24 #include "model/model_smt2_pp.h"
25 #include "ast/scoped_proof.h"
26 #include "qe/qe_lite.h"
27 #include "muz/spacer/spacer_qe_project.h"
28 #include "model/model_pp.h"
29 #include "ast/rewriter/expr_safe_replace.h"
30 
31 #include "ast/datatype_decl_plugin.h"
32 #include "ast/bv_decl_plugin.h"
33 
34 namespace old {
35 
36 /////////////////////////
37 // model_evaluator
38 //
39 
40 
assign_value(expr * e,expr * val)41 void model_evaluator::assign_value(expr* e, expr* val)
42 {
43     rational r;
44     if (m.is_true(val)) {
45         set_true(e);
46     } else if (m.is_false(val)) {
47         set_false(e);
48     } else if (m_arith.is_numeral(val, r)) {
49         set_number(e, r);
50     } else if (m.is_value(val)) {
51         set_value(e, val);
52     } else {
53         IF_VERBOSE(3, verbose_stream() << "Not evaluated " << mk_pp(e, m) << "\n";);
54         TRACE("old_spacer", tout << "Variable is not tracked: " << mk_pp(e, m) << "\n";);
55         set_x(e);
56     }
57 }
58 
setup_model(const model_ref & model)59 void model_evaluator::setup_model(const model_ref& model)
60 {
61     m_numbers.reset();
62     m_values.reset();
63     m_model = model.get();
64     rational r;
65     unsigned sz = model->get_num_constants();
66     for (unsigned i = 0; i < sz; i++) {
67         func_decl * d = model->get_constant(i);
68         expr* val = model->get_const_interp(d);
69         expr* e = m.mk_const(d);
70         m_refs.push_back(e);
71         assign_value(e, val);
72     }
73 }
74 
reset()75 void model_evaluator::reset()
76 {
77     m1.reset();
78     m2.reset();
79     m_values.reset();
80     m_visited.reset();
81     m_numbers.reset();
82     m_refs.reset();
83     m_model = nullptr;
84 }
85 
86 
minimize_literals(ptr_vector<expr> const & formulas,const model_ref & mdl,expr_ref_vector & result)87 void model_evaluator::minimize_literals(ptr_vector<expr> const& formulas,
88                                         const model_ref& mdl, expr_ref_vector& result)
89 {
90 
91     TRACE("old_spacer",
92           tout << "formulas:\n";
93           for (unsigned i = 0; i < formulas.size(); ++i) tout << mk_pp(formulas[i], m) << "\n";
94          );
95 
96     expr_ref tmp(m);
97     ptr_vector<expr> tocollect;
98 
99     setup_model(mdl);
100     collect(formulas, tocollect);
101     for (unsigned i = 0; i < tocollect.size(); ++i) {
102         expr* e = tocollect[i];
103         expr* e1, *e2;
104         SASSERT(m.is_bool(e));
105         SASSERT(is_true(e) || is_false(e));
106         if (is_true(e)) {
107             result.push_back(e);
108         }
109         // hack to break disequalities for arithmetic variables.
110         else if (m.is_eq(e, e1, e2) && m_arith.is_int_real(e1)) {
111             if (get_number(e1) < get_number(e2)) {
112                 result.push_back(m_arith.mk_lt(e1, e2));
113             } else {
114                 result.push_back(m_arith.mk_lt(e2, e1));
115             }
116         } else {
117             result.push_back(m.mk_not(e));
118         }
119     }
120     reset();
121     TRACE("old_spacer",
122           tout << "minimized model:\n";
123           for (unsigned i = 0; i < result.size(); ++i) tout << mk_pp(result[i].get(), m) << "\n";
124          );
125 }
126 
process_formula(app * e,ptr_vector<expr> & todo,ptr_vector<expr> & tocollect)127 void model_evaluator::process_formula(app* e, ptr_vector<expr>& todo, ptr_vector<expr>& tocollect)
128 {
129     SASSERT(m.is_bool(e));
130     SASSERT(is_true(e) || is_false(e));
131     unsigned v = is_true(e);
132     unsigned sz = e->get_num_args();
133     expr* const* args = e->get_args();
134     if (e->get_family_id() == m.get_basic_family_id()) {
135         switch (e->get_decl_kind()) {
136         case OP_TRUE:
137             break;
138         case OP_FALSE:
139             break;
140         case OP_EQ:
141             if (args[0] == args[1]) {
142                 SASSERT(v);
143                 // no-op
144             } else if (m.is_bool(args[0])) {
145                 todo.append(sz, args);
146             } else {
147                 tocollect.push_back(e);
148             }
149             break;
150         case OP_DISTINCT:
151             tocollect.push_back(e);
152             break;
153         case OP_ITE:
154             if (args[1] == args[2]) {
155                 tocollect.push_back(args[1]);
156             } else if (is_true(args[1]) && is_true(args[2])) {
157                 todo.append(2, args + 1);
158             } else if (is_false(args[1]) && is_false(args[2])) {
159                 todo.append(2, args + 1);
160             } else if (is_true(args[0])) {
161                 todo.append(2, args);
162             } else {
163                 SASSERT(is_false(args[0]));
164                 todo.push_back(args[0]);
165                 todo.push_back(args[2]);
166             }
167             break;
168         case OP_AND:
169             if (v) {
170                 todo.append(sz, args);
171             } else {
172                 unsigned i = 0;
173                 for (; !is_false(args[i]) && i < sz; ++i);
174                 if (i == sz) {
175                     fatal_error(1);
176                 }
177                 VERIFY(i < sz);
178                 todo.push_back(args[i]);
179             }
180             break;
181         case OP_OR:
182             if (v) {
183                 unsigned i = 0;
184                 for (; !is_true(args[i]) && i < sz; ++i);
185                 if (i == sz) {
186                     fatal_error(1);
187                 }
188                 VERIFY(i < sz);
189                 todo.push_back(args[i]);
190             } else {
191                 todo.append(sz, args);
192             }
193             break;
194         case OP_XOR:
195         case OP_NOT:
196             todo.append(sz, args);
197             break;
198         case OP_IMPLIES:
199             if (v) {
200                 if (is_true(args[1])) {
201                     todo.push_back(args[1]);
202                 } else if (is_false(args[0])) {
203                     todo.push_back(args[0]);
204                 } else {
205                     IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";);
206                     UNREACHABLE();
207                 }
208             } else {
209                 todo.append(sz, args);
210             }
211             break;
212         default:
213             IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";);
214             UNREACHABLE();
215         }
216     } else {
217         tocollect.push_back(e);
218     }
219 }
220 
collect(ptr_vector<expr> const & formulas,ptr_vector<expr> & tocollect)221 void model_evaluator::collect(ptr_vector<expr> const& formulas, ptr_vector<expr>& tocollect)
222 {
223     ptr_vector<expr> todo;
224     todo.append(formulas);
225     m_visited.reset();
226 
227     VERIFY(check_model(formulas));
228 
229     while (!todo.empty()) {
230         app*  e = to_app(todo.back());
231         todo.pop_back();
232         if (!m_visited.is_marked(e)) {
233             process_formula(e, todo, tocollect);
234             m_visited.mark(e, true);
235         }
236     }
237     m_visited.reset();
238 }
239 
eval_arith(app * e)240 void model_evaluator::eval_arith(app* e)
241 {
242     rational r, r2;
243 
244 #define ARG1 e->get_arg(0)
245 #define ARG2 e->get_arg(1)
246 
247     unsigned arity = e->get_num_args();
248     for (unsigned i = 0; i < arity; ++i) {
249         expr* arg = e->get_arg(i);
250         if (is_x(arg)) {
251             set_x(e);
252             return;
253         }
254         SASSERT(!is_unknown(arg));
255     }
256     switch (e->get_decl_kind()) {
257     case OP_NUM:
258         VERIFY(m_arith.is_numeral(e, r));
259         set_number(e, r);
260         break;
261     case OP_IRRATIONAL_ALGEBRAIC_NUM:
262         set_x(e);
263         break;
264     case OP_LE:
265         set_bool(e, get_number(ARG1) <= get_number(ARG2));
266         break;
267     case OP_GE:
268         set_bool(e, get_number(ARG1) >= get_number(ARG2));
269         break;
270     case OP_LT:
271         set_bool(e, get_number(ARG1) < get_number(ARG2));
272         break;
273     case OP_GT:
274         set_bool(e, get_number(ARG1) > get_number(ARG2));
275         break;
276     case OP_ADD:
277         r = rational::zero();
278         for (unsigned i = 0; i < arity; ++i) {
279             r += get_number(e->get_arg(i));
280         }
281         set_number(e, r);
282         break;
283     case OP_SUB:
284         r = get_number(e->get_arg(0));
285         for (unsigned i = 1; i < arity; ++i) {
286             r -= get_number(e->get_arg(i));
287         }
288         set_number(e, r);
289         break;
290     case OP_UMINUS:
291         SASSERT(arity == 1);
292         set_number(e, -get_number(e->get_arg(0)));
293         break;
294     case OP_MUL:
295         r = rational::one();
296         for (unsigned i = 0; i < arity; ++i) {
297             r *= get_number(e->get_arg(i));
298         }
299         set_number(e, r);
300         break;
301     case OP_DIV:
302         SASSERT(arity == 2);
303         r = get_number(ARG2);
304         if (r.is_zero()) {
305             set_x(e);
306         } else {
307             set_number(e, get_number(ARG1) / r);
308         }
309         break;
310     case OP_IDIV:
311         SASSERT(arity == 2);
312         r = get_number(ARG2);
313         if (r.is_zero()) {
314             set_x(e);
315         } else {
316             set_number(e, div(get_number(ARG1), r));
317         }
318         break;
319     case OP_REM:
320         // rem(v1,v2) = if v2 >= 0 then mod(v1,v2) else -mod(v1,v2)
321         SASSERT(arity == 2);
322         r = get_number(ARG2);
323         if (r.is_zero()) {
324             set_x(e);
325         } else {
326             r2 = mod(get_number(ARG1), r);
327             if (r.is_neg()) { r2.neg(); }
328             set_number(e, r2);
329         }
330         break;
331     case OP_MOD:
332         SASSERT(arity == 2);
333         r = get_number(ARG2);
334         if (r.is_zero()) {
335             set_x(e);
336         } else {
337             set_number(e, mod(get_number(ARG1), r));
338         }
339         break;
340     case OP_TO_REAL:
341         SASSERT(arity == 1);
342         set_number(e, get_number(ARG1));
343         break;
344     case OP_TO_INT:
345         SASSERT(arity == 1);
346         set_number(e, floor(get_number(ARG1)));
347         break;
348     case OP_IS_INT:
349         SASSERT(arity == 1);
350         set_bool(e, get_number(ARG1).is_int());
351         break;
352     case OP_POWER:
353         set_x(e);
354         break;
355     default:
356         IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";);
357         UNREACHABLE();
358         break;
359     }
360 }
361 
inherit_value(expr * e,expr * v)362 void model_evaluator::inherit_value(expr* e, expr* v)
363 {
364     expr* w;
365     SASSERT(!is_unknown(v));
366     SASSERT(e->get_sort() == v->get_sort());
367     if (is_x(v)) {
368         set_x(e);
369     } else if (m.is_bool(e)) {
370         SASSERT(m.is_bool(v));
371         if (is_true(v)) { set_true(e); }
372         else if (is_false(v)) { set_false(e); }
373         else {
374             TRACE("old_spacer", tout << "not inherited:\n" << mk_pp(e, m) << "\n" << mk_pp(v, m) << "\n";);
375             set_x(e);
376         }
377     } else if (m_arith.is_int_real(e)) {
378         set_number(e, get_number(v));
379     } else if (m.is_value(v)) {
380         set_value(e, v);
381     } else if (m_values.find(v, w)) {
382         set_value(e, w);
383     } else {
384         TRACE("old_spacer", tout << "not inherited:\n" << mk_pp(e, m) << "\n" << mk_pp(v, m) << "\n";);
385         set_x(e);
386     }
387 }
388 
eval_exprs(expr_ref_vector & es)389 void model_evaluator::eval_exprs(expr_ref_vector& es)
390 {
391     model_ref mr(m_model);
392     for (unsigned j = 0; j < es.size(); ++j) {
393         if (m_array.is_as_array(es[j].get())) {
394             es[j] = eval(mr, es[j].get());
395         }
396     }
397 }
398 
extract_array_func_interp(expr * a,vector<expr_ref_vector> & stores,expr_ref & else_case)399 bool model_evaluator::extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref& else_case)
400 {
401     SASSERT(m_array.is_array(a));
402 
403     TRACE("old_spacer", tout << mk_pp(a, m) << "\n";);
404     while (m_array.is_store(a)) {
405         expr_ref_vector store(m);
406         store.append(to_app(a)->get_num_args() - 1, to_app(a)->get_args() + 1);
407         eval_exprs(store);
408         stores.push_back(store);
409         a = to_app(a)->get_arg(0);
410     }
411 
412     if (m_array.is_const(a)) {
413         else_case = to_app(a)->get_arg(0);
414         return true;
415     }
416 
417     while (m_array.is_as_array(a)) {
418         func_decl* f = m_array.get_as_array_func_decl(to_app(a));
419         func_interp* g = m_model->get_func_interp(f);
420         unsigned sz = g->num_entries();
421         unsigned arity = f->get_arity();
422         for (unsigned i = 0; i < sz; ++i) {
423             expr_ref_vector store(m);
424             func_entry const* fe = g->get_entry(i);
425             store.append(arity, fe->get_args());
426             store.push_back(fe->get_result());
427             for (unsigned j = 0; j < store.size(); ++j) {
428                 if (!is_ground(store[j].get())) {
429                     TRACE("old_spacer", tout << "could not extract array interpretation: " << mk_pp(a, m) << "\n" << mk_pp(store[j].get(), m) << "\n";);
430                     return false;
431                 }
432             }
433             eval_exprs(store);
434             stores.push_back(store);
435         }
436         else_case = g->get_else();
437         if (!else_case) {
438             TRACE("old_spacer", tout << "no else case " << mk_pp(a, m) << "\n";);
439             return false;
440         }
441         if (!is_ground(else_case)) {
442             TRACE("old_spacer", tout << "non-ground else case " << mk_pp(a, m) << "\n" << mk_pp(else_case, m) << "\n";);
443             return false;
444         }
445         if (m_array.is_as_array(else_case)) {
446             model_ref mr(m_model);
447             else_case = eval(mr, else_case);
448         }
449         TRACE("old_spacer", tout << "else case: " << mk_pp(else_case, m) << "\n";);
450         return true;
451     }
452     TRACE("old_spacer", tout << "no translation: " << mk_pp(a, m) << "\n";);
453 
454     return false;
455 }
456 
457 /**
458    best effort evaluator of extensional array equality.
459 */
eval_array_eq(app * e,expr * arg1,expr * arg2)460 void model_evaluator::eval_array_eq(app* e, expr* arg1, expr* arg2)
461 {
462     TRACE("old_spacer", tout << "array equality: " << mk_pp(e, m) << "\n";);
463     expr_ref v1(m), v2(m);
464     v1 = (*m_model)(arg1);
465     v2 = (*m_model)(arg2);
466     if (v1 == v2) {
467         set_true(e);
468         return;
469     }
470     sort* s = arg1->get_sort();
471     sort* r = get_array_range(s);
472     // give up evaluating finite domain/range arrays
473     if (!r->is_infinite() && !r->is_very_big() && !s->is_infinite() && !s->is_very_big()) {
474         TRACE("old_spacer", tout << "equality is unknown: " << mk_pp(e, m) << "\n";);
475         set_x(e);
476         return;
477     }
478     vector<expr_ref_vector> store;
479     expr_ref else1(m), else2(m);
480     if (!extract_array_func_interp(v1, store, else1) ||
481             !extract_array_func_interp(v2, store, else2)) {
482         TRACE("old_spacer", tout << "equality is unknown: " << mk_pp(e, m) << "\n";);
483         set_x(e);
484         return;
485     }
486 
487     if (else1 != else2) {
488         if (m.is_value(else1) && m.is_value(else2)) {
489             TRACE("old_spacer", tout
490                   << "defaults are different: " << mk_pp(e, m) << " "
491                   << mk_pp(else1, m) << " " << mk_pp(else2, m) << "\n";);
492             set_false(e);
493         } else if (m_array.is_array(else1)) {
494             eval_array_eq(e, else1, else2);
495         } else {
496             TRACE("old_spacer", tout << "equality is unknown: " << mk_pp(e, m) << "\n";);
497             set_x(e);
498         }
499         return;
500     }
501 
502     expr_ref s1(m), s2(m), w1(m), w2(m);
503     expr_ref_vector args1(m), args2(m);
504     args1.push_back(v1);
505     args2.push_back(v2);
506     for (unsigned i = 0; i < store.size(); ++i) {
507         args1.resize(1);
508         args2.resize(1);
509         args1.append(store[i].size() - 1, store[i].data());
510         args2.append(store[i].size() - 1, store[i].data());
511         s1 = m_array.mk_select(args1.size(), args1.data());
512         s2 = m_array.mk_select(args2.size(), args2.data());
513         w1 = (*m_model)(s1);
514         w2 = (*m_model)(s2);
515         if (w1 == w2) {
516             continue;
517         }
518         if (m.is_value(w1) && m.is_value(w2)) {
519             TRACE("old_spacer", tout << "Equality evaluation: " << mk_pp(e, m) << "\n";
520                   tout << mk_pp(s1, m) << " |-> " << mk_pp(w1, m) << "\n";
521                   tout << mk_pp(s2, m) << " |-> " << mk_pp(w2, m) << "\n";);
522             set_false(e);
523         } else if (m_array.is_array(w1)) {
524             eval_array_eq(e, w1, w2);
525             if (is_true(e)) {
526                 continue;
527             }
528         } else {
529             TRACE("old_spacer", tout << "equality is unknown: " << mk_pp(e, m) << "\n";);
530             set_x(e);
531         }
532         return;
533     }
534     set_true(e);
535 }
536 
eval_eq(app * e,expr * arg1,expr * arg2)537 void model_evaluator::eval_eq(app* e, expr* arg1, expr* arg2)
538 {
539     if (arg1 == arg2) {
540         set_true(e);
541     } else if (m_array.is_array(arg1)) {
542         eval_array_eq(e, arg1, arg2);
543     } else if (is_x(arg1) || is_x(arg2)) {
544         set_x(e);
545     } else if (m.is_bool(arg1)) {
546         bool val = is_true(arg1) == is_true(arg2);
547         SASSERT(val == (is_false(arg1) == is_false(arg2)));
548         if (val) {
549             set_true(e);
550         } else {
551             set_false(e);
552         }
553     } else if (m_arith.is_int_real(arg1)) {
554         set_bool(e, get_number(arg1) == get_number(arg2));
555     } else {
556         expr* e1 = get_value(arg1);
557         expr* e2 = get_value(arg2);
558         if (m.is_value(e1) && m.is_value(e2)) {
559             set_bool(e, e1 == e2);
560         } else if (e1 == e2) {
561             set_bool(e, true);
562         } else {
563             TRACE("old_spacer", tout << "not value equal:\n" << mk_pp(e1, m) << "\n" << mk_pp(e2, m) << "\n";);
564             set_x(e);
565         }
566     }
567 }
568 
eval_basic(app * e)569 void model_evaluator::eval_basic(app* e)
570 {
571     expr* arg1, *arg2;
572     expr *argCond, *argThen, *argElse, *arg;
573     bool has_x = false;
574     unsigned arity = e->get_num_args();
575     switch (e->get_decl_kind()) {
576     case OP_AND:
577         for (unsigned j = 0; j < arity; ++j) {
578             expr * arg = e->get_arg(j);
579             if (is_false(arg)) {
580                 set_false(e);
581                 return;
582             } else if (is_x(arg)) {
583                 has_x = true;
584             } else {
585                 SASSERT(is_true(arg));
586             }
587         }
588         if (has_x) {
589             set_x(e);
590         } else {
591             set_true(e);
592         }
593         break;
594     case OP_OR:
595         for (unsigned j = 0; j < arity; ++j) {
596             expr * arg = e->get_arg(j);
597             if (is_true(arg)) {
598                 set_true(e);
599                 return;
600             } else if (is_x(arg)) {
601                 has_x = true;
602             } else {
603                 SASSERT(is_false(arg));
604             }
605         }
606         if (has_x) {
607             set_x(e);
608         } else {
609             set_false(e);
610         }
611         break;
612     case OP_NOT:
613         VERIFY(m.is_not(e, arg));
614         if (is_true(arg)) {
615             set_false(e);
616         } else if (is_false(arg)) {
617             set_true(e);
618         } else {
619             SASSERT(is_x(arg));
620             set_x(e);
621         }
622         break;
623     case OP_IMPLIES:
624         VERIFY(m.is_implies(e, arg1, arg2));
625         if (is_false(arg1) || is_true(arg2)) {
626             set_true(e);
627         } else if (arg1 == arg2) {
628             set_true(e);
629         } else if (is_true(arg1) && is_false(arg2)) {
630             set_false(e);
631         } else {
632             SASSERT(is_x(arg1) || is_x(arg2));
633             set_x(e);
634         }
635         break;
636     case OP_XOR:
637         VERIFY(m.is_xor(e, arg1, arg2));
638         eval_eq(e, arg1, arg2);
639         if (is_false(e)) { set_true(e); }
640         else if (is_true(e)) { set_false(e); }
641         break;
642     case OP_ITE:
643         VERIFY(m.is_ite(e, argCond, argThen, argElse));
644         if (is_true(argCond)) {
645             inherit_value(e, argThen);
646         } else if (is_false(argCond)) {
647             inherit_value(e, argElse);
648         } else if (argThen == argElse) {
649             inherit_value(e, argThen);
650         } else if (m.is_bool(e)) {
651             SASSERT(is_x(argCond));
652             if (is_x(argThen) || is_x(argElse)) {
653                 set_x(e);
654             } else if (is_true(argThen) == is_true(argElse)) {
655                 inherit_value(e, argThen);
656             } else {
657                 set_x(e);
658             }
659         } else {
660             set_x(e);
661         }
662         break;
663     case OP_TRUE:
664         set_true(e);
665         break;
666     case OP_FALSE:
667         set_false(e);
668         break;
669     case OP_EQ:
670         VERIFY(m.is_eq(e, arg1, arg2));
671         eval_eq(e, arg1, arg2);
672         break;
673     case OP_DISTINCT: {
674         vector<rational> values;
675         for (unsigned i = 0; i < arity; ++i) {
676             expr* arg = e->get_arg(i);
677             if (is_x(arg)) {
678                 set_x(e);
679                 return;
680             }
681             values.push_back(get_number(arg));
682         }
683         std::sort(values.begin(), values.end());
684         for (unsigned i = 0; i + 1 < values.size(); ++i) {
685             if (values[i] == values[i + 1]) {
686                 set_false(e);
687                 return;
688             }
689         }
690         set_true(e);
691         break;
692     }
693     default:
694         IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";);
695         UNREACHABLE();
696     }
697 }
698 
eval_fmls(ptr_vector<expr> const & formulas)699 void model_evaluator::eval_fmls(ptr_vector<expr> const& formulas)
700 {
701     ptr_vector<expr> todo(formulas);
702 
703     while (!todo.empty()) {
704         expr * curr_e = todo.back();
705 
706         if (!is_app(curr_e)) {
707             todo.pop_back();
708             continue;
709         }
710         app * curr = to_app(curr_e);
711 
712         if (!is_unknown(curr)) {
713             todo.pop_back();
714             continue;
715         }
716         unsigned arity = curr->get_num_args();
717         for (unsigned i = 0; i < arity; ++i) {
718             if (is_unknown(curr->get_arg(i))) {
719                 todo.push_back(curr->get_arg(i));
720             }
721         }
722         if (todo.back() != curr) {
723             continue;
724         }
725         todo.pop_back();
726         if (curr->get_family_id() == m_arith.get_family_id()) {
727             eval_arith(curr);
728         } else if (curr->get_family_id() == m.get_basic_family_id()) {
729             eval_basic(curr);
730         } else {
731             expr_ref vl(m);
732             vl = eval(m_model, curr);
733             assign_value(curr, vl);
734         }
735 
736         IF_VERBOSE(35, verbose_stream() << "assigned " << mk_pp(curr_e, m)
737                    << (is_true(curr_e) ? "true" : is_false(curr_e) ? "false" : "unknown") << "\n";);
738         SASSERT(!is_unknown(curr));
739     }
740 }
741 
check_model(ptr_vector<expr> const & formulas)742 bool model_evaluator::check_model(ptr_vector<expr> const& formulas)
743 {
744     eval_fmls(formulas);
745     bool has_x = false;
746     for (unsigned i = 0; i < formulas.size(); ++i) {
747         expr * form = formulas[i];
748         SASSERT(!is_unknown(form));
749         TRACE("spacer_verbose",
750               tout << "formula is " << (is_true(form) ? "true" : is_false(form) ? "false" : "unknown") << "\n" << mk_pp(form, m) << "\n";);
751 
752         if (is_false(form)) {
753             IF_VERBOSE(0, verbose_stream() << "formula false in model: " << mk_pp(form, m) << "\n";);
754             UNREACHABLE();
755         }
756         if (is_x(form)) {
757             IF_VERBOSE(0, verbose_stream() << "formula undetermined in model: " << mk_pp(form, m) << "\n";);
758             TRACE("old_spacer", model_smt2_pp(tout, m, *m_model, 0););
759             has_x = true;
760         }
761     }
762     return !has_x;
763 }
764 
eval_heavy(const model_ref & model,expr * fml)765 expr_ref model_evaluator::eval_heavy(const model_ref& model, expr* fml)
766 {
767     expr_ref result(model->get_manager());
768 
769     setup_model(model);
770     ptr_vector<expr> fmls;
771     fmls.push_back(fml);
772     eval_fmls(fmls);
773     if (is_false(fml)) {
774         result = m.mk_false();
775     } else if (is_true(fml) || is_x(fml)) {
776         result = m.mk_true();
777     } else if (m_arith.is_int_real(fml)) {
778         result = m_arith.mk_numeral(get_number(fml), m_arith.is_int(fml));
779     } else {
780         result = get_value(fml);
781     }
782     reset();
783 
784     return result;
785 }
786 
eval(const model_ref & model,func_decl * d)787 expr_ref model_evaluator::eval(const model_ref& model, func_decl* d)
788 {
789     SASSERT(d->get_arity() == 0);
790     expr_ref result(m);
791     if (m_array.is_array(d->get_range())) {
792         expr_ref e(m);
793         e = m.mk_const(d);
794         result = eval(model, e);
795     } else {
796         result = model->get_const_interp(d);
797     }
798     return result;
799 }
800 
eval(const model_ref & model,expr * e)801 expr_ref model_evaluator::eval(const model_ref& model, expr* e){
802     m_model = model.get();
803     model::scoped_model_completion _scm(m_model, true);
804     expr_ref result = (*m_model)(e);
805     if (m_array.is_array(e)) {
806         vector<expr_ref_vector> stores;
807         expr_ref_vector args(m);
808         expr_ref else_case(m);
809         if (extract_array_func_interp(result, stores, else_case)) {
810             result = m_array.mk_const_array(e->get_sort(), else_case);
811             while (!stores.empty() && stores.back().back() == else_case) {
812                 stores.pop_back();
813             }
814             for (unsigned i = stores.size(); i > 0;) {
815                 --i;
816                 args.resize(1);
817                 args[0] = result;
818                 args.append(stores[i]);
819                 result = m_array.mk_store(args);
820             }
821             return result;
822         }
823     }
824     return result;
825 }
826 
827 
828 }
829