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_arith () const
 Return true if this is an integer or real 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 996 of file z3++.h.

Constructor & Destructor Documentation

◆ expr() [1/2]

expr ( context &  c)
inline

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

998:ast(c) {}
z3::ast::ast
ast(context &c)
Definition z3++.h:643

◆ expr() [2/2]

expr ( context &  c,
Z3_ast  n 
)
inline

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

999:ast(c, reinterpret_cast<Z3_ast>(n)) {}
Microsoft.Z3.Z3_ast
System.IntPtr Z3_ast
Definition NativeContext.cs:28

Member Function Documentation

◆ algebraic_i()

unsigned algebraic_i ( ) const
inline

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

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

1233 {
1234 assert(is_algebraic());
1235 unsigned i = Z3_algebraic_get_i(ctx(), m_ast);
1236 check_error();
1237 return i;
1238 }
z3::ast::m_ast
Z3_ast m_ast
Definition z3++.h:641
z3::expr::is_algebraic
bool is_algebraic() const
Return true if expression is an algebraic number.
Definition z3++.h:1115
z3::object::check_error
Z3_error_code check_error() const
Definition z3++.h:563
z3::object::ctx
context & ctx() const
Definition z3++.h:562
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 1206 of file z3++.h.

1206 {
1207 assert(is_algebraic());
1208 Z3_ast r = Z3_get_algebraic_number_lower(ctx(), m_ast, precision);
1209 check_error();
1210 return expr(ctx(), r);
1211 }
z3::expr::expr
expr(context &c)
Definition z3++.h:998
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 1223 of file z3++.h.

1223 {
1224 assert(is_algebraic());
1225 Z3_ast_vector r = Z3_algebraic_get_poly(ctx(), m_ast);
1226 check_error();
1227 return expr_vector(ctx(), r);
1228 }
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.
Microsoft.Z3.Z3_ast_vector
System.IntPtr Z3_ast_vector
Definition NativeContext.cs:29
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 1213 of file z3++.h.

1213 {
1214 assert(is_algebraic());
1215 Z3_ast r = Z3_get_algebraic_number_upper(ctx(), m_ast, precision);
1216 check_error();
1217 return expr(ctx(), r);
1218 }
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 1394 of file z3++.h.

1394{ 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__(), expr::args(), ExprRef::children(), 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 1401 of file z3++.h.

1401 {
1402 expr_vector vec(ctx());
1403 unsigned argCnt = num_args();
1404 for (unsigned i = 0; i < argCnt; ++i)
1405 vec.push_back(arg(i));
1406 return vec;
1407 }
z3::expr::num_args
unsigned num_args() const
Return the number of arguments in this application. This method assumes the expression is an applicat...
Definition z3++.h:1386
z3::expr::arg
expr arg(unsigned i) const
Return the i-th argument of this application. This method assumes the expression is an application.
Definition z3++.h:1394

Referenced by expr::update().

◆ as_binary()

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

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

1075{ if (!is_numeral()) return false; s = Z3_get_numeral_binary_string(ctx(), m_ast); check_error(); return true; }
z3::expr::is_numeral
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
Definition z3++.h:1067
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 1077 of file z3++.h.

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

◆ as_int64()

int64_t as_int64 ( ) const
inline

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

1079{ int64_t r = 0; is_numeral_i64(r); return r; }
z3::expr::is_numeral_i64
bool is_numeral_i64(int64_t &i) const
Definition z3++.h:1068

◆ as_uint64()

uint64_t as_uint64 ( ) const
inline

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

1078{ uint64_t r = 0; is_numeral_u64(r); return r; }
z3::expr::is_numeral_u64
bool is_numeral_u64(uint64_t &i) const
Definition z3++.h:1069

◆ at()

expr at ( expr const &  index) const
inline

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

1697 {
1698 check_context(*this, index);
1699 Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
1700 check_error();
1701 return expr(ctx(), r);
1702 }
z3::object::check_context
friend void check_context(object const &a, object const &b)
Definition z3++.h:566
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...

◆ begin()

iterator begin ( )
inline

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

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

◆ bit2bool()

expr bit2bool ( unsigned  i) const
inline

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

1627{ Z3_ast r = Z3_mk_bit2bool(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); }
z3::context::check_error
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
Definition z3++.h:241
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 1435 of file z3++.h.

1435{ assert(is_quantifier()); Z3_ast r = Z3_get_quantifier_body(ctx(), *this); check_error(); return expr(ctx(), r); }
z3::expr::is_quantifier
bool is_quantifier() const
Return true if this expression is a quantifier.
Definition z3++.h:1093
Z3_get_quantifier_body
Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)
Return body of quantifier.

Referenced by QuantifierRef::children().

◆ bool_value()

Z3_lbool bool_value ( ) const
inline

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

1319 {
1320 return Z3_get_bool_value(ctx(), m_ast);
1321 }
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 1750 of file z3++.h.

1750 {
1751 Z3_ast r = Z3_mk_char_from_bv(ctx(), *this);
1752 check_error();
1753 return expr(ctx(), r);
1754 }
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 1745 of file z3++.h.

1745 {
1746 Z3_ast r = Z3_mk_char_to_bv(ctx(), *this);
1747 check_error();
1748 return expr(ctx(), r);
1749 }
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 1740 of file z3++.h.

1740 {
1741 Z3_ast r = Z3_mk_char_to_int(ctx(), *this);
1742 check_error();
1743 return expr(ctx(), r);
1744 }
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 1691 of file z3++.h.

1691 {
1692 check_context(*this, s);
1693 Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
1694 check_error();
1695 return expr(ctx(), r);
1696 }
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 1379 of file z3++.h.

1379{ 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.
Microsoft.Z3.Z3_func_decl
System.IntPtr Z3_func_decl
Definition NativeContext.cs:30

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

◆ denominator()

expr denominator ( ) const
inline

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

1331 {
1332 assert(is_numeral());
1333 Z3_ast r = Z3_get_denominator(ctx(), m_ast);
1334 check_error();
1335 return expr(ctx(),r);
1336 }
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.

Referenced by RatNumRef::denominator_as_long(), and RatNumRef::is_int_value().

◆ end()

iterator end ( )
inline

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

1833{ return iterator(*this, is_app() ? num_args() : 0); }
z3::expr::is_app
bool is_app() const
Return true if this expression is an application.
Definition z3++.h:1085

◆ ext_rotate_left()

expr ext_rotate_left ( expr const &  n) const
inline

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

1614{ 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 1615 of file z3++.h.

1615{ 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 1676 of file z3++.h.

1676 {
1677 check_context(*this, offset); check_context(offset, length);
1678 Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r);
1679 }
z3::expr::length
expr length() const
Definition z3++.h:1709
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 1626 of file z3++.h.

1626{ Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); }
z3::expr::hi
unsigned hi() const
Definition z3++.h:1629
z3::expr::lo
unsigned lo() const
Definition z3++.h:1628
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 1198 of file z3++.h.

1198 {
1199 assert(is_numeral() || is_algebraic());
1200 return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
1201 }
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 1255 of file z3++.h.

1255 {
1256 int result = 0;
1257 if (!is_numeral_i(result)) {
1258 assert(ctx().enable_exceptions());
1259 if (!ctx().enable_exceptions()) return 0;
1260 Z3_THROW(exception("numeral does not fit in machine int"));
1261 }
1262 return result;
1263 }
z3::expr::is_numeral_i
bool is_numeral_i(int &i) const
Definition z3++.h:1070
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 1291 of file z3++.h.

1291 {
1292 assert(is_numeral());
1293 int64_t result = 0;
1294 if (!is_numeral_i64(result)) {
1295 assert(ctx().enable_exceptions());
1296 if (!ctx().enable_exceptions()) return 0;
1297 Z3_THROW(exception("numeral does not fit in machine int64_t"));
1298 }
1299 return result;
1300 }

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

1274 {
1275 assert(is_numeral());
1276 unsigned result = 0;
1277 if (!is_numeral_u(result)) {
1278 assert(ctx().enable_exceptions());
1279 if (!ctx().enable_exceptions()) return 0;
1280 Z3_THROW(exception("numeral does not fit in machine uint"));
1281 }
1282 return result;
1283 }
z3::expr::is_numeral_u
bool is_numeral_u(unsigned &i) const
Definition z3++.h:1071

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

1308 {
1309 assert(is_numeral());
1310 uint64_t result = 0;
1311 if (!is_numeral_u64(result)) {
1312 assert(ctx().enable_exceptions());
1313 if (!ctx().enable_exceptions()) return 0;
1314 Z3_THROW(exception("numeral does not fit in machine uint64_t"));
1315 }
1316 return result;
1317 }

◆ get_sort()

sort get_sort ( ) const
inline

Return the sort of this expression.

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

1004{ Z3_sort s = Z3_get_sort(*m_ctx, m_ast); check_error(); return sort(*m_ctx, s); }
z3::object::m_ctx
context * m_ctx
Definition z3++.h:558
Z3_get_sort
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.
Microsoft.Z3.Z3_sort
System.IntPtr Z3_sort
Definition NativeContext.cs:33

Referenced by expr::is_arith(), expr::is_array(), expr::is_bool(), expr::is_bv(), expr::is_datatype(), expr::is_finite_domain(), expr::is_finite_field(), expr::is_fpa(), expr::is_int(), expr::is_re(), expr::is_real(), expr::is_relation(), expr::is_seq(), and ModelRef::sorts().

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

1350 {
1351 assert(is_string_value());
1352 char const* s = Z3_get_string(ctx(), m_ast);
1353 check_error();
1354 return std::string(s);
1355 }
z3::expr::is_string_value
bool is_string_value() const
Return true if this expression is a string literal. The string can be accessed using get_string() and...
Definition z3++.h:1343
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...

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

1362 {
1363 assert(is_string_value());
1364 unsigned n = Z3_get_string_length(ctx(), m_ast);
1365 std::u32string s;
1366 s.resize(n);
1367 Z3_get_string_contents(ctx(), m_ast, n, (unsigned*)s.data());
1368 return s;
1369 }
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 1629 of file z3++.h.

1629{ assert (is_app() && Z3_get_decl_num_parameters(ctx(), decl()) == 2); return static_cast<unsigned>(Z3_get_decl_int_parameter(ctx(), decl(), 0)); }
z3::expr::decl
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
Definition z3++.h:1379
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 expr::extract(), and expr::loop().

◆ id()

unsigned id ( ) const
inline

retrieve unique identifier for expression.

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

1243{ 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 1115 of file z3++.h.

1115{ 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 expr::algebraic_i(), expr::algebraic_lower(), expr::algebraic_poly(), expr::algebraic_upper(), and expr::get_decimal_string().

◆ is_and()

bool is_and ( ) const
inline

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

1504{ return is_app() && Z3_OP_AND == decl().decl_kind(); }
z3::func_decl::decl_kind
Z3_decl_kind decl_kind() const
Definition z3++.h:922
Z3_OP_AND
@ Z3_OP_AND
Definition z3_api.h:996

◆ is_app()

bool is_app ( ) const
inline

Return true if this expression is an application.

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

1085{ return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }
z3::ast::kind
Z3_ast_kind kind() const
Definition z3++.h:657
Z3_APP_AST
@ Z3_APP_AST
Definition z3_api.h:145
Z3_NUMERAL_AST
@ Z3_NUMERAL_AST
Definition z3_api.h:144

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

◆ is_arith()

bool is_arith ( ) const
inline

Return true if this is an integer or real expression.

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

1021{ return get_sort().is_arith(); }
z3::expr::get_sort
sort get_sort() const
Return the sort of this expression.
Definition z3++.h:1004
z3::sort::is_arith
bool is_arith() const
Return true if this sort is the Integer or Real sort.
Definition z3++.h:838

◆ is_array()

bool is_array ( ) const
inline

Return true if this is a Array expression.

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

1029{ return get_sort().is_array(); }
z3::sort::is_array
bool is_array() const
Return true if this sort is a Array sort.
Definition z3++.h:846

Referenced by expr::operator[]().

◆ is_bool()

bool is_bool ( ) const
inline

Return true if this is a Boolean expression.

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

1009{ return get_sort().is_bool(); }
z3::sort::is_bool
bool is_bool() const
Return true if this sort is the Boolean sort.
Definition z3++.h:826

Referenced by solver::add(), optimize::add(), optimize::add(), solver::add(), optimize::add(), optimize::add_soft(), and optimize::add_soft().

◆ is_bv()

bool is_bv ( ) const
inline

Return true if this is a Bit-vector expression.

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

1025{ return get_sort().is_bv(); }
z3::sort::is_bv
bool is_bv() const
Return true if this sort is a Bit-vector sort.
Definition z3++.h:842

Referenced by expr::mk_from_ieee_bv().

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

1089{ 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 1033 of file z3++.h.

1033{ return get_sort().is_datatype(); }
z3::sort::is_datatype
bool is_datatype() const
Return true if this sort is a Datatype sort.
Definition z3++.h:850

Referenced by expr::update_field().

◆ is_digit()

expr is_digit ( ) const
inline

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

1755 {
1756 Z3_ast r = Z3_mk_char_is_digit(ctx(), *this);
1757 check_error();
1758 return expr(ctx(), r);
1759 }
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 1510 of file z3++.h.

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

◆ is_eq()

bool is_eq ( ) const
inline

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

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

◆ is_exists()

bool is_exists ( ) const
inline

Return true if this expression is an existential quantifier.

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

1102{ 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 1502 of file z3++.h.

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

◆ is_finite_domain()

bool is_finite_domain ( ) const
inline

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

1056{ return get_sort().is_finite_domain(); }
z3::sort::is_finite_domain
bool is_finite_domain() const
Definition z3++.h:867

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

1055{ return get_sort().is_finite_field(); }
z3::sort::is_finite_field
bool is_finite_field() const
Return true if this sort is a Finite domain sort.
Definition z3++.h:866

◆ is_forall()

bool is_forall ( ) const
inline

Return true if this expression is a universal quantifier.

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

1098{ 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 1060 of file z3++.h.

1060{ return get_sort().is_fpa(); }
z3::sort::is_fpa
bool is_fpa() const
Return true if this sort is a Floating point sort.
Definition z3++.h:871

Referenced by expr::mk_is_inf(), expr::mk_is_nan(), expr::mk_is_normal(), expr::mk_is_subnormal(), expr::mk_is_zero(), and expr::mk_to_ieee_bv().

◆ is_implies()

bool is_implies ( ) const
inline

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

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

◆ is_int()

bool is_int ( ) const
inline

Return true if this is an integer expression.

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

1013{ return get_sort().is_int(); }
z3::sort::is_int
bool is_int() const
Return true if this sort is the Integer sort.
Definition z3++.h:830

Referenced by IntNumRef::as_long(), and ArithSortRef::subsort().

◆ is_ite()

bool is_ite ( ) const
inline

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

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

◆ is_lambda()

bool is_lambda ( ) const
inline

Return true if this expression is a lambda expression.

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

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

Referenced by QuantifierRef::__getitem__(), and QuantifierRef::sort().

◆ is_not()

bool is_not ( ) const
inline

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

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

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

1067{ return kind() == Z3_NUMERAL_AST; }

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

◆ is_numeral() [2/4]

bool is_numeral ( double &  d) const
inline

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

1074{ 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 expr::is_numeral().

◆ is_numeral() [3/4]

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

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

1072{ 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 expr::is_numeral().

◆ is_numeral() [4/4]

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

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

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

Referenced by expr::is_numeral().

◆ is_numeral_i()

bool is_numeral_i ( int &  i) const
inline

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

1070{ 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 expr::get_numeral_int().

◆ is_numeral_i64()

bool is_numeral_i64 ( int64_t &  i) const
inline

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

1068{ 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 expr::as_int64(), and expr::get_numeral_int64().

◆ is_numeral_u()

bool is_numeral_u ( unsigned &  i) const
inline

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

1071{ 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 expr::get_numeral_uint().

◆ is_numeral_u64()

bool is_numeral_u64 ( uint64_t &  i) const
inline

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

1069{ 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 expr::as_uint64(), and expr::get_numeral_uint64().

◆ is_or()

bool is_or ( ) const
inline

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

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

◆ is_quantifier()

bool is_quantifier ( ) const
inline

Return true if this expression is a quantifier.

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

1093{ return kind() == Z3_QUANTIFIER_AST; }
Z3_QUANTIFIER_AST
@ Z3_QUANTIFIER_AST
Definition z3_api.h:147

Referenced by expr::body().

◆ is_re()

bool is_re ( ) const
inline

Return true if this is a regular expression.

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

1045{ return get_sort().is_re(); }
z3::sort::is_re
bool is_re() const
Return true if this sort is a regular expression sort.
Definition z3++.h:862

◆ is_real()

bool is_real ( ) const
inline

Return true if this is a real expression.

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

1017{ return get_sort().is_real(); }
z3::sort::is_real
bool is_real() const
Return true if this sort is the Real sort.
Definition z3++.h:834

◆ is_relation()

bool is_relation ( ) const
inline

Return true if this is a Relation expression.

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

1037{ return get_sort().is_relation(); }
z3::sort::is_relation
bool is_relation() const
Return true if this sort is a Relation sort.
Definition z3++.h:854

◆ is_seq()

bool is_seq ( ) const
inline

Return true if this is a sequence expression.

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

1041{ return get_sort().is_seq(); }
z3::sort::is_seq
bool is_seq() const
Return true if this sort is a Sequence sort.
Definition z3++.h:858

Referenced by expr::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 1343 of file z3++.h.

1343{ 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 expr::get_string(), and expr::get_u32string().

◆ is_true()

bool is_true ( ) const
inline

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

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

◆ is_var()

bool is_var ( ) const
inline

Return true if this expression is a variable.

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

1111{ return kind() == Z3_VAR_AST; }
Z3_VAR_AST
@ Z3_VAR_AST
Definition z3_api.h:146

◆ is_well_sorted()

bool is_well_sorted ( ) const
inline

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

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

1120{ 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 1506 of file z3++.h.

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

◆ itos()

expr itos ( ) const
inline

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

1725 {
1726 Z3_ast r = Z3_mk_int_to_str(ctx(), *this);
1727 check_error();
1728 return expr(ctx(), r);
1729 }
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 1709 of file z3++.h.

1709 {
1710 Z3_ast r = Z3_mk_seq_length(ctx(), *this);
1711 check_error();
1712 return expr(ctx(), r);
1713 }
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 expr::extract().

◆ lo()

unsigned lo ( ) const
inline

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

1628{ 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 expr::extract(), expr::loop(), and expr::loop().

◆ loop() [1/2]

expr loop ( unsigned  lo)
inline

create a looping regular expression.

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

1765 {
1766 Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, 0);
1767 check_error();
1768 return expr(ctx(), r);
1769 }
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 1770 of file z3++.h.

1770 {
1771 Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, hi);
1772 check_error();
1773 return expr(ctx(), r);
1774 }

◆ mk_from_ieee_bv()

expr mk_from_ieee_bv ( sort const &  s) const
inline

Convert this IEEE BV into a fpa.

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

1185 {
1186 assert(is_bv());
1187 Z3_ast r = Z3_mk_fpa_to_fp_bv(ctx(), m_ast, s);
1188 check_error();
1189 return expr(ctx(), r);
1190 }
z3::expr::is_bv
bool is_bv() const
Return true if this is a Bit-vector expression.
Definition z3++.h:1025
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.

◆ mk_is_inf()

expr mk_is_inf ( ) const
inline

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

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

1125 {
1126 assert(is_fpa());
1127 Z3_ast r = Z3_mk_fpa_is_infinite(ctx(), m_ast);
1128 check_error();
1129 return expr(ctx(), r);
1130 }
z3::expr::is_fpa
bool is_fpa() const
Return true if this is a FloatingPoint expression. .
Definition z3++.h:1060
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 1135 of file z3++.h.

1135 {
1136 assert(is_fpa());
1137 Z3_ast r = Z3_mk_fpa_is_nan(ctx(), m_ast);
1138 check_error();
1139 return expr(ctx(), r);
1140 }
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 1145 of file z3++.h.

1145 {
1146 assert(is_fpa());
1147 Z3_ast r = Z3_mk_fpa_is_normal(ctx(), m_ast);
1148 check_error();
1149 return expr(ctx(), r);
1150 }
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 1155 of file z3++.h.

1155 {
1156 assert(is_fpa());
1157 Z3_ast r = Z3_mk_fpa_is_subnormal(ctx(), m_ast);
1158 check_error();
1159 return expr(ctx(), r);
1160 }
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 1165 of file z3++.h.

1165 {
1166 assert(is_fpa());
1167 Z3_ast r = Z3_mk_fpa_is_zero(ctx(), m_ast);
1168 check_error();
1169 return expr(ctx(), r);
1170 }
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 1175 of file z3++.h.

1175 {
1176 assert(is_fpa());
1177 Z3_ast r = Z3_mk_fpa_to_ieee_bv(ctx(), m_ast);
1178 check_error();
1179 return expr(ctx(), r);
1180 }
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 1703 of file z3++.h.

1703 {
1704 check_context(*this, index);
1705 Z3_ast r = Z3_mk_seq_nth(ctx(), *this, index);
1706 check_error();
1707 return expr(ctx(), r);
1708 }
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 expr::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 1386 of file z3++.h.

1386{ 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__(), ExprRef::arg(), FuncEntry::arg_value(), expr::args(), FuncEntry::as_list(), ExprRef::children(), expr::end(), expr::is_const(), and ExprRef::update().

◆ numerator()

expr numerator ( ) const
inline

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

1323 {
1324 assert(is_numeral());
1325 Z3_ast r = Z3_get_numerator(ctx(), m_ast);
1326 check_error();
1327 return expr(ctx(),r);
1328 }
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.

Referenced by RatNumRef::numerator_as_long().

◆ operator Z3_app()

operator Z3_app ( ) const
inline

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

1371{ assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
Microsoft.Z3.Z3_app
System.IntPtr Z3_app
Definition NativeContext.cs:27

◆ operator[]() [1/2]

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

index operator defined on arrays and sequences.

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

1779 {
1780 assert(is_array() || is_seq());
1781 if (is_array()) {
1782 return select(*this, index);
1783 }
1784 return nth(index);
1785 }
z3::expr::is_array
bool is_array() const
Return true if this is a Array expression.
Definition z3++.h:1029
z3::expr::nth
expr nth(expr const &index) const
Definition z3++.h:1703
z3::expr::is_seq
bool is_seq() const
Return true if this is a sequence expression.
Definition z3++.h:1041
z3::select
expr select(expr const &a, expr const &i)
forward declarations
Definition z3++.h:4347

◆ operator[]() [2/2]

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

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

1787 {
1788 return select(*this, index);
1789 }

◆ power()

expr power ( expr const &  n) const
inline

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

1714 {
1715 check_context(*this, n);
1716 Z3_ast r = Z3_mk_seq_power(ctx(), *this, n);
1717 check_error();
1718 return expr(ctx(), r);
1719 }
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 1616 of file z3++.h.

1616{ 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 1680 of file z3++.h.

1680 {
1681 check_context(*this, src); check_context(src, dst);
1682 Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
1683 check_error();
1684 return expr(ctx(), r);
1685 }
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 1612 of file z3++.h.

1612{ 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 1613 of file z3++.h.

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

1735 {
1736 Z3_ast r = Z3_mk_sbv_to_str(ctx(), *this);
1737 check_error();
1738 return expr(ctx(), r);
1739 }
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 1794 of file z3++.h.

1794{ 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 1798 of file z3++.h.

1798{ 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 1720 of file z3++.h.

1720 {
1721 Z3_ast r = Z3_mk_str_to_int(ctx(), *this);
1722 check_error();
1723 return expr(ctx(), r);
1724 }
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 4696 of file z3++.h.

4696 {
4697 array<Z3_ast> _dst(dst.size());
4698 for (unsigned i = 0; i < dst.size(); ++i) {
4699 _dst[i] = dst[i];
4700 }
4701 Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
4702 check_error();
4703 return expr(ctx(), r);
4704 }
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 4683 of file z3++.h.

4683 {
4684 assert(src.size() == dst.size());
4685 array<Z3_ast> _src(src.size());
4686 array<Z3_ast> _dst(dst.size());
4687 for (unsigned i = 0; i < src.size(); ++i) {
4688 _src[i] = src[i];
4689 _dst[i] = dst[i];
4690 }
4691 Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
4692 check_error();
4693 return expr(ctx(), r);
4694 }
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 4706 of file z3++.h.

4706 {
4707 array<Z3_ast> _dst(dst.size());
4708 array<Z3_func_decl> _funs(funs.size());
4709 if (dst.size() != funs.size()) {
4710 Z3_THROW(exception("length of argument lists don't align"));
4711 return expr(ctx(), nullptr);
4712 }
4713 for (unsigned i = 0; i < dst.size(); ++i) {
4714 _dst[i] = dst[i];
4715 _funs[i] = funs[i];
4716 }
4717 Z3_ast r = Z3_substitute_funs(ctx(), m_ast, dst.size(), _funs.ptr(), _dst.ptr());
4718 check_error();
4719 return expr(ctx(), r);
4720 }
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 1730 of file z3++.h.

1730 {
1731 Z3_ast r = Z3_mk_ubv_to_str(ctx(), *this);
1732 check_error();
1733 return expr(ctx(), r);
1734 }
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 1686 of file z3++.h.

1686 {
1687 Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
1688 check_error();
1689 return expr(ctx(), r);
1690 }
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 4722 of file z3++.h.

4722 {
4723 array<Z3_ast> _args(args.size());
4724 for (unsigned i = 0; i < args.size(); ++i) {
4725 _args[i] = args[i];
4726 }
4727 Z3_ast r = Z3_update_term(ctx(), m_ast, args.size(), _args.ptr());
4728 check_error();
4729 return expr(ctx(), r);
4730 }
z3::ast_vector_tpl::size
unsigned size() const
Definition z3++.h:686
z3::expr::args
expr_vector args() const
Return a vector of all the arguments of this application. This method assumes the expression is an ap...
Definition z3++.h:1401
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 4732 of file z3++.h.

4732 {
4733 assert(is_datatype());
4734 Z3_ast r = Z3_datatype_update_field(ctx(), field_access, m_ast, new_value);
4735 check_error();
4736 return expr(ctx(), r);
4737 }
z3::expr::is_datatype
bool is_datatype() const
Return true if this is a Datatype expression.
Definition z3++.h:1033
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.

Friends And Related Symbol Documentation

◆ abs

expr abs ( expr const &  a)
friend

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

2220 {
2221 Z3_ast r;
2222 if (a.is_int()) {
2223 expr zero = a.ctx().int_val(0);
2224 expr ge = a >= zero;
2225 expr na = -a;
2226 r = Z3_mk_ite(a.ctx(), ge, a, na);
2227 }
2228 else if (a.is_real()) {
2229 expr zero = a.ctx().real_val(0);
2230 expr ge = a >= zero;
2231 expr na = -a;
2232 r = Z3_mk_ite(a.ctx(), ge, a, na);
2233 }
2234 else {
2235 r = Z3_mk_fpa_abs(a.ctx(), a);
2236 }
2237 a.check_error();
2238 return expr(a.ctx(), r);
2239 }
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.

◆ atleast

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

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

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

◆ atmost

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

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

2668 {
2669 assert(es.size() > 0);
2670 context& ctx = es[0u].ctx();
2671 array<Z3_ast> _es(es);
2672 Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
2673 ctx.check_error();
2674 return expr(ctx, r);
2675 }
Z3_mk_atmost
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.

◆ bv2int

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

bit-vector and integer conversions.

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

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

◆ bvadd_no_overflow

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

bit-vector overflow/underflow checks

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

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

◆ bvadd_no_underflow

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

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

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

◆ bvmul_no_overflow

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

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

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

◆ bvmul_no_underflow

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

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

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

◆ bvneg_no_overflow

expr bvneg_no_overflow ( expr const &  a)
friend

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

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

◆ bvredand

expr bvredand ( expr const &  a)
friend

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

2214 {
2215 assert(a.is_bv());
2216 Z3_ast r = Z3_mk_bvredand(a.ctx(), a);
2217 a.check_error();
2218 return expr(a.ctx(), r);
2219 }
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.

◆ bvredor

expr bvredor ( expr const &  a)
friend

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

2208 {
2209 assert(a.is_bv());
2210 Z3_ast r = Z3_mk_bvredor(a.ctx(), a);
2211 a.check_error();
2212 return expr(a.ctx(), r);
2213 }
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.

◆ bvsdiv_no_overflow

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

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

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

◆ bvsub_no_overflow

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

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

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

◆ bvsub_no_underflow

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

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

2481 {
2482 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);
2483 }
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.

◆ concat [1/2]

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

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

2702 {
2703 check_context(a, b);
2704 Z3_ast r;
2705 if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
2706 Z3_ast _args[2] = { a, b };
2707 r = Z3_mk_seq_concat(a.ctx(), 2, _args);
2708 }
2709 else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
2710 Z3_ast _args[2] = { a, b };
2711 r = Z3_mk_re_concat(a.ctx(), 2, _args);
2712 }
2713 else {
2714 r = Z3_mk_concat(a.ctx(), a, b);
2715 }
2716 a.ctx().check_error();
2717 return expr(a.ctx(), r);
2718 }
Z3_is_seq_sort
bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
Z3_mk_seq_concat
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
Z3_mk_re_concat
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])
Create the concatenation of the regular languages.
Z3_mk_concat
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
Z3_is_re_sort
bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.

◆ concat [2/2]

expr concat ( expr_vector const &  args)
friend

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

2720 {
2721 Z3_ast r;
2722 assert(args.size() > 0);
2723 if (args.size() == 1) {
2724 return args[0u];
2725 }
2726 context& ctx = args[0u].ctx();
2727 array<Z3_ast> _args(args);
2728 if (Z3_is_seq_sort(ctx, args[0u].get_sort())) {
2729 r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
2730 }
2731 else if (Z3_is_re_sort(ctx, args[0u].get_sort())) {
2732 r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
2733 }
2734 else {
2735 r = _args[args.size()-1];
2736 for (unsigned i = args.size()-1; i > 0; ) {
2737 --i;
2738 r = Z3_mk_concat(ctx, _args[i], r);
2739 ctx.check_error();
2740 }
2741 }
2742 ctx.check_error();
2743 return expr(ctx, r);
2744 }

◆ distinct

expr distinct ( expr_vector const &  args)
friend

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

2693 {
2694 assert(args.size() > 0);
2695 context& ctx = args[0u].ctx();
2696 array<Z3_ast> _args(args);
2697 Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
2698 ctx.check_error();
2699 return expr(ctx, r);
2700 }
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]).

◆ fma

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

FloatingPoint fused multiply-add.

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

2256 {
2257 check_context(a, b); check_context(a, c); check_context(a, rm);
2258 assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
2259 Z3_ast r = Z3_mk_fpa_fma(a.ctx(), rm, a, b, c);
2260 a.check_error();
2261 return expr(a.ctx(), r);
2262 }
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.

◆ fp_eq

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

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

2247 {
2248 check_context(a, b);
2249 assert(a.is_fpa());
2250 Z3_ast r = Z3_mk_fpa_eq(a.ctx(), a, b);
2251 a.check_error();
2252 return expr(a.ctx(), r);
2253 }
Z3_mk_fpa_eq
Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point equality.

◆ fpa_fp

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

2264 {
2265 check_context(sgn, exp); check_context(exp, sig);
2266 assert(sgn.is_bv() && exp.is_bv() && sig.is_bv());
2267 Z3_ast r = Z3_mk_fpa_fp(sgn.ctx(), sgn, exp, sig);
2268 sgn.check_error();
2269 return expr(sgn.ctx(), r);
2270 }
Z3_mk_fpa_fp
Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig)
Create an expression of FloatingPoint sort from three bit-vector expressions.

◆ fpa_to_fpa

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

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

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

2300 {
2301 assert(t.is_fpa());
2302 Z3_ast r = Z3_mk_fpa_to_fp_float(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2303 t.check_error();
2304 return expr(t.ctx(), r);
2305 }
Z3_mk_fpa_to_fp_float
Z3_ast Z3_API Z3_mk_fpa_to_fp_float(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.

◆ fpa_to_sbv

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

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

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

2272 {
2273 assert(t.is_fpa());
2274 Z3_ast r = Z3_mk_fpa_to_sbv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
2275 t.check_error();
2276 return expr(t.ctx(), r);
2277 }
Z3_mk_fpa_to_sbv
Z3_ast Z3_API Z3_mk_fpa_to_sbv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)
Conversion of a floating-point term into a signed bit-vector.

◆ fpa_to_ubv

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

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

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

2279 {
2280 assert(t.is_fpa());
2281 Z3_ast r = Z3_mk_fpa_to_ubv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
2282 t.check_error();
2283 return expr(t.ctx(), r);
2284 }
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.

◆ implies [1/3]

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

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

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

◆ implies [2/3]

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

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

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

◆ implies [3/3]

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

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

1844 {
1845 assert(a.is_bool() && b.is_bool());
1846 _Z3_MK_BIN_(a, b, Z3_mk_implies);
1847 }
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:1837

◆ int2bv

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

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

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

◆ is_int

expr is_int ( expr const &  e)
friend

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

1892{ _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:1884

Referenced by IntNumRef::as_long(), and ArithSortRef::subsort().

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

2319 {
2320 check_context(c, t); check_context(c, e);
2321 assert(c.is_bool());
2322 Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
2323 c.check_error();
2324 return expr(c.ctx(), r);
2325 }

◆ max

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

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

2192 {
2193 check_context(a, b);
2194 Z3_ast r;
2195 if (a.is_arith()) {
2196 r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), a, b);
2197 }
2198 else if (a.is_bv()) {
2199 r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), a, b);
2200 }
2201 else {
2202 assert(a.is_fpa());
2203 r = Z3_mk_fpa_max(a.ctx(), a, b);
2204 }
2205 a.check_error();
2206 return expr(a.ctx(), r);
2207 }
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.

◆ min

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

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

2176 {
2177 check_context(a, b);
2178 Z3_ast r;
2179 if (a.is_arith()) {
2180 r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), b, a);
2181 }
2182 else if (a.is_bv()) {
2183 r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), b, a);
2184 }
2185 else {
2186 assert(a.is_fpa());
2187 r = Z3_mk_fpa_min(a.ctx(), a, b);
2188 }
2189 a.check_error();
2190 return expr(a.ctx(), r);
2191 }
Z3_mk_fpa_min
Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2)
Minimum of floating-point numbers.

◆ mk_and

expr mk_and ( expr_vector const &  args)
friend

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

2780 {
2781 array<Z3_ast> _args(args);
2782 Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2783 args.check_error();
2784 return expr(args.ctx(), r);
2785 }
Z3_mk_and
Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].

◆ mk_or

expr mk_or ( expr_vector const &  args)
friend

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

2774 {
2775 array<Z3_ast> _args(args);
2776 Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2777 args.check_error();
2778 return expr(args.ctx(), r);
2779 }
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].

◆ mk_xor

expr mk_xor ( expr_vector const &  args)
friend

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

2786 {
2787 if (args.empty())
2788 return args.ctx().bool_val(false);
2789 expr r = args[0u];
2790 for (unsigned i = 1; i < args.size(); ++i)
2791 r = r ^ args[i];
2792 return r;
2793 }
z3::ast_vector_tpl::empty
bool empty() const
Definition z3++.h:692
z3::context::bool_val
expr bool_val(bool b)
Definition z3++.h:4184

◆ mod [1/3]

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

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

1856 {
1857 if (a.is_bv()) {
1858 _Z3_MK_BIN_(a, b, Z3_mk_bvsmod);
1859 }
1860 else {
1861 _Z3_MK_BIN_(a, b, Z3_mk_mod);
1862 }
1863 }
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).

◆ mod [2/3]

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

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

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

◆ mod [3/3]

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

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

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

◆ nand

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

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

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

◆ nor

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

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

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

◆ operator!

expr operator! ( expr const &  a)
friend

Return an expression representing not(a).

Precondition
a.is_bool()

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

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

◆ operator!= [1/3]

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

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

1932 {
1933 check_context(a, b);
1934 Z3_ast args[2] = { a, b };
1935 Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1936 a.check_error();
1937 return expr(a.ctx(), r);
1938 }

◆ operator!= [2/3]

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

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

1939{ 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 1940 of file z3++.h.

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

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

◆ operator& [2/3]

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

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

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

◆ operator& [3/3]

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

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

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

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

1905{ 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 1896 of file z3++.h.

1896 {
1897 check_context(a, b);
1898 assert(a.is_bool() && b.is_bool());
1899 Z3_ast args[2] = { a, b };
1900 Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
1901 a.check_error();
1902 return expr(a.ctx(), r);
1903 }

◆ operator* [1/3]

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

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

1978 {
1979 check_context(a, b);
1980 Z3_ast r = 0;
1981 if (a.is_arith() && b.is_arith()) {
1982 Z3_ast args[2] = { a, b };
1983 r = Z3_mk_mul(a.ctx(), 2, args);
1984 }
1985 else if (a.is_finite_field() && b.is_finite_field()) {
1986 Z3_ast args[2] = { a, b };
1987 r = Z3_mk_ff_mul(a.ctx(), 2, args);
1988 }
1989 else if (a.is_bv() && b.is_bv()) {
1990 r = Z3_mk_bvmul(a.ctx(), a, b);
1991 }
1992 else if (a.is_fpa() && b.is_fpa()) {
1993 r = Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1994 }
1995 else {
1996 // operator is not supported by given arguments.
1997 assert(false);
1998 }
1999 a.check_error();
2000 return expr(a.ctx(), r);
2001 }
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.

◆ operator* [2/3]

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

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

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

◆ operator* [3/3]

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

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

2003{ 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 1944 of file z3++.h.

1944 {
1945 check_context(a, b);
1946 Z3_ast r = 0;
1947 if (a.is_arith() && b.is_arith()) {
1948 Z3_ast args[2] = { a, b };
1949 r = Z3_mk_add(a.ctx(), 2, args);
1950 }
1951 else if (a.is_finite_field() && b.is_finite_field()) {
1952 Z3_ast args[2] = { a, b };
1953 r = Z3_mk_ff_add(a.ctx(), 2, args);
1954 }
1955 else if (a.is_bv() && b.is_bv()) {
1956 r = Z3_mk_bvadd(a.ctx(), a, b);
1957 }
1958 else if (a.is_seq() && b.is_seq()) {
1959 return concat(a, b);
1960 }
1961 else if (a.is_re() && b.is_re()) {
1962 Z3_ast _args[2] = { a, b };
1963 r = Z3_mk_re_union(a.ctx(), 2, _args);
1964 }
1965 else if (a.is_fpa() && b.is_fpa()) {
1966 r = Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1967 }
1968 else {
1969 // operator is not supported by given arguments.
1970 assert(false);
1971 }
1972 a.check_error();
1973 return expr(a.ctx(), r);
1974 }
z3::expr::concat
friend expr concat(expr const &a, expr const &b)
Definition z3++.h:2702
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].

◆ operator+ [2/3]

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

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

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

◆ operator+ [3/3]

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

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

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

◆ operator- [1/4]

expr operator- ( expr const &  a)
friend

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

2048 {
2049 Z3_ast r = 0;
2050 if (a.is_arith()) {
2051 r = Z3_mk_unary_minus(a.ctx(), a);
2052 }
2053 else if (a.is_finite_field()) { r = Z3_mk_ff_neg(a.ctx(), a); }
2054 else if (a.is_bv()) {
2055 r = Z3_mk_bvneg(a.ctx(), a);
2056 }
2057 else if (a.is_fpa()) {
2058 r = Z3_mk_fpa_neg(a.ctx(), a);
2059 }
2060 else {
2061 // operator is not supported by given arguments.
2062 assert(false);
2063 }
2064 a.check_error();
2065 return expr(a.ctx(), r);
2066 }
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.

◆ operator- [2/4]

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

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

2068 {
2069 check_context(a, b);
2070 if (a.is_finite_field() && b.is_finite_field()) return a + -b;
2071 Z3_ast r = 0;
2072 if (a.is_arith() && b.is_arith()) {
2073 Z3_ast args[2] = { a, b };
2074 r = Z3_mk_sub(a.ctx(), 2, args);
2075 }
2076 else if (a.is_bv() && b.is_bv()) {
2077 r = Z3_mk_bvsub(a.ctx(), a, b);
2078 }
2079 else if (a.is_fpa() && b.is_fpa()) {
2080 r = Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
2081 }
2082 else {
2083 // operator is not supported by given arguments.
2084 assert(false);
2085 }
2086 a.check_error();
2087 return expr(a.ctx(), r);
2088 }
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 2089 of file z3++.h.

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

◆ operator- [4/4]

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

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

2090{ 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 2026 of file z3++.h.

2026 {
2027 check_context(a, b);
2028 Z3_ast r = 0;
2029 if (a.is_arith() && b.is_arith()) {
2030 r = Z3_mk_div(a.ctx(), a, b);
2031 }
2032 else if (a.is_bv() && b.is_bv()) {
2033 r = Z3_mk_bvsdiv(a.ctx(), a, b);
2034 }
2035 else if (a.is_fpa() && b.is_fpa()) {
2036 r = Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
2037 }
2038 else {
2039 // operator is not supported by given arguments.
2040 assert(false);
2041 }
2042 a.check_error();
2043 return expr(a.ctx(), r);
2044 }
Z3_mk_div
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.
Z3_mk_bvsdiv
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.
Z3_mk_fpa_div
Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point division.

◆ operator/ [2/3]

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

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

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

◆ operator/ [3/3]

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

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

2046{ 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 2117 of file z3++.h.

2117 {
2118 check_context(a, b);
2119 Z3_ast r = 0;
2120 if (a.is_arith() && b.is_arith()) {
2121 r = Z3_mk_lt(a.ctx(), a, b);
2122 }
2123 else if (a.is_bv() && b.is_bv()) {
2124 r = Z3_mk_bvslt(a.ctx(), a, b);
2125 }
2126 else if (a.is_fpa() && b.is_fpa()) {
2127 r = Z3_mk_fpa_lt(a.ctx(), a, b);
2128 }
2129 else {
2130 // operator is not supported by given arguments.
2131 assert(false);
2132 }
2133 a.check_error();
2134 return expr(a.ctx(), r);
2135 }
Z3_mk_bvslt
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than.
Z3_mk_lt
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
Z3_mk_fpa_lt
Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than.

◆ operator< [2/3]

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

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

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

◆ operator< [3/3]

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

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

2137{ 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 2092 of file z3++.h.

2092 {
2093 check_context(a, b);
2094 Z3_ast r = 0;
2095 if (a.is_arith() && b.is_arith()) {
2096 r = Z3_mk_le(a.ctx(), a, b);
2097 }
2098 else if (a.is_bv() && b.is_bv()) {
2099 r = Z3_mk_bvsle(a.ctx(), a, b);
2100 }
2101 else if (a.is_fpa() && b.is_fpa()) {
2102 r = Z3_mk_fpa_leq(a.ctx(), a, b);
2103 }
2104 else {
2105 // operator is not supported by given arguments.
2106 assert(false);
2107 }
2108 a.check_error();
2109 return expr(a.ctx(), r);
2110 }
Z3_mk_bvsle
Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than or equal to.
Z3_mk_le
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
Z3_mk_fpa_leq
Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than or equal.

◆ operator<= [2/3]

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

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

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

◆ operator<= [3/3]

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

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

2112{ 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 1921 of file z3++.h.

1921 {
1922 check_context(a, b);
1923 Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1924 a.check_error();
1925 return expr(a.ctx(), r);
1926 }
Z3_mk_eq
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.

◆ operator== [2/3]

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

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

1927{ 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 1928 of file z3++.h.

1928{ 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 2139 of file z3++.h.

2139 {
2140 check_context(a, b);
2141 Z3_ast r = 0;
2142 if (a.is_arith() && b.is_arith()) {
2143 r = Z3_mk_gt(a.ctx(), a, b);
2144 }
2145 else if (a.is_bv() && b.is_bv()) {
2146 r = Z3_mk_bvsgt(a.ctx(), a, b);
2147 }
2148 else if (a.is_fpa() && b.is_fpa()) {
2149 r = Z3_mk_fpa_gt(a.ctx(), a, b);
2150 }
2151 else {
2152 // operator is not supported by given arguments.
2153 assert(false);
2154 }
2155 a.check_error();
2156 return expr(a.ctx(), r);
2157 }
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.

◆ operator> [2/3]

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

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

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

◆ operator> [3/3]

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

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

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

2006 {
2007 check_context(a, b);
2008 Z3_ast r = 0;
2009 if (a.is_arith() && b.is_arith()) {
2010 r = Z3_mk_ge(a.ctx(), a, b);
2011 }
2012 else if (a.is_bv() && b.is_bv()) {
2013 r = Z3_mk_bvsge(a.ctx(), a, b);
2014 }
2015 else if (a.is_fpa() && b.is_fpa()) {
2016 r = Z3_mk_fpa_geq(a.ctx(), a, b);
2017 }
2018 else {
2019 // operator is not supported by given arguments.
2020 assert(false);
2021 }
2022 a.check_error();
2023 return expr(a.ctx(), r);
2024 }
Z3_mk_bvsge
Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than or equal to.
Z3_mk_fpa_geq
Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than or equal.

◆ operator>= [2/3]

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

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

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

◆ operator>= [3/3]

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

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

2115{ 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 2165 of file z3++.h.

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

◆ operator^ [2/3]

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

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

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

◆ operator^ [3/3]

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

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

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

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

◆ operator| [2/3]

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

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

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

◆ operator| [3/3]

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

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

2171{ 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 1919 of file z3++.h.

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

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

1908 {
1909 check_context(a, b);
1910 assert(a.is_bool() && b.is_bool());
1911 Z3_ast args[2] = { a, b };
1912 Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1913 a.check_error();
1914 return expr(a.ctx(), r);
1915 }

◆ operator~

expr operator~ ( expr const &  a)
friend

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

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

◆ pbeq

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

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

2660 {
2661 assert(es.size() > 0);
2662 context& ctx = es[0u].ctx();
2663 array<Z3_ast> _es(es);
2664 Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
2665 ctx.check_error();
2666 return expr(ctx, r);
2667 }
Z3_mk_pbeq
Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.

◆ pbge

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

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

2652 {
2653 assert(es.size() > 0);
2654 context& ctx = es[0u].ctx();
2655 array<Z3_ast> _es(es);
2656 Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
2657 ctx.check_error();
2658 return expr(ctx, r);
2659 }
Z3_mk_pbge
Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.

◆ pble

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

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

2644 {
2645 assert(es.size() > 0);
2646 context& ctx = es[0u].ctx();
2647 array<Z3_ast> _es(es);
2648 Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
2649 ctx.check_error();
2650 return expr(ctx, r);
2651 }
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.

◆ pw [1/3]

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

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

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

◆ pw [2/3]

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

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

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

◆ pw [3/3]

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

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

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

◆ range

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

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

4590 {
4591 check_context(lo, hi);
4592 Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
4593 lo.check_error();
4594 return expr(lo.ctx(), r);
4595 }
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.

◆ rem [1/3]

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

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

1872 {
1873 if (a.is_fpa() && b.is_fpa()) {
1874 _Z3_MK_BIN_(a, b, Z3_mk_fpa_rem);
1875 } else {
1876 _Z3_MK_BIN_(a, b, Z3_mk_rem);
1877 }
1878 }
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.

◆ rem [2/3]

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

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

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

◆ rem [3/3]

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

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

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

2307 {
2308 assert(t.is_fpa());
2309 Z3_ast r = Z3_mk_fpa_round_to_integral(t.ctx(), t.ctx().fpa_rounding_mode(), t);
2310 t.check_error();
2311 return expr(t.ctx(), r);
2312 }
Z3_mk_fpa_round_to_integral
Z3_ast Z3_API Z3_mk_fpa_round_to_integral(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point roundToIntegral. Rounds a floating-point number to the closest integer,...

◆ sbv_to_fpa

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

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

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

2286 {
2287 assert(t.is_bv());
2288 Z3_ast r = Z3_mk_fpa_to_fp_signed(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2289 t.check_error();
2290 return expr(t.ctx(), r);
2291 }
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.

◆ sqrt

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

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

2240 {
2241 check_context(a, rm);
2242 assert(a.is_fpa());
2243 Z3_ast r = Z3_mk_fpa_sqrt(a.ctx(), rm, a);
2244 a.check_error();
2245 return expr(a.ctx(), r);
2246 }
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.

◆ sum

expr sum ( expr_vector const &  args)
friend

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

2684 {
2685 assert(args.size() > 0);
2686 context& ctx = args[0u].ctx();
2687 array<Z3_ast> _args(args);
2688 Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
2689 ctx.check_error();
2690 return expr(ctx, r);
2691 }

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

2293 {
2294 assert(t.is_bv());
2295 Z3_ast r = Z3_mk_fpa_to_fp_unsigned(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2296 t.check_error();
2297 return expr(t.ctx(), r);
2298 }
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.

◆ xnor

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

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

2175{ 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.
Generated on Tue Oct 20 2026 03:25:28 for Z3 by doxygen 1.9.8