Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules 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 1255 of file z3++.h.

Constructor & Destructor Documentation

solver ( context c)
inline

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

1262 :object(c) { init(Z3_mk_solver(c)); }
object(context &c)
Definition: z3++.h:270
Z3_solver Z3_API Z3_mk_solver(__in Z3_context c)
Create a new (incremental) solver. This solver also uses a set of builtin tactics for handling the fi...
solver ( context c,
Z3_solver  s 
)
inline

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

1263 :object(c) { init(s); }
object(context &c)
Definition: z3++.h:270
solver ( context c,
char const *  logic 
)
inline

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

1264 :object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); }
Z3_solver Z3_API Z3_mk_solver_for_logic(__in Z3_context c, __in Z3_symbol logic)
Create a new solver customized for the given logic. It behaves like Z3_mk_solver if the logic is unkn...
object(context &c)
Definition: z3++.h:270
solver ( solver const &  s)
inline

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

1265 :object(s) { init(s.m_solver); }
object(context &c)
Definition: z3++.h:270
~solver ( )
inline

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

1266 { Z3_solver_dec_ref(ctx(), m_solver); }
void Z3_API Z3_solver_dec_ref(__in Z3_context c, __in Z3_solver s)
Decrement the reference counter of the given solver.
context & ctx() const
Definition: z3++.h:272

Member Function Documentation

void add ( expr const &  e)
inline

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

Referenced by solver::add().

1279 { assert(e.is_bool()); Z3_solver_assert(ctx(), m_solver, e); check_error(); }
void Z3_API Z3_solver_assert(__in Z3_context c, __in Z3_solver s, __in Z3_ast a)
Assert a constraint into the solver.
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
void add ( expr const &  e,
expr const &  p 
)
inline

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

1280  {
1281  assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const());
1282  Z3_solver_assert_and_track(ctx(), m_solver, e, p);
1283  check_error();
1284  }
void Z3_API Z3_solver_assert_and_track(__in Z3_context c, __in Z3_solver s, __in Z3_ast a, __in Z3_ast p)
Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant p...
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
void add ( expr const &  e,
char const *  p 
)
inline

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

1285  {
1286  add(e, ctx().bool_const(p));
1287  }
context & ctx() const
Definition: z3++.h:272
void add(expr const &e)
Definition: z3++.h:1279
expr_vector assertions ( ) const
inline

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

Referenced by Solver::to_smt2().

1314 { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
Z3_ast_vector Z3_API Z3_solver_get_assertions(__in Z3_context c, __in Z3_solver s)
Return the set of asserted formulas as a goal object.
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:68
check_result check ( )
inline

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

1288 { Z3_lbool r = Z3_solver_check(ctx(), m_solver); check_error(); return to_check_result(r); }
Z3_lbool Z3_API Z3_solver_check(__in Z3_context c, __in Z3_solver s)
Check whether the assertions in a given solver are consistent or not.
context & ctx() const
Definition: z3++.h:272
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:135
void check_error() const
Definition: z3++.h:273
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:1249
check_result check ( unsigned  n,
expr *const  assumptions 
)
inline

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

1289  {
1290  array<Z3_ast> _assumptions(n);
1291  for (unsigned i = 0; i < n; i++) {
1292  check_context(*this, assumptions[i]);
1293  _assumptions[i] = assumptions[i];
1294  }
1295  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
1296  check_error();
1297  return to_check_result(r);
1298  }
context & ctx() const
Definition: z3++.h:272
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:135
void check_error() const
Definition: z3++.h:273
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:1249
Z3_lbool Z3_API Z3_solver_check_assumptions(__in Z3_context c, __in Z3_solver s, __in unsigned num_assumptions, __in_ecount(num_assumptions) Z3_ast const assumptions[])
Check whether the assertions in the given solver and optional assumptions are consistent or not...
check_result check ( expr_vector  assumptions)
inline

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

1299  {
1300  unsigned n = assumptions.size();
1301  array<Z3_ast> _assumptions(n);
1302  for (unsigned i = 0; i < n; i++) {
1303  check_context(*this, assumptions[i]);
1304  _assumptions[i] = assumptions[i];
1305  }
1306  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
1307  check_error();
1308  return to_check_result(r);
1309  }
context & ctx() const
Definition: z3++.h:272
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:135
void check_error() const
Definition: z3++.h:273
friend void check_context(object const &a, object const &b)
Definition: z3++.h:276
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:1249
Z3_lbool Z3_API Z3_solver_check_assumptions(__in Z3_context c, __in Z3_solver s, __in unsigned num_assumptions, __in_ecount(num_assumptions) Z3_ast const assumptions[])
Check whether the assertions in the given solver and optional assumptions are consistent or not...
model get_model ( ) const
inline

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

1310 { Z3_model m = Z3_solver_get_model(ctx(), m_solver); check_error(); return model(ctx(), m); }
Z3_model Z3_API Z3_solver_get_model(__in Z3_context c, __in Z3_solver s)
Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions.
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
operator Z3_solver ( ) const
inline

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

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

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

1268  {
1269  Z3_solver_inc_ref(s.ctx(), s.m_solver);
1270  Z3_solver_dec_ref(ctx(), m_solver);
1271  m_ctx = s.m_ctx;
1272  m_solver = s.m_solver;
1273  return *this;
1274  }
void Z3_API Z3_solver_dec_ref(__in Z3_context c, __in Z3_solver s)
Decrement the reference counter of the given solver.
void Z3_API Z3_solver_inc_ref(__in Z3_context c, __in Z3_solver s)
Increment the reference counter of the given solver.
context & ctx() const
Definition: z3++.h:272
context * m_ctx
Definition: z3++.h:268
void pop ( unsigned  n = 1)
inline

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

1277 { Z3_solver_pop(ctx(), m_solver, n); check_error(); }
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
void Z3_API Z3_solver_pop(__in Z3_context c, __in Z3_solver s, unsigned n)
Backtrack n backtracking points.
expr proof ( ) const
inline

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

1315 { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
Z3_ast Z3_API Z3_solver_get_proof(__in Z3_context c, __in Z3_solver s)
Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions.
void push ( )
inline

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

1276 { Z3_solver_push(ctx(), m_solver); check_error(); }
context & ctx() const
Definition: z3++.h:272
void Z3_API Z3_solver_push(__in Z3_context c, __in Z3_solver s)
Create a backtracking point.
void check_error() const
Definition: z3++.h:273
std::string reason_unknown ( ) const
inline

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

1311 { Z3_string r = Z3_solver_get_reason_unknown(ctx(), m_solver); check_error(); return r; }
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
Z3_string Z3_API Z3_solver_get_reason_unknown(__in Z3_context c, __in Z3_solver s)
Return a brief justification for an "unknown" result (i.e., Z3_L_UNDEF) for the commands Z3_solver_ch...
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition: z3_api.h:111
void reset ( )
inline

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

1278 { Z3_solver_reset(ctx(), m_solver); check_error(); }
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
void Z3_API Z3_solver_reset(__in Z3_context c, __in Z3_solver s)
Remove all assertions from the solver.
void set ( params const &  p)
inline

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

1275 { Z3_solver_set_params(ctx(), m_solver, p); check_error(); }
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
void Z3_API Z3_solver_set_params(__in Z3_context c, __in Z3_solver s, __in Z3_params p)
Set the given solver using the given parameters.
stats statistics ( ) const
inline

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

1312 { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); }
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
Z3_stats Z3_API Z3_solver_get_statistics(__in Z3_context c, __in Z3_solver s)
Return statistics for the given solver.
expr_vector unsat_core ( ) const
inline

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

1313 { Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
Z3_ast_vector Z3_API Z3_solver_get_unsat_core(__in Z3_context c, __in Z3_solver s)
Retrieve the unsat core for the last Z3_solver_check_assumptions The unsat core is a subset of the as...
context & ctx() const
Definition: z3++.h:272
void check_error() const
Definition: z3++.h:273
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:68

Friends And Related Function Documentation

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

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

1316 { out << Z3_solver_to_string(s.ctx(), s); return out; }
Z3_string Z3_API Z3_solver_to_string(__in Z3_context c, __in Z3_solver s)
Convert a solver into a string.