Z3
Data Structures | Public Member Functions | Friends
solver Class Reference
+ Inheritance diagram for solver:

Data Structures

class  cube_generator
 
class  cube_iterator
 
struct  simple
 
struct  translate
 

Public Member Functions

 solver (context &c)
 
 solver (context &c, simple)
 
 solver (context &c, Z3_solver s)
 
 solver (context &c, char const *logic)
 
 solver (context &c, solver const &src, translate)
 
 solver (solver const &s)
 
 ~solver ()
 
 operator Z3_solver () const
 
solveroperator= (solver const &s)
 
void set (params const &p)
 
void set (char const *k, bool v)
 
void set (char const *k, unsigned v)
 
void set (char const *k, double v)
 
void set (char const *k, symbol const &v)
 
void set (char const *k, char const *v)
 
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)
 
void add (expr_vector const &v)
 
void from_file (char const *file)
 
void from_string (char const *s)
 
expr lower (expr const &e)
 
expr upper (expr const &e)
 
expr value (expr const &e)
 
check_result check ()
 
check_result check (unsigned n, expr *const assumptions)
 
check_result check (expr_vector const &assumptions)
 
model get_model () const
 
check_result consequences (expr_vector &assumptions, expr_vector &vars, expr_vector &conseq)
 
std::string reason_unknown () const
 
stats statistics () const
 
expr_vector unsat_core () const
 
expr_vector assertions () const
 
expr_vector non_units () const
 
expr_vector units () const
 
expr_vector trail () const
 
expr_vector trail (array< unsigned > &levels) const
 
expr proof () const
 
std::string to_smt2 (char const *status="unknown")
 
std::string dimacs (bool include_names=true) const
 
param_descrs get_param_descrs ()
 
expr_vector cube (expr_vector &vars, unsigned cutoff)
 
cube_generator cubes ()
 
cube_generator cubes (expr_vector &vars)
 
- Public Member Functions inherited from object
 object (context &c)
 
 object (object const &s)
 
contextctx () const
 
Z3_error_code 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 2355 of file z3++.h.

Constructor & Destructor Documentation

◆ solver() [1/6]

solver ( context c)
inline

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

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

◆ solver() [2/6]

solver ( context c,
simple   
)
inline

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

2365 :object(c) { init(Z3_mk_simple_solver(c)); }

◆ solver() [3/6]

solver ( context c,
Z3_solver  s 
)
inline

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

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

◆ solver() [4/6]

solver ( context c,
char const *  logic 
)
inline

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

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

◆ solver() [5/6]

solver ( context c,
solver const &  src,
translate   
)
inline

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

2368 : object(c) { init(Z3_solver_translate(src.ctx(), src, c)); }

◆ solver() [6/6]

solver ( solver const &  s)
inline

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

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

◆ ~solver()

~solver ( )
inline

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

2370 { Z3_solver_dec_ref(ctx(), m_solver); }

Member Function Documentation

◆ add() [1/4]

void add ( expr const &  e)
inline

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

2388 { assert(e.is_bool()); Z3_solver_assert(ctx(), m_solver, e); check_error(); }

Referenced by solver::add().

◆ add() [2/4]

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

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

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

◆ add() [3/4]

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

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

2389  {
2390  assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const());
2391  Z3_solver_assert_and_track(ctx(), m_solver, e, p);
2392  check_error();
2393  }

◆ add() [4/4]

void add ( expr_vector const &  v)
inline

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

2397  {
2398  check_context(*this, v);
2399  for (unsigned i = 0; i < v.size(); ++i)
2400  add(v[i]);
2401  }

◆ assertions()

expr_vector assertions ( ) const
inline

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

2446 { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }

Referenced by solver::to_smt2().

◆ check() [1/3]

check_result check ( )
inline

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

2415 { Z3_lbool r = Z3_solver_check(ctx(), m_solver); check_error(); return to_check_result(r); }

◆ check() [2/3]

check_result check ( expr_vector const &  assumptions)
inline

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

2426  {
2427  unsigned n = assumptions.size();
2428  array<Z3_ast> _assumptions(n);
2429  for (unsigned i = 0; i < n; i++) {
2430  check_context(*this, assumptions[i]);
2431  _assumptions[i] = assumptions[i];
2432  }
2433  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
2434  check_error();
2435  return to_check_result(r);
2436  }

◆ check() [3/3]

check_result check ( unsigned  n,
expr *const  assumptions 
)
inline

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

2416  {
2417  array<Z3_ast> _assumptions(n);
2418  for (unsigned i = 0; i < n; i++) {
2419  check_context(*this, assumptions[i]);
2420  _assumptions[i] = assumptions[i];
2421  }
2422  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
2423  check_error();
2424  return to_check_result(r);
2425  }

◆ consequences()

check_result consequences ( expr_vector assumptions,
expr_vector vars,
expr_vector conseq 
)
inline

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

2438  {
2439  Z3_lbool r = Z3_solver_get_consequences(ctx(), m_solver, assumptions, vars, conseq);
2440  check_error();
2441  return to_check_result(r);
2442  }

◆ cube()

expr_vector cube ( expr_vector vars,
unsigned  cutoff 
)
inline

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

2488  {
2489  Z3_ast_vector r = Z3_solver_cube(ctx(), m_solver, vars, cutoff);
2490  check_error();
2491  return expr_vector(ctx(), r);
2492  }

◆ cubes() [1/2]

cube_generator cubes ( )
inline

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

2575 { return cube_generator(*this); }

◆ cubes() [2/2]

cube_generator cubes ( expr_vector vars)
inline

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

2576 { return cube_generator(*this, vars); }

◆ dimacs()

std::string dimacs ( bool  include_names = true) const
inline

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

2483 { return std::string(Z3_solver_to_dimacs_string(ctx(), m_solver, include_names)); }

◆ from_file()

void from_file ( char const *  file)
inline

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

2402 { Z3_solver_from_file(ctx(), m_solver, file); ctx().check_parser_error(); }

◆ from_string()

void from_string ( char const *  s)
inline

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

2403 { Z3_solver_from_string(ctx(), m_solver, s); ctx().check_parser_error(); }

◆ get_model()

model get_model ( ) const
inline

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

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

◆ get_param_descrs()

param_descrs get_param_descrs ( )
inline

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

2485 { return param_descrs(ctx(), Z3_solver_get_param_descrs(ctx(), m_solver)); }

◆ lower()

expr lower ( expr const &  e)
inline

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

2405  {
2406  Z3_ast r = Z3_solver_get_implied_lower(ctx(), m_solver, e); check_error(); return expr(ctx(), r);
2407  }

◆ non_units()

expr_vector non_units ( ) const
inline

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

2447 { Z3_ast_vector r = Z3_solver_get_non_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }

◆ operator Z3_solver()

operator Z3_solver ( ) const
inline

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

2371 { return m_solver; }

◆ operator=()

solver& operator= ( solver const &  s)
inline

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

2372  {
2373  Z3_solver_inc_ref(s.ctx(), s.m_solver);
2374  Z3_solver_dec_ref(ctx(), m_solver);
2375  m_ctx = s.m_ctx;
2376  m_solver = s.m_solver;
2377  return *this;
2378  }

◆ pop()

void pop ( unsigned  n = 1)
inline

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

2386 { Z3_solver_pop(ctx(), m_solver, n); check_error(); }

◆ proof()

expr proof ( ) const
inline

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

2460 { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }

◆ push()

void push ( )
inline

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

2385 { Z3_solver_push(ctx(), m_solver); check_error(); }

◆ reason_unknown()

std::string reason_unknown ( ) const
inline

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

2443 { Z3_string r = Z3_solver_get_reason_unknown(ctx(), m_solver); check_error(); return r; }

◆ reset()

void reset ( )
inline

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

2387 { Z3_solver_reset(ctx(), m_solver); check_error(); }

◆ set() [1/6]

void set ( char const *  k,
bool  v 
)
inline

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

2380 { params p(ctx()); p.set(k, v); set(p); }

Referenced by solver::set().

◆ set() [2/6]

void set ( char const *  k,
char const *  v 
)
inline

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

2384 { params p(ctx()); p.set(k, v); set(p); }

Referenced by solver::set().

◆ set() [3/6]

void set ( char const *  k,
double  v 
)
inline

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

2382 { params p(ctx()); p.set(k, v); set(p); }

Referenced by solver::set().

◆ set() [4/6]

void set ( char const *  k,
symbol const &  v 
)
inline

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

2383 { params p(ctx()); p.set(k, v); set(p); }

Referenced by solver::set().

◆ set() [5/6]

void set ( char const *  k,
unsigned  v 
)
inline

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

2381 { params p(ctx()); p.set(k, v); set(p); }

Referenced by solver::set().

◆ set() [6/6]

void set ( params const &  p)
inline

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

2379 { Z3_solver_set_params(ctx(), m_solver, p); check_error(); }

◆ statistics()

stats statistics ( ) const
inline

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

2444 { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); }

◆ to_smt2()

std::string to_smt2 ( char const *  status = "unknown")
inline

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

2463  {
2464  array<Z3_ast> es(assertions());
2465  Z3_ast const* fmls = es.ptr();
2466  Z3_ast fml = 0;
2467  unsigned sz = es.size();
2468  if (sz > 0) {
2469  --sz;
2470  fml = fmls[sz];
2471  }
2472  else {
2473  fml = ctx().bool_val(true);
2474  }
2475  return std::string(Z3_benchmark_to_smtlib_string(
2476  ctx(),
2477  "", "", status, "",
2478  sz,
2479  fmls,
2480  fml));
2481  }

◆ trail() [1/2]

expr_vector trail ( ) const
inline

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

2449 { Z3_ast_vector r = Z3_solver_get_trail(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }

◆ trail() [2/2]

expr_vector trail ( array< unsigned > &  levels) const
inline

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

2450  {
2451  Z3_ast_vector r = Z3_solver_get_trail(ctx(), m_solver);
2452  check_error();
2453  expr_vector result(ctx(), r);
2454  unsigned sz = result.size();
2455  levels.resize(sz);
2456  Z3_solver_get_levels(ctx(), m_solver, r, sz, levels.ptr());
2457  check_error();
2458  return result;
2459  }

◆ units()

expr_vector units ( ) const
inline

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

2448 { Z3_ast_vector r = Z3_solver_get_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }

◆ unsat_core()

expr_vector unsat_core ( ) const
inline

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

2445 { Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }

◆ upper()

expr upper ( expr const &  e)
inline

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

2408  {
2409  Z3_ast r = Z3_solver_get_implied_upper(ctx(), m_solver, e); check_error(); return expr(ctx(), r);
2410  }

◆ value()

expr value ( expr const &  e)
inline

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

2411  {
2412  Z3_ast r = Z3_solver_get_implied_value(ctx(), m_solver, e); check_error(); return expr(ctx(), r);
2413  }

Friends And Related Function Documentation

◆ operator<<

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

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

2579 { out << Z3_solver_to_string(s.ctx(), s); return out; }
Z3_solver_get_implied_lower
Z3_ast Z3_API Z3_solver_get_implied_lower(Z3_context c, Z3_solver s, Z3_ast e)
retrieve implied lower bound value for arithmetic expression. If a lower bound is implied at search l...
Z3_solver_to_string
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.
z3::solver::assertions
expr_vector assertions() const
Definition: z3++.h:2446
Z3_solver_get_levels
void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, unsigned sz, unsigned levels[])
retrieve the decision depth of Boolean literals (variables or their negations). Assumes a check-sat c...
Z3_solver_check
Z3_lbool Z3_API Z3_solver_check(Z3_context c, Z3_solver s)
Check whether the assertions in a given solver are consistent or not.
Z3_solver_reset
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
Z3_solver_get_proof
Z3_ast Z3_API Z3_solver_get_proof(Z3_context c, Z3_solver s)
Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions.
Z3_solver_get_reason_unknown
Z3_string Z3_API Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s)
Return a brief justification for an "unknown" result (i.e., Z3_L_UNDEF) for the commands Z3_solver_ch...
Z3_solver_pop
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.
Z3_solver_check_assumptions
Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[])
Check whether the assertions in the given solver and optional assumptions are consistent or not.
Z3_mk_solver_for_logic
Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic)
Create a new solver customized for the given logic. It behaves like Z3_mk_solver if the logic is unkn...
Z3_solver_push
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.
Z3_string
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition: z3_api.h:82
Z3_lbool
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:100
Z3_solver_get_assertions
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)
Return the set of asserted formulas on the solver.
Z3_solver_to_dimacs_string
Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s, bool include_names)
Convert a solver into a DIMACS formatted string.
z3::object::object
object(context &c)
Definition: z3++.h:416
Z3_solver_get_param_descrs
Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s)
Return the parameter description set for the given solver object.
z3::solver::add
void add(expr const &e)
Definition: z3++.h:2388
z3::object::m_ctx
context * m_ctx
Definition: z3++.h:414
z3::context::bool_val
expr bool_val(bool b)
Definition: z3++.h:3183
Z3_solver_get_trail
Z3_ast_vector Z3_API Z3_solver_get_trail(Z3_context c, Z3_solver s)
Return the trail modulo model conversion, in order of decision level The decision level can be retrie...
Z3_solver_dec_ref
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.
Z3_solver_from_string
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a string.
Z3_solver_get_unsat_core
Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s)
Retrieve the unsat core for the last Z3_solver_check_assumptions The unsat core is a subset of the as...
z3::context::check_parser_error
void check_parser_error() const
Definition: z3++.h:194
Z3_solver_get_units
Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s)
Return the set of units modulo model conversion.
Z3_solver_get_implied_value
Z3_ast Z3_API Z3_solver_get_implied_value(Z3_context c, Z3_solver s, Z3_ast e)
retrieve implied value for expression, if any is implied by solver at search level....
Z3_solver_assert_and_track
void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p)
Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant p.
z3::expr_vector
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:72
Z3_solver_get_statistics
Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.
Z3_solver_set_params
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.
Z3_solver_get_non_units
Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s)
Return the set of non units in the solver state.
Z3_solver_cube
Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vars, unsigned backtrack_level)
extract a next cube for a solver. The last cube is the constant true or false. The number of (non-con...
Z3_solver_assert
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.
z3::object::check_context
friend void check_context(object const &a, object const &b)
Definition: z3++.h:422
Z3_solver_translate
Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target)
Copy a solver s from the context source to the context target.
z3::solver::set
void set(params const &p)
Definition: z3++.h:2379
Z3_solver_get_implied_upper
Z3_ast Z3_API Z3_solver_get_implied_upper(Z3_context c, Z3_solver s, Z3_ast e)
retrieve implied upper bound value for arithmetic expression. If an upper bound is implied at search ...
Z3_mk_solver
Z3_solver Z3_API Z3_mk_solver(Z3_context c)
Create a new solver. This solver is a "combined solver" (see combined_solver module) that internally ...
Z3_mk_simple_solver
Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c)
Create a new incremental solver.
Z3_solver_from_file
void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a file.
z3::to_check_result
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:143
z3::object::check_error
Z3_error_code check_error() const
Definition: z3++.h:419
Z3_solver_get_consequences
Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c, Z3_solver s, Z3_ast_vector assumptions, Z3_ast_vector variables, Z3_ast_vector consequences)
retrieve consequences from solver that determine values of the supplied function symbols.
Z3_benchmark_to_smtlib_string
Z3_string Z3_API Z3_benchmark_to_smtlib_string(Z3_context c, Z3_string name, Z3_string logic, Z3_string status, Z3_string attributes, unsigned num_assumptions, Z3_ast const assumptions[], Z3_ast formula)
Convert the given benchmark into SMT-LIB formatted string.
z3::object::ctx
context & ctx() const
Definition: z3++.h:418
Z3_solver_get_model
Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s)
Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions.
Z3_solver_inc_ref
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.