Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Data Structures | Typedefs | Enumerations | Functions
z3 Namespace Reference

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< astast_vector
 
typedef ast_vector_tpl< exprexpr_vector
 
typedef ast_vector_tpl< sortsort_vector
 
typedef ast_vector_tpl< func_declfunc_decl_vector
 

Enumerations

enum  check_result { unsat, sat, unknown }
 

Functions

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 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)
 
std::ostream & operator<< (std::ostream &out, check_result r)
 
check_result to_check_result (Z3_lbool l)
 
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)
 

Detailed Description

Z3 C++ namespace.

Typedef Documentation

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

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

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

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

Enumeration Type Documentation

Enumerator:
unsat 
sat 
unknown 

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

{
};

Function Documentation

tactic z3::cond ( probe const &  p,
tactic const &  t1,
tactic const &  t2 
)
inline

Definition at line 1405 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 1619 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::exists ( expr const &  x,
expr const &  b 
)
inline

Definition at line 921 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 926 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 931 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 936 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);
}
tactic z3::fail_if ( probe const &  p)
inline

Definition at line 1394 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 901 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 906 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 911 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 916 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);
}
func_decl z3::function ( symbol const &  name,
unsigned  arity,
sort const *  domain,
sort const &  range 
)
inline

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

{
return range.ctx().function(name, arity, domain, range);
}
func_decl z3::function ( char const *  name,
unsigned  arity,
sort const *  domain,
sort const &  range 
)
inline

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

{
return range.ctx().function(name, arity, domain, range);
}
func_decl z3::function ( char const *  name,
sort const &  domain,
sort const &  range 
)
inline

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

{
return range.ctx().function(name, domain, range);
}
func_decl z3::function ( char const *  name,
sort const &  d1,
sort const &  d2,
sort const &  range 
)
inline

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

{
return range.ctx().function(name, d1, d2, range);
}
func_decl z3::function ( char const *  name,
sort const &  d1,
sort const &  d2,
sort const &  d3,
sort const &  range 
)
inline

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

{
return range.ctx().function(name, d1, d2, d3, range);
}
func_decl z3::function ( char const *  name,
sort const &  d1,
sort const &  d2,
sort const &  d3,
sort const &  d4,
sort const &  range 
)
inline

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

{
return range.ctx().function(name, d1, d2, d3, d4, range);
}
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

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

{
return range.ctx().function(name, d1, d2, d3, d4, d5, range);
}
std::ostream& z3::operator<< ( std::ostream &  out,
check_result  r 
)
inline

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

{
if (r == unsat) out << "unsat";
else if (r == sat) out << "sat";
else out << "unknown";
return out;
}
expr z3::select ( expr const &  a,
expr const &  i 
)
inline

Definition at line 1601 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

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

{ return select(a, a.ctx().num_val(i, a.get_sort().array_domain())); }
expr z3::store ( expr const &  a,
expr const &  i,
expr const &  v 
)
inline

Definition at line 1608 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);
}
expr z3::store ( expr const &  a,
int  i,
expr const &  v 
)
inline

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

{ return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), v); }
expr z3::store ( expr const &  a,
expr  i,
int  v 
)
inline

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

{ return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }
expr z3::store ( expr const &  a,
int  i,
int  v 
)
inline

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

{
return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
}
check_result z3::to_check_result ( Z3_lbool  l)
inline

Definition at line 1145 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 849 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 ||
return expr(c, a);
}
func_decl z3::to_func_decl ( context &  c,
Z3_func_decl  f 
)
inline

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

{
c.check_error();
return func_decl(c, f);
}
expr z3::to_real ( expr const &  a)
inline

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

{
c.check_error();
return sort(c, s);
}
expr z3::udiv ( expr const &  a,
expr const &  b 
)
inline

unsigned division operator for bitvectors.

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

Referenced by udiv().

{ return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }
expr z3::udiv ( expr const &  a,
int  b 
)
inline

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

{ return udiv(a, a.ctx().num_val(b, a.get_sort())); }
expr z3::udiv ( int  a,
expr const &  b 
)
inline

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

{ return udiv(b.ctx().num_val(a, b.get_sort()), a); }
expr z3::uge ( expr const &  a,
expr const &  b 
)
inline

unsigned greater than or equal to operator for bitvectors.

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

Referenced by uge().

{ return to_expr(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b)); }
expr z3::uge ( expr const &  a,
int  b 
)
inline

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

{ return uge(a, a.ctx().num_val(b, a.get_sort())); }
expr z3::uge ( int  a,
expr const &  b 
)
inline

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

{ return uge(b.ctx().num_val(a, b.get_sort()), a); }
expr z3::ugt ( expr const &  a,
expr const &  b 
)
inline

unsigned greater than operator for bitvectors.

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

Referenced by ugt().

{ return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }
expr z3::ugt ( expr const &  a,
int  b 
)
inline

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

{ return ugt(a, a.ctx().num_val(b, a.get_sort())); }
expr z3::ugt ( int  a,
expr const &  b 
)
inline

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

{ return ugt(b.ctx().num_val(a, b.get_sort()), a); }
expr z3::ule ( expr const &  a,
expr const &  b 
)
inline

unsigned less than or equal to operator for bitvectors.

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

Referenced by ule().

{ return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }
expr z3::ule ( expr const &  a,
int  b 
)
inline

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

{ return ule(a, a.ctx().num_val(b, a.get_sort())); }
expr z3::ule ( int  a,
expr const &  b 
)
inline

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

{ return ule(b.ctx().num_val(a, b.get_sort()), a); }
expr z3::ult ( expr const &  a,
expr const &  b 
)
inline

unsigned less than operator for bitvectors.

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

Referenced by ult().

{ return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); }
expr z3::ult ( expr const &  a,
int  b 
)
inline

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

{ return ult(a, a.ctx().num_val(b, a.get_sort())); }
expr z3::ult ( int  a,
expr const &  b 
)
inline

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

{ return ult(b.ctx().num_val(a, b.get_sort()), a); }
tactic z3::when ( probe const &  p,
tactic const &  t 
)
inline

Definition at line 1399 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);
}