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  constructor_list
 
class  constructors
 
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
 
class  user_propagator_base
 

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, double b)
 
expr operator== (double 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, double b)
 
expr operator!= (double 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 bvredor (expr const &a)
 
expr bvredand (expr const &a)
 
expr abs (expr const &a)
 
expr sqrt (expr const &a, expr const &rm)
 
expr fp_eq (expr const &a, expr const &b)
 
expr operator~ (expr const &a)
 
expr fma (expr const &a, expr const &b, expr const &c, expr const &rm)
 
expr fpa_fp (expr const &sgn, expr const &exp, expr const &sig)
 
expr fpa_to_sbv (expr const &t, unsigned sz)
 
expr fpa_to_ubv (expr const &t, unsigned sz)
 
expr sbv_to_fpa (expr const &t, sort s)
 
expr ubv_to_fpa (expr const &t, sort s)
 
expr fpa_to_fpa (expr const &t, sort s)
 
expr round_fpa_to_closest_integer (expr const &t)
 
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 sge (expr const &a, expr const &b)
 signed greater than or equal to operator for bitvectors. More...
 
expr sge (expr const &a, int b)
 
expr sge (int a, expr const &b)
 
expr sgt (expr const &a, expr const &b)
 signed greater than operator for bitvectors. More...
 
expr sgt (expr const &a, int b)
 
expr sgt (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)
 
expr mk_xor (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_diff (expr const &a, expr const &b)
 
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 73 of file z3++.h.

◆ expr_vector

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

◆ func_decl_vector

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

◆ sort_vector

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

Enumeration Type Documentation

◆ check_result

Enumerator
unsat 
sat 
unknown 

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

134  {
135  unsat, sat, unknown
136  };

◆ rounding_mode

Enumerator
RNA 
RNE 
RTP 
RTN 
RTZ 

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

138  {
139  RNA,
140  RNE,
141  RTP,
142  RTN,
143  RTZ
144  };

Function Documentation

◆ abs()

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

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

1962  {
1963  Z3_ast r;
1964  if (a.is_int()) {
1965  expr zero = a.ctx().int_val(0);
1966  expr ge = a >= zero;
1967  expr na = -a;
1968  r = Z3_mk_ite(a.ctx(), ge, a, na);
1969  }
1970  else if (a.is_real()) {
1971  expr zero = a.ctx().real_val(0);
1972  expr ge = a >= zero;
1973  expr na = -a;
1974  r = Z3_mk_ite(a.ctx(), ge, a, na);
1975  }
1976  else {
1977  r = Z3_mk_fpa_abs(a.ctx(), a);
1978  }
1979  a.check_error();
1980  return expr(a.ctx(), r);
1981  }

◆ as_array()

expr z3::as_array ( func_decl f)
inline

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

3801  {
3802  Z3_ast r = Z3_mk_as_array(f.ctx(), f);
3803  f.check_error();
3804  return expr(f.ctx(), r);
3805  }

◆ ashr() [1/3]

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

arithmetic shift right operator for bitvectors

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

2188 { 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 2189 of file z3++.h.

2189 { 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 2190 of file z3++.h.

2190 { 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 2397 of file z3++.h.

2397  {
2398  assert(es.size() > 0);
2399  context& ctx = es[0u].ctx();
2400  array<Z3_ast> _es(es);
2401  Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
2402  ctx.check_error();
2403  return expr(ctx, r);
2404  }

◆ atmost()

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

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

2389  {
2390  assert(es.size() > 0);
2391  context& ctx = es[0u].ctx();
2392  array<Z3_ast> _es(es);
2393  Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
2394  ctx.check_error();
2395  return expr(ctx, r);
2396  }

◆ bv2int()

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

bit-vector and integer conversions.

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

2200 { 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 2206 of file z3++.h.

2206  {
2207  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);
2208  }

◆ bvadd_no_underflow()

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

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

2209  {
2210  check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2211  }

◆ bvmul_no_overflow()

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

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

2224  {
2225  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);
2226  }

◆ bvmul_no_underflow()

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

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

2227  {
2228  check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2229  }

◆ bvneg_no_overflow()

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

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

2221  {
2222  Z3_ast r = Z3_mk_bvneg_no_overflow(a.ctx(), a); a.check_error(); return expr(a.ctx(), r);
2223  }

◆ bvredand()

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

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

1956  {
1957  assert(a.is_bv());
1958  Z3_ast r = Z3_mk_bvredand(a.ctx(), a);
1959  a.check_error();
1960  return expr(a.ctx(), r);
1961  }

◆ bvredor()

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

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

1950  {
1951  assert(a.is_bv());
1952  Z3_ast r = Z3_mk_bvredor(a.ctx(), a);
1953  a.check_error();
1954  return expr(a.ctx(), r);
1955  }

◆ bvsdiv_no_overflow()

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

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

2218  {
2219  check_context(a, b); Z3_ast r = Z3_mk_bvsdiv_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2220  }

◆ bvsub_no_overflow()

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

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

2212  {
2213  check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2214  }

◆ bvsub_no_underflow()

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

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

2215  {
2216  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);
2217  }

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

2423  {
2424  check_context(a, b);
2425  Z3_ast r;
2426  if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
2427  Z3_ast _args[2] = { a, b };
2428  r = Z3_mk_seq_concat(a.ctx(), 2, _args);
2429  }
2430  else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
2431  Z3_ast _args[2] = { a, b };
2432  r = Z3_mk_re_concat(a.ctx(), 2, _args);
2433  }
2434  else {
2435  r = Z3_mk_concat(a.ctx(), a, b);
2436  }
2437  a.ctx().check_error();
2438  return expr(a.ctx(), r);
2439  }

Referenced by operator+().

◆ concat() [2/2]

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

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

2441  {
2442  Z3_ast r;
2443  assert(args.size() > 0);
2444  if (args.size() == 1) {
2445  return args[0u];
2446  }
2447  context& ctx = args[0u].ctx();
2448  array<Z3_ast> _args(args);
2449  if (Z3_is_seq_sort(ctx, args[0u].get_sort())) {
2450  r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
2451  }
2452  else if (Z3_is_re_sort(ctx, args[0u].get_sort())) {
2453  r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
2454  }
2455  else {
2456  r = _args[args.size()-1];
2457  for (unsigned i = args.size()-1; i > 0; ) {
2458  --i;
2459  r = Z3_mk_concat(ctx, _args[i], r);
2460  ctx.check_error();
2461  }
2462  }
2463  ctx.check_error();
2464  return expr(ctx, r);
2465  }

◆ cond()

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

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

3299  {
3300  check_context(p, t1); check_context(p, t2);
3301  Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2);
3302  t1.check_error();
3303  return tactic(t1.ctx(), r);
3304  }

◆ const_array()

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

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

3818  {
3819  MK_EXPR2(Z3_mk_const_array, d, v);
3820  }

◆ distinct()

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

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

2414  {
2415  assert(args.size() > 0);
2416  context& ctx = args[0u].ctx();
2417  array<Z3_ast> _args(args);
2418  Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
2419  ctx.check_error();
2420  return expr(ctx, r);
2421  }

◆ empty()

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

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

3874  {
3875  Z3_ast r = Z3_mk_seq_empty(s.ctx(), s);
3876  s.check_error();
3877  return expr(s.ctx(), r);
3878  }

◆ empty_set()

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

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

3822  {
3824  }

◆ eq()

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

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

561 { 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 2316 of file z3++.h.

2316  {
2317  check_context(x, b);
2318  Z3_app vars[] = {(Z3_app) x};
2319  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2320  }

◆ exists() [2/5]

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

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

2321  {
2322  check_context(x1, b); check_context(x2, b);
2323  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2324  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2325  }

◆ exists() [3/5]

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

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

2326  {
2327  check_context(x1, b); check_context(x2, b); check_context(x3, b);
2328  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2329  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2330  }

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

2331  {
2332  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2333  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2334  Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2335  }

◆ exists() [5/5]

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

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

2336  {
2337  array<Z3_app> vars(xs);
2338  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);
2339  }

◆ fail_if()

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

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

3288  {
3289  Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
3290  p.check_error();
3291  return tactic(p.ctx(), r);
3292  }

◆ fma()

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

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

1998  {
1999  check_context(a, b); check_context(a, c); check_context(a, rm);
2000  assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
2001  Z3_ast r = Z3_mk_fpa_fma(a.ctx(), rm, a, b, c);
2002  a.check_error();
2003  return expr(a.ctx(), r);
2004  }

◆ forall() [1/5]

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

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

2292  {
2293  check_context(x, b);
2294  Z3_app vars[] = {(Z3_app) x};
2295  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2296  }

◆ forall() [2/5]

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

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

2297  {
2298  check_context(x1, b); check_context(x2, b);
2299  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2300  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2301  }

◆ forall() [3/5]

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

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

2302  {
2303  check_context(x1, b); check_context(x2, b); check_context(x3, b);
2304  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2305  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2306  }

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

2307  {
2308  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2309  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2310  Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2311  }

◆ forall() [5/5]

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

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

2312  {
2313  array<Z3_app> vars(xs);
2314  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);
2315  }

◆ fp_eq()

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

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

1989  {
1990  check_context(a, b);
1991  assert(a.is_fpa());
1992  Z3_ast r = Z3_mk_fpa_eq(a.ctx(), a, b);
1993  a.check_error();
1994  return expr(a.ctx(), r);
1995  }

◆ fpa_fp()

expr z3::fpa_fp ( expr const &  sgn,
expr const &  exp,
expr const &  sig 
)
inline

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

2006  {
2007  check_context(sgn, exp); check_context(exp, sig);
2008  assert(sgn.is_bv() && exp.is_bv() && sig.is_bv());
2009  Z3_ast r = Z3_mk_fpa_fp(sgn.ctx(), sgn, exp, sig);
2010  sgn.check_error();
2011  return expr(sgn.ctx(), r);
2012  }

◆ fpa_to_fpa()

expr z3::fpa_to_fpa ( expr const &  t,
sort  s 
)
inline

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

2042  {
2043  assert(t.is_fpa());
2044  Z3_ast r = Z3_mk_fpa_to_fp_float(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2045  t.check_error();
2046  return expr(t.ctx(), r);
2047  }

◆ fpa_to_sbv()

expr z3::fpa_to_sbv ( expr const &  t,
unsigned  sz 
)
inline

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

2014  {
2015  assert(t.is_fpa());
2016  Z3_ast r = Z3_mk_fpa_to_sbv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
2017  t.check_error();
2018  return expr(t.ctx(), r);
2019  }

◆ fpa_to_ubv()

expr z3::fpa_to_ubv ( expr const &  t,
unsigned  sz 
)
inline

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

2021  {
2022  assert(t.is_fpa());
2023  Z3_ast r = Z3_mk_fpa_to_ubv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
2024  t.check_error();
2025  return expr(t.ctx(), r);
2026  }

◆ full_set()

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

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

3826  {
3828  }

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

3741  {
3742  return range.ctx().function(name, d1, d2, d3, d4, d5, range);
3743  }

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

3738  {
3739  return range.ctx().function(name, d1, d2, d3, d4, range);
3740  }

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

3735  {
3736  return range.ctx().function(name, d1, d2, d3, range);
3737  }

◆ function() [4/9]

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

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

3732  {
3733  return range.ctx().function(name, d1, d2, range);
3734  }

◆ function() [5/9]

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

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

3729  {
3730  return range.ctx().function(name, domain, range);
3731  }

◆ function() [6/9]

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

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

3744  {
3745  return range.ctx().function(name, domain, range);
3746  }

◆ function() [7/9]

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

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

3726  {
3727  return range.ctx().function(name, arity, domain, range);
3728  }

◆ function() [8/9]

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

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

3747  {
3748  return range.ctx().function(name.c_str(), domain, range);
3749  }

◆ function() [9/9]

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

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

3723  {
3724  return range.ctx().function(name, arity, domain, range);
3725  }

◆ implies() [1/3]

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

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

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

◆ implies() [2/3]

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

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

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

◆ implies() [3/3]

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

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

1598  {
1599  assert(a.is_bool() && b.is_bool());
1600  _Z3_MK_BIN_(a, b, Z3_mk_implies);
1601  }

Referenced by implies().

◆ in_re()

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

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

3906  {
3907  MK_EXPR2(Z3_mk_seq_in_re, s, re);
3908  }

◆ indexof()

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

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

3891  {
3892  check_context(s, substr); check_context(s, offset);
3893  Z3_ast r = Z3_mk_seq_index(s.ctx(), s, substr, offset);
3894  s.check_error();
3895  return expr(s.ctx(), r);
3896  }

◆ int2bv()

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

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

2201 { 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 1646 of file z3++.h.

1646 { _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 2061 of file z3++.h.

2061  {
2062  check_context(c, t); check_context(c, e);
2063  assert(c.is_bool());
2064  Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
2065  c.check_error();
2066  return expr(c.ctx(), r);
2067  }

◆ lambda() [1/5]

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

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

2340  {
2341  check_context(x, b);
2342  Z3_app vars[] = {(Z3_app) x};
2343  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 1, vars, b); b.check_error(); return expr(b.ctx(), r);
2344  }

◆ lambda() [2/5]

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

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

2345  {
2346  check_context(x1, b); check_context(x2, b);
2347  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2348  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 2, vars, b); b.check_error(); return expr(b.ctx(), r);
2349  }

◆ lambda() [3/5]

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

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

2350  {
2351  check_context(x1, b); check_context(x2, b); check_context(x3, b);
2352  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2353  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 3, vars, b); b.check_error(); return expr(b.ctx(), r);
2354  }

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

2355  {
2356  check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2357  Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2358  Z3_ast r = Z3_mk_lambda_const(b.ctx(), 4, vars, b); b.check_error(); return expr(b.ctx(), r);
2359  }

◆ lambda() [5/5]

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

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

2360  {
2361  array<Z3_app> vars(xs);
2362  Z3_ast r = Z3_mk_lambda_const(b.ctx(), vars.size(), vars.ptr(), b); b.check_error(); return expr(b.ctx(), r);
2363  }

◆ last_indexof()

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

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

3897  {
3898  check_context(s, substr);
3899  Z3_ast r = Z3_mk_seq_last_index(s.ctx(), s, substr);
3900  s.check_error();
3901  return expr(s.ctx(), r);
3902  }

◆ linear_order()

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

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

2237  {
2238  return to_func_decl(a.ctx(), Z3_mk_linear_order(a.ctx(), a, index));
2239  }

◆ lshr() [1/3]

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

logic shift right operator for bitvectors

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

2181 { 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 2182 of file z3++.h.

2182 { 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 2183 of file z3++.h.

2183 { 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 1935 of file z3++.h.

1935  {
1936  check_context(a, b);
1937  Z3_ast r;
1938  if (a.is_arith()) {
1939  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), a, b);
1940  }
1941  else if (a.is_bv()) {
1942  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), a, b);
1943  }
1944  else {
1945  assert(a.is_fpa());
1946  r = Z3_mk_fpa_max(a.ctx(), a, b);
1947  }
1948  return expr(a.ctx(), r);
1949  }

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

◆ min()

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

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

1920  {
1921  check_context(a, b);
1922  Z3_ast r;
1923  if (a.is_arith()) {
1924  r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), b, a);
1925  }
1926  else if (a.is_bv()) {
1927  r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), b, a);
1928  }
1929  else {
1930  assert(a.is_fpa());
1931  r = Z3_mk_fpa_min(a.ctx(), a, b);
1932  }
1933  return expr(a.ctx(), r);
1934  }

◆ mk_and()

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

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

2473  {
2474  array<Z3_ast> _args(args);
2475  Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2476  args.check_error();
2477  return expr(args.ctx(), r);
2478  }

◆ mk_or()

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

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

2467  {
2468  array<Z3_ast> _args(args);
2469  Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2470  args.check_error();
2471  return expr(args.ctx(), r);
2472  }

◆ mk_xor()

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

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

2479  {
2480  if (args.empty())
2481  return args.ctx().bool_val(false);
2482  expr r = args[0u];
2483  for (unsigned i = 1; i < args.size(); ++i)
2484  r = r ^ args[i];
2485  return r;
2486  }

◆ mod() [1/3]

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

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

1610  {
1611  if (a.is_bv()) {
1612  _Z3_MK_BIN_(a, b, Z3_mk_bvsmod);
1613  }
1614  else {
1615  _Z3_MK_BIN_(a, b, Z3_mk_mod);
1616  }
1617  }

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

◆ mod() [2/3]

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

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

1618 { 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 1619 of file z3++.h.

1619 { 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 1917 of file z3++.h.

1917 { if (a.is_bool()) return !(a && b); 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 1918 of file z3++.h.

1918 { if (a.is_bool()) return !(a || b); 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 1644 of file z3++.h.

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

◆ operator!() [2/2]

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

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

3122  {
3123  Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
3124  }

◆ operator!=() [1/5]

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

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

1696 { assert(b.is_fpa()); return b.ctx().fpa_val(a) != b; }

◆ operator!=() [2/5]

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

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

1695 { assert(a.is_fpa()); return a != a.ctx().fpa_val(b); }

◆ operator!=() [3/5]

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

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

1686  {
1687  check_context(a, b);
1688  Z3_ast args[2] = { a, b };
1689  Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1690  a.check_error();
1691  return expr(a.ctx(), r);
1692  }

◆ operator!=() [4/5]

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

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

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

◆ operator!=() [5/5]

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

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

1694 { 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 1621 of file z3++.h.

1621 { return mod(a, b); }

◆ operator%() [2/3]

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

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

1622 { return mod(a, b); }

◆ operator%() [3/3]

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

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

1623 { return mod(a, b); }

◆ operator&() [1/4]

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

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

1905 { if (a.is_bool()) return a && b; 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 1906 of file z3++.h.

1906 { 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 1907 of file z3++.h.

1907 { 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 3003 of file z3++.h.

3003  {
3004  check_context(t1, t2);
3005  Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
3006  t1.check_error();
3007  return tactic(t1.ctx(), r);
3008  }

◆ operator&&() [1/4]

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

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

1660 { 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 1659 of file z3++.h.

1659 { 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 1650 of file z3++.h.

1650  {
1651  check_context(a, b);
1652  assert(a.is_bool() && b.is_bool());
1653  Z3_ast args[2] = { a, b };
1654  Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
1655  a.check_error();
1656  return expr(a.ctx(), r);
1657  }

◆ operator&&() [4/4]

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

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

3116  {
3117  check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3118  }

◆ operator*() [1/3]

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

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

1728  {
1729  check_context(a, b);
1730  Z3_ast r = 0;
1731  if (a.is_arith() && b.is_arith()) {
1732  Z3_ast args[2] = { a, b };
1733  r = Z3_mk_mul(a.ctx(), 2, args);
1734  }
1735  else if (a.is_bv() && b.is_bv()) {
1736  r = Z3_mk_bvmul(a.ctx(), a, b);
1737  }
1738  else if (a.is_fpa() && b.is_fpa()) {
1739  r = Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1740  }
1741  else {
1742  // operator is not supported by given arguments.
1743  assert(false);
1744  }
1745  a.check_error();
1746  return expr(a.ctx(), r);
1747  }

◆ operator*() [2/3]

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

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

1748 { 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 1749 of file z3++.h.

1749 { 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 1698 of file z3++.h.

1698  {
1699  check_context(a, b);
1700  Z3_ast r = 0;
1701  if (a.is_arith() && b.is_arith()) {
1702  Z3_ast args[2] = { a, b };
1703  r = Z3_mk_add(a.ctx(), 2, args);
1704  }
1705  else if (a.is_bv() && b.is_bv()) {
1706  r = Z3_mk_bvadd(a.ctx(), a, b);
1707  }
1708  else if (a.is_seq() && b.is_seq()) {
1709  return concat(a, b);
1710  }
1711  else if (a.is_re() && b.is_re()) {
1712  Z3_ast _args[2] = { a, b };
1713  r = Z3_mk_re_union(a.ctx(), 2, _args);
1714  }
1715  else if (a.is_fpa() && b.is_fpa()) {
1716  r = Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1717  }
1718  else {
1719  // operator is not supported by given arguments.
1720  assert(false);
1721  }
1722  a.check_error();
1723  return expr(a.ctx(), r);
1724  }

◆ operator+() [2/3]

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

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

1725 { 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 1726 of file z3++.h.

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

◆ operator-() [1/4]

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

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

1794  {
1795  Z3_ast r = 0;
1796  if (a.is_arith()) {
1797  r = Z3_mk_unary_minus(a.ctx(), a);
1798  }
1799  else if (a.is_bv()) {
1800  r = Z3_mk_bvneg(a.ctx(), a);
1801  }
1802  else if (a.is_fpa()) {
1803  r = Z3_mk_fpa_neg(a.ctx(), a);
1804  }
1805  else {
1806  // operator is not supported by given arguments.
1807  assert(false);
1808  }
1809  a.check_error();
1810  return expr(a.ctx(), r);
1811  }

◆ operator-() [2/4]

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

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

1813  {
1814  check_context(a, b);
1815  Z3_ast r = 0;
1816  if (a.is_arith() && b.is_arith()) {
1817  Z3_ast args[2] = { a, b };
1818  r = Z3_mk_sub(a.ctx(), 2, args);
1819  }
1820  else if (a.is_bv() && b.is_bv()) {
1821  r = Z3_mk_bvsub(a.ctx(), a, b);
1822  }
1823  else if (a.is_fpa() && b.is_fpa()) {
1824  r = Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1825  }
1826  else {
1827  // operator is not supported by given arguments.
1828  assert(false);
1829  }
1830  a.check_error();
1831  return expr(a.ctx(), r);
1832  }

◆ operator-() [3/4]

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

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

1833 { 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 1834 of file z3++.h.

1834 { 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 1772 of file z3++.h.

1772  {
1773  check_context(a, b);
1774  Z3_ast r = 0;
1775  if (a.is_arith() && b.is_arith()) {
1776  r = Z3_mk_div(a.ctx(), a, b);
1777  }
1778  else if (a.is_bv() && b.is_bv()) {
1779  r = Z3_mk_bvsdiv(a.ctx(), a, b);
1780  }
1781  else if (a.is_fpa() && b.is_fpa()) {
1782  r = Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1783  }
1784  else {
1785  // operator is not supported by given arguments.
1786  assert(false);
1787  }
1788  a.check_error();
1789  return expr(a.ctx(), r);
1790  }

◆ operator/() [2/3]

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

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

1791 { 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 1792 of file z3++.h.

1792 { 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 3105 of file z3++.h.

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

◆ operator<() [2/6]

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

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

1861  {
1862  check_context(a, b);
1863  Z3_ast r = 0;
1864  if (a.is_arith() && b.is_arith()) {
1865  r = Z3_mk_lt(a.ctx(), a, b);
1866  }
1867  else if (a.is_bv() && b.is_bv()) {
1868  r = Z3_mk_bvslt(a.ctx(), a, b);
1869  }
1870  else if (a.is_fpa() && b.is_fpa()) {
1871  r = Z3_mk_fpa_lt(a.ctx(), a, b);
1872  }
1873  else {
1874  // operator is not supported by given arguments.
1875  assert(false);
1876  }
1877  a.check_error();
1878  return expr(a.ctx(), r);
1879  }

◆ operator<() [3/6]

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

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

1880 { 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 1881 of file z3++.h.

1881 { 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 3104 of file z3++.h.

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

◆ operator<() [6/6]

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

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

3101  {
3102  check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3103  }

◆ operator<<() [1/13]

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

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

2961 { 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 557 of file z3++.h.

557  {
558  out << Z3_ast_to_string(n.ctx(), n.m_ast); return out;
559  }

◆ operator<<() [3/13]

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

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

2655  {
2656  if (r == unsat) out << "unsat";
2657  else if (r == sat) out << "sat";
2658  else out << "unknown";
2659  return out;
2660  }

◆ operator<<() [4/13]

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

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

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

◆ operator<<() [5/13]

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

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

3286 { 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 2937 of file z3++.h.

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

2623 { return out << m.to_string(); }

◆ operator<<() [8/13]

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

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

3228 { 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 500 of file z3++.h.

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

◆ operator<<() [10/13]

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

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

524  {
525  out << Z3_params_to_string(p.ctx(), p); return out;
526  }

◆ operator<<() [11/13]

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

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

2878 { 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 2652 of file z3++.h.

2652 { 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 468 of file z3++.h.

468  {
469  if (s.kind() == Z3_INT_SYMBOL)
470  out << "k!" << s.to_int();
471  else
472  out << s.str();
473  return out;
474  }

◆ operator<=() [1/6]

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

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

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

◆ operator<=() [2/6]

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

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

1836  {
1837  check_context(a, b);
1838  Z3_ast r = 0;
1839  if (a.is_arith() && b.is_arith()) {
1840  r = Z3_mk_le(a.ctx(), a, b);
1841  }
1842  else if (a.is_bv() && b.is_bv()) {
1843  r = Z3_mk_bvsle(a.ctx(), a, b);
1844  }
1845  else if (a.is_fpa() && b.is_fpa()) {
1846  r = Z3_mk_fpa_leq(a.ctx(), a, b);
1847  }
1848  else {
1849  // operator is not supported by given arguments.
1850  assert(false);
1851  }
1852  a.check_error();
1853  return expr(a.ctx(), r);
1854  }

◆ operator<=() [3/6]

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

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

1855 { 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 1856 of file z3++.h.

1856 { 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 3094 of file z3++.h.

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

◆ operator<=() [6/6]

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

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

3091  {
3092  check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3093  }

◆ operator==() [1/8]

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

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

1684 { assert(b.is_fpa()); return b.ctx().fpa_val(a) == b; }

◆ operator==() [2/8]

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

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

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

◆ operator==() [3/8]

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

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

1683 { assert(a.is_fpa()); return a == a.ctx().fpa_val(b); }

◆ operator==() [4/8]

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

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

1675  {
1676  check_context(a, b);
1677  Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1678  a.check_error();
1679  return expr(a.ctx(), r);
1680  }

◆ operator==() [5/8]

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

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

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

◆ operator==() [6/8]

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

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

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

◆ operator==() [7/8]

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

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

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

◆ operator==() [8/8]

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

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

3111  {
3112  check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3113  }

◆ operator>() [1/6]

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

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

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

◆ operator>() [2/6]

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

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

1883  {
1884  check_context(a, b);
1885  Z3_ast r = 0;
1886  if (a.is_arith() && b.is_arith()) {
1887  r = Z3_mk_gt(a.ctx(), a, b);
1888  }
1889  else if (a.is_bv() && b.is_bv()) {
1890  r = Z3_mk_bvsgt(a.ctx(), a, b);
1891  }
1892  else if (a.is_fpa() && b.is_fpa()) {
1893  r = Z3_mk_fpa_gt(a.ctx(), a, b);
1894  }
1895  else {
1896  // operator is not supported by given arguments.
1897  assert(false);
1898  }
1899  a.check_error();
1900  return expr(a.ctx(), r);
1901  }

◆ operator>() [3/6]

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

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

1902 { 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 1903 of file z3++.h.

1903 { 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 3109 of file z3++.h.

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

◆ operator>() [6/6]

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

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

3106  {
3107  check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3108  }

◆ operator>=() [1/6]

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

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

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

◆ operator>=() [2/6]

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

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

1752  {
1753  check_context(a, b);
1754  Z3_ast r = 0;
1755  if (a.is_arith() && b.is_arith()) {
1756  r = Z3_mk_ge(a.ctx(), a, b);
1757  }
1758  else if (a.is_bv() && b.is_bv()) {
1759  r = Z3_mk_bvsge(a.ctx(), a, b);
1760  }
1761  else if (a.is_fpa() && b.is_fpa()) {
1762  r = Z3_mk_fpa_geq(a.ctx(), a, b);
1763  }
1764  else {
1765  // operator is not supported by given arguments.
1766  assert(false);
1767  }
1768  a.check_error();
1769  return expr(a.ctx(), r);
1770  }

◆ operator>=() [3/6]

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

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

1858 { 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 1859 of file z3++.h.

1859 { 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 3099 of file z3++.h.

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

◆ operator>=() [6/6]

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

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

3096  {
3097  check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3098  }

◆ operator^() [1/3]

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

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

1909 { check_context(a, b); Z3_ast r = a.is_bool() ? Z3_mk_xor(a.ctx(), a, b) : 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 1910 of file z3++.h.

1910 { 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 1911 of file z3++.h.

1911 { 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 1913 of file z3++.h.

1913 { if (a.is_bool()) return a || b; 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 1914 of file z3++.h.

1914 { 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 1915 of file z3++.h.

1915 { 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 3010 of file z3++.h.

3010  {
3011  check_context(t1, t2);
3012  Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
3013  t1.check_error();
3014  return tactic(t1.ctx(), r);
3015  }

◆ operator||() [1/4]

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

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

1673 { 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 1671 of file z3++.h.

1671 { 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 1662 of file z3++.h.

1662  {
1663  check_context(a, b);
1664  assert(a.is_bool() && b.is_bool());
1665  Z3_ast args[2] = { a, b };
1666  Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1667  a.check_error();
1668  return expr(a.ctx(), r);
1669  }

◆ operator||() [4/4]

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

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

3119  {
3120  check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3121  }

◆ operator~()

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

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

1996 { 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 3912 of file z3++.h.

3912  {
3914  }

◆ par_and_then()

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

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

3042  {
3043  check_context(t1, t2);
3044  Z3_tactic r = Z3_tactic_par_and_then(t1.ctx(), t1, t2);
3045  t1.check_error();
3046  return tactic(t1.ctx(), r);
3047  }

◆ par_or()

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

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

3033  {
3034  if (n == 0) {
3035  Z3_THROW(exception("a non-zero number of tactics need to be passed to par_or"));
3036  }
3037  array<Z3_tactic> buffer(n);
3038  for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];
3039  return tactic(tactics[0u].ctx(), Z3_tactic_par_or(tactics[0u].ctx(), n, buffer.ptr()));
3040  }

◆ partial_order()

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

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

2240  {
2241  return to_func_decl(a.ctx(), Z3_mk_partial_order(a.ctx(), a, index));
2242  }

◆ pbeq()

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

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

2381  {
2382  assert(es.size() > 0);
2383  context& ctx = es[0u].ctx();
2384  array<Z3_ast> _es(es);
2385  Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
2386  ctx.check_error();
2387  return expr(ctx, r);
2388  }

◆ pbge()

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

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

2373  {
2374  assert(es.size() > 0);
2375  context& ctx = es[0u].ctx();
2376  array<Z3_ast> _es(es);
2377  Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
2378  ctx.check_error();
2379  return expr(ctx, r);
2380  }

◆ pble()

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

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

2365  {
2366  assert(es.size() > 0);
2367  context& ctx = es[0u].ctx();
2368  array<Z3_ast> _es(es);
2369  Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
2370  ctx.check_error();
2371  return expr(ctx, r);
2372  }

◆ piecewise_linear_order()

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

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

2243  {
2244  return to_func_decl(a.ctx(), Z3_mk_piecewise_linear_order(a.ctx(), a, index));
2245  }

◆ plus()

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

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

3909  {
3910  MK_EXPR1(Z3_mk_re_plus, re);
3911  }

◆ prefixof()

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

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

3885  {
3886  check_context(a, b);
3887  Z3_ast r = Z3_mk_seq_prefix(a.ctx(), a, b);
3888  a.check_error();
3889  return expr(a.ctx(), r);
3890  }

◆ pw() [1/3]

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

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

1606 { _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 1607 of file z3++.h.

1607 { 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 1608 of file z3++.h.

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

◆ range()

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

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

3946  {
3947  check_context(lo, hi);
3948  Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
3949  lo.check_error();
3950  return expr(lo.ctx(), r);
3951  }

Referenced by AstVector::__getitem__(), z3py::AndThen(), z3py::ArraySort(), Goal::as_expr(), ApplyResult::as_expr(), FuncEntry::as_list(), FuncInterp::as_list(), NativeSolver::AssertInjective(), z3py::AtLeast(), z3py::BoolVector(), Solver::check(), Optimize::check(), ExprRef::children(), z3py::Concat(), Solver::consequences(), z3py::CreateDatatypes(), ModelRef::decls(), z3py::describe_probes(), z3py::DisjointSum(), z3py::EnumSort(), z3py::eq(), z3py::FreshFunction(), context::function(), z3py::Function(), function(), Statistics::get_key_value(), z3py::Intersect(), z3py::IntVector(), z3py::is_quantifier(), Statistics::keys(), z3py::Lambda(), Context::MkArrayConst(), Context::MkArraySort(), NativeContext::MkArraySort(), Context::MkConst(), Context::MkConstDecl(), NativeContext::MkConstDecl(), Context::MkFreshConst(), Context::MkFreshConstDecl(), Context::MkFreshFuncDecl(), NativeContext::MkFreshFuncDecl(), Context::MkFuncDecl(), NativeContext::MkFuncDecl(), Context::MkRecFuncDecl(), Context::MkUserPropagatorFuncDecl(), z3py::OrElse(), z3py::ParOr(), z3py::probes(), z3py::PropagateFunction(), z3py::RealVarVector(), z3py::RealVector(), z3py::RecAddDefinition(), context::recfun(), recfun(), z3py::RecFunction(), z3py::set_default_fp_sort(), Fixedpoint::set_predicate_representation(), ModelRef::sorts(), z3py::substitute(), z3py::substitute_funs(), z3py::substitute_vars(), z3py::tactics(), Solver::to_smt2(), z3py::TupleSort(), z3py::Union(), z3py::Update(), ModelRef::update_value(), and context::user_propagate_function().

◆ re_complement()

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

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

3943  {
3945  }

◆ re_diff()

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

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

3936  {
3937  check_context(a, b);
3938  context& ctx = a.ctx();
3939  Z3_ast r = Z3_mk_re_diff(ctx, a, b);
3940  ctx.check_error();
3941  return expr(ctx, r);
3942  }

◆ re_empty()

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

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

3918  {
3919  Z3_ast r = Z3_mk_re_empty(s.ctx(), s);
3920  s.check_error();
3921  return expr(s.ctx(), r);
3922  }

◆ re_full()

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

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

3923  {
3924  Z3_ast r = Z3_mk_re_full(s.ctx(), s);
3925  s.check_error();
3926  return expr(s.ctx(), r);
3927  }

◆ re_intersect()

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

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

3928  {
3929  assert(args.size() > 0);
3930  context& ctx = args[0u].ctx();
3931  array<Z3_ast> _args(args);
3932  Z3_ast r = Z3_mk_re_intersect(ctx, _args.size(), _args.ptr());
3933  ctx.check_error();
3934  return expr(ctx, r);
3935  }

◆ recfun() [1/4]

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

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

3760  {
3761  return range.ctx().recfun(name, d1, d2, range);
3762  }

◆ recfun() [2/4]

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

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

3757  {
3758  return range.ctx().recfun(name, d1, range);
3759  }

◆ recfun() [3/4]

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

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

3754  {
3755  return range.ctx().recfun(name, arity, domain, range);
3756  }

◆ recfun() [4/4]

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

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

3751  {
3752  return range.ctx().recfun(name, arity, domain, range);
3753  }

◆ rem() [1/3]

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

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

1626  {
1627  if (a.is_fpa() && b.is_fpa()) {
1628  _Z3_MK_BIN_(a, b, Z3_mk_fpa_rem);
1629  } else {
1630  _Z3_MK_BIN_(a, b, Z3_mk_rem);
1631  }
1632  }

Referenced by rem().

◆ rem() [2/3]

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

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

1633 { 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 1634 of file z3++.h.

1634 { 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 3017 of file z3++.h.

3017  {
3018  Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
3019  t.check_error();
3020  return tactic(t.ctx(), r);
3021  }

◆ reset_params()

void z3::reset_params ( )
inline

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

◆ round_fpa_to_closest_integer()

expr z3::round_fpa_to_closest_integer ( expr const &  t)
inline

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

2049  {
2050  assert(t.is_fpa());
2051  Z3_ast r = Z3_mk_fpa_round_to_integral(t.ctx(), t.ctx().fpa_rounding_mode(), t);
2052  t.check_error();
2053  return expr(t.ctx(), r);
2054  }

◆ sbv_to_fpa()

expr z3::sbv_to_fpa ( expr const &  t,
sort  s 
)
inline

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

2028  {
2029  assert(t.is_bv());
2030  Z3_ast r = Z3_mk_fpa_to_fp_signed(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2031  t.check_error();
2032  return expr(t.ctx(), r);
2033  }

◆ select() [1/3]

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

forward declarations

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

3764  {
3765  check_context(a, i);
3766  Z3_ast r = Z3_mk_select(a.ctx(), a, i);
3767  a.check_error();
3768  return expr(a.ctx(), r);
3769  }

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

◆ select() [2/3]

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

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

3773  {
3774  check_context(a, i);
3775  array<Z3_ast> idxs(i);
3776  Z3_ast r = Z3_mk_select_n(a.ctx(), a, idxs.size(), idxs.ptr());
3777  a.check_error();
3778  return expr(a.ctx(), r);
3779  }

◆ select() [3/3]

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

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

3770  {
3771  return select(a, a.ctx().num_val(i, a.get_sort().array_domain()));
3772  }

◆ set_add()

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

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

3830  {
3831  MK_EXPR2(Z3_mk_set_add, s, e);
3832  }

◆ set_complement()

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

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

3858  {
3860  }

◆ set_del()

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

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

3834  {
3835  MK_EXPR2(Z3_mk_set_del, s, e);
3836  }

◆ set_difference()

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

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

3854  {
3856  }

◆ set_intersect()

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

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

3846  {
3847  check_context(a, b);
3848  Z3_ast es[2] = { a, b };
3849  Z3_ast r = Z3_mk_set_intersect(a.ctx(), 2, es);
3850  a.check_error();
3851  return expr(a.ctx(), r);
3852  }

◆ set_member()

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

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

3862  {
3863  MK_EXPR2(Z3_mk_set_member, s, e);
3864  }

◆ set_param() [1/3]

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

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

80 { 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 79 of file z3++.h.

79 { Z3_global_param_set(param, value); }

◆ set_param() [3/3]

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

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

81 { auto str = std::to_string(value); Z3_global_param_set(param, str.c_str()); }

◆ set_subset()

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

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

3866  {
3867  MK_EXPR2(Z3_mk_set_subset, a, b);
3868  }

◆ set_union()

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

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

3838  {
3839  check_context(a, b);
3840  Z3_ast es[2] = { a, b };
3841  Z3_ast r = Z3_mk_set_union(a.ctx(), 2, es);
3842  a.check_error();
3843  return expr(a.ctx(), r);
3844  }

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

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

◆ sge() [1/3]

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

signed greater than or equal to operator for bitvectors.

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

2108 { return to_expr(a.ctx(), Z3_mk_bvsge(a.ctx(), a, b)); }

Referenced by sge().

◆ sge() [2/3]

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

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

2109 { return sge(a, a.ctx().num_val(b, a.get_sort())); }

◆ sge() [3/3]

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

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

2110 { return sge(b.ctx().num_val(a, b.get_sort()), b); }

◆ sgt() [1/3]

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

signed greater than operator for bitvectors.

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

2114 { return to_expr(a.ctx(), Z3_mk_bvsgt(a.ctx(), a, b)); }

Referenced by sgt().

◆ sgt() [2/3]

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

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

2115 { return sgt(a, a.ctx().num_val(b, a.get_sort())); }

◆ sgt() [3/3]

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

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

2116 { return sgt(b.ctx().num_val(a, b.get_sort()), b); }

◆ shl() [1/3]

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

shift left operator for bitvectors

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

2174 { 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 2175 of file z3++.h.

2175 { 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 2176 of file z3++.h.

2176 { 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 2096 of file z3++.h.

2096 { 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 2097 of file z3++.h.

2097 { 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 2098 of file z3++.h.

2098 { 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 2102 of file z3++.h.

2102 { 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 2103 of file z3++.h.

2103 { 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 2104 of file z3++.h.

2104 { 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 2160 of file z3++.h.

2160 { 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 2161 of file z3++.h.

2161 { 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 2162 of file z3++.h.

2162 { 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 1982 of file z3++.h.

1982  {
1983  check_context(a, rm);
1984  assert(a.is_fpa());
1985  Z3_ast r = Z3_mk_fpa_sqrt(a.ctx(), rm, a);
1986  a.check_error();
1987  return expr(a.ctx(), r);
1988  }

◆ srem() [1/3]

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

signed remainder operator for bitvectors

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

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

2154 { 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 2155 of file z3++.h.

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

◆ star()

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

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

3915  {
3916  MK_EXPR1(Z3_mk_re_star, re);
3917  }

◆ store() [1/5]

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

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

3781  {
3782  check_context(a, i); check_context(a, v);
3783  Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
3784  a.check_error();
3785  return expr(a.ctx(), r);
3786  }

Referenced by store().

◆ store() [2/5]

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

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

3789 { 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 3793 of file z3++.h.

3793  {
3794  check_context(a, i); check_context(a, v);
3795  array<Z3_ast> idxs(i);
3796  Z3_ast r = Z3_mk_store_n(a.ctx(), a, idxs.size(), idxs.ptr(), v);
3797  a.check_error();
3798  return expr(a.ctx(), r);
3799  }

◆ store() [4/5]

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

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

3788 { 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 3790 of file z3++.h.

3790  {
3791  return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
3792  }

◆ suffixof()

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

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

3879  {
3880  check_context(a, b);
3881  Z3_ast r = Z3_mk_seq_suffix(a.ctx(), a, b);
3882  a.check_error();
3883  return expr(a.ctx(), r);
3884  }

◆ sum()

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

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

2405  {
2406  assert(args.size() > 0);
2407  context& ctx = args[0u].ctx();
2408  array<Z3_ast> _args(args);
2409  Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
2410  ctx.check_error();
2411  return expr(ctx, r);
2412  }

◆ to_check_result()

check_result z3::to_check_result ( Z3_lbool  l)
inline

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

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

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

2074  {
2075  c.check_error();
2076  assert(Z3_get_ast_kind(c, a) == Z3_APP_AST ||
2077  Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
2078  Z3_get_ast_kind(c, a) == Z3_VAR_AST ||
2080  return expr(c, a);
2081  }

Referenced by ashr(), lshr(), sext(), sge(), sgt(), 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 2088 of file z3++.h.

2088  {
2089  c.check_error();
2090  return func_decl(c, f);
2091  }

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

3903  {
3905  }

◆ to_real()

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

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

3721 { 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 2083 of file z3++.h.

2083  {
2084  c.check_error();
2085  return sort(c, s);
2086  }

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

2246  {
2247  return to_func_decl(a.ctx(), Z3_mk_tree_order(a.ctx(), a, index));
2248  }

◆ try_for()

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

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

3028  {
3029  Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
3030  t.check_error();
3031  return tactic(t.ctx(), r);
3032  }

◆ ubv_to_fpa()

expr z3::ubv_to_fpa ( expr const &  t,
sort  s 
)
inline

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

2035  {
2036  assert(t.is_bv());
2037  Z3_ast r = Z3_mk_fpa_to_fp_unsigned(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2038  t.check_error();
2039  return expr(t.ctx(), r);
2040  }

◆ udiv() [1/3]

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

unsigned division operator for bitvectors.

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

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

2147 { 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 2148 of file z3++.h.

2148 { 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 2134 of file z3++.h.

2134 { 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 2135 of file z3++.h.

2135 { 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 2136 of file z3++.h.

2136 { 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 2140 of file z3++.h.

2140 { 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 2141 of file z3++.h.

2141 { 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 2142 of file z3++.h.

2142 { 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 2122 of file z3++.h.

2122 { 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 2123 of file z3++.h.

2123 { 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 2124 of file z3++.h.

2124 { 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 2128 of file z3++.h.

2128 { 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 2129 of file z3++.h.

2129 { 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 2130 of file z3++.h.

2130 { 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 2167 of file z3++.h.

2167 { 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 2168 of file z3++.h.

2168 { 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 2169 of file z3++.h.

2169 { 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 3293 of file z3++.h.

3293  {
3294  check_context(p, t);
3295  Z3_tactic r = Z3_tactic_when(t.ctx(), p, t);
3296  t.check_error();
3297  return tactic(t.ctx(), r);
3298  }

◆ with()

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

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

3023  {
3024  Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
3025  t.check_error();
3026  return tactic(t.ctx(), r);
3027  }

◆ xnor()

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

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

1919 { if (a.is_bool()) return !(a ^ b); 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 2195 of file z3++.h.

2195 { return to_expr(a.ctx(), Z3_mk_zero_ext(a.ctx(), i, a)); }
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_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_empty_set
Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain)
Create the empty set.
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_bvuge
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
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_re_diff
Z3_ast Z3_API Z3_mk_re_diff(Z3_context c, Z3_ast re1, Z3_ast re2)
Create the difference of regular expressions.
Z3_mk_fpa_fp
Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig)
Create an expression of FloatingPoint sort from three bit-vector expressions.
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_bvudiv
Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned division.
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_VAR_AST
@ Z3_VAR_AST
Definition: z3_api.h:142
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_is_eq_ast
bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2)
Compare terms.
z3::sgt
expr sgt(int a, expr const &b)
Definition: z3++.h:2116
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_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_L_TRUE
@ Z3_L_TRUE
Definition: z3_api.h:63
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_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_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::smod
expr smod(int a, expr const &b)
Definition: z3++.h:2162
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_fpa_to_fp_unsigned
Z3_ast Z3_API Z3_mk_fpa_to_fp_unsigned(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort.
Z3_mk_int2real
Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1)
Coerce an integer to a real.
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_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_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_BIN_
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1591
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_mk_fpa_to_ubv
Z3_ast Z3_API Z3_mk_fpa_to_ubv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)
Conversion of a floating-point term into an unsigned bit-vector.
z3::pw
expr pw(int a, expr const &b)
Definition: z3++.h:1608
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_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_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_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_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_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_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...
Z3_mk_fpa_to_fp_float
Z3_ast Z3_API Z3_mk_fpa_to_fp_float(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
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_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_bvashr
Z3_ast Z3_API Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2)
Arithmetic shift right.
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_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::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3946
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_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_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_THROW
#define Z3_THROW(x)
Definition: z3++.h:102
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_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_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...
z3py.tactics
def tactics(ctx=None)
Definition: z3py.py:8424
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::rem
expr rem(int a, expr const &b)
Definition: z3++.h:1634
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_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_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_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_fpa_rem
Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point remainder.
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_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::shl
expr shl(int a, expr const &b)
Definition: z3++.h:2176
Z3_L_FALSE
@ Z3_L_FALSE
Definition: z3_api.h:61
Z3_QUANTIFIER_AST
@ Z3_QUANTIFIER_AST
Definition: z3_api.h:143
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_bvnand
Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nand.
Z3_mk_bvugt
Z3_ast Z3_API Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater 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_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_concat
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
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::context::function
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3462
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::sge
expr sge(int a, expr const &b)
Definition: z3++.h:2110
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_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_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_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_mk_bvnor
Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nor.
Z3_mk_fpa_eq
Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point equality.
Z3_mk_bvredand
Z3_ast Z3_API Z3_mk_bvredand(Z3_context c, Z3_ast t1)
Take conjunction of bits in vector, return vector of length 1.
_Z3_MK_UN_
#define _Z3_MK_UN_(a, mkun)
Definition: z3++.h:1638
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::slt
expr slt(int a, expr const &b)
Definition: z3++.h:2104
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_mk_lt
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
z3::ugt
expr ugt(int a, expr const &b)
Definition: z3++.h:2142
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_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_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_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::RTN
@ RTN
Definition: z3++.h:142
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_bvsdiv
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.
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_not
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).
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_mk_full_set
Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain)
Create the full set.
z3::lshr
expr lshr(int a, expr const &b)
Definition: z3++.h:2183
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_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_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::ashr
expr ashr(int a, expr const &b)
Definition: z3++.h:2190
z3::srem
expr srem(int a, expr const &b)
Definition: z3++.h:2155
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_set_member
Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set)
Check for set membership.
z3::ule
expr ule(int a, expr const &b)
Definition: z3++.h:2124
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::concat
expr concat(expr_vector const &args)
Definition: z3++.h:2441
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_fpa_abs
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.
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_mk_re_plus
Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re)
Create the regular language re+.
z3::ult
expr ult(int a, expr const &b)
Definition: z3++.h:2130
z3::RTP
@ RTP
Definition: z3++.h:141
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_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.
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_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::unsat
@ unsat
Definition: z3++.h:135
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_bvxnor
Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise xnor.
z3::unknown
@ unknown
Definition: z3++.h:135
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_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::sle
expr sle(int a, expr const &b)
Definition: z3++.h:2098
z3::udiv
expr udiv(int a, expr const &b)
Definition: z3++.h:2148
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.
Microsoft.Z3.Z3_app
System.IntPtr Z3_app
Definition: NativeContext.cs:27
z3::context::recfun
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3533
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:2074
z3::select
expr select(expr const &a, int i)
Definition: z3++.h:3770
Z3_mk_bvurem
Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned remainder.
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_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_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_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_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_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_mul
Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point multiplication.
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::implies
expr implies(bool a, expr const &b)
Definition: z3++.h:1603
z3::store
expr store(expr const &a, expr_vector const &i, expr const &v)
Definition: z3++.h:3793
Z3_mk_bvor
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.
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_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::urem
expr urem(int a, expr const &b)
Definition: z3++.h:2169
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_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_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
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement addition.
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_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_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_mk_bvnot
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
z3::max
expr max(expr const &a, expr const &b)
Definition: z3++.h:1935
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_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_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_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_APP_AST
@ Z3_APP_AST
Definition: z3_api.h:141
Z3_mk_fpa_neg
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.
Z3_mk_seq_last_index
Z3_ast Z3_API Z3_mk_seq_last_index(Z3_context c, Z3_ast, Z3_ast substr)
Return index of the last occurrence of substr in s. If s does not contain substr, then the value is -...
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_mk_bvult
Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than.
Z3_mk_bvneg
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.
z3::check_context
void check_context(object const &a, object const &b)
Definition: z3++.h:455
Z3_mk_bvshl
Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2)
Shift left.
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_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::uge
expr uge(int a, expr const &b)
Definition: z3++.h:2136
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_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_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_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_bvlshr
Z3_ast Z3_API Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2)
Logical shift right.
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_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_fpa_round_to_integral
Z3_ast Z3_API Z3_mk_fpa_round_to_integral(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point roundToIntegral. Rounds a floating-point number to the closest integer,...
MK_EXPR2
#define MK_EXPR2(_fn, _arg1, _arg2)
Definition: z3++.h:3812
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_mk_gt
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
Microsoft.Z3.Z3_ast
System.IntPtr Z3_ast
Definition: NativeContext.cs:28
z3::to_func_decl
func_decl to_func_decl(context &c, Z3_func_decl f)
Definition: z3++.h:2088
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_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_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.
MK_EXPR1
#define MK_EXPR1(_fn, _arg)
Definition: z3++.h:3807
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::sat
@ sat
Definition: z3++.h:135
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_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_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_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::mod
expr mod(int a, expr const &b)
Definition: z3++.h:1619
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_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_bvand
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.
z3::RTZ
@ RTZ
Definition: z3++.h:143
Z3_mk_fpa_to_fp_signed
Z3_ast Z3_API Z3_mk_fpa_to_fp_signed(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.
Z3_mk_bvxor
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
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_const_array
Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v)
Create the constant array.
Z3_mk_fpa_geq
Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than or equal.
Z3_NUMERAL_AST
@ Z3_NUMERAL_AST
Definition: z3_api.h:140
z3::object::ctx
context & ctx() const
Definition: z3++.h:451
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_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_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 the first occurrence of substr in s starting from offset offset. If s does not contai...
Z3_mk_fpa_to_sbv
Z3_ast Z3_API Z3_mk_fpa_to_sbv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)
Conversion of a floating-point term into a signed bit-vector.
Z3_INT_SYMBOL
@ Z3_INT_SYMBOL
Definition: z3_api.h:75
Z3_mk_bvredor
Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1)
Take disjunction of bits in vector, return vector of length 1.
Z3_mk_xor
Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 xor t2.
z3::RNA
@ RNA
Definition: z3++.h:139
z3::RNE
@ RNE
Definition: z3++.h:140
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_fpa_sqrt
Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point square root.