Z3 |

Data Structures | Typedefs | Enumerations | Functions
z3 Namespace Reference

Z3 C++ namespace. More...

## Data Structures
class | apply_result
class | array
class | ast
class | ast_vector_tpl
class | cast_ast
class | cast_ast< ast >
class | cast_ast< expr >
class | cast_ast< func_decl >
class | cast_ast< sort >
class | config
| Z3 global configuration object. More...
class | context
| A Context manages all other Z3 objects, global configuration options, etc. More...
class | exception
| Exception used to sign API usage errors. More...
class | expr
| A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort Boolean. Every expression has a sort. More...
class | fixedpoint
class | func_decl
| Function declaration (aka function definition). It is the signature of interpreted and uninterpreted functions in Z3. The basic building block in Z3 is the function application. More...
class | func_entry
class | func_interp
class | goal
class | model
class | object
class | optimize
class | param_descrs
class | params
class | probe
class | scoped_context
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< ast > | ast_vector
typedef ast_vector_tpl< expr > | expr_vector
typedef ast_vector_tpl< sort > | sort_vector
typedef ast_vector_tpl< func_decl > | func_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)
std::ostream & | operator<< (std::ostream &out, model const &m)
std::ostream & | operator<< (std::ostream &out, stats const &s)
std::ostream & | operator<< (std::ostream &out, check_result r)
std::ostream & | operator<< (std::ostream &out, solver const &s)
std::ostream & | operator<< (std::ostream &out, goal const &g)
std::ostream & | operator<< (std::ostream &out, apply_result const &r)
tactic | operator& (tactic const &t1, tactic const &t2)
tactic | operator| (tactic const &t1, tactic const &t2)
tactic | repeat (tactic const &t, unsigned max=UINT_MAX)
tactic | with (tactic const &t, params const &p)
tactic | try_for (tactic const &t, unsigned ms)
tactic | par_or (unsigned n, tactic const *tactics)
tactic | par_and_then (tactic const &t1, tactic const &t2)
probe | operator<= (probe const &p1, probe const &p2)
probe | operator<= (probe const &p1, double p2)
probe | operator<= (double p1, probe const &p2)
probe | operator>= (probe const &p1, probe const &p2)
probe | operator>= (probe const &p1, double p2)
probe | operator>= (double p1, probe const &p2)
probe | operator< (probe const &p1, probe const &p2)
probe | operator< (probe const &p1, double p2)
probe | operator< (double p1, probe const &p2)
probe | operator> (probe const &p1, probe const &p2)
probe | operator> (probe const &p1, double p2)
probe | operator> (double p1, probe const &p2)
probe | operator== (probe const &p1, probe const &p2)
probe | operator== (probe const &p1, double p2)
probe | operator== (double p1, probe const &p2)
probe | operator&& (probe const &p1, probe const &p2)
probe | operator|| (probe const &p1, probe const &p2)
probe | operator! (probe const &p)
std::ostream & | operator<< (std::ostream &out, optimize const &s)
std::ostream & | operator<< (std::ostream &out, fixedpoint const &f)
tactic | fail_if (probe const &p)
tactic | when (probe const &p, tactic const &t)
tactic | cond (probe const &p, tactic const &t1, tactic const &t2)
expr | to_real (expr const &a)
func_decl | function (symbol const &name, unsigned arity, sort const *domain, sort const &range)
func_decl | function (char const *name, unsigned arity, sort const *domain, sort const &range)
func_decl | function (char const *name, sort const &domain, sort const &range)
func_decl | function (char const *name, sort const &d1, sort const &d2, sort const &range)
func_decl | function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &range)
func_decl | function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &d4, sort const &range)
func_decl | function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &d4, sort const &d5, sort const &range)
func_decl | function (char const *name, sort_vector const &domain, sort const &range)
func_decl | function (std::string const &name, sort_vector const &domain, sort const &range)
func_decl | recfun (symbol const &name, unsigned arity, sort const *domain, sort const &range)
func_decl | recfun (char const *name, unsigned arity, sort const *domain, sort const &range)
func_decl | recfun (char const *name, sort const &d1, sort const &range)
func_decl | recfun (char const *name, sort const &d1, sort const &d2, sort const &range)
expr | select (expr const &a, int i)
expr | store (expr const &a, expr const &i, expr const &v)
expr | store (expr const &a, int i, expr const &v)
expr | store (expr const &a, expr i, int v)
expr | store (expr const &a, int i, int v)
expr | store (expr const &a, expr_vector const &i, expr const &v)
expr | as_array (func_decl &f)
expr | const_array (sort const &d, expr const &v)
expr | empty_set (sort const &s)
expr | full_set (sort const &s)
expr | set_add (expr const &s, expr const &e)
expr | set_del (expr const &s, expr const &e)
expr | set_union (expr const &a, expr const &b)
expr | set_intersect (expr const &a, expr const &b)
expr | set_difference (expr const &a, expr const &b)
expr | set_complement (expr const &a)
expr | set_member (expr const &s, expr const &e)
expr | set_subset (expr const &a, expr const &b)
expr | empty (sort const &s)
expr | suffixof (expr const &a, expr const &b)
expr | prefixof (expr const &a, expr const &b)
expr | indexof (expr const &s, expr const &substr, expr const &offset)
expr | last_indexof (expr const &s, expr const &substr)
expr | to_re (expr const &s)
expr | in_re (expr const &s, expr const &re)
expr | plus (expr const &re)
expr | option (expr const &re)
expr | star (expr const &re)
expr | re_empty (sort const &s)
expr | re_full (sort const &s)
expr | re_intersect (expr_vector const &args)
expr | re_complement (expr const &a)
expr | range (expr const &lo, expr const &hi)

## Detailed Description

Z3 C++ namespace.

## Typedef Documentation

## ◆ ast_vector

typedef ast_vector_tpl<ast> ast_vector

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

## ◆ expr_vector

typedef ast_vector_tpl<expr> expr_vector

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

## ◆ func_decl_vector

typedef ast_vector_tpl<func_decl> func_decl_vector

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

## ◆ sort_vector

typedef ast_vector_tpl<sort> sort_vector

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

## Enumeration Type Documentation

## ◆ check_result

enum check_result

Enumerator
unsat |
sat |
unknown |

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

132 {
133 unsat, sat, unknown
134 };
z3::unknown
@ unknown
Definition: z3++.h:133
z3::sat
@ sat
Definition: z3++.h:133
z3::unsat
@ unsat
Definition: z3++.h:133

## ◆ rounding_mode

enum rounding_mode

Enumerator
RNA |
RNE |
RTP |
RTN |
RTZ |

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

136 {
137 RNA,
138 RNE,
139 RTP,
140 RTN,
141 RTZ
142 };
z3::RNE
@ RNE
Definition: z3++.h:138
z3::RNA
@ RNA
Definition: z3++.h:137
z3::RTZ
@ RTZ
Definition: z3++.h:141
z3::RTN
@ RTN
Definition: z3++.h:140
z3::RTP
@ RTP
Definition: z3++.h:139

## Function Documentation

## ◆ abs()

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

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

1863 {
1864 Z3_ast r;
1865 if (a.is_int()) {
1866 expr zero = a.ctx().int_val(0);
1867 r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
1868 }
1869 else if (a.is_real()) {
1870 expr zero = a.ctx().real_val(0);
1871 r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
1872 }
1873 else {
1874 r = Z3_mk_fpa_abs(a.ctx(), a);
1875 }
1876 a.check_error();
1877 return expr(a.ctx(), r);
1878 }
z3::context::real_val
expr real_val(int n, int d)
Definition: z3++.h:3396
z3::context::int_val
expr int_val(int n)
Definition: z3++.h:3390
z3::expr
A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort ...
Definition: z3++.h:757
z3::object::ctx
context & ctx() const
Definition: z3++.h:422
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_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_abs
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.

## ◆ as_array()

expr z3::as_array | ( | func_decl & | f | ) |
| inline

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

3587 {
3588 Z3_ast r = Z3_mk_as_array(f.ctx(), f);
3589 f.check_error();
3590 return expr(f.ctx(), r);
3591 }
z3::object::check_error
Z3_error_code check_error() const
Definition: z3++.h:423
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...

## ◆ ashr() [1/3]

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

arithmetic shift right operator for bitvectors

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

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

Referenced by ashr().

## ◆ ashr() [2/3]

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

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

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

## ◆ ashr() [3/3]

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

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

2087{ 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 2294 of file z3++.h.

2294 {
2295 assert(es.size() > 0);
2296 context& ctx = es[0].ctx();
2297 array<Z3_ast> _es(es);
2298 Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
2299 ctx.check_error();
2300 return expr(ctx, r);
2301 }
z3::array
Definition: z3++.h:400
z3::context
A Context manages all other Z3 objects, global configuration options, etc.
Definition: z3++.h:156
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition: z3++.h:188
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.

## ◆ atmost()

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

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

2286 {
2287 assert(es.size() > 0);
2288 context& ctx = es[0].ctx();
2289 array<Z3_ast> _es(es);
2290 Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
2291 ctx.check_error();
2292 return expr(ctx, r);
2293 }
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.

## ◆ bv2int()

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

bit-vector and integer conversions.

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

2097{ Z3_ast r = Z3_mk_bv2int(a.ctx(), a, is_signed); a.check_error(); return expr(a.ctx(), r); }
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...

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

2103 {
2104 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);
2105 }
z3::check_context
void check_context(object const &a, object const &b)
Definition: z3++.h:426
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.

## ◆ bvadd_no_underflow()

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

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

2106 {
2107 check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2108 }
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.

## ◆ bvmul_no_overflow()

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

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

2121 {
2122 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);
2123 }
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.

## ◆ bvmul_no_underflow()

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

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

2124 {
2125 check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2126 }
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...

## ◆ bvneg_no_overflow()

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

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

2118 {
2119 Z3_ast r = Z3_mk_bvneg_no_overflow(a.ctx(), a); a.check_error(); return expr(a.ctx(), r);
2120 }
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.

## ◆ bvredand()

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

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

1857 {
1858 assert(a.is_bv());
1859 Z3_ast r = Z3_mk_bvredor(a.ctx(), a);
1860 a.check_error();
1861 return expr(a.ctx(), r);
1862 }
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.

## ◆ bvredor()

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

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

1851 {
1852 assert(a.is_bv());
1853 Z3_ast r = Z3_mk_bvredor(a.ctx(), a);
1854 a.check_error();
1855 return expr(a.ctx(), r);
1856 }

## ◆ bvsdiv_no_overflow()

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

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

2115 {
2116 check_context(a, b); Z3_ast r = Z3_mk_bvsdiv_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2117 }
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.

## ◆ bvsub_no_overflow()

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

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

2109 {
2110 check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2111 }
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.

## ◆ bvsub_no_underflow()

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

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

2112 {
2113 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);
2114 }
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.

## ◆ check_context()

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

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

426{ (void)a; (void)b; assert(a.m_ctx == b.m_ctx); }

Referenced by cond(), exists(), forall(), context::function(), indexof(), lambda(), last_indexof(), prefixof(), context::recdef(), context::recfun(), select(), set_intersect(), set_union(), store(), suffixof(), and when().

## ◆ concat() [1/2]

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

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

2320 {
2321 check_context(a, b);
2322 Z3_ast r;
2323 if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
2324 Z3_ast _args[2] = { a, b };
2325 r = Z3_mk_seq_concat(a.ctx(), 2, _args);
2326 }
2327 else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
2328 Z3_ast _args[2] = { a, b };
2329 r = Z3_mk_re_concat(a.ctx(), 2, _args);
2330 }
2331 else {
2332 r = Z3_mk_concat(a.ctx(), a, b);
2333 }
2334 a.ctx().check_error();
2335 return expr(a.ctx(), r);
2336 }
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_seq_concat
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
Z3_mk_re_concat
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])
Create the concatenation of the regular languages.
Z3_mk_concat
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
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.

## ◆ concat() [2/2]

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

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

2338 {
2339 Z3_ast r;
2340 assert(args.size() > 0);
2341 if (args.size() == 1) {
2342 return args[0];
2343 }
2344 context& ctx = args[0].ctx();
2345 array<Z3_ast> _args(args);
2346 if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
2347 r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
2348 }
2349 else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
2350 r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
2351 }
2352 else {
2353 r = _args[args.size()-1];
2354 for (unsigned i = args.size()-1; i > 0; ) {
2355 --i;
2356 r = Z3_mk_concat(ctx, _args[i], r);
2357 ctx.check_error();
2358 }
2359 }
2360 ctx.check_error();
2361 return expr(ctx, r);
2362 }

## ◆ cond()

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

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

3187 {
3188 check_context(p, t1); check_context(p, t2);
3189 Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2);
3190 t1.check_error();
3191 return tactic(t1.ctx(), r);
3192 }
z3::tactic
Definition: z3++.h:2851
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...

## ◆ const_array()

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

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

3604 {
3605 MK_EXPR2(Z3_mk_const_array, d, v);
3606 }
MK_EXPR2
#define MK_EXPR2(_fn, _arg1, _arg2)
Definition: z3++.h:3598
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.

## ◆ distinct()

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

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

2311 {
2312 assert(args.size() > 0);
2313 context& ctx = args[0].ctx();
2314 array<Z3_ast> _args(args);
2315 Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
2316 ctx.check_error();
2317 return expr(ctx, r);
2318 }
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]).

## ◆ empty()

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

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

3660 {
3661 Z3_ast r = Z3_mk_seq_empty(s.ctx(), s);
3662 s.check_error();
3663 return expr(s.ctx(), r);
3664 }
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.

## ◆ empty_set()

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

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

3608 {
3609 MK_EXPR1(Z3_mk_empty_set, s);
3610 }
MK_EXPR1
#define MK_EXPR1(_fn, _arg)
Definition: z3++.h:3593
Z3_mk_empty_set
Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain)
Create the empty set.

## ◆ eq()

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

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

540{ return Z3_is_eq_ast(a.ctx(), a, b); }
Z3_is_eq_ast
bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2)
Compare terms.

## ◆ exists() [1/5]

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

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

2213 {
2214 check_context(x, b);
2215 Z3_app vars[] = {(Z3_app) x};
2216 Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2217 }
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.

## ◆ exists() [2/5]

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

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

2218 {
2219 check_context(x1, b); check_context(x2, b);
2220 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2221 Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2222 }

## ◆ exists() [3/5]

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

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

2223 {
2224 check_context(x1, b); check_context(x2, b); check_context(x3, b);
2225 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2226 Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2227 }

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

2228 {
2229 check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2230 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2231 Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2232 }

## ◆ exists() [5/5]

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

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

2233 {
2234 array<Z3_app> vars(xs);
2235 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);
2236 }

## ◆ fail_if()

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

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

3176 {
3177 Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
3178 p.check_error();
3179 return tactic(p.ctx(), r);
3180 }
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.

## ◆ fma()

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

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

1895 {
1896 check_context(a, b); check_context(a, c); check_context(a, rm);
1897 assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
1898 Z3_ast r = Z3_mk_fpa_fma(a.ctx(), rm, a, b, c);
1899 a.check_error();
1900 return expr(a.ctx(), r);
1901 }
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.

## ◆ forall() [1/5]

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

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

2189 {
2190 check_context(x, b);
2191 Z3_app vars[] = {(Z3_app) x};
2192 Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2193 }
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.

## ◆ forall() [2/5]

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

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

2194 {
2195 check_context(x1, b); check_context(x2, b);
2196 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2197 Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2198 }

## ◆ forall() [3/5]

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

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

2199 {
2200 check_context(x1, b); check_context(x2, b); check_context(x3, b);
2201 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2202 Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2203 }

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

2204 {
2205 check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2206 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2207 Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2208 }

## ◆ forall() [5/5]

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

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

2209 {
2210 array<Z3_app> vars(xs);
2211 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);
2212 }

## ◆ fp_eq()

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

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

1886 {
1887 check_context(a, b);
1888 assert(a.is_fpa());
1889 Z3_ast r = Z3_mk_fpa_eq(a.ctx(), a, b);
1890 a.check_error();
1891 return expr(a.ctx(), r);
1892 }
Z3_mk_fpa_eq
Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point equality.

## ◆ fpa_fp()

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

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

1903 {
1904 check_context(sgn, exp); check_context(exp, sig);
1905 assert(sgn.is_bv() && exp.is_bv() && sig.is_bv());
1906 Z3_ast r = Z3_mk_fpa_fp(sgn.ctx(), sgn, exp, sig);
1907 sgn.check_error();
1908 return expr(sgn.ctx(), r);
1909 }
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.

## ◆ fpa_to_fpa()

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

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

1939 {
1940 assert(t.is_fpa());
1941 Z3_ast r = Z3_mk_fpa_to_fp_float(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
1942 t.check_error();
1943 return expr(t.ctx(), r);
1944 }
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.

## ◆ fpa_to_sbv()

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

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

1911 {
1912 assert(t.is_fpa());
1913 Z3_ast r = Z3_mk_fpa_to_sbv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
1914 t.check_error();
1915 return expr(t.ctx(), r);
1916 }
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.

## ◆ fpa_to_ubv()

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

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

1918 {
1919 assert(t.is_fpa());
1920 Z3_ast r = Z3_mk_fpa_to_ubv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
1921 t.check_error();
1922 return expr(t.ctx(), r);
1923 }
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.

## ◆ full_set()

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

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

3612 {
3613 MK_EXPR1(Z3_mk_full_set, s);
3614 }
Z3_mk_full_set
Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain)
Create the full set.

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

3527 {
3528 return range.ctx().function(name, d1, d2, d3, d4, d5, range);
3529 }
z3::context::function
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3257
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3725

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

3524 {
3525 return range.ctx().function(name, d1, d2, d3, d4, range);
3526 }

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

3521 {
3522 return range.ctx().function(name, d1, d2, d3, range);
3523 }

## ◆ function() [4/9]

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

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

3518 {
3519 return range.ctx().function(name, d1, d2, range);
3520 }

## ◆ function() [5/9]

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

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

3515 {
3516 return range.ctx().function(name, domain, range);
3517 }

## ◆ function() [6/9]

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

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

3530 {
3531 return range.ctx().function(name, domain, range);
3532 }

## ◆ function() [7/9]

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

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

3512 {
3513 return range.ctx().function(name, arity, domain, range);
3514 }

## ◆ function() [8/9]

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

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

3533 {
3534 return range.ctx().function(name.c_str(), domain, range);
3535 }

## ◆ function() [9/9]

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

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

3509 {
3510 return range.ctx().function(name, arity, domain, range);
3511 }

## ◆ implies() [1/3]

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

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

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

## ◆ implies() [2/3]

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

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

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

## ◆ implies() [3/3]

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

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

1499 {
1500 assert(a.is_bool() && b.is_bool());
1501 _Z3_MK_BIN_(a, b, Z3_mk_implies);
1502 }
_Z3_MK_BIN_
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1492
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.

## ◆ in_re()

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

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

3692 {
3693 MK_EXPR2(Z3_mk_seq_in_re, s, re);
3694 }
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.

## ◆ indexof()

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

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

3677 {
3678 check_context(s, substr); check_context(s, offset);
3679 Z3_ast r = Z3_mk_seq_index(s.ctx(), s, substr, offset);
3680 s.check_error();
3681 return expr(s.ctx(), r);
3682 }
Z3_mk_seq_index
Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset)
Return index of first occurrence of substr in s starting from offset offset. If s does not contain su...

## ◆ int2bv()

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

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

2098{ Z3_ast r = Z3_mk_int2bv(a.ctx(), n, a); a.check_error(); return expr(a.ctx(), r); }
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.

## ◆ is_int()

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

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

1547{ _Z3_MK_UN_(e, Z3_mk_is_int); }
_Z3_MK_UN_
#define _Z3_MK_UN_(a, mkun)
Definition: z3++.h:1539
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.

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

1958 {
1959 check_context(c, t); check_context(c, e);
1960 assert(c.is_bool());
1961 Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
1962 c.check_error();
1963 return expr(c.ctx(), r);
1964 }

## ◆ lambda() [1/5]

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

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

2237 {
2238 check_context(x, b);
2239 Z3_app vars[] = {(Z3_app) x};
2240 Z3_ast r = Z3_mk_lambda_const(b.ctx(), 1, vars, b); b.check_error(); return expr(b.ctx(), r);
2241 }
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.

## ◆ lambda() [2/5]

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

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

2242 {
2243 check_context(x1, b); check_context(x2, b);
2244 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2245 Z3_ast r = Z3_mk_lambda_const(b.ctx(), 2, vars, b); b.check_error(); return expr(b.ctx(), r);
2246 }

## ◆ lambda() [3/5]

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

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

2247 {
2248 check_context(x1, b); check_context(x2, b); check_context(x3, b);
2249 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2250 Z3_ast r = Z3_mk_lambda_const(b.ctx(), 3, vars, b); b.check_error(); return expr(b.ctx(), r);
2251 }

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

2252 {
2253 check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2254 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2255 Z3_ast r = Z3_mk_lambda_const(b.ctx(), 4, vars, b); b.check_error(); return expr(b.ctx(), r);
2256 }

## ◆ lambda() [5/5]

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

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

2257 {
2258 array<Z3_app> vars(xs);
2259 Z3_ast r = Z3_mk_lambda_const(b.ctx(), vars.size(), vars.ptr(), b); b.check_error(); return expr(b.ctx(), r);
2260 }

## ◆ last_indexof()

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

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

3683 {
3684 check_context(s, substr);
3685 Z3_ast r = Z3_mk_seq_last_index(s.ctx(), s, substr);
3686 s.check_error();
3687 return expr(s.ctx(), r);
3688 }
Z3_mk_seq_last_index
Z3_ast Z3_API Z3_mk_seq_last_index(Z3_context c, Z3_ast, Z3_ast substr)
Return the last occurrence of substr in s. If s does not contain substr, then the value is -1,...

## ◆ linear_order()

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

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

2134 {
2135 return to_func_decl(a.ctx(), Z3_mk_linear_order(a.ctx(), a, index));
2136 }
z3::to_func_decl
func_decl to_func_decl(context &c, Z3_func_decl f)
Definition: z3++.h:1985
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.

## ◆ lshr() [1/3]

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

logic shift right operator for bitvectors

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

2078{ return to_expr(a.ctx(), Z3_mk_bvlshr(a.ctx(), a, b)); }
Z3_mk_bvlshr
Z3_ast Z3_API Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2)
Logical shift right.

Referenced by lshr().

## ◆ lshr() [2/3]

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

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

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

## ◆ lshr() [3/3]

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

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

2080{ 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 1836 of file z3++.h.

1836 {
1837 check_context(a, b);
1838 Z3_ast r;
1839 if (a.is_arith()) {
1840 r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), a, b);
1841 }
1842 else if (a.is_bv()) {
1843 r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), a, b);
1844 }
1845 else {
1846 assert(a.is_fpa());
1847 r = Z3_mk_fpa_max(a.ctx(), a, b);
1848 }
1849 return expr(a.ctx(), r);
1850 }
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_fpa_max
Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2)
Maximum of floating-point numbers.

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

## ◆ min()

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

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

1821 {
1822 check_context(a, b);
1823 Z3_ast r;
1824 if (a.is_arith()) {
1825 r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), b, a);
1826 }
1827 else if (a.is_bv()) {
1828 r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), b, a);
1829 }
1830 else {
1831 assert(a.is_fpa());
1832 r = Z3_mk_fpa_min(a.ctx(), a, b);
1833 }
1834 return expr(a.ctx(), r);
1835 }
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.

## ◆ mk_and()

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

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

2370 {
2371 array<Z3_ast> _args(args);
2372 Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2373 args.check_error();
2374 return expr(args.ctx(), r);
2375 }
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].

## ◆ mk_or()

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

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

2364 {
2365 array<Z3_ast> _args(args);
2366 Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2367 args.check_error();
2368 return expr(args.ctx(), r);
2369 }
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].

## ◆ mod() [1/3]

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

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

1511 {
1512 if (a.is_bv()) {
1513 _Z3_MK_BIN_(a, b, Z3_mk_bvsmod);
1514 }
1515 else {
1516 _Z3_MK_BIN_(a, b, Z3_mk_mod);
1517 }
1518 }
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_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).

Referenced by operator%().

## ◆ mod() [2/3]

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

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

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

## ◆ mod() [3/3]

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

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

1520{ 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 1818 of file z3++.h.

1818{ 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); }
Z3_mk_bvnand
Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nand.

## ◆ nor()

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

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

1819{ 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); }
Z3_mk_bvnor
Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nor.

## ◆ operator!() [1/2]

expr z3::operator! | ( | expr const & | a | ) |
| inline

Precondition
  a.is_bool()

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

1545{ assert(a.is_bool()); _Z3_MK_UN_(a, Z3_mk_not); }
Z3_mk_not
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).

## ◆ operator!() [2/2]

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

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

3010 {
3011 Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
3012 }
z3::probe
Definition: z3++.h:2937
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.

## ◆ operator!=() [1/5]

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

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

1597{ 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 1596 of file z3++.h.

1596{ 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 1587 of file z3++.h.

1587 {
1588 check_context(a, b);
1589 Z3_ast args[2] = { a, b };
1590 Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1591 a.check_error();
1592 return expr(a.ctx(), r);
1593 }

## ◆ operator!=() [4/5]

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

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

1594{ 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 1595 of file z3++.h.

1595{ 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 1522 of file z3++.h.

1522{ return mod(a, b); }

## ◆ operator%() [2/3]

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

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

1523{ return mod(a, b); }

## ◆ operator%() [3/3]

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

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

1524{ return mod(a, b); }

## ◆ operator&() [1/4]

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

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

1806{ 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); }
Z3_mk_bvand
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.

## ◆ operator&() [2/4]

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

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

1807{ 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 1808 of file z3++.h.

1808{ 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 2891 of file z3++.h.

2891 {
2892 check_context(t1, t2);
2893 Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
2894 t1.check_error();
2895 return tactic(t1.ctx(), r);
2896 }
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.

## ◆ operator&&() [1/4]

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

Precondition
  b.is_bool()

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

1561{ 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 1560 of file z3++.h.

1560{ 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 1551 of file z3++.h.

1551 {
1552 check_context(a, b);
1553 assert(a.is_bool() && b.is_bool());
1554 Z3_ast args[2] = { a, b };
1555 Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
1556 a.check_error();
1557 return expr(a.ctx(), r);
1558 }

## ◆ operator&&() [4/4]

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

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

3004 {
3005 check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3006 }
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.

## ◆ operator*() [1/3]

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

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

1629 {
1630 check_context(a, b);
1631 Z3_ast r = 0;
1632 if (a.is_arith() && b.is_arith()) {
1633 Z3_ast args[2] = { a, b };
1634 r = Z3_mk_mul(a.ctx(), 2, args);
1635 }
1636 else if (a.is_bv() && b.is_bv()) {
1637 r = Z3_mk_bvmul(a.ctx(), a, b);
1638 }
1639 else if (a.is_fpa() && b.is_fpa()) {
1640 r = Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1641 }
1642 else {
1643 // operator is not supported by given arguments.
1644 assert(false);
1645 }
1646 a.check_error();
1647 return expr(a.ctx(), r);
1648 }
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_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_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.

## ◆ operator*() [2/3]

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

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

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

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

1599 {
1600 check_context(a, b);
1601 Z3_ast r = 0;
1602 if (a.is_arith() && b.is_arith()) {
1603 Z3_ast args[2] = { a, b };
1604 r = Z3_mk_add(a.ctx(), 2, args);
1605 }
1606 else if (a.is_bv() && b.is_bv()) {
1607 r = Z3_mk_bvadd(a.ctx(), a, b);
1608 }
1609 else if (a.is_seq() && b.is_seq()) {
1610 return concat(a, b);
1611 }
1612 else if (a.is_re() && b.is_re()) {
1613 Z3_ast _args[2] = { a, b };
1614 r = Z3_mk_re_union(a.ctx(), 2, _args);
1615 }
1616 else if (a.is_fpa() && b.is_fpa()) {
1617 r = Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1618 }
1619 else {
1620 // operator is not supported by given arguments.
1621 assert(false);
1622 }
1623 a.check_error();
1624 return expr(a.ctx(), r);
1625 }
z3::concat
expr concat(expr_vector const &args)
Definition: z3++.h:2338
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_bvadd
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement addition.
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_add
Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point addition.

## ◆ operator+() [2/3]

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

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

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

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

## ◆ operator-() [1/4]

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

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

1695 {
1696 Z3_ast r = 0;
1697 if (a.is_arith()) {
1698 r = Z3_mk_unary_minus(a.ctx(), a);
1699 }
1700 else if (a.is_bv()) {
1701 r = Z3_mk_bvneg(a.ctx(), a);
1702 }
1703 else if (a.is_fpa()) {
1704 r = Z3_mk_fpa_neg(a.ctx(), a);
1705 }
1706 else {
1707 // operator is not supported by given arguments.
1708 assert(false);
1709 }
1710 a.check_error();
1711 return expr(a.ctx(), r);
1712 }
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_bvneg
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.
Z3_mk_fpa_neg
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.

## ◆ operator-() [2/4]

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

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

1714 {
1715 check_context(a, b);
1716 Z3_ast r = 0;
1717 if (a.is_arith() && b.is_arith()) {
1718 Z3_ast args[2] = { a, b };
1719 r = Z3_mk_sub(a.ctx(), 2, args);
1720 }
1721 else if (a.is_bv() && b.is_bv()) {
1722 r = Z3_mk_bvsub(a.ctx(), a, b);
1723 }
1724 else if (a.is_fpa() && b.is_fpa()) {
1725 r = Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1726 }
1727 else {
1728 // operator is not supported by given arguments.
1729 assert(false);
1730 }
1731 a.check_error();
1732 return expr(a.ctx(), r);
1733 }
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_sub
Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] - ... - args[num_args - 1].
Z3_mk_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.

## ◆ operator-() [3/4]

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

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

1734{ 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 1735 of file z3++.h.

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

1673 {
1674 check_context(a, b);
1675 Z3_ast r = 0;
1676 if (a.is_arith() && b.is_arith()) {
1677 r = Z3_mk_div(a.ctx(), a, b);
1678 }
1679 else if (a.is_bv() && b.is_bv()) {
1680 r = Z3_mk_bvsdiv(a.ctx(), a, b);
1681 }
1682 else if (a.is_fpa() && b.is_fpa()) {
1683 r = Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1684 }
1685 else {
1686 // operator is not supported by given arguments.
1687 assert(false);
1688 }
1689 a.check_error();
1690 return expr(a.ctx(), r);
1691 }
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_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_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.

## ◆ operator/() [2/3]

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

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

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

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

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

## ◆ operator<() [2/6]

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

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

1762 {
1763 check_context(a, b);
1764 Z3_ast r = 0;
1765 if (a.is_arith() && b.is_arith()) {
1766 r = Z3_mk_lt(a.ctx(), a, b);
1767 }
1768 else if (a.is_bv() && b.is_bv()) {
1769 r = Z3_mk_bvslt(a.ctx(), a, b);
1770 }
1771 else if (a.is_fpa() && b.is_fpa()) {
1772 r = Z3_mk_fpa_lt(a.ctx(), a, b);
1773 }
1774 else {
1775 // operator is not supported by given arguments.
1776 assert(false);
1777 }
1778 a.check_error();
1779 return expr(a.ctx(), r);
1780 }
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_lt
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
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.

## ◆ operator<() [3/6]

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

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

1781{ 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 1782 of file z3++.h.

1782{ 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 2992 of file z3++.h.

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

## ◆ operator<() [6/6]

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

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

2989 {
2990 check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2991 }
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...

## ◆ operator<<() [1/13]

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

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

2849{ out << Z3_apply_result_to_string(r.ctx(), r); return out; }
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.

## ◆ operator<<() [2/13]

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

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

536 {
537 out << Z3_ast_to_string(n.ctx(), n.m_ast); return out;
538 }
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.

## ◆ operator<<() [3/13]

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

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

2544 {
2545 if (r == unsat) out << "unsat";
2546 else if (r == sat) out << "sat";
2547 else out << "unknown";
2548 return out;
2549 }

## ◆ operator<<() [4/13]

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

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

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

## ◆ operator<<() [5/13]

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

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

3174{ return out << Z3_fixedpoint_to_string(f.ctx(), f, 0, 0); }
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.

## ◆ operator<<() [6/13]

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

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

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

## ◆ operator<<() [7/13]

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

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

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

## ◆ operator<<() [8/13]

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

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

3116{ out << Z3_optimize_to_string(s.ctx(), s.m_opt); return out; }
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.

## ◆ operator<<() [9/13]

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

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

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

## ◆ operator<<() [10/13]

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

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

494 {
495 out << Z3_params_to_string(p.ctx(), p); return out;
496 }
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...

## ◆ operator<<() [11/13]

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

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

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

## ◆ operator<<() [12/13]

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

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

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

## ◆ operator<<() [13/13]

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

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

439 {
440 if (s.kind() == Z3_INT_SYMBOL)
441 out << "k!" << s.to_int();
442 else
443 out << s.str();
444 return out;
445 }
Z3_INT_SYMBOL
@ Z3_INT_SYMBOL
Definition: z3_api.h:117

## ◆ operator<=() [1/6]

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

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

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

## ◆ operator<=() [2/6]

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

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

1737 {
1738 check_context(a, b);
1739 Z3_ast r = 0;
1740 if (a.is_arith() && b.is_arith()) {
1741 r = Z3_mk_le(a.ctx(), a, b);
1742 }
1743 else if (a.is_bv() && b.is_bv()) {
1744 r = Z3_mk_bvsle(a.ctx(), a, b);
1745 }
1746 else if (a.is_fpa() && b.is_fpa()) {
1747 r = Z3_mk_fpa_leq(a.ctx(), a, b);
1748 }
1749 else {
1750 // operator is not supported by given arguments.
1751 assert(false);
1752 }
1753 a.check_error();
1754 return expr(a.ctx(), r);
1755 }
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_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_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.

## ◆ operator<=() [3/6]

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

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

1756{ 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 1757 of file z3++.h.

1757{ 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 2982 of file z3++.h.

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

## ◆ operator<=() [6/6]

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

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

2979 {
2980 check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2981 }
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...

## ◆ operator==() [1/8]

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

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

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

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

## ◆ operator==() [3/8]

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

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

1584{ 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 1576 of file z3++.h.

1576 {
1577 check_context(a, b);
1578 Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1579 a.check_error();
1580 return expr(a.ctx(), r);
1581 }
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.

## ◆ operator==() [5/8]

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

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

1582{ 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 1583 of file z3++.h.

1583{ 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 3002 of file z3++.h.

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

## ◆ operator==() [8/8]

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

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

2999 {
3000 check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3001 }
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 ...

## ◆ operator>() [1/6]

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

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

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

## ◆ operator>() [2/6]

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

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

1784 {
1785 check_context(a, b);
1786 Z3_ast r = 0;
1787 if (a.is_arith() && b.is_arith()) {
1788 r = Z3_mk_gt(a.ctx(), a, b);
1789 }
1790 else if (a.is_bv() && b.is_bv()) {
1791 r = Z3_mk_bvsgt(a.ctx(), a, b);
1792 }
1793 else if (a.is_fpa() && b.is_fpa()) {
1794 r = Z3_mk_fpa_gt(a.ctx(), a, b);
1795 }
1796 else {
1797 // operator is not supported by given arguments.
1798 assert(false);
1799 }
1800 a.check_error();
1801 return expr(a.ctx(), r);
1802 }
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_gt
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
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.

## ◆ operator>() [3/6]

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

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

1803{ 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 1804 of file z3++.h.

1804{ 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 2997 of file z3++.h.

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

## ◆ operator>() [6/6]

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

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

2994 {
2995 check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2996 }
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...

## ◆ operator>=() [1/6]

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

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

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

## ◆ operator>=() [2/6]

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

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

1653 {
1654 check_context(a, b);
1655 Z3_ast r = 0;
1656 if (a.is_arith() && b.is_arith()) {
1657 r = Z3_mk_ge(a.ctx(), a, b);
1658 }
1659 else if (a.is_bv() && b.is_bv()) {
1660 r = Z3_mk_bvsge(a.ctx(), a, b);
1661 }
1662 else if (a.is_fpa() && b.is_fpa()) {
1663 r = Z3_mk_fpa_geq(a.ctx(), a, b);
1664 }
1665 else {
1666 // operator is not supported by given arguments.
1667 assert(false);
1668 }
1669 a.check_error();
1670 return expr(a.ctx(), r);
1671 }
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_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.

## ◆ operator>=() [3/6]

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

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

1759{ 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 1760 of file z3++.h.

1760{ 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 2987 of file z3++.h.

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

## ◆ operator>=() [6/6]

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

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

2984 {
2985 check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
2986 }
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...

## ◆ operator^() [1/3]

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

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

1810{ 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); }
Z3_mk_bvxor
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
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.

## ◆ operator^() [2/3]

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

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

1811{ 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 1812 of file z3++.h.

1812{ 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 1814 of file z3++.h.

1814{ 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); }
Z3_mk_bvor
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.

## ◆ operator|() [2/4]

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

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

1815{ 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 1816 of file z3++.h.

1816{ 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 2898 of file z3++.h.

2898 {
2899 check_context(t1, t2);
2900 Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
2901 t1.check_error();
2902 return tactic(t1.ctx(), r);
2903 }
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...

## ◆ operator||() [1/4]

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

Precondition
  b.is_bool()

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

1574{ 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 1572 of file z3++.h.

1572{ 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 1563 of file z3++.h.

1563 {
1564 check_context(a, b);
1565 assert(a.is_bool() && b.is_bool());
1566 Z3_ast args[2] = { a, b };
1567 Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1568 a.check_error();
1569 return expr(a.ctx(), r);
1570 }

## ◆ operator||() [4/4]

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

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

3007 {
3008 check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3009 }
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.

## ◆ operator~()

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

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

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

## ◆ option()

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

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

3698 {
3699 MK_EXPR1(Z3_mk_re_option, re);
3700 }
Z3_mk_re_option
Z3_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re)
Create the regular language [re].

## ◆ par_and_then()

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

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

2930 {
2931 check_context(t1, t2);
2932 Z3_tactic r = Z3_tactic_par_and_then(t1.ctx(), t1, t2);
2933 t1.check_error();
2934 return tactic(t1.ctx(), r);
2935 }
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....

## ◆ par_or()

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

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

2921 {
2922 if (n == 0) {
2923 Z3_THROW(exception("a non-zero number of tactics need to be passed to par_or"));
2924 }
2925 array<Z3_tactic> buffer(n);
2926 for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];
2927 return tactic(tactics[0].ctx(), Z3_tactic_par_or(tactics[0].ctx(), n, buffer.ptr()));
2928 }
z3::exception
Exception used to sign API usage errors.
Definition: z3++.h:85
z3py.tactics
def tactics(ctx=None)
Definition: z3py.py:8323
Z3_THROW
#define Z3_THROW(x)
Definition: z3++.h:100
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.

## ◆ partial_order()

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

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

2137 {
2138 return to_func_decl(a.ctx(), Z3_mk_partial_order(a.ctx(), a, index));
2139 }
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.

## ◆ pbeq()

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

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

2278 {
2279 assert(es.size() > 0);
2280 context& ctx = es[0].ctx();
2281 array<Z3_ast> _es(es);
2282 Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
2283 ctx.check_error();
2284 return expr(ctx, r);
2285 }
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.

## ◆ pbge()

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

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

2270 {
2271 assert(es.size() > 0);
2272 context& ctx = es[0].ctx();
2273 array<Z3_ast> _es(es);
2274 Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
2275 ctx.check_error();
2276 return expr(ctx, r);
2277 }
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.

## ◆ pble()

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

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

2262 {
2263 assert(es.size() > 0);
2264 context& ctx = es[0].ctx();
2265 array<Z3_ast> _es(es);
2266 Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
2267 ctx.check_error();
2268 return expr(ctx, r);
2269 }
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.

## ◆ piecewise_linear_order()

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

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

2140 {
2141 return to_func_decl(a.ctx(), Z3_mk_piecewise_linear_order(a.ctx(), a, index));
2142 }
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.

## ◆ plus()

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

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

3695 {
3696 MK_EXPR1(Z3_mk_re_plus, re);
3697 }
Z3_mk_re_plus
Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re)
Create the regular language re+.

## ◆ prefixof()

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

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

3671 {
3672 check_context(a, b);
3673 Z3_ast r = Z3_mk_seq_prefix(a.ctx(), a, b);
3674 a.check_error();
3675 return expr(a.ctx(), r);
3676 }
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.

## ◆ pw() [1/3]

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

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

1507{ _Z3_MK_BIN_(a, b, Z3_mk_power); }
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.

## ◆ pw() [2/3]

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

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

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

## ◆ pw() [3/3]

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

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

1509{ 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 3725 of file z3++.h.

3725 {
3726 check_context(lo, hi);
3727 Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
3728 lo.check_error();
3729 return expr(lo.ctx(), r);
3730 }
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.

Referenced by AstVector::__getitem__(), z3py::AndThen(), z3py::ArraySort(), Goal::as_expr(), ApplyResult::as_expr(), FuncEntry::as_list(), FuncInterp::as_list(), 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(), z3py::Function(), context::function(), function(), Statistics::get_key_value(), z3py::Intersect(), z3py::IntVector(), z3py::is_quantifier(), Statistics::keys(), z3py::Lambda(), Context::MkArrayConst(), Context::MkArraySort(), Context::MkConst(), Context::MkConstDecl(), Context::MkFreshConst(), Context::MkFreshConstDecl(), Context::MkFreshFuncDecl(), Context::MkFuncDecl(), Context::MkRecFuncDecl(), z3py::OrElse(), z3py::ParOr(), z3py::probes(), UserPropagateBase::propagate(), z3py::RealVarVector(), z3py::RealVector(), z3py::RecAddDefinition(), context::recfun(), recfun(), z3py::RecFunction(), AstVector::resize(), z3py::set_default_fp_sort(), Fixedpoint::set_predicate_representation(), ModelRef::sorts(), z3py::substitute(), z3py::substitute_vars(), z3py::tactics(), Solver::to_smt2(), z3py::TupleSort(), z3py::Union(), and z3py::Update().

## ◆ re_complement()

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

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

3722 {
3723 MK_EXPR1(Z3_mk_re_complement, a);
3724 }
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.

## ◆ re_empty()

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

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

3704 {
3705 Z3_ast r = Z3_mk_re_empty(s.ctx(), s);
3706 s.check_error();
3707 return expr(s.ctx(), r);
3708 }
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.

## ◆ re_full()

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

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

3709 {
3710 Z3_ast r = Z3_mk_re_full(s.ctx(), s);
3711 s.check_error();
3712 return expr(s.ctx(), r);
3713 }
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.

## ◆ re_intersect()

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

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

3714 {
3715 assert(args.size() > 0);
3716 context& ctx = args[0].ctx();
3717 array<Z3_ast> _args(args);
3718 Z3_ast r = Z3_mk_re_intersect(ctx, _args.size(), _args.ptr());
3719 ctx.check_error();
3720 return expr(ctx, r);
3721 }
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.

## ◆ recfun() [1/4]

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

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

3546 {
3547 return range.ctx().recfun(name, d1, d2, range);
3548 }
z3::context::recfun
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition: z3++.h:3328

## ◆ recfun() [2/4]

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

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

3543 {
3544 return range.ctx().recfun(name, d1, range);
3545 }

## ◆ recfun() [3/4]

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

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

3540 {
3541 return range.ctx().recfun(name, arity, domain, range);
3542 }

## ◆ recfun() [4/4]

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

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

3537 {
3538 return range.ctx().recfun(name, arity, domain, range);
3539 }

## ◆ rem() [1/3]

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

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

1527 {
1528 if (a.is_fpa() && b.is_fpa()) {
1529 _Z3_MK_BIN_(a, b, Z3_mk_fpa_rem);
1530 } else {
1531 _Z3_MK_BIN_(a, b, Z3_mk_rem);
1532 }
1533 }
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_rem
Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point remainder.

## ◆ rem() [2/3]

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

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

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

## ◆ rem() [3/3]

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

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

1535{ 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 2905 of file z3++.h.

2905 {
2906 Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
2907 t.check_error();
2908 return tactic(t.ctx(), r);
2909 }
z3::max
expr max(expr const &a, expr const &b)
Definition: z3++.h:1836
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...

## ◆ reset_params()

void z3::reset_params | ( |  | ) |
| inline

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

80{ Z3_global_param_reset_all(); }
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...

## ◆ round_fpa_to_closest_integer()

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

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

1946 {
1947 assert(t.is_fpa());
1948 Z3_ast r = Z3_mk_fpa_round_to_integral(t.ctx(), t.ctx().fpa_rounding_mode(), t);
1949 t.check_error();
1950 return expr(t.ctx(), r);
1951 }
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,...

## ◆ sbv_to_fpa()

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

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

1925 {
1926 assert(t.is_bv());
1927 Z3_ast r = Z3_mk_fpa_to_fp_signed(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
1928 t.check_error();
1929 return expr(t.ctx(), r);
1930 }
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.

## ◆ select() [1/3]

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

forward declarations

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

3550 {
3551 check_context(a, i);
3552 Z3_ast r = Z3_mk_select(a.ctx(), a, i);
3553 a.check_error();
3554 return expr(a.ctx(), r);
3555 }
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.

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

## ◆ select() [2/3]

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

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

3559 {
3560 check_context(a, i);
3561 array<Z3_ast> idxs(i);
3562 Z3_ast r = Z3_mk_select_n(a.ctx(), a, idxs.size(), idxs.ptr());
3563 a.check_error();
3564 return expr(a.ctx(), r);
3565 }
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.

## ◆ select() [3/3]

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

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

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

## ◆ set_add()

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

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

3616 {
3617 MK_EXPR2(Z3_mk_set_add, s, e);
3618 }
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.

## ◆ set_complement()

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

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

3644 {
3645 MK_EXPR1(Z3_mk_set_complement, a);
3646 }
Z3_mk_set_complement
Z3_ast Z3_API Z3_mk_set_complement(Z3_context c, Z3_ast arg)
Take the complement of a set.

## ◆ set_del()

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

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

3620 {
3621 MK_EXPR2(Z3_mk_set_del, s, e);
3622 }
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.

## ◆ set_difference()

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

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

3640 {
3641 MK_EXPR2(Z3_mk_set_difference, a, b);
3642 }
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.

## ◆ set_intersect()

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

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

3632 {
3633 check_context(a, b);
3634 Z3_ast es[2] = { a, b };
3635 Z3_ast r = Z3_mk_set_intersect(a.ctx(), 2, es);
3636 a.check_error();
3637 return expr(a.ctx(), r);
3638 }
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.

## ◆ set_member()

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

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

3648 {
3649 MK_EXPR2(Z3_mk_set_member, s, e);
3650 }
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.

## ◆ set_param() [1/3]

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

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

78{ Z3_global_param_set(param, value ? "true" : "false"); }
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.

## ◆ set_param() [2/3]

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

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

77{ Z3_global_param_set(param, value); }

## ◆ set_param() [3/3]

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

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

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

3652 {
3653 MK_EXPR2(Z3_mk_set_subset, a, b);
3654 }
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.

## ◆ set_union()

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

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

3624 {
3625 check_context(a, b);
3626 Z3_ast es[2] = { a, b };
3627 Z3_ast r = Z3_mk_set_union(a.ctx(), 2, es);
3628 a.check_error();
3629 return expr(a.ctx(), r);
3630 }
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.

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

2132{ return to_expr(a.ctx(), Z3_mk_sign_ext(a.ctx(), i, a)); }
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,...

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

2005{ 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 2006 of file z3++.h.

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

## ◆ sge() [3/3]

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

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

2007{ 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 2011 of file z3++.h.

2011{ 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 2012 of file z3++.h.

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

## ◆ sgt() [3/3]

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

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

2013{ 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 2071 of file z3++.h.

2071{ return to_expr(a.ctx(), Z3_mk_bvshl(a.ctx(), a, b)); }
Z3_mk_bvshl
Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2)
Shift left.

Referenced by shl().

## ◆ shl() [2/3]

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

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

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

## ◆ shl() [3/3]

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

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

2073{ 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 1993 of file z3++.h.

1993{ 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 1994 of file z3++.h.

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

## ◆ sle() [3/3]

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

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

1995{ 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 1999 of file z3++.h.

1999{ 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 2000 of file z3++.h.

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

## ◆ slt() [3/3]

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

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

2001{ 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 2057 of file z3++.h.

2057{ 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 2058 of file z3++.h.

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

## ◆ smod() [3/3]

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

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

2059{ 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 1879 of file z3++.h.

1879 {
1880 check_context(a, rm);
1881 assert(a.is_fpa());
1882 Z3_ast r = Z3_mk_fpa_sqrt(a.ctx(), rm, a);
1883 a.check_error();
1884 return expr(a.ctx(), r);
1885 }
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.

## ◆ srem() [1/3]

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

signed remainder operator for bitvectors

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

2050{ return to_expr(a.ctx(), Z3_mk_bvsrem(a.ctx(), a, b)); }
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).

Referenced by srem().

## ◆ srem() [2/3]

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

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

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

## ◆ srem() [3/3]

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

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

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

## ◆ star()

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

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

3701 {
3702 MK_EXPR1(Z3_mk_re_star, re);
3703 }
Z3_mk_re_star
Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re)
Create the regular language re*.

## ◆ store() [1/5]

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

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

3567 {
3568 check_context(a, i); check_context(a, v);
3569 Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
3570 a.check_error();
3571 return expr(a.ctx(), r);
3572 }
Z3_mk_store
Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v)
Array update.

Referenced by store().

## ◆ store() [2/5]

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

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

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

## ◆ store() [3/5]

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

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

3579 {
3580 check_context(a, i); check_context(a, v);
3581 array<Z3_ast> idxs(i);
3582 Z3_ast r = Z3_mk_store_n(a.ctx(), a, idxs.size(), idxs.ptr(), v);
3583 a.check_error();
3584 return expr(a.ctx(), r);
3585 }
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.

## ◆ store() [4/5]

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

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

3574{ 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 3576 of file z3++.h.

3576 {
3577 return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
3578 }

## ◆ suffixof()

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

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

3665 {
3666 check_context(a, b);
3667 Z3_ast r = Z3_mk_seq_suffix(a.ctx(), a, b);
3668 a.check_error();
3669 return expr(a.ctx(), r);
3670 }
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.

## ◆ sum()

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

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

2302 {
2303 assert(args.size() > 0);
2304 context& ctx = args[0].ctx();
2305 array<Z3_ast> _args(args);
2306 Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
2307 ctx.check_error();
2308 return expr(ctx, r);
2309 }

## ◆ to_check_result()

check_result z3::to_check_result | ( | Z3_lbool | l | ) |
| inline

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

144 {
145 if (l == Z3_L_TRUE) return sat;
146 else if (l == Z3_L_FALSE) return unsat;
147 return unknown;
148 }
Z3_L_TRUE
@ Z3_L_TRUE
Definition: z3_api.h:105
Z3_L_FALSE
@ Z3_L_FALSE
Definition: z3_api.h:103

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

1971 {
1972 c.check_error();
1973 assert(Z3_get_ast_kind(c, a) == Z3_APP_AST ||
1974 Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST ||
1975 Z3_get_ast_kind(c, a) == Z3_VAR_AST ||
1976 Z3_get_ast_kind(c, a) == Z3_QUANTIFIER_AST);
1977 return expr(c, a);
1978 }
Z3_APP_AST
@ Z3_APP_AST
Definition: z3_api.h:182
Z3_VAR_AST
@ Z3_VAR_AST
Definition: z3_api.h:183
Z3_NUMERAL_AST
@ Z3_NUMERAL_AST
Definition: z3_api.h:181
Z3_QUANTIFIER_AST
@ Z3_QUANTIFIER_AST
Definition: z3_api.h:184
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.

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

1985 {
1986 c.check_error();
1987 return func_decl(c, f);
1988 }
z3::func_decl
Function declaration (aka function definition). It is the signature of interpreted and uninterpreted ...
Definition: z3++.h:711

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

3689 {
3690 MK_EXPR1(Z3_mk_seq_to_re, s);
3691 }
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.

## ◆ to_real()

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

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

3507{ Z3_ast r = Z3_mk_int2real(a.ctx(), a); a.check_error(); return expr(a.ctx(), r); }
Z3_mk_int2real
Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1)
Coerce an integer to a real.

## ◆ to_sort()

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

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

1980 {
1981 c.check_error();
1982 return sort(c, s);
1983 }
z3::sort
A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort.
Definition: z3++.h:612

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

2143 {
2144 return to_func_decl(a.ctx(), Z3_mk_tree_order(a.ctx(), a, index));
2145 }
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.

## ◆ try_for()

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

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

2916 {
2917 Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
2918 t.check_error();
2919 return tactic(t.ctx(), r);
2920 }
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...

## ◆ ubv_to_fpa()

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

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

1932 {
1933 assert(t.is_bv());
1934 Z3_ast r = Z3_mk_fpa_to_fp_unsigned(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
1935 t.check_error();
1936 return expr(t.ctx(), r);
1937 }
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.

## ◆ udiv() [1/3]

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

unsigned division operator for bitvectors.

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

2043{ return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }
Z3_mk_bvudiv
Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned division.

Referenced by udiv().

## ◆ udiv() [2/3]

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

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

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

## ◆ udiv() [3/3]

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

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

2045{ 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 2031 of file z3++.h.

2031{ 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 2032 of file z3++.h.

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

## ◆ uge() [3/3]

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

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

2033{ 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 2037 of file z3++.h.

2037{ return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }
Z3_mk_bvugt
Z3_ast Z3_API Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than.

Referenced by ugt().

## ◆ ugt() [2/3]

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

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

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

## ◆ ugt() [3/3]

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

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

2039{ 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 2019 of file z3++.h.

2019{ return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }
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.

Referenced by ule().

## ◆ ule() [2/3]

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

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

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

## ◆ ule() [3/3]

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

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

2021{ 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 2025 of file z3++.h.

2025{ return to_expr(a.ctx(), Z3_mk_bvult(a.ctx(), a, b)); }
Z3_mk_bvult
Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than.

Referenced by ult().

## ◆ ult() [2/3]

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

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

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

## ◆ ult() [3/3]

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

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

2027{ 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 2064 of file z3++.h.

2064{ return to_expr(a.ctx(), Z3_mk_bvurem(a.ctx(), a, b)); }
Z3_mk_bvurem
Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned remainder.

Referenced by urem().

## ◆ urem() [2/3]

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

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

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

## ◆ urem() [3/3]

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

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

2066{ 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 3181 of file z3++.h.

3181 {
3182 check_context(p, t);
3183 Z3_tactic r = Z3_tactic_when(t.ctx(), p, t);
3184 t.check_error();
3185 return tactic(t.ctx(), r);
3186 }
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...

## ◆ with()

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

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

2911 {
2912 Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
2913 t.check_error();
2914 return tactic(t.ctx(), r);
2915 }
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.

## ◆ xnor()

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

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

1820{ 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); }
Z3_mk_bvxnor
Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise xnor.

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

2092{ return to_expr(a.ctx(), Z3_mk_zero_ext(a.ctx(), i, a)); }
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,...