Z3
Loading...
Searching...
No Matches
Data Structures | Public Member Functions | Friends
expr Class Reference

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...

#include <z3++.h>

Inheritance diagram for expr:

Data Structures

class  iterator

Public Member Functions

 expr (context &c)
 expr (context &c, Z3_ast n)
sort get_sort () const
 Return the sort of this expression.
bool is_bool () const
 Return true if this is a Boolean expression.
bool is_int () const
 Return true if this is an integer expression.
bool is_real () const
 Return true if this is a real expression.
bool is_complex () const
 Return true if this expression is Complex.
bool is_arith () const
 Return true if this is an Integer, Real, or Complex expression.
bool is_bv () const
 Return true if this is a Bit-vector expression.
bool is_array () const
 Return true if this is a Array expression.
bool is_datatype () const
 Return true if this is a Datatype expression.
bool is_relation () const
 Return true if this is a Relation expression.
bool is_seq () const
 Return true if this is a sequence expression.
bool is_re () const
 Return true if this is a regular expression.
bool is_finite_field () const
 Return true if this is a Finite-domain expression.
bool is_finite_domain () const
bool is_fpa () const
 Return true if this is a FloatingPoint expression. .
bool is_numeral () const
 Return true if this expression is a numeral. Specialized functions also return representations for the numerals as small integers, 64 bit integers or rational or decimal strings.
bool is_numeral_i64 (int64_t &i) const
bool is_numeral_u64 (uint64_t &i) const
bool is_numeral_i (int &i) const
bool is_numeral_u (unsigned &i) const
bool is_numeral (std::string &s) const
bool is_numeral (std::string &s, unsigned precision) const
bool is_numeral (double &d) const
bool as_binary (std::string &s) const
double as_double () const
uint64_t as_uint64 () const
int64_t as_int64 () const
bool is_app () const
 Return true if this expression is an application.
bool is_const () const
 Return true if this expression is a constant (i.e., an application with 0 arguments).
bool is_quantifier () const
 Return true if this expression is a quantifier.
bool is_forall () const
 Return true if this expression is a universal quantifier.
bool is_exists () const
 Return true if this expression is an existential quantifier.
bool is_lambda () const
 Return true if this expression is a lambda expression.
bool is_var () const
 Return true if this expression is a variable.
bool is_algebraic () const
 Return true if expression is an algebraic number.
bool is_well_sorted () const
 Return true if this expression is well sorted (aka type correct).
expr mk_is_inf () const
 Return Boolean expression to test for whether an FP expression is inf.
expr mk_is_nan () const
 Return Boolean expression to test for whether an FP expression is a NaN.
expr mk_is_normal () const
 Return Boolean expression to test for whether an FP expression is a normal.
expr mk_is_subnormal () const
 Return Boolean expression to test for whether an FP expression is a subnormal.
expr mk_is_zero () const
 Return Boolean expression to test for whether an FP expression is a zero.
expr mk_to_ieee_bv () const
 Convert this fpa into an IEEE BV.
expr mk_from_ieee_bv (sort const &s) const
 Convert this IEEE BV into a fpa.
std::string get_decimal_string (int precision) const
 Return string representation of numeral or algebraic number This method assumes the expression is numeral or algebraic.
expr algebraic_lower (unsigned precision) const
expr algebraic_upper (unsigned precision) const
expr_vector algebraic_poly () const
 Return coefficients for p of an algebraic number (root-obj p i).
unsigned algebraic_i () const
 Return i of an algebraic number (root-obj p i).
unsigned id () const
 retrieve unique identifier for expression.
int get_numeral_int () const
 Return int value of numeral, throw if result cannot fit in machine int.
unsigned get_numeral_uint () const
 Return uint value of numeral, throw if result cannot fit in machine uint.
int64_t get_numeral_int64 () const
 Return int64_t value of numeral, throw if result cannot fit in int64_t.
uint64_t get_numeral_uint64 () const
 Return uint64_t value of numeral, throw if result cannot fit in uint64_t.
Z3_lbool bool_value () const
expr numerator () const
expr denominator () const
bool is_string_value () const
 Return true if this expression is a string literal. The string can be accessed using get_string() and get_escaped_string().
std::string get_string () const
 for a string value expression return an escaped string value.
std::u32string get_u32string () const
 for a string value expression return an unespaced string value.
 operator Z3_app () const
func_decl decl () const
 Return the declaration associated with this application. This method assumes the expression is an application.
unsigned num_args () const
 Return the number of arguments in this application. This method assumes the expression is an application.
expr arg (unsigned i) const
 Return the i-th argument of this application. This method assumes the expression is an application.
expr_vector args () const
 Return a vector of all the arguments of this application. This method assumes the expression is an application.
expr update (expr_vector const &args) const
 Update the arguments of this application. Return a new expression with the same function declaration and updated arguments. The number of new arguments must match the current number of arguments.
expr update_field (func_decl const &field_access, expr const &new_value) const
 Update a datatype field. Return a new datatype expression with the specified field updated to the new value. The remaining fields are unchanged.
expr body () const
 Return the 'body' of this quantifier.
bool is_true () const
bool is_false () const
bool is_not () const
bool is_and () const
bool is_or () const
bool is_xor () const
bool is_implies () const
bool is_eq () const
bool is_ite () const
bool is_distinct () const
expr rotate_left (unsigned i) const
expr rotate_right (unsigned i) const
expr ext_rotate_left (expr const &n) const
expr ext_rotate_right (expr const &n) const
expr repeat (unsigned i) const
expr extract (unsigned hi, unsigned lo) const
expr bit2bool (unsigned i) const
unsigned lo () const
unsigned hi () const
expr extract (expr const &offset, expr const &length) const
 sequence and regular expression operations.
expr replace (expr const &src, expr const &dst) const
expr unit () const
expr contains (expr const &s) const
expr at (expr const &index) const
expr nth (expr const &index) const
expr length () const
expr power (expr const &n) const
expr stoi () const
expr itos () const
expr ubvtos () const
expr sbvtos () const
expr char_to_int () const
expr char_to_bv () const
expr char_from_bv () const
expr is_digit () const
expr loop (unsigned lo)
 create a looping regular expression.
expr loop (unsigned lo, unsigned hi)
expr operator[] (expr const &index) const
expr operator[] (expr_vector const &index) const
expr simplify () const
 Return a simplified version of this expression.
expr simplify (params const &p) const
 Return a simplified version of this expression. The parameter p is a set of parameters for the Z3 simplifier.
expr substitute (expr_vector const &src, expr_vector const &dst)
 Apply substitution. Replace src expressions by dst.
expr substitute (expr_vector const &dst)
 Apply substitution. Replace bound variables by expressions.
expr substitute (func_decl_vector const &funs, expr_vector const &bodies)
 Apply function substitution by macro definitions.
iterator begin ()
iterator end ()
Public Member Functions inherited from ast
 ast (context &c)
 ast (context &c, Z3_ast n)
 ast (ast const &s)
 ~ast () override
 operator Z3_ast () const
 operator bool () const
ast & operator= (ast const &s)
Z3_ast_kind kind () const
unsigned hash () const
std::string to_string () const
Public Member Functions inherited from object
 object (context &c)
virtual ~object ()=default
context & ctx () const
Z3_error_code check_error () const

Friends

expr operator! (expr const &a)
 Return an expression representing not(a).
expr operator&& (expr const &a, expr const &b)
 Return an expression representing a and b.
expr operator&& (expr const &a, bool b)
 Return an expression representing a and b. The C++ Boolean value b is automatically converted into a Z3 Boolean constant.
expr operator&& (bool a, expr const &b)
 Return an expression representing a and b. The C++ Boolean value a is automatically converted into a Z3 Boolean constant.
expr operator|| (expr const &a, expr const &b)
 Return an expression representing a or b.
expr operator|| (expr const &a, bool b)
 Return an expression representing a or b. The C++ Boolean value b is automatically converted into a Z3 Boolean constant.
expr operator|| (bool a, expr const &b)
 Return an expression representing a or b. The C++ Boolean value a is automatically converted into a Z3 Boolean constant.
expr implies (expr const &a, expr const &b)
expr implies (expr const &a, bool b)
expr implies (bool a, expr const &b)
expr mk_or (expr_vector const &args)
expr mk_xor (expr_vector const &args)
expr mk_and (expr_vector const &args)
expr ite (expr const &c, expr const &t, expr const &e)
 Create the if-then-else expression ite(c, t, e).
expr distinct (expr_vector const &args)
expr concat (expr const &a, expr const &b)
expr concat (expr_vector const &args)
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 sum (expr_vector const &args)
expr operator* (expr const &a, expr const &b)
expr operator* (expr const &a, int b)
expr operator* (int 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 rem (expr const &a, expr const &b)
expr rem (expr const &a, int b)
expr rem (int a, expr const &b)
expr is_int (expr const &e)
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, 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 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 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 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 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)
 FloatingPoint fused multiply-add.
expr fpa_fp (expr const &sgn, expr const &exp, expr const &sig)
 Create an expression of FloatingPoint sort from three bit-vector expressions.
expr fpa_to_sbv (expr const &t, unsigned sz)
 Conversion of a floating-point term into a signed bit-vector.
expr fpa_to_ubv (expr const &t, unsigned sz)
 Conversion of a floating-point term into an unsigned bit-vector.
expr sbv_to_fpa (expr const &t, sort s)
 Conversion of a signed bit-vector term into a floating-point.
expr ubv_to_fpa (expr const &t, sort s)
 Conversion of an unsigned bit-vector term into a floating-point.
expr fpa_to_fpa (expr const &t, sort s)
 Conversion of a floating-point term into another floating-point.
expr round_fpa_to_closest_integer (expr const &t)
 Round a floating-point term into its closest integer.
expr range (expr const &lo, expr const &hi)

Additional Inherited Members

Protected Attributes inherited from ast
Z3_ast m_ast
Protected Attributes inherited from object
context * m_ctx

Detailed Description

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.

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

Constructor & Destructor Documentation

◆ expr() [1/2]

expr ( context & c)
inline

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

1005:ast(c) {}

Referenced by abs, algebraic_lower(), algebraic_upper(), arg(), func_entry::arg(), z3::array_default(), z3::array_ext(), z3::as_array(), goal::as_expr(), at(), atleast, atmost, bit2bool(), body(), context::bool_val(), bv2int, context::bv_val(), context::bv_val(), context::bv_val(), context::bv_val(), context::bv_val(), context::bv_val(), bvadd_no_overflow, bvadd_no_underflow, bvmul_no_overflow, bvmul_no_underflow, bvneg_no_overflow, bvredand, bvredor, bvsdiv_no_overflow, bvsub_no_overflow, bvsub_no_underflow, char_from_bv(), char_to_bv(), char_to_int(), z3::complex(), concat, concat, solver::congruence_explain(), solver::congruence_next(), solver::congruence_root(), context::constant(), contains(), denominator(), distinct, func_interp::else_value(), z3::empty(), model::eval(), z3::exists(), z3::exists(), z3::exists(), z3::exists(), z3::exists(), ext_rotate_left(), ext_rotate_right(), extract(), extract(), z3::finite_set_empty(), fma, z3::foldl(), z3::foldli(), z3::forall(), z3::forall(), z3::forall(), z3::forall(), z3::forall(), fp_eq, fpa_fp, context::fpa_inf(), context::fpa_nan(), context::fpa_rounding_mode(), fpa_to_fpa, fpa_to_sbv, fpa_to_ubv, context::fpa_val(), context::fpa_val(), fixedpoint::get_answer(), model::get_const_interp(), fixedpoint::get_cover_delta(), parameter::get_expr(), z3::imag_part(), implies, implies, implies, z3::indexof(), int2bv, context::int_val(), context::int_val(), context::int_val(), context::int_val(), context::int_val(), is_digit(), is_int, ite, expr::iterator::iterator(), itos(), z3::lambda(), z3::lambda(), z3::lambda(), z3::lambda(), z3::lambda(), z3::last_indexof(), length(), loop(), loop(), optimize::lower(), z3::map(), z3::mapi(), max, min, mk_and, mk_from_ieee_bv(), mk_is_inf(), mk_is_nan(), mk_is_normal(), mk_is_subnormal(), mk_is_zero(), mk_or, mk_to_ieee_bv(), mk_xor, mod, mod, mod, nand, nor, nth(), context::num_val(), numerator(), operator!, operator!=, operator!=, operator!=, operator&, operator&, operator&, operator&&, operator&&, operator&&, cast_ast< expr >::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), expr::iterator::operator*(), operator*, operator*, operator*, operator+, operator+, operator+, operator-, operator-, operator-, operator-, operator/, operator/, operator/, operator<, operator<, operator<, operator<=, operator<=, operator<=, operator==, operator==, operator==, operator>, operator>, operator>, operator>=, operator>=, operator>=, operator[](), operator[](), goal::operator[](), operator^, operator^, operator^, operator|, operator|, operator|, operator||, operator||, operator||, operator~, pbeq, pbge, pble, power(), z3::prefixof(), solver::proof(), pw, pw, pw, z3::qe_lite(), z3::qe_model_project(), z3::qe_model_project_skolem(), z3::qe_model_project_with_witness(), range, z3::re_diff(), z3::re_empty(), z3::re_full(), z3::re_intersect(), z3::real_part(), context::real_val(), context::real_val(), context::real_val(), context::real_val(), context::real_val(), context::real_val(), rem, rem, rem, repeat(), replace(), rotate_left(), rotate_right(), round_fpa_to_closest_integer, sbv_to_fpa, sbvtos(), z3::select(), z3::select(), z3::set_intersect(), z3::set_union(), simplify(), simplify(), sqrt, stoi(), z3::store(), z3::store(), context::string_val(), context::string_val(), context::string_val(), context::string_val(), substitute(), substitute(), substitute(), z3::suffixof(), sum, z3::to_expr(), z3::to_real(), ubv_to_fpa, ubvtos(), unit(), update(), update_field(), optimize::upper(), func_entry::value(), context::variable(), and xnor.

◆ expr() [2/2]

expr ( context & c,
Z3_ast n )
inline

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

1006:ast(c, reinterpret_cast<Z3_ast>(n)) {}

Member Function Documentation

◆ algebraic_i()

unsigned algebraic_i ( ) const
inline

Return i of an algebraic number (root-obj p i).

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

1242 {
1243 assert(is_algebraic());
1244 unsigned i = Z3_algebraic_get_i(ctx(), m_ast);
1245 check_error();
1246 return i;
1247 }
Z3_algebraic_get_i
unsigned Z3_API Z3_algebraic_get_i(Z3_context c, Z3_ast a)
Return which root of the polynomial the algebraic number represents.

◆ algebraic_lower()

expr algebraic_lower ( unsigned precision) const
inline

Retrieve lower and upper bounds for algebraic numerals based on a decimal precision

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

1215 {
1216 assert(is_algebraic());
1217 Z3_ast r = Z3_get_algebraic_number_lower(ctx(), m_ast, precision);
1218 check_error();
1219 return expr(ctx(), r);
1220 }
Z3_get_algebraic_number_lower
Z3_ast Z3_API Z3_get_algebraic_number_lower(Z3_context c, Z3_ast a, unsigned precision)
Return a lower bound for the given real algebraic number. The interval isolating the number is smalle...

◆ algebraic_poly()

expr_vector algebraic_poly ( ) const
inline

Return coefficients for p of an algebraic number (root-obj p i).

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

1232 {
1233 assert(is_algebraic());
1234 Z3_ast_vector r = Z3_algebraic_get_poly(ctx(), m_ast);
1235 check_error();
1236 return expr_vector(ctx(), r);
1237 }
Z3_algebraic_get_poly
Z3_ast_vector Z3_API Z3_algebraic_get_poly(Z3_context c, Z3_ast a)
Return the coefficients of the defining polynomial.
z3::expr_vector
ast_vector_tpl< expr > expr_vector
Definition z3++.h:77

◆ algebraic_upper()

expr algebraic_upper ( unsigned precision) const
inline

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

1222 {
1223 assert(is_algebraic());
1224 Z3_ast r = Z3_get_algebraic_number_upper(ctx(), m_ast, precision);
1225 check_error();
1226 return expr(ctx(), r);
1227 }
Z3_get_algebraic_number_upper
Z3_ast Z3_API Z3_get_algebraic_number_upper(Z3_context c, Z3_ast a, unsigned precision)
Return a upper bound for the given real algebraic number. The interval isolating the number is smalle...

◆ arg()

expr arg ( unsigned i) const
inline

Return the i-th argument of this application. This method assumes the expression is an application.

Precondition
is_app()
i < num_args()

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

1403{ Z3_ast r = Z3_get_app_arg(ctx(), *this, i); check_error(); return expr(ctx(), r); }
Z3_get_app_arg
Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i)
Return the i-th argument of the given application.

Referenced by AstRef::__bool__(), args(), and expr::iterator::operator*().

◆ args()

expr_vector args ( ) const
inline

Return a vector of all the arguments of this application. This method assumes the expression is an application.

Precondition
is_app()

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

1410 {
1411 expr_vector vec(ctx());
1412 unsigned argCnt = num_args();
1413 for (unsigned i = 0; i < argCnt; ++i)
1414 vec.push_back(arg(i));
1415 return vec;
1416 }

Referenced by concat, distinct, mk_and, mk_or, mk_xor, operator!=, operator&&, operator*, operator+, operator-, operator||, sum, and update().

◆ as_binary()

bool as_binary ( std::string & s) const
inline

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

1084{ if (!is_numeral()) return false; s = Z3_get_numeral_binary_string(ctx(), m_ast); check_error(); return true; }
Z3_get_numeral_binary_string
Z3_string Z3_API Z3_get_numeral_binary_string(Z3_context c, Z3_ast a)
Return numeral value, as a binary string of a numeric constant term.

◆ as_double()

double as_double ( ) const
inline

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

1086{ double d = 0; is_numeral(d); return d; }

◆ as_int64()

int64_t as_int64 ( ) const
inline

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

1088{ int64_t r = 0; is_numeral_i64(r); return r; }

◆ as_uint64()

uint64_t as_uint64 ( ) const
inline

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

1087{ uint64_t r = 0; is_numeral_u64(r); return r; }

◆ at()

expr at ( expr const & index) const
inline

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

1706 {
1707 check_context(*this, index);
1708 Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
1709 check_error();
1710 return expr(ctx(), r);
1711 }
Z3_mk_seq_at
Z3_ast Z3_API Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index)
Retrieve from s the unit sequence positioned at position index. The sequence is empty if the index is...
z3::check_context
void check_context(object const &a, object const &b)
Definition z3++.h:571

◆ begin()

iterator begin ( )
inline

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

1841{ return iterator(*this, 0); }

◆ bit2bool()

expr bit2bool ( unsigned i) const
inline

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

1636{ Z3_ast r = Z3_mk_bit2bool(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
Z3_mk_bit2bool
Z3_ast Z3_API Z3_mk_bit2bool(Z3_context c, unsigned i, Z3_ast t1)
Extracts the bit at position i of a bit-vector and yields a boolean.

◆ body()

expr body ( ) const
inline

Return the 'body' of this quantifier.

Precondition
is_quantifier()

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

1444{ assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }
Z3_get_quantifier_body
Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)
Return body of quantifier.
z3py.is_quantifier
is_quantifier(a)
Definition z3py.py:2344

◆ bool_value()

Z3_lbool bool_value ( ) const
inline

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

1328 {
1329 return Z3_get_bool_value(ctx(), m_ast);
1330 }
Z3_get_bool_value
Z3_lbool Z3_API Z3_get_bool_value(Z3_context c, Z3_ast a)
Return Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF otherwise.

◆ char_from_bv()

expr char_from_bv ( ) const
inline

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

1759 {
1760 Z3_ast r = Z3_mk_char_from_bv(ctx(), *this);
1761 check_error();
1762 return expr(ctx(), r);
1763 }
Z3_mk_char_from_bv
Z3_ast Z3_API Z3_mk_char_from_bv(Z3_context c, Z3_ast bv)
Create a character from a bit-vector (code point).

◆ char_to_bv()

expr char_to_bv ( ) const
inline

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

1754 {
1755 Z3_ast r = Z3_mk_char_to_bv(ctx(), *this);
1756 check_error();
1757 return expr(ctx(), r);
1758 }
Z3_mk_char_to_bv
Z3_ast Z3_API Z3_mk_char_to_bv(Z3_context c, Z3_ast ch)
Create a bit-vector (code point) from character.

◆ char_to_int()

expr char_to_int ( ) const
inline

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

1749 {
1750 Z3_ast r = Z3_mk_char_to_int(ctx(), *this);
1751 check_error();
1752 return expr(ctx(), r);
1753 }
Z3_mk_char_to_int
Z3_ast Z3_API Z3_mk_char_to_int(Z3_context c, Z3_ast ch)
Create an integer (code point) from character.

◆ contains()

expr contains ( expr const & s) const
inline

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

1700 {
1701 check_context(*this, s);
1702 Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
1703 check_error();
1704 return expr(ctx(), r);
1705 }
Z3_mk_seq_contains
Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee)
Check if container contains containee.

◆ decl()

func_decl decl ( ) const
inline

Return the declaration associated with this application. This method assumes the expression is an application.

Precondition
is_app()

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

1388{ Z3_func_decl f = Z3_get_app_decl(ctx(), *this); check_error(); return func_decl(ctx(), f); }
Z3_get_app_decl
Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a)
Return the declaration of a constant or function application.

Referenced by hi(), is_and(), is_distinct(), is_eq(), is_false(), is_implies(), is_ite(), is_not(), is_or(), is_true(), is_xor(), and lo().

◆ denominator()

expr denominator ( ) const
inline

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

1340 {
1341 assert(is_numeral());
1342 Z3_ast r = Z3_get_denominator(ctx(), m_ast);
1343 check_error();
1344 return expr(ctx(),r);
1345 }
Z3_get_denominator
Z3_ast Z3_API Z3_get_denominator(Z3_context c, Z3_ast a)
Return the denominator (as a numeral AST) of a numeral AST of sort Real.

◆ end()

iterator end ( )
inline

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

1842{ return iterator(*this, is_app() ? num_args() : 0); }
z3py.is_app
is_app(a)
Definition z3py.py:1395

◆ ext_rotate_left()

expr ext_rotate_left ( expr const & n) const
inline

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

1623{ Z3_ast r = Z3_mk_ext_rotate_left(ctx(), *this, n); ctx().check_error(); return expr(ctx(), r); }
Z3_mk_ext_rotate_left
Z3_ast Z3_API Z3_mk_ext_rotate_left(Z3_context c, Z3_ast t1, Z3_ast t2)
Rotate bits of t1 to the left t2 times.

◆ ext_rotate_right()

expr ext_rotate_right ( expr const & n) const
inline

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

1624{ Z3_ast r = Z3_mk_ext_rotate_right(ctx(), *this, n); ctx().check_error(); return expr(ctx(), r); }
Z3_mk_ext_rotate_right
Z3_ast Z3_API Z3_mk_ext_rotate_right(Z3_context c, Z3_ast t1, Z3_ast t2)
Rotate bits of t1 to the right t2 times.

◆ extract() [1/2]

expr extract ( expr const & offset,
expr const & length ) const
inline

sequence and regular expression operations.

  • is overloaded as sequence concatenation and regular expression union. concat is overloaded to handle sequences and regular expressions

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

1685 {
1686 check_context(*this, offset); check_context(offset, length);
1687 Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r);
1688 }
Z3_mk_seq_extract
Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length)
Extract subsequence starting at offset of length.

◆ extract() [2/2]

expr extract ( unsigned hi,
unsigned lo ) const
inline

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

1635{ Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }
Z3_mk_extract
Z3_ast Z3_API Z3_mk_extract(Z3_context c, unsigned high, unsigned low, Z3_ast t1)
Extract the bits high down to low from a bit-vector of size m to yield a new bit-vector of size n,...

◆ get_decimal_string()

std::string get_decimal_string ( int precision) const
inline

Return string representation of numeral or algebraic number This method assumes the expression is numeral or algebraic.

Precondition
is_numeral() || is_algebraic()

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

1207 {
1208 assert(is_numeral() || is_algebraic());
1209 return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
1210 }
Z3_get_numeral_decimal_string
Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision)
Return numeral as a string in decimal notation. The result has at most precision decimal places.

◆ get_numeral_int()

int get_numeral_int ( ) const
inline

Return int value of numeral, throw if result cannot fit in machine int.

It only makes sense to use this function if the caller can ensure that the result is an integer or if exceptions are enabled. If exceptions are disabled, then use the is_numeral_i function.

Precondition
is_numeral()

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

1264 {
1265 int result = 0;
1266 if (!is_numeral_i(result)) {
1267 assert(ctx().enable_exceptions());
1268 if (!ctx().enable_exceptions()) return 0;
1269 Z3_THROW(exception("numeral does not fit in machine int"));
1270 }
1271 return result;
1272 }
Z3_THROW
#define Z3_THROW(x)
Definition z3++.h:134

◆ get_numeral_int64()

int64_t get_numeral_int64 ( ) const
inline

Return int64_t value of numeral, throw if result cannot fit in int64_t.

Precondition
is_numeral()

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

1300 {
1301 assert(is_numeral());
1302 int64_t result = 0;
1303 if (!is_numeral_i64(result)) {
1304 assert(ctx().enable_exceptions());
1305 if (!ctx().enable_exceptions()) return 0;
1306 Z3_THROW(exception("numeral does not fit in machine int64_t"));
1307 }
1308 return result;
1309 }

◆ get_numeral_uint()

unsigned get_numeral_uint ( ) const
inline

Return uint value of numeral, throw if result cannot fit in machine uint.

It only makes sense to use this function if the caller can ensure that the result is an integer or if exceptions are enabled. If exceptions are disabled, then use the is_numeral_u function.

Precondition
is_numeral()

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

1283 {
1284 assert(is_numeral());
1285 unsigned result = 0;
1286 if (!is_numeral_u(result)) {
1287 assert(ctx().enable_exceptions());
1288 if (!ctx().enable_exceptions()) return 0;
1289 Z3_THROW(exception("numeral does not fit in machine uint"));
1290 }
1291 return result;
1292 }

◆ get_numeral_uint64()

uint64_t get_numeral_uint64 ( ) const
inline

Return uint64_t value of numeral, throw if result cannot fit in uint64_t.

Precondition
is_numeral()

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

1317 {
1318 assert(is_numeral());
1319 uint64_t result = 0;
1320 if (!is_numeral_u64(result)) {
1321 assert(ctx().enable_exceptions());
1322 if (!ctx().enable_exceptions()) return 0;
1323 Z3_THROW(exception("numeral does not fit in machine uint64_t"));
1324 }
1325 return result;
1326 }

◆ get_sort()

sort get_sort ( ) const
inline

Return the sort of this expression.

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

1011{ Z3_sort s = Z3_get_sort(*m_ctx, m_ast); check_error(); return sort(*m_ctx, s); }
Z3_get_sort
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.

Referenced by z3::ashr(), z3::ashr(), concat, concat, is_arith(), is_array(), is_bool(), is_bv(), is_complex(), is_datatype(), is_finite_domain(), is_finite_field(), is_fpa(), is_int(), is_re(), is_real(), is_relation(), is_seq(), z3::lshr(), z3::lshr(), mod, mod, operator!=, operator!=, operator&, operator&, operator*, operator*, operator+, operator+, operator-, operator-, operator/, operator/, operator<, operator<, operator<=, operator<=, operator==, operator==, operator>, operator>, operator>=, operator>=, operator^, operator^, operator|, operator|, pw, pw, rem, rem, z3::sdiv(), z3::sdiv(), z3::select(), optimize::set_initial_value(), solver::set_initial_value(), z3::sge(), z3::sge(), z3::sgt(), z3::sgt(), z3::shl(), z3::shl(), z3::sle(), z3::sle(), z3::slt(), z3::slt(), z3::smod(), z3::smod(), z3::srem(), z3::srem(), z3::store(), z3::store(), z3::store(), z3::udiv(), z3::udiv(), z3::uge(), z3::uge(), z3::ugt(), z3::ugt(), z3::ule(), z3::ule(), z3::ult(), z3::ult(), z3::urem(), and z3::urem().

◆ get_string()

std::string get_string ( ) const
inline

for a string value expression return an escaped string value.

Precondition
expression is for a string value.

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

1359 {
1360 assert(is_string_value());
1361 char const* s = Z3_get_string(ctx(), m_ast);
1362 check_error();
1363 return std::string(s);
1364 }
Z3_get_string
Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s)
Retrieve the string constant stored in s. Characters outside the basic printable ASCII range are esca...
z3py.is_string_value
bool is_string_value(Any a)
Definition z3py.py:11916

◆ get_u32string()

std::u32string get_u32string ( ) const
inline

for a string value expression return an unespaced string value.

Precondition
expression is for a string value.

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

1371 {
1372 assert(is_string_value());
1373 unsigned n = Z3_get_string_length(ctx(), m_ast);
1374 std::u32string s;
1375 s.resize(n);
1376 Z3_get_string_contents(ctx(), m_ast, n, (unsigned*)s.data());
1377 return s;
1378 }
Z3_get_string_contents
void Z3_API Z3_get_string_contents(Z3_context c, Z3_ast s, unsigned length, unsigned contents[])
Retrieve the unescaped string constant stored in s.
Z3_get_string_length
unsigned Z3_API Z3_get_string_length(Z3_context c, Z3_ast s)
Retrieve the length of the unescaped string constant stored in s.

◆ hi()

unsigned hi ( ) const
inline

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

1638{ assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 0)); }
Z3_get_decl_num_parameters
unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d)
Return the number of parameters associated with a declaration.
Z3_get_decl_int_parameter
int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the integer value associated with an integer parameter.

Referenced by extract(), loop(), and range.

◆ id()

unsigned id ( ) const
inline

retrieve unique identifier for expression.

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

1252{ unsigned r = Z3_get_ast_id(ctx(), m_ast); check_error(); return r; }
Z3_get_ast_id
unsigned Z3_API Z3_get_ast_id(Z3_context c, Z3_ast t)
Return a unique identifier for t. The identifier is unique up to structural equality....

◆ is_algebraic()

bool is_algebraic ( ) const
inline

Return true if expression is an algebraic number.

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

1124{ return Z3_is_algebraic_number(ctx(), m_ast); }
Z3_is_algebraic_number
bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a)
Return true if the given AST is a real algebraic number.

Referenced by algebraic_i(), algebraic_lower(), algebraic_poly(), algebraic_upper(), and get_decimal_string().

◆ is_and()

bool is_and ( ) const
inline

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

1513{ return is_app() && Z3_OP_AND == decl().decl_kind(); }
Z3_OP_AND
@ Z3_OP_AND
Definition z3_api.h:1005

◆ is_app()

bool is_app ( ) const
inline

Return true if this expression is an application.

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

1094{ return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }
Z3_APP_AST
@ Z3_APP_AST
Definition z3_api.h:146
Z3_NUMERAL_AST
@ Z3_NUMERAL_AST
Definition z3_api.h:145

Referenced by end(), hi(), is_and(), is_const(), is_distinct(), is_eq(), is_false(), is_implies(), is_ite(), is_not(), is_or(), is_true(), is_xor(), lo(), and operator Z3_app().

◆ is_arith()

bool is_arith ( ) const
inline

Return true if this is an Integer, Real, or Complex expression.

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

1030{ return get_sort().is_arith(); }

Referenced by max, min, operator!=, operator!=, operator*, operator+, operator-, operator-, operator/, operator<, operator<=, operator==, operator==, operator>, and operator>=.

◆ is_array()

bool is_array ( ) const
inline

Return true if this is a Array expression.

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

1038{ return get_sort().is_array(); }

Referenced by operator[]().

◆ is_bool()

bool is_bool ( ) const
inline

Return true if this is a Boolean expression.

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

1016{ return get_sort().is_bool(); }

Referenced by optimize::add(), optimize::add(), optimize::add(), solver::add(), solver::add(), optimize::add_soft(), optimize::add_soft(), implies, ite, nand, nor, operator!, operator&, operator&&, operator^, operator|, operator||, and xnor.

◆ is_bv()

bool is_bv ( ) const
inline

Return true if this is a Bit-vector expression.

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

1034{ return get_sort().is_bv(); }

Referenced by bvredand, bvredor, fpa_fp, max, min, mk_from_ieee_bv(), mod, operator!=, operator!=, operator*, operator+, operator-, operator-, operator/, operator<, operator<=, operator==, operator==, operator>, operator>=, sbv_to_fpa, and ubv_to_fpa.

◆ is_complex()

bool is_complex ( ) const
inline

Return true if this expression is Complex.

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

1026{ return get_sort().is_complex(); }

◆ is_const()

bool is_const ( ) const
inline

Return true if this expression is a constant (i.e., an application with 0 arguments).

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

1098{ return is_app() && num_args() == 0; }

Referenced by solver::add().

◆ is_datatype()

bool is_datatype ( ) const
inline

Return true if this is a Datatype expression.

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

1042{ return get_sort().is_datatype(); }

Referenced by update_field().

◆ is_digit()

expr is_digit ( ) const
inline

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

1764 {
1765 Z3_ast r = Z3_mk_char_is_digit(ctx(), *this);
1766 check_error();
1767 return expr(ctx(), r);
1768 }
Z3_mk_char_is_digit
Z3_ast Z3_API Z3_mk_char_is_digit(Z3_context c, Z3_ast ch)
Create a check if the character is a digit.

◆ is_distinct()

bool is_distinct ( ) const
inline

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

1519{ return is_app() && Z3_OP_DISTINCT == decl().decl_kind(); }
Z3_OP_DISTINCT
@ Z3_OP_DISTINCT
Definition z3_api.h:1003

◆ is_eq()

bool is_eq ( ) const
inline

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

1517{ return is_app() && Z3_OP_EQ == decl().decl_kind(); }
Z3_OP_EQ
@ Z3_OP_EQ
Definition z3_api.h:1002

◆ is_exists()

bool is_exists ( ) const
inline

Return true if this expression is an existential quantifier.

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

1111{ return Z3_is_quantifier_exists(ctx(), m_ast); }
Z3_is_quantifier_exists
bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a)
Determine if ast is an existential quantifier.

◆ is_false()

bool is_false ( ) const
inline

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

1511{ return is_app() && Z3_OP_FALSE == decl().decl_kind(); }
Z3_OP_FALSE
@ Z3_OP_FALSE
Definition z3_api.h:1001

◆ is_finite_domain()

bool is_finite_domain ( ) const
inline

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

1065{ return get_sort().is_finite_domain(); }

◆ is_finite_field()

bool is_finite_field ( ) const
inline

Return true if this is a Finite-domain expression.

Remarks
Finite-domain is special kind of interpreted sort: is_bool(), is_bv() and is_finite_domain() are mutually exclusive.

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

1064{ return get_sort().is_finite_field(); }

Referenced by operator!=, operator!=, operator*, operator+, operator-, operator-, operator==, and operator==.

◆ is_forall()

bool is_forall ( ) const
inline

Return true if this expression is a universal quantifier.

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

1107{ return Z3_is_quantifier_forall(ctx(), m_ast); }
Z3_is_quantifier_forall
bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a)
Determine if an ast is a universal quantifier.

◆ is_fpa()

bool is_fpa ( ) const
inline

Return true if this is a FloatingPoint expression. .

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

1069{ return get_sort().is_fpa(); }

Referenced by fma, fp_eq, fpa_to_fpa, fpa_to_sbv, fpa_to_ubv, max, min, mk_is_inf(), mk_is_nan(), mk_is_normal(), mk_is_subnormal(), mk_is_zero(), mk_to_ieee_bv(), operator!=, operator!=, z3::operator!=(), z3::operator!=(), operator*, operator+, operator-, operator-, operator/, operator<, operator<=, operator==, operator==, z3::operator==(), z3::operator==(), operator>, operator>=, rem, round_fpa_to_closest_integer, and sqrt.

◆ is_implies()

bool is_implies ( ) const
inline

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

1516{ return is_app() && Z3_OP_IMPLIES == decl().decl_kind(); }
Z3_OP_IMPLIES
@ Z3_OP_IMPLIES
Definition z3_api.h:1010

◆ is_int()

bool is_int ( ) const
inline

Return true if this is an integer expression.

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

1020{ return get_sort().is_int(); }

Referenced by abs, and is_int.

◆ is_ite()

bool is_ite ( ) const
inline

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

1518{ return is_app() && Z3_OP_ITE == decl().decl_kind(); }
Z3_OP_ITE
@ Z3_OP_ITE
Definition z3_api.h:1004

◆ is_lambda()

bool is_lambda ( ) const
inline

Return true if this expression is a lambda expression.

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

1115{ return Z3_is_lambda(ctx(), m_ast); }
Z3_is_lambda
bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a)
Determine if ast is a lambda expression.

◆ is_not()

bool is_not ( ) const
inline

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

1512{ return is_app() && Z3_OP_NOT == decl().decl_kind(); }
Z3_OP_NOT
@ Z3_OP_NOT
Definition z3_api.h:1009

◆ is_numeral() [1/4]

bool is_numeral ( ) const
inline

Return true if this expression is a numeral. Specialized functions also return representations for the numerals as small integers, 64 bit integers or rational or decimal strings.

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

1076{ return kind() == Z3_NUMERAL_AST; }

Referenced by as_binary(), as_double(), denominator(), get_decimal_string(), get_numeral_int64(), get_numeral_uint(), get_numeral_uint64(), and numerator().

◆ is_numeral() [2/4]

bool is_numeral ( double & d) const
inline

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

1083{ if (!is_numeral()) return false; d = Z3_get_numeral_double(ctx(), m_ast); check_error(); return true; }
Z3_get_numeral_double
double Z3_API Z3_get_numeral_double(Z3_context c, Z3_ast a)
Return numeral as a double.

Referenced by is_numeral().

◆ is_numeral() [3/4]

bool is_numeral ( std::string & s) const
inline

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

1081{ if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); check_error(); return true; }
Z3_get_numeral_string
Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a)
Return numeral value, as a decimal string of a numeric constant term.

Referenced by is_numeral().

◆ is_numeral() [4/4]

bool is_numeral ( std::string & s,
unsigned precision ) const
inline

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

1082{ if (!is_numeral()) return false; s = Z3_get_numeral_decimal_string(ctx(), m_ast, precision); check_error(); return true; }

Referenced by is_numeral().

◆ is_numeral_i()

bool is_numeral_i ( int & i) const
inline

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

1079{ bool r = Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;}
Z3_get_numeral_int
bool Z3_API Z3_get_numeral_int(Z3_context c, Z3_ast v, int *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int....

Referenced by get_numeral_int().

◆ is_numeral_i64()

bool is_numeral_i64 ( int64_t & i) const
inline

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

1077{ bool r = Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;}
Z3_get_numeral_int64
bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, int64_t *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int64_t int....

Referenced by as_int64(), and get_numeral_int64().

◆ is_numeral_u()

bool is_numeral_u ( unsigned & i) const
inline

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

1080{ bool r = Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;}
Z3_get_numeral_uint
bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine unsigned int....

Referenced by get_numeral_uint().

◆ is_numeral_u64()

bool is_numeral_u64 ( uint64_t & i) const
inline

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

1078{ bool r = Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;}
Z3_get_numeral_uint64
bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, uint64_t *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine uint64_t int....

Referenced by as_uint64(), and get_numeral_uint64().

◆ is_or()

bool is_or ( ) const
inline

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

1514{ return is_app() && Z3_OP_OR == decl().decl_kind(); }
Z3_OP_OR
@ Z3_OP_OR
Definition z3_api.h:1006

◆ is_quantifier()

bool is_quantifier ( ) const
inline

Return true if this expression is a quantifier.

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

1102{ return kind() == Z3_QUANTIFIER_AST; }
Z3_QUANTIFIER_AST
@ Z3_QUANTIFIER_AST
Definition z3_api.h:148

Referenced by body().

◆ is_re()

bool is_re ( ) const
inline

Return true if this is a regular expression.

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

1054{ return get_sort().is_re(); }

Referenced by operator+.

◆ is_real()

bool is_real ( ) const
inline

Return true if this is a real expression.

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

1024{ return get_sort().is_real(); }

Referenced by abs.

◆ is_relation()

bool is_relation ( ) const
inline

Return true if this is a Relation expression.

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

1046{ return get_sort().is_relation(); }

◆ is_seq()

bool is_seq ( ) const
inline

Return true if this is a sequence expression.

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

1050{ return get_sort().is_seq(); }

Referenced by operator+, and operator[]().

◆ is_string_value()

bool is_string_value ( ) const
inline

Return true if this expression is a string literal. The string can be accessed using get_string() and get_escaped_string().

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

1352{ return Z3_is_string(ctx(), m_ast); }
Z3_is_string
bool Z3_API Z3_is_string(Z3_context c, Z3_ast s)
Determine if s is a string constant.

Referenced by get_string(), and get_u32string().

◆ is_true()

bool is_true ( ) const
inline

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

1510{ return is_app() && Z3_OP_TRUE == decl().decl_kind(); }
Z3_OP_TRUE
@ Z3_OP_TRUE
Definition z3_api.h:1000

◆ is_var()

bool is_var ( ) const
inline

Return true if this expression is a variable.

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

1120{ return kind() == Z3_VAR_AST; }
Z3_VAR_AST
@ Z3_VAR_AST
Definition z3_api.h:147

◆ is_well_sorted()

bool is_well_sorted ( ) const
inline

Return true if this expression is well sorted (aka type correct).

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

1129{ bool r = Z3_is_well_sorted(ctx(), m_ast); check_error(); return r; }
Z3_is_well_sorted
bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t)
Return true if the given expression t is well sorted.

◆ is_xor()

bool is_xor ( ) const
inline

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

1515{ return is_app() && Z3_OP_XOR == decl().decl_kind(); }
Z3_OP_XOR
@ Z3_OP_XOR
Definition z3_api.h:1008

◆ itos()

expr itos ( ) const
inline

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

1734 {
1735 Z3_ast r = Z3_mk_int_to_str(ctx(), *this);
1736 check_error();
1737 return expr(ctx(), r);
1738 }
Z3_mk_int_to_str
Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s)
Integer to string conversion.

◆ length()

expr length ( ) const
inline

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

1718 {
1719 Z3_ast r = Z3_mk_seq_length(ctx(), *this);
1720 check_error();
1721 return expr(ctx(), r);
1722 }
Z3_mk_seq_length
Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s)
Return the length of the sequence s.

Referenced by extract().

◆ lo()

unsigned lo ( ) const
inline

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

1637{ assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 1)); }

Referenced by extract(), loop(), loop(), and range.

◆ loop() [1/2]

expr loop ( unsigned lo)
inline

create a looping regular expression.

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

1774 {
1775 Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, 0);
1776 check_error();
1777 return expr(ctx(), r);
1778 }
Z3_mk_re_loop
Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi)
Create a regular expression loop. The supplied regular expression r is repeated between lo and hi tim...

◆ loop() [2/2]

expr loop ( unsigned lo,
unsigned hi )
inline

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

1779 {
1780 Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, hi);
1781 check_error();
1782 return expr(ctx(), r);
1783 }

◆ mk_from_ieee_bv()

expr mk_from_ieee_bv ( sort const & s) const
inline

Convert this IEEE BV into a fpa.

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

1194 {
1195 assert(is_bv());
1196 Z3_ast r = Z3_mk_fpa_to_fp_bv(ctx(), m_ast, s);
1197 check_error();
1198 return expr(ctx(), r);
1199 }
Z3_mk_fpa_to_fp_bv
Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(Z3_context c, Z3_ast bv, Z3_sort s)
Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
z3py.is_bv
is_bv(a)
Definition z3py.py:4232

◆ mk_is_inf()

expr mk_is_inf ( ) const
inline

Return Boolean expression to test for whether an FP expression is inf.

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

1134 {
1135 assert(is_fpa());
1136 Z3_ast r = Z3_mk_fpa_is_infinite(ctx(), m_ast);
1137 check_error();
1138 return expr(ctx(), r);
1139 }
Z3_mk_fpa_is_infinite
Z3_ast Z3_API Z3_mk_fpa_is_infinite(Z3_context c, Z3_ast t)
Predicate indicating whether t is a floating-point number representing +oo or -oo.

◆ mk_is_nan()

expr mk_is_nan ( ) const
inline

Return Boolean expression to test for whether an FP expression is a NaN.

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

1144 {
1145 assert(is_fpa());
1146 Z3_ast r = Z3_mk_fpa_is_nan(ctx(), m_ast);
1147 check_error();
1148 return expr(ctx(), r);
1149 }
Z3_mk_fpa_is_nan
Z3_ast Z3_API Z3_mk_fpa_is_nan(Z3_context c, Z3_ast t)
Predicate indicating whether t is a NaN.

◆ mk_is_normal()

expr mk_is_normal ( ) const
inline

Return Boolean expression to test for whether an FP expression is a normal.

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

1154 {
1155 assert(is_fpa());
1156 Z3_ast r = Z3_mk_fpa_is_normal(ctx(), m_ast);
1157 check_error();
1158 return expr(ctx(), r);
1159 }
Z3_mk_fpa_is_normal
Z3_ast Z3_API Z3_mk_fpa_is_normal(Z3_context c, Z3_ast t)
Predicate indicating whether t is a normal floating-point number.

◆ mk_is_subnormal()

expr mk_is_subnormal ( ) const
inline

Return Boolean expression to test for whether an FP expression is a subnormal.

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

1164 {
1165 assert(is_fpa());
1166 Z3_ast r = Z3_mk_fpa_is_subnormal(ctx(), m_ast);
1167 check_error();
1168 return expr(ctx(), r);
1169 }
Z3_mk_fpa_is_subnormal
Z3_ast Z3_API Z3_mk_fpa_is_subnormal(Z3_context c, Z3_ast t)
Predicate indicating whether t is a subnormal floating-point number.

◆ mk_is_zero()

expr mk_is_zero ( ) const
inline

Return Boolean expression to test for whether an FP expression is a zero.

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

1174 {
1175 assert(is_fpa());
1176 Z3_ast r = Z3_mk_fpa_is_zero(ctx(), m_ast);
1177 check_error();
1178 return expr(ctx(), r);
1179 }
Z3_mk_fpa_is_zero
Z3_ast Z3_API Z3_mk_fpa_is_zero(Z3_context c, Z3_ast t)
Predicate indicating whether t is a floating-point number with zero value, i.e., +zero or -zero.

◆ mk_to_ieee_bv()

expr mk_to_ieee_bv ( ) const
inline

Convert this fpa into an IEEE BV.

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

1184 {
1185 assert(is_fpa());
1186 Z3_ast r = Z3_mk_fpa_to_ieee_bv(ctx(), m_ast);
1187 check_error();
1188 return expr(ctx(), r);
1189 }
Z3_mk_fpa_to_ieee_bv
Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(Z3_context c, Z3_ast t)
Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.

◆ nth()

expr nth ( expr const & index) const
inline

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

1712 {
1713 check_context(*this, index);
1714 Z3_ast r = Z3_mk_seq_nth(ctx(), *this, index);
1715 check_error();
1716 return expr(ctx(), r);
1717 }
Z3_mk_seq_nth
Z3_ast Z3_API Z3_mk_seq_nth(Z3_context c, Z3_ast s, Z3_ast index)
Retrieve from s the element positioned at position index. The function is under-specified if the inde...

Referenced by operator[]().

◆ num_args()

unsigned num_args ( ) const
inline

Return the number of arguments in this application. This method assumes the expression is an application.

Precondition
is_app()

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

1395{ unsigned r = Z3_get_app_num_args(ctx(), *this); check_error(); return r; }
Z3_get_app_num_args
unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a)
Return the number of argument of an application. If t is an constant, then the number of arguments is...

Referenced by AstRef::__bool__(), args(), end(), and is_const().

◆ numerator()

expr numerator ( ) const
inline

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

1332 {
1333 assert(is_numeral());
1334 Z3_ast r = Z3_get_numerator(ctx(), m_ast);
1335 check_error();
1336 return expr(ctx(),r);
1337 }
Z3_get_numerator
Z3_ast Z3_API Z3_get_numerator(Z3_context c, Z3_ast a)
Return the numerator (as a numeral AST) of a numeral AST of sort Real.

◆ operator Z3_app()

operator Z3_app ( ) const
inline

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

1380{ assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }

◆ operator[]() [1/2]

expr operator[] ( expr const & index) const
inline

index operator defined on arrays and sequences.

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

1788 {
1789 assert(is_array() || is_seq());
1790 if (is_array()) {
1791 return select(*this, index);
1792 }
1793 return nth(index);
1794 }
z3::select
expr select(expr const &a, expr const &i)
forward declarations
Definition z3++.h:4388
z3py.is_array
bool is_array(Any a)
Definition z3py.py:4961
z3py.is_seq
is_seq(a)
Definition z3py.py:11898

◆ operator[]() [2/2]

expr operator[] ( expr_vector const & index) const
inline

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

1796 {
1797 return select(*this, index);
1798 }

◆ power()

expr power ( expr const & n) const
inline

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

1723 {
1724 check_context(*this, n);
1725 Z3_ast r = Z3_mk_seq_power(ctx(), *this, n);
1726 check_error();
1727 return expr(ctx(), r);
1728 }
Z3_mk_seq_power
Z3_ast Z3_API Z3_mk_seq_power(Z3_context c, Z3_ast s, Z3_ast n)
Create the sequence s concatenated n times with itself. The result is the empty sequence when n is no...

◆ repeat()

expr repeat ( unsigned i) const
inline

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

1625{ Z3_ast r = Z3_mk_repeat(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
Z3_mk_repeat
Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1)
Repeat the given bit-vector up length i.

◆ replace()

expr replace ( expr const & src,
expr const & dst ) const
inline

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

1689 {
1690 check_context(*this, src); check_context(src, dst);
1691 Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
1692 check_error();
1693 return expr(ctx(), r);
1694 }
Z3_mk_seq_replace
Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst)
Replace the first occurrence of src with dst in s.

◆ rotate_left()

expr rotate_left ( unsigned i) const
inline

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

1621{ Z3_ast r = Z3_mk_rotate_left(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
Z3_mk_rotate_left
Z3_ast Z3_API Z3_mk_rotate_left(Z3_context c, unsigned i, Z3_ast t1)
Rotate bits of t1 to the left i times.

◆ rotate_right()

expr rotate_right ( unsigned i) const
inline

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

1622{ Z3_ast r = Z3_mk_rotate_right(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
Z3_mk_rotate_right
Z3_ast Z3_API Z3_mk_rotate_right(Z3_context c, unsigned i, Z3_ast t1)
Rotate bits of t1 to the right i times.

◆ sbvtos()

expr sbvtos ( ) const
inline

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

1744 {
1745 Z3_ast r = Z3_mk_sbv_to_str(ctx(), *this);
1746 check_error();
1747 return expr(ctx(), r);
1748 }
Z3_mk_sbv_to_str
Z3_ast Z3_API Z3_mk_sbv_to_str(Z3_context c, Z3_ast s)
Signed bit-vector to string conversion.

◆ simplify() [1/2]

expr simplify ( ) const
inline

Return a simplified version of this expression.

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

1803{ Z3_ast r = Z3_simplify(ctx(), m_ast); check_error(); return expr(ctx(), r); }
Z3_simplify
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.

◆ simplify() [2/2]

expr simplify ( params const & p) const
inline

Return a simplified version of this expression. The parameter p is a set of parameters for the Z3 simplifier.

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

1807{ Z3_ast r = Z3_simplify_ex(ctx(), m_ast, p); check_error(); return expr(ctx(), r); }
Z3_simplify_ex
Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)
Interface to simplifier.

◆ stoi()

expr stoi ( ) const
inline

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

1729 {
1730 Z3_ast r = Z3_mk_str_to_int(ctx(), *this);
1731 check_error();
1732 return expr(ctx(), r);
1733 }
Z3_mk_str_to_int
Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s)
Convert string to integer.

◆ substitute() [1/3]

expr substitute ( expr_vector const & dst)
inline

Apply substitution. Replace bound variables by expressions.

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

4737 {
4738 array<Z3_ast> _dst(dst.size());
4739 for (unsigned i = 0; i < dst.size(); ++i) {
4740 _dst[i] = dst[i];
4741 }
4742 Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
4743 check_error();
4744 return expr(ctx(), r);
4745 }
Z3_substitute_vars
Z3_ast Z3_API Z3_substitute_vars(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const to[])
Substitute the variables in a with the expressions in to. For every i smaller than num_exprs,...

◆ substitute() [2/3]

expr substitute ( expr_vector const & src,
expr_vector const & dst )
inline

Apply substitution. Replace src expressions by dst.

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

4724 {
4725 assert(src.size() == dst.size());
4726 array<Z3_ast> _src(src.size());
4727 array<Z3_ast> _dst(dst.size());
4728 for (unsigned i = 0; i < src.size(); ++i) {
4729 _src[i] = src[i];
4730 _dst[i] = dst[i];
4731 }
4732 Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
4733 check_error();
4734 return expr(ctx(), r);
4735 }
Z3_substitute
Z3_ast Z3_API Z3_substitute(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const from[], Z3_ast const to[])
Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs....

◆ substitute() [3/3]

expr substitute ( func_decl_vector const & funs,
expr_vector const & bodies )
inline

Apply function substitution by macro definitions.

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

4747 {
4748 array<Z3_ast> _dst(dst.size());
4749 array<Z3_func_decl> _funs(funs.size());
4750 if (dst.size() != funs.size()) {
4751 Z3_THROW(exception("length of argument lists don't align"));
4752 return expr(ctx(), nullptr);
4753 }
4754 for (unsigned i = 0; i < dst.size(); ++i) {
4755 _dst[i] = dst[i];
4756 _funs[i] = funs[i];
4757 }
4758 Z3_ast r = Z3_substitute_funs(ctx(), m_ast, dst.size(), _funs.ptr(), _dst.ptr());
4759 check_error();
4760 return expr(ctx(), r);
4761 }
Z3_substitute_funs
Z3_ast Z3_API Z3_substitute_funs(Z3_context c, Z3_ast a, unsigned num_funs, Z3_func_decl const from[], Z3_ast const to[])
Substitute functions in from with new expressions in to.

◆ ubvtos()

expr ubvtos ( ) const
inline

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

1739 {
1740 Z3_ast r = Z3_mk_ubv_to_str(ctx(), *this);
1741 check_error();
1742 return expr(ctx(), r);
1743 }
Z3_mk_ubv_to_str
Z3_ast Z3_API Z3_mk_ubv_to_str(Z3_context c, Z3_ast s)
Unsigned bit-vector to string conversion.

◆ unit()

expr unit ( ) const
inline

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

1695 {
1696 Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
1697 check_error();
1698 return expr(ctx(), r);
1699 }
Z3_mk_seq_unit
Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a)
Create a unit sequence of a.

◆ update()

expr update ( expr_vector const & args) const
inline

Update the arguments of this application. Return a new expression with the same function declaration and updated arguments. The number of new arguments must match the current number of arguments.

Precondition
is_app()
args.size() == num_args()

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

4763 {
4764 array<Z3_ast> _args(args.size());
4765 for (unsigned i = 0; i < args.size(); ++i) {
4766 _args[i] = args[i];
4767 }
4768 Z3_ast r = Z3_update_term(ctx(), m_ast, args.size(), _args.ptr());
4769 check_error();
4770 return expr(ctx(), r);
4771 }
Z3_update_term
Z3_ast Z3_API Z3_update_term(Z3_context c, Z3_ast a, unsigned num_args, Z3_ast const args[])
Update the arguments of term a using the arguments args. The number of arguments num_args should coin...

◆ update_field()

expr update_field ( func_decl const & field_access,
expr const & new_value ) const
inline

Update a datatype field. Return a new datatype expression with the specified field updated to the new value. The remaining fields are unchanged.

Precondition
is_datatype()
Parameters
field_accessThe accessor function declaration for the field to update
new_valueThe new value for the field

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

4773 {
4774 assert(is_datatype());
4775 Z3_ast r = Z3_datatype_update_field(ctx(), field_access, m_ast, new_value);
4776 check_error();
4777 return expr(ctx(), r);
4778 }
Z3_datatype_update_field
Z3_ast Z3_API Z3_datatype_update_field(Z3_context c, Z3_func_decl field_access, Z3_ast t, Z3_ast value)
Update record field with a value.

◆ abs

expr abs ( expr const & a)
friend

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

2249 {
2250 Z3_ast r;
2251 if (a.is_int()) {
2252 expr zero = a.ctx().int_val(0);
2253 expr ge = a >= zero;
2254 expr na = -a;
2255 r = Z3_mk_ite(a.ctx(), ge, a, na);
2256 }
2257 else if (a.is_real()) {
2258 expr zero = a.ctx().real_val(0);
2259 expr ge = a >= zero;
2260 expr na = -a;
2261 r = Z3_mk_ite(a.ctx(), ge, a, na);
2262 }
2263 else {
2264 r = Z3_mk_fpa_abs(a.ctx(), a);
2265 }
2266 a.check_error();
2267 return expr(a.ctx(), r);
2268 }
Z3_mk_ite
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
Z3_mk_fpa_abs
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.

Referenced by abs.

◆ atleast

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

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

2705 {
2706 assert(es.size() > 0);
2707 context& ctx = es[0u].ctx();
2708 array<Z3_ast> _es(es);
2709 Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
2710 ctx.check_error();
2711 return expr(ctx, r);
2712 }
Z3_mk_atleast
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.

Referenced by atleast.

◆ atmost

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

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

2697 {
2698 assert(es.size() > 0);
2699 context& ctx = es[0u].ctx();
2700 array<Z3_ast> _es(es);
2701 Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
2702 ctx.check_error();
2703 return expr(ctx, r);
2704 }
Z3_mk_atmost
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.

Referenced by atmost.

◆ bv2int

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

bit-vector and integer conversions.

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

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

Referenced by bv2int.

◆ bvadd_no_overflow

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

bit-vector overflow/underflow checks

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

2501 {
2502 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);
2503 }
Z3_mk_bvadd_no_overflow
Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.

Referenced by bvadd_no_overflow.

◆ bvadd_no_underflow

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

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

2504 {
2505 check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2506 }
Z3_mk_bvadd_no_underflow
Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.

Referenced by bvadd_no_underflow.

◆ bvmul_no_overflow

expr bvmul_no_overflow ( expr const & a,
expr const & b,
bool is_signed )
friend

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

2519 {
2520 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);
2521 }
Z3_mk_bvmul_no_overflow
Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.

Referenced by bvmul_no_overflow.

◆ bvmul_no_underflow

expr bvmul_no_underflow ( expr const & a,
expr const & b )
friend

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

2522 {
2523 check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2524 }
Z3_mk_bvmul_no_underflow
Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflo...

Referenced by bvmul_no_underflow.

◆ bvneg_no_overflow

expr bvneg_no_overflow ( expr const & a)
friend

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

2516 {
2517 Z3_ast r = Z3_mk_bvneg_no_overflow(a.ctx(), a); a.check_error(); return expr(a.ctx(), r);
2518 }
Z3_mk_bvneg_no_overflow
Z3_ast Z3_API Z3_mk_bvneg_no_overflow(Z3_context c, Z3_ast t1)
Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector.

Referenced by bvneg_no_overflow.

◆ bvredand

expr bvredand ( expr const & a)
friend

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

2243 {
2244 assert(a.is_bv());
2245 Z3_ast r = Z3_mk_bvredand(a.ctx(), a);
2246 a.check_error();
2247 return expr(a.ctx(), r);
2248 }
Z3_mk_bvredand
Z3_ast Z3_API Z3_mk_bvredand(Z3_context c, Z3_ast t1)
Take conjunction of bits in vector, return vector of length 1.

Referenced by bvredand.

◆ bvredor

expr bvredor ( expr const & a)
friend

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

2237 {
2238 assert(a.is_bv());
2239 Z3_ast r = Z3_mk_bvredor(a.ctx(), a);
2240 a.check_error();
2241 return expr(a.ctx(), r);
2242 }
Z3_mk_bvredor
Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1)
Take disjunction of bits in vector, return vector of length 1.

Referenced by bvredor.

◆ bvsdiv_no_overflow

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

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

2513 {
2514 check_context(a, b); Z3_ast r = Z3_mk_bvsdiv_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2515 }
Z3_mk_bvsdiv_no_overflow
Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.

Referenced by bvsdiv_no_overflow.

◆ bvsub_no_overflow

expr bvsub_no_overflow ( expr const & a,
expr const & b )
friend

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

2507 {
2508 check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2509 }
Z3_mk_bvsub_no_overflow
Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.

Referenced by bvsub_no_overflow.

◆ bvsub_no_underflow

expr bvsub_no_underflow ( expr const & a,
expr const & b,
bool is_signed )
friend

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

2510 {
2511 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);
2512 }
Z3_mk_bvsub_no_underflow
Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.

Referenced by bvsub_no_underflow.

◆ concat [1/2]

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

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

2731 {
2732 check_context(a, b);
2733 Z3_ast r;
2734 if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
2735 Z3_ast _args[2] = { a, b };
2736 r = Z3_mk_seq_concat(a.ctx(), 2, _args);
2737 }
2738 else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
2739 Z3_ast _args[2] = { a, b };
2740 r = Z3_mk_re_concat(a.ctx(), 2, _args);
2741 }
2742 else {
2743 r = Z3_mk_concat(a.ctx(), a, b);
2744 }
2745 a.ctx().check_error();
2746 return expr(a.ctx(), r);
2747 }
Z3_is_seq_sort
bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
Z3_mk_seq_concat
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
Z3_mk_re_concat
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])
Create the concatenation of the regular languages.
Z3_mk_concat
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
Z3_is_re_sort
bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.

Referenced by concat, concat, and operator+.

◆ concat [2/2]

expr concat ( expr_vector const & args)
friend

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

2749 {
2750 Z3_ast r;
2751 assert(args.size() > 0);
2752 if (args.size() == 1) {
2753 return args[0u];
2754 }
2755 context& ctx = args[0u].ctx();
2756 array<Z3_ast> _args(args);
2757 if (Z3_is_seq_sort(ctx, args[0u].get_sort())) {
2758 r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
2759 }
2760 else if (Z3_is_re_sort(ctx, args[0u].get_sort())) {
2761 r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
2762 }
2763 else {
2764 r = _args[args.size()-1];
2765 for (unsigned i = args.size()-1; i > 0; ) {
2766 --i;
2767 r = Z3_mk_concat(ctx, _args[i], r);
2768 ctx.check_error();
2769 }
2770 }
2771 ctx.check_error();
2772 return expr(ctx, r);
2773 }

◆ distinct

expr distinct ( expr_vector const & args)
friend

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

2722 {
2723 assert(args.size() > 0);
2724 context& ctx = args[0u].ctx();
2725 array<Z3_ast> _args(args);
2726 Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
2727 ctx.check_error();
2728 return expr(ctx, r);
2729 }
Z3_mk_distinct
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).

Referenced by distinct.

◆ fma

expr fma ( expr const & a,
expr const & b,
expr const & c,
expr const & rm )
friend

FloatingPoint fused multiply-add.

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

2285 {
2286 check_context(a, b); check_context(a, c); check_context(a, rm);
2287 assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
2288 Z3_ast r = Z3_mk_fpa_fma(a.ctx(), rm, a, b, c);
2289 a.check_error();
2290 return expr(a.ctx(), r);
2291 }
Z3_mk_fpa_fma
Z3_ast Z3_API Z3_mk_fpa_fma(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Floating-point fused multiply-add.

Referenced by fma.

◆ fp_eq

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

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

2276 {
2277 check_context(a, b);
2278 assert(a.is_fpa());
2279 Z3_ast r = Z3_mk_fpa_eq(a.ctx(), a, b);
2280 a.check_error();
2281 return expr(a.ctx(), r);
2282 }
Z3_mk_fpa_eq
Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point equality.

Referenced by fp_eq.

◆ fpa_fp

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

Create an expression of FloatingPoint sort from three bit-vector expressions.

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

2293 {
2294 check_context(sgn, exp); check_context(exp, sig);
2295 assert(sgn.is_bv() && exp.is_bv() && sig.is_bv());
2296 Z3_ast r = Z3_mk_fpa_fp(sgn.ctx(), sgn, exp, sig);
2297 sgn.check_error();
2298 return expr(sgn.ctx(), r);
2299 }

Referenced by fpa_fp.

◆ fpa_to_fpa

expr fpa_to_fpa ( expr const & t,
sort s )
friend

Conversion of a floating-point term into another floating-point.

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

2329 {
2330 assert(t.is_fpa());
2331 Z3_ast r = Z3_mk_fpa_to_fp_float(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2332 t.check_error();
2333 return expr(t.ctx(), r);
2334 }
Z3_mk_fpa_to_fp_float
Z3_ast Z3_API Z3_mk_fpa_to_fp_float(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.

Referenced by fpa_to_fpa.

◆ fpa_to_sbv

expr fpa_to_sbv ( expr const & t,
unsigned sz )
friend

Conversion of a floating-point term into a signed bit-vector.

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

2301 {
2302 assert(t.is_fpa());
2303 Z3_ast r = Z3_mk_fpa_to_sbv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
2304 t.check_error();
2305 return expr(t.ctx(), r);
2306 }
Z3_mk_fpa_to_sbv
Z3_ast Z3_API Z3_mk_fpa_to_sbv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)
Conversion of a floating-point term into a signed bit-vector.

Referenced by fpa_to_sbv.

◆ fpa_to_ubv

expr fpa_to_ubv ( expr const & t,
unsigned sz )
friend

Conversion of a floating-point term into an unsigned bit-vector.

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

2308 {
2309 assert(t.is_fpa());
2310 Z3_ast r = Z3_mk_fpa_to_ubv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
2311 t.check_error();
2312 return expr(t.ctx(), r);
2313 }
Z3_mk_fpa_to_ubv
Z3_ast Z3_API Z3_mk_fpa_to_ubv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)
Conversion of a floating-point term into an unsigned bit-vector.

Referenced by fpa_to_ubv.

◆ implies [1/3]

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

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

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

◆ implies [2/3]

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

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

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

◆ implies [3/3]

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

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

1853 {
1854 assert(a.is_bool() && b.is_bool());
1855 _Z3_MK_BIN_(a, b, Z3_mk_implies);
1856 }
Z3_mk_implies
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
_Z3_MK_BIN_
#define _Z3_MK_BIN_(a, b, binop)
Definition z3++.h:1846

Referenced by implies, implies, and implies.

◆ int2bv

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

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

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

Referenced by int2bv.

◆ is_int

expr is_int ( expr const & e)
friend

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

1921{ _Z3_MK_UN_(e, Z3_mk_is_int); }
Z3_mk_is_int
Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1)
Check if a real number is an integer.
_Z3_MK_UN_
#define _Z3_MK_UN_(a, mkun)
Definition z3++.h:1893

◆ ite

expr ite ( expr const & c,
expr const & t,
expr const & e )
friend

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

Precondition
c.is_bool()

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

2348 {
2349 check_context(c, t); check_context(c, e);
2350 assert(c.is_bool());
2351 Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
2352 c.check_error();
2353 return expr(c.ctx(), r);
2354 }

Referenced by ite.

◆ max

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

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

2221 {
2222 check_context(a, b);
2223 Z3_ast r;
2224 if (a.is_arith()) {
2225 r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), a, b);
2226 }
2227 else if (a.is_bv()) {
2228 r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), a, b);
2229 }
2230 else {
2231 assert(a.is_fpa());
2232 r = Z3_mk_fpa_max(a.ctx(), a, b);
2233 }
2234 a.check_error();
2235 return expr(a.ctx(), r);
2236 }
Z3_mk_ge
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
Z3_mk_fpa_max
Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2)
Maximum of floating-point numbers.
Z3_mk_bvuge
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.

Referenced by max.

◆ min

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

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

2205 {
2206 check_context(a, b);
2207 Z3_ast r;
2208 if (a.is_arith()) {
2209 r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), b, a);
2210 }
2211 else if (a.is_bv()) {
2212 r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), b, a);
2213 }
2214 else {
2215 assert(a.is_fpa());
2216 r = Z3_mk_fpa_min(a.ctx(), a, b);
2217 }
2218 a.check_error();
2219 return expr(a.ctx(), r);
2220 }
Z3_mk_fpa_min
Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2)
Minimum of floating-point numbers.

Referenced by min.

◆ mk_and

expr mk_and ( expr_vector const & args)
friend

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

2809 {
2810 array<Z3_ast> _args(args);
2811 Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2812 args.check_error();
2813 return expr(args.ctx(), r);
2814 }
Z3_mk_and
Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].

Referenced by mk_and.

◆ mk_or

expr mk_or ( expr_vector const & args)
friend

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

2803 {
2804 array<Z3_ast> _args(args);
2805 Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2806 args.check_error();
2807 return expr(args.ctx(), r);
2808 }
Z3_mk_or
Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] or ... or args[num_args-1].

Referenced by mk_or.

◆ mk_xor

expr mk_xor ( expr_vector const & args)
friend

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

2815 {
2816 if (args.empty())
2817 return args.ctx().bool_val(false);
2818 expr r = args[0u];
2819 for (unsigned i = 1; i < args.size(); ++i)
2820 r = r ^ args[i];
2821 return r;
2822 }

Referenced by mk_xor.

◆ mod [1/3]

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

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

1865 {
1866 if (a.is_bv()) {
1867 _Z3_MK_BIN_(a, b, Z3_mk_bvsmod);
1868 }
1869 else {
1870 _Z3_MK_BIN_(a, b, Z3_mk_mod);
1871 }
1872 }
Z3_mk_mod
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.
Z3_mk_bvsmod
Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows divisor).

Referenced by mod, mod, and mod.

◆ mod [2/3]

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

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

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

◆ mod [3/3]

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

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

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

◆ nand

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

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

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

Referenced by nand.

◆ nor

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

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

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

Referenced by nor.

◆ operator!

expr operator! ( expr const & a)
friend

Return an expression representing not(a).

Precondition
a.is_bool()

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

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

Referenced by operator!.

◆ operator!= [1/3]

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

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

1961 {
1962 check_context(a, b);
1963 Z3_ast args[2] = { a, b };
1964 Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1965 a.check_error();
1966 return expr(a.ctx(), r);
1967 }

Referenced by operator!=, operator!=, and operator!=.

◆ operator!= [2/3]

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

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

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

◆ operator!= [3/3]

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

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

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

◆ operator& [1/3]

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

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

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

Referenced by operator&, operator&, and operator&.

◆ operator& [2/3]

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

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

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

◆ operator& [3/3]

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

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

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

◆ operator&& [1/3]

expr operator&& ( bool a,
expr const & b )
friend

Return an expression representing a and b. The C++ Boolean value a is automatically converted into a Z3 Boolean constant.

Precondition
b.is_bool()

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

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

◆ operator&& [2/3]

expr operator&& ( expr const & a,
bool b )
friend

Return an expression representing a and b. The C++ Boolean value b is automatically converted into a Z3 Boolean constant.

Precondition
a.is_bool()

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

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

◆ operator&& [3/3]

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

Return an expression representing a and b.

Precondition
a.is_bool()
b.is_bool()

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

1925 {
1926 check_context(a, b);
1927 assert(a.is_bool() && b.is_bool());
1928 Z3_ast args[2] = { a, b };
1929 Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
1930 a.check_error();
1931 return expr(a.ctx(), r);
1932 }

Referenced by operator&&, operator&&, and operator&&.

◆ operator* [1/3]

expr operator* ( expr const & a,
expr const & b )
friend

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

2007 {
2008 check_context(a, b);
2009 Z3_ast r = 0;
2010 if (a.is_arith() && b.is_arith()) {
2011 Z3_ast args[2] = { a, b };
2012 r = Z3_mk_mul(a.ctx(), 2, args);
2013 }
2014 else if (a.is_finite_field() && b.is_finite_field()) {
2015 Z3_ast args[2] = { a, b };
2016 r = Z3_mk_ff_mul(a.ctx(), 2, args);
2017 }
2018 else if (a.is_bv() && b.is_bv()) {
2019 r = Z3_mk_bvmul(a.ctx(), a, b);
2020 }
2021 else if (a.is_fpa() && b.is_fpa()) {
2022 r = Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
2023 }
2024 else {
2025 // operator is not supported by given arguments.
2026 assert(false);
2027 }
2028 a.check_error();
2029 return expr(a.ctx(), r);
2030 }
Z3_mk_mul
Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] * ... * args[num_args-1].
Z3_mk_bvmul
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
Z3_mk_ff_mul
Z3_ast Z3_API Z3_mk_ff_mul(Z3_context c, unsigned n, Z3_ast const args[])
Multiply at least two elements of the same prime field.
Z3_mk_fpa_mul
Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point multiplication.

Referenced by operator*, operator*, and operator*.

◆ operator* [2/3]

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

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

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

◆ operator* [3/3]

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

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

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

◆ operator+ [1/3]

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

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

1973 {
1974 check_context(a, b);
1975 Z3_ast r = 0;
1976 if (a.is_arith() && b.is_arith()) {
1977 Z3_ast args[2] = { a, b };
1978 r = Z3_mk_add(a.ctx(), 2, args);
1979 }
1980 else if (a.is_finite_field() && b.is_finite_field()) {
1981 Z3_ast args[2] = { a, b };
1982 r = Z3_mk_ff_add(a.ctx(), 2, args);
1983 }
1984 else if (a.is_bv() && b.is_bv()) {
1985 r = Z3_mk_bvadd(a.ctx(), a, b);
1986 }
1987 else if (a.is_seq() && b.is_seq()) {
1988 return concat(a, b);
1989 }
1990 else if (a.is_re() && b.is_re()) {
1991 Z3_ast _args[2] = { a, b };
1992 r = Z3_mk_re_union(a.ctx(), 2, _args);
1993 }
1994 else if (a.is_fpa() && b.is_fpa()) {
1995 r = Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1996 }
1997 else {
1998 // operator is not supported by given arguments.
1999 assert(false);
2000 }
2001 a.check_error();
2002 return expr(a.ctx(), r);
2003 }
Z3_mk_re_union
Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[])
Create the union of the regular languages.
Z3_mk_bvadd
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement addition.
Z3_mk_ff_add
Z3_ast Z3_API Z3_mk_ff_add(Z3_context c, unsigned n, Z3_ast const args[])
Sum at least two elements of the same prime field.
Z3_mk_fpa_add
Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point addition.
Z3_mk_add
Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] + ... + args[num_args-1].
z3::concat
expr concat(expr const &a, expr const &b)
Definition z3++.h:2731

Referenced by operator+, operator+, and operator+.

◆ operator+ [2/3]

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

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

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

◆ operator+ [3/3]

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

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

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

◆ operator- [1/4]

expr operator- ( expr const & a)
friend

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

2077 {
2078 Z3_ast r = 0;
2079 if (a.is_arith()) {
2080 r = Z3_mk_unary_minus(a.ctx(), a);
2081 }
2082 else if (a.is_finite_field()) { r = Z3_mk_ff_neg(a.ctx(), a); }
2083 else if (a.is_bv()) {
2084 r = Z3_mk_bvneg(a.ctx(), a);
2085 }
2086 else if (a.is_fpa()) {
2087 r = Z3_mk_fpa_neg(a.ctx(), a);
2088 }
2089 else {
2090 // operator is not supported by given arguments.
2091 assert(false);
2092 }
2093 a.check_error();
2094 return expr(a.ctx(), r);
2095 }
Z3_mk_ff_neg
Z3_ast Z3_API Z3_mk_ff_neg(Z3_context c, Z3_ast a)
Additive inverse in a prime field.
Z3_mk_unary_minus
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
Z3_mk_fpa_neg
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.
Z3_mk_bvneg
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.

Referenced by operator-, operator-, operator-, and operator-.

◆ operator- [2/4]

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

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

2097 {
2098 check_context(a, b);
2099 if (a.is_finite_field() && b.is_finite_field()) return a + -b;
2100 Z3_ast r = 0;
2101 if (a.is_arith() && b.is_arith()) {
2102 Z3_ast args[2] = { a, b };
2103 r = Z3_mk_sub(a.ctx(), 2, args);
2104 }
2105 else if (a.is_bv() && b.is_bv()) {
2106 r = Z3_mk_bvsub(a.ctx(), a, b);
2107 }
2108 else if (a.is_fpa() && b.is_fpa()) {
2109 r = Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
2110 }
2111 else {
2112 // operator is not supported by given arguments.
2113 assert(false);
2114 }
2115 a.check_error();
2116 return expr(a.ctx(), r);
2117 }
Z3_mk_fpa_sub
Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point subtraction.
Z3_mk_bvsub
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
Z3_mk_sub
Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] - ... - args[num_args - 1].

◆ operator- [3/4]

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

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

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

◆ operator- [4/4]

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

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

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

◆ operator/ [1/3]

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

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

2055 {
2056 check_context(a, b);
2057 Z3_ast r = 0;
2058 if (a.is_arith() && b.is_arith()) {
2059 r = Z3_mk_div(a.ctx(), a, b);
2060 }
2061 else if (a.is_bv() && b.is_bv()) {
2062 r = Z3_mk_bvsdiv(a.ctx(), a, b);
2063 }
2064 else if (a.is_fpa() && b.is_fpa()) {
2065 r = Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
2066 }
2067 else {
2068 // operator is not supported by given arguments.
2069 assert(false);
2070 }
2071 a.check_error();
2072 return expr(a.ctx(), r);
2073 }
Z3_mk_div
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.
Z3_mk_bvsdiv
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.
Z3_mk_fpa_div
Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point division.

Referenced by operator/, operator/, and operator/.

◆ operator/ [2/3]

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

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

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

◆ operator/ [3/3]

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

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

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

◆ operator< [1/3]

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

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

2146 {
2147 check_context(a, b);
2148 Z3_ast r = 0;
2149 if (a.is_arith() && b.is_arith()) {
2150 r = Z3_mk_lt(a.ctx(), a, b);
2151 }
2152 else if (a.is_bv() && b.is_bv()) {
2153 r = Z3_mk_bvslt(a.ctx(), a, b);
2154 }
2155 else if (a.is_fpa() && b.is_fpa()) {
2156 r = Z3_mk_fpa_lt(a.ctx(), a, b);
2157 }
2158 else {
2159 // operator is not supported by given arguments.
2160 assert(false);
2161 }
2162 a.check_error();
2163 return expr(a.ctx(), r);
2164 }
Z3_mk_bvslt
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than.
Z3_mk_lt
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
Z3_mk_fpa_lt
Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than.

Referenced by operator<, operator<, and operator<.

◆ operator< [2/3]

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

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

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

◆ operator< [3/3]

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

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

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

◆ operator<= [1/3]

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

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

2121 {
2122 check_context(a, b);
2123 Z3_ast r = 0;
2124 if (a.is_arith() && b.is_arith()) {
2125 r = Z3_mk_le(a.ctx(), a, b);
2126 }
2127 else if (a.is_bv() && b.is_bv()) {
2128 r = Z3_mk_bvsle(a.ctx(), a, b);
2129 }
2130 else if (a.is_fpa() && b.is_fpa()) {
2131 r = Z3_mk_fpa_leq(a.ctx(), a, b);
2132 }
2133 else {
2134 // operator is not supported by given arguments.
2135 assert(false);
2136 }
2137 a.check_error();
2138 return expr(a.ctx(), r);
2139 }
Z3_mk_bvsle
Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than or equal to.
Z3_mk_le
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
Z3_mk_fpa_leq
Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than or equal.

Referenced by operator<=, operator<=, and operator<=.

◆ operator<= [2/3]

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

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

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

◆ operator<= [3/3]

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

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

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

◆ operator== [1/3]

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

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

1950 {
1951 check_context(a, b);
1952 Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1953 a.check_error();
1954 return expr(a.ctx(), r);
1955 }
Z3_mk_eq
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.

Referenced by operator==, operator==, and operator==.

◆ operator== [2/3]

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

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

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

◆ operator== [3/3]

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

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

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

◆ operator> [1/3]

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

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

2168 {
2169 check_context(a, b);
2170 Z3_ast r = 0;
2171 if (a.is_arith() && b.is_arith()) {
2172 r = Z3_mk_gt(a.ctx(), a, b);
2173 }
2174 else if (a.is_bv() && b.is_bv()) {
2175 r = Z3_mk_bvsgt(a.ctx(), a, b);
2176 }
2177 else if (a.is_fpa() && b.is_fpa()) {
2178 r = Z3_mk_fpa_gt(a.ctx(), a, b);
2179 }
2180 else {
2181 // operator is not supported by given arguments.
2182 assert(false);
2183 }
2184 a.check_error();
2185 return expr(a.ctx(), r);
2186 }
Z3_mk_bvsgt
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than.
Z3_mk_fpa_gt
Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than.
Z3_mk_gt
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.

Referenced by operator>, operator>, and operator>.

◆ operator> [2/3]

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

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

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

◆ operator> [3/3]

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

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

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

◆ operator>= [1/3]

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

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

2035 {
2036 check_context(a, b);
2037 Z3_ast r = 0;
2038 if (a.is_arith() && b.is_arith()) {
2039 r = Z3_mk_ge(a.ctx(), a, b);
2040 }
2041 else if (a.is_bv() && b.is_bv()) {
2042 r = Z3_mk_bvsge(a.ctx(), a, b);
2043 }
2044 else if (a.is_fpa() && b.is_fpa()) {
2045 r = Z3_mk_fpa_geq(a.ctx(), a, b);
2046 }
2047 else {
2048 // operator is not supported by given arguments.
2049 assert(false);
2050 }
2051 a.check_error();
2052 return expr(a.ctx(), r);
2053 }
Z3_mk_bvsge
Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than or equal to.
Z3_mk_fpa_geq
Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than or equal.

Referenced by operator>=, operator>=, and operator>=.

◆ operator>= [2/3]

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

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

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

◆ operator>= [3/3]

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

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

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

◆ operator^ [1/3]

expr operator^ ( expr const & a,
expr const & b )
friend

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

2194{ 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_mk_bvxor
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
Z3_mk_xor
Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 xor t2.

Referenced by operator^, operator^, and operator^.

◆ operator^ [2/3]

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

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

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

◆ operator^ [3/3]

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

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

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

◆ operator| [1/3]

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

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

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

Referenced by operator|, operator|, and operator|.

◆ operator| [2/3]

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

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

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

◆ operator| [3/3]

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

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

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

◆ operator|| [1/3]

expr operator|| ( bool a,
expr const & b )
friend

Return an expression representing a or b. The C++ Boolean value a is automatically converted into a Z3 Boolean constant.

Precondition
b.is_bool()

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

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

◆ operator|| [2/3]

expr operator|| ( expr const & a,
bool b )
friend

Return an expression representing a or b. The C++ Boolean value b is automatically converted into a Z3 Boolean constant.

Precondition
a.is_bool()

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

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

◆ operator|| [3/3]

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

Return an expression representing a or b.

Precondition
a.is_bool()
b.is_bool()

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

1937 {
1938 check_context(a, b);
1939 assert(a.is_bool() && b.is_bool());
1940 Z3_ast args[2] = { a, b };
1941 Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1942 a.check_error();
1943 return expr(a.ctx(), r);
1944 }

Referenced by operator||, operator||, and operator||.

◆ operator~

expr operator~ ( expr const & a)
friend

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

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

Referenced by operator~.

◆ pbeq

expr pbeq ( expr_vector const & es,
int const * coeffs,
int bound )
friend

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

2689 {
2690 assert(es.size() > 0);
2691 context& ctx = es[0u].ctx();
2692 array<Z3_ast> _es(es);
2693 Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
2694 ctx.check_error();
2695 return expr(ctx, r);
2696 }
Z3_mk_pbeq
Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.

Referenced by pbeq.

◆ pbge

expr pbge ( expr_vector const & es,
int const * coeffs,
int bound )
friend

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

2681 {
2682 assert(es.size() > 0);
2683 context& ctx = es[0u].ctx();
2684 array<Z3_ast> _es(es);
2685 Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
2686 ctx.check_error();
2687 return expr(ctx, r);
2688 }
Z3_mk_pbge
Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.

Referenced by pbge.

◆ pble

expr pble ( expr_vector const & es,
int const * coeffs,
int bound )
friend

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

2673 {
2674 assert(es.size() > 0);
2675 context& ctx = es[0u].ctx();
2676 array<Z3_ast> _es(es);
2677 Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
2678 ctx.check_error();
2679 return expr(ctx, r);
2680 }
Z3_mk_pble
Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.

Referenced by pble.

◆ pw [1/3]

expr pw ( expr const & a,
expr const & b )
friend

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

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

Referenced by pw, pw, and pw.

◆ pw [2/3]

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

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

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

◆ pw [3/3]

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

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

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

◆ range

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

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

4631 {
4632 check_context(lo, hi);
4633 Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
4634 lo.check_error();
4635 return expr(lo.ctx(), r);
4636 }
Z3_mk_re_range
Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi)
Create the range regular expression over two sequences of length 1.

Referenced by range.

◆ rem [1/3]

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

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

1881 {
1882 if (a.is_fpa() && b.is_fpa()) {
1883 _Z3_MK_BIN_(a, b, Z3_mk_fpa_rem);
1884 } else {
1885 _Z3_MK_BIN_(a, b, Z3_mk_rem);
1886 }
1887 }
Z3_mk_fpa_rem
Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point remainder.
Z3_mk_rem
Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 rem arg2.

Referenced by rem, rem, and rem.

◆ rem [2/3]

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

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

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

◆ rem [3/3]

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

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

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

◆ round_fpa_to_closest_integer

expr round_fpa_to_closest_integer ( expr const & t)
friend

Round a floating-point term into its closest integer.

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

2336 {
2337 assert(t.is_fpa());
2338 Z3_ast r = Z3_mk_fpa_round_to_integral(t.ctx(), t.ctx().fpa_rounding_mode(), t);
2339 t.check_error();
2340 return expr(t.ctx(), r);
2341 }
Z3_mk_fpa_round_to_integral
Z3_ast Z3_API Z3_mk_fpa_round_to_integral(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point roundToIntegral. Rounds a floating-point number to the closest integer,...

Referenced by round_fpa_to_closest_integer.

◆ sbv_to_fpa

expr sbv_to_fpa ( expr const & t,
sort s )
friend

Conversion of a signed bit-vector term into a floating-point.

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

2315 {
2316 assert(t.is_bv());
2317 Z3_ast r = Z3_mk_fpa_to_fp_signed(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2318 t.check_error();
2319 return expr(t.ctx(), r);
2320 }
Z3_mk_fpa_to_fp_signed
Z3_ast Z3_API Z3_mk_fpa_to_fp_signed(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.

Referenced by sbv_to_fpa.

◆ sqrt

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

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

2269 {
2270 check_context(a, rm);
2271 assert(a.is_fpa());
2272 Z3_ast r = Z3_mk_fpa_sqrt(a.ctx(), rm, a);
2273 a.check_error();
2274 return expr(a.ctx(), r);
2275 }
Z3_mk_fpa_sqrt
Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point square root.

Referenced by sqrt.

◆ sum

expr sum ( expr_vector const & args)
friend

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

2713 {
2714 assert(args.size() > 0);
2715 context& ctx = args[0u].ctx();
2716 array<Z3_ast> _args(args);
2717 Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
2718 ctx.check_error();
2719 return expr(ctx, r);
2720 }

Referenced by sum.

◆ ubv_to_fpa

expr ubv_to_fpa ( expr const & t,
sort s )
friend

Conversion of an unsigned bit-vector term into a floating-point.

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

2322 {
2323 assert(t.is_bv());
2324 Z3_ast r = Z3_mk_fpa_to_fp_unsigned(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2325 t.check_error();
2326 return expr(t.ctx(), r);
2327 }
Z3_mk_fpa_to_fp_unsigned
Z3_ast Z3_API Z3_mk_fpa_to_fp_unsigned(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort.

Referenced by ubv_to_fpa.

◆ xnor

expr xnor ( expr const & a,
expr const & b )
friend

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

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

Referenced by xnor.

Generated by doxygen 1.18.0