solver Class Reference

Inheritance diagram for solver:

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)

---

Detailed Description

Definition at line 1255 of file z3++.h.

---

Constructor & Destructor Documentation

solver

(

context &

c

)

[inline]

Definition at line 1262 of file z3++.h.

:object(c) { init(Z3_mk_solver(c)); }

solver	(	context &	c,
		Z3_solver	s
	)		[inline]

Definition at line 1263 of file z3++.h.

:object(c) { init(s); }

solver	(	context &	c,
		char const *	logic
	)		[inline]

Definition at line 1264 of file z3++.h.

:object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); }

solver

(

solver const &

s

)

[inline]

Definition at line 1265 of file z3++.h.

:object(s) { init(s.m_solver); }

~solver

(

)

[inline]

Definition at line 1266 of file z3++.h.

{ Z3_solver_dec_ref(ctx(), m_solver); }

---

Member Function Documentation

void add

(

expr const &

e

)

[inline]

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(); }

void add	(	expr const &	e,
		expr const &	p
	)		[inline]

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(); 
        }

void add	(	expr const &	e,
		char const *	p
	)		[inline]

Definition at line 1285 of file z3++.h.

                                                 {
            add(e, ctx().bool_const(p));
        }

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); 
        }

model get_model

(

)

const [inline]

Definition at line 1310 of file z3++.h.

{ Z3_model m = Z3_solver_get_model(ctx(), m_solver); check_error(); return model(ctx(), m); }

operator Z3_solver

(

)

const [inline]

Definition at line 1267 of file z3++.h.

{ return m_solver; }

solver& operator=

(

solver const &

s

)

[inline]

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(); }

expr proof

(

)

const [inline]

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(); }

void set

(

params const &

p

)

[inline]

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); }

---

Friends And Related Function Documentation

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; }