Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Public Member Functions | Friends
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
 
solveroperator= (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
 
- Public Member Functions inherited from object
 object (context &c)
 
 object (object const &s)
 
contextctx () const
 
void check_error () const
 

Friends

std::ostream & operator<< (std::ostream &out, solver const &s)
 

Additional Inherited Members

- Protected Attributes inherited from object
contextm_ctx
 

Detailed Description

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

Constructor & Destructor Documentation

solver ( context c)
inline

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

:object(c) { init(Z3_mk_solver(c)); }
solver ( context c,
Z3_solver  s 
)
inline

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

:object(c) { init(s); }
solver ( context c,
char const *  logic 
)
inline

Definition at line 1160 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 1161 of file z3++.h.

:object(s) { init(s.m_solver); }
~solver ( )
inline

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

{ Z3_solver_dec_ref(ctx(), m_solver); }

Member Function Documentation

void add ( expr const &  e)
inline

Definition at line 1175 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 1176 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);
}
void add ( expr const &  e,
char const *  p 
)
inline

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

{
add(e, ctx().bool_const(p));
}
expr_vector assertions ( ) const
inline

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

{ 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 1184 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 1185 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());
return to_check_result(r);
}
check_result check ( expr_vector  assumptions)
inline

Definition at line 1195 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());
return to_check_result(r);
}
model get_model ( ) const
inline

Definition at line 1206 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 1163 of file z3++.h.

{ return m_solver; }
solver& operator= ( solver const &  s)
inline

Definition at line 1164 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 1173 of file z3++.h.

{ Z3_solver_pop(ctx(), m_solver, n); check_error(); }
expr proof ( ) const
inline

Definition at line 1211 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 1172 of file z3++.h.

{ Z3_solver_push(ctx(), m_solver); check_error(); }
std::string reason_unknown ( ) const
inline

Definition at line 1207 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 1174 of file z3++.h.

{ Z3_solver_reset(ctx(), m_solver); check_error(); }
void set ( params const &  p)
inline

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

{ Z3_solver_set_params(ctx(), m_solver, p); check_error(); }
stats statistics ( ) const
inline

Definition at line 1208 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 1209 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 1212 of file z3++.h.

{ out << Z3_solver_to_string(s.ctx(), s); return out; }