Z3 C++ namespace. More...
Data Structures | |
class | exception |
Exception used to sign API usage errors. More... | |
class | config |
Z3 global configuration object. More... | |
class | context |
A Context manages all other Z3 objects, global configuration options, etc. More... | |
class | array |
class | object |
class | symbol |
class | params |
class | ast |
class | sort |
A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort. More... | |
class | func_decl |
Function declaration (aka function definition). It is the signature of interpreted and uninterpreted functions in Z3. The basic building block in Z3 is the function application. More... | |
class | expr |
A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort Boolean. Every expression has a sort. More... | |
class | cast_ast< ast > |
class | cast_ast< expr > |
class | cast_ast< sort > |
class | cast_ast< func_decl > |
class | ast_vector_tpl |
class | func_entry |
class | func_interp |
class | model |
class | stats |
class | solver |
class | goal |
class | apply_result |
class | tactic |
class | probe |
Typedefs | |
typedef ast_vector_tpl< ast > | ast_vector |
typedef ast_vector_tpl< expr > | expr_vector |
typedef ast_vector_tpl< sort > | sort_vector |
typedef ast_vector_tpl< func_decl > | func_decl_vector |
Enumerations | |
enum | check_result { unsat, sat, unknown } |
Functions | |
void | set_param (char const *param, char const *value) |
void | set_param (char const *param, bool value) |
void | set_param (char const *param, int value) |
void | reset_params () |
void | check_context (object const &a, object const &b) |
bool | eq (ast const &a, ast const &b) |
expr | implies (expr const &a, bool b) |
expr | implies (bool a, expr const &b) |
expr | pw (expr const &a, expr const &b) |
expr | pw (expr const &a, int b) |
expr | pw (int a, expr const &b) |
expr | ite (expr const &c, expr const &t, expr const &e) |
Create the if-then-else expression ite(c, t, e) | |
expr | to_expr (context &c, Z3_ast a) |
Wraps a Z3_ast as an expr object. It also checks for errors. This function allows the user to use the whole C API with the C++ layer defined in this file. | |
sort | to_sort (context &c, Z3_sort s) |
func_decl | to_func_decl (context &c, Z3_func_decl f) |
expr | ule (expr const &a, expr const &b) |
unsigned less than or equal to operator for bitvectors. | |
expr | ule (expr const &a, int b) |
expr | ule (int a, expr const &b) |
expr | ult (expr const &a, expr const &b) |
unsigned less than operator for bitvectors. | |
expr | ult (expr const &a, int b) |
expr | ult (int a, expr const &b) |
expr | uge (expr const &a, expr const &b) |
unsigned greater than or equal to operator for bitvectors. | |
expr | uge (expr const &a, int b) |
expr | uge (int a, expr const &b) |
expr | ugt (expr const &a, expr const &b) |
unsigned greater than operator for bitvectors. | |
expr | ugt (expr const &a, int b) |
expr | ugt (int a, expr const &b) |
expr | udiv (expr const &a, expr const &b) |
unsigned division operator for bitvectors. | |
expr | udiv (expr const &a, int b) |
expr | udiv (int a, expr const &b) |
expr | forall (expr const &x, expr const &b) |
expr | forall (expr const &x1, expr const &x2, expr const &b) |
expr | forall (expr const &x1, expr const &x2, expr const &x3, expr const &b) |
expr | forall (expr const &x1, expr const &x2, expr const &x3, expr const &x4, expr const &b) |
expr | forall (expr_vector const &xs, expr const &b) |
expr | exists (expr const &x, expr const &b) |
expr | exists (expr const &x1, expr const &x2, expr const &b) |
expr | exists (expr const &x1, expr const &x2, expr const &x3, expr const &b) |
expr | exists (expr const &x1, expr const &x2, expr const &x3, expr const &x4, expr const &b) |
expr | exists (expr_vector const &xs, expr const &b) |
expr | distinct (expr_vector const &args) |
std::ostream & | operator<< (std::ostream &out, check_result r) |
check_result | to_check_result (Z3_lbool l) |
tactic | repeat (tactic const &t, unsigned max=UINT_MAX) |
tactic | with (tactic const &t, params const &p) |
tactic | try_for (tactic const &t, unsigned ms) |
tactic | fail_if (probe const &p) |
tactic | when (probe const &p, tactic const &t) |
tactic | cond (probe const &p, tactic const &t1, tactic const &t2) |
expr | to_real (expr const &a) |
func_decl | function (symbol const &name, unsigned arity, sort const *domain, sort const &range) |
func_decl | function (char const *name, unsigned arity, sort const *domain, sort const &range) |
func_decl | function (char const *name, sort const &domain, sort const &range) |
func_decl | function (char const *name, sort const &d1, sort const &d2, sort const &range) |
func_decl | function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &range) |
func_decl | function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &d4, sort const &range) |
func_decl | function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &d4, sort const &d5, sort const &range) |
expr | select (expr const &a, expr const &i) |
expr | select (expr const &a, int i) |
expr | store (expr const &a, expr const &i, expr const &v) |
expr | store (expr const &a, int i, expr const &v) |
expr | store (expr const &a, expr i, int v) |
expr | store (expr const &a, int i, int v) |
expr | const_array (sort const &d, expr const &v) |
Z3 C++ namespace.
typedef ast_vector_tpl<ast> ast_vector |
typedef ast_vector_tpl<expr> expr_vector |
typedef ast_vector_tpl<func_decl> func_decl_vector |
typedef ast_vector_tpl<sort> sort_vector |
enum check_result |
void z3::check_context | ( | object const & | a, |
object const & | b | ||
) | [inline] |
Definition at line 1527 of file z3++.h.
{ check_context(p, t1); check_context(p, t2); Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2); t1.check_error(); return tactic(t1.ctx(), r); }
expr z3::const_array | ( | sort const & | d, |
expr const & | v | ||
) | [inline] |
Definition at line 1783 of file z3++.h.
{ check_context(d, v); Z3_ast r = Z3_mk_const_array(d.ctx(), d, v); d.check_error(); return expr(d.ctx(), r); }
expr z3::distinct | ( | expr_vector const & | args | ) | [inline] |
Definition at line 1100 of file z3++.h.
{ assert(args.size() > 0); context& ctx = args[0].ctx(); array<Z3_ast> _args(args); Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr()); ctx.check_error(); return expr(ctx, r); }
bool z3::eq | ( | ast const & | a, |
ast const & | b | ||
) | [inline] |
Definition at line 344 of file z3++.h.
{ return Z3_is_eq_ast(a.ctx(), a, b) != 0; }
expr z3::exists | ( | expr const & | x, |
expr const & | b | ||
) | [inline] |
Definition at line 1074 of file z3++.h.
{ check_context(x, b); Z3_app vars[] = {(Z3_app) x}; Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); }
expr z3::exists | ( | expr const & | x1, |
expr const & | x2, | ||
expr const & | b | ||
) | [inline] |
Definition at line 1079 of file z3++.h.
{ check_context(x1, b); check_context(x2, b); Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2}; Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); }
expr z3::exists | ( | expr const & | x1, |
expr const & | x2, | ||
expr const & | x3, | ||
expr const & | b | ||
) | [inline] |
Definition at line 1084 of file z3++.h.
{ check_context(x1, b); check_context(x2, b); check_context(x3, b); Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 }; Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); }
expr z3::exists | ( | expr const & | x1, |
expr const & | x2, | ||
expr const & | x3, | ||
expr const & | x4, | ||
expr const & | b | ||
) | [inline] |
Definition at line 1089 of file z3++.h.
{ check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b); Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 }; Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); }
expr z3::exists | ( | expr_vector const & | xs, |
expr const & | b | ||
) | [inline] |
Definition at line 1094 of file z3++.h.
{ array<Z3_app> vars(xs); Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, 0, b); b.check_error(); return expr(b.ctx(), r); }
tactic z3::fail_if | ( | probe const & | p | ) | [inline] |
Definition at line 1516 of file z3++.h.
{ Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p); p.check_error(); return tactic(p.ctx(), r); }
expr z3::forall | ( | expr const & | x, |
expr const & | b | ||
) | [inline] |
Definition at line 1050 of file z3++.h.
{ check_context(x, b); Z3_app vars[] = {(Z3_app) x}; Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); }
expr z3::forall | ( | expr const & | x1, |
expr const & | x2, | ||
expr const & | b | ||
) | [inline] |
Definition at line 1055 of file z3++.h.
{ check_context(x1, b); check_context(x2, b); Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2}; Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); }
expr z3::forall | ( | expr const & | x1, |
expr const & | x2, | ||
expr const & | x3, | ||
expr const & | b | ||
) | [inline] |
Definition at line 1060 of file z3++.h.
{ check_context(x1, b); check_context(x2, b); check_context(x3, b); Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 }; Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); }
expr z3::forall | ( | expr const & | x1, |
expr const & | x2, | ||
expr const & | x3, | ||
expr const & | x4, | ||
expr const & | b | ||
) | [inline] |
Definition at line 1065 of file z3++.h.
{ check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b); Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 }; Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r); }
expr z3::forall | ( | expr_vector const & | xs, |
expr const & | b | ||
) | [inline] |
Definition at line 1070 of file z3++.h.
{ array<Z3_app> vars(xs); Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, 0, b); b.check_error(); return expr(b.ctx(), r); }
func_decl z3::function | ( | symbol const & | name, |
unsigned | arity, | ||
sort const * | domain, | ||
sort const & | range | ||
) | [inline] |
func_decl z3::function | ( | char const * | name, |
unsigned | arity, | ||
sort const * | domain, | ||
sort const & | range | ||
) | [inline] |
func_decl z3::function | ( | char const * | name, |
sort const & | domain, | ||
sort const & | range | ||
) | [inline] |
func_decl z3::function | ( | char const * | name, |
sort const & | d1, | ||
sort const & | d2, | ||
sort const & | range | ||
) | [inline] |
func_decl z3::function | ( | char const * | name, |
sort const & | d1, | ||
sort const & | d2, | ||
sort const & | d3, | ||
sort const & | range | ||
) | [inline] |
func_decl z3::function | ( | char const * | name, |
sort const & | d1, | ||
sort const & | d2, | ||
sort const & | d3, | ||
sort const & | d4, | ||
sort const & | range | ||
) | [inline] |
func_decl z3::function | ( | char const * | name, |
sort const & | d1, | ||
sort const & | d2, | ||
sort const & | d3, | ||
sort const & | d4, | ||
sort const & | d5, | ||
sort const & | range | ||
) | [inline] |
expr z3::implies | ( | expr const & | a, |
bool | b | ||
) | [inline] |
expr z3::implies | ( | bool | a, |
expr const & | b | ||
) | [inline] |
Create the if-then-else expression ite(c, t, e)
Definition at line 914 of file z3++.h.
{ check_context(c, t); check_context(c, e); assert(c.is_bool()); Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e); c.check_error(); return expr(c.ctx(), r); }
std::ostream& z3::operator<< | ( | std::ostream & | out, |
check_result | r | ||
) | [inline] |
Definition at line 894 of file z3++.h.
Referenced by pw().
{ assert(a.is_arith() && b.is_arith()); check_context(a, b); Z3_ast r = Z3_mk_power(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
tactic z3::repeat | ( | tactic const & | t, |
unsigned | max = UINT_MAX |
||
) | [inline] |
Definition at line 1440 of file z3++.h.
{ Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max); t.check_error(); return tactic(t.ctx(), r); }
void z3::reset_params | ( | ) | [inline] |
Definition at line 75 of file z3++.h.
{ Z3_global_param_reset_all(); }
expr z3::select | ( | expr const & | a, |
expr const & | i | ||
) | [inline] |
Definition at line 1765 of file z3++.h.
Referenced by select().
{ check_context(a, i); Z3_ast r = Z3_mk_select(a.ctx(), a, i); a.check_error(); return expr(a.ctx(), r); }
expr z3::select | ( | expr const & | a, |
int | i | ||
) | [inline] |
void z3::set_param | ( | char const * | param, |
char const * | value | ||
) | [inline] |
Definition at line 72 of file z3++.h.
{ Z3_global_param_set(param, value); }
void z3::set_param | ( | char const * | param, |
bool | value | ||
) | [inline] |
Definition at line 73 of file z3++.h.
{ Z3_global_param_set(param, value ? "true" : "false"); }
void z3::set_param | ( | char const * | param, |
int | value | ||
) | [inline] |
Definition at line 74 of file z3++.h.
{ std::ostringstream oss; oss << value; Z3_global_param_set(param, oss.str().c_str()); }
Definition at line 1772 of file z3++.h.
Referenced by store().
{ check_context(a, i); check_context(a, v); Z3_ast r = Z3_mk_store(a.ctx(), a, i, v); a.check_error(); return expr(a.ctx(), r); }
check_result z3::to_check_result | ( | Z3_lbool | l | ) | [inline] |
Definition at line 1249 of file z3++.h.
Referenced by solver::check().
{ if (l == Z3_L_TRUE) return sat; else if (l == Z3_L_FALSE) return unsat; return unknown; }
expr z3::to_expr | ( | context & | c, |
Z3_ast | a | ||
) | [inline] |
Wraps a Z3_ast as an expr object. It also checks for errors. This function allows the user to use the whole C API with the C++ layer defined in this file.
Definition at line 927 of file z3++.h.
Referenced by udiv(), uge(), ugt(), ule(), and ult().
{ c.check_error(); assert(Z3_get_ast_kind(c, a) == Z3_APP_AST || Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST || Z3_get_ast_kind(c, a) == Z3_VAR_AST || Z3_get_ast_kind(c, a) == Z3_QUANTIFIER_AST); return expr(c, a); }
func_decl z3::to_func_decl | ( | context & | c, |
Z3_func_decl | f | ||
) | [inline] |
expr z3::to_real | ( | expr const & | a | ) | [inline] |
Definition at line 1741 of file z3++.h.
{ Z3_ast r = Z3_mk_int2real(a.ctx(), a); a.check_error(); return expr(a.ctx(), r); }
sort z3::to_sort | ( | context & | c, |
Z3_sort | s | ||
) | [inline] |
Definition at line 936 of file z3++.h.
Referenced by context::enumeration_sort().
{
c.check_error();
return sort(c, s);
}
tactic z3::try_for | ( | tactic const & | t, |
unsigned | ms | ||
) | [inline] |
Definition at line 1451 of file z3++.h.
{ Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms); t.check_error(); return tactic(t.ctx(), r); }
unsigned division operator for bitvectors.
Definition at line 973 of file z3++.h.
Referenced by udiv().
{ return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }
unsigned greater than or equal to operator for bitvectors.
Definition at line 961 of file z3++.h.
Referenced by uge().
{ return to_expr(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b)); }
unsigned greater than operator for bitvectors.
Definition at line 967 of file z3++.h.
Referenced by ugt().
{ return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }
unsigned less than or equal to operator for bitvectors.
Definition at line 949 of file z3++.h.
Referenced by ule().
{ return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }
unsigned less than operator for bitvectors.
Definition at line 955 of file z3++.h.
Referenced by ult().
{ return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); }
Definition at line 1521 of file z3++.h.
{ check_context(p, t); Z3_tactic r = Z3_tactic_when(t.ctx(), p, t); t.check_error(); return tactic(t.ctx(), r); }
Definition at line 1446 of file z3++.h.
{ Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p); t.check_error(); return tactic(t.ctx(), r); }