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

Z3 C++ namespace. More...

Data Structures

class  apply_result
 
class  array
 
class  ast
 
class  ast_vector_tpl
 
singleton  cast_ast
 
class  cast_ast< ast >
 
class  cast_ast< expr >
 
class  cast_ast< func_decl >
 
class  cast_ast< sort >
 
class  config
 Z3 global configuration object. More...
 
class  context
 A Context manages all other Z3 objects, global configuration options, etc. More...
 
class  exception
 Exception used to sign API usage errors. More...
 
class  expr
 A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort Boolean. Every expression has a sort. More...
 
class  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 }
 
enum  rounding_mode {
  RNA, RNE, RTP, RTN,
  RTZ
}
 

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 select (expr const &a, expr const &i)
 forward declarations More...
 
expr select (expr const &a, expr_vector const &i)
 
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 operator% (expr const &a, expr const &b)
 
expr operator% (expr const &a, int b)
 
expr operator% (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 min (expr const &a, expr const &b)
 
expr max (expr const &a, expr const &b)
 
expr abs (expr const &a)
 
expr sqrt (expr const &a, expr const &rm)
 
expr operator~ (expr const &a)
 
expr fma (expr const &a, expr const &b, expr const &c, expr const &rm)
 
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 sle (expr const &a, expr const &b)
 signed less than or equal to operator for bitvectors. More...
 
expr sle (expr const &a, int b)
 
expr sle (int a, expr const &b)
 
expr slt (expr const &a, expr const &b)
 signed less than operator for bitvectors. More...
 
expr slt (expr const &a, int b)
 
expr slt (int a, expr const &b)
 
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 bv2int (expr const &a, bool is_signed)
 bit-vector and integer conversions. More...
 
expr int2bv (unsigned n, expr const &a)
 
expr bvadd_no_overflow (expr const &a, expr const &b, bool is_signed)
 bit-vector overflow/underflow checks More...
 
expr bvadd_no_underflow (expr const &a, expr const &b)
 
expr bvsub_no_overflow (expr const &a, expr const &b)
 
expr bvsub_no_underflow (expr const &a, expr const &b, bool is_signed)
 
expr bvsdiv_no_overflow (expr const &a, expr const &b)
 
expr bvneg_no_overflow (expr const &a)
 
expr bvmul_no_overflow (expr const &a, expr const &b, bool is_signed)
 
expr bvmul_no_underflow (expr const &a, expr const &b)
 
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...
 
func_decl linear_order (sort const &a, unsigned index)
 
func_decl partial_order (sort const &a, unsigned index)
 
func_decl piecewise_linear_order (sort const &a, unsigned index)
 
func_decl tree_order (sort const &a, unsigned index)
 
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 lambda (expr const &x, expr const &b)
 
expr lambda (expr const &x1, expr const &x2, expr const &b)
 
expr lambda (expr const &x1, expr const &x2, expr const &x3, expr const &b)
 
expr lambda (expr const &x1, expr const &x2, expr const &x3, expr const &x4, expr const &b)
 
expr lambda (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)
 
func_decl function (char const *name, sort_vector const &domain, sort const &range)
 
func_decl function (std::string const &name, sort_vector const &domain, sort const &range)
 
func_decl recfun (symbol const &name, unsigned arity, sort const *domain, sort const &range)
 
func_decl recfun (char const *name, unsigned arity, sort const *domain, sort const &range)
 
func_decl recfun (char const *name, sort const &d1, sort const &range)
 
func_decl recfun (char const *name, sort const &d1, sort const &d2, sort const &range)
 
expr select (expr const &a, int i)
 
expr store (expr const &a, expr const &i, expr const &v)
 
expr store (expr const &a, int i, expr const &v)
 
expr store (expr const &a, expr i, int v)
 
expr store (expr const &a, int i, int v)
 
expr 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 last_indexof (expr const &s, expr const &substr)
 
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)
 

Detailed Description

Z3 C++ namespace.

Typedef Documentation

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

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

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

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

Function Documentation

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

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

1606  {
1607  Z3_ast r;
1608  if (a.is_int()) {
1609  expr zero = a.ctx().int_val(0);
1610  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
1611  }
1612  else if (a.is_real()) {
1613  expr zero = a.ctx().real_val(0);
1614  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
1615  }
1616  else {
1617  r = Z3_mk_fpa_abs(a.ctx(), a);
1618  }
1619  a.check_error();
1620  return expr(a.ctx(), r);
1621  }
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.
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_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).
expr z3::as_array ( func_decl &  f)
inline

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

3293  {
3294  Z3_ast r = Z3_mk_as_array(f.ctx(), f);
3295  f.check_error();
3296  return expr(f.ctx(), r);
3297  }
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...
expr z3::ashr ( expr const &  a,
expr const &  b 
)
inline

arithmetic shift right operator for bitvectors

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

Referenced by ashr().

1760 { 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:1658
expr z3::ashr ( expr const &  a,
int  b 
)
inline

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

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

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

1762 { return ashr(b.ctx().num_val(a, b.get_sort()), b); }
expr ashr(int a, expr const &b)
Definition: z3++.h:1762
expr z3::atleast ( expr_vector const &  es,
unsigned  bound 
)
inline

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

2040  {
2041  assert(es.size() > 0);
2042  context& ctx = es[0].ctx();
2043  array<Z3_ast> _es(es);
2044  Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
2045  ctx.check_error();
2046  return expr(ctx, r);
2047  }
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
expr z3::atmost ( expr_vector const &  es,
unsigned  bound 
)
inline

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

2032  {
2033  assert(es.size() > 0);
2034  context& ctx = es[0].ctx();
2035  array<Z3_ast> _es(es);
2036  Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
2037  ctx.check_error();
2038  return expr(ctx, r);
2039  }
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
expr z3::bv2int ( expr const &  a,
bool  is_signed 
)
inline

bit-vector and integer conversions.

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

1772 { Z3_ast r = Z3_mk_bv2int(a.ctx(), a, is_signed); a.check_error(); return expr(a.ctx(), r); }
Z3_ast Z3_API Z3_mk_bv2int(Z3_context c, Z3_ast t1, bool is_signed)
Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 is t...
expr z3::bvadd_no_overflow ( expr const &  a,
expr const &  b,
bool  is_signed 
)
inline

bit-vector overflow/underflow checks

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

1778  {
1779  check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_overflow(a.ctx(), a, b, is_signed); a.check_error(); return expr(a.ctx(), r);
1780  }
void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.
expr z3::bvadd_no_underflow ( expr const &  a,
expr const &  b 
)
inline

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

1781  {
1782  check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1783  }
void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow...
expr z3::bvmul_no_overflow ( expr const &  a,
expr const &  b,
bool  is_signed 
)
inline

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

1796  {
1797  check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_overflow(a.ctx(), a, b, is_signed); a.check_error(); return expr(a.ctx(), r);
1798  }
void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow...
expr z3::bvmul_no_underflow ( expr const &  a,
expr const &  b 
)
inline

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

1799  {
1800  check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1801  }
Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflo...
void check_context(object const &a, object const &b)
Definition: z3++.h:410
expr z3::bvneg_no_overflow ( expr const &  a)
inline

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

1793  {
1794  Z3_ast r = Z3_mk_bvneg_no_overflow(a.ctx(), a); a.check_error(); return expr(a.ctx(), r);
1795  }
Z3_ast Z3_API Z3_mk_bvneg_no_overflow(Z3_context c, Z3_ast t1)
Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector...
expr z3::bvsdiv_no_overflow ( expr const &  a,
expr const &  b 
)
inline

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

1790  {
1791  check_context(a, b); Z3_ast r = Z3_mk_bvsdiv_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1792  }
Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow...
void check_context(object const &a, object const &b)
Definition: z3++.h:410
expr z3::bvsub_no_overflow ( expr const &  a,
expr const &  b 
)
inline

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

1784  {
1785  check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1786  }
void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow...
expr z3::bvsub_no_underflow ( expr const &  a,
expr const &  b,
bool  is_signed 
)
inline

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

1787  {
1788  check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_underflow(a.ctx(), a, b, is_signed); a.check_error(); return expr(a.ctx(), r);
1789  }
Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow...
void check_context(object const &a, object const &b)
Definition: z3++.h:410
void z3::check_context ( object const &  a,
object const &  b 
)
inline
expr z3::concat ( expr const &  a,
expr const &  b 
)
inline

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

Referenced by operator+().

2066  {
2067  check_context(a, b);
2068  Z3_ast r;
2069  if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
2070  Z3_ast _args[2] = { a, b };
2071  r = Z3_mk_seq_concat(a.ctx(), 2, _args);
2072  }
2073  else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
2074  Z3_ast _args[2] = { a, b };
2075  r = Z3_mk_re_concat(a.ctx(), 2, _args);
2076  }
2077  else {
2078  r = Z3_mk_concat(a.ctx(), a, b);
2079  }
2080  a.ctx().check_error();
2081  return expr(a.ctx(), r);
2082  }
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.
bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
void check_context(object const &a, object const &b)
Definition: z3++.h:410
bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.
expr z3::concat ( expr_vector const &  args)
inline

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

2084  {
2085  Z3_ast r;
2086  assert(args.size() > 0);
2087  if (args.size() == 1) {
2088  return args[0];
2089  }
2090  context& ctx = args[0].ctx();
2091  array<Z3_ast> _args(args);
2092  if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
2093  r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
2094  }
2095  else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
2096  r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
2097  }
2098  else {
2099  r = _args[args.size()-1];
2100  for (unsigned i = args.size()-1; i > 0; ) {
2101  --i;
2102  r = Z3_mk_concat(ctx, _args[i], r);
2103  ctx.check_error();
2104  }
2105  }
2106  ctx.check_error();
2107  return expr(ctx, r);
2108  }
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.
bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.
tactic z3::cond ( probe const &  p,
tactic const &  t1,
tactic const &  t2 
)
inline

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

2898  {
2899  check_context(p, t1); check_context(p, t2);
2900  Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2);
2901  t1.check_error();
2902  return tactic(t1.ctx(), r);
2903  }
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:410
expr z3::const_array ( sort const &  d,
expr const &  v 
)
inline

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

3310  {
3311  MK_EXPR2(Z3_mk_const_array, d, v);
3312  }
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:3304
expr z3::distinct ( expr_vector const &  args)
inline

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

2057  {
2058  assert(args.size() > 0);
2059  context& ctx = args[0].ctx();
2060  array<Z3_ast> _args(args);
2061  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
2062  ctx.check_error();
2063  return expr(ctx, r);
2064  }
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]).
expr z3::empty ( sort const &  s)
inline

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

3366  {
3367  Z3_ast r = Z3_mk_seq_empty(s.ctx(), s);
3368  s.check_error();
3369  return expr(s.ctx(), r);
3370  }
Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq)
Create an empty sequence of the sequence sort seq.
expr z3::empty_set ( sort const &  s)
inline

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

3314  {
3316  }
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:3299
bool z3::eq ( ast const &  a,
ast const &  b 
)
inline

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

510 { return Z3_is_eq_ast(a.ctx(), a, b); }
bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2)
Compare terms.
expr z3::exists ( expr const &  x,
expr const &  b 
)
inline

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

1959  {
1960  check_context(x, b);
1961  Z3_app vars[] = {(Z3_app) x};
1962  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1963  }
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:410
expr z3::exists ( expr const &  x1,
expr const &  x2,
expr const &  b 
)
inline

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

1964  {
1965  check_context(x1, b); check_context(x2, b);
1966  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1967  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1968  }
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:410
expr z3::exists ( expr const &  x1,
expr const &  x2,
expr const &  x3,
expr const &  b 
)
inline

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

1969  {
1970  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1971  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1972  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1973  }
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:410
expr z3::exists ( expr const &  x1,
expr const &  x2,
expr const &  x3,
expr const &  x4,
expr const &  b 
)
inline

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

1974  {
1975  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
1976  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1977  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1978  }
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:410
expr z3::exists ( expr_vector const &  xs,
expr const &  b 
)
inline

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

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

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

2887  {
2888  Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
2889  p.check_error();
2890  return tactic(p.ctx(), r);
2891  }
Z3_tactic Z3_API Z3_tactic_fail_if(Z3_context c, Z3_probe p)
Return a tactic that fails if the probe p evaluates to false.
expr z3::fma ( expr const &  a,
expr const &  b,
expr const &  c,
expr const &  rm 
)
inline

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

1631  {
1632  check_context(a, b); check_context(a, c); check_context(a, rm);
1633  assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
1634  Z3_ast r = Z3_mk_fpa_fma(a.ctx(), rm, a, b, c);
1635  a.check_error();
1636  return expr(a.ctx(), r);
1637  }
Z3_ast Z3_API Z3_mk_fpa_fma(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Floating-point fused multiply-add.
void check_context(object const &a, object const &b)
Definition: z3++.h:410
expr z3::forall ( expr const &  x,
expr const &  b 
)
inline

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

1935  {
1936  check_context(x, b);
1937  Z3_app vars[] = {(Z3_app) x};
1938  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1939  }
void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_ast Z3_API Z3_mk_forall_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables...
expr z3::forall ( expr const &  x1,
expr const &  x2,
expr const &  b 
)
inline

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

1940  {
1941  check_context(x1, b); check_context(x2, b);
1942  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1943  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1944  }
void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_ast Z3_API Z3_mk_forall_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables...
expr z3::forall ( expr const &  x1,
expr const &  x2,
expr const &  x3,
expr const &  b 
)
inline

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

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

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

1950  {
1951  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
1952  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
1953  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1954  }
void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_ast Z3_API Z3_mk_forall_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables...
expr z3::forall ( expr_vector const &  xs,
expr const &  b 
)
inline

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

1955  {
1956  array<Z3_app> vars(xs);
1957  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);
1958  }
Z3_ast Z3_API Z3_mk_forall_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables...
expr z3::full_set ( sort const &  s)
inline

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

3318  {
3320  }
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:3299
func_decl z3::function ( symbol const &  name,
unsigned  arity,
sort const *  domain,
sort const &  range 
)
inline

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

3215  {
3216  return range.ctx().function(name, arity, domain, range);
3217  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3431
context & ctx() const
Definition: z3++.h:406
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:2979
func_decl z3::function ( char const *  name,
unsigned  arity,
sort const *  domain,
sort const &  range 
)
inline

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

3218  {
3219  return range.ctx().function(name, arity, domain, range);
3220  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3431
context & ctx() const
Definition: z3++.h:406
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:2979
func_decl z3::function ( char const *  name,
sort const &  domain,
sort const &  range 
)
inline

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

3221  {
3222  return range.ctx().function(name, domain, range);
3223  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3431
context & ctx() const
Definition: z3++.h:406
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:2979
func_decl z3::function ( char const *  name,
sort const &  d1,
sort const &  d2,
sort const &  range 
)
inline

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

3224  {
3225  return range.ctx().function(name, d1, d2, range);
3226  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3431
context & ctx() const
Definition: z3++.h:406
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:2979
func_decl z3::function ( char const *  name,
sort const &  d1,
sort const &  d2,
sort const &  d3,
sort const &  range 
)
inline

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

3227  {
3228  return range.ctx().function(name, d1, d2, d3, range);
3229  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3431
context & ctx() const
Definition: z3++.h:406
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:2979
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 3230 of file z3++.h.

3230  {
3231  return range.ctx().function(name, d1, d2, d3, d4, range);
3232  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3431
context & ctx() const
Definition: z3++.h:406
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:2979
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 3233 of file z3++.h.

3233  {
3234  return range.ctx().function(name, d1, d2, d3, d4, d5, range);
3235  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3431
context & ctx() const
Definition: z3++.h:406
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:2979
func_decl z3::function ( char const *  name,
sort_vector const &  domain,
sort const &  range 
)
inline

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

3236  {
3237  return range.ctx().function(name, domain, range);
3238  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3431
context & ctx() const
Definition: z3++.h:406
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:2979
func_decl z3::function ( std::string const &  name,
sort_vector const &  domain,
sort const &  range 
)
inline

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

3239  {
3240  return range.ctx().function(name.c_str(), domain, range);
3241  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3431
context & ctx() const
Definition: z3++.h:406
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:2979
expr z3::implies ( expr const &  a,
expr const &  b 
)
inline

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

Referenced by implies().

1261  {
1262  assert(a.is_bool() && b.is_bool());
1263  _Z3_MK_BIN_(a, b, Z3_mk_implies);
1264  }
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:1254
expr z3::implies ( expr const &  a,
bool  b 
)
inline

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

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

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

1266 { return implies(b.ctx().bool_val(a), b); }
expr implies(bool a, expr const &b)
Definition: z3++.h:1266
expr z3::in_re ( expr const &  s,
expr const &  re 
)
inline

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

3398  {
3399  MK_EXPR2(Z3_mk_seq_in_re, s, re);
3400  }
#define MK_EXPR2(_fn, _arg1, _arg2)
Definition: z3++.h:3304
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.
expr z3::indexof ( expr const &  s,
expr const &  substr,
expr const &  offset 
)
inline

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

3383  {
3384  check_context(s, substr); check_context(s, offset);
3385  Z3_ast r = Z3_mk_seq_index(s.ctx(), s, substr, offset);
3386  s.check_error();
3387  return expr(s.ctx(), r);
3388  }
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:410
expr z3::int2bv ( unsigned  n,
expr const &  a 
)
inline

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

1773 { Z3_ast r = Z3_mk_int2bv(a.ctx(), n, a); a.check_error(); return expr(a.ctx(), r); }
Z3_ast Z3_API Z3_mk_int2bv(Z3_context c, unsigned n, Z3_ast t1)
Create an n bit bit-vector from the integer argument t1.
expr z3::is_int ( expr const &  e)
inline

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

1309 { _Z3_MK_UN_(e, Z3_mk_is_int); }
#define _Z3_MK_UN_(a, mkun)
Definition: z3++.h:1301
Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1)
Check if a real number is an integer.
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 1645 of file z3++.h.

1645  {
1646  check_context(c, t); check_context(c, e);
1647  assert(c.is_bool());
1648  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
1649  c.check_error();
1650  return expr(c.ctx(), r);
1651  }
void check_context(object const &a, object const &b)
Definition: z3++.h:410
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).
expr z3::lambda ( expr const &  x,
expr const &  b 
)
inline

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

1983  {
1984  check_context(x, b);
1985  Z3_app vars[] = {(Z3_app) x};
1986  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 1, vars, b); b.check_error(); return expr(b.ctx(), r);
1987  }
Z3_ast Z3_API Z3_mk_lambda_const(Z3_context c, unsigned num_bound, Z3_app const bound[], Z3_ast body)
Create a lambda expression using a list of constants that form the set of bound variables.
void check_context(object const &a, object const &b)
Definition: z3++.h:410
expr z3::lambda ( expr const &  x1,
expr const &  x2,
expr const &  b 
)
inline

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

1988  {
1989  check_context(x1, b); check_context(x2, b);
1990  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1991  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 2, vars, b); b.check_error(); return expr(b.ctx(), r);
1992  }
Z3_ast Z3_API Z3_mk_lambda_const(Z3_context c, unsigned num_bound, Z3_app const bound[], Z3_ast body)
Create a lambda expression using a list of constants that form the set of bound variables.
void check_context(object const &a, object const &b)
Definition: z3++.h:410
expr z3::lambda ( expr const &  x1,
expr const &  x2,
expr const &  x3,
expr const &  b 
)
inline

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

1993  {
1994  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1995  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1996  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 3, vars, b); b.check_error(); return expr(b.ctx(), r);
1997  }
Z3_ast Z3_API Z3_mk_lambda_const(Z3_context c, unsigned num_bound, Z3_app const bound[], Z3_ast body)
Create a lambda expression using a list of constants that form the set of bound variables.
void check_context(object const &a, object const &b)
Definition: z3++.h:410
expr z3::lambda ( expr const &  x1,
expr const &  x2,
expr const &  x3,
expr const &  x4,
expr const &  b 
)
inline

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

1998  {
1999  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2000  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2001  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 4, vars, b); b.check_error(); return expr(b.ctx(), r);
2002  }
Z3_ast Z3_API Z3_mk_lambda_const(Z3_context c, unsigned num_bound, Z3_app const bound[], Z3_ast body)
Create a lambda expression using a list of constants that form the set of bound variables.
void check_context(object const &a, object const &b)
Definition: z3++.h:410
expr z3::lambda ( expr_vector const &  xs,
expr const &  b 
)
inline

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

2003  {
2004  array<Z3_app> vars(xs);
2005  Z3_ast r = Z3_mk_lambda_const(b.ctx(), vars.size(), vars.ptr(), b); b.check_error(); return expr(b.ctx(), r);
2006  }
Z3_ast Z3_API Z3_mk_lambda_const(Z3_context c, unsigned num_bound, Z3_app const bound[], Z3_ast body)
Create a lambda expression using a list of constants that form the set of bound variables.
expr z3::last_indexof ( expr const &  s,
expr const &  substr 
)
inline

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

3389  {
3390  check_context(s, substr);
3391  Z3_ast r = Z3_mk_seq_last_index(s.ctx(), s, substr);
3392  s.check_error();
3393  return expr(s.ctx(), r);
3394  }
void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_ast Z3_API Z3_mk_seq_last_index(Z3_context c, Z3_ast, Z3_ast substr)
Return the last occurrence of substr in s. If s does not contain substr, then the value is -1...
func_decl z3::linear_order ( sort const &  a,
unsigned  index 
)
inline

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

1809  {
1810  return to_func_decl(a.ctx(), Z3_mk_linear_order(a.ctx(), a, index));
1811  }
func_decl to_func_decl(context &c, Z3_func_decl f)
Definition: z3++.h:1672
Z3_func_decl Z3_API Z3_mk_linear_order(Z3_context c, Z3_sort a, unsigned id)
create a linear ordering relation over signature a. The relation is identified by the index id...
expr z3::lshr ( expr const &  a,
expr const &  b 
)
inline

logic shift right operator for bitvectors

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

Referenced by lshr().

1753 { 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:1658
expr z3::lshr ( expr const &  a,
int  b 
)
inline

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

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

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

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

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

Referenced by repeat().

1591  {
1592  check_context(a, b);
1593  Z3_ast r;
1594  if (a.is_arith()) {
1595  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), a, b);
1596  }
1597  else if (a.is_bv()) {
1598  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), a, b);
1599  }
1600  else {
1601  assert(a.is_fpa());
1602  r = Z3_mk_fpa_max(a.ctx(), a, b);
1603  }
1604  return expr(a.ctx(), r);
1605  }
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2)
Maximum of floating-point numbers.
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
void check_context(object const &a, object const &b)
Definition: z3++.h:410
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).
expr z3::min ( expr const &  a,
expr const &  b 
)
inline

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

1576  {
1577  check_context(a, b);
1578  Z3_ast r;
1579  if (a.is_arith()) {
1580  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), b, a);
1581  }
1582  else if (a.is_bv()) {
1583  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), b, a);
1584  }
1585  else {
1586  assert(a.is_fpa());
1587  r = Z3_mk_fpa_min(a.ctx(), a, b);
1588  }
1589  return expr(a.ctx(), r);
1590  }
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
void check_context(object const &a, object const &b)
Definition: z3++.h:410
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).
Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2)
Minimum of floating-point numbers.
expr z3::mk_and ( expr_vector const &  args)
inline

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

2116  {
2117  array<Z3_ast> _args(args);
2118  Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2119  args.check_error();
2120  return expr(args.ctx(), r);
2121  }
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].
expr z3::mk_or ( expr_vector const &  args)
inline

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

2110  {
2111  array<Z3_ast> _args(args);
2112  Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2113  args.check_error();
2114  return expr(args.ctx(), r);
2115  }
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].
expr z3::mod ( expr const &  a,
expr const &  b 
)
inline

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

Referenced by mod(), and operator%().

1273  {
1274  if (a.is_bv()) {
1275  _Z3_MK_BIN_(a, b, Z3_mk_bvsmod);
1276  }
1277  else {
1278  _Z3_MK_BIN_(a, b, Z3_mk_mod);
1279  }
1280  }
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.
Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows divisor).
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1254
expr z3::mod ( expr const &  a,
int  b 
)
inline

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

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

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

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

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

1573 { 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:410
expr z3::nor ( expr const &  a,
expr const &  b 
)
inline

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

1574 { 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:410
expr z3::operator! ( expr const &  a)
inline
Precondition
a.is_bool()

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

1307 { assert(a.is_bool()); _Z3_MK_UN_(a, Z3_mk_not); }
#define _Z3_MK_UN_(a, mkun)
Definition: z3++.h:1301
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).
probe z3::operator! ( probe const &  p)
inline

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

2751  {
2752  Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
2753  }
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.
expr z3::operator!= ( expr const &  a,
expr const &  b 
)
inline

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

1347  {
1348  check_context(a, b);
1349  Z3_ast args[2] = { a, b };
1350  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1351  a.check_error();
1352  return expr(a.ctx(), r);
1353  }
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:410
expr z3::operator!= ( expr const &  a,
int  b 
)
inline

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

1354 { assert(a.is_arith() || a.is_bv() || a.is_fpa()); return a != a.ctx().num_val(b, a.get_sort()); }
expr z3::operator!= ( int  a,
expr const &  b 
)
inline

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

1355 { assert(b.is_arith() || b.is_bv() || b.is_fpa()); return b.ctx().num_val(a, b.get_sort()) != b; }
expr z3::operator% ( expr const &  a,
expr const &  b 
)
inline

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

1284 { return mod(a, b); }
expr mod(int a, expr const &b)
Definition: z3++.h:1282
expr z3::operator% ( expr const &  a,
int  b 
)
inline

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

1285 { return mod(a, b); }
expr mod(int a, expr const &b)
Definition: z3++.h:1282
expr z3::operator% ( int  a,
expr const &  b 
)
inline

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

1286 { return mod(a, b); }
expr mod(int a, expr const &b)
Definition: z3++.h:1282
expr z3::operator& ( expr const &  a,
expr const &  b 
)
inline

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

1561 { 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:410
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.
expr z3::operator& ( expr const &  a,
int  b 
)
inline

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

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

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

1563 { return b.ctx().num_val(a, b.get_sort()) & b; }
tactic z3::operator& ( tactic const &  t1,
tactic const &  t2 
)
inline

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

2632  {
2633  check_context(t1, t2);
2634  Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
2635  t1.check_error();
2636  return tactic(t1.ctx(), r);
2637  }
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:410
expr z3::operator&& ( expr const &  a,
expr const &  b 
)
inline
Precondition
a.is_bool()
b.is_bool()

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

1313  {
1314  check_context(a, b);
1315  assert(a.is_bool() && b.is_bool());
1316  Z3_ast args[2] = { a, b };
1317  Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
1318  a.check_error();
1319  return expr(a.ctx(), r);
1320  }
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:410
expr z3::operator&& ( expr const &  a,
bool  b 
)
inline
Precondition
a.is_bool()

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

1322 { return a && a.ctx().bool_val(b); }
expr z3::operator&& ( bool  a,
expr const &  b 
)
inline
Precondition
b.is_bool()

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

1323 { return b.ctx().bool_val(a) && b; }
probe z3::operator&& ( probe const &  p1,
probe const &  p2 
)
inline

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

2745  {
2746  check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2747  }
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:410
expr z3::operator* ( expr const &  a,
expr const &  b 
)
inline

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

1387  {
1388  check_context(a, b);
1389  Z3_ast r = 0;
1390  if (a.is_arith() && b.is_arith()) {
1391  Z3_ast args[2] = { a, b };
1392  r = Z3_mk_mul(a.ctx(), 2, args);
1393  }
1394  else if (a.is_bv() && b.is_bv()) {
1395  r = Z3_mk_bvmul(a.ctx(), a, b);
1396  }
1397  else if (a.is_fpa() && b.is_fpa()) {
1398  r = Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1399  }
1400  else {
1401  // operator is not supported by given arguments.
1402  assert(false);
1403  }
1404  a.check_error();
1405  return expr(a.ctx(), r);
1406  }
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].
Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point multiplication.
void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
expr z3::operator* ( expr const &  a,
int  b 
)
inline

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

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

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

1408 { return b.ctx().num_val(a, b.get_sort()) * b; }
expr z3::operator+ ( expr const &  a,
expr const &  b 
)
inline

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

1357  {
1358  check_context(a, b);
1359  Z3_ast r = 0;
1360  if (a.is_arith() && b.is_arith()) {
1361  Z3_ast args[2] = { a, b };
1362  r = Z3_mk_add(a.ctx(), 2, args);
1363  }
1364  else if (a.is_bv() && b.is_bv()) {
1365  r = Z3_mk_bvadd(a.ctx(), a, b);
1366  }
1367  else if (a.is_seq() && b.is_seq()) {
1368  return concat(a, b);
1369  }
1370  else if (a.is_re() && b.is_re()) {
1371  Z3_ast _args[2] = { a, b };
1372  r = Z3_mk_re_union(a.ctx(), 2, _args);
1373  }
1374  else if (a.is_fpa() && b.is_fpa()) {
1375  r = Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1376  }
1377  else {
1378  // operator is not supported by given arguments.
1379  assert(false);
1380  }
1381  a.check_error();
1382  return expr(a.ctx(), r);
1383  }
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].
Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point addition.
expr concat(expr_vector const &args)
Definition: z3++.h:2084
void check_context(object const &a, object const &b)
Definition: z3++.h:410
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's complement addition.
expr z3::operator+ ( expr const &  a,
int  b 
)
inline

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

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

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

1385 { return b.ctx().num_val(a, b.get_sort()) + b; }
expr z3::operator- ( expr const &  a)
inline

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

1450  {
1451  Z3_ast r = 0;
1452  if (a.is_arith()) {
1453  r = Z3_mk_unary_minus(a.ctx(), a);
1454  }
1455  else if (a.is_bv()) {
1456  r = Z3_mk_bvneg(a.ctx(), a);
1457  }
1458  else if (a.is_fpa()) {
1459  r = Z3_mk_fpa_neg(a.ctx(), a);
1460  }
1461  else {
1462  // operator is not supported by given arguments.
1463  assert(false);
1464  }
1465  a.check_error();
1466  return expr(a.ctx(), r);
1467  }
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_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.
expr z3::operator- ( expr const &  a,
expr const &  b 
)
inline

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

1469  {
1470  check_context(a, b);
1471  Z3_ast r = 0;
1472  if (a.is_arith() && b.is_arith()) {
1473  Z3_ast args[2] = { a, b };
1474  r = Z3_mk_sub(a.ctx(), 2, args);
1475  }
1476  else if (a.is_bv() && b.is_bv()) {
1477  r = Z3_mk_bvsub(a.ctx(), a, b);
1478  }
1479  else if (a.is_fpa() && b.is_fpa()) {
1480  r = Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1481  }
1482  else {
1483  // operator is not supported by given arguments.
1484  assert(false);
1485  }
1486  a.check_error();
1487  return expr(a.ctx(), r);
1488  }
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:410
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point subtraction.
expr z3::operator- ( expr const &  a,
int  b 
)
inline

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

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

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

1490 { return b.ctx().num_val(a, b.get_sort()) - b; }
expr z3::operator/ ( expr const &  a,
expr const &  b 
)
inline

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

1428  {
1429  check_context(a, b);
1430  Z3_ast r = 0;
1431  if (a.is_arith() && b.is_arith()) {
1432  r = Z3_mk_div(a.ctx(), a, b);
1433  }
1434  else if (a.is_bv() && b.is_bv()) {
1435  r = Z3_mk_bvsdiv(a.ctx(), a, b);
1436  }
1437  else if (a.is_fpa() && b.is_fpa()) {
1438  r = Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1439  }
1440  else {
1441  // operator is not supported by given arguments.
1442  assert(false);
1443  }
1444  a.check_error();
1445  return expr(a.ctx(), r);
1446  }
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two'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.
Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point division.
void check_context(object const &a, object const &b)
Definition: z3++.h:410
expr z3::operator/ ( expr const &  a,
int  b 
)
inline

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

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

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

1448 { return b.ctx().num_val(a, b.get_sort()) / b; }
expr z3::operator< ( expr const &  a,
expr const &  b 
)
inline

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

1517  {
1518  check_context(a, b);
1519  Z3_ast r = 0;
1520  if (a.is_arith() && b.is_arith()) {
1521  r = Z3_mk_lt(a.ctx(), a, b);
1522  }
1523  else if (a.is_bv() && b.is_bv()) {
1524  r = Z3_mk_bvslt(a.ctx(), a, b);
1525  }
1526  else if (a.is_fpa() && b.is_fpa()) {
1527  r = Z3_mk_fpa_lt(a.ctx(), a, b);
1528  }
1529  else {
1530  // operator is not supported by given arguments.
1531  assert(false);
1532  }
1533  a.check_error();
1534  return expr(a.ctx(), r);
1535  }
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two'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:410
Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than.
expr z3::operator< ( expr const &  a,
int  b 
)
inline

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

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

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

1537 { return b.ctx().num_val(a, b.get_sort()) < b; }
probe z3::operator< ( probe const &  p1,
probe const &  p2 
)
inline

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

2730  {
2731  check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2732  }
void check_context(object const &a, object const &b)
Definition: z3++.h:410
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...
probe z3::operator< ( probe const &  p1,
double  p2 
)
inline

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

2733 { return p1 < probe(p1.ctx(), p2); }
probe z3::operator< ( double  p1,
probe const &  p2 
)
inline

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

2734 { return probe(p2.ctx(), p1) < p2; }
std::ostream& z3::operator<< ( std::ostream &  out,
exception const &  e 
)
inline

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

90 { out << e.msg(); return out; }
std::ostream& z3::operator<< ( std::ostream &  out,
symbol const &  s 
)
inline

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

425  {
426  if (s.kind() == Z3_INT_SYMBOL)
427  out << "k!" << s.to_int();
428  else
429  out << s.str().c_str();
430  return out;
431  }
std::ostream& z3::operator<< ( std::ostream &  out,
param_descrs const &  d 
)
inline

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

456 { return out << d.to_string(); }
std::ostream& z3::operator<< ( std::ostream &  out,
params const &  p 
)
inline

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

480  {
481  out << Z3_params_to_string(p.ctx(), p); return out;
482  }
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...
std::ostream& z3::operator<< ( std::ostream &  out,
ast const &  n 
)
inline

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

506  {
507  out << Z3_ast_to_string(n.ctx(), n.m_ast); return out;
508  }
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.
std::ostream& z3::operator<< ( std::ostream &  out,
model const &  m 
)
inline

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

2256 { 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.
std::ostream& z3::operator<< ( std::ostream &  out,
stats const &  s 
)
inline

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

2285 { 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.
std::ostream& z3::operator<< ( std::ostream &  out,
check_result  r 
)
inline

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

2288  {
2289  if (r == unsat) out << "unsat";
2290  else if (r == sat) out << "sat";
2291  else out << "unknown";
2292  return out;
2293  }
Definition: z3++.h:130
std::ostream& z3::operator<< ( std::ostream &  out,
solver const &  s 
)
inline

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

2507 { 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.
std::ostream& z3::operator<< ( std::ostream &  out,
goal const &  g 
)
inline

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

2566 { 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.
std::ostream& z3::operator<< ( std::ostream &  out,
apply_result const &  r 
)
inline

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

2590 { 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.
std::ostream& z3::operator<< ( std::ostream &  out,
optimize const &  s 
)
inline

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

2843 { 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.
std::ostream& z3::operator<< ( std::ostream &  out,
fixedpoint const &  f 
)
inline

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

2885 { 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.
expr z3::operator<= ( expr const &  a,
expr const &  b 
)
inline

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

1492  {
1493  check_context(a, b);
1494  Z3_ast r = 0;
1495  if (a.is_arith() && b.is_arith()) {
1496  r = Z3_mk_le(a.ctx(), a, b);
1497  }
1498  else if (a.is_bv() && b.is_bv()) {
1499  r = Z3_mk_bvsle(a.ctx(), a, b);
1500  }
1501  else if (a.is_fpa() && b.is_fpa()) {
1502  r = Z3_mk_fpa_leq(a.ctx(), a, b);
1503  }
1504  else {
1505  // operator is not supported by given arguments.
1506  assert(false);
1507  }
1508  a.check_error();
1509  return expr(a.ctx(), r);
1510  }
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's complement signed less than or equal to.
void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than or equal.
expr z3::operator<= ( expr const &  a,
int  b 
)
inline

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

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

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

1512 { return b.ctx().num_val(a, b.get_sort()) <= b; }
probe z3::operator<= ( probe const &  p1,
probe const &  p2 
)
inline

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

2720  {
2721  check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2722  }
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:410
probe z3::operator<= ( probe const &  p1,
double  p2 
)
inline

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

2723 { return p1 <= probe(p1.ctx(), p2); }
probe z3::operator<= ( double  p1,
probe const &  p2 
)
inline

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

2724 { return probe(p2.ctx(), p1) <= p2; }
expr z3::operator== ( expr const &  a,
expr const &  b 
)
inline

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

1338  {
1339  check_context(a, b);
1340  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1341  a.check_error();
1342  return expr(a.ctx(), r);
1343  }
void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.
expr z3::operator== ( expr const &  a,
int  b 
)
inline

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

1344 { assert(a.is_arith() || a.is_bv() || a.is_fpa()); return a == a.ctx().num_val(b, a.get_sort()); }
expr z3::operator== ( int  a,
expr const &  b 
)
inline

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

1345 { assert(b.is_arith() || b.is_bv() || b.is_fpa()); return b.ctx().num_val(a, b.get_sort()) == b; }
probe z3::operator== ( probe const &  p1,
probe const &  p2 
)
inline

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

2740  {
2741  check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2742  }
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:410
probe z3::operator== ( probe const &  p1,
double  p2 
)
inline

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

2743 { return p1 == probe(p1.ctx(), p2); }
probe z3::operator== ( double  p1,
probe const &  p2 
)
inline

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

2744 { return probe(p2.ctx(), p1) == p2; }
expr z3::operator> ( expr const &  a,
expr const &  b 
)
inline

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

1539  {
1540  check_context(a, b);
1541  Z3_ast r = 0;
1542  if (a.is_arith() && b.is_arith()) {
1543  r = Z3_mk_gt(a.ctx(), a, b);
1544  }
1545  else if (a.is_bv() && b.is_bv()) {
1546  r = Z3_mk_bvsgt(a.ctx(), a, b);
1547  }
1548  else if (a.is_fpa() && b.is_fpa()) {
1549  r = Z3_mk_fpa_gt(a.ctx(), a, b);
1550  }
1551  else {
1552  // operator is not supported by given arguments.
1553  assert(false);
1554  }
1555  a.check_error();
1556  return expr(a.ctx(), r);
1557  }
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two'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:410
Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than.
expr z3::operator> ( expr const &  a,
int  b 
)
inline

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

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

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

1559 { return b.ctx().num_val(a, b.get_sort()) > b; }
probe z3::operator> ( probe const &  p1,
probe const &  p2 
)
inline

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

2735  {
2736  check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2737  }
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:410
probe z3::operator> ( probe const &  p1,
double  p2 
)
inline

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

2738 { return p1 > probe(p1.ctx(), p2); }
probe z3::operator> ( double  p1,
probe const &  p2 
)
inline

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

2739 { return probe(p2.ctx(), p1) > p2; }
expr z3::operator>= ( expr const &  a,
expr const &  b 
)
inline

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

1411  {
1412  check_context(a, b);
1413  Z3_ast r = 0;
1414  if (a.is_arith() && b.is_arith()) {
1415  r = Z3_mk_ge(a.ctx(), a, b);
1416  }
1417  else if (a.is_bv() && b.is_bv()) {
1418  r = Z3_mk_bvsge(a.ctx(), a, b);
1419  }
1420  else {
1421  // operator is not supported by given arguments.
1422  assert(false);
1423  }
1424  a.check_error();
1425  return expr(a.ctx(), r);
1426  }
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's complement signed greater than or equal to.
void check_context(object const &a, object const &b)
Definition: z3++.h:410
expr z3::operator>= ( expr const &  a,
int  b 
)
inline

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

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

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

1515 { return b.ctx().num_val(a, b.get_sort()) >= b; }
probe z3::operator>= ( probe const &  p1,
probe const &  p2 
)
inline

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

2725  {
2726  check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2727  }
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:410
probe z3::operator>= ( probe const &  p1,
double  p2 
)
inline

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

2728 { return p1 >= probe(p1.ctx(), p2); }
probe z3::operator>= ( double  p1,
probe const &  p2 
)
inline

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

2729 { return probe(p2.ctx(), p1) >= p2; }
expr z3::operator^ ( expr const &  a,
expr const &  b 
)
inline

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

1565 { 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:410
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
expr z3::operator^ ( expr const &  a,
int  b 
)
inline

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

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

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

1567 { return b.ctx().num_val(a, b.get_sort()) ^ b; }
expr z3::operator| ( expr const &  a,
expr const &  b 
)
inline

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

1569 { 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:410
expr z3::operator| ( expr const &  a,
int  b 
)
inline

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

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

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

1571 { return b.ctx().num_val(a, b.get_sort()) | b; }
tactic z3::operator| ( tactic const &  t1,
tactic const &  t2 
)
inline

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

2639  {
2640  check_context(t1, t2);
2641  Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
2642  t1.check_error();
2643  return tactic(t1.ctx(), r);
2644  }
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:410
expr z3::operator|| ( expr const &  a,
expr const &  b 
)
inline
Precondition
a.is_bool()
b.is_bool()

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

1325  {
1326  check_context(a, b);
1327  assert(a.is_bool() && b.is_bool());
1328  Z3_ast args[2] = { a, b };
1329  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1330  a.check_error();
1331  return expr(a.ctx(), r);
1332  }
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:410
expr z3::operator|| ( expr const &  a,
bool  b 
)
inline
Precondition
a.is_bool()

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

1334 { return a || a.ctx().bool_val(b); }
expr z3::operator|| ( bool  a,
expr const &  b 
)
inline
Precondition
b.is_bool()

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

1336 { return b.ctx().bool_val(a) || b; }
probe z3::operator|| ( probe const &  p1,
probe const &  p2 
)
inline

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

2748  {
2749  check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2750  }
void check_context(object const &a, object const &b)
Definition: z3++.h:410
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.
expr z3::operator~ ( expr const &  a)
inline

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

1629 { 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.
expr z3::option ( expr const &  re)
inline

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

3404  {
3406  }
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:3299
tactic z3::par_and_then ( tactic const &  t1,
tactic const &  t2 
)
inline

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

2671  {
2672  check_context(t1, t2);
2673  Z3_tactic r = Z3_tactic_par_and_then(t1.ctx(), t1, t2);
2674  t1.check_error();
2675  return tactic(t1.ctx(), r);
2676  }
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:410
tactic z3::par_or ( unsigned  n,
tactic const *  tactics 
)
inline

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

2662  {
2663  if (n == 0) {
2664  Z3_THROW(exception("a non-zero number of tactics need to be passed to par_or"));
2665  }
2666  array<Z3_tactic> buffer(n);
2667  for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];
2668  return tactic(tactics[0].ctx(), Z3_tactic_par_or(tactics[0].ctx(), n, buffer.ptr()));
2669  }
#define Z3_THROW(x)
Definition: z3++.h:96
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.
func_decl z3::partial_order ( sort const &  a,
unsigned  index 
)
inline

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

1812  {
1813  return to_func_decl(a.ctx(), Z3_mk_partial_order(a.ctx(), a, index));
1814  }
func_decl to_func_decl(context &c, Z3_func_decl f)
Definition: z3++.h:1672
Z3_func_decl Z3_API Z3_mk_partial_order(Z3_context c, Z3_sort a, unsigned id)
create a partial ordering relation over signature a and index id.
expr z3::pbeq ( expr_vector const &  es,
int const *  coeffs,
int  bound 
)
inline

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

2024  {
2025  assert(es.size() > 0);
2026  context& ctx = es[0].ctx();
2027  array<Z3_ast> _es(es);
2028  Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
2029  ctx.check_error();
2030  return expr(ctx, r);
2031  }
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.
expr z3::pbge ( expr_vector const &  es,
int const *  coeffs,
int  bound 
)
inline

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

2016  {
2017  assert(es.size() > 0);
2018  context& ctx = es[0].ctx();
2019  array<Z3_ast> _es(es);
2020  Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
2021  ctx.check_error();
2022  return expr(ctx, r);
2023  }
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.
expr z3::pble ( expr_vector const &  es,
int const *  coeffs,
int  bound 
)
inline

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

2008  {
2009  assert(es.size() > 0);
2010  context& ctx = es[0].ctx();
2011  array<Z3_ast> _es(es);
2012  Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
2013  ctx.check_error();
2014  return expr(ctx, r);
2015  }
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.
func_decl z3::piecewise_linear_order ( sort const &  a,
unsigned  index 
)
inline

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

1815  {
1816  return to_func_decl(a.ctx(), Z3_mk_piecewise_linear_order(a.ctx(), a, index));
1817  }
func_decl to_func_decl(context &c, Z3_func_decl f)
Definition: z3++.h:1672
Z3_func_decl Z3_API Z3_mk_piecewise_linear_order(Z3_context c, Z3_sort a, unsigned id)
create a piecewise linear ordering relation over signature a and index id.
expr z3::plus ( expr const &  re)
inline

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

3401  {
3402  MK_EXPR1(Z3_mk_re_plus, re);
3403  }
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:3299
expr z3::prefixof ( expr const &  a,
expr const &  b 
)
inline

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

3377  {
3378  check_context(a, b);
3379  Z3_ast r = Z3_mk_seq_prefix(a.ctx(), a, b);
3380  a.check_error();
3381  return expr(a.ctx(), r);
3382  }
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:410
expr z3::pw ( expr const &  a,
expr const &  b 
)
inline

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

Referenced by pw().

1269 { _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:1254
expr z3::pw ( expr const &  a,
int  b 
)
inline

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

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

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

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

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

Referenced by context::function(), function(), and context::recfun().

3431  {
3432  check_context(lo, hi);
3433  Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
3434  lo.check_error();
3435  return expr(lo.ctx(), r);
3436  }
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:410
expr z3::re_complement ( expr const &  a)
inline

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

3428  {
3430  }
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:3299
expr z3::re_empty ( sort const &  s)
inline

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

3410  {
3411  Z3_ast r = Z3_mk_re_empty(s.ctx(), s);
3412  s.check_error();
3413  return expr(s.ctx(), r);
3414  }
Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re)
Create an empty regular expression of sort re.
expr z3::re_full ( sort const &  s)
inline

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

3415  {
3416  Z3_ast r = Z3_mk_re_full(s.ctx(), s);
3417  s.check_error();
3418  return expr(s.ctx(), r);
3419  }
Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re)
Create an universal regular expression of sort re.
expr z3::re_intersect ( expr_vector const &  args)
inline

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

3420  {
3421  assert(args.size() > 0);
3422  context& ctx = args[0].ctx();
3423  array<Z3_ast> _args(args);
3424  Z3_ast r = Z3_mk_re_intersect(ctx, _args.size(), _args.ptr());
3425  ctx.check_error();
3426  return expr(ctx, r);
3427  }
Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[])
Create the intersection of the regular languages.
func_decl z3::recfun ( symbol const &  name,
unsigned  arity,
sort const *  domain,
sort const &  range 
)
inline

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

3243  {
3244  return range.ctx().recfun(name, arity, domain, range);
3245  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3431
context & ctx() const
Definition: z3++.h:406
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3050
func_decl z3::recfun ( char const *  name,
unsigned  arity,
sort const *  domain,
sort const &  range 
)
inline

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

3246  {
3247  return range.ctx().recfun(name, arity, domain, range);
3248  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3431
context & ctx() const
Definition: z3++.h:406
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3050
func_decl z3::recfun ( char const *  name,
sort const &  d1,
sort const &  range 
)
inline

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

3249  {
3250  return range.ctx().recfun(name, d1, range);
3251  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3431
context & ctx() const
Definition: z3++.h:406
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3050
func_decl z3::recfun ( char const *  name,
sort const &  d1,
sort const &  d2,
sort const &  range 
)
inline

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

3252  {
3253  return range.ctx().recfun(name, d1, d2, range);
3254  }
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3431
context & ctx() const
Definition: z3++.h:406
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3050
expr z3::rem ( expr const &  a,
expr const &  b 
)
inline

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

Referenced by rem().

1289  {
1290  if (a.is_fpa() && b.is_fpa()) {
1291  _Z3_MK_BIN_(a, b, Z3_mk_fpa_rem);
1292  } else {
1293  _Z3_MK_BIN_(a, b, Z3_mk_rem);
1294  }
1295  }
Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point remainder.
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:1254
expr z3::rem ( expr const &  a,
int  b 
)
inline

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

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

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

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

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

2646  {
2647  Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
2648  t.check_error();
2649  return tactic(t.ctx(), r);
2650  }
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...
expr max(expr const &a, expr const &b)
Definition: z3++.h:1591
void z3::reset_params ( )
inline

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

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

forward declarations

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

Referenced by expr::operator[](), and select().

3256  {
3257  check_context(a, i);
3258  Z3_ast r = Z3_mk_select(a.ctx(), a, i);
3259  a.check_error();
3260  return expr(a.ctx(), r);
3261  }
void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i)
Array read. The argument a is the array and i is the index of the array that gets read...
expr select ( expr const &  a,
expr_vector const &  i 
)
inline

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

3265  {
3266  check_context(a, i);
3267  array<Z3_ast> idxs(i);
3268  Z3_ast r = Z3_mk_select_n(a.ctx(), a, idxs.size(), idxs.ptr());
3269  a.check_error();
3270  return expr(a.ctx(), r);
3271  }
void check_context(object const &a, object const &b)
Definition: z3++.h:410
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...
expr z3::select ( expr const &  a,
int  i 
)
inline

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

3262  {
3263  return select(a, a.ctx().num_val(i, a.get_sort().array_domain()));
3264  }
expr select(expr const &a, int i)
Definition: z3++.h:3262
expr z3::set_add ( expr const &  s,
expr const &  e 
)
inline

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

3322  {
3323  MK_EXPR2(Z3_mk_set_add, s, e);
3324  }
#define MK_EXPR2(_fn, _arg1, _arg2)
Definition: z3++.h:3304
Z3_ast Z3_API Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem)
Add an element to a set.
expr z3::set_complement ( expr const &  a)
inline

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

3350  {
3352  }
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:3299
expr z3::set_del ( expr const &  s,
expr const &  e 
)
inline

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

3326  {
3327  MK_EXPR2(Z3_mk_set_del, s, e);
3328  }
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:3304
expr z3::set_difference ( expr const &  a,
expr const &  b 
)
inline

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

3346  {
3348  }
#define MK_EXPR2(_fn, _arg1, _arg2)
Definition: z3++.h:3304
Z3_ast Z3_API Z3_mk_set_difference(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Take the set difference between two sets.
expr z3::set_intersect ( expr const &  a,
expr const &  b 
)
inline

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

3338  {
3339  check_context(a, b);
3340  Z3_ast es[2] = { a, b };
3341  Z3_ast r = Z3_mk_set_intersect(a.ctx(), 2, es);
3342  a.check_error();
3343  return expr(a.ctx(), r);
3344  }
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:410
expr z3::set_member ( expr const &  s,
expr const &  e 
)
inline

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

3354  {
3355  MK_EXPR2(Z3_mk_set_member, s, e);
3356  }
#define MK_EXPR2(_fn, _arg1, _arg2)
Definition: z3++.h:3304
Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set)
Check for set membership.
void z3::set_param ( char const *  param,
char const *  value 
)
inline

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

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

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

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

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

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

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

3358  {
3359  MK_EXPR2(Z3_mk_set_subset, a, b);
3360  }
#define MK_EXPR2(_fn, _arg1, _arg2)
Definition: z3++.h:3304
Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Check for subsetness of sets.
expr z3::set_union ( expr const &  a,
expr const &  b 
)
inline

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

3330  {
3331  check_context(a, b);
3332  Z3_ast es[2] = { a, b };
3333  Z3_ast r = Z3_mk_set_union(a.ctx(), 2, es);
3334  a.check_error();
3335  return expr(a.ctx(), r);
3336  }
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:410
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 1807 of file z3++.h.

1807 { 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:1658
expr z3::shl ( expr const &  a,
expr const &  b 
)
inline

shift left operator for bitvectors

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

Referenced by shl().

1746 { 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:1658
expr z3::shl ( expr const &  a,
int  b 
)
inline

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

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

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

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

signed less than or equal to operator for bitvectors.

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

Referenced by sle().

1680 { return to_expr(a.ctx(), Z3_mk_bvsle(a.ctx(), a, b)); }
Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed 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:1658
expr z3::sle ( expr const &  a,
int  b 
)
inline

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

1681 { return sle(a, a.ctx().num_val(b, a.get_sort())); }
expr sle(int a, expr const &b)
Definition: z3++.h:1682
expr z3::sle ( int  a,
expr const &  b 
)
inline

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

1682 { return sle(b.ctx().num_val(a, b.get_sort()), b); }
expr sle(int a, expr const &b)
Definition: z3++.h:1682
expr z3::slt ( expr const &  a,
expr const &  b 
)
inline

signed less than operator for bitvectors.

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

Referenced by slt().

1686 { return to_expr(a.ctx(), Z3_mk_bvslt(a.ctx(), a, b)); }
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed 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:1658
expr z3::slt ( expr const &  a,
int  b 
)
inline

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

1687 { return slt(a, a.ctx().num_val(b, a.get_sort())); }
expr slt(int a, expr const &b)
Definition: z3++.h:1688
expr z3::slt ( int  a,
expr const &  b 
)
inline

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

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

signed modulus operator for bitvectors

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

Referenced by smod().

1732 { 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'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:1658
expr z3::smod ( expr const &  a,
int  b 
)
inline

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

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

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

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

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

1622  {
1623  check_context(a, rm);
1624  assert(a.is_fpa());
1625  Z3_ast r = Z3_mk_fpa_sqrt(a.ctx(), rm, a);
1626  a.check_error();
1627  return expr(a.ctx(), r);
1628  }
void check_context(object const &a, object const &b)
Definition: z3++.h:410
Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point square root.
expr z3::srem ( expr const &  a,
expr const &  b 
)
inline

signed remainder operator for bitvectors

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

Referenced by srem().

1725 { 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'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:1658
expr z3::srem ( expr const &  a,
int  b 
)
inline

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

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

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

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

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

3407  {
3408  MK_EXPR1(Z3_mk_re_star, re);
3409  }
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:3299
expr z3::store ( expr const &  a,
expr const &  i,
expr const &  v 
)
inline

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

Referenced by store().

3273  {
3274  check_context(a, i); check_context(a, v);
3275  Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
3276  a.check_error();
3277  return expr(a.ctx(), r);
3278  }
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:410
expr z3::store ( expr const &  a,
int  i,
expr const &  v 
)
inline

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

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

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

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

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

3282  {
3283  return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
3284  }
expr store(expr const &a, expr_vector const &i, expr const &v)
Definition: z3++.h:3285
expr z3::store ( expr const &  a,
expr_vector const &  i,
expr const &  v 
)
inline

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

3285  {
3286  check_context(a, i); check_context(a, v);
3287  array<Z3_ast> idxs(i);
3288  Z3_ast r = Z3_mk_store_n(a.ctx(), a, idxs.size(), idxs.ptr(), v);
3289  a.check_error();
3290  return expr(a.ctx(), r);
3291  }
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:410
expr z3::suffixof ( expr const &  a,
expr const &  b 
)
inline

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

3371  {
3372  check_context(a, b);
3373  Z3_ast r = Z3_mk_seq_suffix(a.ctx(), a, b);
3374  a.check_error();
3375  return expr(a.ctx(), r);
3376  }
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:410
expr z3::sum ( expr_vector const &  args)
inline

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

2048  {
2049  assert(args.size() > 0);
2050  context& ctx = args[0].ctx();
2051  array<Z3_ast> _args(args);
2052  Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
2053  ctx.check_error();
2054  return expr(ctx, r);
2055  }
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].
check_result z3::to_check_result ( Z3_lbool  l)
inline

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

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

141  {
142  if (l == Z3_L_TRUE) return sat;
143  else if (l == Z3_L_FALSE) return unsat;
144  return unknown;
145  }
Definition: z3++.h:130
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 1658 of file z3++.h.

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

1658  {
1659  c.check_error();
1660  assert(Z3_get_ast_kind(c, a) == Z3_APP_AST ||
1661  Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
1662  Z3_get_ast_kind(c, a) == Z3_VAR_AST ||
1664  return expr(c, a);
1665  }
Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a)
Return the kind of the given AST.
func_decl z3::to_func_decl ( context &  c,
Z3_func_decl  f 
)
inline

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

Referenced by linear_order(), partial_order(), piecewise_linear_order(), and tree_order().

1672  {
1673  c.check_error();
1674  return func_decl(c, f);
1675  }
expr z3::to_re ( expr const &  s)
inline

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

3395  {
3397  }
#define MK_EXPR1(_fn, _arg)
Definition: z3++.h:3299
Z3_ast Z3_API Z3_mk_seq_to_re(Z3_context c, Z3_ast seq)
Create a regular expression that accepts the sequence seq.
expr z3::to_real ( expr const &  a)
inline

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

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

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

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

1667  {
1668  c.check_error();
1669  return sort(c, s);
1670  }
func_decl z3::tree_order ( sort const &  a,
unsigned  index 
)
inline

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

1818  {
1819  return to_func_decl(a.ctx(), Z3_mk_tree_order(a.ctx(), a, index));
1820  }
func_decl to_func_decl(context &c, Z3_func_decl f)
Definition: z3++.h:1672
Z3_func_decl Z3_API Z3_mk_tree_order(Z3_context c, Z3_sort a, unsigned id)
create a tree ordering relation over signature a identified using index id.
tactic z3::try_for ( tactic const &  t,
unsigned  ms 
)
inline

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

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

unsigned division operator for bitvectors.

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

Referenced by udiv().

1718 { 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:1658
expr z3::udiv ( expr const &  a,
int  b 
)
inline

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

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

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

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

unsigned greater than or equal to operator for bitvectors.

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

Referenced by uge().

1706 { 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:1658
expr z3::uge ( expr const &  a,
int  b 
)
inline

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

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

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

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

unsigned greater than operator for bitvectors.

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

Referenced by ugt().

1712 { 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:1658
expr z3::ugt ( expr const &  a,
int  b 
)
inline

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

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

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

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

unsigned less than or equal to operator for bitvectors.

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

Referenced by ule().

1694 { 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:1658
expr z3::ule ( expr const &  a,
int  b 
)
inline

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

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

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

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

unsigned less than operator for bitvectors.

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

Referenced by ult().

1700 { 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:1658
expr z3::ult ( expr const &  a,
int  b 
)
inline

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

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

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

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

unsigned reminder operator for bitvectors

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

Referenced by urem().

1739 { 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:1658
expr z3::urem ( expr const &  a,
int  b 
)
inline

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

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

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

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

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

2892  {
2893  check_context(p, t);
2894  Z3_tactic r = Z3_tactic_when(t.ctx(), p, t);
2895  t.check_error();
2896  return tactic(t.ctx(), r);
2897  }
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:410
tactic z3::with ( tactic const &  t,
params const &  p 
)
inline

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

2652  {
2653  Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
2654  t.check_error();
2655  return tactic(t.ctx(), r);
2656  }
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.
expr z3::xnor ( expr const &  a,
expr const &  b 
)
inline

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

1575 { 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:410
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 1767 of file z3++.h.

1767 { 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:1658
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...