Z3 |

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:

## Public Member Functions
| expr (context &c)
| expr (context &c, Z3_ast n)
sort | get_sort () const
| Return the sort of this expression. More...
bool | is_bool () const
| Return true if this is a Boolean expression. More...
bool | is_int () const
| Return true if this is an integer expression. More...
bool | is_real () const
| Return true if this is a real expression. More...
bool | is_arith () const
| Return true if this is an integer or real expression. More...
bool | is_bv () const
| Return true if this is a Bit-vector expression. More...
bool | is_array () const
| Return true if this is a Array expression. More...
bool | is_datatype () const
| Return true if this is a Datatype expression. More...
bool | is_relation () const
| Return true if this is a Relation expression. More...
bool | is_seq () const
| Return true if this is a sequence expression. More...
bool | is_re () const
| Return true if this is a regular expression. More...
bool | is_finite_domain () const
| Return true if this is a Finite-domain expression. More...
bool | is_fpa () const
| Return true if this is a FloatingPoint expression. . More...
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. More...
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
uint64_t | as_int64 () const
bool | is_app () const
| Return true if this expression is an application. More...
bool | is_const () const
| Return true if this expression is a constant (i.e., an application with 0 arguments). More...
bool | is_quantifier () const
| Return true if this expression is a quantifier. More...
bool | is_forall () const
| Return true if this expression is a universal quantifier. More...
bool | is_exists () const
| Return true if this expression is an existential quantifier. More...
bool | is_lambda () const
| Return true if this expression is a lambda expression. More...
bool | is_var () const
| Return true if this expression is a variable. More...
bool | is_algebraic () const
| Return true if expression is an algebraic number. More...
bool | is_well_sorted () const
| Return true if this expression is well sorted (aka type correct). More...
expr | mk_is_inf () const
| Return Boolean expression to test for whether an FP expression is inf. More...
expr | mk_is_nan () const
| Return Boolean expression to test for whether an FP expression is a NaN. More...
expr | mk_is_normal () const
| Return Boolean expression to test for whether an FP expression is a normal. More...
expr | mk_is_subnormal () const
| Return Boolean expression to test for whether an FP expression is a subnormal. More...
expr | mk_is_zero () const
| Return Boolean expression to test for whether an FP expression is a zero. More...
expr | mk_to_ieee_bv () const
| Convert this fpa into an IEEE BV. More...
expr | mk_from_ieee_bv (sort const &s) const
| Convert this IEEE BV into a fpa. More...
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. More...
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) More...
unsigned | algebraic_i () const
| Return i of an algebraic number (root-obj p i) More...
unsigned | id () const
| retrieve unique identifier for expression. More...
int | get_numeral_int () const
| Return int value of numeral, throw if result cannot fit in machine int. More...
unsigned | get_numeral_uint () const
| Return uint value of numeral, throw if result cannot fit in machine uint. More...
int64_t | get_numeral_int64 () const
| Return `int64_t` value of numeral, throw if result cannot fit in `int64_t`. More...
uint64_t | get_numeral_uint64 () const
| Return `uint64_t` value of numeral, throw if result cannot fit in `uint64_t`. More...
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()` More...
std::string | get_escaped_string () const
| for a string value expression return an escaped or unescaped string value. More...
std::string | get_string () const
| operator Z3_app () const
func_decl | decl () const
| Return the declaration associated with this application. This method assumes the expression is an application. More...
unsigned | num_args () const
| Return the number of arguments in this application. This method assumes the expression is an application. More...
expr | arg (unsigned i) const
| Return the i-th argument of this application. This method assumes the expression is an application. More...
expr | body () const
| Return the 'body' of this quantifier. More...
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)
expr | rotate_right (unsigned i)
expr | repeat (unsigned i)
expr | extract (unsigned hi, unsigned lo) const
unsigned | lo () const
unsigned | hi () const
expr | extract (expr const &offset, expr const &length) const
| sequence and regular expression operations. More...
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 | stoi () const
expr | itos () const
expr | loop (unsigned lo)
| create a looping regular expression. More...
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. More...
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. More...
expr | substitute (expr_vector const &src, expr_vector const &dst)
| Apply substitution. Replace src expressions by dst. More...
expr | substitute (expr_vector const &dst)
| Apply substitution. Replace bound variables by expressions. More...
Public Member Functions inherited from ast
| ast (context &c)
| ast (context &c, Z3_ast n)
| ast (ast const &s)
| ast (ast &&s) noexcept
| ~ast ()
| operator Z3_ast () const
| operator bool () const
ast & | operator= (ast const &s)
ast & | operator= (ast &&s) noexcept
Z3_ast_kind | kind () const
unsigned | hash () const
std::string | to_string () const
Public Member Functions inherited from object
| object (context &c)
context & | ctx () const
Z3_error_code | check_error () const

## Friends
expr | operator! (expr const &a)
| Return an expression representing `not(a)`. More...
expr | operator&& (expr const &a, expr const &b)
| Return an expression representing `a and b`. More...
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. More...
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. More...
expr | operator|| (expr const &a, expr const &b)
| Return an expression representing `a or b`. More...
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. More...
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. More...
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_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)` More...
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. More...
expr | int2bv (unsigned n, expr const &a)
expr | bvadd_no_overflow (expr const &a, expr const &b, bool is_signed)
| bit-vector overflow/underflow checks More...
expr | bvadd_no_underflow (expr const &a, expr const &b)
expr | bvsub_no_overflow (expr const &a, expr const &b)
expr | bvsub_no_underflow (expr const &a, expr const &b, bool is_signed)
expr | bvsdiv_no_overflow (expr const &a, expr const &b)
expr | bvneg_no_overflow (expr const &a)
expr | bvmul_no_overflow (expr const &a, expr const &b, bool is_signed)
expr | bvmul_no_underflow (expr const &a, expr const &b)
expr | 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. More...
expr | fpa_fp (expr const &sgn, expr const &exp, expr const &sig)
| Create an expression of FloatingPoint sort from three bit-vector expressions. More...
expr | fpa_to_sbv (expr const &t, unsigned sz)
| Conversion of a floating-point term into a signed bit-vector. More...
expr | fpa_to_ubv (expr const &t, unsigned sz)
| Conversion of a floating-point term into an unsigned bit-vector. More...
expr | sbv_to_fpa (expr const &t, sort s)
| Conversion of a signed bit-vector term into a floating-point. More...
expr | ubv_to_fpa (expr const &t, sort s)
| Conversion of an unsigned bit-vector term into a floating-point. More...
expr | fpa_to_fpa (expr const &t, sort s)
| Conversion of a floating-point term into another floating-point. More...
expr | round_fpa_to_closest_integer (expr const &t)
| Round a floating-point term into its closest integer. More...
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 757 of file z3++.h.

## Constructor & Destructor Documentation

## ◆ expr() [1/2]

expr | ( | context & | c | ) |
| inline

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

759:ast(c) {}
z3::ast::ast
ast(context &c)
Definition: z3++.h:502

Referenced by expr::algebraic_lower(), expr::algebraic_upper(), expr::arg(), expr::at(), expr::body(), expr::contains(), expr::denominator(), expr::extract(), expr::itos(), expr::length(), expr::loop(), expr::mk_from_ieee_bv(), expr::mk_is_inf(), expr::mk_is_nan(), expr::mk_is_normal(), expr::mk_is_subnormal(), expr::mk_is_zero(), expr::mk_to_ieee_bv(), expr::nth(), expr::numerator(), expr::repeat(), expr::replace(), expr::rotate_left(), expr::rotate_right(), expr::simplify(), expr::stoi(), expr::substitute(), and expr::unit().

## ◆ expr() [2/2]

expr | ( | context & | c,
|  | Z3_ast | n
| ) |  |
| inline

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

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

## Member Function Documentation

## ◆ algebraic_i()

unsigned algebraic_i | ( |  | ) | const
| inline

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

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

993 {
994 assert(is_algebraic());
995 unsigned i = Z3_algebraic_get_i(ctx(), m_ast);
996 check_error();
997 return i;
998 }
z3::ast::m_ast
Z3_ast m_ast
Definition: z3++.h:500
z3::expr::is_algebraic
bool is_algebraic() const
Return true if expression is an algebraic number.
Definition: z3++.h:875
z3::object::check_error
Z3_error_code check_error() const
Definition: z3++.h:423
z3::object::ctx
context & ctx() const
Definition: z3++.h:422
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 966 of file z3++.h.

966 {
967 assert(is_algebraic());
968 Z3_ast r = Z3_get_algebraic_number_lower(ctx(), m_ast, precision);
969 check_error();
970 return expr(ctx(), r);
971 }
z3::expr::expr
expr(context &c)
Definition: z3++.h:759
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 983 of file z3++.h.

983 {
984 assert(is_algebraic());
985 Z3_ast_vector r = Z3_algebraic_get_poly(ctx(), m_ast);
986 check_error();
987 return expr_vector(ctx(), r);
988 }
z3::expr_vector
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:73
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.

## ◆ algebraic_upper()

expr algebraic_upper | ( | unsigned | precision | ) | const
| inline

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

973 {
974 assert(is_algebraic());
975 Z3_ast r = Z3_get_algebraic_number_upper(ctx(), m_ast, precision);
976 check_error();
977 return expr(ctx(), r);
978 }
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 1148 of file z3++.h.

1148{ 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__(), and ExprRef::children().

## ◆ as_binary()

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

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

835{ 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:827
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 837 of file z3++.h.

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

## ◆ as_int64()

uint64_t as_int64 | ( |  | ) | const
| inline

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

839{ 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:828

## ◆ as_uint64()

uint64_t as_uint64 | ( |  | ) | const
| inline

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

838{ 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:829

## ◆ at()

expr at | ( | expr const & | index | ) | const
| inline

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

1413 {
1414 check_context(*this, index);
1415 Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
1416 check_error();
1417 return expr(ctx(), r);
1418 }
z3::object::check_context
friend void check_context(object const &a, object const &b)
Definition: z3++.h:426
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...

## ◆ body()

expr body | ( |  | ) | const
| inline

Return the 'body' of this quantifier.

Precondition
  is_quantifier()

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

1155{ 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:853
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 1079 of file z3++.h.

1079 {
1080 return Z3_get_bool_value(ctx(), m_ast);
1081 }
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.

## ◆ contains()

expr contains | ( | expr const & | s | ) | const
| inline

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

1407 {
1408 check_context(*this, s);
1409 Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
1410 check_error();
1411 return expr(ctx(), r);
1412 }
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 1133 of file z3++.h.

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

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

1091 {
1092 assert(is_numeral());
1093 Z3_ast r = Z3_get_denominator(ctx(), m_ast);
1094 check_error();
1095 return expr(ctx(),r);
1096 }
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().

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

1392 {
1393 check_context(*this, offset); check_context(offset, length);
1394 Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r);
1395 }
z3::expr::length
expr length() const
Definition: z3++.h:1425
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 1343 of file z3++.h.

1343{ Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *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:188
z3::expr::hi
unsigned hi() const
Definition: z3++.h:1345
z3::expr::lo
unsigned lo() const
Definition: z3++.h:1344
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 958 of file z3++.h.

958 {
959 assert(is_numeral() || is_algebraic());
960 return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
961 }
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_escaped_string()

std::string get_escaped_string | ( |  | ) | const
| inline

for a string value expression return an escaped or unescaped string value.

Precondition
  expression is for a string value.

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

1110 {
1111 assert(is_string_value());
1112 char const* s = Z3_get_string(ctx(), m_ast);
1113 check_error();
1114 return std::string(s);
1115 }
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:1103
Z3_get_string
Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s)
Retrieve the string constant stored in s.

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

1015 {
1016 int result = 0;
1017 if (!is_numeral_i(result)) {
1018 assert(ctx().enable_exceptions());
1019 if (!ctx().enable_exceptions()) return 0;
1020 Z3_THROW(exception("numeral does not fit in machine int"));
1021 }
1022 return result;
1023 }
z3::expr::is_numeral_i
bool is_numeral_i(int &i) const
Definition: z3++.h:830
Z3_THROW
#define Z3_THROW(x)
Definition: z3++.h:100

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

1051 {
1052 assert(is_numeral());
1053 int64_t result = 0;
1054 if (!is_numeral_i64(result)) {
1055 assert(ctx().enable_exceptions());
1056 if (!ctx().enable_exceptions()) return 0;
1057 Z3_THROW(exception("numeral does not fit in machine int64_t"));
1058 }
1059 return result;
1060 }

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

1034 {
1035 assert(is_numeral());
1036 unsigned result = 0;
1037 if (!is_numeral_u(result)) {
1038 assert(ctx().enable_exceptions());
1039 if (!ctx().enable_exceptions()) return 0;
1040 Z3_THROW(exception("numeral does not fit in machine uint"));
1041 }
1042 return result;
1043 }
z3::expr::is_numeral_u
bool is_numeral_u(unsigned &i) const
Definition: z3++.h:831

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

1068 {
1069 assert(is_numeral());
1070 uint64_t result = 0;
1071 if (!is_numeral_u64(result)) {
1072 assert(ctx().enable_exceptions());
1073 if (!ctx().enable_exceptions()) return 0;
1074 Z3_THROW(exception("numeral does not fit in machine uint64_t"));
1075 }
1076 return result;
1077 }

## ◆ get_sort()

sort get_sort | ( |  | ) | const
| inline

Return the sort of this expression.

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

765{ 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:419
Z3_get_sort
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.

Referenced by z3::ashr(), expr::is_arith(), expr::is_array(), expr::is_bool(), expr::is_bv(), expr::is_datatype(), expr::is_finite_domain(), expr::is_fpa(), expr::is_int(), expr::is_re(), expr::is_real(), expr::is_relation(), expr::is_seq(), z3::lshr(), z3::select(), z3::sge(), z3::sgt(), z3::shl(), z3::sle(), z3::slt(), z3::smod(), ModelRef::sorts(), z3::srem(), z3::store(), z3::udiv(), z3::uge(), z3::ugt(), z3::ule(), z3::ult(), and z3::urem().

## ◆ get_string()

std::string get_string | ( |  | ) | const
| inline

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

1117 {
1118 assert(is_string_value());
1119 unsigned n;
1120 char const* s = Z3_get_lstring(ctx(), m_ast, &n);
1121 check_error();
1122 return std::string(s, n);
1123 }
Z3_get_lstring
Z3_char_ptr Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned *length)
Retrieve the unescaped string constant stored in s.

## ◆ hi()

unsigned hi | ( |  | ) | const
| inline

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

1345{ 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::is_app
bool is_app() const
Return true if this expression is an application.
Definition: z3++.h:845
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:1133
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 1003 of file z3++.h.

1003{ 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 875 of file z3++.h.

875{ 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 1223 of file z3++.h.

1223{ return is_app() && Z3_OP_AND == decl().decl_kind(); }
z3::func_decl::decl_kind
Z3_decl_kind decl_kind() const
Definition: z3++.h:726
Z3_OP_AND
@ Z3_OP_AND
Definition: z3_api.h:1007

## ◆ is_app()

bool is_app | ( |  | ) | const
| inline

Return true if this expression is an application.

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

845{ return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }
z3::ast::kind
Z3_ast_kind kind() const
Definition: z3++.h:525
Z3_APP_AST
@ Z3_APP_AST
Definition: z3_api.h:182
Z3_NUMERAL_AST
@ Z3_NUMERAL_AST
Definition: z3_api.h:181

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

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

## ◆ is_array()

bool is_array | ( |  | ) | const
| inline

Return true if this is a Array expression.

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

790{ 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:655

Referenced by expr::operator[]().

## ◆ is_bool()

bool is_bool | ( |  | ) | const
| inline

Return true if this is a Boolean expression.

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

770{ 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:635

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

## ◆ is_bv()

bool is_bv | ( |  | ) | const
| inline

Return true if this is a Bit-vector expression.

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

786{ 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:651

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

849{ return is_app() && num_args() == 0; }
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:1140

Referenced by solver::add().

## ◆ is_datatype()

bool is_datatype | ( |  | ) | const
| inline

Return true if this is a Datatype expression.

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

794{ 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:659

## ◆ is_distinct()

bool is_distinct | ( |  | ) | const
| inline

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

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

## ◆ is_eq()

bool is_eq | ( |  | ) | const
| inline

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

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

## ◆ is_exists()

bool is_exists | ( |  | ) | const
| inline

Return true if this expression is an existential quantifier.

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

862{ 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 1221 of file z3++.h.

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

## ◆ is_finite_domain()

bool is_finite_domain | ( |  | ) | 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 816 of file z3++.h.

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

## ◆ is_forall()

bool is_forall | ( |  | ) | const
| inline

Return true if this expression is a universal quantifier.

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

858{ 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 820 of file z3++.h.

820{ 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:679

Referenced by expr::mk_is_inf(), expr::mk_is_nan(), expr::mk_is_normal(), expr::mk_is_subnormal(), expr::mk_is_zero(), expr::mk_to_ieee_bv(), z3::operator!=(), and z3::operator==().

## ◆ is_implies()

bool is_implies | ( |  | ) | const
| inline

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

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

## ◆ is_int()

bool is_int | ( |  | ) | const
| inline

Return true if this is an integer expression.

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

774{ 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:639

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

## ◆ is_ite()

bool is_ite | ( |  | ) | const
| inline

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

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

## ◆ is_lambda()

bool is_lambda | ( |  | ) | const
| inline

Return true if this expression is a lambda expression.

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

866{ 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 1222 of file z3++.h.

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

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

827{ 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 834 of file z3++.h.

834{ 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 832 of file z3++.h.

832{ 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 833 of file z3++.h.

833{ 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 830 of file z3++.h.

830{ 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 828 of file z3++.h.

828{ 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 831 of file z3++.h.

831{ 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 829 of file z3++.h.

829{ 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 1224 of file z3++.h.

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

## ◆ is_quantifier()

bool is_quantifier | ( |  | ) | const
| inline

Return true if this expression is a quantifier.

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

853{ return kind() == Z3_QUANTIFIER_AST; }
Z3_QUANTIFIER_AST
@ Z3_QUANTIFIER_AST
Definition: z3_api.h:184

Referenced by expr::body().

## ◆ is_re()

bool is_re | ( |  | ) | const
| inline

Return true if this is a regular expression.

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

806{ 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:671

## ◆ is_real()

bool is_real | ( |  | ) | const
| inline

Return true if this is a real expression.

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

778{ 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:643

## ◆ is_relation()

bool is_relation | ( |  | ) | const
| inline

Return true if this is a Relation expression.

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

798{ 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:663

## ◆ is_seq()

bool is_seq | ( |  | ) | const
| inline

Return true if this is a sequence expression.

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

802{ 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:667

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

1103{ 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 SeqRef::as_string(), expr::get_escaped_string(), and expr::get_string().

## ◆ is_true()

bool is_true | ( |  | ) | const
| inline

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

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

## ◆ is_var()

bool is_var | ( |  | ) | const
| inline

Return true if this expression is a variable.

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

871{ return kind() == Z3_VAR_AST; }
Z3_VAR_AST
@ Z3_VAR_AST
Definition: z3_api.h:183

## ◆ is_well_sorted()

bool is_well_sorted | ( |  | ) | const
| inline

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

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

880{ 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 1225 of file z3++.h.

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

## ◆ itos()

expr itos | ( |  | ) | const
| inline

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

1435 {
1436 Z3_ast r = Z3_mk_int_to_str(ctx(), *this);
1437 check_error();
1438 return expr(ctx(), r);
1439 }
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 1425 of file z3++.h.

1425 {
1426 Z3_ast r = Z3_mk_seq_length(ctx(), *this);
1427 check_error();
1428 return expr(ctx(), r);
1429 }
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 1344 of file z3++.h.

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

## ◆ loop() [1/2]

expr loop | ( | unsigned | lo | ) |
| inline

create a looping regular expression.

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

1445 {
1446 Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, 0);
1447 check_error();
1448 return expr(ctx(), r);
1449 }
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 1450 of file z3++.h.

1450 {
1451 Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, hi);
1452 check_error();
1453 return expr(ctx(), r);
1454 }

## ◆ mk_from_ieee_bv()

expr mk_from_ieee_bv | ( | sort const & | s | ) | const
| inline

Convert this IEEE BV into a fpa.

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

945 {
946 assert(is_bv());
947 Z3_ast r = Z3_mk_fpa_to_fp_bv(ctx(), m_ast, s);
948 check_error();
949 return expr(ctx(), r);
950 }
z3::expr::is_bv
bool is_bv() const
Return true if this is a Bit-vector expression.
Definition: z3++.h:786
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 885 of file z3++.h.

885 {
886 assert(is_fpa());
887 Z3_ast r = Z3_mk_fpa_is_infinite(ctx(), m_ast);
888 check_error();
889 return expr(ctx(), r);
890 }
z3::expr::is_fpa
bool is_fpa() const
Return true if this is a FloatingPoint expression. .
Definition: z3++.h:820
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 895 of file z3++.h.

895 {
896 assert(is_fpa());
897 Z3_ast r = Z3_mk_fpa_is_nan(ctx(), m_ast);
898 check_error();
899 return expr(ctx(), r);
900 }
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 905 of file z3++.h.

905 {
906 assert(is_fpa());
907 Z3_ast r = Z3_mk_fpa_is_normal(ctx(), m_ast);
908 check_error();
909 return expr(ctx(), r);
910 }
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 915 of file z3++.h.

915 {
916 assert(is_fpa());
917 Z3_ast r = Z3_mk_fpa_is_subnormal(ctx(), m_ast);
918 check_error();
919 return expr(ctx(), r);
920 }
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 925 of file z3++.h.

925 {
926 assert(is_fpa());
927 Z3_ast r = Z3_mk_fpa_is_zero(ctx(), m_ast);
928 check_error();
929 return expr(ctx(), r);
930 }
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 935 of file z3++.h.

935 {
936 assert(is_fpa());
937 Z3_ast r = Z3_mk_fpa_to_ieee_bv(ctx(), m_ast);
938 check_error();
939 return expr(ctx(), r);
940 }
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 1419 of file z3++.h.

1419 {
1420 check_context(*this, index);
1421 Z3_ast r = Z3_mk_seq_nth(ctx(), *this, index);
1422 check_error();
1423 return expr(ctx(), r);
1424 }
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 1140 of file z3++.h.

1140{ 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(), FuncEntry::as_list(), ExprRef::children(), and expr::is_const().

## ◆ numerator()

expr numerator | ( |  | ) | const
| inline

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

1083 {
1084 assert(is_numeral());
1085 Z3_ast r = Z3_get_numerator(ctx(), m_ast);
1086 check_error();
1087 return expr(ctx(),r);
1088 }
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 1125 of file z3++.h.

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

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

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

index operator defined on arrays and sequences.

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

1459 {
1460 assert(is_array() || is_seq());
1461 if (is_array()) {
1462 return select(*this, index);
1463 }
1464 return nth(index);
1465 }
z3::expr::is_array
bool is_array() const
Return true if this is a Array expression.
Definition: z3++.h:790
z3::expr::nth
expr nth(expr const &index) const
Definition: z3++.h:1419
z3::expr::is_seq
bool is_seq() const
Return true if this is a sequence expression.
Definition: z3++.h:802
z3::select
expr select(expr const &a, expr const &i)
forward declarations
Definition: z3++.h:3550

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

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

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

1467 {
1468 return select(*this, index);
1469 }

## ◆ repeat()

expr repeat | ( | unsigned | i | ) |
| inline

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

1333{ 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 1396 of file z3++.h.

1396 {
1397 check_context(*this, src); check_context(src, dst);
1398 Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
1399 check_error();
1400 return expr(ctx(), r);
1401 }
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 | ) |
| inline

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

1331{ 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 | ) |
| inline

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

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

## ◆ simplify() [1/2]

expr simplify | ( |  | ) | const
| inline

Return a simplified version of this expression.

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

1474{ 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 1478 of file z3++.h.

1478{ 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 1430 of file z3++.h.

1430 {
1431 Z3_ast r = Z3_mk_str_to_int(ctx(), *this);
1432 check_error();
1433 return expr(ctx(), r);
1434 }
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/2]

expr substitute | ( | expr_vector const & | dst | ) |
| inline

Apply substitution. Replace bound variables by expressions.

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

3795 {
3796 array<Z3_ast> _dst(dst.size());
3797 for (unsigned i = 0; i < dst.size(); ++i) {
3798 _dst[i] = dst[i];
3799 }
3800 Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
3801 check_error();
3802 return expr(ctx(), r);
3803 }
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 free variables in a with the expressions in to. For every i smaller than num_exprs,...

## ◆ substitute() [2/2]

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

Apply substitution. Replace src expressions by dst.

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

3782 {
3783 assert(src.size() == dst.size());
3784 array<Z3_ast> _src(src.size());
3785 array<Z3_ast> _dst(dst.size());
3786 for (unsigned i = 0; i < src.size(); ++i) {
3787 _src[i] = src[i];
3788 _dst[i] = dst[i];
3789 }
3790 Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
3791 check_error();
3792 return expr(ctx(), r);
3793 }
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....

## ◆ unit()

expr unit | ( |  | ) | const
| inline

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

1402 {
1403 Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
1404 check_error();
1405 return expr(ctx(), r);
1406 }
Z3_mk_seq_unit
Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a)
Create a unit sequence of a.

## Friends And Related Function Documentation

## ◆ abs

expr abs | ( | expr const & | a | ) |
| friend

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

1863 {
1864 Z3_ast r;
1865 if (a.is_int()) {
1866 expr zero = a.ctx().int_val(0);
1867 r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
1868 }
1869 else if (a.is_real()) {
1870 expr zero = a.ctx().real_val(0);
1871 r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
1872 }
1873 else {
1874 r = Z3_mk_fpa_abs(a.ctx(), a);
1875 }
1876 a.check_error();
1877 return expr(a.ctx(), r);
1878 }
Z3_mk_ge
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
Z3_mk_ite
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
Z3_mk_fpa_abs
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.

## ◆ atleast

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

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

2294 {
2295 assert(es.size() > 0);
2296 context& ctx = es[0].ctx();
2297 array<Z3_ast> _es(es);
2298 Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
2299 ctx.check_error();
2300 return expr(ctx, r);
2301 }
Z3_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 2286 of file z3++.h.

2286 {
2287 assert(es.size() > 0);
2288 context& ctx = es[0].ctx();
2289 array<Z3_ast> _es(es);
2290 Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
2291 ctx.check_error();
2292 return expr(ctx, r);
2293 }
Z3_mk_atmost
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.

## ◆ bv2int

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

bit-vector and integer conversions.

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

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

## ◆ bvadd_no_overflow

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

bit-vector overflow/underflow checks

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

2103 {
2104 check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_overflow(a.ctx(), a, b, is_signed); a.check_error(); return expr(a.ctx(), r);
2105 }
Z3_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 2106 of file z3++.h.

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

## ◆ bvmul_no_overflow

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

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

2121 {
2122 check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_overflow(a.ctx(), a, b, is_signed); a.check_error(); return expr(a.ctx(), r);
2123 }
Z3_mk_bvmul_no_overflow
Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.

## ◆ bvmul_no_underflow

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

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

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

## ◆ bvneg_no_overflow

expr bvneg_no_overflow | ( | expr const & | a | ) |
| friend

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

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

## ◆ bvredand

expr bvredand | ( | expr const & | a | ) |
| friend

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

1857 {
1858 assert(a.is_bv());
1859 Z3_ast r = Z3_mk_bvredor(a.ctx(), a);
1860 a.check_error();
1861 return expr(a.ctx(), r);
1862 }
Z3_mk_bvredor
Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1)
Take disjunction of bits in vector, return vector of length 1.

## ◆ bvredor

expr bvredor | ( | expr const & | a | ) |
| friend

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

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

## ◆ bvsdiv_no_overflow

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

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

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

## ◆ bvsub_no_overflow

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

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

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

## ◆ bvsub_no_underflow

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

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

2112 {
2113 check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_underflow(a.ctx(), a, b, is_signed); a.check_error(); return expr(a.ctx(), r);
2114 }
Z3_mk_bvsub_no_underflow
Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.

## ◆ concat [1/2]

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

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

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

## ◆ concat [2/2]

expr concat | ( | expr_vector const & | args | ) |
| friend

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

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

## ◆ distinct

expr distinct | ( | expr_vector const & | args | ) |
| friend

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

2311 {
2312 assert(args.size() > 0);
2313 context& ctx = args[0].ctx();
2314 array<Z3_ast> _args(args);
2315 Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
2316 ctx.check_error();
2317 return expr(ctx, r);
2318 }
Z3_mk_distinct
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).

## ◆ fma

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

FloatingPoint fused multiply-add.

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

1895 {
1896 check_context(a, b); check_context(a, c); check_context(a, rm);
1897 assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
1898 Z3_ast r = Z3_mk_fpa_fma(a.ctx(), rm, a, b, c);
1899 a.check_error();
1900 return expr(a.ctx(), r);
1901 }
Z3_mk_fpa_fma
Z3_ast Z3_API Z3_mk_fpa_fma(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Floating-point fused multiply-add.

## ◆ fp_eq

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

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

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

## ◆ fpa_fp

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

1903 {
1904 check_context(sgn, exp); check_context(exp, sig);
1905 assert(sgn.is_bv() && exp.is_bv() && sig.is_bv());
1906 Z3_ast r = Z3_mk_fpa_fp(sgn.ctx(), sgn, exp, sig);
1907 sgn.check_error();
1908 return expr(sgn.ctx(), r);
1909 }
Z3_mk_fpa_fp
Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig)
Create an expression of FloatingPoint sort from three bit-vector expressions.

## ◆ fpa_to_fpa

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

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

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

1939 {
1940 assert(t.is_fpa());
1941 Z3_ast r = Z3_mk_fpa_to_fp_float(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
1942 t.check_error();
1943 return expr(t.ctx(), r);
1944 }
Z3_mk_fpa_to_fp_float
Z3_ast Z3_API Z3_mk_fpa_to_fp_float(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.

## ◆ fpa_to_sbv

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

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

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

1911 {
1912 assert(t.is_fpa());
1913 Z3_ast r = Z3_mk_fpa_to_sbv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
1914 t.check_error();
1915 return expr(t.ctx(), r);
1916 }
Z3_mk_fpa_to_sbv
Z3_ast Z3_API Z3_mk_fpa_to_sbv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)
Conversion of a floating-point term into a signed bit-vector.

## ◆ fpa_to_ubv

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

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

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

1918 {
1919 assert(t.is_fpa());
1920 Z3_ast r = Z3_mk_fpa_to_ubv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
1921 t.check_error();
1922 return expr(t.ctx(), r);
1923 }
Z3_mk_fpa_to_ubv
Z3_ast Z3_API Z3_mk_fpa_to_ubv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)
Conversion of a floating-point term into an unsigned bit-vector.

## ◆ implies [1/3]

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

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

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

## ◆ implies [2/3]

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

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

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

## ◆ implies [3/3]

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

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

1499 {
1500 assert(a.is_bool() && b.is_bool());
1501 _Z3_MK_BIN_(a, b, Z3_mk_implies);
1502 }
_Z3_MK_BIN_
#define _Z3_MK_BIN_(a, b, binop)
Definition: z3++.h:1492
Z3_mk_implies
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.

## ◆ int2bv

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

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

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

## ◆ is_int

expr is_int | ( | expr const & | e | ) |
| friend

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

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

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

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

## ◆ max

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

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

1836 {
1837 check_context(a, b);
1838 Z3_ast r;
1839 if (a.is_arith()) {
1840 r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), a, b);
1841 }
1842 else if (a.is_bv()) {
1843 r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), a, b);
1844 }
1845 else {
1846 assert(a.is_fpa());
1847 r = Z3_mk_fpa_max(a.ctx(), a, b);
1848 }
1849 return expr(a.ctx(), r);
1850 }
Z3_mk_bvuge
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
Z3_mk_fpa_max
Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2)
Maximum of floating-point numbers.

## ◆ min

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

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

1821 {
1822 check_context(a, b);
1823 Z3_ast r;
1824 if (a.is_arith()) {
1825 r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), b, a);
1826 }
1827 else if (a.is_bv()) {
1828 r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), b, a);
1829 }
1830 else {
1831 assert(a.is_fpa());
1832 r = Z3_mk_fpa_min(a.ctx(), a, b);
1833 }
1834 return expr(a.ctx(), r);
1835 }
Z3_mk_fpa_min
Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2)
Minimum of floating-point numbers.

## ◆ mk_and

expr mk_and | ( | expr_vector const & | args | ) |
| friend

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

2370 {
2371 array<Z3_ast> _args(args);
2372 Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2373 args.check_error();
2374 return expr(args.ctx(), r);
2375 }
Z3_mk_and
Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].

## ◆ mk_or

expr mk_or | ( | expr_vector const & | args | ) |
| friend

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

2364 {
2365 array<Z3_ast> _args(args);
2366 Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2367 args.check_error();
2368 return expr(args.ctx(), r);
2369 }
Z3_mk_or
Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] or ... or args[num_args-1].

## ◆ mod [1/3]

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

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

1511 {
1512 if (a.is_bv()) {
1513 _Z3_MK_BIN_(a, b, Z3_mk_bvsmod);
1514 }
1515 else {
1516 _Z3_MK_BIN_(a, b, Z3_mk_mod);
1517 }
1518 }
Z3_mk_mod
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.
Z3_mk_bvsmod
Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows divisor).

## ◆ mod [2/3]

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

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

1519{ 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:1511

## ◆ mod [3/3]

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

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

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

## ◆ nand

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

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

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

## ◆ nor

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

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

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

## ◆ operator!

expr operator! | ( | expr const & | a | ) |
| friend

Return an expression representing `not(a)`.

Precondition
  a.is_bool()

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

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

## ◆ operator!= [1/3]

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

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

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

## ◆ operator!= [2/3]

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

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

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

## ◆ operator!= [3/3]

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

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

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

## ◆ operator& [1/3]

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

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

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

## ◆ operator& [2/3]

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

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

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

## ◆ operator& [3/3]

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

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

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

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

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

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

## ◆ operator* [1/3]

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

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

1629 {
1630 check_context(a, b);
1631 Z3_ast r = 0;
1632 if (a.is_arith() && b.is_arith()) {
1633 Z3_ast args[2] = { a, b };
1634 r = Z3_mk_mul(a.ctx(), 2, args);
1635 }
1636 else if (a.is_bv() && b.is_bv()) {
1637 r = Z3_mk_bvmul(a.ctx(), a, b);
1638 }
1639 else if (a.is_fpa() && b.is_fpa()) {
1640 r = Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1641 }
1642 else {
1643 // operator is not supported by given arguments.
1644 assert(false);
1645 }
1646 a.check_error();
1647 return expr(a.ctx(), r);
1648 }
Z3_mk_mul
Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] * ... * args[num_args-1].
Z3_mk_bvmul
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
Z3_mk_fpa_mul
Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point multiplication.

## ◆ operator* [2/3]

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

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

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

## ◆ operator* [3/3]

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

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

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

1599 {
1600 check_context(a, b);
1601 Z3_ast r = 0;
1602 if (a.is_arith() && b.is_arith()) {
1603 Z3_ast args[2] = { a, b };
1604 r = Z3_mk_add(a.ctx(), 2, args);
1605 }
1606 else if (a.is_bv() && b.is_bv()) {
1607 r = Z3_mk_bvadd(a.ctx(), a, b);
1608 }
1609 else if (a.is_seq() && b.is_seq()) {
1610 return concat(a, b);
1611 }
1612 else if (a.is_re() && b.is_re()) {
1613 Z3_ast _args[2] = { a, b };
1614 r = Z3_mk_re_union(a.ctx(), 2, _args);
1615 }
1616 else if (a.is_fpa() && b.is_fpa()) {
1617 r = Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1618 }
1619 else {
1620 // operator is not supported by given arguments.
1621 assert(false);
1622 }
1623 a.check_error();
1624 return expr(a.ctx(), r);
1625 }
z3::expr::concat
friend expr concat(expr const &a, expr const &b)
Definition: z3++.h:2320
Z3_mk_re_union
Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[])
Create the union of the regular languages.
Z3_mk_bvadd
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement addition.
Z3_mk_add
Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] + ... + args[num_args-1].
Z3_mk_fpa_add
Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point addition.

## ◆ operator+ [2/3]

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

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

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

## ◆ operator+ [3/3]

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

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

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

## ◆ operator- [1/4]

expr operator- | ( | expr const & | a | ) |
| friend

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

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

## ◆ operator- [2/4]

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

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

1714 {
1715 check_context(a, b);
1716 Z3_ast r = 0;
1717 if (a.is_arith() && b.is_arith()) {
1718 Z3_ast args[2] = { a, b };
1719 r = Z3_mk_sub(a.ctx(), 2, args);
1720 }
1721 else if (a.is_bv() && b.is_bv()) {
1722 r = Z3_mk_bvsub(a.ctx(), a, b);
1723 }
1724 else if (a.is_fpa() && b.is_fpa()) {
1725 r = Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1726 }
1727 else {
1728 // operator is not supported by given arguments.
1729 assert(false);
1730 }
1731 a.check_error();
1732 return expr(a.ctx(), r);
1733 }
Z3_mk_bvsub
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
Z3_mk_sub
Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] - ... - args[num_args - 1].
Z3_mk_fpa_sub
Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point subtraction.

## ◆ operator- [3/4]

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

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

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

## ◆ operator- [4/4]

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

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

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

1673 {
1674 check_context(a, b);
1675 Z3_ast r = 0;
1676 if (a.is_arith() && b.is_arith()) {
1677 r = Z3_mk_div(a.ctx(), a, b);
1678 }
1679 else if (a.is_bv() && b.is_bv()) {
1680 r = Z3_mk_bvsdiv(a.ctx(), a, b);
1681 }
1682 else if (a.is_fpa() && b.is_fpa()) {
1683 r = Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1684 }
1685 else {
1686 // operator is not supported by given arguments.
1687 assert(false);
1688 }
1689 a.check_error();
1690 return expr(a.ctx(), r);
1691 }
Z3_mk_div
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.
Z3_mk_bvsdiv
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.
Z3_mk_fpa_div
Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point division.

## ◆ operator/ [2/3]

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

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

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

## ◆ operator/ [3/3]

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

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

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

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

## ◆ operator< [2/3]

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

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

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

## ◆ operator< [3/3]

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

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

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

1737 {
1738 check_context(a, b);
1739 Z3_ast r = 0;
1740 if (a.is_arith() && b.is_arith()) {
1741 r = Z3_mk_le(a.ctx(), a, b);
1742 }
1743 else if (a.is_bv() && b.is_bv()) {
1744 r = Z3_mk_bvsle(a.ctx(), a, b);
1745 }
1746 else if (a.is_fpa() && b.is_fpa()) {
1747 r = Z3_mk_fpa_leq(a.ctx(), a, b);
1748 }
1749 else {
1750 // operator is not supported by given arguments.
1751 assert(false);
1752 }
1753 a.check_error();
1754 return expr(a.ctx(), r);
1755 }
Z3_mk_bvsle
Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than or equal to.
Z3_mk_le
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
Z3_mk_fpa_leq
Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than or equal.

## ◆ operator<= [2/3]

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

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

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

## ◆ operator<= [3/3]

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

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

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

1576 {
1577 check_context(a, b);
1578 Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1579 a.check_error();
1580 return expr(a.ctx(), r);
1581 }
Z3_mk_eq
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.

## ◆ operator== [2/3]

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

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

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

## ◆ operator== [3/3]

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

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

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

## ◆ operator> [1/3]

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

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

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

## ◆ operator> [2/3]

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

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

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

## ◆ operator> [3/3]

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

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

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

1653 {
1654 check_context(a, b);
1655 Z3_ast r = 0;
1656 if (a.is_arith() && b.is_arith()) {
1657 r = Z3_mk_ge(a.ctx(), a, b);
1658 }
1659 else if (a.is_bv() && b.is_bv()) {
1660 r = Z3_mk_bvsge(a.ctx(), a, b);
1661 }
1662 else if (a.is_fpa() && b.is_fpa()) {
1663 r = Z3_mk_fpa_geq(a.ctx(), a, b);
1664 }
1665 else {
1666 // operator is not supported by given arguments.
1667 assert(false);
1668 }
1669 a.check_error();
1670 return expr(a.ctx(), r);
1671 }
Z3_mk_bvsge
Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than or equal to.
Z3_mk_fpa_geq
Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than or equal.

## ◆ operator>= [2/3]

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

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

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

## ◆ operator>= [3/3]

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

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

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

1810{ check_context(a, b); Z3_ast r = a.is_bool() ? Z3_mk_xor(a.ctx(), a, b) : Z3_mk_bvxor(a.ctx(), a, b); return expr(a.ctx(), r); }
Z3_mk_bvxor
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
Z3_mk_xor
Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 xor t2.

## ◆ operator^ [2/3]

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

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

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

## ◆ operator^ [3/3]

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

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

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

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

## ◆ operator| [2/3]

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

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

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

## ◆ operator| [3/3]

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

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

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

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

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

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

## ◆ operator~

expr operator~ | ( | expr const & | a | ) |
| friend

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

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

## ◆ pbeq

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

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

2278 {
2279 assert(es.size() > 0);
2280 context& ctx = es[0].ctx();
2281 array<Z3_ast> _es(es);
2282 Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
2283 ctx.check_error();
2284 return expr(ctx, r);
2285 }
Z3_mk_pbeq
Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.

## ◆ pbge

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

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

2270 {
2271 assert(es.size() > 0);
2272 context& ctx = es[0].ctx();
2273 array<Z3_ast> _es(es);
2274 Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
2275 ctx.check_error();
2276 return expr(ctx, r);
2277 }
Z3_mk_pbge
Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.

## ◆ pble

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

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

2262 {
2263 assert(es.size() > 0);
2264 context& ctx = es[0].ctx();
2265 array<Z3_ast> _es(es);
2266 Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
2267 ctx.check_error();
2268 return expr(ctx, r);
2269 }
Z3_mk_pble
Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.

## ◆ pw [1/3]

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

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

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

## ◆ pw [2/3]

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

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

1508{ 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:1507

## ◆ pw [3/3]

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

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

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

## ◆ range

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

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

3725 {
3726 check_context(lo, hi);
3727 Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
3728 lo.check_error();
3729 return expr(lo.ctx(), r);
3730 }
Z3_mk_re_range
Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi)
Create the range regular expression over two sequences of length 1.

## ◆ rem [1/3]

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

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

1527 {
1528 if (a.is_fpa() && b.is_fpa()) {
1529 _Z3_MK_BIN_(a, b, Z3_mk_fpa_rem);
1530 } else {
1531 _Z3_MK_BIN_(a, b, Z3_mk_rem);
1532 }
1533 }
Z3_mk_rem
Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 rem arg2.
Z3_mk_fpa_rem
Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point remainder.

## ◆ rem [2/3]

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

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

1534{ 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:1527

## ◆ rem [3/3]

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

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

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

1946 {
1947 assert(t.is_fpa());
1948 Z3_ast r = Z3_mk_fpa_round_to_integral(t.ctx(), t.ctx().fpa_rounding_mode(), t);
1949 t.check_error();
1950 return expr(t.ctx(), r);
1951 }
Z3_mk_fpa_round_to_integral
Z3_ast Z3_API Z3_mk_fpa_round_to_integral(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point roundToIntegral. Rounds a floating-point number to the closest integer,...

## ◆ sbv_to_fpa

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

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

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

1925 {
1926 assert(t.is_bv());
1927 Z3_ast r = Z3_mk_fpa_to_fp_signed(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
1928 t.check_error();
1929 return expr(t.ctx(), r);
1930 }
Z3_mk_fpa_to_fp_signed
Z3_ast Z3_API Z3_mk_fpa_to_fp_signed(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.

## ◆ sqrt

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

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

1879 {
1880 check_context(a, rm);
1881 assert(a.is_fpa());
1882 Z3_ast r = Z3_mk_fpa_sqrt(a.ctx(), rm, a);
1883 a.check_error();
1884 return expr(a.ctx(), r);
1885 }
Z3_mk_fpa_sqrt
Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point square root.

## ◆ sum

expr sum | ( | expr_vector const & | args | ) |
| friend

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

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

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

1932 {
1933 assert(t.is_bv());
1934 Z3_ast r = Z3_mk_fpa_to_fp_unsigned(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
1935 t.check_error();
1936 return expr(t.ctx(), r);
1937 }
Z3_mk_fpa_to_fp_unsigned
Z3_ast Z3_API Z3_mk_fpa_to_fp_unsigned(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort.

## ◆ xnor

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

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

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