Public Member Functions | |
solver (context &c) | |
solver (context &c, Z3_solver s) | |
solver (context &c, char const *logic) | |
solver (solver const &s) | |
~solver () | |
operator Z3_solver () const | |
solver & | operator= (solver const &s) |
void | set (params const &p) |
void | push () |
void | pop (unsigned n=1) |
void | reset () |
void | add (expr const &e) |
void | add (expr const &e, expr const &p) |
void | add (expr const &e, char const *p) |
check_result | check () |
check_result | check (unsigned n, expr *const assumptions) |
check_result | check (expr_vector assumptions) |
model | get_model () const |
std::string | reason_unknown () const |
stats | statistics () const |
expr_vector | unsat_core () const |
expr_vector | assertions () const |
expr | proof () const |
Friends | |
std::ostream & | operator<< (std::ostream &out, solver const &s) |
Definition at line 1262 of file z3++.h.
:object(c) { init(Z3_mk_solver(c)); }
Definition at line 1264 of file z3++.h.
:object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); }
~solver | ( | ) | [inline] |
Definition at line 1266 of file z3++.h.
{ Z3_solver_dec_ref(ctx(), m_solver); }
Definition at line 1279 of file z3++.h.
Referenced by solver::add().
{ assert(e.is_bool()); Z3_solver_assert(ctx(), m_solver, e); check_error(); }
Definition at line 1280 of file z3++.h.
{ assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const()); Z3_solver_assert_and_track(ctx(), m_solver, e, p); check_error(); }
expr_vector assertions | ( | ) | const [inline] |
Definition at line 1314 of file z3++.h.
Referenced by Solver::to_smt2().
{ Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
check_result check | ( | ) | [inline] |
Definition at line 1288 of file z3++.h.
{ Z3_lbool r = Z3_solver_check(ctx(), m_solver); check_error(); return to_check_result(r); }
check_result check | ( | unsigned | n, |
expr *const | assumptions | ||
) | [inline] |
Definition at line 1289 of file z3++.h.
{ array<Z3_ast> _assumptions(n); for (unsigned i = 0; i < n; i++) { check_context(*this, assumptions[i]); _assumptions[i] = assumptions[i]; } Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr()); check_error(); return to_check_result(r); }
check_result check | ( | expr_vector | assumptions | ) | [inline] |
Definition at line 1299 of file z3++.h.
{ unsigned n = assumptions.size(); array<Z3_ast> _assumptions(n); for (unsigned i = 0; i < n; i++) { check_context(*this, assumptions[i]); _assumptions[i] = assumptions[i]; } Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr()); check_error(); return to_check_result(r); }
Definition at line 1310 of file z3++.h.
{ Z3_model m = Z3_solver_get_model(ctx(), m_solver); check_error(); return model(ctx(), m); }
Definition at line 1268 of file z3++.h.
{ Z3_solver_inc_ref(s.ctx(), s.m_solver); Z3_solver_dec_ref(ctx(), m_solver); m_ctx = s.m_ctx; m_solver = s.m_solver; return *this; }
void pop | ( | unsigned | n = 1 | ) | [inline] |
Definition at line 1277 of file z3++.h.
{ Z3_solver_pop(ctx(), m_solver, n); check_error(); }
Definition at line 1315 of file z3++.h.
{ Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
void push | ( | ) | [inline] |
Definition at line 1276 of file z3++.h.
{ Z3_solver_push(ctx(), m_solver); check_error(); }
std::string reason_unknown | ( | ) | const [inline] |
Definition at line 1311 of file z3++.h.
{ Z3_string r = Z3_solver_get_reason_unknown(ctx(), m_solver); check_error(); return r; }
void reset | ( | ) | [inline] |
Definition at line 1278 of file z3++.h.
{ Z3_solver_reset(ctx(), m_solver); check_error(); }
Definition at line 1275 of file z3++.h.
{ Z3_solver_set_params(ctx(), m_solver, p); check_error(); }
stats statistics | ( | ) | const [inline] |
Definition at line 1312 of file z3++.h.
{ Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); }
expr_vector unsat_core | ( | ) | const [inline] |
Definition at line 1313 of file z3++.h.
{ Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
std::ostream& operator<< | ( | std::ostream & | out, |
solver const & | s | ||
) | [friend] |
Definition at line 1316 of file z3++.h.
{ out << Z3_solver_to_string(s.ctx(), s); return out; }