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

Data Structures

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 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
 
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 proof () const
 
std::string to_smt2 (char const *status="unknown")
 
param_descrs get_param_descrs ()
 
- 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 1686 of file z3++.h.

Constructor & Destructor Documentation

§ solver() [1/6]

solver ( context c)
inline

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

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

§ solver() [2/6]

solver ( context c,
simple   
)
inline

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

1696 :object(c) { init(Z3_mk_simple_solver(c)); }
object(context &c)
Definition: z3++.h:330
Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c)
Create a new (incremental) solver.

§ solver() [3/6]

solver ( context c,
Z3_solver  s 
)
inline

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

1697 :object(c) { init(s); }
object(context &c)
Definition: z3++.h:330

§ solver() [4/6]

solver ( context c,
char const *  logic 
)
inline

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

1698 :object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(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...
object(context &c)
Definition: z3++.h:330

§ solver() [5/6]

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

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

1699 : object(c) { init(Z3_solver_translate(src.ctx(), src, c)); }
object(context &c)
Definition: z3++.h:330
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 a the context target.

§ solver() [6/6]

solver ( solver const &  s)
inline

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

1700 :object(s) { init(s.m_solver); }
object(context &c)
Definition: z3++.h:330

§ ~solver()

~solver ( )
inline

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

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

Member Function Documentation

§ add() [1/3]

void add ( expr const &  e)
inline

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

Referenced by Fixedpoint::__iadd__(), and Optimize::__iadd__().

1714 { assert(e.is_bool()); Z3_solver_assert(ctx(), m_solver, e); check_error(); }
context & ctx() const
Definition: z3++.h:332
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.
void check_error() const
Definition: z3++.h:333

§ add() [2/3]

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

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

Referenced by Fixedpoint::__iadd__(), and Optimize::__iadd__().

1715  {
1716  assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const());
1717  Z3_solver_assert_and_track(ctx(), m_solver, e, p);
1718  check_error();
1719  }
context & ctx() const
Definition: z3++.h:332
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...
void check_error() const
Definition: z3++.h:333

§ add() [3/3]

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

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

Referenced by Fixedpoint::__iadd__(), and Optimize::__iadd__().

1720  {
1721  add(e, ctx().bool_const(p));
1722  }
context & ctx() const
Definition: z3++.h:332
void add(expr const &e)
Definition: z3++.h:1714

§ assertions()

expr_vector assertions ( ) const
inline

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

Referenced by Solver::to_smt2().

1754 { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
context & ctx() const
Definition: z3++.h:332
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)
Return the set of asserted formulas on the solver.
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:68
void check_error() const
Definition: z3++.h:333

§ check() [1/3]

check_result check ( )
inline

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

1723 { Z3_lbool r = Z3_solver_check(ctx(), m_solver); check_error(); return to_check_result(r); }
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.
context & ctx() const
Definition: z3++.h:332
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:105
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:124
void check_error() const
Definition: z3++.h:333

§ check() [2/3]

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

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

1724  {
1725  array<Z3_ast> _assumptions(n);
1726  for (unsigned i = 0; i < n; i++) {
1727  check_context(*this, assumptions[i]);
1728  _assumptions[i] = assumptions[i];
1729  }
1730  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
1731  check_error();
1732  return to_check_result(r);
1733  }
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...
context & ctx() const
Definition: z3++.h:332
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:105
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:124
void check_error() const
Definition: z3++.h:333

§ check() [3/3]

check_result check ( expr_vector  assumptions)
inline

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

1734  {
1735  unsigned n = assumptions.size();
1736  array<Z3_ast> _assumptions(n);
1737  for (unsigned i = 0; i < n; i++) {
1738  check_context(*this, assumptions[i]);
1739  _assumptions[i] = assumptions[i];
1740  }
1741  Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
1742  check_error();
1743  return to_check_result(r);
1744  }
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...
context & ctx() const
Definition: z3++.h:332
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:105
friend void check_context(object const &a, object const &b)
Definition: z3++.h:336
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:124
void check_error() const
Definition: z3++.h:333

§ consequences()

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

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

1746  {
1747  Z3_lbool r = Z3_solver_get_consequences(ctx(), m_solver, assumptions, vars, conseq);
1748  check_error();
1749  return to_check_result(r);
1750  }
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.
context & ctx() const
Definition: z3++.h:332
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:105
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:124
void check_error() const
Definition: z3++.h:333

§ get_model()

model get_model ( ) const
inline

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

1745 { Z3_model m = Z3_solver_get_model(ctx(), m_solver); check_error(); return model(ctx(), m); }
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.
context & ctx() const
Definition: z3++.h:332
void check_error() const
Definition: z3++.h:333

§ get_param_descrs()

param_descrs get_param_descrs ( )
inline

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

1777 { return param_descrs(ctx(), Z3_solver_get_param_descrs(ctx(), m_solver)); }
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.
context & ctx() const
Definition: z3++.h:332

§ operator Z3_solver()

operator Z3_solver ( ) const
inline

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

1702 { return m_solver; }

§ operator=()

solver& operator= ( solver const &  s)
inline

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

1703  {
1704  Z3_solver_inc_ref(s.ctx(), s.m_solver);
1705  Z3_solver_dec_ref(ctx(), m_solver);
1706  m_ctx = s.m_ctx;
1707  m_solver = s.m_solver;
1708  return *this;
1709  }
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.
context & ctx() const
Definition: z3++.h:332
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.
context * m_ctx
Definition: z3++.h:328

§ pop()

void pop ( unsigned  n = 1)
inline

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

1712 { Z3_solver_pop(ctx(), m_solver, n); check_error(); }
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.
context & ctx() const
Definition: z3++.h:332
void check_error() const
Definition: z3++.h:333

§ proof()

expr proof ( ) const
inline

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

1755 { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
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.
context & ctx() const
Definition: z3++.h:332
void check_error() const
Definition: z3++.h:333

§ push()

void push ( )
inline

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

1711 { Z3_solver_push(ctx(), m_solver); check_error(); }
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.
context & ctx() const
Definition: z3++.h:332
void check_error() const
Definition: z3++.h:333

§ reason_unknown()

std::string reason_unknown ( ) const
inline

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

1751 { Z3_string r = Z3_solver_get_reason_unknown(ctx(), m_solver); check_error(); return r; }
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...
context & ctx() const
Definition: z3++.h:332
void check_error() const
Definition: z3++.h:333
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition: z3_api.h:89

§ reset()

void reset ( )
inline

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

1713 { Z3_solver_reset(ctx(), m_solver); check_error(); }
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
context & ctx() const
Definition: z3++.h:332
void check_error() const
Definition: z3++.h:333

§ set()

void set ( params const &  p)
inline

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

1710 { Z3_solver_set_params(ctx(), m_solver, p); check_error(); }
context & ctx() const
Definition: z3++.h:332
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.
void check_error() const
Definition: z3++.h:333

§ statistics()

stats statistics ( ) const
inline

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

1752 { Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); }
context & ctx() const
Definition: z3++.h:332
Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.
void check_error() const
Definition: z3++.h:333

§ to_smt2()

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

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

1758  {
1759  array<Z3_ast> es(assertions());
1760  Z3_ast const* fmls = es.ptr();
1761  Z3_ast fml = 0;
1762  unsigned sz = es.size();
1763  if (sz > 0) {
1764  --sz;
1765  fml = fmls[sz];
1766  }
1767  else {
1768  fml = ctx().bool_val(true);
1769  }
1770  return std::string(Z3_benchmark_to_smtlib_string(
1771  ctx(),
1772  "", "", status, "",
1773  sz,
1774  fmls,
1775  fml));
1776  }
context & ctx() const
Definition: z3++.h:332
expr bool_val(bool b)
Definition: z3++.h:2197
expr_vector assertions() const
Definition: z3++.h:1754
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.

§ unsat_core()

expr_vector unsat_core ( ) const
inline

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

1753 { Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
context & ctx() const
Definition: z3++.h:332
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...
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:68
void check_error() const
Definition: z3++.h:333

Friends And Related Function Documentation

§ operator<<

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

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

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