1 #include "model/model.h"
2 #include "model/model_evaluator.h"
3 #include "model/model_pp.h"
4 #include "ast/arith_decl_plugin.h"
5 #include "ast/reg_decl_plugins.h"
6 #include "ast/ast_pp.h"
7
8
tst_model_evaluator()9 void tst_model_evaluator() {
10 ast_manager m;
11 reg_decl_plugins(m);
12 arith_util a(m);
13
14 model mdl(m);
15
16 sort* sI = a.mk_int();
17
18 sort* dom[2] = { sI, m.mk_bool_sort() };
19 func_decl_ref f(m.mk_func_decl(symbol("f"), 2, dom, sI), m);
20 func_decl_ref g(m.mk_func_decl(symbol("g"), 2, dom, sI), m);
21 func_decl_ref h(m.mk_func_decl(symbol("h"), 2, dom, sI), m);
22 func_decl_ref F(m.mk_func_decl(symbol("F"), 2, dom, sI), m);
23 func_decl_ref G(m.mk_func_decl(symbol("G"), 2, dom, sI), m);
24 expr_ref vI0(m.mk_var(0, sI), m);
25 expr_ref vI1(m.mk_var(1, sI), m);
26 expr_ref vB0(m.mk_var(0, m.mk_bool_sort()), m);
27 expr_ref vB1(m.mk_var(1, m.mk_bool_sort()), m);
28 expr_ref vB2(m.mk_var(2, m.mk_bool_sort()), m);
29 expr* vI0p = vI0.get();
30 expr* vI1p = vI1.get();
31 expr* vB1p = vB1.get();
32 expr* vB2p = vB2.get();
33
34 expr_ref f01(m.mk_app(f, vI0p, vB1p), m);
35 expr_ref g01(m.mk_app(g, vI0p, vB1p), m);
36 expr_ref h01(m.mk_app(h, vI0p, vB1p), m);
37 func_interp* fi = alloc(func_interp, m, 2);
38 func_interp* gi = alloc(func_interp, m, 2);
39 func_interp* hi = alloc(func_interp, m, 2);
40 hi->set_else(m.mk_ite(vB1p, m.mk_app(f, vI0p, vB1p), m.mk_app(g, vI0p, vB1p)));
41 mdl.register_decl(h, hi);
42
43
44 model_evaluator eval(mdl);
45
46 expr_ref e(m), v(m);
47
48 {
49 symbol nI("N");
50 fi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0p, m.mk_app(F, vI1p, vB2p))), vI0p, a.mk_int(1)));
51 gi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0p, m.mk_app(G, vI1p, vB2p))), a.mk_int(2), vI0p));
52 mdl.register_decl(g, gi);
53 mdl.register_decl(f, fi);
54 model_pp(std::cout, mdl);
55 e = m.mk_app(h, vI0p, vB1p);
56 eval(e, v);
57 std::cout << e << " " << v << "\n";
58 }
59
60 {
61 fi->set_else(m.mk_app(F, vI0p, vB1p));
62 gi->set_else(m.mk_app(G, vI0p, vB1p));
63 model_pp(std::cout, mdl);
64 e = m.mk_app(h, vI0p, vB1p);
65 eval(e, v);
66 std::cout << e << " " << v << "\n";
67 }
68
69 }
70