Z3
 
Loading...
Searching...
No Matches
Data Structures | Typedefs | Enumerations | Functions
z3 Namespace Reference

Z3 C++ namespace. More...

Data Structures

class  apply_result
 
class  array
 
class  ast
 
class  ast_vector_tpl
 
class  cast_ast
 
class  cast_ast< ast >
 
class  cast_ast< expr >
 
class  cast_ast< func_decl >
 
class  cast_ast< sort >
 
class  config
 Z3 global configuration object. More...
 
class  constructor_list
 
class  constructors
 
class  context
 A Context manages all other Z3 objects, global configuration options, etc. More...
 
class  exception
 Exception used to sign API usage errors. More...
 
class  expr
 A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort Boolean. Every expression has a sort. More...
 
class  fixedpoint
 
class  func_decl
 Function declaration (aka function definition). It is the signature of interpreted and uninterpreted functions in Z3. The basic building block in Z3 is the function application. More...
 
class  func_entry
 
class  func_interp
 
class  goal
 
class  model
 
class  object
 
class  on_clause
 
class  optimize
 
class  param_descrs
 
class  parameter
 class for auxiliary parameters associated with func_decl The class is initialized with a func_decl or application expression and an index The accessor get_expr, get_sort, ... is available depending on the value of kind(). The caller is responsible to check that the kind of the parameter aligns with the call (get_expr etc). More...
 
class  params
 
class  probe
 
class  simplifier
 
class  solver
 
class  sort
 A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort. More...
 
class  stats
 
class  symbol
 
class  tactic
 
class  user_propagator_base
 

Typedefs

typedef ast_vector_tpl< astast_vector
 
typedef ast_vector_tpl< exprexpr_vector
 
typedef ast_vector_tpl< sortsort_vector
 
typedef ast_vector_tpl< func_declfunc_decl_vector
 
typedef std::function< void(expr const &proof, std::vector< unsigned > const &deps, expr_vector const &clause)> on_clause_eh_t
 

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
 
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)
 
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.
 
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.
 
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.
 
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.
 
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.
 
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.
 
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.
 
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.
 
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.
 
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.
 
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
 
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
 
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
 
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
 
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
 
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
 
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.
 
expr bv2int (expr const &a, bool is_signed)
 bit-vector and integer conversions.
 
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
 
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.
 
func_decl linear_order (sort const &a, unsigned index)
 
func_decl partial_order (sort const &a, unsigned index)
 
func_decl piecewise_linear_order (sort const &a, unsigned index)
 
func_decl tree_order (sort const &a, unsigned index)
 
expr forall (expr const &x, expr const &b)
 
expr forall (expr const &x1, expr const &x2, expr const &b)
 
expr forall (expr const &x1, expr const &x2, expr const &x3, expr const &b)
 
expr forall (expr const &x1, expr const &x2, expr const &x3, expr const &x4, expr const &b)
 
expr forall (expr_vector const &xs, expr const &b)
 
expr exists (expr const &x, expr const &b)
 
expr exists (expr const &x1, expr const &x2, expr const &b)
 
expr exists (expr const &x1, expr const &x2, expr const &x3, expr const &b)
 
expr exists (expr const &x1, expr const &x2, expr const &x3, expr const &x4, expr const &b)
 
expr exists (expr_vector const &xs, expr const &b)
 
expr lambda (expr const &x, expr const &b)
 
expr lambda (expr const &x1, expr const &x2, expr const &b)
 
expr lambda (expr const &x1, expr const &x2, expr const &x3, expr const &b)
 
expr lambda (expr const &x1, expr const &x2, expr const &x3, expr const &x4, expr const &b)
 
expr lambda (expr_vector const &xs, expr const &b)
 
expr pble (expr_vector const &es, int const *coeffs, int bound)
 
expr pbge (expr_vector const &es, int const *coeffs, int bound)
 
expr pbeq (expr_vector const &es, int const *coeffs, int bound)
 
expr atmost (expr_vector const &es, unsigned bound)
 
expr atleast (expr_vector const &es, unsigned bound)
 
expr sum (expr_vector const &args)
 
expr distinct (expr_vector const &args)
 
expr concat (expr const &a, expr const &b)
 
expr concat (expr_vector const &args)
 
expr mk_or (expr_vector const &args)
 
expr mk_and (expr_vector const &args)
 
expr mk_xor (expr_vector const &args)
 
std::ostream & operator<< (std::ostream &out, model const &m)
 
std::ostream & operator<< (std::ostream &out, stats const &s)
 
std::ostream & operator<< (std::ostream &out, check_result r)
 
std::ostream & operator<< (std::ostream &out, solver const &s)
 
std::ostream & operator<< (std::ostream &out, goal const &g)
 
std::ostream & operator<< (std::ostream &out, apply_result const &r)
 
tactic operator& (tactic const &t1, tactic const &t2)
 
tactic operator| (tactic const &t1, tactic const &t2)
 
tactic repeat (tactic const &t, unsigned max=UINT_MAX)
 
tactic with (tactic const &t, params const &p)
 
tactic try_for (tactic const &t, unsigned ms)
 
tactic par_or (unsigned n, tactic const *tactics)
 
tactic par_and_then (tactic const &t1, tactic const &t2)
 
simplifier operator& (simplifier const &t1, simplifier const &t2)
 
simplifier with (simplifier const &t, params const &p)
 
probe operator<= (probe const &p1, probe const &p2)
 
probe operator<= (probe const &p1, double p2)
 
probe operator<= (double p1, probe const &p2)
 
probe operator>= (probe const &p1, probe const &p2)
 
probe operator>= (probe const &p1, double p2)
 
probe operator>= (double p1, probe const &p2)
 
probe operator< (probe const &p1, probe const &p2)
 
probe operator< (probe const &p1, double p2)
 
probe operator< (double p1, probe const &p2)
 
probe operator> (probe const &p1, probe const &p2)
 
probe operator> (probe const &p1, double p2)
 
probe operator> (double p1, probe const &p2)
 
probe operator== (probe const &p1, probe const &p2)
 
probe operator== (probe const &p1, double p2)
 
probe operator== (double p1, probe const &p2)
 
probe operator&& (probe const &p1, probe const &p2)
 
probe operator|| (probe const &p1, probe const &p2)
 
probe operator! (probe const &p)
 
std::ostream & operator<< (std::ostream &out, optimize const &s)
 
std::ostream & operator<< (std::ostream &out, fixedpoint const &f)
 
tactic fail_if (probe const &p)
 
tactic when (probe const &p, tactic const &t)
 
tactic cond (probe const &p, tactic const &t1, tactic const &t2)
 
expr to_real (expr const &a)
 
func_decl function (symbol const &name, unsigned arity, sort const *domain, sort const &range)
 
func_decl function (char const *name, unsigned arity, sort const *domain, sort const &range)
 
func_decl function (char const *name, sort const &domain, sort const &range)
 
func_decl function (char const *name, sort const &d1, sort const &d2, sort const &range)
 
func_decl function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &range)
 
func_decl function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &d4, sort const &range)
 
func_decl function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &d4, sort const &d5, sort const &range)
 
func_decl function (char const *name, sort_vector const &domain, sort const &range)
 
func_decl function (std::string const &name, sort_vector const &domain, sort const &range)
 
func_decl recfun (symbol const &name, unsigned arity, sort const *domain, sort const &range)
 
func_decl recfun (char const *name, unsigned arity, sort const *domain, sort const &range)
 
func_decl recfun (char const *name, sort const &d1, sort const &range)
 
func_decl recfun (char const *name, sort const &d1, sort const &d2, sort const &range)
 
expr select (expr const &a, int i)
 
expr store (expr const &a, expr const &i, expr const &v)
 
expr store (expr const &a, int i, expr const &v)
 
expr store (expr const &a, expr i, int v)
 
expr store (expr const &a, int i, int v)
 
expr store (expr const &a, expr_vector const &i, expr const &v)
 
expr as_array (func_decl &f)
 
expr const_array (sort const &d, expr const &v)
 
expr empty_set (sort const &s)
 
expr full_set (sort const &s)
 
expr set_add (expr const &s, expr const &e)
 
expr set_del (expr const &s, expr const &e)
 
expr set_union (expr const &a, expr const &b)
 
expr set_intersect (expr const &a, expr const &b)
 
expr set_difference (expr const &a, expr const &b)
 
expr set_complement (expr const &a)
 
expr set_member (expr const &s, expr const &e)
 
expr set_subset (expr const &a, expr const &b)
 
expr empty (sort const &s)
 
expr suffixof (expr const &a, expr const &b)
 
expr prefixof (expr const &a, expr const &b)
 
expr indexof (expr const &s, expr const &substr, expr const &offset)
 
expr last_indexof (expr const &s, expr const &substr)
 
expr to_re (expr const &s)
 
expr in_re (expr const &s, expr const &re)
 
expr plus (expr const &re)
 
expr option (expr const &re)
 
expr star (expr const &re)
 
expr re_empty (sort const &s)
 
expr re_full (sort const &s)
 
expr re_intersect (expr_vector const &args)
 
expr re_diff (expr const &a, expr const &b)
 
expr re_complement (expr const &a)
 
expr range (expr const &lo, expr const &hi)
 

Detailed Description

Z3 C++ namespace.

Typedef Documentation

◆ ast_vector

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

◆ expr_vector

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

◆ func_decl_vector

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

◆ on_clause_eh_t

typedef std::function<void(expr const& proof, std::vector<unsigned> const& deps, expr_vector const& clause)> on_clause_eh_t

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

◆ sort_vector

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

Enumeration Type Documentation

◆ check_result

Enumerator
unsat 
sat 
unknown 

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

135 {
136 unsat, sat, unknown
137 };

◆ rounding_mode

Enumerator
RNA 
RNE 
RTP 
RTN 
RTZ 

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

139 {
140 RNA,
141 RNE,
142 RTP,
143 RTN,
144 RTZ
145 };
@ RNE
Definition z3++.h:141
@ RNA
Definition z3++.h:140
@ RTZ
Definition z3++.h:144
@ RTN
Definition z3++.h:143
@ RTP
Definition z3++.h:142

Function Documentation

◆ abs()

expr abs ( expr const &  a)
inline

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

1994 {
1995 Z3_ast r;
1996 if (a.is_int()) {
1997 expr zero = a.ctx().int_val(0);
1998 expr ge = a >= zero;
1999 expr na = -a;
2000 r = Z3_mk_ite(a.ctx(), ge, a, na);
2001 }
2002 else if (a.is_real()) {
2003 expr zero = a.ctx().real_val(0);
2004 expr ge = a >= zero;
2005 expr na = -a;
2006 r = Z3_mk_ite(a.ctx(), ge, a, na);
2007 }
2008 else {
2009 r = Z3_mk_fpa_abs(a.ctx(), a);
2010 }
2011 a.check_error();
2012 return expr(a.ctx(), r);
2013 }
expr int_val(int n)
Definition z3++.h:3742
expr real_val(int n)
Definition z3++.h:3749
A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort ...
Definition z3++.h:810
context & ctx() const
Definition z3++.h:473
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.

◆ as_array()

expr as_array ( func_decl f)
inline

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

3940 {
3941 Z3_ast r = Z3_mk_as_array(f.ctx(), f);
3942 f.check_error();
3943 return expr(f.ctx(), r);
3944 }
Z3_error_code check_error() const
Definition z3++.h:474
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 ashr ( expr const &  a,
expr const &  b 
)
inline

arithmetic shift right operator for bitvectors

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

2220{ return to_expr(a.ctx(), Z3_mk_bvashr(a.ctx(), a, b)); }
Z3_ast Z3_API Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2)
Arithmetic shift right.
expr to_expr(context &c, Z3_ast a)
Wraps a Z3_ast as an expr object. It also checks for errors. This function allows the user to use the...
Definition z3++.h:2106

Referenced by ashr(), and ashr().

◆ ashr() [2/3]

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

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

2221{ return ashr(a, a.ctx().num_val(b, a.get_sort())); }
expr ashr(expr const &a, expr const &b)
arithmetic shift right operator for bitvectors
Definition z3++.h:2220

◆ ashr() [3/3]

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

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

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

◆ atleast()

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

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

2429 {
2430 assert(es.size() > 0);
2431 context& ctx = es[0u].ctx();
2432 array<Z3_ast> _es(es);
2433 Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
2434 ctx.check_error();
2435 return expr(ctx, r);
2436 }
A Context manages all other Z3 objects, global configuration options, etc.
Definition z3++.h:160
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition z3++.h:192
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.

◆ atmost()

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

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

2421 {
2422 assert(es.size() > 0);
2423 context& ctx = es[0u].ctx();
2424 array<Z3_ast> _es(es);
2425 Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
2426 ctx.check_error();
2427 return expr(ctx, r);
2428 }
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.

◆ bv2int()

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

bit-vector and integer conversions.

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

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

◆ bvadd_no_overflow()

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

bit-vector overflow/underflow checks

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

2238 {
2239 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);
2240 }
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.
void check_context(object const &a, object const &b)
Definition z3++.h:477

◆ bvadd_no_underflow()

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

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

2241 {
2242 check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2243 }
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 bvmul_no_overflow ( expr const &  a,
expr const &  b,
bool  is_signed 
)
inline

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

2256 {
2257 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);
2258 }
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 bvmul_no_underflow ( expr const &  a,
expr const &  b 
)
inline

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

2259 {
2260 check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2261 }
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 bvneg_no_overflow ( expr const &  a)
inline

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

2253 {
2254 Z3_ast r = Z3_mk_bvneg_no_overflow(a.ctx(), a); a.check_error(); return expr(a.ctx(), r);
2255 }
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 bvredand ( expr const &  a)
inline

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

1988 {
1989 assert(a.is_bv());
1990 Z3_ast r = Z3_mk_bvredand(a.ctx(), a);
1991 a.check_error();
1992 return expr(a.ctx(), r);
1993 }
Z3_ast Z3_API Z3_mk_bvredand(Z3_context c, Z3_ast t1)
Take conjunction of bits in vector, return vector of length 1.

◆ bvredor()

expr bvredor ( expr const &  a)
inline

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

1982 {
1983 assert(a.is_bv());
1984 Z3_ast r = Z3_mk_bvredor(a.ctx(), a);
1985 a.check_error();
1986 return expr(a.ctx(), r);
1987 }
Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1)
Take disjunction of bits in vector, return vector of length 1.

◆ bvsdiv_no_overflow()

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

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

2250 {
2251 check_context(a, b); Z3_ast r = Z3_mk_bvsdiv_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2252 }
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 bvsub_no_overflow ( expr const &  a,
expr const &  b 
)
inline

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

2244 {
2245 check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2246 }
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 bvsub_no_underflow ( expr const &  a,
expr const &  b,
bool  is_signed 
)
inline

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

2247 {
2248 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);
2249 }
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 check_context ( object const &  a,
object const &  b 
)
inline

◆ concat() [1/2]

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

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

2455 {
2456 check_context(a, b);
2457 Z3_ast r;
2458 if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
2459 Z3_ast _args[2] = { a, b };
2460 r = Z3_mk_seq_concat(a.ctx(), 2, _args);
2461 }
2462 else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
2463 Z3_ast _args[2] = { a, b };
2464 r = Z3_mk_re_concat(a.ctx(), 2, _args);
2465 }
2466 else {
2467 r = Z3_mk_concat(a.ctx(), a, b);
2468 }
2469 a.ctx().check_error();
2470 return expr(a.ctx(), r);
2471 }
bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])
Create the concatenation of the regular languages.
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
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 concat ( expr_vector const &  args)
inline

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

2473 {
2474 Z3_ast r;
2475 assert(args.size() > 0);
2476 if (args.size() == 1) {
2477 return args[0u];
2478 }
2479 context& ctx = args[0u].ctx();
2480 array<Z3_ast> _args(args);
2481 if (Z3_is_seq_sort(ctx, args[0u].get_sort())) {
2482 r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
2483 }
2484 else if (Z3_is_re_sort(ctx, args[0u].get_sort())) {
2485 r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
2486 }
2487 else {
2488 r = _args[args.size()-1];
2489 for (unsigned i = args.size()-1; i > 0; ) {
2490 --i;
2491 r = Z3_mk_concat(ctx, _args[i], r);
2492 ctx.check_error();
2493 }
2494 }
2495 ctx.check_error();
2496 return expr(ctx, r);
2497 }

◆ cond()

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

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

3420 {
3421 check_context(p, t1); check_context(p, t2);
3422 Z3_tactic r = Z3_tactic_cond(t1.ctx(), p, t1, t2);
3423 t1.check_error();
3424 return tactic(t1.ctx(), r);
3425 }
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 const_array ( sort const &  d,
expr const &  v 
)
inline

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

3957 {
3959 }
Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v)
Create the constant array.
#define MK_EXPR2(_fn, _arg1, _arg2)
Definition z3++.h:3951

◆ distinct()

expr distinct ( expr_vector const &  args)
inline

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

2446 {
2447 assert(args.size() > 0);
2448 context& ctx = args[0u].ctx();
2449 array<Z3_ast> _args(args);
2450 Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
2451 ctx.check_error();
2452 return expr(ctx, r);
2453 }
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 empty ( sort const &  s)
inline

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

4013 {
4014 Z3_ast r = Z3_mk_seq_empty(s.ctx(), s);
4015 s.check_error();
4016 return expr(s.ctx(), r);
4017 }
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 empty_set ( sort const &  s)
inline

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

3961 {
3963 }
Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain)
Create the empty set.
#define MK_EXPR1(_fn, _arg)
Definition z3++.h:3946

◆ eq()

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

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

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

◆ exists() [1/5]

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

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

2348 {
2349 check_context(x, b);
2350 Z3_app vars[] = {(Z3_app) x};
2351 Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2352 }
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 exists ( expr const &  x1,
expr const &  x2,
expr const &  b 
)
inline

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

2353 {
2354 check_context(x1, b); check_context(x2, b);
2355 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2356 Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2357 }

◆ exists() [3/5]

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

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

2358 {
2359 check_context(x1, b); check_context(x2, b); check_context(x3, b);
2360 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2361 Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2362 }

◆ exists() [4/5]

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

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

2363 {
2364 check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2365 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2366 Z3_ast r = Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2367 }

◆ exists() [5/5]

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

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

2368 {
2369 array<Z3_app> vars(xs);
2370 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);
2371 }

◆ fail_if()

tactic fail_if ( probe const &  p)
inline

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

3409 {
3410 Z3_tactic r = Z3_tactic_fail_if(p.ctx(), p);
3411 p.check_error();
3412 return tactic(p.ctx(), r);
3413 }
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 fma ( expr const &  a,
expr const &  b,
expr const &  c,
expr const &  rm 
)
inline

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

2030 {
2031 check_context(a, b); check_context(a, c); check_context(a, rm);
2032 assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
2033 Z3_ast r = Z3_mk_fpa_fma(a.ctx(), rm, a, b, c);
2034 a.check_error();
2035 return expr(a.ctx(), r);
2036 }
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 forall ( expr const &  x,
expr const &  b 
)
inline

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

2324 {
2325 check_context(x, b);
2326 Z3_app vars[] = {(Z3_app) x};
2327 Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2328 }
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 forall ( expr const &  x1,
expr const &  x2,
expr const &  b 
)
inline

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

2329 {
2330 check_context(x1, b); check_context(x2, b);
2331 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2332 Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2333 }

◆ forall() [3/5]

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

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

2334 {
2335 check_context(x1, b); check_context(x2, b); check_context(x3, b);
2336 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2337 Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2338 }

◆ forall() [4/5]

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

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

2339 {
2340 check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2341 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2342 Z3_ast r = Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error(); return expr(b.ctx(), r);
2343 }

◆ forall() [5/5]

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

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

2344 {
2345 array<Z3_app> vars(xs);
2346 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);
2347 }

◆ fp_eq()

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

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

2021 {
2022 check_context(a, b);
2023 assert(a.is_fpa());
2024 Z3_ast r = Z3_mk_fpa_eq(a.ctx(), a, b);
2025 a.check_error();
2026 return expr(a.ctx(), r);
2027 }
Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point equality.

◆ fpa_fp()

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

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

2038 {
2039 check_context(sgn, exp); check_context(exp, sig);
2040 assert(sgn.is_bv() && exp.is_bv() && sig.is_bv());
2041 Z3_ast r = Z3_mk_fpa_fp(sgn.ctx(), sgn, exp, sig);
2042 sgn.check_error();
2043 return expr(sgn.ctx(), r);
2044 }
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 fpa_to_fpa ( expr const &  t,
sort  s 
)
inline

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

2074 {
2075 assert(t.is_fpa());
2076 Z3_ast r = Z3_mk_fpa_to_fp_float(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2077 t.check_error();
2078 return expr(t.ctx(), r);
2079 }
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 fpa_to_sbv ( expr const &  t,
unsigned  sz 
)
inline

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

2046 {
2047 assert(t.is_fpa());
2048 Z3_ast r = Z3_mk_fpa_to_sbv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
2049 t.check_error();
2050 return expr(t.ctx(), r);
2051 }
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 fpa_to_ubv ( expr const &  t,
unsigned  sz 
)
inline

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

2053 {
2054 assert(t.is_fpa());
2055 Z3_ast r = Z3_mk_fpa_to_ubv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
2056 t.check_error();
2057 return expr(t.ctx(), r);
2058 }
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 full_set ( sort const &  s)
inline

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

3965 {
3967 }
Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain)
Create the full set.

◆ function() [1/9]

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

3880 {
3881 return range.ctx().function(name, d1, d2, d3, d4, d5, range);
3882 }
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition z3++.h:3583
expr range(expr const &lo, expr const &hi)
Definition z3++.h:4085

◆ function() [2/9]

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

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

3877 {
3878 return range.ctx().function(name, d1, d2, d3, d4, range);
3879 }

◆ function() [3/9]

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

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

3874 {
3875 return range.ctx().function(name, d1, d2, d3, range);
3876 }

◆ function() [4/9]

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

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

3871 {
3872 return range.ctx().function(name, d1, d2, range);
3873 }

◆ function() [5/9]

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

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

3868 {
3869 return range.ctx().function(name, domain, range);
3870 }

◆ function() [6/9]

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

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

3883 {
3884 return range.ctx().function(name, domain, range);
3885 }

◆ function() [7/9]

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

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

3865 {
3866 return range.ctx().function(name, arity, domain, range);
3867 }

◆ function() [8/9]

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

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

3886 {
3887 return range.ctx().function(name.c_str(), domain, range);
3888 }

◆ function() [9/9]

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

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

3862 {
3863 return range.ctx().function(name, arity, domain, range);
3864 }

◆ implies() [1/3]

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

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

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

◆ implies() [2/3]

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

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

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

◆ implies() [3/3]

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

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

1628 {
1629 assert(a.is_bool() && b.is_bool());
1631 }
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
#define _Z3_MK_BIN_(a, b, binop)
Definition z3++.h:1621

◆ in_re()

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

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

4045 {
4046 MK_EXPR2(Z3_mk_seq_in_re, s, re);
4047 }
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 indexof ( expr const &  s,
expr const &  substr,
expr const &  offset 
)
inline

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

4030 {
4031 check_context(s, substr); check_context(s, offset);
4032 Z3_ast r = Z3_mk_seq_index(s.ctx(), s, substr, offset);
4033 s.check_error();
4034 return expr(s.ctx(), r);
4035 }
Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset)
Return index of the first occurrence of substr in s starting from offset offset. If s does not contai...

◆ int2bv()

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

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

2233{ Z3_ast r = Z3_mk_int2bv(a.ctx(), n, a); a.check_error(); return expr(a.ctx(), r); }
Z3_ast Z3_API Z3_mk_int2bv(Z3_context c, unsigned n, Z3_ast t1)
Create an n bit bit-vector from the integer argument t1.

◆ is_int()

expr is_int ( expr const &  e)
inline

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

1676{ _Z3_MK_UN_(e, 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.
#define _Z3_MK_UN_(a, mkun)
Definition z3++.h:1668

◆ ite()

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

2093 {
2094 check_context(c, t); check_context(c, e);
2095 assert(c.is_bool());
2096 Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
2097 c.check_error();
2098 return expr(c.ctx(), r);
2099 }

◆ lambda() [1/5]

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

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

2372 {
2373 check_context(x, b);
2374 Z3_app vars[] = {(Z3_app) x};
2375 Z3_ast r = Z3_mk_lambda_const(b.ctx(), 1, vars, b); b.check_error(); return expr(b.ctx(), r);
2376 }
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 lambda ( expr const &  x1,
expr const &  x2,
expr const &  b 
)
inline

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

2377 {
2378 check_context(x1, b); check_context(x2, b);
2379 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2380 Z3_ast r = Z3_mk_lambda_const(b.ctx(), 2, vars, b); b.check_error(); return expr(b.ctx(), r);
2381 }

◆ lambda() [3/5]

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

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

2382 {
2383 check_context(x1, b); check_context(x2, b); check_context(x3, b);
2384 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2385 Z3_ast r = Z3_mk_lambda_const(b.ctx(), 3, vars, b); b.check_error(); return expr(b.ctx(), r);
2386 }

◆ lambda() [4/5]

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

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

2387 {
2388 check_context(x1, b); check_context(x2, b); check_context(x3, b); check_context(x4, b);
2389 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2390 Z3_ast r = Z3_mk_lambda_const(b.ctx(), 4, vars, b); b.check_error(); return expr(b.ctx(), r);
2391 }

◆ lambda() [5/5]

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

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

2392 {
2393 array<Z3_app> vars(xs);
2394 Z3_ast r = Z3_mk_lambda_const(b.ctx(), vars.size(), vars.ptr(), b); b.check_error(); return expr(b.ctx(), r);
2395 }

◆ last_indexof()

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

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

4036 {
4037 check_context(s, substr);
4038 Z3_ast r = Z3_mk_seq_last_index(s.ctx(), s, substr);
4039 s.check_error();
4040 return expr(s.ctx(), r);
4041 }
Z3_ast Z3_API Z3_mk_seq_last_index(Z3_context c, Z3_ast s, Z3_ast substr)
Return index of the last occurrence of substr in s. If s does not contain substr, then the value is -...

◆ linear_order()

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

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

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

◆ lshr() [1/3]

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

logic shift right operator for bitvectors

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

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

Referenced by lshr(), and lshr().

◆ lshr() [2/3]

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

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

2214{ return lshr(a, a.ctx().num_val(b, a.get_sort())); }
expr lshr(expr const &a, expr const &b)
logic shift right operator for bitvectors
Definition z3++.h:2213

◆ lshr() [3/3]

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

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

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

◆ max()

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

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

1966 {
1967 check_context(a, b);
1968 Z3_ast r;
1969 if (a.is_arith()) {
1970 r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), a, b);
1971 }
1972 else if (a.is_bv()) {
1973 r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), a, b);
1974 }
1975 else {
1976 assert(a.is_fpa());
1977 r = Z3_mk_fpa_max(a.ctx(), a, b);
1978 }
1979 a.check_error();
1980 return expr(a.ctx(), r);
1981 }
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2)
Maximum of floating-point numbers.
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.

◆ min()

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

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

1950 {
1951 check_context(a, b);
1952 Z3_ast r;
1953 if (a.is_arith()) {
1954 r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), b, a);
1955 }
1956 else if (a.is_bv()) {
1957 r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), b, a);
1958 }
1959 else {
1960 assert(a.is_fpa());
1961 r = Z3_mk_fpa_min(a.ctx(), a, b);
1962 }
1963 a.check_error();
1964 return expr(a.ctx(), r);
1965 }
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 mk_and ( expr_vector const &  args)
inline

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

2505 {
2506 array<Z3_ast> _args(args);
2507 Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2508 args.check_error();
2509 return expr(args.ctx(), r);
2510 }
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 mk_or ( expr_vector const &  args)
inline

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

2499 {
2500 array<Z3_ast> _args(args);
2501 Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2502 args.check_error();
2503 return expr(args.ctx(), r);
2504 }
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].

◆ mk_xor()

expr mk_xor ( expr_vector const &  args)
inline

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

2511 {
2512 if (args.empty())
2513 return args.ctx().bool_val(false);
2514 expr r = args[0u];
2515 for (unsigned i = 1; i < args.size(); ++i)
2516 r = r ^ args[i];
2517 return r;
2518 }

◆ mod() [1/3]

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

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

1640 {
1641 if (a.is_bv()) {
1642 _Z3_MK_BIN_(a, b, Z3_mk_bvsmod);
1643 }
1644 else {
1645 _Z3_MK_BIN_(a, b, Z3_mk_mod);
1646 }
1647 }
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.
Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows divisor).

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

◆ mod() [2/3]

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

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

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

◆ mod() [3/3]

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

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

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

◆ nand()

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

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

1947{ if (a.is_bool()) return !(a && b); check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nand.

◆ nor()

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

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

1948{ if (a.is_bool()) return !(a || b); check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nor.

◆ operator!() [1/2]

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

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

1674{ assert(a.is_bool()); _Z3_MK_UN_(a, 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 operator! ( probe const &  p)
inline

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

3243 {
3244 Z3_probe r = Z3_probe_not(p.ctx(), p); p.check_error(); return probe(p.ctx(), r);
3245 }
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 operator!= ( double  a,
expr const &  b 
)
inline

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

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

◆ operator!=() [2/5]

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

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

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

◆ operator!=() [3/5]

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

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

1716 {
1717 check_context(a, b);
1718 Z3_ast args[2] = { a, b };
1719 Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1720 a.check_error();
1721 return expr(a.ctx(), r);
1722 }

◆ operator!=() [4/5]

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

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

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

◆ operator!=() [5/5]

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

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

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

◆ operator%() [1/3]

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

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

1651{ return mod(a, b); }

◆ operator%() [2/3]

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

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

1652{ return mod(a, b); }

◆ operator%() [3/3]

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

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

1653{ return mod(a, b); }

◆ operator&() [1/5]

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

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

1935{ if (a.is_bool()) return a && b; check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.

◆ operator&() [2/5]

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

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

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

◆ operator&() [3/5]

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

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

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

◆ operator&() [4/5]

simplifier operator& ( simplifier const &  t1,
simplifier const &  t2 
)
inline

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

3157 {
3158 check_context(t1, t2);
3159 Z3_simplifier r = Z3_simplifier_and_then(t1.ctx(), t1, t2);
3160 t1.check_error();
3161 return simplifier(t1.ctx(), r);
3162 }
Z3_simplifier Z3_API Z3_simplifier_and_then(Z3_context c, Z3_simplifier t1, Z3_simplifier t2)
Return a simplifier that applies t1 to a given goal and t2 to every subgoal produced by t1.

◆ operator&() [5/5]

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

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

3083 {
3084 check_context(t1, t2);
3085 Z3_tactic r = Z3_tactic_and_then(t1.ctx(), t1, t2);
3086 t1.check_error();
3087 return tactic(t1.ctx(), r);
3088 }
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 operator&& ( bool  a,
expr const &  b 
)
inline
Precondition
b.is_bool()

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

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

◆ operator&&() [2/4]

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

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

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

◆ operator&&() [3/4]

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

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

1680 {
1681 check_context(a, b);
1682 assert(a.is_bool() && b.is_bool());
1683 Z3_ast args[2] = { a, b };
1684 Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
1685 a.check_error();
1686 return expr(a.ctx(), r);
1687 }

◆ operator&&() [4/4]

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

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

3237 {
3238 check_context(p1, p2); Z3_probe r = Z3_probe_and(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3239 }
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 operator* ( expr const &  a,
expr const &  b 
)
inline

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

1758 {
1759 check_context(a, b);
1760 Z3_ast r = 0;
1761 if (a.is_arith() && b.is_arith()) {
1762 Z3_ast args[2] = { a, b };
1763 r = Z3_mk_mul(a.ctx(), 2, args);
1764 }
1765 else if (a.is_bv() && b.is_bv()) {
1766 r = Z3_mk_bvmul(a.ctx(), a, b);
1767 }
1768 else if (a.is_fpa() && b.is_fpa()) {
1769 r = Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1770 }
1771 else {
1772 // operator is not supported by given arguments.
1773 assert(false);
1774 }
1775 a.check_error();
1776 return expr(a.ctx(), r);
1777 }
Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] * ... * args[num_args-1].
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
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 operator* ( expr const &  a,
int  b 
)
inline

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

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

◆ operator*() [3/3]

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

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

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

◆ operator+() [1/3]

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

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

1728 {
1729 check_context(a, b);
1730 Z3_ast r = 0;
1731 if (a.is_arith() && b.is_arith()) {
1732 Z3_ast args[2] = { a, b };
1733 r = Z3_mk_add(a.ctx(), 2, args);
1734 }
1735 else if (a.is_bv() && b.is_bv()) {
1736 r = Z3_mk_bvadd(a.ctx(), a, b);
1737 }
1738 else if (a.is_seq() && b.is_seq()) {
1739 return concat(a, b);
1740 }
1741 else if (a.is_re() && b.is_re()) {
1742 Z3_ast _args[2] = { a, b };
1743 r = Z3_mk_re_union(a.ctx(), 2, _args);
1744 }
1745 else if (a.is_fpa() && b.is_fpa()) {
1746 r = Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1747 }
1748 else {
1749 // operator is not supported by given arguments.
1750 assert(false);
1751 }
1752 a.check_error();
1753 return expr(a.ctx(), r);
1754 }
Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[])
Create the union of the regular languages.
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement addition.
Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point addition.
Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] + ... + args[num_args-1].
expr concat(expr const &a, expr const &b)
Definition z3++.h:2455

◆ operator+() [2/3]

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

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

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

◆ operator+() [3/3]

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

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

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

◆ operator-() [1/4]

expr operator- ( expr const &  a)
inline

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

1824 {
1825 Z3_ast r = 0;
1826 if (a.is_arith()) {
1827 r = Z3_mk_unary_minus(a.ctx(), a);
1828 }
1829 else if (a.is_bv()) {
1830 r = Z3_mk_bvneg(a.ctx(), a);
1831 }
1832 else if (a.is_fpa()) {
1833 r = Z3_mk_fpa_neg(a.ctx(), a);
1834 }
1835 else {
1836 // operator is not supported by given arguments.
1837 assert(false);
1838 }
1839 a.check_error();
1840 return expr(a.ctx(), r);
1841 }
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.

◆ operator-() [2/4]

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

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

1843 {
1844 check_context(a, b);
1845 Z3_ast r = 0;
1846 if (a.is_arith() && b.is_arith()) {
1847 Z3_ast args[2] = { a, b };
1848 r = Z3_mk_sub(a.ctx(), 2, args);
1849 }
1850 else if (a.is_bv() && b.is_bv()) {
1851 r = Z3_mk_bvsub(a.ctx(), a, b);
1852 }
1853 else if (a.is_fpa() && b.is_fpa()) {
1854 r = Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1855 }
1856 else {
1857 // operator is not supported by given arguments.
1858 assert(false);
1859 }
1860 a.check_error();
1861 return expr(a.ctx(), r);
1862 }
Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point subtraction.
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] - ... - args[num_args - 1].

◆ operator-() [3/4]

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

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

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

◆ operator-() [4/4]

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

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

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

◆ operator/() [1/3]

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

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

1802 {
1803 check_context(a, b);
1804 Z3_ast r = 0;
1805 if (a.is_arith() && b.is_arith()) {
1806 r = Z3_mk_div(a.ctx(), a, b);
1807 }
1808 else if (a.is_bv() && b.is_bv()) {
1809 r = Z3_mk_bvsdiv(a.ctx(), a, b);
1810 }
1811 else if (a.is_fpa() && b.is_fpa()) {
1812 r = Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1813 }
1814 else {
1815 // operator is not supported by given arguments.
1816 assert(false);
1817 }
1818 a.check_error();
1819 return expr(a.ctx(), r);
1820 }
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.
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 operator/ ( expr const &  a,
int  b 
)
inline

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

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

◆ operator/() [3/3]

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

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

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

◆ operator<() [1/6]

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

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

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

◆ operator<() [2/6]

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

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

1891 {
1892 check_context(a, b);
1893 Z3_ast r = 0;
1894 if (a.is_arith() && b.is_arith()) {
1895 r = Z3_mk_lt(a.ctx(), a, b);
1896 }
1897 else if (a.is_bv() && b.is_bv()) {
1898 r = Z3_mk_bvslt(a.ctx(), a, b);
1899 }
1900 else if (a.is_fpa() && b.is_fpa()) {
1901 r = Z3_mk_fpa_lt(a.ctx(), a, b);
1902 }
1903 else {
1904 // operator is not supported by given arguments.
1905 assert(false);
1906 }
1907 a.check_error();
1908 return expr(a.ctx(), r);
1909 }
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than.
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
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 operator< ( expr const &  a,
int  b 
)
inline

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

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

◆ operator<() [4/6]

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

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

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

◆ operator<() [5/6]

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

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

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

◆ operator<() [6/6]

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

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

3222 {
3223 check_context(p1, p2); Z3_probe r = Z3_probe_lt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3224 }
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 & operator<< ( std::ostream &  out,
apply_result const &  r 
)
inline

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

3041{ out << Z3_apply_result_to_string(r.ctx(), r); return out; }
Z3_string Z3_API Z3_apply_result_to_string(Z3_context c, Z3_apply_result r)
Convert the Z3_apply_result object returned by Z3_tactic_apply into a string.

◆ operator<<() [2/13]

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

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

579 {
580 out << Z3_ast_to_string(n.ctx(), n.m_ast); return out;
581 }
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 & operator<< ( std::ostream &  out,
check_result  r 
)
inline

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

2687 {
2688 if (r == unsat) out << "unsat";
2689 else if (r == sat) out << "sat";
2690 else out << "unknown";
2691 return out;
2692 }

◆ operator<<() [4/13]

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

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

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

◆ operator<<() [5/13]

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

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

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

◆ operator<<() [6/13]

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

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

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

◆ operator<<() [7/13]

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

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

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

◆ operator<<() [8/13]

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

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

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

◆ operator<<() [9/13]

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

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

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

◆ operator<<() [10/13]

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

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

546 {
547 out << Z3_params_to_string(p.ctx(), p); return out;
548 }
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 & operator<< ( std::ostream &  out,
solver const &  s 
)
inline

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

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

◆ operator<<() [12/13]

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

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

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

◆ operator<<() [13/13]

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

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

490 {
491 if (s.kind() == Z3_INT_SYMBOL)
492 out << "k!" << s.to_int();
493 else
494 out << s.str();
495 return out;
496 }
@ Z3_INT_SYMBOL
Definition z3_api.h:76

◆ operator<=() [1/6]

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

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

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

◆ operator<=() [2/6]

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

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

1866 {
1867 check_context(a, b);
1868 Z3_ast r = 0;
1869 if (a.is_arith() && b.is_arith()) {
1870 r = Z3_mk_le(a.ctx(), a, b);
1871 }
1872 else if (a.is_bv() && b.is_bv()) {
1873 r = Z3_mk_bvsle(a.ctx(), a, b);
1874 }
1875 else if (a.is_fpa() && b.is_fpa()) {
1876 r = Z3_mk_fpa_leq(a.ctx(), a, b);
1877 }
1878 else {
1879 // operator is not supported by given arguments.
1880 assert(false);
1881 }
1882 a.check_error();
1883 return expr(a.ctx(), r);
1884 }
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_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than or equal.

◆ operator<=() [3/6]

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

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

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

◆ operator<=() [4/6]

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

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

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

◆ operator<=() [5/6]

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

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

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

◆ operator<=() [6/6]

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

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

3212 {
3213 check_context(p1, p2); Z3_probe r = Z3_probe_le(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3214 }
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 operator== ( double  a,
expr const &  b 
)
inline

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

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

◆ operator==() [2/8]

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

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

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

◆ operator==() [3/8]

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

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

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

◆ operator==() [4/8]

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

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

1705 {
1706 check_context(a, b);
1707 Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1708 a.check_error();
1709 return expr(a.ctx(), r);
1710 }
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 operator== ( expr const &  a,
int  b 
)
inline

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

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

◆ operator==() [6/8]

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

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

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

◆ operator==() [7/8]

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

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

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

◆ operator==() [8/8]

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

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

3232 {
3233 check_context(p1, p2); Z3_probe r = Z3_probe_eq(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3234 }
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 operator> ( double  p1,
probe const &  p2 
)
inline

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

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

◆ operator>() [2/6]

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

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

1913 {
1914 check_context(a, b);
1915 Z3_ast r = 0;
1916 if (a.is_arith() && b.is_arith()) {
1917 r = Z3_mk_gt(a.ctx(), a, b);
1918 }
1919 else if (a.is_bv() && b.is_bv()) {
1920 r = Z3_mk_bvsgt(a.ctx(), a, b);
1921 }
1922 else if (a.is_fpa() && b.is_fpa()) {
1923 r = Z3_mk_fpa_gt(a.ctx(), a, b);
1924 }
1925 else {
1926 // operator is not supported by given arguments.
1927 assert(false);
1928 }
1929 a.check_error();
1930 return expr(a.ctx(), r);
1931 }
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than.
Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than.
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.

◆ operator>() [3/6]

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

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

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

◆ operator>() [4/6]

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

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

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

◆ operator>() [5/6]

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

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

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

◆ operator>() [6/6]

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

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

3227 {
3228 check_context(p1, p2); Z3_probe r = Z3_probe_gt(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3229 }
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 operator>= ( double  p1,
probe const &  p2 
)
inline

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

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

◆ operator>=() [2/6]

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

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

1782 {
1783 check_context(a, b);
1784 Z3_ast r = 0;
1785 if (a.is_arith() && b.is_arith()) {
1786 r = Z3_mk_ge(a.ctx(), a, b);
1787 }
1788 else if (a.is_bv() && b.is_bv()) {
1789 r = Z3_mk_bvsge(a.ctx(), a, b);
1790 }
1791 else if (a.is_fpa() && b.is_fpa()) {
1792 r = Z3_mk_fpa_geq(a.ctx(), a, b);
1793 }
1794 else {
1795 // operator is not supported by given arguments.
1796 assert(false);
1797 }
1798 a.check_error();
1799 return expr(a.ctx(), r);
1800 }
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_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 operator>= ( expr const &  a,
int  b 
)
inline

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

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

◆ operator>=() [4/6]

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

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

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

◆ operator>=() [5/6]

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

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

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

◆ operator>=() [6/6]

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

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

3217 {
3218 check_context(p1, p2); Z3_probe r = Z3_probe_ge(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3219 }
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 operator^ ( expr const &  a,
expr const &  b 
)
inline

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

1939{ check_context(a, b); Z3_ast r = a.is_bool() ? Z3_mk_xor(a.ctx(), a, b) : Z3_mk_bvxor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
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 operator^ ( expr const &  a,
int  b 
)
inline

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

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

◆ operator^() [3/3]

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

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

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

◆ operator|() [1/4]

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

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

1943{ if (a.is_bool()) return a || b; check_context(a, b); Z3_ast r = Z3_mk_bvor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.

◆ operator|() [2/4]

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

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

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

◆ operator|() [3/4]

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

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

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

◆ operator|() [4/4]

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

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

3090 {
3091 check_context(t1, t2);
3092 Z3_tactic r = Z3_tactic_or_else(t1.ctx(), t1, t2);
3093 t1.check_error();
3094 return tactic(t1.ctx(), r);
3095 }
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 operator|| ( bool  a,
expr const &  b 
)
inline
Precondition
b.is_bool()

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

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

◆ operator||() [2/4]

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

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

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

◆ operator||() [3/4]

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

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

1692 {
1693 check_context(a, b);
1694 assert(a.is_bool() && b.is_bool());
1695 Z3_ast args[2] = { a, b };
1696 Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1697 a.check_error();
1698 return expr(a.ctx(), r);
1699 }

◆ operator||() [4/4]

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

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

3240 {
3241 check_context(p1, p2); Z3_probe r = Z3_probe_or(p1.ctx(), p1, p2); p1.check_error(); return probe(p1.ctx(), r);
3242 }
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 operator~ ( expr const &  a)
inline

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

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

◆ option()

expr option ( expr const &  re)
inline

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

4051 {
4053 }
Z3_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re)
Create the regular language [re].

◆ par_and_then()

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

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

3122 {
3123 check_context(t1, t2);
3124 Z3_tactic r = Z3_tactic_par_and_then(t1.ctx(), t1, t2);
3125 t1.check_error();
3126 return tactic(t1.ctx(), r);
3127 }
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 par_or ( unsigned  n,
tactic const *  tactics 
)
inline

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

3113 {
3114 if (n == 0) {
3115 Z3_THROW(exception("a non-zero number of tactics need to be passed to par_or"));
3116 }
3117 array<Z3_tactic> buffer(n);
3118 for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];
3119 return tactic(tactics[0u].ctx(), Z3_tactic_par_or(tactics[0u].ctx(), n, buffer.ptr()));
3120 }
Exception used to sign API usage errors.
Definition z3++.h:88
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.
#define Z3_THROW(x)
Definition z3++.h:103

◆ partial_order()

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

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

2272 {
2273 return to_func_decl(a.ctx(), Z3_mk_partial_order(a.ctx(), a, index));
2274 }
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 pbeq ( expr_vector const &  es,
int const *  coeffs,
int  bound 
)
inline

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

2413 {
2414 assert(es.size() > 0);
2415 context& ctx = es[0u].ctx();
2416 array<Z3_ast> _es(es);
2417 Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
2418 ctx.check_error();
2419 return expr(ctx, r);
2420 }
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 pbge ( expr_vector const &  es,
int const *  coeffs,
int  bound 
)
inline

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

2405 {
2406 assert(es.size() > 0);
2407 context& ctx = es[0u].ctx();
2408 array<Z3_ast> _es(es);
2409 Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
2410 ctx.check_error();
2411 return expr(ctx, r);
2412 }
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 pble ( expr_vector const &  es,
int const *  coeffs,
int  bound 
)
inline

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

2397 {
2398 assert(es.size() > 0);
2399 context& ctx = es[0u].ctx();
2400 array<Z3_ast> _es(es);
2401 Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
2402 ctx.check_error();
2403 return expr(ctx, r);
2404 }
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 piecewise_linear_order ( sort const &  a,
unsigned  index 
)
inline

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

2275 {
2276 return to_func_decl(a.ctx(), Z3_mk_piecewise_linear_order(a.ctx(), a, index));
2277 }
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 plus ( expr const &  re)
inline

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

4048 {
4050 }
Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re)
Create the regular language re+.

◆ prefixof()

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

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

4024 {
4025 check_context(a, b);
4026 Z3_ast r = Z3_mk_seq_prefix(a.ctx(), a, b);
4027 a.check_error();
4028 return expr(a.ctx(), r);
4029 }
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 pw ( expr const &  a,
expr const &  b 
)
inline

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

1636{ _Z3_MK_BIN_(a, b, Z3_mk_power); }
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 ^ arg2.

◆ pw() [2/3]

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

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

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

◆ pw() [3/3]

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

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

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

◆ range()

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

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

4085 {
4086 check_context(lo, hi);
4087 Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
4088 lo.check_error();
4089 return expr(lo.ctx(), r);
4090 }
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 context::function(), function(), context::function(), function(), context::function(), function(), context::function(), function(), context::function(), function(), context::function(), function(), context::function(), function(), function(), context::function(), context::function(), function(), context::recfun(), recfun(), recfun(), context::recfun(), context::recfun(), context::recfun(), recfun(), context::recfun(), context::recfun(), recfun(), and context::user_propagate_function().

◆ re_complement()

expr re_complement ( expr const &  a)
inline

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

4082 {
4084 }
Z3_ast Z3_API Z3_mk_re_complement(Z3_context c, Z3_ast re)
Create the complement of the regular language re.

◆ re_diff()

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

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

4075 {
4076 check_context(a, b);
4077 context& ctx = a.ctx();
4078 Z3_ast r = Z3_mk_re_diff(ctx, a, b);
4079 ctx.check_error();
4080 return expr(ctx, r);
4081 }
Z3_ast Z3_API Z3_mk_re_diff(Z3_context c, Z3_ast re1, Z3_ast re2)
Create the difference of regular expressions.

◆ re_empty()

expr re_empty ( sort const &  s)
inline

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

4057 {
4058 Z3_ast r = Z3_mk_re_empty(s.ctx(), s);
4059 s.check_error();
4060 return expr(s.ctx(), r);
4061 }
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 re_full ( sort const &  s)
inline

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

4062 {
4063 Z3_ast r = Z3_mk_re_full(s.ctx(), s);
4064 s.check_error();
4065 return expr(s.ctx(), r);
4066 }
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 re_intersect ( expr_vector const &  args)
inline

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

4067 {
4068 assert(args.size() > 0);
4069 context& ctx = args[0u].ctx();
4070 array<Z3_ast> _args(args);
4071 Z3_ast r = Z3_mk_re_intersect(ctx, _args.size(), _args.ptr());
4072 ctx.check_error();
4073 return expr(ctx, r);
4074 }
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 recfun ( char const *  name,
sort const &  d1,
sort const &  d2,
sort const &  range 
)
inline

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

3899 {
3900 return range.ctx().recfun(name, d1, d2, range);
3901 }
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Definition z3++.h:3654

◆ recfun() [2/4]

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

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

3896 {
3897 return range.ctx().recfun(name, d1, range);
3898 }

◆ recfun() [3/4]

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

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

3893 {
3894 return range.ctx().recfun(name, arity, domain, range);
3895 }

◆ recfun() [4/4]

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

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

3890 {
3891 return range.ctx().recfun(name, arity, domain, range);
3892 }

◆ rem() [1/3]

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

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

1656 {
1657 if (a.is_fpa() && b.is_fpa()) {
1659 } else {
1660 _Z3_MK_BIN_(a, b, Z3_mk_rem);
1661 }
1662 }
Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point remainder.
Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 rem arg2.

◆ rem() [2/3]

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

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

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

◆ rem() [3/3]

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

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

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

◆ repeat()

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

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

3097 {
3098 Z3_tactic r = Z3_tactic_repeat(t.ctx(), t, max);
3099 t.check_error();
3100 return tactic(t.ctx(), r);
3101 }
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 reset_params ( )
inline

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

void Z3_API Z3_global_param_reset_all(void)
Restore the value of all global (and module) parameters. This command will not affect already created...

◆ round_fpa_to_closest_integer()

expr round_fpa_to_closest_integer ( expr const &  t)
inline

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

2081 {
2082 assert(t.is_fpa());
2083 Z3_ast r = Z3_mk_fpa_round_to_integral(t.ctx(), t.ctx().fpa_rounding_mode(), t);
2084 t.check_error();
2085 return expr(t.ctx(), r);
2086 }
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 sbv_to_fpa ( expr const &  t,
sort  s 
)
inline

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

2060 {
2061 assert(t.is_bv());
2062 Z3_ast r = Z3_mk_fpa_to_fp_signed(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2063 t.check_error();
2064 return expr(t.ctx(), r);
2065 }
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 3903 of file z3++.h.

3903 {
3904 check_context(a, i);
3905 Z3_ast r = Z3_mk_select(a.ctx(), a, i);
3906 a.check_error();
3907 return expr(a.ctx(), r);
3908 }
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[](), expr::operator[](), and select().

◆ select() [2/3]

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

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

3912 {
3913 check_context(a, i);
3914 array<Z3_ast> idxs(i);
3915 Z3_ast r = Z3_mk_select_n(a.ctx(), a, idxs.size(), idxs.ptr());
3916 a.check_error();
3917 return expr(a.ctx(), r);
3918 }
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 select ( expr const &  a,
int  i 
)
inline

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

3909 {
3910 return select(a, a.ctx().num_val(i, a.get_sort().array_domain()));
3911 }
expr select(expr const &a, expr const &i)
forward declarations
Definition z3++.h:3903

◆ set_add()

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

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

3969 {
3970 MK_EXPR2(Z3_mk_set_add, s, e);
3971 }
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 set_complement ( expr const &  a)
inline

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

3997 {
3999 }
Z3_ast Z3_API Z3_mk_set_complement(Z3_context c, Z3_ast arg)
Take the complement of a set.

◆ set_del()

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

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

3973 {
3974 MK_EXPR2(Z3_mk_set_del, s, e);
3975 }
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 set_difference ( expr const &  a,
expr const &  b 
)
inline

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

3993 {
3995 }
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 set_intersect ( expr const &  a,
expr const &  b 
)
inline

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

3985 {
3986 check_context(a, b);
3987 Z3_ast es[2] = { a, b };
3988 Z3_ast r = Z3_mk_set_intersect(a.ctx(), 2, es);
3989 a.check_error();
3990 return expr(a.ctx(), r);
3991 }
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 set_member ( expr const &  s,
expr const &  e 
)
inline

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

4001 {
4003 }
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 set_param ( char const *  param,
bool  value 
)
inline

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

81{ Z3_global_param_set(param, value ? "true" : "false"); }
void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value)
Set a global (or module) parameter. This setting is shared by all Z3 contexts.

◆ set_param() [2/3]

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

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

80{ Z3_global_param_set(param, value); }

◆ set_param() [3/3]

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

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

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

◆ set_subset()

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

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

4005 {
4007 }
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 set_union ( expr const &  a,
expr const &  b 
)
inline

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

3977 {
3978 check_context(a, b);
3979 Z3_ast es[2] = { a, b };
3980 Z3_ast r = Z3_mk_set_union(a.ctx(), 2, es);
3981 a.check_error();
3982 return expr(a.ctx(), r);
3983 }
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 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 2267 of file z3++.h.

2267{ return to_expr(a.ctx(), Z3_mk_sign_ext(a.ctx(), i, a)); }
Z3_ast Z3_API Z3_mk_sign_ext(Z3_context c, unsigned i, Z3_ast t1)
Sign-extend of the given bit-vector to the (signed) equivalent bit-vector of size m+i,...

◆ sge() [1/3]

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

signed greater than or equal to operator for bitvectors.

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

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

Referenced by sge(), and sge().

◆ sge() [2/3]

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

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

2141{ return sge(a, a.ctx().num_val(b, a.get_sort())); }
expr sge(expr const &a, expr const &b)
signed greater than or equal to operator for bitvectors.
Definition z3++.h:2140

◆ sge() [3/3]

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

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

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

◆ sgt() [1/3]

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

signed greater than operator for bitvectors.

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

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

Referenced by sgt(), and sgt().

◆ sgt() [2/3]

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

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

2147{ return sgt(a, a.ctx().num_val(b, a.get_sort())); }
expr sgt(expr const &a, expr const &b)
signed greater than operator for bitvectors.
Definition z3++.h:2146

◆ sgt() [3/3]

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

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

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

◆ shl() [1/3]

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

shift left operator for bitvectors

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

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

Referenced by shl(), and shl().

◆ shl() [2/3]

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

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

2207{ return shl(a, a.ctx().num_val(b, a.get_sort())); }
expr shl(expr const &a, expr const &b)
shift left operator for bitvectors
Definition z3++.h:2206

◆ shl() [3/3]

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

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

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

◆ sle() [1/3]

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

signed less than or equal to operator for bitvectors.

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

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

Referenced by sle(), and sle().

◆ sle() [2/3]

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

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

2129{ return sle(a, a.ctx().num_val(b, a.get_sort())); }
expr sle(expr const &a, expr const &b)
signed less than or equal to operator for bitvectors.
Definition z3++.h:2128

◆ sle() [3/3]

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

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

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

◆ slt() [1/3]

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

signed less than operator for bitvectors.

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

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

Referenced by slt(), and slt().

◆ slt() [2/3]

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

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

2135{ return slt(a, a.ctx().num_val(b, a.get_sort())); }
expr slt(expr const &a, expr const &b)
signed less than operator for bitvectors.
Definition z3++.h:2134

◆ slt() [3/3]

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

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

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

◆ smod() [1/3]

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

signed modulus operator for bitvectors

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

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

Referenced by smod(), and smod().

◆ smod() [2/3]

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

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

2193{ return smod(a, a.ctx().num_val(b, a.get_sort())); }
expr smod(expr const &a, expr const &b)
signed modulus operator for bitvectors
Definition z3++.h:2192

◆ smod() [3/3]

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

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

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

◆ sqrt()

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

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

2014 {
2015 check_context(a, rm);
2016 assert(a.is_fpa());
2017 Z3_ast r = Z3_mk_fpa_sqrt(a.ctx(), rm, a);
2018 a.check_error();
2019 return expr(a.ctx(), r);
2020 }
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 srem ( expr const &  a,
expr const &  b 
)
inline

signed remainder operator for bitvectors

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

2185{ return to_expr(a.ctx(), Z3_mk_bvsrem(a.ctx(), a, b)); }
Z3_ast Z3_API Z3_mk_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows dividend).

Referenced by srem(), and srem().

◆ srem() [2/3]

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

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

2186{ return srem(a, a.ctx().num_val(b, a.get_sort())); }
expr srem(expr const &a, expr const &b)
signed remainder operator for bitvectors
Definition z3++.h:2185

◆ srem() [3/3]

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

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

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

◆ star()

expr star ( expr const &  re)
inline

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

4054 {
4056 }
Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re)
Create the regular language re*.

◆ store() [1/5]

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

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

3920 {
3921 check_context(a, i); check_context(a, v);
3922 Z3_ast r = Z3_mk_store(a.ctx(), a, i, v);
3923 a.check_error();
3924 return expr(a.ctx(), r);
3925 }
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(), and store().

◆ store() [2/5]

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

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

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

◆ store() [3/5]

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

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

3932 {
3933 check_context(a, i); check_context(a, v);
3934 array<Z3_ast> idxs(i);
3935 Z3_ast r = Z3_mk_store_n(a.ctx(), a, idxs.size(), idxs.ptr(), v);
3936 a.check_error();
3937 return expr(a.ctx(), r);
3938 }
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 store ( expr const &  a,
int  i,
expr const &  v 
)
inline

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

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

◆ store() [5/5]

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

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

3929 {
3930 return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
3931 }

◆ suffixof()

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

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

4018 {
4019 check_context(a, b);
4020 Z3_ast r = Z3_mk_seq_suffix(a.ctx(), a, b);
4021 a.check_error();
4022 return expr(a.ctx(), r);
4023 }
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 sum ( expr_vector const &  args)
inline

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

2437 {
2438 assert(args.size() > 0);
2439 context& ctx = args[0u].ctx();
2440 array<Z3_ast> _args(args);
2441 Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
2442 ctx.check_error();
2443 return expr(ctx, r);
2444 }

◆ to_check_result()

check_result to_check_result ( Z3_lbool  l)
inline

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

147 {
148 if (l == Z3_L_TRUE) return sat;
149 else if (l == Z3_L_FALSE) return unsat;
150 return unknown;
151 }
@ Z3_L_TRUE
Definition z3_api.h:64
@ Z3_L_FALSE
Definition z3_api.h:62

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

◆ to_expr()

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

2106 {
2107 c.check_error();
2108 assert(Z3_get_ast_kind(c, a) == Z3_APP_AST ||
2110 Z3_get_ast_kind(c, a) == Z3_VAR_AST ||
2112 return expr(c, a);
2113 }
Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a)
Return the kind of the given AST.
@ Z3_APP_AST
Definition z3_api.h:143
@ Z3_VAR_AST
Definition z3_api.h:144
@ Z3_NUMERAL_AST
Definition z3_api.h:142
@ Z3_QUANTIFIER_AST
Definition z3_api.h:145

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 to_func_decl ( context c,
Z3_func_decl  f 
)
inline

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

2120 {
2121 c.check_error();
2122 return func_decl(c, f);
2123 }
Function declaration (aka function definition). It is the signature of interpreted and uninterpreted ...
Definition z3++.h:759

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

◆ to_re()

expr to_re ( expr const &  s)
inline

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

4042 {
4044 }
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 to_real ( expr const &  a)
inline

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

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

◆ to_sort()

sort to_sort ( context c,
Z3_sort  s 
)
inline

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

2115 {
2116 c.check_error();
2117 return sort(c, s);
2118 }
A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort.
Definition z3++.h:656

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

◆ tree_order()

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

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

2278 {
2279 return to_func_decl(a.ctx(), Z3_mk_tree_order(a.ctx(), a, index));
2280 }
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 try_for ( tactic const &  t,
unsigned  ms 
)
inline

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

3108 {
3109 Z3_tactic r = Z3_tactic_try_for(t.ctx(), t, ms);
3110 t.check_error();
3111 return tactic(t.ctx(), r);
3112 }
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 ubv_to_fpa ( expr const &  t,
sort  s 
)
inline

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

2067 {
2068 assert(t.is_bv());
2069 Z3_ast r = Z3_mk_fpa_to_fp_unsigned(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2070 t.check_error();
2071 return expr(t.ctx(), r);
2072 }
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 udiv ( expr const &  a,
expr const &  b 
)
inline

unsigned division operator for bitvectors.

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

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

Referenced by udiv(), and udiv().

◆ udiv() [2/3]

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

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

2179{ return udiv(a, a.ctx().num_val(b, a.get_sort())); }
expr udiv(expr const &a, expr const &b)
unsigned division operator for bitvectors.
Definition z3++.h:2178

◆ udiv() [3/3]

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

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

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

◆ uge() [1/3]

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

unsigned greater than or equal to operator for bitvectors.

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

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

Referenced by uge(), and uge().

◆ uge() [2/3]

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

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

2167{ return uge(a, a.ctx().num_val(b, a.get_sort())); }
expr uge(expr const &a, expr const &b)
unsigned greater than or equal to operator for bitvectors.
Definition z3++.h:2166

◆ uge() [3/3]

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

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

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

◆ ugt() [1/3]

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

unsigned greater than operator for bitvectors.

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

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

Referenced by ugt(), and ugt().

◆ ugt() [2/3]

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

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

2173{ return ugt(a, a.ctx().num_val(b, a.get_sort())); }
expr ugt(expr const &a, expr const &b)
unsigned greater than operator for bitvectors.
Definition z3++.h:2172

◆ ugt() [3/3]

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

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

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

◆ ule() [1/3]

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

unsigned less than or equal to operator for bitvectors.

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

2154{ return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }
Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than or equal to.

Referenced by ule(), and ule().

◆ ule() [2/3]

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

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

2155{ return ule(a, a.ctx().num_val(b, a.get_sort())); }
expr ule(expr const &a, expr const &b)
unsigned less than or equal to operator for bitvectors.
Definition z3++.h:2154

◆ ule() [3/3]

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

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

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

◆ ult() [1/3]

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

unsigned less than operator for bitvectors.

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

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

Referenced by ult(), and ult().

◆ ult() [2/3]

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

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

2161{ return ult(a, a.ctx().num_val(b, a.get_sort())); }
expr ult(expr const &a, expr const &b)
unsigned less than operator for bitvectors.
Definition z3++.h:2160

◆ ult() [3/3]

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

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

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

◆ urem() [1/3]

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

unsigned reminder operator for bitvectors

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

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

Referenced by urem(), and urem().

◆ urem() [2/3]

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

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

2200{ return urem(a, a.ctx().num_val(b, a.get_sort())); }
expr urem(expr const &a, expr const &b)
unsigned reminder operator for bitvectors
Definition z3++.h:2199

◆ urem() [3/3]

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

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

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

◆ when()

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

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

3414 {
3415 check_context(p, t);
3416 Z3_tactic r = Z3_tactic_when(t.ctx(), p, t);
3417 t.check_error();
3418 return tactic(t.ctx(), r);
3419 }
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() [1/2]

simplifier with ( simplifier const &  t,
params const &  p 
)
inline

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

3164 {
3165 Z3_simplifier r = Z3_simplifier_using_params(t.ctx(), t, p);
3166 t.check_error();
3167 return simplifier(t.ctx(), r);
3168 }
Z3_simplifier Z3_API Z3_simplifier_using_params(Z3_context c, Z3_simplifier t, Z3_params p)
Return a simplifier that applies t using the given set of parameters.

◆ with() [2/2]

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

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

3103 {
3104 Z3_tactic r = Z3_tactic_using_params(t.ctx(), t, p);
3105 t.check_error();
3106 return tactic(t.ctx(), r);
3107 }
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 xnor ( expr const &  a,
expr const &  b 
)
inline

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

1949{ if (a.is_bool()) return !(a ^ b); check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise xnor.

◆ zext()

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

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