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

Z3 C++ namespace. More...

Data Structures

class  apply_result
 
class  array
 
class  ast
 
class  ast_vector_tpl
 
class  cast_ast
 
class  cast_ast< ast >
 
class  cast_ast< expr >
 
class  cast_ast< func_decl >
 
class  cast_ast< sort >
 
class  config
 Z3 global configuration object. More...
 
class  context
 A Context manages all other Z3 objects, global configuration options, etc. More...
 
class  exception
 Exception used to sign API usage errors. More...
 
class  expr
 A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort Boolean. Every expression has a sort. More...
 
class  fixedpoint
 
class  func_decl
 Function declaration (aka function definition). It is the signature of interpreted and uninterpreted functions in Z3. The basic building block in Z3 is the function application. More...
 
class  func_entry
 
class  func_interp
 
class  goal
 
class  model
 
class  object
 
class  optimize
 
class  param_descrs
 
class  params
 
class  probe
 
class  solver
 
class  sort
 A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort. More...
 
class  stats
 
class  symbol
 
class  tactic
 

Typedefs

typedef ast_vector_tpl< astast_vector
 
typedef ast_vector_tpl< exprexpr_vector
 
typedef ast_vector_tpl< sortsort_vector
 
typedef ast_vector_tpl< func_declfunc_decl_vector
 

Enumerations

enum  check_result { unsat, sat, unknown }
 
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

◆ ast_vector

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

◆ expr_vector

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

◆ func_decl_vector

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

◆ sort_vector

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

Enumeration Type Documentation

◆ check_result

Enumerator
unsat 
sat 
unknown 

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

132  {
133  unsat, sat, unknown
134  };

◆ rounding_mode

Enumerator
RNA 
RNE 
RTP 
RTN 
RTZ 

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

136  {
137  RNA,
138  RNE,
139  RTP,
140  RTN,
141  RTZ
142  };

Function Documentation

◆ abs()

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

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

1722  {
1723  Z3_ast r;
1724  if (a.is_int()) {
1725  expr zero = a.ctx().int_val(0);
1726  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
1727  }
1728  else if (a.is_real()) {
1729  expr zero = a.ctx().real_val(0);
1730  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
1731  }
1732  else {
1733  r = Z3_mk_fpa_abs(a.ctx(), a);
1734  }
1735  a.check_error();
1736  return expr(a.ctx(), r);
1737  }

◆ as_array()

expr z3::as_array ( func_decl f)
inline

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

3350  {
3351  Z3_ast r = Z3_mk_as_array(f.ctx(), f);
3352  f.check_error();
3353  return expr(f.ctx(), r);
3354  }

◆ ashr() [1/3]

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

arithmetic shift right operator for bitvectors

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

1876 { return to_expr(a.ctx(), Z3_mk_bvashr(a.ctx(), a, b)); }

Referenced by ashr().

◆ ashr() [2/3]

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

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

1877 { return ashr(a, a.ctx().num_val(b, a.get_sort())); }

◆ ashr() [3/3]

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

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

1878 { return ashr(b.ctx().num_val(a, b.get_sort()), b); }

◆ atleast()

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

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

2087  {
2088  assert(es.size() > 0);
2089  context& ctx = es[0].ctx();
2090  array<Z3_ast> _es(es);
2091  Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
2092  ctx.check_error();
2093  return expr(ctx, r);
2094  }

◆ atmost()

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

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

2079  {
2080  assert(es.size() > 0);
2081  context& ctx = es[0].ctx();
2082  array<Z3_ast> _es(es);
2083  Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
2084  ctx.check_error();
2085  return expr(ctx, r);
2086  }

◆ bv2int()

expr z3::bv2int ( expr const &  a,
bool  is_signed 
)
inline

bit-vector and integer conversions.

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

1888 { Z3_ast r = Z3_mk_bv2int(a.ctx(), a, is_signed); a.check_error(); return expr(a.ctx(), r); }

◆ bvadd_no_overflow()

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

bit-vector overflow/underflow checks

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

1894  {
1895  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);
1896  }

◆ bvadd_no_underflow()

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

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

1897  {
1898  check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1899  }

◆ bvmul_no_overflow()

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

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

1912  {
1913  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);
1914  }

◆ bvmul_no_underflow()

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

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

1915  {
1916  check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1917  }

◆ bvneg_no_overflow()

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

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

1909  {
1910  Z3_ast r = Z3_mk_bvneg_no_overflow(a.ctx(), a); a.check_error(); return expr(a.ctx(), r);
1911  }

◆ bvsdiv_no_overflow()

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

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

1906  {
1907  check_context(a, b); Z3_ast r = Z3_mk_bvsdiv_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1908  }

◆ bvsub_no_overflow()

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

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

1900  {
1901  check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
1902  }

◆ bvsub_no_underflow()

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

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

1903  {
1904  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);
1905  }

◆ check_context()

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

◆ concat() [1/2]

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

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

2113  {
2114  check_context(a, b);
2115  Z3_ast r;
2116  if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
2117  Z3_ast _args[2] = { a, b };
2118  r = Z3_mk_seq_concat(a.ctx(), 2, _args);
2119  }
2120  else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
2121  Z3_ast _args[2] = { a, b };
2122  r = Z3_mk_re_concat(a.ctx(), 2, _args);
2123  }
2124  else {
2125  r = Z3_mk_concat(a.ctx(), a, b);
2126  }
2127  a.ctx().check_error();
2128  return expr(a.ctx(), r);
2129  }

Referenced by operator+().

◆ concat() [2/2]

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

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

2131  {
2132  Z3_ast r;
2133  assert(args.size() > 0);
2134  if (args.size() == 1) {
2135  return args[0];
2136  }
2137  context& ctx = args[0].ctx();
2138  array<Z3_ast> _args(args);
2139  if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
2140  r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
2141  }
2142  else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
2143  r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
2144  }
2145  else {
2146  r = _args[args.size()-1];
2147  for (unsigned i = args.size()-1; i > 0; ) {
2148  --i;
2149  r = Z3_mk_concat(ctx, _args[i], r);
2150  ctx.check_error();
2151  }
2152  }
2153  ctx.check_error();
2154  return expr(ctx, r);
2155  }

◆ cond()

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

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

2955  {
2956  check_context(p, t1); check_context(p, t2);
2957  Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2);
2958  t1.check_error();
2959  return tactic(t1.ctx(), r);
2960  }

◆ const_array()

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

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

3367  {
3368  MK_EXPR2(Z3_mk_const_array, d, v);
3369  }

◆ distinct()

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

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

2104  {
2105  assert(args.size() > 0);
2106  context& ctx = args[0].ctx();
2107  array<Z3_ast> _args(args);
2108  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
2109  ctx.check_error();
2110  return expr(ctx, r);
2111  }

◆ empty()

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

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

3423  {
3424  Z3_ast r = Z3_mk_seq_empty(s.ctx(), s);
3425  s.check_error();
3426  return expr(s.ctx(), r);
3427  }

◆ empty_set()

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

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

3371  {
3373  }

◆ eq()

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

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

513 { return Z3_is_eq_ast(a.ctx(), a, b); }

◆ exists() [1/5]

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

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

2006  {
2007  check_context(x, b);
2008  Z3_app vars[] = {(Z3_app) x};
2009  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2010  }

◆ exists() [2/5]

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

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

2011  {
2012  check_context(x1, b); check_context(x2, b);
2013  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2014  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2015  }

◆ exists() [3/5]

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

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

2016  {
2017  check_context(x1, b); check_context(x2, b); check_context(x3, b);
2018  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2019  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2020  }

◆ exists() [4/5]

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

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

2021  {
2022  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2023  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2024  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2025  }

◆ exists() [5/5]

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

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

2026  {
2027  array<Z3_app> vars(xs);
2028  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);
2029  }

◆ fail_if()

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

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

2944  {
2945  Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
2946  p.check_error();
2947  return tactic(p.ctx(), r);
2948  }

◆ fma()

expr z3::fma ( expr const &  a,
expr const &  b,
expr const &  c,
expr const &  rm 
)
inline

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

1747  {
1748  check_context(a, b); check_context(a, c); check_context(a, rm);
1749  assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
1750  Z3_ast r = Z3_mk_fpa_fma(a.ctx(), rm, a, b, c);
1751  a.check_error();
1752  return expr(a.ctx(), r);
1753  }

◆ forall() [1/5]

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

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

1982  {
1983  check_context(x, b);
1984  Z3_app vars[] = {(Z3_app) x};
1985  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1986  }

◆ forall() [2/5]

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

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

1987  {
1988  check_context(x1, b); check_context(x2, b);
1989  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
1990  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1991  }

◆ forall() [3/5]

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

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

1992  {
1993  check_context(x1, b); check_context(x2, b); check_context(x3, b);
1994  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
1995  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
1996  }

◆ forall() [4/5]

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

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

1997  {
1998  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
1999  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2000  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2001  }

◆ forall() [5/5]

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

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

2002  {
2003  array<Z3_app> vars(xs);
2004  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);
2005  }

◆ full_set()

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

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

3375  {
3377  }

◆ function() [1/9]

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

3290  {
3291  return range.ctx().function(name, d1, d2, d3, d4, d5, range);
3292  }

◆ function() [2/9]

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

3287  {
3288  return range.ctx().function(name, d1, d2, d3, d4, range);
3289  }

◆ function() [3/9]

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

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

3284  {
3285  return range.ctx().function(name, d1, d2, d3, range);
3286  }

◆ function() [4/9]

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

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

3281  {
3282  return range.ctx().function(name, d1, d2, range);
3283  }

◆ function() [5/9]

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

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

3278  {
3279  return range.ctx().function(name, domain, range);
3280  }

◆ function() [6/9]

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

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

3293  {
3294  return range.ctx().function(name, domain, range);
3295  }

◆ function() [7/9]

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

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

3275  {
3276  return range.ctx().function(name, arity, domain, range);
3277  }

◆ function() [8/9]

func_decl z3::function ( std::string const &  name,
sort_vector const &  domain,
sort const &  range 
)
inline

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

3296  {
3297  return range.ctx().function(name.c_str(), domain, range);
3298  }

◆ function() [9/9]

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

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

3272  {
3273  return range.ctx().function(name, arity, domain, range);
3274  }

◆ implies() [1/3]

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

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

1382 { return implies(b.ctx().bool_val(a), b); }

◆ implies() [2/3]

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

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

1381 { return implies(a, a.ctx().bool_val(b)); }

◆ implies() [3/3]

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

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

1377  {
1378  assert(a.is_bool() && b.is_bool());
1379  _Z3_MK_BIN_(a, b, Z3_mk_implies);
1380  }

Referenced by implies().

◆ in_re()

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

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

3455  {
3456  MK_EXPR2(Z3_mk_seq_in_re, s, re);
3457  }

◆ indexof()

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

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

3440  {
3441  check_context(s, substr); check_context(s, offset);
3442  Z3_ast r = Z3_mk_seq_index(s.ctx(), s, substr, offset);
3443  s.check_error();
3444  return expr(s.ctx(), r);
3445  }

◆ int2bv()

expr z3::int2bv ( unsigned  n,
expr const &  a 
)
inline

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

1889 { Z3_ast r = Z3_mk_int2bv(a.ctx(), n, a); a.check_error(); return expr(a.ctx(), r); }

◆ is_int()

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

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

1425 { _Z3_MK_UN_(e, Z3_mk_is_int); }

◆ ite()

expr z3::ite ( expr const &  c,
expr const &  t,
expr const &  e 
)
inline

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

Precondition
c.is_bool()

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

1761  {
1762  check_context(c, t); check_context(c, e);
1763  assert(c.is_bool());
1764  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
1765  c.check_error();
1766  return expr(c.ctx(), r);
1767  }

◆ lambda() [1/5]

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

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

2030  {
2031  check_context(x, b);
2032  Z3_app vars[] = {(Z3_app) x};
2033  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 1, vars, b); b.check_error(); return expr(b.ctx(), r);
2034  }

◆ lambda() [2/5]

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

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

2035  {
2036  check_context(x1, b); check_context(x2, b);
2037  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2038  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 2, vars, b); b.check_error(); return expr(b.ctx(), r);
2039  }

◆ lambda() [3/5]

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

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

2040  {
2041  check_context(x1, b); check_context(x2, b); check_context(x3, b);
2042  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2043  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 3, vars, b); b.check_error(); return expr(b.ctx(), r);
2044  }

◆ lambda() [4/5]

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

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

2045  {
2046  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2047  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2048  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 4, vars, b); b.check_error(); return expr(b.ctx(), r);
2049  }

◆ lambda() [5/5]

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

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

2050  {
2051  array<Z3_app> vars(xs);
2052  Z3_ast r = Z3_mk_lambda_const(b.ctx(), vars.size(), vars.ptr(), b); b.check_error(); return expr(b.ctx(), r);
2053  }

◆ last_indexof()

expr z3::last_indexof ( expr const &  s,
expr const &  substr 
)
inline

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

3446  {
3447  check_context(s, substr);
3448  Z3_ast r = Z3_mk_seq_last_index(s.ctx(), s, substr);
3449  s.check_error();
3450  return expr(s.ctx(), r);
3451  }

◆ linear_order()

func_decl z3::linear_order ( sort const &  a,
unsigned  index 
)
inline

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

1925  {
1926  return to_func_decl(a.ctx(), Z3_mk_linear_order(a.ctx(), a, index));
1927  }

◆ lshr() [1/3]

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

logic shift right operator for bitvectors

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

1869 { return to_expr(a.ctx(), Z3_mk_bvlshr(a.ctx(), a, b)); }

Referenced by lshr().

◆ lshr() [2/3]

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

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

1870 { return lshr(a, a.ctx().num_val(b, a.get_sort())); }

◆ lshr() [3/3]

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

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

1871 { return lshr(b.ctx().num_val(a, b.get_sort()), b); }

◆ max()

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

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

1707  {
1708  check_context(a, b);
1709  Z3_ast r;
1710  if (a.is_arith()) {
1711  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), a, b);
1712  }
1713  else if (a.is_bv()) {
1714  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), a, b);
1715  }
1716  else {
1717  assert(a.is_fpa());
1718  r = Z3_mk_fpa_max(a.ctx(), a, b);
1719  }
1720  return expr(a.ctx(), r);
1721  }

Referenced by repeat(), and Context::repeat().

◆ min()

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

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

1692  {
1693  check_context(a, b);
1694  Z3_ast r;
1695  if (a.is_arith()) {
1696  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), b, a);
1697  }
1698  else if (a.is_bv()) {
1699  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), b, a);
1700  }
1701  else {
1702  assert(a.is_fpa());
1703  r = Z3_mk_fpa_min(a.ctx(), a, b);
1704  }
1705  return expr(a.ctx(), r);
1706  }

◆ mk_and()

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

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

2163  {
2164  array<Z3_ast> _args(args);
2165  Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2166  args.check_error();
2167  return expr(args.ctx(), r);
2168  }

◆ mk_or()

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

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

2157  {
2158  array<Z3_ast> _args(args);
2159  Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2160  args.check_error();
2161  return expr(args.ctx(), r);
2162  }

◆ mod() [1/3]

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

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

1389  {
1390  if (a.is_bv()) {
1391  _Z3_MK_BIN_(a, b, Z3_mk_bvsmod);
1392  }
1393  else {
1394  _Z3_MK_BIN_(a, b, Z3_mk_mod);
1395  }
1396  }

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

◆ mod() [2/3]

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

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

1397 { return mod(a, a.ctx().num_val(b, a.get_sort())); }

◆ mod() [3/3]

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

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

1398 { return mod(b.ctx().num_val(a, b.get_sort()), b); }

◆ nand()

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

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

1689 { check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); return expr(a.ctx(), r); }

◆ nor()

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

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

1690 { check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); return expr(a.ctx(), r); }

◆ operator!() [1/2]

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

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

1423 { assert(a.is_bool()); _Z3_MK_UN_(a, Z3_mk_not); }

◆ operator!() [2/2]

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

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

2798  {
2799  Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
2800  }

◆ operator!=() [1/3]

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

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

1463  {
1464  check_context(a, b);
1465  Z3_ast args[2] = { a, b };
1466  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1467  a.check_error();
1468  return expr(a.ctx(), r);
1469  }

◆ operator!=() [2/3]

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

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

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

◆ operator!=() [3/3]

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

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

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

◆ operator%() [1/3]

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

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

1400 { return mod(a, b); }

◆ operator%() [2/3]

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

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

1401 { return mod(a, b); }

◆ operator%() [3/3]

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

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

1402 { return mod(a, b); }

◆ operator&() [1/4]

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

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

1677 { check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); return expr(a.ctx(), r); }

◆ operator&() [2/4]

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

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

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

◆ operator&() [3/4]

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

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

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

◆ operator&() [4/4]

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

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

2679  {
2680  check_context(t1, t2);
2681  Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
2682  t1.check_error();
2683  return tactic(t1.ctx(), r);
2684  }

◆ operator&&() [1/4]

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

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

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

◆ operator&&() [2/4]

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

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

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

◆ operator&&() [3/4]

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

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

1429  {
1430  check_context(a, b);
1431  assert(a.is_bool() && b.is_bool());
1432  Z3_ast args[2] = { a, b };
1433  Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
1434  a.check_error();
1435  return expr(a.ctx(), r);
1436  }

◆ operator&&() [4/4]

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

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

2792  {
2793  check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2794  }

◆ operator*() [1/3]

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

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

1503  {
1504  check_context(a, b);
1505  Z3_ast r = 0;
1506  if (a.is_arith() && b.is_arith()) {
1507  Z3_ast args[2] = { a, b };
1508  r = Z3_mk_mul(a.ctx(), 2, args);
1509  }
1510  else if (a.is_bv() && b.is_bv()) {
1511  r = Z3_mk_bvmul(a.ctx(), a, b);
1512  }
1513  else if (a.is_fpa() && b.is_fpa()) {
1514  r = Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1515  }
1516  else {
1517  // operator is not supported by given arguments.
1518  assert(false);
1519  }
1520  a.check_error();
1521  return expr(a.ctx(), r);
1522  }

◆ operator*() [2/3]

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

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

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

◆ operator*() [3/3]

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

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

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

◆ operator+() [1/3]

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

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

1473  {
1474  check_context(a, b);
1475  Z3_ast r = 0;
1476  if (a.is_arith() && b.is_arith()) {
1477  Z3_ast args[2] = { a, b };
1478  r = Z3_mk_add(a.ctx(), 2, args);
1479  }
1480  else if (a.is_bv() && b.is_bv()) {
1481  r = Z3_mk_bvadd(a.ctx(), a, b);
1482  }
1483  else if (a.is_seq() && b.is_seq()) {
1484  return concat(a, b);
1485  }
1486  else if (a.is_re() && b.is_re()) {
1487  Z3_ast _args[2] = { a, b };
1488  r = Z3_mk_re_union(a.ctx(), 2, _args);
1489  }
1490  else if (a.is_fpa() && b.is_fpa()) {
1491  r = Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1492  }
1493  else {
1494  // operator is not supported by given arguments.
1495  assert(false);
1496  }
1497  a.check_error();
1498  return expr(a.ctx(), r);
1499  }

◆ operator+() [2/3]

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

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

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

◆ operator+() [3/3]

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

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

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

◆ operator-() [1/4]

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

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

1566  {
1567  Z3_ast r = 0;
1568  if (a.is_arith()) {
1569  r = Z3_mk_unary_minus(a.ctx(), a);
1570  }
1571  else if (a.is_bv()) {
1572  r = Z3_mk_bvneg(a.ctx(), a);
1573  }
1574  else if (a.is_fpa()) {
1575  r = Z3_mk_fpa_neg(a.ctx(), a);
1576  }
1577  else {
1578  // operator is not supported by given arguments.
1579  assert(false);
1580  }
1581  a.check_error();
1582  return expr(a.ctx(), r);
1583  }

◆ operator-() [2/4]

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

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

1585  {
1586  check_context(a, b);
1587  Z3_ast r = 0;
1588  if (a.is_arith() && b.is_arith()) {
1589  Z3_ast args[2] = { a, b };
1590  r = Z3_mk_sub(a.ctx(), 2, args);
1591  }
1592  else if (a.is_bv() && b.is_bv()) {
1593  r = Z3_mk_bvsub(a.ctx(), a, b);
1594  }
1595  else if (a.is_fpa() && b.is_fpa()) {
1596  r = Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1597  }
1598  else {
1599  // operator is not supported by given arguments.
1600  assert(false);
1601  }
1602  a.check_error();
1603  return expr(a.ctx(), r);
1604  }

◆ operator-() [3/4]

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

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

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

◆ operator-() [4/4]

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

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

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

◆ operator/() [1/3]

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

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

1544  {
1545  check_context(a, b);
1546  Z3_ast r = 0;
1547  if (a.is_arith() && b.is_arith()) {
1548  r = Z3_mk_div(a.ctx(), a, b);
1549  }
1550  else if (a.is_bv() && b.is_bv()) {
1551  r = Z3_mk_bvsdiv(a.ctx(), a, b);
1552  }
1553  else if (a.is_fpa() && b.is_fpa()) {
1554  r = Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1555  }
1556  else {
1557  // operator is not supported by given arguments.
1558  assert(false);
1559  }
1560  a.check_error();
1561  return expr(a.ctx(), r);
1562  }

◆ operator/() [2/3]

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

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

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

◆ operator/() [3/3]

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

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

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

◆ operator<() [1/6]

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

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

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

◆ operator<() [2/6]

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

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

1633  {
1634  check_context(a, b);
1635  Z3_ast r = 0;
1636  if (a.is_arith() && b.is_arith()) {
1637  r = Z3_mk_lt(a.ctx(), a, b);
1638  }
1639  else if (a.is_bv() && b.is_bv()) {
1640  r = Z3_mk_bvslt(a.ctx(), a, b);
1641  }
1642  else if (a.is_fpa() && b.is_fpa()) {
1643  r = Z3_mk_fpa_lt(a.ctx(), a, b);
1644  }
1645  else {
1646  // operator is not supported by given arguments.
1647  assert(false);
1648  }
1649  a.check_error();
1650  return expr(a.ctx(), r);
1651  }

◆ operator<() [3/6]

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

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

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

◆ operator<() [4/6]

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

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

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

◆ operator<() [5/6]

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

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

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

◆ operator<() [6/6]

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

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

2777  {
2778  check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2779  }

◆ operator<<() [1/13]

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

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

2637 { out << Z3_apply_result_to_string(r.ctx(), r); return out; }

◆ operator<<() [2/13]

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

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

509  {
510  out << Z3_ast_to_string(n.ctx(), n.m_ast); return out;
511  }

◆ operator<<() [3/13]

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

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

2335  {
2336  if (r == unsat) out << "unsat";
2337  else if (r == sat) out << "sat";
2338  else out << "unknown";
2339  return out;
2340  }

◆ operator<<() [4/13]

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

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

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

◆ operator<<() [5/13]

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

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

2942 { return out << Z3_fixedpoint_to_string(f.ctx(), f, 0, 0); }

◆ operator<<() [6/13]

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

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

2613 { out << Z3_goal_to_string(g.ctx(), g); return out; }

◆ operator<<() [7/13]

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

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

2303 { out << Z3_model_to_string(m.ctx(), m); return out; }

◆ operator<<() [8/13]

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

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

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

◆ operator<<() [9/13]

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

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

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

◆ operator<<() [10/13]

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

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

483  {
484  out << Z3_params_to_string(p.ctx(), p); return out;
485  }

◆ operator<<() [11/13]

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

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

2554 { out << Z3_solver_to_string(s.ctx(), s); return out; }

◆ operator<<() [12/13]

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

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

2332 { out << Z3_stats_to_string(s.ctx(), s); return out; }

◆ operator<<() [13/13]

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

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

428  {
429  if (s.kind() == Z3_INT_SYMBOL)
430  out << "k!" << s.to_int();
431  else
432  out << s.str();
433  return out;
434  }

◆ operator<=() [1/6]

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

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

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

◆ operator<=() [2/6]

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

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

1608  {
1609  check_context(a, b);
1610  Z3_ast r = 0;
1611  if (a.is_arith() && b.is_arith()) {
1612  r = Z3_mk_le(a.ctx(), a, b);
1613  }
1614  else if (a.is_bv() && b.is_bv()) {
1615  r = Z3_mk_bvsle(a.ctx(), a, b);
1616  }
1617  else if (a.is_fpa() && b.is_fpa()) {
1618  r = Z3_mk_fpa_leq(a.ctx(), a, b);
1619  }
1620  else {
1621  // operator is not supported by given arguments.
1622  assert(false);
1623  }
1624  a.check_error();
1625  return expr(a.ctx(), r);
1626  }

◆ operator<=() [3/6]

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

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

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

◆ operator<=() [4/6]

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

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

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

◆ operator<=() [5/6]

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

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

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

◆ operator<=() [6/6]

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

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

2767  {
2768  check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2769  }

◆ operator==() [1/6]

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

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

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

◆ operator==() [2/6]

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

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

1454  {
1455  check_context(a, b);
1456  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1457  a.check_error();
1458  return expr(a.ctx(), r);
1459  }

◆ operator==() [3/6]

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

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

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

◆ operator==() [4/6]

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

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

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

◆ operator==() [5/6]

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

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

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

◆ operator==() [6/6]

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

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

2787  {
2788  check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2789  }

◆ operator>() [1/6]

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

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

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

◆ operator>() [2/6]

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

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

1655  {
1656  check_context(a, b);
1657  Z3_ast r = 0;
1658  if (a.is_arith() && b.is_arith()) {
1659  r = Z3_mk_gt(a.ctx(), a, b);
1660  }
1661  else if (a.is_bv() && b.is_bv()) {
1662  r = Z3_mk_bvsgt(a.ctx(), a, b);
1663  }
1664  else if (a.is_fpa() && b.is_fpa()) {
1665  r = Z3_mk_fpa_gt(a.ctx(), a, b);
1666  }
1667  else {
1668  // operator is not supported by given arguments.
1669  assert(false);
1670  }
1671  a.check_error();
1672  return expr(a.ctx(), r);
1673  }

◆ operator>() [3/6]

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

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

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

◆ operator>() [4/6]

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

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

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

◆ operator>() [5/6]

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

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

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

◆ operator>() [6/6]

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

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

2782  {
2783  check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2784  }

◆ operator>=() [1/6]

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

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

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

◆ operator>=() [2/6]

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

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

1527  {
1528  check_context(a, b);
1529  Z3_ast r = 0;
1530  if (a.is_arith() && b.is_arith()) {
1531  r = Z3_mk_ge(a.ctx(), a, b);
1532  }
1533  else if (a.is_bv() && b.is_bv()) {
1534  r = Z3_mk_bvsge(a.ctx(), a, b);
1535  }
1536  else {
1537  // operator is not supported by given arguments.
1538  assert(false);
1539  }
1540  a.check_error();
1541  return expr(a.ctx(), r);
1542  }

◆ operator>=() [3/6]

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

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

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

◆ operator>=() [4/6]

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

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

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

◆ operator>=() [5/6]

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

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

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

◆ operator>=() [6/6]

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

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

2772  {
2773  check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2774  }

◆ operator^() [1/3]

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

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

1681 { check_context(a, b); Z3_ast r = Z3_mk_bvxor(a.ctx(), a, b); return expr(a.ctx(), r); }

◆ operator^() [2/3]

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

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

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

◆ operator^() [3/3]

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

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

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

◆ operator|() [1/4]

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

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

1685 { check_context(a, b); Z3_ast r = Z3_mk_bvor(a.ctx(), a, b); return expr(a.ctx(), r); }

◆ operator|() [2/4]

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

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

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

◆ operator|() [3/4]

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

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

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

◆ operator|() [4/4]

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

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

2686  {
2687  check_context(t1, t2);
2688  Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
2689  t1.check_error();
2690  return tactic(t1.ctx(), r);
2691  }

◆ operator||() [1/4]

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

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

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

◆ operator||() [2/4]

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

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

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

◆ operator||() [3/4]

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

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

1441  {
1442  check_context(a, b);
1443  assert(a.is_bool() && b.is_bool());
1444  Z3_ast args[2] = { a, b };
1445  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1446  a.check_error();
1447  return expr(a.ctx(), r);
1448  }

◆ operator||() [4/4]

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

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

2795  {
2796  check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2797  }

◆ operator~()

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

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

1745 { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); }

◆ option()

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

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

3461  {
3463  }

◆ par_and_then()

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

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

2718  {
2719  check_context(t1, t2);
2720  Z3_tactic r = Z3_tactic_par_and_then(t1.ctx(), t1, t2);
2721  t1.check_error();
2722  return tactic(t1.ctx(), r);
2723  }

◆ par_or()

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

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

2709  {
2710  if (n == 0) {
2711  Z3_THROW(exception("a non-zero number of tactics need to be passed to par_or"));
2712  }
2713  array<Z3_tactic> buffer(n);
2714  for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];
2715  return tactic(tactics[0].ctx(), Z3_tactic_par_or(tactics[0].ctx(), n, buffer.ptr()));
2716  }

◆ partial_order()

func_decl z3::partial_order ( sort const &  a,
unsigned  index 
)
inline

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

1928  {
1929  return to_func_decl(a.ctx(), Z3_mk_partial_order(a.ctx(), a, index));
1930  }

◆ pbeq()

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

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

2071  {
2072  assert(es.size() > 0);
2073  context& ctx = es[0].ctx();
2074  array<Z3_ast> _es(es);
2075  Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
2076  ctx.check_error();
2077  return expr(ctx, r);
2078  }

◆ pbge()

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

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

2063  {
2064  assert(es.size() > 0);
2065  context& ctx = es[0].ctx();
2066  array<Z3_ast> _es(es);
2067  Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
2068  ctx.check_error();
2069  return expr(ctx, r);
2070  }

◆ pble()

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

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

2055  {
2056  assert(es.size() > 0);
2057  context& ctx = es[0].ctx();
2058  array<Z3_ast> _es(es);
2059  Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
2060  ctx.check_error();
2061  return expr(ctx, r);
2062  }

◆ piecewise_linear_order()

func_decl z3::piecewise_linear_order ( sort const &  a,
unsigned  index 
)
inline

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

1931  {
1932  return to_func_decl(a.ctx(), Z3_mk_piecewise_linear_order(a.ctx(), a, index));
1933  }

◆ plus()

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

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

3458  {
3459  MK_EXPR1(Z3_mk_re_plus, re);
3460  }

◆ prefixof()

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

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

3434  {
3435  check_context(a, b);
3436  Z3_ast r = Z3_mk_seq_prefix(a.ctx(), a, b);
3437  a.check_error();
3438  return expr(a.ctx(), r);
3439  }

◆ pw() [1/3]

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

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

1385 { _Z3_MK_BIN_(a, b, Z3_mk_power); }

Referenced by pw().

◆ pw() [2/3]

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

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

1386 { return pw(a, a.ctx().num_val(b, a.get_sort())); }

◆ pw() [3/3]

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

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

1387 { return pw(b.ctx().num_val(a, b.get_sort()), b); }

◆ range()

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

◆ re_complement()

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

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

3485  {
3487  }

◆ re_empty()

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

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

3467  {
3468  Z3_ast r = Z3_mk_re_empty(s.ctx(), s);
3469  s.check_error();
3470  return expr(s.ctx(), r);
3471  }

◆ re_full()

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

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

3472  {
3473  Z3_ast r = Z3_mk_re_full(s.ctx(), s);
3474  s.check_error();
3475  return expr(s.ctx(), r);
3476  }

◆ re_intersect()

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

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

3477  {
3478  assert(args.size() > 0);
3479  context& ctx = args[0].ctx();
3480  array<Z3_ast> _args(args);
3481  Z3_ast r = Z3_mk_re_intersect(ctx, _args.size(), _args.ptr());
3482  ctx.check_error();
3483  return expr(ctx, r);
3484  }

◆ recfun() [1/4]

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

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

3309  {
3310  return range.ctx().recfun(name, d1, d2, range);
3311  }

◆ recfun() [2/4]

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

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

3306  {
3307  return range.ctx().recfun(name, d1, range);
3308  }

◆ recfun() [3/4]

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

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

3303  {
3304  return range.ctx().recfun(name, arity, domain, range);
3305  }

◆ recfun() [4/4]

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

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

3300  {
3301  return range.ctx().recfun(name, arity, domain, range);
3302  }

◆ rem() [1/3]

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

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

1405  {
1406  if (a.is_fpa() && b.is_fpa()) {
1407  _Z3_MK_BIN_(a, b, Z3_mk_fpa_rem);
1408  } else {
1409  _Z3_MK_BIN_(a, b, Z3_mk_rem);
1410  }
1411  }

Referenced by rem().

◆ rem() [2/3]

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

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

1412 { return rem(a, a.ctx().num_val(b, a.get_sort())); }

◆ rem() [3/3]

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

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

1413 { return rem(b.ctx().num_val(a, b.get_sort()), b); }

◆ repeat()

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

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

2693  {
2694  Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
2695  t.check_error();
2696  return tactic(t.ctx(), r);
2697  }

◆ reset_params()

void z3::reset_params ( )
inline

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

◆ select() [1/3]

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

forward declarations

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

3313  {
3314  check_context(a, i);
3315  Z3_ast r = Z3_mk_select(a.ctx(), a, i);
3316  a.check_error();
3317  return expr(a.ctx(), r);
3318  }

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

◆ select() [2/3]

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

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

3322  {
3323  check_context(a, i);
3324  array<Z3_ast> idxs(i);
3325  Z3_ast r = Z3_mk_select_n(a.ctx(), a, idxs.size(), idxs.ptr());
3326  a.check_error();
3327  return expr(a.ctx(), r);
3328  }

◆ select() [3/3]

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

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

3319  {
3320  return select(a, a.ctx().num_val(i, a.get_sort().array_domain()));
3321  }

◆ set_add()

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

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

3379  {
3380  MK_EXPR2(Z3_mk_set_add, s, e);
3381  }

◆ set_complement()

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

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

3407  {
3409  }

◆ set_del()

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

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

3383  {
3384  MK_EXPR2(Z3_mk_set_del, s, e);
3385  }

◆ set_difference()

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

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

3403  {
3405  }

◆ set_intersect()

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

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

3395  {
3396  check_context(a, b);
3397  Z3_ast es[2] = { a, b };
3398  Z3_ast r = Z3_mk_set_intersect(a.ctx(), 2, es);
3399  a.check_error();
3400  return expr(a.ctx(), r);
3401  }

◆ set_member()

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

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

3411  {
3412  MK_EXPR2(Z3_mk_set_member, s, e);
3413  }

◆ set_param() [1/3]

void z3::set_param ( char const *  param,
bool  value 
)
inline

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

77 { Z3_global_param_set(param, value ? "true" : "false"); }

◆ set_param() [2/3]

void z3::set_param ( char const *  param,
char const *  value 
)
inline

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

76 { Z3_global_param_set(param, value); }

◆ set_param() [3/3]

void z3::set_param ( char const *  param,
int  value 
)
inline

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

78 { std::ostringstream oss; oss << value; Z3_global_param_set(param, oss.str().c_str()); }

◆ set_subset()

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

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

3415  {
3416  MK_EXPR2(Z3_mk_set_subset, a, b);
3417  }

◆ set_union()

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

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

3387  {
3388  check_context(a, b);
3389  Z3_ast es[2] = { a, b };
3390  Z3_ast r = Z3_mk_set_union(a.ctx(), 2, es);
3391  a.check_error();
3392  return expr(a.ctx(), r);
3393  }

◆ sext()

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

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

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

1923 { return to_expr(a.ctx(), Z3_mk_sign_ext(a.ctx(), i, a)); }

◆ shl() [1/3]

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

shift left operator for bitvectors

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

1862 { return to_expr(a.ctx(), Z3_mk_bvshl(a.ctx(), a, b)); }

Referenced by shl().

◆ shl() [2/3]

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

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

1863 { return shl(a, a.ctx().num_val(b, a.get_sort())); }

◆ shl() [3/3]

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

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

1864 { return shl(b.ctx().num_val(a, b.get_sort()), b); }

◆ sle() [1/3]

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

signed less than or equal to operator for bitvectors.

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

1796 { return to_expr(a.ctx(), Z3_mk_bvsle(a.ctx(), a, b)); }

Referenced by sle().

◆ sle() [2/3]

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

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

1797 { return sle(a, a.ctx().num_val(b, a.get_sort())); }

◆ sle() [3/3]

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

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

1798 { return sle(b.ctx().num_val(a, b.get_sort()), b); }

◆ slt() [1/3]

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

signed less than operator for bitvectors.

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

1802 { return to_expr(a.ctx(), Z3_mk_bvslt(a.ctx(), a, b)); }

Referenced by slt().

◆ slt() [2/3]

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

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

1803 { return slt(a, a.ctx().num_val(b, a.get_sort())); }

◆ slt() [3/3]

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

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

1804 { return slt(b.ctx().num_val(a, b.get_sort()), b); }

◆ smod() [1/3]

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

signed modulus operator for bitvectors

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

1848 { return to_expr(a.ctx(), Z3_mk_bvsmod(a.ctx(), a, b)); }

Referenced by smod().

◆ smod() [2/3]

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

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

1849 { return smod(a, a.ctx().num_val(b, a.get_sort())); }

◆ smod() [3/3]

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

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

1850 { return smod(b.ctx().num_val(a, b.get_sort()), b); }

◆ sqrt()

expr z3::sqrt ( expr const &  a,
expr const &  rm 
)
inline

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

1738  {
1739  check_context(a, rm);
1740  assert(a.is_fpa());
1741  Z3_ast r = Z3_mk_fpa_sqrt(a.ctx(), rm, a);
1742  a.check_error();
1743  return expr(a.ctx(), r);
1744  }

◆ srem() [1/3]

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

signed remainder operator for bitvectors

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

1841 { return to_expr(a.ctx(), Z3_mk_bvsrem(a.ctx(), a, b)); }

Referenced by srem().

◆ srem() [2/3]

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

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

1842 { return srem(a, a.ctx().num_val(b, a.get_sort())); }

◆ srem() [3/3]

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

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

1843 { return srem(b.ctx().num_val(a, b.get_sort()), b); }

◆ star()

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

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

3464  {
3465  MK_EXPR1(Z3_mk_re_star, re);
3466  }

◆ store() [1/5]

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

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

3330  {
3331  check_context(a, i); check_context(a, v);
3332  Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
3333  a.check_error();
3334  return expr(a.ctx(), r);
3335  }

Referenced by store().

◆ store() [2/5]

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

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

3338 { return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }

◆ store() [3/5]

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

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

3342  {
3343  check_context(a, i); check_context(a, v);
3344  array<Z3_ast> idxs(i);
3345  Z3_ast r = Z3_mk_store_n(a.ctx(), a, idxs.size(), idxs.ptr(), v);
3346  a.check_error();
3347  return expr(a.ctx(), r);
3348  }

◆ store() [4/5]

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

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

3337 { return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), v); }

◆ store() [5/5]

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

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

3339  {
3340  return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
3341  }

◆ suffixof()

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

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

3428  {
3429  check_context(a, b);
3430  Z3_ast r = Z3_mk_seq_suffix(a.ctx(), a, b);
3431  a.check_error();
3432  return expr(a.ctx(), r);
3433  }

◆ sum()

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

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

2095  {
2096  assert(args.size() > 0);
2097  context& ctx = args[0].ctx();
2098  array<Z3_ast> _args(args);
2099  Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
2100  ctx.check_error();
2101  return expr(ctx, r);
2102  }

◆ to_check_result()

check_result z3::to_check_result ( Z3_lbool  l)
inline

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

144  {
145  if (l == Z3_L_TRUE) return sat;
146  else if (l == Z3_L_FALSE) return unsat;
147  return unknown;
148  }

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

◆ to_expr()

expr z3::to_expr ( context c,
Z3_ast  a 
)
inline

Wraps a Z3_ast as an expr object. It also checks for errors. This function allows the user to use the whole C API with the C++ layer defined in this file.

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

1774  {
1775  c.check_error();
1776  assert(Z3_get_ast_kind(c, a) == Z3_APP_AST ||
1777  Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
1778  Z3_get_ast_kind(c, a) == Z3_VAR_AST ||
1780  return expr(c, a);
1781  }

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

◆ to_func_decl()

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

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

1788  {
1789  c.check_error();
1790  return func_decl(c, f);
1791  }

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

◆ to_re()

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

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

3452  {
3454  }

◆ to_real()

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

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

3270 { Z3_ast r = Z3_mk_int2real(a.ctx(), a); a.check_error(); return expr(a.ctx(), r); }

◆ to_sort()

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

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

1783  {
1784  c.check_error();
1785  return sort(c, s);
1786  }

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

◆ tree_order()

func_decl z3::tree_order ( sort const &  a,
unsigned  index 
)
inline

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

1934  {
1935  return to_func_decl(a.ctx(), Z3_mk_tree_order(a.ctx(), a, index));
1936  }

◆ try_for()

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

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

2704  {
2705  Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
2706  t.check_error();
2707  return tactic(t.ctx(), r);
2708  }

◆ udiv() [1/3]

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

unsigned division operator for bitvectors.

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

1834 { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }

Referenced by udiv().

◆ udiv() [2/3]

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

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

1835 { return udiv(a, a.ctx().num_val(b, a.get_sort())); }

◆ udiv() [3/3]

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

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

1836 { return udiv(b.ctx().num_val(a, b.get_sort()), b); }

◆ uge() [1/3]

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

unsigned greater than or equal to operator for bitvectors.

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

1822 { return to_expr(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b)); }

Referenced by uge().

◆ uge() [2/3]

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

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

1823 { return uge(a, a.ctx().num_val(b, a.get_sort())); }

◆ uge() [3/3]

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

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

1824 { return uge(b.ctx().num_val(a, b.get_sort()), b); }

◆ ugt() [1/3]

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

unsigned greater than operator for bitvectors.

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

1828 { return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }

Referenced by ugt().

◆ ugt() [2/3]

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

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

1829 { return ugt(a, a.ctx().num_val(b, a.get_sort())); }

◆ ugt() [3/3]

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

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

1830 { return ugt(b.ctx().num_val(a, b.get_sort()), b); }

◆ ule() [1/3]

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

unsigned less than or equal to operator for bitvectors.

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

1810 { return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }

Referenced by ule().

◆ ule() [2/3]

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

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

1811 { return ule(a, a.ctx().num_val(b, a.get_sort())); }

◆ ule() [3/3]

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

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

1812 { return ule(b.ctx().num_val(a, b.get_sort()), b); }

◆ ult() [1/3]

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

unsigned less than operator for bitvectors.

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

1816 { return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); }

Referenced by ult().

◆ ult() [2/3]

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

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

1817 { return ult(a, a.ctx().num_val(b, a.get_sort())); }

◆ ult() [3/3]

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

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

1818 { return ult(b.ctx().num_val(a, b.get_sort()), b); }

◆ urem() [1/3]

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

unsigned reminder operator for bitvectors

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

1855 { return to_expr(a.ctx(), Z3_mk_bvurem(a.ctx(), a, b)); }

Referenced by urem().

◆ urem() [2/3]

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

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

1856 { return urem(a, a.ctx().num_val(b, a.get_sort())); }

◆ urem() [3/3]

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

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

1857 { return urem(b.ctx().num_val(a, b.get_sort()), b); }

◆ when()

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

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

2949  {
2950  check_context(p, t);
2951  Z3_tactic r = Z3_tactic_when(t.ctx(), p, t);
2952  t.check_error();
2953  return tactic(t.ctx(), r);
2954  }

◆ with()

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

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

2699  {
2700  Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
2701  t.check_error();
2702  return tactic(t.ctx(), r);
2703  }

◆ xnor()

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

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

1691 { check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); return expr(a.ctx(), r); }

◆ zext()

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

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

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

1883 { return to_expr(a.ctx(), Z3_mk_zero_ext(a.ctx(), i, a)); }
Z3_mk_re_plus
Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re)
Create the regular language re+.
Z3_global_param_reset_all
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...
Z3_mk_unary_minus
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
Z3_mk_store_n
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.
Z3_apply_result_to_string
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.
Z3_mk_re_option
Z3_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re)
Create the regular language [re].
Z3_mk_bvshl
Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2)
Shift left.
Z3_tactic_par_and_then
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....
Z3_mk_forall_const
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.
Z3_mk_select
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.
Z3_solver_to_string
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.
Z3_mk_re_complement
Z3_ast Z3_API Z3_mk_re_complement(Z3_context c, Z3_ast re)
Create the complement of the regular language re.
Z3_mk_fpa_min
Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2)
Minimum of floating-point numbers.
z3::smod
expr smod(int a, expr const &b)
Definition: z3++.h:1850
Z3_mk_bvslt
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than.
Z3_mk_ge
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
Z3_mk_bvmul_no_underflow
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...
Z3_mk_bvmul_no_overflow
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.
Z3_mk_fpa_rem
Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point remainder.
Z3_probe_le
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...
_Z3_MK_BIN_
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1370
Z3_get_ast_kind
Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a)
Return the kind of the given AST.
Z3_probe_and
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.
z3::pw
expr pw(int a, expr const &b)
Definition: z3++.h:1387
Z3_mk_zero_ext
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,...
Z3_mk_seq_concat
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
Z3_tactic_fail_if
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.
Z3_APP_AST
@ Z3_APP_AST
Definition: z3_api.h:180
Z3_mk_gt
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
Z3_tactic_try_for
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...
Z3_mk_fpa_fma
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.
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3488
Z3_mk_re_full
Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re)
Create an universal regular expression of sort re.
Z3_mk_bv2int
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...
Z3_mk_and
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].
Z3_mk_fpa_sqrt
Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point square root.
Z3_THROW
#define Z3_THROW(x)
Definition: z3++.h:99
Z3_params_to_string
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...
z3py.tactics
def tactics(ctx=None)
Definition: z3py.py:7910
Z3_mk_set_del
Z3_ast Z3_API Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem)
Remove an element to a set.
Z3_mk_seq_suffix
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.
z3::rem
expr rem(int a, expr const &b)
Definition: z3++.h:1413
Z3_mk_bvneg_no_overflow
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.
Z3_mk_bvmul
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
Z3_mk_full_set
Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain)
Create the full set.
Z3_is_eq_ast
bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2)
Compare terms.
Z3_mk_or
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].
Z3_mk_set_union
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.
Z3_mk_set_intersect
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.
z3::shl
expr shl(int a, expr const &b)
Definition: z3++.h:1864
Z3_mk_distinct
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]).
Z3_mk_empty_set
Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain)
Create the empty set.
Z3_mk_bvnor
Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nor.
Z3_L_TRUE
@ Z3_L_TRUE
Definition: z3_api.h:103
Z3_mk_fpa_leq
Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than or equal.
Z3_mk_linear_order
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.
Z3_optimize_to_string
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)
Print the current context as a string.
Z3_mk_add
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::context::function
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3036
Z3_probe_or
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.
Z3_mk_bvugt
Z3_ast Z3_API Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than.
Z3_mk_seq_prefix
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.
Z3_mk_concat
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
Z3_mk_implies
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
Z3_mk_rem
Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 rem arg2.
Z3_mk_pbeq
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.
Z3_is_re_sort
bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.
_Z3_MK_UN_
#define _Z3_MK_UN_(a, mkun)
Definition: z3++.h:1417
Z3_mk_bvadd_no_overflow
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.
z3::slt
expr slt(int a, expr const &b)
Definition: z3++.h:1804
Z3_mk_bvnot
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
Z3_ast_to_string
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.
z3::ugt
expr ugt(int a, expr const &b)
Definition: z3++.h:1830
Z3_mk_re_star
Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re)
Create the regular language re*.
Z3_mk_eq
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.
z3::RTN
@ RTN
Definition: z3++.h:140
z3::lshr
expr lshr(int a, expr const &b)
Definition: z3++.h:1871
Z3_mk_fpa_gt
Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than.
Z3_mk_set_complement
Z3_ast Z3_API Z3_mk_set_complement(Z3_context c, Z3_ast arg)
Take the complement of a set.
Z3_mk_fpa_sub
Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point subtraction.
Z3_mk_fpa_neg
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.
z3::ashr
expr ashr(int a, expr const &b)
Definition: z3++.h:1878
Z3_tactic_using_params
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.
z3::srem
expr srem(int a, expr const &b)
Definition: z3++.h:1843
Z3_mk_exists_const
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.
Z3_mk_bvsge
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.
z3::ule
expr ule(int a, expr const &b)
Definition: z3++.h:1812
Z3_mk_seq_last_index
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,...
Z3_mk_bvadd
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement addition.
Z3_stats_to_string
Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)
Convert a statistics into a string.
z3::concat
expr concat(expr_vector const &args)
Definition: z3++.h:2131
Z3_mk_bvneg
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.
z3::ult
expr ult(int a, expr const &b)
Definition: z3++.h:1818
z3::RTP
@ RTP
Definition: z3++.h:139
Z3_mk_re_range
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.
Z3_mk_ite
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::unsat
@ unsat
Definition: z3++.h:133
z3::unknown
@ unknown
Definition: z3++.h:133
Z3_INT_SYMBOL
@ Z3_INT_SYMBOL
Definition: z3_api.h:115
Z3_mk_seq_in_re
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.
Z3_mk_set_difference
Z3_ast Z3_API Z3_mk_set_difference(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Take the set difference between two sets.
Z3_mk_bvule
Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than or equal to.
z3::sle
expr sle(int a, expr const &b)
Definition: z3++.h:1798
z3::udiv
expr udiv(int a, expr const &b)
Definition: z3++.h:1836
z3::context::recfun
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3107
z3::to_expr
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:1774
Z3_VAR_AST
@ Z3_VAR_AST
Definition: z3_api.h:181
Z3_tactic_cond
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...
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.
Z3_mk_fpa_div
Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point division.
z3::select
expr select(expr const &a, int i)
Definition: z3++.h:3319
Z3_goal_to_string
Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g)
Convert a goal into a string.
Z3_mk_div
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_tactic_repeat
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...
Z3_mk_lt
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
Z3_NUMERAL_AST
@ Z3_NUMERAL_AST
Definition: z3_api.h:179
Z3_mk_seq_to_re
Z3_ast Z3_API Z3_mk_seq_to_re(Z3_context c, Z3_ast seq)
Create a regular expression that accepts the sequence seq.
Z3_probe_ge
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...
Z3_mk_bvashr
Z3_ast Z3_API Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2)
Arithmetic shift right.
Z3_mk_bvurem
Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned remainder.
z3::implies
expr implies(bool a, expr const &b)
Definition: z3++.h:1382
Z3_mk_bvsub_no_overflow
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.
z3::store
expr store(expr const &a, expr_vector const &i, expr const &v)
Definition: z3++.h:3342
Z3_mk_bvsmod
Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows divisor).
Z3_probe_eq
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 ...
z3::urem
expr urem(int a, expr const &b)
Definition: z3++.h:1857
Z3_mk_as_array
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...
Z3_mk_bvadd_no_underflow
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.
Z3_probe_lt
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...
Z3_mk_seq_empty
Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq)
Create an empty sequence of the sequence sort seq.
Z3_mk_select_n
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.
Z3_probe_not
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.
Z3_mk_bvsle
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.
Z3_mk_int2bv
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.
Z3_is_seq_sort
bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
Z3_fixedpoint_to_string
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.
z3::max
expr max(expr const &a, expr const &b)
Definition: z3++.h:1707
Z3_mk_atleast
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
Z3_mk_bvnand
Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nand.
Z3_mk_bvsdiv
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.
Z3_model_to_string
Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m)
Convert the given model into a string.
Z3_mk_set_member
Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set)
Check for set membership.
Z3_tactic_par_or
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.
z3::check_context
void check_context(object const &a, object const &b)
Definition: z3++.h:413
Z3_mk_fpa_lt
Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than.
Z3_mk_bvult
Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than.
Z3_mk_re_union
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_mk_bvudiv
Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned division.
Z3_L_FALSE
@ Z3_L_FALSE
Definition: z3_api.h:101
Z3_mk_bvsub
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
Z3_probe_gt
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...
Z3_mk_sign_ext
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,...
Z3_mk_tree_order
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.
Z3_mk_pble
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.
Z3_mk_bvand
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.
z3::uge
expr uge(int a, expr const &b)
Definition: z3++.h:1824
Z3_mk_bvxnor
Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise xnor.
Z3_mk_bvsub_no_underflow
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.
Z3_mk_fpa_max
Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2)
Maximum of floating-point numbers.
Z3_mk_store
Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v)
Array update.
Z3_mk_not
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).
Z3_mk_fpa_mul
Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point multiplication.
MK_EXPR2
#define MK_EXPR2(_fn, _arg1, _arg2)
Definition: z3++.h:3361
Z3_mk_set_add
Z3_ast Z3_API Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem)
Add an element to a set.
Z3_mk_seq_index
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...
Z3_mk_const_array
Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v)
Create the constant array.
z3::to_func_decl
func_decl to_func_decl(context &c, Z3_func_decl f)
Definition: z3++.h:1788
Z3_mk_int2real
Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1)
Coerce an integer to a real.
Z3_mk_re_intersect
Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[])
Create the intersection of the regular languages.
Z3_mk_fpa_add
Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point addition.
Z3_mk_bvxor
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
Z3_mk_fpa_abs
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.
MK_EXPR1
#define MK_EXPR1(_fn, _arg)
Definition: z3++.h:3356
z3::sat
@ sat
Definition: z3++.h:133
Z3_mk_is_int
Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1)
Check if a real number is an integer.
Z3_global_param_set
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.
Z3_mk_bvsdiv_no_overflow
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.
Z3_mk_bvuge
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
z3::mod
expr mod(int a, expr const &b)
Definition: z3++.h:1398
Z3_mk_atmost
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
Z3_mk_bvsrem
Z3_ast Z3_API Z3_mk_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows dividend).
z3::RTZ
@ RTZ
Definition: z3++.h:141
Z3_mk_mod
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.
Z3_mk_lambda_const
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.
Z3_tactic_and_then
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.
Z3_tactic_or_else
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...
Z3_mk_set_subset
Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Check for subsetness of sets.
Z3_mk_le
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
Z3_mk_bvsgt
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than.
Z3_mk_bvlshr
Z3_ast Z3_API Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2)
Logical shift right.
Z3_mk_pbge
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.
Z3_mk_sub
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].
Z3_mk_re_empty
Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re)
Create an empty regular expression of sort re.
z3::object::ctx
context & ctx() const
Definition: z3++.h:409
Z3_QUANTIFIER_AST
@ Z3_QUANTIFIER_AST
Definition: z3_api.h:182
Z3_tactic_when
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...
Z3_mk_re_concat
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])
Create the concatenation of the regular languages.
Z3_mk_mul
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::RNA
@ RNA
Definition: z3++.h:137
z3::RNE
@ RNE
Definition: z3++.h:138
Z3_mk_bvor
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.
Z3_mk_partial_order
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.
Z3_mk_piecewise_linear_order
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.