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  param_descrs
 
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 ()
 
std::ostream & operator<< (std::ostream &out, exception const &e)
 
check_result to_check_result (Z3_lbool l)
 
void check_context (object const &a, object const &b)
 
std::ostream & operator<< (std::ostream &out, symbol const &s)
 
std::ostream & operator<< (std::ostream &out, param_descrs const &d)
 
std::ostream & operator<< (std::ostream &out, params const &p)
 
std::ostream & operator<< (std::ostream &out, ast const &n)
 
bool eq (ast const &a, ast const &b)
 
expr implies (expr const &a, expr 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 operator! (expr const &a)
 
expr operator && (expr const &a, expr const &b)
 
expr operator && (expr const &a, bool b)
 
expr operator && (bool a, expr const &b)
 
expr operator|| (expr const &a, expr const &b)
 
expr operator|| (expr const &a, bool b)
 
expr operator|| (bool a, expr const &b)
 
expr operator== (expr const &a, expr const &b)
 
expr operator== (expr const &a, int b)
 
expr operator== (int a, expr const &b)
 
expr operator!= (expr const &a, expr const &b)
 
expr operator!= (expr const &a, int b)
 
expr operator!= (int a, expr const &b)
 
expr operator+ (expr const &a, expr const &b)
 
expr operator+ (expr const &a, int b)
 
expr operator+ (int a, expr const &b)
 
expr operator* (expr const &a, expr const &b)
 
expr operator* (expr const &a, int b)
 
expr operator* (int a, expr const &b)
 
expr operator>= (expr const &a, expr const &b)
 
expr operator/ (expr const &a, expr const &b)
 
expr operator/ (expr const &a, int b)
 
expr operator/ (int a, expr const &b)
 
expr operator- (expr const &a)
 
expr operator- (expr const &a, expr const &b)
 
expr operator- (expr const &a, int b)
 
expr operator- (int a, expr const &b)
 
expr operator<= (expr const &a, expr const &b)
 
expr operator<= (expr const &a, int b)
 
expr operator<= (int a, expr const &b)
 
expr operator>= (expr const &a, int b)
 
expr operator>= (int a, expr const &b)
 
expr operator< (expr const &a, expr const &b)
 
expr operator< (expr const &a, int b)
 
expr operator< (int a, expr const &b)
 
expr operator> (expr const &a, expr const &b)
 
expr operator> (expr const &a, int b)
 
expr operator> (int a, expr const &b)
 
expr operator & (expr const &a, expr const &b)
 
expr operator & (expr const &a, int b)
 
expr operator & (int a, expr const &b)
 
expr operator^ (expr const &a, expr const &b)
 
expr operator^ (expr const &a, int b)
 
expr operator^ (int a, expr const &b)
 
expr operator| (expr const &a, expr const &b)
 
expr operator| (expr const &a, int b)
 
expr operator| (int a, expr const &b)
 
expr operator~ (expr const &a)
 
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 srem (expr const &a, expr const &b)
 signed reminder operator for bitvectors More...
 
expr srem (expr const &a, int b)
 
expr srem (int a, expr const &b)
 
expr urem (expr const &a, expr const &b)
 unsigned reminder operator for bitvectors More...
 
expr urem (expr const &a, int b)
 
expr urem (int a, expr const &b)
 
expr shl (expr const &a, expr const &b)
 shift left operator for bitvectors More...
 
expr shl (expr const &a, int b)
 
expr shl (int a, expr const &b)
 
expr lshr (expr const &a, expr const &b)
 logic shift right operator for bitvectors More...
 
expr lshr (expr const &a, int b)
 
expr lshr (int a, expr const &b)
 
expr ashr (expr const &a, expr const &b)
 arithmetic shift right operator for bitvectors More...
 
expr ashr (expr const &a, int b)
 
expr ashr (int a, expr const &b)
 
expr zext (expr const &a, unsigned i)
 Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i, where m is the size of the given bit-vector. More...
 
expr sext (expr const &a, unsigned i)
 Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector. More...
 
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)
 
expr concat (expr_vector const &args)
 
expr mk_or (expr_vector const &args)
 
expr mk_and (expr_vector const &args)
 
std::ostream & operator<< (std::ostream &out, model const &m)
 
std::ostream & operator<< (std::ostream &out, stats const &s)
 
std::ostream & operator<< (std::ostream &out, check_result r)
 
std::ostream & operator<< (std::ostream &out, solver const &s)
 
std::ostream & operator<< (std::ostream &out, goal const &g)
 
std::ostream & operator<< (std::ostream &out, apply_result const &r)
 
tactic operator & (tactic const &t1, tactic const &t2)
 
tactic operator| (tactic const &t1, tactic const &t2)
 
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)
 
probe operator<= (probe const &p1, probe const &p2)
 
probe operator<= (probe const &p1, double p2)
 
probe operator<= (double p1, probe const &p2)
 
probe operator>= (probe const &p1, probe const &p2)
 
probe operator>= (probe const &p1, double p2)
 
probe operator>= (double p1, probe const &p2)
 
probe operator< (probe const &p1, probe const &p2)
 
probe operator< (probe const &p1, double p2)
 
probe operator< (double p1, probe const &p2)
 
probe operator> (probe const &p1, probe const &p2)
 
probe operator> (probe const &p1, double p2)
 
probe operator> (double p1, probe const &p2)
 
probe operator== (probe const &p1, probe const &p2)
 
probe operator== (probe const &p1, double p2)
 
probe operator== (double p1, probe const &p2)
 
probe operator && (probe const &p1, probe const &p2)
 
probe operator|| (probe const &p1, probe const &p2)
 
probe operator! (probe const &p)
 
std::ostream & operator<< (std::ostream &out, optimize const &s)
 
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)
 
expr empty_set (sort const &s)
 
expr full_set (sort const &s)
 
expr set_add (expr const &s, expr const &e)
 
expr set_del (expr const &s, expr const &e)
 
expr set_union (expr const &a, expr const &b)
 
expr set_intersect (expr const &a, expr const &b)
 
expr set_difference (expr const &a, expr const &b)
 
expr set_complement (expr const &a)
 
expr set_member (expr const &s, expr const &e)
 
expr set_subset (expr const &a, expr const &b)
 
expr empty (sort const &s)
 
expr suffixof (expr const &a, expr const &b)
 
expr prefixof (expr const &a, expr const &b)
 
expr indexof (expr const &s, expr const &substr, expr const &offset)
 
expr to_re (expr const &s)
 
expr in_re (expr const &s, expr const &re)
 
expr plus (expr const &re)
 
expr option (expr const &re)
 
expr star (expr const &re)
 
expr interpolant (expr const &a)
 

Detailed Description

Z3 C++ namespace.

Typedef Documentation

§ ast_vector

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

§ expr_vector

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

§ func_decl_vector

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

§ sort_vector

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

Enumeration Type Documentation

§ check_result

Enumerator
unsat 
sat 
unknown 

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

120  {
121  unsat, sat, unknown
122  };
Definition: z3++.h:121

Function Documentation

§ ashr() [1/3]

expr z3::ashr ( expr const &  a,
expr const &  b 
)
inline

arithmetic shift right operator for bitvectors

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

Referenced by ashr().

1331 { return to_expr(a.ctx(), Z3_mk_bvashr(a.ctx(), a, b)); }
Z3_ast Z3_API Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2)
Arithmetic shift right.
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:1250

§ ashr() [2/3]

expr z3::ashr ( expr const &  a,
int  b 
)
inline

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

1332 { return ashr(a, a.ctx().num_val(b, a.get_sort())); }
expr ashr(int a, expr const &b)
Definition: z3++.h:1333

§ ashr() [3/3]

expr z3::ashr ( int  a,
expr const &  b 
)
inline

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

1333 { return ashr(b.ctx().num_val(a, b.get_sort()), b); }
expr ashr(int a, expr const &b)
Definition: z3++.h:1333

§ check_context()

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

§ concat() [1/2]

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

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

Referenced by expr::body(), and operator+().

1478  {
1479  check_context(a, b);
1480  Z3_ast r;
1481  if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
1482  Z3_ast _args[2] = { a, b };
1483  r = Z3_mk_seq_concat(a.ctx(), 2, _args);
1484  }
1485  else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
1486  Z3_ast _args[2] = { a, b };
1487  r = Z3_mk_re_concat(a.ctx(), 2, _args);
1488  }
1489  else {
1490  r = Z3_mk_concat(a.ctx(), a, b);
1491  }
1492  a.ctx().check_error();
1493  return expr(a.ctx(), r);
1494  }
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:336

§ concat() [2/2]

expr z3::concat ( expr_vector const &  args)
inline

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

1496  {
1497  Z3_ast r;
1498  assert(args.size() > 0);
1499  if (args.size() == 1) {
1500  return args[0];
1501  }
1502  context& ctx = args[0].ctx();
1503  array<Z3_ast> _args(args);
1504  if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
1505  r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
1506  }
1507  else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
1508  r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
1509  }
1510  else {
1511  r = _args[args.size()-1];
1512  for (unsigned i = args.size()-1; i > 0; ) {
1513  --i;
1514  r = Z3_mk_concat(ctx, _args[i], r);
1515  ctx.check_error();
1516  }
1517  }
1518  ctx.check_error();
1519  return expr(ctx, r);
1520  }
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.

§ cond()

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

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

2077  {
2078  check_context(p, t1); check_context(p, t2);
2079  Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2);
2080  t1.check_error();
2081  return tactic(t1.ctx(), r);
2082  }
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:336

§ const_array()

expr z3::const_array ( sort const &  d,
expr const &  v 
)
inline

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

2359  {
2360  MK_EXPR2(Z3_mk_const_array, d, v);
2361  }
Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v)
Create the constant array.
#define MK_EXPR2(_fn, _arg1, _arg2)
Definition: z3++.h:2353

§ distinct()

expr z3::distinct ( expr_vector const &  args)
inline

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

Referenced by expr::body().

1469  {
1470  assert(args.size() > 0);
1471  context& ctx = args[0].ctx();
1472  array<Z3_ast> _args(args);
1473  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
1474  ctx.check_error();
1475  return expr(ctx, r);
1476  }
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]).

§ empty()

expr z3::empty ( sort const &  s)
inline

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

2415  {
2416  Z3_ast r = Z3_mk_seq_empty(s.ctx(), s);
2417  s.check_error();
2418  return expr(s.ctx(), r);
2419  }

§ empty_set()

expr z3::empty_set ( sort const &  s)
inline

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

2363  {
2365  }
Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain)
Create the empty set.
#define MK_EXPR1(_fn, _arg)
Definition: z3++.h:2348

§ eq()

bool z3::eq ( ast const &  a,
ast const &  b 
)
inline

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

Referenced by ast::hash().

433 { return Z3_is_eq_ast(a.ctx(), a, b) != 0; }

§ exists() [1/5]

expr z3::exists ( expr const &  x,
expr const &  b 
)
inline

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

1443  {
1444  check_context(x, b);
1445  Z3_app vars[] = {(Z3_app) x};
1446  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1447  }
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ exists() [2/5]

expr z3::exists ( expr const &  x1,
expr const &  x2,
expr const &  b 
)
inline

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

1448  {
1449  check_context(x1, b); check_context(x2, b);
1450  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1451  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1452  }
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ exists() [3/5]

expr z3::exists ( expr const &  x1,
expr const &  x2,
expr const &  x3,
expr const &  b 
)
inline

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

1453  {
1454  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1455  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1456  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1457  }
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ exists() [4/5]

expr z3::exists ( expr const &  x1,
expr const &  x2,
expr const &  x3,
expr const &  x4,
expr const &  b 
)
inline

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

1458  {
1459  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
1460  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1461  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1462  }
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ exists() [5/5]

expr z3::exists ( expr_vector const &  xs,
expr const &  b 
)
inline

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

1463  {
1464  array<Z3_app> vars(xs);
1465  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);
1466  }

§ fail_if()

tactic z3::fail_if ( probe const &  p)
inline

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

2066  {
2067  Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
2068  p.check_error();
2069  return tactic(p.ctx(), r);
2070  }
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.

§ forall() [1/5]

expr z3::forall ( expr const &  x,
expr const &  b 
)
inline

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

1419  {
1420  check_context(x, b);
1421  Z3_app vars[] = {(Z3_app) x};
1422  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1423  }
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ forall() [2/5]

expr z3::forall ( expr const &  x1,
expr const &  x2,
expr const &  b 
)
inline

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

1424  {
1425  check_context(x1, b); check_context(x2, b);
1426  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1427  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1428  }
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ forall() [3/5]

expr z3::forall ( expr const &  x1,
expr const &  x2,
expr const &  x3,
expr const &  b 
)
inline

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

1429  {
1430  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1431  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1432  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1433  }
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ forall() [4/5]

expr z3::forall ( expr const &  x1,
expr const &  x2,
expr const &  x3,
expr const &  x4,
expr const &  b 
)
inline

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

1434  {
1435  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
1436  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1437  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1438  }
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ forall() [5/5]

expr z3::forall ( expr_vector const &  xs,
expr const &  b 
)
inline

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

1439  {
1440  array<Z3_app> vars(xs);
1441  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);
1442  }

§ full_set()

expr z3::full_set ( sort const &  s)
inline

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

2367  {
2369  }
Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain)
Create the full set.
#define MK_EXPR1(_fn, _arg)
Definition: z3++.h:2348

§ function() [1/7]

func_decl z3::function ( symbol const &  name,
unsigned  arity,
sort const *  domain,
sort const &  range 
)
inline

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

2307  {
2308  return range.ctx().function(name, arity, domain, range);
2309  }

§ function() [2/7]

func_decl z3::function ( char const *  name,
unsigned  arity,
sort const *  domain,
sort const &  range 
)
inline

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

2310  {
2311  return range.ctx().function(name, arity, domain, range);
2312  }

§ function() [3/7]

func_decl z3::function ( char const *  name,
sort const &  domain,
sort const &  range 
)
inline

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

2313  {
2314  return range.ctx().function(name, domain, range);
2315  }

§ function() [4/7]

func_decl z3::function ( char const *  name,
sort const &  d1,
sort const &  d2,
sort const &  range 
)
inline

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

2316  {
2317  return range.ctx().function(name, d1, d2, range);
2318  }

§ function() [5/7]

func_decl z3::function ( char const *  name,
sort const &  d1,
sort const &  d2,
sort const &  d3,
sort const &  range 
)
inline

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

2319  {
2320  return range.ctx().function(name, d1, d2, d3, range);
2321  }

§ function() [6/7]

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 2322 of file z3++.h.

2322  {
2323  return range.ctx().function(name, d1, d2, d3, d4, range);
2324  }

§ function() [7/7]

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 2325 of file z3++.h.

2325  {
2326  return range.ctx().function(name, d1, d2, d3, d4, d5, range);
2327  }

§ implies() [1/3]

expr z3::implies ( expr const &  a,
expr const &  b 
)
inline

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

Referenced by expr::body(), and implies().

961  {
962  check_context(a, b);
963  assert(a.is_bool() && b.is_bool());
964  Z3_ast r = Z3_mk_implies(a.ctx(), a, b);
965  a.check_error();
966  return expr(a.ctx(), r);
967  }
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ implies() [2/3]

expr z3::implies ( expr const &  a,
bool  b 
)
inline

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

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

§ implies() [3/3]

expr z3::implies ( bool  a,
expr const &  b 
)
inline

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

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

§ in_re()

expr z3::in_re ( expr const &  s,
expr const &  re 
)
inline

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

2443  {
2444  check_context(s, re);
2445  Z3_ast r = Z3_mk_seq_in_re(s.ctx(), s, re);
2446  s.check_error();
2447  return expr(s.ctx(), r);
2448  }
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ indexof()

expr z3::indexof ( expr const &  s,
expr const &  substr,
expr const &  offset 
)
inline

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

2432  {
2433  check_context(s, substr); check_context(s, offset);
2434  Z3_ast r = Z3_mk_seq_index(s.ctx(), s, substr, offset);
2435  s.check_error();
2436  return expr(s.ctx(), r);
2437  }
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ interpolant()

expr z3::interpolant ( expr const &  a)
inline

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

2465  {
2466  return expr(a.ctx(), Z3_mk_interpolant(a.ctx(), a));
2467  }
Z3_ast Z3_API Z3_mk_interpolant(Z3_context c, Z3_ast a)
Create an AST node marking a formula position for interpolation.

§ ite()

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 1237 of file z3++.h.

Referenced by expr::body().

1237  {
1238  check_context(c, t); check_context(c, e);
1239  assert(c.is_bool());
1240  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
1241  c.check_error();
1242  return expr(c.ctx(), r);
1243  }
void check_context(object const &a, object const &b)
Definition: z3++.h:336
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).

§ lshr() [1/3]

expr z3::lshr ( expr const &  a,
expr const &  b 
)
inline

logic shift right operator for bitvectors

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

Referenced by lshr().

1324 { return to_expr(a.ctx(), Z3_mk_bvlshr(a.ctx(), a, b)); }
Z3_ast Z3_API Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2)
Logical shift right.
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:1250

§ lshr() [2/3]

expr z3::lshr ( expr const &  a,
int  b 
)
inline

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

1325 { return lshr(a, a.ctx().num_val(b, a.get_sort())); }
expr lshr(int a, expr const &b)
Definition: z3++.h:1326

§ lshr() [3/3]

expr z3::lshr ( int  a,
expr const &  b 
)
inline

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

1326 { return lshr(b.ctx().num_val(a, b.get_sort()), b); }
expr lshr(int a, expr const &b)
Definition: z3++.h:1326

§ mk_and()

expr z3::mk_and ( expr_vector const &  args)
inline

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

Referenced by expr::body().

1528  {
1529  array<Z3_ast> _args(args);
1530  Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
1531  args.check_error();
1532  return expr(args.ctx(), r);
1533  }
Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].

§ mk_or()

expr z3::mk_or ( expr_vector const &  args)
inline

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

Referenced by expr::body().

1522  {
1523  array<Z3_ast> _args(args);
1524  Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
1525  args.check_error();
1526  return expr(args.ctx(), r);
1527  }
Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] or ... or args[num_args-1].

§ operator &() [1/4]

expr z3::operator& ( expr const &  a,
expr const &  b 
)
inline

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

Referenced by expr::body(), and tactic::help().

1214 { check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); return expr(a.ctx(), r); }
void check_context(object const &a, object const &b)
Definition: z3++.h:336
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.

§ operator &() [2/4]

expr z3::operator& ( expr const &  a,
int  b 
)
inline

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

1215 { return a & a.ctx().num_val(b, a.get_sort()); }

§ operator &() [3/4]

expr z3::operator& ( int  a,
expr const &  b 
)
inline

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

1216 { return b.ctx().num_val(a, b.get_sort()) & b; }

§ operator &() [4/4]

tactic z3::operator& ( tactic const &  t1,
tactic const &  t2 
)
inline

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

1896  {
1897  check_context(t1, t2);
1898  Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
1899  t1.check_error();
1900  return tactic(t1.ctx(), r);
1901  }
void check_context(object const &a, object const &b)
Definition: z3++.h:336
Z3_tactic Z3_API Z3_tactic_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and t2 to every subgoal produced by t1...

§ operator &&() [1/4]

expr z3::operator&& ( expr const &  a,
expr const &  b 
)
inline
Precondition
a.is_bool()
b.is_bool()

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

Referenced by expr::body(), and probe::operator()().

990  {
991  check_context(a, b);
992  assert(a.is_bool() && b.is_bool());
993  Z3_ast args[2] = { a, b };
994  Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
995  a.check_error();
996  return expr(a.ctx(), r);
997  }
Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ operator &&() [2/4]

expr z3::operator&& ( expr const &  a,
bool  b 
)
inline
Precondition
a.is_bool()

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

999 { return a && a.ctx().bool_val(b); }

§ operator &&() [3/4]

expr z3::operator&& ( bool  a,
expr const &  b 
)
inline
Precondition
b.is_bool()

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

1000 { return b.ctx().bool_val(a) && b; }

§ operator &&() [4/4]

probe z3::operator&& ( probe const &  p1,
probe const &  p2 
)
inline

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

1995  {
1996  check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1997  }
Z3_probe Z3_API Z3_probe_and(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when p1 and p2 evaluates to true.
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ operator!() [1/2]

expr z3::operator! ( expr const &  a)
inline
Precondition
a.is_bool()

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

Referenced by expr::body(), and probe::operator()().

983  {
984  assert(a.is_bool());
985  Z3_ast r = Z3_mk_not(a.ctx(), a);
986  a.check_error();
987  return expr(a.ctx(), r);
988  }
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).

§ operator!() [2/2]

probe z3::operator! ( probe const &  p)
inline

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

2001  {
2002  Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
2003  }
Z3_probe Z3_API Z3_probe_not(Z3_context x, Z3_probe p)
Return a probe that evaluates to "true" when p does not evaluate to true.

§ operator!=() [1/3]

expr z3::operator!= ( expr const &  a,
expr const &  b 
)
inline

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

Referenced by expr::body().

1024  {
1025  check_context(a, b);
1026  Z3_ast args[2] = { a, b };
1027  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1028  a.check_error();
1029  return expr(a.ctx(), r);
1030  }
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]).
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ operator!=() [2/3]

expr z3::operator!= ( expr const &  a,
int  b 
)
inline

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

1031 { assert(a.is_arith() || a.is_bv()); return a != a.ctx().num_val(b, a.get_sort()); }

§ operator!=() [3/3]

expr z3::operator!= ( int  a,
expr const &  b 
)
inline

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

1032 { assert(b.is_arith() || b.is_bv()); return b.ctx().num_val(a, b.get_sort()) != b; }

§ operator*() [1/3]

expr z3::operator* ( expr const &  a,
expr const &  b 
)
inline

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

Referenced by expr::body().

1061  {
1062  check_context(a, b);
1063  Z3_ast r = 0;
1064  if (a.is_arith() && b.is_arith()) {
1065  Z3_ast args[2] = { a, b };
1066  r = Z3_mk_mul(a.ctx(), 2, args);
1067  }
1068  else if (a.is_bv() && b.is_bv()) {
1069  r = Z3_mk_bvmul(a.ctx(), a, b);
1070  }
1071  else {
1072  // operator is not supported by given arguments.
1073  assert(false);
1074  }
1075  a.check_error();
1076  return expr(a.ctx(), r);
1077  }
Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] * ... * args[num_args-1].
void check_context(object const &a, object const &b)
Definition: z3++.h:336
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two&#39;s complement multiplication.

§ operator*() [2/3]

expr z3::operator* ( expr const &  a,
int  b 
)
inline

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

1078 { return a * a.ctx().num_val(b, a.get_sort()); }

§ operator*() [3/3]

expr z3::operator* ( int  a,
expr const &  b 
)
inline

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

1079 { return b.ctx().num_val(a, b.get_sort()) * b; }

§ operator+() [1/3]

expr z3::operator+ ( expr const &  a,
expr const &  b 
)
inline

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

Referenced by expr::body().

1034  {
1035  check_context(a, b);
1036  Z3_ast r = 0;
1037  if (a.is_arith() && b.is_arith()) {
1038  Z3_ast args[2] = { a, b };
1039  r = Z3_mk_add(a.ctx(), 2, args);
1040  }
1041  else if (a.is_bv() && b.is_bv()) {
1042  r = Z3_mk_bvadd(a.ctx(), a, b);
1043  }
1044  else if (a.is_seq() && b.is_seq()) {
1045  return concat(a, b);
1046  }
1047  else if (a.is_re() && b.is_re()) {
1048  Z3_ast _args[2] = { a, b };
1049  r = Z3_mk_re_union(a.ctx(), 2, _args);
1050  }
1051  else {
1052  // operator is not supported by given arguments.
1053  assert(false);
1054  }
1055  a.check_error();
1056  return expr(a.ctx(), r);
1057  }
Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] + ... + args[num_args-1].
expr concat(expr_vector const &args)
Definition: z3++.h:1496
void check_context(object const &a, object const &b)
Definition: z3++.h:336
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two&#39;s complement addition.

§ operator+() [2/3]

expr z3::operator+ ( expr const &  a,
int  b 
)
inline

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

1058 { return a + a.ctx().num_val(b, a.get_sort()); }

§ operator+() [3/3]

expr z3::operator+ ( int  a,
expr const &  b 
)
inline

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

1059 { return b.ctx().num_val(a, b.get_sort()) + b; }

§ operator-() [1/4]

expr z3::operator- ( expr const &  a)
inline

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

Referenced by expr::body().

1118  {
1119  Z3_ast r = 0;
1120  if (a.is_arith()) {
1121  r = Z3_mk_unary_minus(a.ctx(), a);
1122  }
1123  else if (a.is_bv()) {
1124  r = Z3_mk_bvneg(a.ctx(), a);
1125  }
1126  else {
1127  // operator is not supported by given arguments.
1128  assert(false);
1129  }
1130  a.check_error();
1131  return expr(a.ctx(), r);
1132  }
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two&#39;s complement unary minus.

§ operator-() [2/4]

expr z3::operator- ( expr const &  a,
expr const &  b 
)
inline

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

1134  {
1135  check_context(a, b);
1136  Z3_ast r = 0;
1137  if (a.is_arith() && b.is_arith()) {
1138  Z3_ast args[2] = { a, b };
1139  r = Z3_mk_sub(a.ctx(), 2, args);
1140  }
1141  else if (a.is_bv() && b.is_bv()) {
1142  r = Z3_mk_bvsub(a.ctx(), a, b);
1143  }
1144  else {
1145  // operator is not supported by given arguments.
1146  assert(false);
1147  }
1148  a.check_error();
1149  return expr(a.ctx(), r);
1150  }
Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] - ... - args[num_args - 1].
void check_context(object const &a, object const &b)
Definition: z3++.h:336
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two&#39;s complement subtraction.

§ operator-() [3/4]

expr z3::operator- ( expr const &  a,
int  b 
)
inline

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

1151 { return a - a.ctx().num_val(b, a.get_sort()); }

§ operator-() [4/4]

expr z3::operator- ( int  a,
expr const &  b 
)
inline

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

1152 { return b.ctx().num_val(a, b.get_sort()) - b; }

§ operator/() [1/3]

expr z3::operator/ ( expr const &  a,
expr const &  b 
)
inline

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

Referenced by expr::body().

1099  {
1100  check_context(a, b);
1101  Z3_ast r = 0;
1102  if (a.is_arith() && b.is_arith()) {
1103  r = Z3_mk_div(a.ctx(), a, b);
1104  }
1105  else if (a.is_bv() && b.is_bv()) {
1106  r = Z3_mk_bvsdiv(a.ctx(), a, b);
1107  }
1108  else {
1109  // operator is not supported by given arguments.
1110  assert(false);
1111  }
1112  a.check_error();
1113  return expr(a.ctx(), r);
1114  }
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed division.
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ operator/() [2/3]

expr z3::operator/ ( expr const &  a,
int  b 
)
inline

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

1115 { return a / a.ctx().num_val(b, a.get_sort()); }

§ operator/() [3/3]

expr z3::operator/ ( int  a,
expr const &  b 
)
inline

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

1116 { return b.ctx().num_val(a, b.get_sort()) / b; }

§ operator<() [1/6]

expr z3::operator< ( expr const &  a,
expr const &  b 
)
inline

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

Referenced by expr::body(), and probe::operator()().

1176  {
1177  check_context(a, b);
1178  Z3_ast r = 0;
1179  if (a.is_arith() && b.is_arith()) {
1180  r = Z3_mk_lt(a.ctx(), a, b);
1181  }
1182  else if (a.is_bv() && b.is_bv()) {
1183  r = Z3_mk_bvslt(a.ctx(), a, b);
1184  }
1185  else {
1186  // operator is not supported by given arguments.
1187  assert(false);
1188  }
1189  a.check_error();
1190  return expr(a.ctx(), r);
1191  }
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed less than.
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ operator<() [2/6]

expr z3::operator< ( expr const &  a,
int  b 
)
inline

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

1192 { return a < a.ctx().num_val(b, a.get_sort()); }

§ operator<() [3/6]

expr z3::operator< ( int  a,
expr const &  b 
)
inline

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

1193 { return b.ctx().num_val(a, b.get_sort()) < b; }

§ operator<() [4/6]

probe z3::operator< ( probe const &  p1,
probe const &  p2 
)
inline

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

1980  {
1981  check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1982  }
Z3_probe Z3_API Z3_probe_lt(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than the value returned...
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ operator<() [5/6]

probe z3::operator< ( probe const &  p1,
double  p2 
)
inline

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

1983 { return p1 < probe(p1.ctx(), p2); }

§ operator<() [6/6]

probe z3::operator< ( double  p1,
probe const &  p2 
)
inline

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

1984 { return probe(p2.ctx(), p1) < p2; }

§ operator<<() [1/12]

std::ostream& z3::operator<< ( std::ostream &  out,
exception const &  e 
)
inline

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

87 { out << e.msg(); return out; }

§ operator<<() [2/12]

std::ostream& z3::operator<< ( std::ostream &  out,
symbol const &  s 
)
inline

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

351  {
352  if (s.kind() == Z3_INT_SYMBOL)
353  out << "k!" << s.to_int();
354  else
355  out << s.str().c_str();
356  return out;
357  }

§ operator<<() [3/12]

std::ostream& z3::operator<< ( std::ostream &  out,
param_descrs const &  d 
)
inline

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

382 { return out << d.to_string(); }

§ operator<<() [4/12]

std::ostream& z3::operator<< ( std::ostream &  out,
params const &  p 
)
inline

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

405  {
406  out << Z3_params_to_string(p.ctx(), p); return out;
407  }
Z3_string Z3_API Z3_params_to_string(Z3_context c, Z3_params p)
Convert a parameter set into a string. This function is mainly used for printing the contents of a pa...

§ operator<<() [5/12]

std::ostream& z3::operator<< ( std::ostream &  out,
ast const &  n 
)
inline

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

429  {
430  out << Z3_ast_to_string(n.ctx(), n.m_ast); return out;
431  }
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.

§ operator<<() [6/12]

std::ostream& z3::operator<< ( std::ostream &  out,
model const &  m 
)
inline

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

1646 { out << Z3_model_to_string(m.ctx(), m); return out; }
Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m)
Convert the given model into a string.

§ operator<<() [7/12]

std::ostream& z3::operator<< ( std::ostream &  out,
stats const &  s 
)
inline

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

1675 { out << Z3_stats_to_string(s.ctx(), s); return out; }
Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)
Convert a statistics into a string.

§ operator<<() [8/12]

std::ostream& z3::operator<< ( std::ostream &  out,
check_result  r 
)
inline

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

1678  {
1679  if (r == unsat) out << "unsat";
1680  else if (r == sat) out << "sat";
1681  else out << "unknown";
1682  return out;
1683  }
Definition: z3++.h:121

§ operator<<() [9/12]

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

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

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

§ operator<<() [10/12]

std::ostream& z3::operator<< ( std::ostream &  out,
goal const &  g 
)
inline

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

1826 { out << Z3_goal_to_string(g.ctx(), g); return out; }
Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g)
Convert a goal into a string.

§ operator<<() [11/12]

std::ostream& z3::operator<< ( std::ostream &  out,
apply_result const &  r 
)
inline

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

1856 { out << Z3_apply_result_to_string(r.ctx(), r); return out; }
Z3_string Z3_API Z3_apply_result_to_string(Z3_context c, Z3_apply_result r)
Convert the Z3_apply_result object returned by Z3_tactic_apply into a string.

§ operator<<() [12/12]

std::ostream& z3::operator<< ( std::ostream &  out,
optimize const &  s 
)
inline

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

2064 { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; }

§ operator<=() [1/6]

expr z3::operator<= ( expr const &  a,
expr const &  b 
)
inline

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

Referenced by expr::body(), and probe::operator()().

1154  {
1155  check_context(a, b);
1156  Z3_ast r = 0;
1157  if (a.is_arith() && b.is_arith()) {
1158  r = Z3_mk_le(a.ctx(), a, b);
1159  }
1160  else if (a.is_bv() && b.is_bv()) {
1161  r = Z3_mk_bvsle(a.ctx(), a, b);
1162  }
1163  else {
1164  // operator is not supported by given arguments.
1165  assert(false);
1166  }
1167  a.check_error();
1168  return expr(a.ctx(), r);
1169  }
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed less than or equal to.
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ operator<=() [2/6]

expr z3::operator<= ( expr const &  a,
int  b 
)
inline

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

1170 { return a <= a.ctx().num_val(b, a.get_sort()); }

§ operator<=() [3/6]

expr z3::operator<= ( int  a,
expr const &  b 
)
inline

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

1171 { return b.ctx().num_val(a, b.get_sort()) <= b; }

§ operator<=() [4/6]

probe z3::operator<= ( probe const &  p1,
probe const &  p2 
)
inline

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

1970  {
1971  check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1972  }
Z3_probe Z3_API Z3_probe_le(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than or equal to the va...
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ operator<=() [5/6]

probe z3::operator<= ( probe const &  p1,
double  p2 
)
inline

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

1973 { return p1 <= probe(p1.ctx(), p2); }

§ operator<=() [6/6]

probe z3::operator<= ( double  p1,
probe const &  p2 
)
inline

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

1974 { return probe(p2.ctx(), p1) <= p2; }

§ operator==() [1/6]

expr z3::operator== ( expr const &  a,
expr const &  b 
)
inline

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

Referenced by expr::body(), and probe::operator()().

1015  {
1016  check_context(a, b);
1017  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1018  a.check_error();
1019  return expr(a.ctx(), r);
1020  }
void check_context(object const &a, object const &b)
Definition: z3++.h:336
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.

§ operator==() [2/6]

expr z3::operator== ( expr const &  a,
int  b 
)
inline

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

1021 { assert(a.is_arith() || a.is_bv()); return a == a.ctx().num_val(b, a.get_sort()); }

§ operator==() [3/6]

expr z3::operator== ( int  a,
expr const &  b 
)
inline

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

1022 { assert(b.is_arith() || b.is_bv()); return b.ctx().num_val(a, b.get_sort()) == b; }

§ operator==() [4/6]

probe z3::operator== ( probe const &  p1,
probe const &  p2 
)
inline

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

1990  {
1991  check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1992  }
void check_context(object const &a, object const &b)
Definition: z3++.h:336
Z3_probe Z3_API Z3_probe_eq(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is equal to the value returned ...

§ operator==() [5/6]

probe z3::operator== ( probe const &  p1,
double  p2 
)
inline

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

1993 { return p1 == probe(p1.ctx(), p2); }

§ operator==() [6/6]

probe z3::operator== ( double  p1,
probe const &  p2 
)
inline

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

1994 { return probe(p2.ctx(), p1) == p2; }

§ operator>() [1/6]

expr z3::operator> ( expr const &  a,
expr const &  b 
)
inline

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

Referenced by expr::body(), and probe::operator()().

1195  {
1196  check_context(a, b);
1197  Z3_ast r = 0;
1198  if (a.is_arith() && b.is_arith()) {
1199  r = Z3_mk_gt(a.ctx(), a, b);
1200  }
1201  else if (a.is_bv() && b.is_bv()) {
1202  r = Z3_mk_bvsgt(a.ctx(), a, b);
1203  }
1204  else {
1205  // operator is not supported by given arguments.
1206  assert(false);
1207  }
1208  a.check_error();
1209  return expr(a.ctx(), r);
1210  }
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed greater than.
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ operator>() [2/6]

expr z3::operator> ( expr const &  a,
int  b 
)
inline

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

1211 { return a > a.ctx().num_val(b, a.get_sort()); }

§ operator>() [3/6]

expr z3::operator> ( int  a,
expr const &  b 
)
inline

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

1212 { return b.ctx().num_val(a, b.get_sort()) > b; }

§ operator>() [4/6]

probe z3::operator> ( probe const &  p1,
probe const &  p2 
)
inline

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

1985  {
1986  check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1987  }
void check_context(object const &a, object const &b)
Definition: z3++.h:336
Z3_probe Z3_API Z3_probe_gt(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than the value retur...

§ operator>() [5/6]

probe z3::operator> ( probe const &  p1,
double  p2 
)
inline

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

1988 { return p1 > probe(p1.ctx(), p2); }

§ operator>() [6/6]

probe z3::operator> ( double  p1,
probe const &  p2 
)
inline

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

1989 { return probe(p2.ctx(), p1) > p2; }

§ operator>=() [1/6]

expr z3::operator>= ( expr const &  a,
expr const &  b 
)
inline

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

Referenced by expr::body(), and probe::operator()().

1082  {
1083  check_context(a, b);
1084  Z3_ast r = 0;
1085  if (a.is_arith() && b.is_arith()) {
1086  r = Z3_mk_ge(a.ctx(), a, b);
1087  }
1088  else if (a.is_bv() && b.is_bv()) {
1089  r = Z3_mk_bvsge(a.ctx(), a, b);
1090  }
1091  else {
1092  // operator is not supported by given arguments.
1093  assert(false);
1094  }
1095  a.check_error();
1096  return expr(a.ctx(), r);
1097  }
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed greater than or equal to.
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ operator>=() [2/6]

expr z3::operator>= ( expr const &  a,
int  b 
)
inline

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

1173 { return a >= a.ctx().num_val(b, a.get_sort()); }

§ operator>=() [3/6]

expr z3::operator>= ( int  a,
expr const &  b 
)
inline

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

1174 { return b.ctx().num_val(a, b.get_sort()) >= b; }

§ operator>=() [4/6]

probe z3::operator>= ( probe const &  p1,
probe const &  p2 
)
inline

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

1975  {
1976  check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
1977  }
Z3_probe Z3_API Z3_probe_ge(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than or equal to the...
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ operator>=() [5/6]

probe z3::operator>= ( probe const &  p1,
double  p2 
)
inline

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

1978 { return p1 >= probe(p1.ctx(), p2); }

§ operator>=() [6/6]

probe z3::operator>= ( double  p1,
probe const &  p2 
)
inline

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

1979 { return probe(p2.ctx(), p1) >= p2; }

§ operator^() [1/3]

expr z3::operator^ ( expr const &  a,
expr const &  b 
)
inline

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

Referenced by expr::body().

1218 { check_context(a, b); Z3_ast r = Z3_mk_bvxor(a.ctx(), a, b); return expr(a.ctx(), r); }
void check_context(object const &a, object const &b)
Definition: z3++.h:336
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.

§ operator^() [2/3]

expr z3::operator^ ( expr const &  a,
int  b 
)
inline

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

1219 { return a ^ a.ctx().num_val(b, a.get_sort()); }

§ operator^() [3/3]

expr z3::operator^ ( int  a,
expr const &  b 
)
inline

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

1220 { return b.ctx().num_val(a, b.get_sort()) ^ b; }

§ operator|() [1/4]

expr z3::operator| ( expr const &  a,
expr const &  b 
)
inline

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

Referenced by expr::body(), and tactic::help().

1222 { check_context(a, b); Z3_ast r = Z3_mk_bvor(a.ctx(), a, b); return expr(a.ctx(), r); }
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ operator|() [2/4]

expr z3::operator| ( expr const &  a,
int  b 
)
inline

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

1223 { return a | a.ctx().num_val(b, a.get_sort()); }

§ operator|() [3/4]

expr z3::operator| ( int  a,
expr const &  b 
)
inline

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

1224 { return b.ctx().num_val(a, b.get_sort()) | b; }

§ operator|() [4/4]

tactic z3::operator| ( tactic const &  t1,
tactic const &  t2 
)
inline

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

1903  {
1904  check_context(t1, t2);
1905  Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
1906  t1.check_error();
1907  return tactic(t1.ctx(), r);
1908  }
void check_context(object const &a, object const &b)
Definition: z3++.h:336
Z3_tactic Z3_API Z3_tactic_or_else(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that first applies t1 to a given goal, if it fails then returns the result of t2 appl...

§ operator||() [1/4]

expr z3::operator|| ( expr const &  a,
expr const &  b 
)
inline
Precondition
a.is_bool()
b.is_bool()

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

Referenced by expr::body(), and probe::operator()().

1002  {
1003  check_context(a, b);
1004  assert(a.is_bool() && b.is_bool());
1005  Z3_ast args[2] = { a, b };
1006  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1007  a.check_error();
1008  return expr(a.ctx(), r);
1009  }
Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] or ... or args[num_args-1].
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ operator||() [2/4]

expr z3::operator|| ( expr const &  a,
bool  b 
)
inline
Precondition
a.is_bool()

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

1011 { return a || a.ctx().bool_val(b); }

§ operator||() [3/4]

expr z3::operator|| ( bool  a,
expr const &  b 
)
inline
Precondition
b.is_bool()

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

1013 { return b.ctx().bool_val(a) || b; }

§ operator||() [4/4]

probe z3::operator|| ( probe const &  p1,
probe const &  p2 
)
inline

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

1998  {
1999  check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2000  }
Z3_probe Z3_API Z3_probe_or(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when p1 or p2 evaluates to true.
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ operator~()

expr z3::operator~ ( expr const &  a)
inline

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

Referenced by expr::body().

1226 { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.

§ option()

expr z3::option ( expr const &  re)
inline

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

2454  {
2455  Z3_ast r = Z3_mk_re_option(re.ctx(), re);
2456  re.check_error();
2457  return expr(re.ctx(), r);
2458  }

§ plus()

expr z3::plus ( expr const &  re)
inline

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

2449  {
2450  Z3_ast r = Z3_mk_re_plus(re.ctx(), re);
2451  re.check_error();
2452  return expr(re.ctx(), r);
2453  }

§ prefixof()

expr z3::prefixof ( expr const &  a,
expr const &  b 
)
inline

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

2426  {
2427  check_context(a, b);
2428  Z3_ast r = Z3_mk_seq_prefix(a.ctx(), a, b);
2429  a.check_error();
2430  return expr(a.ctx(), r);
2431  }
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ pw() [1/3]

expr z3::pw ( expr const &  a,
expr const &  b 
)
inline

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

Referenced by expr::body(), and pw().

972  {
973  assert(a.is_arith() && b.is_arith());
974  check_context(a, b);
975  Z3_ast r = Z3_mk_power(a.ctx(), a, b);
976  a.check_error();
977  return expr(a.ctx(), r);
978  }
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:336

§ pw() [2/3]

expr z3::pw ( expr const &  a,
int  b 
)
inline

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

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

§ pw() [3/3]

expr z3::pw ( int  a,
expr const &  b 
)
inline

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

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

§ repeat()

tactic z3::repeat ( tactic const &  t,
unsigned  max = UINT_MAX 
)
inline

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

Referenced by tactic::help().

1910  {
1911  Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
1912  t.check_error();
1913  return tactic(t.ctx(), r);
1914  }
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...

§ reset_params()

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...

§ select() [1/2]

expr z3::select ( expr const &  a,
expr const &  i 
)
inline

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

Referenced by select().

2329  {
2330  check_context(a, i);
2331  Z3_ast r = Z3_mk_select(a.ctx(), a, i);
2332  a.check_error();
2333  return expr(a.ctx(), r);
2334  }
void check_context(object const &a, object const &b)
Definition: z3++.h:336
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...

§ select() [2/2]

expr z3::select ( expr const &  a,
int  i 
)
inline

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

2335 { return select(a, a.ctx().num_val(i, a.get_sort().array_domain())); }
expr select(expr const &a, int i)
Definition: z3++.h:2335

§ set_add()

expr z3::set_add ( expr const &  s,
expr const &  e 
)
inline

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

2371  {
2372  MK_EXPR2(Z3_mk_set_add, s, e);
2373  }
#define MK_EXPR2(_fn, _arg1, _arg2)
Definition: z3++.h:2353
Z3_ast Z3_API Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem)
Add an element to a set.

§ set_complement()

expr z3::set_complement ( expr const &  a)
inline

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

2399  {
2401  }
Z3_ast Z3_API Z3_mk_set_complement(Z3_context c, Z3_ast arg)
Take the complement of a set.
#define MK_EXPR1(_fn, _arg)
Definition: z3++.h:2348

§ set_del()

expr z3::set_del ( expr const &  s,
expr const &  e 
)
inline

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

2375  {
2376  MK_EXPR2(Z3_mk_set_del, s, e);
2377  }
Z3_ast Z3_API Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem)
Remove an element to a set.
#define MK_EXPR2(_fn, _arg1, _arg2)
Definition: z3++.h:2353

§ set_difference()

expr z3::set_difference ( expr const &  a,
expr const &  b 
)
inline

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

2395  {
2397  }
#define MK_EXPR2(_fn, _arg1, _arg2)
Definition: z3++.h:2353
Z3_ast Z3_API Z3_mk_set_difference(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Take the set difference between two sets.

§ set_intersect()

expr z3::set_intersect ( expr const &  a,
expr const &  b 
)
inline

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

2387  {
2388  check_context(a, b);
2389  Z3_ast es[2] = { a, b };
2390  Z3_ast r = Z3_mk_set_intersect(a.ctx(), 2, es);
2391  a.check_error();
2392  return expr(a.ctx(), r);
2393  }
Z3_ast Z3_API Z3_mk_set_intersect(Z3_context c, unsigned num_args, Z3_ast const args[])
Take the intersection of a list of sets.
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ set_member()

expr z3::set_member ( expr const &  s,
expr const &  e 
)
inline

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

2403  {
2404  MK_EXPR2(Z3_mk_set_member, s, e);
2405  }
#define MK_EXPR2(_fn, _arg1, _arg2)
Definition: z3++.h:2353
Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set)
Check for set membership.

§ set_param() [1/3]

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.

§ set_param() [2/3]

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.

§ set_param() [3/3]

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.

§ set_subset()

expr z3::set_subset ( expr const &  a,
expr const &  b 
)
inline

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

2407  {
2408  MK_EXPR2(Z3_mk_set_subset, a, b);
2409  }
#define MK_EXPR2(_fn, _arg1, _arg2)
Definition: z3++.h:2353
Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Check for subsetness of sets.

§ set_union()

expr z3::set_union ( expr const &  a,
expr const &  b 
)
inline

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

2379  {
2380  check_context(a, b);
2381  Z3_ast es[2] = { a, b };
2382  Z3_ast r = Z3_mk_set_union(a.ctx(), 2, es);
2383  a.check_error();
2384  return expr(a.ctx(), r);
2385  }
Z3_ast Z3_API Z3_mk_set_union(Z3_context c, unsigned num_args, Z3_ast const args[])
Take the union of a list of sets.
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ sext()

expr z3::sext ( expr const &  a,
unsigned  i 
)
inline

Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector.

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

1343 { return to_expr(a.ctx(), Z3_mk_sign_ext(a.ctx(), i, a)); }
Z3_ast Z3_API Z3_mk_sign_ext(Z3_context c, unsigned i, Z3_ast t1)
Sign-extend of the given bit-vector to the (signed) equivalent bit-vector of size m+i...
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:1250

§ shl() [1/3]

expr z3::shl ( expr const &  a,
expr const &  b 
)
inline

shift left operator for bitvectors

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

Referenced by shl().

1317 { return to_expr(a.ctx(), Z3_mk_bvshl(a.ctx(), a, b)); }
Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2)
Shift left.
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:1250

§ shl() [2/3]

expr z3::shl ( expr const &  a,
int  b 
)
inline

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

1318 { return shl(a, a.ctx().num_val(b, a.get_sort())); }
expr shl(int a, expr const &b)
Definition: z3++.h:1319

§ shl() [3/3]

expr z3::shl ( int  a,
expr const &  b 
)
inline

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

1319 { return shl(b.ctx().num_val(a, b.get_sort()), b); }
expr shl(int a, expr const &b)
Definition: z3++.h:1319

§ srem() [1/3]

expr z3::srem ( expr const &  a,
expr const &  b 
)
inline

signed reminder operator for bitvectors

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

Referenced by srem().

1303 { return to_expr(a.ctx(), Z3_mk_bvsrem(a.ctx(), a, b)); }
Z3_ast Z3_API Z3_mk_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2)
Two&#39;s complement signed remainder (sign follows dividend).
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:1250

§ srem() [2/3]

expr z3::srem ( expr const &  a,
int  b 
)
inline

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

1304 { return srem(a, a.ctx().num_val(b, a.get_sort())); }
expr srem(int a, expr const &b)
Definition: z3++.h:1305

§ srem() [3/3]

expr z3::srem ( int  a,
expr const &  b 
)
inline

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

1305 { return srem(b.ctx().num_val(a, b.get_sort()), b); }
expr srem(int a, expr const &b)
Definition: z3++.h:1305

§ star()

expr z3::star ( expr const &  re)
inline

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

2459  {
2460  Z3_ast r = Z3_mk_re_star(re.ctx(), re);
2461  re.check_error();
2462  return expr(re.ctx(), r);
2463  }

§ store() [1/4]

expr z3::store ( expr const &  a,
expr const &  i,
expr const &  v 
)
inline

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

Referenced by store().

2336  {
2337  check_context(a, i); check_context(a, v);
2338  Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
2339  a.check_error();
2340  return expr(a.ctx(), r);
2341  }
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:336

§ store() [2/4]

expr z3::store ( expr const &  a,
int  i,
expr const &  v 
)
inline

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

2342 { 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:2344

§ store() [3/4]

expr z3::store ( expr const &  a,
expr  i,
int  v 
)
inline

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

2343 { 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:2344

§ store() [4/4]

expr z3::store ( expr const &  a,
int  i,
int  v 
)
inline

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

2344  {
2345  return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
2346  }
expr store(expr const &a, int i, int v)
Definition: z3++.h:2344

§ suffixof()

expr z3::suffixof ( expr const &  a,
expr const &  b 
)
inline

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

2420  {
2421  check_context(a, b);
2422  Z3_ast r = Z3_mk_seq_suffix(a.ctx(), a, b);
2423  a.check_error();
2424  return expr(a.ctx(), r);
2425  }
void check_context(object const &a, object const &b)
Definition: z3++.h:336

§ to_check_result()

check_result z3::to_check_result ( Z3_lbool  l)
inline

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

Referenced by solver::check(), optimize::check(), context::compute_interpolant(), and solver::consequences().

124  {
125  if (l == Z3_L_TRUE) return sat;
126  else if (l == Z3_L_FALSE) return unsat;
127  return unknown;
128  }
Definition: z3++.h:121

§ to_expr()

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 1250 of file z3++.h.

Referenced by ashr(), lshr(), sext(), shl(), srem(), udiv(), uge(), ugt(), ule(), ult(), urem(), and zext().

1250  {
1251  c.check_error();
1252  assert(Z3_get_ast_kind(c, a) == Z3_APP_AST ||
1253  Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
1254  Z3_get_ast_kind(c, a) == Z3_VAR_AST ||
1255  Z3_get_ast_kind(c, a) == Z3_QUANTIFIER_AST);
1256  return expr(c, a);
1257  }

§ to_func_decl()

func_decl z3::to_func_decl ( context c,
Z3_func_decl  f 
)
inline

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

1264  {
1265  c.check_error();
1266  return func_decl(c, f);
1267  }

§ to_re()

expr z3::to_re ( expr const &  s)
inline

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

2438  {
2439  Z3_ast r = Z3_mk_seq_to_re(s.ctx(), s);
2440  s.check_error();
2441  return expr(s.ctx(), r);
2442  }

§ to_real()

expr z3::to_real ( expr const &  a)
inline

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

2305 { 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.

§ to_sort()

sort z3::to_sort ( context c,
Z3_sort  s 
)
inline

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

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

1259  {
1260  c.check_error();
1261  return sort(c, s);
1262  }

§ try_for()

tactic z3::try_for ( tactic const &  t,
unsigned  ms 
)
inline

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

Referenced by tactic::help().

1921  {
1922  Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
1923  t.check_error();
1924  return tactic(t.ctx(), r);
1925  }
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...

§ udiv() [1/3]

expr z3::udiv ( expr const &  a,
expr const &  b 
)
inline

unsigned division operator for bitvectors.

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

Referenced by udiv().

1296 { 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:1250

§ udiv() [2/3]

expr z3::udiv ( expr const &  a,
int  b 
)
inline

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

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

§ udiv() [3/3]

expr z3::udiv ( int  a,
expr const &  b 
)
inline

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

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

§ uge() [1/3]

expr z3::uge ( expr const &  a,
expr const &  b 
)
inline

unsigned greater than or equal to operator for bitvectors.

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

Referenced by uge().

1284 { 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:1250

§ uge() [2/3]

expr z3::uge ( expr const &  a,
int  b 
)
inline

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

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

§ uge() [3/3]

expr z3::uge ( int  a,
expr const &  b 
)
inline

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

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

§ ugt() [1/3]

expr z3::ugt ( expr const &  a,
expr const &  b 
)
inline

unsigned greater than operator for bitvectors.

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

Referenced by ugt().

1290 { 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:1250

§ ugt() [2/3]

expr z3::ugt ( expr const &  a,
int  b 
)
inline

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

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

§ ugt() [3/3]

expr z3::ugt ( int  a,
expr const &  b 
)
inline

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

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

§ ule() [1/3]

expr z3::ule ( expr const &  a,
expr const &  b 
)
inline

unsigned less than or equal to operator for bitvectors.

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

Referenced by ule().

1272 { 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:1250

§ ule() [2/3]

expr z3::ule ( expr const &  a,
int  b 
)
inline

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

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

§ ule() [3/3]

expr z3::ule ( int  a,
expr const &  b 
)
inline

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

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

§ ult() [1/3]

expr z3::ult ( expr const &  a,
expr const &  b 
)
inline

unsigned less than operator for bitvectors.

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

Referenced by ult().

1278 { 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:1250

§ ult() [2/3]

expr z3::ult ( expr const &  a,
int  b 
)
inline

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

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

§ ult() [3/3]

expr z3::ult ( int  a,
expr const &  b 
)
inline

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

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

§ urem() [1/3]

expr z3::urem ( expr const &  a,
expr const &  b 
)
inline

unsigned reminder operator for bitvectors

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

Referenced by urem().

1310 { return to_expr(a.ctx(), Z3_mk_bvurem(a.ctx(), a, b)); }
Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned remainder.
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:1250

§ urem() [2/3]

expr z3::urem ( expr const &  a,
int  b 
)
inline

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

1311 { return urem(a, a.ctx().num_val(b, a.get_sort())); }
expr urem(int a, expr const &b)
Definition: z3++.h:1312

§ urem() [3/3]

expr z3::urem ( int  a,
expr const &  b 
)
inline

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

1312 { return urem(b.ctx().num_val(a, b.get_sort()), b); }
expr urem(int a, expr const &b)
Definition: z3++.h:1312

§ when()

tactic z3::when ( probe const &  p,
tactic const &  t 
)
inline

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

2071  {
2072  check_context(p, t);
2073  Z3_tactic r = Z3_tactic_when(t.ctx(), p, t);
2074  t.check_error();
2075  return tactic(t.ctx(), r);
2076  }
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:336

§ with()

tactic z3::with ( tactic const &  t,
params const &  p 
)
inline

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

Referenced by tactic::help().

1916  {
1917  Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
1918  t.check_error();
1919  return tactic(t.ctx(), r);
1920  }
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.

§ zext()

expr z3::zext ( expr const &  a,
unsigned  i 
)
inline

Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i, where m is the size of the given bit-vector.

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

1338 { return to_expr(a.ctx(), Z3_mk_zero_ext(a.ctx(), i, a)); }
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:1250
Z3_ast Z3_API Z3_mk_zero_ext(Z3_context c, unsigned i, Z3_ast t1)
Extend the given bit-vector with zeros to the (unsigned) equivalent bit-vector of size m+i...