Z3
Data Structures | Typedefs | Enumerations | Functions
z3 Namespace Reference

Z3 C++ namespace. More...

Data Structures

class  apply_result
 
class  array
 
class  ast
 
class  ast_vector_tpl
 
class  cast_ast
 
class  cast_ast< ast >
 
class  cast_ast< expr >
 
class  cast_ast< func_decl >
 
class  cast_ast< sort >
 
class  config
 Z3 global configuration object. More...
 
class  context
 A Context manages all other Z3 objects, global configuration options, etc. More...
 
class  exception
 Exception used to sign API usage errors. 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  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  func_entry
 
class  func_interp
 
class  goal
 
class  model
 
class  object
 
class  optimize
 
class  params
 
class  probe
 
class  solver
 
class  sort
 A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort. More...
 
class  stats
 
class  symbol
 
class  tactic
 

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

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) More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
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)
 
expr concat (expr const &a, expr const &b)
 
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)
 

Detailed Description

Z3 C++ namespace.

Typedef Documentation

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

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

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

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

Enumeration Type Documentation

Enumerator
unsat 
sat 
unknown 

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

1254  {
1255  unsat, sat, unknown
1256  };
Definition: z3++.h:1255

Function Documentation

void z3::check_context ( object const &  a,
object const &  b 
)
inline
expr z3::concat ( expr const &  a,
expr const &  b 
)
inline

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

1118  {
1119  check_context(a, b);
1120  Z3_ast r = Z3_mk_concat(a.ctx(), a, b);
1121  a.ctx().check_error();
1122  return expr(a.ctx(), r);
1123  }
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
void check_context(object const &a, object const &b)
Definition: z3++.h:281
tactic z3::cond ( probe const &  p,
tactic const &  t1,
tactic const &  t2 
)
inline

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

1619  {
1620  check_context(p, t1); check_context(p, t2);
1621  Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2);
1622  t1.check_error();
1623  return tactic(t1.ctx(), r);
1624  }
Z3_tactic Z3_API Z3_tactic_cond(Z3_context c, Z3_probe p, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal if the probe p evaluates to true, and t2 if p evaluat...
void check_context(object const &a, object const &b)
Definition: z3++.h:281
expr z3::const_array ( sort const &  d,
expr const &  v 
)
inline

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

1882  {
1883  check_context(d, v);
1884  Z3_ast r = Z3_mk_const_array(d.ctx(), d, v);
1885  d.check_error();
1886  return expr(d.ctx(), r);
1887  }
Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v)
Create the constant array.
void check_context(object const &a, object const &b)
Definition: z3++.h:281
expr z3::distinct ( expr_vector const &  args)
inline

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

1109  {
1110  assert(args.size() > 0);
1111  context& ctx = args[0].ctx();
1112  array<Z3_ast> _args(args);
1113  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
1114  ctx.check_error();
1115  return expr(ctx, r);
1116  }
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).The distinct construct is us...
bool z3::eq ( ast const &  a,
ast const &  b 
)
inline

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

349 { return Z3_is_eq_ast(a.ctx(), a, b) != 0; }
Z3_bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2)
compare terms.
expr z3::exists ( expr const &  x,
expr const &  b 
)
inline

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

1083  {
1084  check_context(x, b);
1085  Z3_app vars[] = {(Z3_app) x};
1086  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1087  }
Z3_ast Z3_API Z3_mk_exists_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Similar to Z3_mk_forall_const.
System.IntPtr Z3_app
Definition: Native.cs:14
void check_context(object const &a, object const &b)
Definition: z3++.h:281
expr z3::exists ( expr const &  x1,
expr const &  x2,
expr const &  b 
)
inline

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

1088  {
1089  check_context(x1, b); check_context(x2, b);
1090  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1091  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1092  }
Z3_ast Z3_API Z3_mk_exists_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Similar to Z3_mk_forall_const.
System.IntPtr Z3_app
Definition: Native.cs:14
void check_context(object const &a, object const &b)
Definition: z3++.h:281
expr z3::exists ( expr const &  x1,
expr const &  x2,
expr const &  x3,
expr const &  b 
)
inline

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

1093  {
1094  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1095  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1096  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1097  }
Z3_ast Z3_API Z3_mk_exists_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Similar to Z3_mk_forall_const.
System.IntPtr Z3_app
Definition: Native.cs:14
void check_context(object const &a, object const &b)
Definition: z3++.h:281
expr z3::exists ( expr const &  x1,
expr const &  x2,
expr const &  x3,
expr const &  x4,
expr const &  b 
)
inline

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

1098  {
1099  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
1100  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1101  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1102  }
Z3_ast Z3_API Z3_mk_exists_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Similar to Z3_mk_forall_const.
System.IntPtr Z3_app
Definition: Native.cs:14
void check_context(object const &a, object const &b)
Definition: z3++.h:281
expr z3::exists ( expr_vector const &  xs,
expr const &  b 
)
inline

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

1103  {
1104  array<Z3_app> vars(xs);
1105  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);
1106  }
Z3_ast Z3_API Z3_mk_exists_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Similar to Z3_mk_forall_const.
tactic z3::fail_if ( probe const &  p)
inline

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

1608  {
1609  Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
1610  p.check_error();
1611  return tactic(p.ctx(), r);
1612  }
Z3_tactic Z3_API Z3_tactic_fail_if(Z3_context c, Z3_probe p)
Return a tactic that fails if the probe p evaluates to false.
expr z3::forall ( expr const &  x,
expr const &  b 
)
inline

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

1059  {
1060  check_context(x, b);
1061  Z3_app vars[] = {(Z3_app) x};
1062  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1063  }
System.IntPtr Z3_app
Definition: Native.cs:14
void check_context(object const &a, object const &b)
Definition: z3++.h:281
Z3_ast Z3_API Z3_mk_forall_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables...
expr z3::forall ( expr const &  x1,
expr const &  x2,
expr const &  b 
)
inline

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

1064  {
1065  check_context(x1, b); check_context(x2, b);
1066  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1067  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1068  }
System.IntPtr Z3_app
Definition: Native.cs:14
void check_context(object const &a, object const &b)
Definition: z3++.h:281
Z3_ast Z3_API Z3_mk_forall_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables...
expr z3::forall ( expr const &  x1,
expr const &  x2,
expr const &  x3,
expr const &  b 
)
inline

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

1069  {
1070  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1071  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1072  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1073  }
System.IntPtr Z3_app
Definition: Native.cs:14
void check_context(object const &a, object const &b)
Definition: z3++.h:281
Z3_ast Z3_API Z3_mk_forall_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables...
expr z3::forall ( expr const &  x1,
expr const &  x2,
expr const &  x3,
expr const &  x4,
expr const &  b 
)
inline

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

1074  {
1075  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
1076  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1077  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1078  }
System.IntPtr Z3_app
Definition: Native.cs:14
void check_context(object const &a, object const &b)
Definition: z3++.h:281
Z3_ast Z3_API Z3_mk_forall_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables...
expr z3::forall ( expr_vector const &  xs,
expr const &  b 
)
inline

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

1079  {
1080  array<Z3_app> vars(xs);
1081  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);
1082  }
Z3_ast Z3_API Z3_mk_forall_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables...
func_decl z3::function ( symbol const &  name,
unsigned  arity,
sort const *  domain,
sort const &  range 
)
inline

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

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

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

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

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

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

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

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

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

1854  {
1855  return range.ctx().function(name, d1, d2, d3, range);
1856  }
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 1857 of file z3++.h.

1857  {
1858  return range.ctx().function(name, d1, d2, d3, d4, range);
1859  }
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 1860 of file z3++.h.

1860  {
1861  return range.ctx().function(name, d1, d2, d3, d4, d5, range);
1862  }
expr z3::implies ( expr const &  a,
bool  b 
)
inline

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

Referenced by implies().

900 { return implies(a, a.ctx().bool_val(b)); }
expr implies(bool a, expr const &b)
Definition: z3++.h:901
expr z3::implies ( bool  a,
expr const &  b 
)
inline

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

901 { return implies(b.ctx().bool_val(a), b); }
expr implies(bool a, expr const &b)
Definition: z3++.h:901
expr z3::ite ( expr const &  c,
expr const &  t,
expr const &  e 
)
inline

Create the if-then-else expression ite(c, t, e)

Precondition
c.is_bool()

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

923  {
924  check_context(c, t); check_context(c, e);
925  assert(c.is_bool());
926  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
927  c.check_error();
928  return expr(c.ctx(), r);
929  }
void check_context(object const &a, object const &b)
Definition: z3++.h:281
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
std::ostream& z3::operator<< ( std::ostream &  out,
check_result  r 
)
inline

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

1258  {
1259  if (r == unsat) out << "unsat";
1260  else if (r == sat) out << "sat";
1261  else out << "unknown";
1262  return out;
1263  }
Definition: z3++.h:1255
expr z3::pw ( expr const &  a,
expr const &  b 
)
inline

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

Referenced by pw().

903  {
904  assert(a.is_arith() && b.is_arith());
905  check_context(a, b);
906  Z3_ast r = Z3_mk_power(a.ctx(), a, b);
907  a.check_error();
908  return expr(a.ctx(), r);
909  }
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1^arg2.
void check_context(object const &a, object const &b)
Definition: z3++.h:281
expr z3::pw ( expr const &  a,
int  b 
)
inline

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

910 { return pw(a, a.ctx().num_val(b, a.get_sort())); }
expr pw(int a, expr const &b)
Definition: z3++.h:911
expr z3::pw ( int  a,
expr const &  b 
)
inline

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

911 { return pw(b.ctx().num_val(a, b.get_sort()), b); }
expr pw(int a, expr const &b)
Definition: z3++.h:911
tactic z3::repeat ( tactic const &  t,
unsigned  max = UINT_MAX 
)
inline

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

1476  {
1477  Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
1478  t.check_error();
1479  return tactic(t.ctx(), r);
1480  }
Z3_tactic Z3_API Z3_tactic_repeat(Z3_context c, Z3_tactic t, unsigned max)
Return a tactic that keeps applying t until the goal is not modified anymore or the maximum number of...
void z3::reset_params ( )
inline

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

void Z3_API Z3_global_param_reset_all(void)
Restore the value of all global (and module) parameters. This command will not affect already created...
expr z3::select ( expr const &  a,
expr const &  i 
)
inline

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

Referenced by select().

1864  {
1865  check_context(a, i);
1866  Z3_ast r = Z3_mk_select(a.ctx(), a, i);
1867  a.check_error();
1868  return expr(a.ctx(), r);
1869  }
void check_context(object const &a, object const &b)
Definition: z3++.h:281
Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i)
Array read. The argument a is the array and i is the index of the array that gets read...
expr z3::select ( expr const &  a,
int  i 
)
inline

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

1870 { return select(a, a.ctx().num_val(i, a.get_sort().array_domain())); }
expr select(expr const &a, int i)
Definition: z3++.h:1870
void z3::set_param ( char const *  param,
char const *  value 
)
inline

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

72 { Z3_global_param_set(param, value); }
void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value)
Set a global (or module) parameter. This setting is shared by all Z3 contexts.
void z3::set_param ( char const *  param,
bool  value 
)
inline

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

73 { Z3_global_param_set(param, value ? "true" : "false"); }
void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value)
Set a global (or module) parameter. This setting is shared by all Z3 contexts.
void z3::set_param ( char const *  param,
int  value 
)
inline

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

74 { std::ostringstream oss; oss << value; Z3_global_param_set(param, oss.str().c_str()); }
void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value)
Set a global (or module) parameter. This setting is shared by all Z3 contexts.
expr z3::store ( expr const &  a,
expr const &  i,
expr const &  v 
)
inline

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

Referenced by store().

1871  {
1872  check_context(a, i); check_context(a, v);
1873  Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
1874  a.check_error();
1875  return expr(a.ctx(), r);
1876  }
Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v)
Array update.
void check_context(object const &a, object const &b)
Definition: z3++.h:281
expr z3::store ( expr const &  a,
int  i,
expr const &  v 
)
inline

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

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

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

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

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

1879  {
1880  return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
1881  }
expr store(expr const &a, int i, int v)
Definition: z3++.h:1879
check_result z3::to_check_result ( Z3_lbool  l)
inline

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

Referenced by solver::check(), and optimize::check().

1265  {
1266  if (l == Z3_L_TRUE) return sat;
1267  else if (l == Z3_L_FALSE) return unsat;
1268  return unknown;
1269  }
Definition: z3++.h:1255
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 936 of file z3++.h.

Referenced by udiv(), uge(), ugt(), ule(), and ult().

936  {
937  c.check_error();
938  assert(Z3_get_ast_kind(c, a) == Z3_APP_AST ||
939  Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
940  Z3_get_ast_kind(c, a) == Z3_VAR_AST ||
942  return expr(c, a);
943  }
Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a)
Return the kind of the given AST.
func_decl z3::to_func_decl ( context c,
Z3_func_decl  f 
)
inline

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

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

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

1840 { Z3_ast r = Z3_mk_int2real(a.ctx(), a); a.check_error(); return expr(a.ctx(), r); }
Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1)
Coerce an integer to a real.
sort z3::to_sort ( context c,
Z3_sort  s 
)
inline

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

Referenced by context::enumeration_sort(), and context::uninterpreted_sort().

945  {
946  c.check_error();
947  return sort(c, s);
948  }
tactic z3::try_for ( tactic const &  t,
unsigned  ms 
)
inline

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

1487  {
1488  Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
1489  t.check_error();
1490  return tactic(t.ctx(), r);
1491  }
Z3_tactic Z3_API Z3_tactic_try_for(Z3_context c, Z3_tactic t, unsigned ms)
Return a tactic that applies t to a given goal for ms milliseconds. If t does not terminate in ms mil...
expr z3::udiv ( expr const &  a,
expr const &  b 
)
inline

unsigned division operator for bitvectors.

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

Referenced by udiv().

982 { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }
Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned division.
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...
Definition: z3++.h:936
expr z3::udiv ( expr const &  a,
int  b 
)
inline

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

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

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

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

unsigned greater than or equal to operator for bitvectors.

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

Referenced by uge().

970 { return to_expr(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b)); }
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
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...
Definition: z3++.h:936
expr z3::uge ( expr const &  a,
int  b 
)
inline

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

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

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

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

unsigned greater than operator for bitvectors.

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

Referenced by ugt().

976 { return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }
Z3_ast Z3_API Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than.
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...
Definition: z3++.h:936
expr z3::ugt ( expr const &  a,
int  b 
)
inline

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

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

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

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

unsigned less than or equal to operator for bitvectors.

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

Referenced by ule().

958 { return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }
Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than or equal to.
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...
Definition: z3++.h:936
expr z3::ule ( expr const &  a,
int  b 
)
inline

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

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

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

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

unsigned less than operator for bitvectors.

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

Referenced by ult().

964 { return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); }
Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than.
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...
Definition: z3++.h:936
expr z3::ult ( expr const &  a,
int  b 
)
inline

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

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

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

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

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

1613  {
1614  check_context(p, t);
1615  Z3_tactic r = Z3_tactic_when(t.ctx(), p, t);
1616  t.check_error();
1617  return tactic(t.ctx(), r);
1618  }
Z3_tactic Z3_API Z3_tactic_when(Z3_context c, Z3_probe p, Z3_tactic t)
Return a tactic that applies t to a given goal is the probe p evaluates to true. If p evaluates to fa...
void check_context(object const &a, object const &b)
Definition: z3++.h:281
tactic z3::with ( tactic const &  t,
params const &  p 
)
inline

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

1482  {
1483  Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
1484  t.check_error();
1485  return tactic(t.ctx(), r);
1486  }
Z3_tactic Z3_API Z3_tactic_using_params(Z3_context c, Z3_tactic t, Z3_params p)
Return a tactic that applies t using the given set of parameters.