1
2 /*++
3 Copyright (c) 2015 Microsoft Corporation
4
5 --*/
6
7
8 #include "ast/ast.h"
9 #include "smt/params/smt_params.h"
10 #include "smt/smt_context.h"
11 #include "ast/arith_decl_plugin.h"
12 #include "ast/bv_decl_plugin.h"
13 #include "ast/array_decl_plugin.h"
14 #include "model/model_v2_pp.h"
15 #include "ast/reg_decl_plugins.h"
16
tst_model_retrieval()17 void tst_model_retrieval()
18 {
19 memory::initialize(0);
20 smt_params params;
21 params.m_model = true;
22
23
24 ast_manager m;
25 reg_decl_plugins(m);
26
27 family_id array_fid = m.mk_family_id(symbol("array"));
28 array_util au(m);
29
30 // arr_s and select_fn creation copy-pasted from z3.cpp
31
32 parameter sparams[2] = { parameter(to_sort(m.mk_bool_sort())), parameter(to_sort(m.mk_bool_sort())) };
33 sort_ref arr_s(m.mk_sort(array_fid, ARRAY_SORT, 2, sparams), m);
34
35 sort * domain2[2] = {arr_s, m.mk_bool_sort()};
36 func_decl_ref select_fn(
37 m.mk_func_decl(array_fid, OP_SELECT, 2, arr_s->get_parameters(), 2, domain2), m);
38
39
40 app_ref a1(m.mk_const(symbol("a1"), arr_s), m);
41 app_ref a2(m.mk_const(symbol("a2"), arr_s), m);
42
43 // (= true (select a1 true))
44 app_ref fml(m.mk_eq(m.mk_true(),
45 m.mk_app(select_fn.get(), a1, m.mk_true())), m);
46
47 smt::context ctx(m, params);
48 ctx.assert_expr(fml);
49 lbool check_result = ctx.check();
50 std::cout<<((check_result==l_true) ? "satisfiable" :
51 (check_result==l_false) ? "unsatisfiable" : "unknown")<<"\n";
52 ref<model> model;
53 ctx.get_model(model);
54 model_v2_pp(std::cout, *model, false);
55 expr_ref a1_val(model->get_const_interp(a1->get_decl()), m);
56
57 app_ref fml2(m.mk_eq(a2, a1_val), m);
58 ctx.assert_expr(fml2);
59 std::cout<<"--------------------------\n";
60 ctx.display(std::cout);
61 std::cout<<"--------------------------\n";
62 check_result = ctx.check();
63 ctx.display(std::cout);
64 std::cout<<"--------------------------\n";
65 std::cout<<((check_result==l_true) ? "satisfiable" :
66 (check_result==l_false) ? "unsatisfiable" : "unknown")<<"\n";
67 }
68