1
2 /*++
3 Copyright (c) 2015 Microsoft Corporation
4
5 --*/
6
7 #include "smt/smt_context.h"
8 #include "ast/reg_decl_plugins.h"
9
tst_smt_context()10 void tst_smt_context()
11 {
12 smt_params params;
13
14 ast_manager m;
15 reg_decl_plugins(m);
16
17 smt::context ctx(m, params);
18
19 app_ref a1(m.mk_const(symbol("a"), m.mk_bool_sort()), m);
20 app_ref b1(m.mk_const(symbol("b"), m.mk_bool_sort()), m);
21 app_ref c1(m.mk_const(symbol("c"), m.mk_bool_sort()), m);
22 app_ref na1(m.mk_not(a1), m);
23 ctx.assert_expr(na1);
24
25 app_ref b_or_c(m.mk_or(c1.get(), b1.get()), m);
26 ctx.assert_expr(b_or_c);
27
28 {
29 app_ref nc(m.mk_not(c1), m);
30 ptr_vector<expr> assumptions;
31 assumptions.push_back(nc.get());
32
33 ctx.check(assumptions.size(), assumptions.data());
34 }
35
36 ctx.check();
37 }
38