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  fixedpoint
 
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 mod (expr const &a, expr const &b)
 
expr mod (expr const &a, int b)
 
expr mod (int a, expr const &b)
 
expr rem (expr const &a, expr const &b)
 
expr rem (expr const &a, int b)
 
expr rem (int a, expr const &b)
 
expr operator! (expr const &a)
 
expr is_int (expr const &e)
 
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 nand (expr const &a, expr const &b)
 
expr nor (expr const &a, expr const &b)
 
expr xnor (expr const &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 remainder operator for bitvectors More...
 
expr srem (expr const &a, int b)
 
expr srem (int a, expr const &b)
 
expr smod (expr const &a, expr const &b)
 signed modulus operator for bitvectors More...
 
expr smod (expr const &a, int b)
 
expr smod (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 pble (expr_vector const &es, int const *coeffs, int bound)
 
expr pbge (expr_vector const &es, int const *coeffs, int bound)
 
expr pbeq (expr_vector const &es, int const *coeffs, int bound)
 
expr atmost (expr_vector const &es, unsigned bound)
 
expr atleast (expr_vector const &es, unsigned bound)
 
expr sum (expr_vector const &args)
 
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)
 
tactic par_or (unsigned n, tactic const *tactics)
 
tactic par_and_then (tactic const &t1, tactic const &t2)
 
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)
 
std::ostream & operator<< (std::ostream &out, fixedpoint const &f)
 
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 select (expr const &a, expr_vector const &i)
 
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 store (expr const &a, expr_vector const &i, expr const &v)
 
expr as_array (func_decl &f)
 
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 re_empty (sort const &s)
 
expr re_full (sort const &s)
 
expr re_intersect (expr_vector const &args)
 
expr re_complement (expr const &a)
 
expr range (expr const &lo, expr const &hi)
 
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 126 of file z3++.h.

126  {
127  unsat, sat, unknown
128  };
Definition: z3++.h:127

Function Documentation

◆ as_array()

expr z3::as_array ( func_decl f)
inline

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

2681  {
2682  Z3_ast r = Z3_mk_as_array(f.ctx(), f);
2683  f.check_error();
2684  return expr(f.ctx(), r);
2685  }
Z3_ast Z3_API Z3_mk_as_array(Z3_context c, Z3_func_decl f)
Create array with the same interpretation as a function. The array satisfies the property (f x) = (se...

◆ ashr() [1/3]

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

arithmetic shift right operator for bitvectors

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

Referenced by ashr().

1467 { 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:1379

◆ ashr() [2/3]

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

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

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

◆ ashr() [3/3]

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

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

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

◆ atleast()

expr z3::atleast ( expr_vector const &  es,
unsigned  bound 
)
inline

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

1667  {
1668  assert(es.size() > 0);
1669  context& ctx = es[0].ctx();
1670  array<Z3_ast> _es(es);
1671  Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
1672  ctx.check_error();
1673  return expr(ctx, r);
1674  }
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.

◆ atmost()

expr z3::atmost ( expr_vector const &  es,
unsigned  bound 
)
inline

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

1659  {
1660  assert(es.size() > 0);
1661  context& ctx = es[0].ctx();
1662  array<Z3_ast> _es(es);
1663  Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
1664  ctx.check_error();
1665  return expr(ctx, r);
1666  }
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.

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

Referenced by operator+().

1693  {
1694  check_context(a, b);
1695  Z3_ast r;
1696  if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
1697  Z3_ast _args[2] = { a, b };
1698  r = Z3_mk_seq_concat(a.ctx(), 2, _args);
1699  }
1700  else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
1701  Z3_ast _args[2] = { a, b };
1702  r = Z3_mk_re_concat(a.ctx(), 2, _args);
1703  }
1704  else {
1705  r = Z3_mk_concat(a.ctx(), a, b);
1706  }
1707  a.ctx().check_error();
1708  return expr(a.ctx(), r);
1709  }
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])
Create the concatenation of the regular languages.
Z3_bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
Z3_bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.
void check_context(object const &a, object const &b)
Definition: z3++.h:368

◆ concat() [2/2]

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

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

1711  {
1712  Z3_ast r;
1713  assert(args.size() > 0);
1714  if (args.size() == 1) {
1715  return args[0];
1716  }
1717  context& ctx = args[0].ctx();
1718  array<Z3_ast> _args(args);
1719  if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
1720  r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
1721  }
1722  else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
1723  r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
1724  }
1725  else {
1726  r = _args[args.size()-1];
1727  for (unsigned i = args.size()-1; i > 0; ) {
1728  --i;
1729  r = Z3_mk_concat(ctx, _args[i], r);
1730  ctx.check_error();
1731  }
1732  }
1733  ctx.check_error();
1734  return expr(ctx, r);
1735  }
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])
Create the concatenation of the regular languages.
Z3_bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
Z3_bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.

◆ cond()

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

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

2385  {
2386  check_context(p, t1); check_context(p, t2);
2387  Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2);
2388  t1.check_error();
2389  return tactic(t1.ctx(), r);
2390  }
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:368

◆ const_array()

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

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

2698  {
2699  MK_EXPR2(Z3_mk_const_array, d, v);
2700  }
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:2692

◆ distinct()

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

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

1684  {
1685  assert(args.size() > 0);
1686  context& ctx = args[0].ctx();
1687  array<Z3_ast> _args(args);
1688  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
1689  ctx.check_error();
1690  return expr(ctx, r);
1691  }
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 2754 of file z3++.h.

2754  {
2755  Z3_ast r = Z3_mk_seq_empty(s.ctx(), s);
2756  s.check_error();
2757  return expr(s.ctx(), r);
2758  }
Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq)
Create an empty sequence of the sequence sort seq.

◆ empty_set()

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

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

2702  {
2704  }
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:2687

◆ eq()

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

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

467 { return Z3_is_eq_ast(a.ctx(), a, b) != 0; }
Z3_bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2)
Compare terms.

◆ exists() [1/5]

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

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

1611  {
1612  check_context(x, b);
1613  Z3_app vars[] = {(Z3_app) x};
1614  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1615  }
Z3_ast Z3_API Z3_mk_exists_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Similar to Z3_mk_forall_const.
void check_context(object const &a, object const &b)
Definition: z3++.h:368

◆ exists() [2/5]

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

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

1616  {
1617  check_context(x1, b); check_context(x2, b);
1618  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1619  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1620  }
Z3_ast Z3_API Z3_mk_exists_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Similar to Z3_mk_forall_const.
void check_context(object const &a, object const &b)
Definition: z3++.h:368

◆ exists() [3/5]

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

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

1621  {
1622  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1623  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1624  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1625  }
Z3_ast Z3_API Z3_mk_exists_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Similar to Z3_mk_forall_const.
void check_context(object const &a, object const &b)
Definition: z3++.h:368

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

1626  {
1627  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
1628  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1629  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1630  }
Z3_ast Z3_API Z3_mk_exists_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Similar to Z3_mk_forall_const.
void check_context(object const &a, object const &b)
Definition: z3++.h:368

◆ exists() [5/5]

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

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

1631  {
1632  array<Z3_app> vars(xs);
1633  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);
1634  }
Z3_ast Z3_API Z3_mk_exists_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Similar to Z3_mk_forall_const.

◆ fail_if()

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

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

2374  {
2375  Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
2376  p.check_error();
2377  return tactic(p.ctx(), r);
2378  }
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 1587 of file z3++.h.

1587  {
1588  check_context(x, b);
1589  Z3_app vars[] = {(Z3_app) x};
1590  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1591  }
void check_context(object const &a, object const &b)
Definition: z3++.h:368
Z3_ast Z3_API Z3_mk_forall_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables...

◆ forall() [2/5]

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

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

1592  {
1593  check_context(x1, b); check_context(x2, b);
1594  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1595  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1596  }
void check_context(object const &a, object const &b)
Definition: z3++.h:368
Z3_ast Z3_API Z3_mk_forall_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables...

◆ forall() [3/5]

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

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

1597  {
1598  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1599  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1600  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1601  }
void check_context(object const &a, object const &b)
Definition: z3++.h:368
Z3_ast Z3_API Z3_mk_forall_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables...

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

1602  {
1603  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
1604  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1605  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1606  }
void check_context(object const &a, object const &b)
Definition: z3++.h:368
Z3_ast Z3_API Z3_mk_forall_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables...

◆ forall() [5/5]

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

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

1607  {
1608  array<Z3_app> vars(xs);
1609  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);
1610  }
Z3_ast Z3_API Z3_mk_forall_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables...

◆ full_set()

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

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

2706  {
2708  }
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:2687

◆ function() [1/7]

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

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

2625  {
2626  return range.ctx().function(name, arity, domain, range);
2627  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813
context & ctx() const
Definition: z3++.h:364
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:2428

◆ function() [2/7]

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

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

2628  {
2629  return range.ctx().function(name, arity, domain, range);
2630  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813
context & ctx() const
Definition: z3++.h:364
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:2428

◆ function() [3/7]

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

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

2631  {
2632  return range.ctx().function(name, domain, range);
2633  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813
context & ctx() const
Definition: z3++.h:364
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:2428

◆ function() [4/7]

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

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

2634  {
2635  return range.ctx().function(name, d1, d2, range);
2636  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813
context & ctx() const
Definition: z3++.h:364
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:2428

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

2637  {
2638  return range.ctx().function(name, d1, d2, d3, range);
2639  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813
context & ctx() const
Definition: z3++.h:364
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:2428

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

2640  {
2641  return range.ctx().function(name, d1, d2, d3, d4, range);
2642  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813
context & ctx() const
Definition: z3++.h:364
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:2428

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

2643  {
2644  return range.ctx().function(name, d1, d2, d3, d4, d5, range);
2645  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813
context & ctx() const
Definition: z3++.h:364
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:2428

◆ implies() [1/3]

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

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

Referenced by implies().

1082  {
1083  assert(a.is_bool() && b.is_bool());
1084  _Z3_MK_BIN_(a, b, Z3_mk_implies);
1085  }
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1075

◆ implies() [2/3]

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

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

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

◆ implies() [3/3]

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

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

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

◆ in_re()

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

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

2780  {
2781  MK_EXPR2(Z3_mk_seq_in_re, s, re);
2782  }
#define MK_EXPR2(_fn, _arg1, _arg2)
Definition: z3++.h:2692
Z3_ast Z3_API Z3_mk_seq_in_re(Z3_context c, Z3_ast seq, Z3_ast re)
Check if seq is in the language generated by the regular expression re.

◆ indexof()

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

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

2771  {
2772  check_context(s, substr); check_context(s, offset);
2773  Z3_ast r = Z3_mk_seq_index(s.ctx(), s, substr, offset);
2774  s.check_error();
2775  return expr(s.ctx(), r);
2776  }
Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset)
Return index of first occurrence of substr in s starting from offset offset. If s does not contain su...
void check_context(object const &a, object const &b)
Definition: z3++.h:368

◆ interpolant()

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

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

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

◆ is_int()

expr z3::is_int ( expr const &  e)
inline

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

1112 { _Z3_MK_UN_(e, Z3_mk_is_int); }
#define _Z3_MK_UN_(a, mkun)
Definition: z3++.h:1104
Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1)
Check if a real number is an integer.

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

1366  {
1367  check_context(c, t); check_context(c, e);
1368  assert(c.is_bool());
1369  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
1370  c.check_error();
1371  return expr(c.ctx(), r);
1372  }
void check_context(object const &a, object const &b)
Definition: z3++.h:368
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 1460 of file z3++.h.

Referenced by lshr().

1460 { 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:1379

◆ lshr() [2/3]

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

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

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

◆ lshr() [3/3]

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

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

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

◆ mk_and()

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

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

1743  {
1744  array<Z3_ast> _args(args);
1745  Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
1746  args.check_error();
1747  return expr(args.ctx(), r);
1748  }
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 1737 of file z3++.h.

1737  {
1738  array<Z3_ast> _args(args);
1739  Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
1740  args.check_error();
1741  return expr(args.ctx(), r);
1742  }
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].

◆ mod() [1/3]

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

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

Referenced by mod().

1094 { _Z3_MK_BIN_(a, b, Z3_mk_mod); }
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1075

◆ mod() [2/3]

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

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

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

◆ mod() [3/3]

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

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

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

◆ nand()

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

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

1352 { check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); return expr(a.ctx(), r); }
Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nand.
void check_context(object const &a, object const &b)
Definition: z3++.h:368

◆ nor()

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

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

1353 { check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); return expr(a.ctx(), r); }
Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nor.
void check_context(object const &a, object const &b)
Definition: z3++.h:368

◆ operator &() [1/4]

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

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

1340 { 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:368
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 1341 of file z3++.h.

1341 { 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 1342 of file z3++.h.

1342 { 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 2146 of file z3++.h.

2146  {
2147  check_context(t1, t2);
2148  Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
2149  t1.check_error();
2150  return tactic(t1.ctx(), r);
2151  }
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...
void check_context(object const &a, object const &b)
Definition: z3++.h:368

◆ operator &&() [1/4]

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

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

1116  {
1117  check_context(a, b);
1118  assert(a.is_bool() && b.is_bool());
1119  Z3_ast args[2] = { a, b };
1120  Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
1121  a.check_error();
1122  return expr(a.ctx(), r);
1123  }
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:368

◆ operator &&() [2/4]

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

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

1125 { 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 1126 of file z3++.h.

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

◆ operator &&() [4/4]

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

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

2259  {
2260  check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2261  }
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:368

◆ operator!() [1/2]

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

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

1110 { assert(a.is_bool()); _Z3_MK_UN_(a, Z3_mk_not); }
#define _Z3_MK_UN_(a, mkun)
Definition: z3++.h:1104
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 2265 of file z3++.h.

2265  {
2266  Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
2267  }
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 1150 of file z3++.h.

1150  {
1151  check_context(a, b);
1152  Z3_ast args[2] = { a, b };
1153  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1154  a.check_error();
1155  return expr(a.ctx(), r);
1156  }
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:368

◆ operator!=() [2/3]

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

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

1157 { 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 1158 of file z3++.h.

1158 { 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 1187 of file z3++.h.

1187  {
1188  check_context(a, b);
1189  Z3_ast r = 0;
1190  if (a.is_arith() && b.is_arith()) {
1191  Z3_ast args[2] = { a, b };
1192  r = Z3_mk_mul(a.ctx(), 2, args);
1193  }
1194  else if (a.is_bv() && b.is_bv()) {
1195  r = Z3_mk_bvmul(a.ctx(), a, b);
1196  }
1197  else {
1198  // operator is not supported by given arguments.
1199  assert(false);
1200  }
1201  a.check_error();
1202  return expr(a.ctx(), r);
1203  }
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:368
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 1204 of file z3++.h.

1204 { 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 1205 of file z3++.h.

1205 { 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 1160 of file z3++.h.

1160  {
1161  check_context(a, b);
1162  Z3_ast r = 0;
1163  if (a.is_arith() && b.is_arith()) {
1164  Z3_ast args[2] = { a, b };
1165  r = Z3_mk_add(a.ctx(), 2, args);
1166  }
1167  else if (a.is_bv() && b.is_bv()) {
1168  r = Z3_mk_bvadd(a.ctx(), a, b);
1169  }
1170  else if (a.is_seq() && b.is_seq()) {
1171  return concat(a, b);
1172  }
1173  else if (a.is_re() && b.is_re()) {
1174  Z3_ast _args[2] = { a, b };
1175  r = Z3_mk_re_union(a.ctx(), 2, _args);
1176  }
1177  else {
1178  // operator is not supported by given arguments.
1179  assert(false);
1180  }
1181  a.check_error();
1182  return expr(a.ctx(), r);
1183  }
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:1711
void check_context(object const &a, object const &b)
Definition: z3++.h:368
Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[])
Create the union of the regular languages.
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 1184 of file z3++.h.

1184 { 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 1185 of file z3++.h.

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

◆ operator-() [1/4]

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

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

1244  {
1245  Z3_ast r = 0;
1246  if (a.is_arith()) {
1247  r = Z3_mk_unary_minus(a.ctx(), a);
1248  }
1249  else if (a.is_bv()) {
1250  r = Z3_mk_bvneg(a.ctx(), a);
1251  }
1252  else {
1253  // operator is not supported by given arguments.
1254  assert(false);
1255  }
1256  a.check_error();
1257  return expr(a.ctx(), r);
1258  }
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 1260 of file z3++.h.

1260  {
1261  check_context(a, b);
1262  Z3_ast r = 0;
1263  if (a.is_arith() && b.is_arith()) {
1264  Z3_ast args[2] = { a, b };
1265  r = Z3_mk_sub(a.ctx(), 2, args);
1266  }
1267  else if (a.is_bv() && b.is_bv()) {
1268  r = Z3_mk_bvsub(a.ctx(), a, b);
1269  }
1270  else {
1271  // operator is not supported by given arguments.
1272  assert(false);
1273  }
1274  a.check_error();
1275  return expr(a.ctx(), r);
1276  }
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:368
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 1277 of file z3++.h.

1277 { 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 1278 of file z3++.h.

1278 { 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 1225 of file z3++.h.

1225  {
1226  check_context(a, b);
1227  Z3_ast r = 0;
1228  if (a.is_arith() && b.is_arith()) {
1229  r = Z3_mk_div(a.ctx(), a, b);
1230  }
1231  else if (a.is_bv() && b.is_bv()) {
1232  r = Z3_mk_bvsdiv(a.ctx(), a, b);
1233  }
1234  else {
1235  // operator is not supported by given arguments.
1236  assert(false);
1237  }
1238  a.check_error();
1239  return expr(a.ctx(), r);
1240  }
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:368

◆ operator/() [2/3]

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

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

1241 { 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 1242 of file z3++.h.

1242 { 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 1302 of file z3++.h.

1302  {
1303  check_context(a, b);
1304  Z3_ast r = 0;
1305  if (a.is_arith() && b.is_arith()) {
1306  r = Z3_mk_lt(a.ctx(), a, b);
1307  }
1308  else if (a.is_bv() && b.is_bv()) {
1309  r = Z3_mk_bvslt(a.ctx(), a, b);
1310  }
1311  else {
1312  // operator is not supported by given arguments.
1313  assert(false);
1314  }
1315  a.check_error();
1316  return expr(a.ctx(), r);
1317  }
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:368

◆ operator<() [2/6]

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

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

1318 { 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 1319 of file z3++.h.

1319 { 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 2244 of file z3++.h.

2244  {
2245  check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2246  }
void check_context(object const &a, object const &b)
Definition: z3++.h:368
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...

◆ operator<() [5/6]

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

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

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

◆ operator<() [6/6]

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

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

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

◆ operator<<() [1/13]

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/13]

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

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

383  {
384  if (s.kind() == Z3_INT_SYMBOL)
385  out << "k!" << s.to_int();
386  else
387  out << s.str().c_str();
388  return out;
389  }

◆ operator<<() [3/13]

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

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

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

◆ operator<<() [4/13]

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

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

437  {
438  out << Z3_params_to_string(p.ctx(), p); return out;
439  }
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/13]

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

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

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

◆ operator<<() [6/13]

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

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

1881 { 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/13]

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

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

1910 { 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/13]

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

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

1913  {
1914  if (r == unsat) out << "unsat";
1915  else if (r == sat) out << "sat";
1916  else out << "unknown";
1917  return out;
1918  }
Definition: z3++.h:127

◆ operator<<() [9/13]

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

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

2026 { 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/13]

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

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

2074 { 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/13]

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

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

2104 { 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/13]

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

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

2328 { out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; }
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)
Print the current context as a string.

◆ operator<<() [13/13]

std::ostream& z3::operator<< ( std::ostream &  out,
fixedpoint const &  f 
)
inline

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

2372 { return out << Z3_fixedpoint_to_string(f.ctx(), f, 0, 0); }
Z3_string Z3_API Z3_fixedpoint_to_string(Z3_context c, Z3_fixedpoint f, unsigned num_queries, Z3_ast queries[])
Print the current rules and background axioms as a string.

◆ operator<=() [1/6]

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

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

1280  {
1281  check_context(a, b);
1282  Z3_ast r = 0;
1283  if (a.is_arith() && b.is_arith()) {
1284  r = Z3_mk_le(a.ctx(), a, b);
1285  }
1286  else if (a.is_bv() && b.is_bv()) {
1287  r = Z3_mk_bvsle(a.ctx(), a, b);
1288  }
1289  else {
1290  // operator is not supported by given arguments.
1291  assert(false);
1292  }
1293  a.check_error();
1294  return expr(a.ctx(), r);
1295  }
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:368

◆ operator<=() [2/6]

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

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

1296 { 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 1297 of file z3++.h.

1297 { 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 2234 of file z3++.h.

2234  {
2235  check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2236  }
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:368

◆ operator<=() [5/6]

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

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

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

◆ operator<=() [6/6]

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

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

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

◆ operator==() [1/6]

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

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

1141  {
1142  check_context(a, b);
1143  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1144  a.check_error();
1145  return expr(a.ctx(), r);
1146  }
void check_context(object const &a, object const &b)
Definition: z3++.h:368
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 1147 of file z3++.h.

1147 { 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 1148 of file z3++.h.

1148 { 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 2254 of file z3++.h.

2254  {
2255  check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2256  }
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 ...
void check_context(object const &a, object const &b)
Definition: z3++.h:368

◆ operator==() [5/6]

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

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

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

◆ operator==() [6/6]

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

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

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

◆ operator>() [1/6]

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

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

1321  {
1322  check_context(a, b);
1323  Z3_ast r = 0;
1324  if (a.is_arith() && b.is_arith()) {
1325  r = Z3_mk_gt(a.ctx(), a, b);
1326  }
1327  else if (a.is_bv() && b.is_bv()) {
1328  r = Z3_mk_bvsgt(a.ctx(), a, b);
1329  }
1330  else {
1331  // operator is not supported by given arguments.
1332  assert(false);
1333  }
1334  a.check_error();
1335  return expr(a.ctx(), r);
1336  }
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:368

◆ operator>() [2/6]

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

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

1337 { 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 1338 of file z3++.h.

1338 { 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 2249 of file z3++.h.

2249  {
2250  check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2251  }
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...
void check_context(object const &a, object const &b)
Definition: z3++.h:368

◆ operator>() [5/6]

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

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

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

◆ operator>() [6/6]

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

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

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

◆ operator>=() [1/6]

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

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

1208  {
1209  check_context(a, b);
1210  Z3_ast r = 0;
1211  if (a.is_arith() && b.is_arith()) {
1212  r = Z3_mk_ge(a.ctx(), a, b);
1213  }
1214  else if (a.is_bv() && b.is_bv()) {
1215  r = Z3_mk_bvsge(a.ctx(), a, b);
1216  }
1217  else {
1218  // operator is not supported by given arguments.
1219  assert(false);
1220  }
1221  a.check_error();
1222  return expr(a.ctx(), r);
1223  }
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:368

◆ operator>=() [2/6]

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

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

1299 { 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 1300 of file z3++.h.

1300 { 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 2239 of file z3++.h.

2239  {
2240  check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2241  }
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:368

◆ operator>=() [5/6]

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

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

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

◆ operator>=() [6/6]

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

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

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

◆ operator^() [1/3]

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

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

1344 { 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:368
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 1345 of file z3++.h.

1345 { 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 1346 of file z3++.h.

1346 { 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 1348 of file z3++.h.

1348 { 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:368

◆ operator|() [2/4]

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

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

1349 { 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 1350 of file z3++.h.

1350 { 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 2153 of file z3++.h.

2153  {
2154  check_context(t1, t2);
2155  Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
2156  t1.check_error();
2157  return tactic(t1.ctx(), r);
2158  }
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...
void check_context(object const &a, object const &b)
Definition: z3++.h:368

◆ operator||() [1/4]

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

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

1128  {
1129  check_context(a, b);
1130  assert(a.is_bool() && b.is_bool());
1131  Z3_ast args[2] = { a, b };
1132  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1133  a.check_error();
1134  return expr(a.ctx(), r);
1135  }
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:368

◆ operator||() [2/4]

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

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

1137 { 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 1139 of file z3++.h.

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

◆ operator||() [4/4]

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

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

2262  {
2263  check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2264  }
void check_context(object const &a, object const &b)
Definition: z3++.h:368
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.

◆ operator~()

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

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

1356 { 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 2786 of file z3++.h.

2786  {
2788  }
Z3_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re)
Create the regular language [re].
#define MK_EXPR1(_fn, _arg)
Definition: z3++.h:2687

◆ par_and_then()

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

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

2185  {
2186  check_context(t1, t2);
2187  Z3_tactic r = Z3_tactic_par_and_then(t1.ctx(), t1, t2);
2188  t1.check_error();
2189  return tactic(t1.ctx(), r);
2190  }
Z3_tactic Z3_API Z3_tactic_par_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1...
void check_context(object const &a, object const &b)
Definition: z3++.h:368

◆ par_or()

tactic z3::par_or ( unsigned  n,
tactic const *  tactics 
)
inline

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

2176  {
2177  if (n == 0) {
2178  Z3_THROW(exception("a non-zero number of tactics need to be passed to par_or"));
2179  }
2180  array<Z3_tactic> buffer(n);
2181  for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];
2182  return tactic(tactics[0].ctx(), Z3_tactic_par_or(tactics[0].ctx(), n, buffer.ptr()));
2183  }
#define Z3_THROW(x)
Definition: z3++.h:93
def tactics(ctx=None)
Definition: z3py.py:7417
Z3_tactic Z3_API Z3_tactic_par_or(Z3_context c, unsigned num, Z3_tactic const ts[])
Return a tactic that applies the given tactics in parallel.

◆ pbeq()

expr z3::pbeq ( expr_vector const &  es,
int const *  coeffs,
int  bound 
)
inline

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

1651  {
1652  assert(es.size() > 0);
1653  context& ctx = es[0].ctx();
1654  array<Z3_ast> _es(es);
1655  Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
1656  ctx.check_error();
1657  return expr(ctx, r);
1658  }
Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.

◆ pbge()

expr z3::pbge ( expr_vector const &  es,
int const *  coeffs,
int  bound 
)
inline

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

1643  {
1644  assert(es.size() > 0);
1645  context& ctx = es[0].ctx();
1646  array<Z3_ast> _es(es);
1647  Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
1648  ctx.check_error();
1649  return expr(ctx, r);
1650  }
Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.

◆ pble()

expr z3::pble ( expr_vector const &  es,
int const *  coeffs,
int  bound 
)
inline

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

1635  {
1636  assert(es.size() > 0);
1637  context& ctx = es[0].ctx();
1638  array<Z3_ast> _es(es);
1639  Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
1640  ctx.check_error();
1641  return expr(ctx, r);
1642  }
Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.

◆ plus()

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

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

2783  {
2784  MK_EXPR1(Z3_mk_re_plus, re);
2785  }
Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re)
Create the regular language re+.
#define MK_EXPR1(_fn, _arg)
Definition: z3++.h:2687

◆ prefixof()

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

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

2765  {
2766  check_context(a, b);
2767  Z3_ast r = Z3_mk_seq_prefix(a.ctx(), a, b);
2768  a.check_error();
2769  return expr(a.ctx(), r);
2770  }
Z3_ast Z3_API Z3_mk_seq_prefix(Z3_context c, Z3_ast prefix, Z3_ast s)
Check if prefix is a prefix of s.
void check_context(object const &a, object const &b)
Definition: z3++.h:368

◆ pw() [1/3]

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

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

Referenced by pw().

1090 { _Z3_MK_BIN_(a, b, Z3_mk_power); }
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 ^ arg2.
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1075

◆ pw() [2/3]

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

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

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

◆ pw() [3/3]

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

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

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

◆ range()

expr z3::range ( expr const &  lo,
expr const &  hi 
)
inline

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

Referenced by z3py::AndThen(), ApplyResult::as_expr(), z3py::AtLeast(), ExprRef::children(), z3py::describe_probes(), z3py::eq(), context::function(), z3py::Function(), function(), Context::mkArrayConst(), Context::mkArraySort(), Context::mkConst(), Context::mkConstDecl(), Context::mkFreshConst(), Context::mkFreshConstDecl(), Context::mkFreshFuncDecl(), Context::mkFuncDecl(), z3py::OrElse(), z3py::ParOr(), z3py::probes(), z3py::RealVarVector(), AstVector::resize(), Fixedpoint::set_predicate_representation(), z3py::substitute(), z3py::substitute_vars(), z3py::tactics(), and Solver::to_smt2().

2813  {
2814  check_context(lo, hi);
2815  Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
2816  lo.check_error();
2817  return expr(lo.ctx(), r);
2818  }
Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi)
Create the range regular expression over two sequences of length 1.
void check_context(object const &a, object const &b)
Definition: z3++.h:368

◆ re_complement()

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

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

2810  {
2812  }
Z3_ast Z3_API Z3_mk_re_complement(Z3_context c, Z3_ast re)
Create the complement of the regular language re.
#define MK_EXPR1(_fn, _arg)
Definition: z3++.h:2687

◆ re_empty()

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

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

2792  {
2793  Z3_ast r = Z3_mk_re_empty(s.ctx(), s);
2794  s.check_error();
2795  return expr(s.ctx(), r);
2796  }
Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re)
Create an empty regular expression of sort re.

◆ re_full()

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

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

2797  {
2798  Z3_ast r = Z3_mk_re_full(s.ctx(), s);
2799  s.check_error();
2800  return expr(s.ctx(), r);
2801  }
Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re)
Create an universal regular expression of sort re.

◆ re_intersect()

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

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

2802  {
2803  assert(args.size() > 0);
2804  context& ctx = args[0].ctx();
2805  array<Z3_ast> _args(args);
2806  Z3_ast r = Z3_mk_re_intersect(ctx, _args.size(), _args.ptr());
2807  ctx.check_error();
2808  return expr(ctx, r);
2809  }
Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[])
Create the intersection of the regular languages.

◆ rem() [1/3]

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

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

Referenced by rem().

1098 { _Z3_MK_BIN_(a, b, Z3_mk_rem); }
Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 rem arg2.
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1075

◆ rem() [2/3]

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

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

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

◆ rem() [3/3]

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

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

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

◆ repeat()

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

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

2160  {
2161  Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
2162  t.check_error();
2163  return tactic(t.ctx(), r);
2164  }
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/3]

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

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

Referenced by select().

2647  {
2648  check_context(a, i);
2649  Z3_ast r = Z3_mk_select(a.ctx(), a, i);
2650  a.check_error();
2651  return expr(a.ctx(), r);
2652  }
void check_context(object const &a, object const &b)
Definition: z3++.h:368
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/3]

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

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

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

◆ select() [3/3]

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

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

2660  {
2661  check_context(a, i);
2662  array<Z3_ast> idxs(i);
2663  Z3_ast r = Z3_mk_select_n(a.ctx(), a, idxs.size(), idxs.ptr());
2664  a.check_error();
2665  return expr(a.ctx(), r);
2666  }
void check_context(object const &a, object const &b)
Definition: z3++.h:368
Z3_ast Z3_API Z3_mk_select_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const *idxs)
n-ary Array read. The argument a is the array and idxs are the indices of the array that gets read...

◆ set_add()

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

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

2710  {
2711  MK_EXPR2(Z3_mk_set_add, s, e);
2712  }
#define MK_EXPR2(_fn, _arg1, _arg2)
Definition: z3++.h:2692
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 2738 of file z3++.h.

2738  {
2740  }
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:2687

◆ set_del()

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

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

2714  {
2715  MK_EXPR2(Z3_mk_set_del, s, e);
2716  }
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:2692

◆ set_difference()

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

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

2734  {
2736  }
#define MK_EXPR2(_fn, _arg1, _arg2)
Definition: z3++.h:2692
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 2726 of file z3++.h.

2726  {
2727  check_context(a, b);
2728  Z3_ast es[2] = { a, b };
2729  Z3_ast r = Z3_mk_set_intersect(a.ctx(), 2, es);
2730  a.check_error();
2731  return expr(a.ctx(), r);
2732  }
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:368

◆ set_member()

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

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

2742  {
2743  MK_EXPR2(Z3_mk_set_member, s, e);
2744  }
#define MK_EXPR2(_fn, _arg1, _arg2)
Definition: z3++.h:2692
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 2746 of file z3++.h.

2746  {
2747  MK_EXPR2(Z3_mk_set_subset, a, b);
2748  }
#define MK_EXPR2(_fn, _arg1, _arg2)
Definition: z3++.h:2692
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 2718 of file z3++.h.

2718  {
2719  check_context(a, b);
2720  Z3_ast es[2] = { a, b };
2721  Z3_ast r = Z3_mk_set_union(a.ctx(), 2, es);
2722  a.check_error();
2723  return expr(a.ctx(), r);
2724  }
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:368

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

1479 { 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:1379

◆ shl() [1/3]

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

shift left operator for bitvectors

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

Referenced by shl().

1453 { 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:1379

◆ shl() [2/3]

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

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

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

◆ shl() [3/3]

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

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

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

◆ smod() [1/3]

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

signed modulus operator for bitvectors

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

Referenced by smod().

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

◆ smod() [2/3]

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

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

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

◆ smod() [3/3]

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

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

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

◆ srem() [1/3]

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

signed remainder operator for bitvectors

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

Referenced by srem().

1432 { 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:1379

◆ srem() [2/3]

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

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

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

◆ srem() [3/3]

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

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

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

◆ star()

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

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

2789  {
2790  MK_EXPR1(Z3_mk_re_star, re);
2791  }
Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re)
Create the regular language re*.
#define MK_EXPR1(_fn, _arg)
Definition: z3++.h:2687

◆ store() [1/5]

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

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

Referenced by store().

2654  {
2655  check_context(a, i); check_context(a, v);
2656  Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
2657  a.check_error();
2658  return expr(a.ctx(), r);
2659  }
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:368

◆ store() [2/5]

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

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

2668 { return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), v); }
expr store(expr const &a, expr_vector const &i, expr const &v)
Definition: z3++.h:2673

◆ store() [3/5]

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

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

2669 { return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }
expr store(expr const &a, expr_vector const &i, expr const &v)
Definition: z3++.h:2673

◆ store() [4/5]

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

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

2670  {
2671  return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
2672  }
expr store(expr const &a, expr_vector const &i, expr const &v)
Definition: z3++.h:2673

◆ store() [5/5]

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

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

2673  {
2674  check_context(a, i); check_context(a, v);
2675  array<Z3_ast> idxs(i);
2676  Z3_ast r = Z3_mk_store_n(a.ctx(), a, idxs.size(), idxs.ptr(), v);
2677  a.check_error();
2678  return expr(a.ctx(), r);
2679  }
Z3_ast Z3_API Z3_mk_store_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const *idxs, Z3_ast v)
n-ary Array update.
void check_context(object const &a, object const &b)
Definition: z3++.h:368

◆ suffixof()

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

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

2759  {
2760  check_context(a, b);
2761  Z3_ast r = Z3_mk_seq_suffix(a.ctx(), a, b);
2762  a.check_error();
2763  return expr(a.ctx(), r);
2764  }
Z3_ast Z3_API Z3_mk_seq_suffix(Z3_context c, Z3_ast suffix, Z3_ast s)
Check if suffix is a suffix of s.
void check_context(object const &a, object const &b)
Definition: z3++.h:368

◆ sum()

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

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

1675  {
1676  assert(args.size() > 0);
1677  context& ctx = args[0].ctx();
1678  array<Z3_ast> _args(args);
1679  Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
1680  ctx.check_error();
1681  return expr(ctx, r);
1682  }
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].

◆ to_check_result()

check_result z3::to_check_result ( Z3_lbool  l)
inline

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

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

130  {
131  if (l == Z3_L_TRUE) return sat;
132  else if (l == Z3_L_FALSE) return unsat;
133  return unknown;
134  }
Definition: z3++.h:127

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

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

1379  {
1380  c.check_error();
1381  assert(Z3_get_ast_kind(c, a) == Z3_APP_AST ||
1382  Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
1383  Z3_get_ast_kind(c, a) == Z3_VAR_AST ||
1385  return expr(c, a);
1386  }
Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a)
Return the kind of the given AST.

◆ to_func_decl()

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

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

1393  {
1394  c.check_error();
1395  return func_decl(c, f);
1396  }

◆ to_re()

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

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

2777  {
2779  }
#define MK_EXPR1(_fn, _arg)
Definition: z3++.h:2687
Z3_ast Z3_API Z3_mk_seq_to_re(Z3_context c, Z3_ast seq)
Create a regular expression that accepts the sequence seq.

◆ to_real()

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

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

2623 { 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 1388 of file z3++.h.

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

1388  {
1389  c.check_error();
1390  return sort(c, s);
1391  }

◆ try_for()

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

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

2171  {
2172  Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
2173  t.check_error();
2174  return tactic(t.ctx(), r);
2175  }
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 1425 of file z3++.h.

Referenced by udiv().

1425 { 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:1379

◆ udiv() [2/3]

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

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

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

◆ udiv() [3/3]

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

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

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

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

Referenced by uge().

1413 { 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:1379

◆ uge() [2/3]

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

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

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

◆ uge() [3/3]

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

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

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

◆ ugt() [1/3]

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

unsigned greater than operator for bitvectors.

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

Referenced by ugt().

1419 { 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:1379

◆ ugt() [2/3]

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

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

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

◆ ugt() [3/3]

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

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

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

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

Referenced by ule().

1401 { 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:1379

◆ ule() [2/3]

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

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

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

◆ ule() [3/3]

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

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

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

◆ ult() [1/3]

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

unsigned less than operator for bitvectors.

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

Referenced by ult().

1407 { 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:1379

◆ ult() [2/3]

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

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

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

◆ ult() [3/3]

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

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

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

◆ urem() [1/3]

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

unsigned reminder operator for bitvectors

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

Referenced by urem().

1446 { 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:1379

◆ urem() [2/3]

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

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

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

◆ urem() [3/3]

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

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

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

◆ when()

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

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

2379  {
2380  check_context(p, t);
2381  Z3_tactic r = Z3_tactic_when(t.ctx(), p, t);
2382  t.check_error();
2383  return tactic(t.ctx(), r);
2384  }
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:368

◆ with()

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

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

2166  {
2167  Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
2168  t.check_error();
2169  return tactic(t.ctx(), r);
2170  }
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.

◆ xnor()

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

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

1354 { check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); return expr(a.ctx(), r); }
Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise xnor.
void check_context(object const &a, object const &b)
Definition: z3++.h:368

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

1474 { 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:1379
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...