Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
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
 
singleton  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  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)
 
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.

Function Documentation

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

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

Referenced by cond(), const_array(), exists(), forall(), context::function(), ite(), pw(), select(), store(), and when().

276 { assert(a.m_ctx == b.m_ctx); }
tactic z3::cond ( probe const &  p,
tactic const &  t1,
tactic const &  t2 
)
inline

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

1527  {
1528  check_context(p, t1); check_context(p, t2);
1529  Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2);
1530  t1.check_error();
1531  return tactic(t1.ctx(), r);
1532  }
Z3_tactic Z3_API Z3_tactic_cond(__in Z3_context c, __in Z3_probe p, __in Z3_tactic t1, __in 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:276
expr z3::const_array ( sort const &  d,
expr const &  v 
)
inline

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

1783  {
1784  check_context(d, v);
1785  Z3_ast r = Z3_mk_const_array(d.ctx(), d, v);
1786  d.check_error();
1787  return expr(d.ctx(), r);
1788  }
void check_context(object const &a, object const &b)
Definition: z3++.h:276
Z3_ast Z3_API Z3_mk_const_array(__in Z3_context c, __in Z3_sort domain, __in Z3_ast v)
Create the constant array.
expr z3::distinct ( expr_vector const &  args)
inline

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

1100  {
1101  assert(args.size() > 0);
1102  context& ctx = args[0].ctx();
1103  array<Z3_ast> _args(args);
1104  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
1105  ctx.check_error();
1106  return expr(ctx, r);
1107  }
Z3_ast Z3_API Z3_mk_distinct(__in Z3_context c, __in unsigned num_args, __in_ecount(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 344 of file z3++.h.

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

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

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

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

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

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

1084  {
1085  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1086  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1087  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1088  }
System.IntPtr Z3_app
Definition: Native.cs:14
Z3_ast Z3_API Z3_mk_exists_const(__in Z3_context c, unsigned weight, unsigned num_bound, __in_ecount(num_bound) Z3_app const bound[], unsigned num_patterns, __in_ecount(num_patterns) Z3_pattern const patterns[], __in Z3_ast body)
Similar to Z3_mk_forall_const.
void check_context(object const &a, object const &b)
Definition: z3++.h:276
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.

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

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

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

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

1516  {
1517  Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
1518  p.check_error();
1519  return tactic(p.ctx(), r);
1520  }
Z3_tactic Z3_API Z3_tactic_fail_if(__in Z3_context c, __in 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 1050 of file z3++.h.

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

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

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

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

1060  {
1061  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1062  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1063  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1064  }
Z3_ast Z3_API Z3_mk_forall_const(__in Z3_context c, unsigned weight, unsigned num_bound, __in_ecount(num_bound) Z3_app const bound[], unsigned num_patterns, __in_ecount(num_patterns) Z3_pattern const patterns[], __in Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables...
System.IntPtr Z3_app
Definition: Native.cs:14
void check_context(object const &a, object const &b)
Definition: z3++.h:276
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.

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

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

1070  {
1071  array<Z3_app> vars(xs);
1072  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);
1073  }
Z3_ast Z3_API Z3_mk_forall_const(__in Z3_context c, unsigned weight, unsigned num_bound, __in_ecount(num_bound) Z3_app const bound[], unsigned num_patterns, __in_ecount(num_patterns) Z3_pattern const patterns[], __in 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 1743 of file z3++.h.

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

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

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

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

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

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

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

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

1755  {
1756  return range.ctx().function(name, d1, d2, d3, range);
1757  }
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 1758 of file z3++.h.

1758  {
1759  return range.ctx().function(name, d1, d2, d3, d4, range);
1760  }
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 1761 of file z3++.h.

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

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

Referenced by implies().

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

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

892 { return implies(b.ctx().bool_val(a), b); }
expr implies(bool a, expr const &b)
Definition: z3++.h:892
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 914 of file z3++.h.

914  {
915  check_context(c, t); check_context(c, e);
916  assert(c.is_bool());
917  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
918  c.check_error();
919  return expr(c.ctx(), r);
920  }
Z3_ast Z3_API Z3_mk_ite(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2, __in Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
void check_context(object const &a, object const &b)
Definition: z3++.h:276
std::ostream& z3::operator<< ( std::ostream &  out,
check_result  r 
)
inline

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

1242  {
1243  if (r == unsat) out << "unsat";
1244  else if (r == sat) out << "sat";
1245  else out << "unknown";
1246  return out;
1247  }
Definition: z3++.h:1239
expr z3::pw ( expr const &  a,
expr const &  b 
)
inline

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

Referenced by pw().

894  {
895  assert(a.is_arith() && b.is_arith());
896  check_context(a, b);
897  Z3_ast r = Z3_mk_power(a.ctx(), a, b);
898  a.check_error();
899  return expr(a.ctx(), r);
900  }
Z3_ast Z3_API Z3_mk_power(__in Z3_context c, __in Z3_ast arg1, __in Z3_ast arg2)
Create an AST node representing arg1^arg2.
void check_context(object const &a, object const &b)
Definition: z3++.h:276
expr z3::pw ( expr const &  a,
int  b 
)
inline

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

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

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

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

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

1440  {
1441  Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
1442  t.check_error();
1443  return tactic(t.ctx(), r);
1444  }
Z3_tactic Z3_API Z3_tactic_repeat(__in Z3_context c, __in 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 1765 of file z3++.h.

Referenced by select().

1765  {
1766  check_context(a, i);
1767  Z3_ast r = Z3_mk_select(a.ctx(), a, i);
1768  a.check_error();
1769  return expr(a.ctx(), r);
1770  }
Z3_ast Z3_API Z3_mk_select(__in Z3_context c, __in Z3_ast a, __in Z3_ast i)
Array read. The argument a is the array and i is the index of the array that gets read...
void check_context(object const &a, object const &b)
Definition: z3++.h:276
expr z3::select ( expr const &  a,
int  i 
)
inline

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

1771 { return select(a, a.ctx().num_val(i, a.get_sort().array_domain())); }
expr select(expr const &a, int i)
Definition: z3++.h:1771
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(__in Z3_string param_id, __in 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(__in Z3_string param_id, __in 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(__in Z3_string param_id, __in 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 1772 of file z3++.h.

Referenced by store().

1772  {
1773  check_context(a, i); check_context(a, v);
1774  Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
1775  a.check_error();
1776  return expr(a.ctx(), r);
1777  }
void check_context(object const &a, object const &b)
Definition: z3++.h:276
Z3_ast Z3_API Z3_mk_store(__in Z3_context c, __in Z3_ast a, __in Z3_ast i, __in Z3_ast v)
Array update.
expr z3::store ( expr const &  a,
int  i,
expr const &  v 
)
inline

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

1778 { 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:1780
expr z3::store ( expr const &  a,
expr  i,
int  v 
)
inline

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

1779 { 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:1780
expr z3::store ( expr const &  a,
int  i,
int  v 
)
inline

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

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

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

Referenced by solver::check().

1249  {
1250  if (l == Z3_L_TRUE) return sat;
1251  else if (l == Z3_L_FALSE) return unsat;
1252  return unknown;
1253  }
Definition: z3++.h:1239
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().

927  {
928  c.check_error();
929  assert(Z3_get_ast_kind(c, a) == Z3_APP_AST ||
930  Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
931  Z3_get_ast_kind(c, a) == Z3_VAR_AST ||
933  return expr(c, a);
934  }
Z3_ast_kind Z3_API Z3_get_ast_kind(__in Z3_context c, __in 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 941 of file z3++.h.

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

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

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

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

Referenced by context::enumeration_sort().

936  {
937  c.check_error();
938  return sort(c, s);
939  }
tactic z3::try_for ( tactic const &  t,
unsigned  ms 
)
inline

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

1451  {
1452  Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
1453  t.check_error();
1454  return tactic(t.ctx(), r);
1455  }
Z3_tactic Z3_API Z3_tactic_try_for(__in Z3_context c, __in Z3_tactic t, __in 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 973 of file z3++.h.

Referenced by udiv().

973 { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }
Z3_ast Z3_API Z3_mk_bvudiv(__in Z3_context c, __in Z3_ast t1, __in 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:927
expr z3::udiv ( expr const &  a,
int  b 
)
inline

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

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

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

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

unsigned greater than or equal to operator for bitvectors.

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

Referenced by uge().

961 { return to_expr(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b)); }
Z3_ast Z3_API Z3_mk_bvuge(__in Z3_context c, __in Z3_ast t1, __in 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:927
expr z3::uge ( expr const &  a,
int  b 
)
inline

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

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

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

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

unsigned greater than operator for bitvectors.

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

Referenced by ugt().

967 { return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }
Z3_ast Z3_API Z3_mk_bvugt(__in Z3_context c, __in Z3_ast t1, __in 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:927
expr z3::ugt ( expr const &  a,
int  b 
)
inline

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

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

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

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

unsigned less than or equal to operator for bitvectors.

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

Referenced by ule().

949 { return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }
Z3_ast Z3_API Z3_mk_bvule(__in Z3_context c, __in Z3_ast t1, __in 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:927
expr z3::ule ( expr const &  a,
int  b 
)
inline

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

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

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

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

unsigned less than operator for bitvectors.

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

Referenced by ult().

955 { return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); }
Z3_ast Z3_API Z3_mk_bvult(__in Z3_context c, __in Z3_ast t1, __in 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:927
expr z3::ult ( expr const &  a,
int  b 
)
inline

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

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

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

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

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

1521  {
1522  check_context(p, t);
1523  Z3_tactic r = Z3_tactic_when(t.ctx(), p, t);
1524  t.check_error();
1525  return tactic(t.ctx(), r);
1526  }
Z3_tactic Z3_API Z3_tactic_when(__in Z3_context c, __in Z3_probe p, __in 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:276
tactic z3::with ( tactic const &  t,
params const &  p 
)
inline

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

1446  {
1447  Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
1448  t.check_error();
1449  return tactic(t.ctx(), r);
1450  }
Z3_tactic Z3_API Z3_tactic_using_params(__in Z3_context c, __in Z3_tactic t, __in Z3_params p)
Return a tactic that applies t using the given set of parameters.