1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 solver_na2as.cpp
7
8 Abstract:
9
10 Solver that implements "named" assertions using assumptions (aka answer literals).
11 That is, a named assertion assert_expr(t, a) is mapped into
12 a implies t
13 and 'a' is used as an extra assumption for check_sat.
14
15 Author:
16
17 Leonardo (leonardo) 2012-11-02
18
19 Notes:
20
21 --*/
22 #include "solver/solver_na2as.h"
23 #include "ast/ast_smt2_pp.h"
24
25
solver_na2as(ast_manager & m)26 solver_na2as::solver_na2as(ast_manager & m):
27 m(m),
28 m_assumptions(m) {
29 }
30
~solver_na2as()31 solver_na2as::~solver_na2as() {}
32
assert_expr_core2(expr * t,expr * a)33 void solver_na2as::assert_expr_core2(expr * t, expr * a) {
34 if (a == nullptr) {
35 assert_expr_core(t);
36 }
37 else {
38 SASSERT(is_uninterp_const(a));
39 SASSERT(m.is_bool(a));
40 TRACE("solver_na2as", tout << "asserting\n" << mk_ismt2_pp(t, m) << "\n" << mk_ismt2_pp(a, m) << "\n";);
41 m_assumptions.push_back(a);
42 expr_ref new_t(m);
43 new_t = m.mk_implies(a, t);
44 assert_expr_core(new_t);
45 }
46 }
47
48 struct append_assumptions {
49 expr_ref_vector & m_assumptions;
50 unsigned m_old_sz;
append_assumptionsappend_assumptions51 append_assumptions(expr_ref_vector & _m_assumptions,
52 unsigned num_assumptions,
53 expr * const * assumptions):
54 m_assumptions(_m_assumptions) {
55 m_old_sz = m_assumptions.size();
56 m_assumptions.append(num_assumptions, assumptions);
57 }
58
~append_assumptionsappend_assumptions59 ~append_assumptions() {
60 m_assumptions.shrink(m_old_sz);
61 }
62 };
63
check_sat_core(unsigned num_assumptions,expr * const * assumptions)64 lbool solver_na2as::check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
65 append_assumptions app(m_assumptions, num_assumptions, assumptions);
66 TRACE("solver_na2as", display(tout););
67 return check_sat_core2(m_assumptions.size(), m_assumptions.data());
68 }
69
check_sat_cc(const expr_ref_vector & assumptions,vector<expr_ref_vector> const & clauses)70 lbool solver_na2as::check_sat_cc(const expr_ref_vector &assumptions, vector<expr_ref_vector> const &clauses) {
71 if (clauses.empty()) return check_sat(assumptions.size(), assumptions.data());
72 append_assumptions app(m_assumptions, assumptions.size(), assumptions.data());
73 return check_sat_cc_core(m_assumptions, clauses);
74 }
75
get_consequences(expr_ref_vector const & asms,expr_ref_vector const & vars,expr_ref_vector & consequences)76 lbool solver_na2as::get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
77 append_assumptions app(m_assumptions, asms.size(), asms.data());
78 return get_consequences_core(m_assumptions, vars, consequences);
79 }
80
find_mutexes(expr_ref_vector const & vars,vector<expr_ref_vector> & mutexes)81 lbool solver_na2as::find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
82 return l_true;
83 }
84
85
push()86 void solver_na2as::push() {
87 unsigned n = m_assumptions.size();
88 push_core();
89 m_scopes.push_back(n);
90 }
91
pop(unsigned n)92 void solver_na2as::pop(unsigned n) {
93 if (n > 0 && !m_scopes.empty()) {
94 unsigned lvl = m_scopes.size();
95 n = std::min(lvl, n);
96 pop_core(n);
97 unsigned new_lvl = lvl - n;
98 restore_assumptions(m_scopes[new_lvl]);
99 m_scopes.shrink(new_lvl);
100 }
101 }
102
restore_assumptions(unsigned old_sz)103 void solver_na2as::restore_assumptions(unsigned old_sz) {
104 m_assumptions.shrink(old_sz);
105 }
106
get_scope_level() const107 unsigned solver_na2as::get_scope_level() const {
108 return m_scopes.size();
109 }
110
111