1 #include "ast/reg_decl_plugins.h"
2 #include "solver/solver_pool.h"
3 #include "smt/smt_solver.h"
4
5
tst_cube_clause()6 void tst_cube_clause() {
7 ast_manager m;
8 reg_decl_plugins(m);
9 params_ref p;
10 lbool r;
11 ref<solver> solver = mk_smt_solver(m, p, symbol::null);
12
13 expr_ref a(m.mk_const(symbol("a"), m.mk_bool_sort()), m);
14 expr_ref b(m.mk_const(symbol("b"), m.mk_bool_sort()), m);
15 expr_ref c(m.mk_const(symbol("c"), m.mk_bool_sort()), m);
16 expr_ref d(m.mk_const(symbol("d"), m.mk_bool_sort()), m);
17 expr_ref e(m.mk_const(symbol("e"), m.mk_bool_sort()), m);
18 expr_ref f(m.mk_const(symbol("f"), m.mk_bool_sort()), m);
19 expr_ref g(m.mk_const(symbol("g"), m.mk_bool_sort()), m);
20 expr_ref fml(m);
21 fml = m.mk_not(m.mk_and(a, b));
22 solver->assert_expr(fml);
23 fml = m.mk_not(m.mk_and(c, d));
24 solver->assert_expr(fml);
25 fml = m.mk_not(m.mk_and(e, f));
26 solver->assert_expr(fml);
27 expr_ref_vector cube(m), clause(m), core(m);
28 r = solver->check_sat(cube);
29 std::cout << r << "\n";
30 cube.push_back(a);
31 r = solver->check_sat(cube);
32 std::cout << r << "\n";
33 cube.push_back(c);
34 cube.push_back(e);
35 r = solver->check_sat(cube);
36 std::cout << r << "\n";
37 clause.push_back(b);
38 vector<expr_ref_vector> clauses;
39 clauses.push_back(clause);
40 r = solver->check_sat_cc(cube, clauses);
41 std::cout << r << "\n";
42 core.reset();
43 solver->get_unsat_core(core);
44 std::cout << core << "\n";
45 clause.push_back(d);
46 clauses.reset();
47 clauses.push_back(clause);
48 r = solver->check_sat_cc(cube, clauses);
49 std::cout << r << "\n";
50 core.reset();
51 solver->get_unsat_core(core);
52 std::cout << core << "\n";
53 clause.push_back(f);
54 clauses.reset();
55 clauses.push_back(clause);
56 r = solver->check_sat_cc(cube, clauses);
57 std::cout << r << "\n";
58 core.reset();
59 solver->get_unsat_core(core);
60 std::cout << core << "\n";
61 clause.push_back(g);
62 clauses.reset();
63 clauses.push_back(clause);
64 r = solver->check_sat_cc(cube, clauses);
65 std::cout << r << "\n";
66 }
67