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

A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort Boolean. Every expression has a sort. More...

#include <z3++.h>

Inheritance diagram for expr:

Data Structures

class  iterator

Public Member Functions

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

Friends

expr operator! (expr const &a)
 Return an expression representing not(a).
expr operator&& (expr const &a, expr const &b)
 Return an expression representing a and b.
expr operator&& (expr const &a, bool b)
 Return an expression representing a and b. The C++ Boolean value b is automatically converted into a Z3 Boolean constant.
expr operator&& (bool a, expr const &b)
 Return an expression representing a and b. The C++ Boolean value a is automatically converted into a Z3 Boolean constant.
expr operator|| (expr const &a, expr const &b)
 Return an expression representing a or b.
expr operator|| (expr const &a, bool b)
 Return an expression representing a or b. The C++ Boolean value b is automatically converted into a Z3 Boolean constant.
expr operator|| (bool a, expr const &b)
 Return an expression representing a or b. The C++ Boolean value a is automatically converted into a Z3 Boolean constant.
expr implies (expr const &a, expr const &b)
expr implies (expr const &a, bool b)
expr implies (bool a, expr const &b)
expr mk_or (expr_vector const &args)
expr mk_xor (expr_vector const &args)
expr mk_and (expr_vector const &args)
expr ite (expr const &c, expr const &t, expr const &e)
 Create the if-then-else expression ite(c, t, e).
expr distinct (expr_vector const &args)
expr concat (expr const &a, expr const &b)
expr concat (expr_vector const &args)
expr operator== (expr const &a, expr const &b)
expr operator== (expr const &a, int b)
expr operator== (int a, expr const &b)
expr operator!= (expr const &a, expr const &b)
expr operator!= (expr const &a, int b)
expr operator!= (int a, expr const &b)
expr operator+ (expr const &a, expr const &b)
expr operator+ (expr const &a, int b)
expr operator+ (int a, expr const &b)
expr sum (expr_vector const &args)
expr operator* (expr const &a, expr const &b)
expr operator* (expr const &a, int b)
expr operator* (int a, expr const &b)
expr pw (expr const &a, expr const &b)
expr pw (expr const &a, int b)
expr pw (int a, expr const &b)
expr mod (expr const &a, expr const &b)
expr mod (expr const &a, int b)
expr mod (int a, expr const &b)
expr rem (expr const &a, expr const &b)
expr rem (expr const &a, int b)
expr rem (int a, expr const &b)
expr is_int (expr const &e)
expr operator/ (expr const &a, expr const &b)
expr operator/ (expr const &a, int b)
expr operator/ (int a, expr const &b)
expr operator- (expr const &a)
expr operator- (expr const &a, expr const &b)
expr operator- (expr const &a, int b)
expr operator- (int a, expr const &b)
expr operator<= (expr const &a, expr const &b)
expr operator<= (expr const &a, int b)
expr operator<= (int a, expr const &b)
expr operator>= (expr const &a, expr const &b)
expr operator>= (expr const &a, int b)
expr operator>= (int a, expr const &b)
expr operator< (expr const &a, expr const &b)
expr operator< (expr const &a, int b)
expr operator< (int a, expr const &b)
expr operator> (expr const &a, expr const &b)
expr operator> (expr const &a, int b)
expr operator> (int a, expr const &b)
expr pble (expr_vector const &es, int const *coeffs, int bound)
expr pbge (expr_vector const &es, int const *coeffs, int bound)
expr pbeq (expr_vector const &es, int const *coeffs, int bound)
expr atmost (expr_vector const &es, unsigned bound)
expr atleast (expr_vector const &es, unsigned bound)
expr operator& (expr const &a, expr const &b)
expr operator& (expr const &a, int b)
expr operator& (int a, expr const &b)
expr operator^ (expr const &a, expr const &b)
expr operator^ (expr const &a, int b)
expr operator^ (int a, expr const &b)
expr operator| (expr const &a, expr const &b)
expr operator| (expr const &a, int b)
expr operator| (int a, expr const &b)
expr nand (expr const &a, expr const &b)
expr nor (expr const &a, expr const &b)
expr xnor (expr const &a, expr const &b)
expr min (expr const &a, expr const &b)
expr max (expr const &a, expr const &b)
expr bv2int (expr const &a, bool is_signed)
 bit-vector and integer conversions.
expr int2bv (unsigned n, expr const &a)
expr bvadd_no_overflow (expr const &a, expr const &b, bool is_signed)
 bit-vector overflow/underflow checks
expr bvadd_no_underflow (expr const &a, expr const &b)
expr bvsub_no_overflow (expr const &a, expr const &b)
expr bvsub_no_underflow (expr const &a, expr const &b, bool is_signed)
expr bvsdiv_no_overflow (expr const &a, expr const &b)
expr bvneg_no_overflow (expr const &a)
expr bvmul_no_overflow (expr const &a, expr const &b, bool is_signed)
expr bvmul_no_underflow (expr const &a, expr const &b)
expr bvredor (expr const &a)
expr bvredand (expr const &a)
expr abs (expr const &a)
expr sqrt (expr const &a, expr const &rm)
expr fp_eq (expr const &a, expr const &b)
expr operator~ (expr const &a)
expr fma (expr const &a, expr const &b, expr const &c, expr const &rm)
 FloatingPoint fused multiply-add.
expr fpa_fp (expr const &sgn, expr const &exp, expr const &sig)
 Create an expression of FloatingPoint sort from three bit-vector expressions.
expr fpa_to_sbv (expr const &t, unsigned sz)
 Conversion of a floating-point term into a signed bit-vector.
expr fpa_to_ubv (expr const &t, unsigned sz)
 Conversion of a floating-point term into an unsigned bit-vector.
expr sbv_to_fpa (expr const &t, sort s)
 Conversion of a signed bit-vector term into a floating-point.
expr ubv_to_fpa (expr const &t, sort s)
 Conversion of an unsigned bit-vector term into a floating-point.
expr fpa_to_fpa (expr const &t, sort s)
 Conversion of a floating-point term into another floating-point.
expr round_fpa_to_closest_integer (expr const &t)
 Round a floating-point term into its closest integer.
expr range (expr const &lo, expr const &hi)

Additional Inherited Members

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

Detailed Description

A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort Boolean. Every expression has a sort.

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

Constructor & Destructor Documentation

◆ expr() [1/2]

expr ( context & c)
inline

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

830:ast(c) {}

Referenced by abs, algebraic_lower(), algebraic_upper(), arg(), at(), atleast, atmost, bit2bool(), body(), bv2int, bvadd_no_overflow, bvadd_no_underflow, bvmul_no_overflow, bvmul_no_underflow, bvneg_no_overflow, bvredand, bvredor, bvsdiv_no_overflow, bvsub_no_overflow, bvsub_no_underflow, char_from_bv(), char_to_bv(), char_to_int(), concat, concat, contains(), denominator(), distinct, extract(), extract(), fma, fp_eq, fpa_fp, fpa_to_fpa, fpa_to_sbv, fpa_to_ubv, implies, implies, implies, int2bv, is_digit(), is_int, ite, expr::iterator::iterator(), itos(), length(), loop(), loop(), max, min, mk_and, mk_from_ieee_bv(), mk_is_inf(), mk_is_nan(), mk_is_normal(), mk_is_subnormal(), mk_is_zero(), mk_or, mk_to_ieee_bv(), mk_xor, mod, mod, mod, nand, nor, nth(), numerator(), operator!, operator!=, operator!=, operator!=, operator&, operator&, operator&, operator&&, operator&&, operator&&, expr::iterator::operator*(), operator*, operator*, operator*, operator+, operator+, operator+, operator-, operator-, operator-, operator-, operator/, operator/, operator/, operator<, operator<, operator<, operator<=, operator<=, operator<=, operator==, operator==, operator==, operator>, operator>, operator>, operator>=, operator>=, operator>=, operator[](), operator[](), operator^, operator^, operator^, operator|, operator|, operator|, operator||, operator||, operator||, operator~, pbeq, pbge, pble, pw, pw, pw, range, rem, rem, rem, repeat(), replace(), rotate_left(), rotate_right(), round_fpa_to_closest_integer, sbv_to_fpa, sbvtos(), simplify(), simplify(), sqrt, stoi(), substitute(), substitute(), substitute(), sum, ubv_to_fpa, ubvtos(), unit(), and xnor.

◆ expr() [2/2]

expr ( context & c,
Z3_ast n )
inline

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

831: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 1064 of file z3++.h.

1064 {
1065 assert(is_algebraic());
1066 unsigned i = Z3_algebraic_get_i(ctx(), m_ast);
1067 check_error();
1068 return i;
1069 }
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 1037 of file z3++.h.

1037 {
1038 assert(is_algebraic());
1039 Z3_ast r = Z3_get_algebraic_number_lower(ctx(), m_ast, precision);
1040 check_error();
1041 return expr(ctx(), r);
1042 }
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 1054 of file z3++.h.

1054 {
1055 assert(is_algebraic());
1056 Z3_ast_vector r = Z3_algebraic_get_poly(ctx(), m_ast);
1057 check_error();
1058 return expr_vector(ctx(), r);
1059 }
Z3_algebraic_get_poly
Z3_ast_vector Z3_API Z3_algebraic_get_poly(Z3_context c, Z3_ast a)
Return the coefficients of the defining polynomial.
z3::expr_vector
ast_vector_tpl< expr > expr_vector
Definition z3++.h:76

◆ algebraic_upper()

expr algebraic_upper ( unsigned precision) const
inline

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

1044 {
1045 assert(is_algebraic());
1046 Z3_ast r = Z3_get_algebraic_number_upper(ctx(), m_ast, precision);
1047 check_error();
1048 return expr(ctx(), r);
1049 }
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 1225 of file z3++.h.

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

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

◆ args()

expr_vector args ( ) const
inline

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

Precondition
is_app()

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

1232 {
1233 expr_vector vec(ctx());
1234 unsigned argCnt = num_args();
1235 for (unsigned i = 0; i < argCnt; i++)
1236 vec.push_back(arg(i));
1237 return vec;
1238 }

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

◆ as_binary()

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

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

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

◆ as_double()

double as_double ( ) const
inline

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

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

◆ as_int64()

int64_t as_int64 ( ) const
inline

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

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

◆ as_uint64()

uint64_t as_uint64 ( ) const
inline

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

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

◆ at()

expr at ( expr const & index) const
inline

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

1505 {
1506 check_context(*this, index);
1507 Z3_ast r = Z3_mk_seq_at(ctx(), *this, index);
1508 check_error();
1509 return expr(ctx(), r);
1510 }
Z3_mk_seq_at
Z3_ast Z3_API Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index)
Retrieve from s the unit sequence positioned at position index. The sequence is empty if the index is...
z3::check_context
void check_context(object const &a, object const &b)
Definition z3++.h:495

◆ begin()

iterator begin ( )
inline

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

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

◆ bit2bool()

expr bit2bool ( unsigned i) const
inline

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

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

◆ body()

expr body ( ) const
inline

Return the 'body' of this quantifier.

Precondition
is_quantifier()

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

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

◆ bool_value()

Z3_lbool bool_value ( ) const
inline

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

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

◆ char_from_bv()

expr char_from_bv ( ) const
inline

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

1552 {
1553 Z3_ast r = Z3_mk_char_from_bv(ctx(), *this);
1554 check_error();
1555 return expr(ctx(), r);
1556 }
Z3_mk_char_from_bv
Z3_ast Z3_API Z3_mk_char_from_bv(Z3_context c, Z3_ast bv)
Create a character from a bit-vector (code point).

◆ char_to_bv()

expr char_to_bv ( ) const
inline

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

1547 {
1548 Z3_ast r = Z3_mk_char_to_bv(ctx(), *this);
1549 check_error();
1550 return expr(ctx(), r);
1551 }
Z3_mk_char_to_bv
Z3_ast Z3_API Z3_mk_char_to_bv(Z3_context c, Z3_ast ch)
Create a bit-vector (code point) from character.

◆ char_to_int()

expr char_to_int ( ) const
inline

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

1542 {
1543 Z3_ast r = Z3_mk_char_to_int(ctx(), *this);
1544 check_error();
1545 return expr(ctx(), r);
1546 }
Z3_mk_char_to_int
Z3_ast Z3_API Z3_mk_char_to_int(Z3_context c, Z3_ast ch)
Create an integer (code point) from character.

◆ contains()

expr contains ( expr const & s) const
inline

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

1499 {
1500 check_context(*this, s);
1501 Z3_ast r = Z3_mk_seq_contains(ctx(), *this, s);
1502 check_error();
1503 return expr(ctx(), r);
1504 }
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 1210 of file z3++.h.

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

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

◆ denominator()

expr denominator ( ) const
inline

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

1162 {
1163 assert(is_numeral());
1164 Z3_ast r = Z3_get_denominator(ctx(), m_ast);
1165 check_error();
1166 return expr(ctx(),r);
1167 }
Z3_get_denominator
Z3_ast Z3_API Z3_get_denominator(Z3_context c, Z3_ast a)
Return the denominator (as a numeral AST) of a numeral AST of sort Real.

◆ end()

iterator end ( )
inline

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

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

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

1484 {
1485 check_context(*this, offset); check_context(offset, length);
1486 Z3_ast r = Z3_mk_seq_extract(ctx(), *this, offset, length); check_error(); return expr(ctx(), r);
1487 }
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 1434 of file z3++.h.

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

◆ get_decimal_string()

std::string get_decimal_string ( int precision) const
inline

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

Precondition
is_numeral() || is_algebraic()

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

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

◆ get_numeral_int()

int get_numeral_int ( ) const
inline

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

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

Precondition
is_numeral()

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

1086 {
1087 int result = 0;
1088 if (!is_numeral_i(result)) {
1089 assert(ctx().enable_exceptions());
1090 if (!ctx().enable_exceptions()) return 0;
1091 Z3_THROW(exception("numeral does not fit in machine int"));
1092 }
1093 return result;
1094 }
Z3_THROW
#define Z3_THROW(x)
Definition z3++.h:103

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

1122 {
1123 assert(is_numeral());
1124 int64_t result = 0;
1125 if (!is_numeral_i64(result)) {
1126 assert(ctx().enable_exceptions());
1127 if (!ctx().enable_exceptions()) return 0;
1128 Z3_THROW(exception("numeral does not fit in machine int64_t"));
1129 }
1130 return result;
1131 }

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

1105 {
1106 assert(is_numeral());
1107 unsigned result = 0;
1108 if (!is_numeral_u(result)) {
1109 assert(ctx().enable_exceptions());
1110 if (!ctx().enable_exceptions()) return 0;
1111 Z3_THROW(exception("numeral does not fit in machine uint"));
1112 }
1113 return result;
1114 }

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

1139 {
1140 assert(is_numeral());
1141 uint64_t result = 0;
1142 if (!is_numeral_u64(result)) {
1143 assert(ctx().enable_exceptions());
1144 if (!ctx().enable_exceptions()) return 0;
1145 Z3_THROW(exception("numeral does not fit in machine uint64_t"));
1146 }
1147 return result;
1148 }

◆ get_sort()

sort get_sort ( ) const
inline

Return the sort of this expression.

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

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

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

◆ get_string()

std::string get_string ( ) const
inline

for a string value expression return an escaped string value.

Precondition
expression is for a string value.

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

1181 {
1182 assert(is_string_value());
1183 char const* s = Z3_get_string(ctx(), m_ast);
1184 check_error();
1185 return std::string(s);
1186 }
Z3_get_string
Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s)
Retrieve the string constant stored in s. Characters outside the basic printable ASCII range are esca...
z3py.is_string_value
bool is_string_value(Any a)
Definition z3py.py:11219

◆ get_u32string()

std::u32string get_u32string ( ) const
inline

for a string value expression return an unespaced string value.

Precondition
expression is for a string value.

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

1193 {
1194 assert(is_string_value());
1195 unsigned n = Z3_get_string_length(ctx(), m_ast);
1196 std::u32string s;
1197 s.resize(n);
1198 Z3_get_string_contents(ctx(), m_ast, n, (unsigned*)s.data());
1199 return s;
1200 }
Z3_get_string_contents
void Z3_API Z3_get_string_contents(Z3_context c, Z3_ast s, unsigned length, unsigned contents[])
Retrieve the unescaped string constant stored in s.
Z3_get_string_length
unsigned Z3_API Z3_get_string_length(Z3_context c, Z3_ast s)
Retrieve the length of the unescaped string constant stored in s.

◆ hi()

unsigned hi ( ) const
inline

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

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

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

◆ id()

unsigned id ( ) const
inline

retrieve unique identifier for expression.

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

1074{ 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 946 of file z3++.h.

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

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

◆ is_and()

bool is_and ( ) const
inline

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

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

◆ is_app()

bool is_app ( ) const
inline

Return true if this expression is an application.

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

916{ return kind() == Z3_APP_AST || kind() == Z3_NUMERAL_AST; }
Z3_APP_AST
@ Z3_APP_AST
Definition z3_api.h:144
Z3_NUMERAL_AST
@ Z3_NUMERAL_AST
Definition z3_api.h:143

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

◆ is_arith()

bool is_arith ( ) const
inline

Return true if this is an integer or real expression.

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

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

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

◆ is_array()

bool is_array ( ) const
inline

Return true if this is a Array expression.

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

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

Referenced by operator[]().

◆ is_bool()

bool is_bool ( ) const
inline

Return true if this is a Boolean expression.

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

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

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

◆ is_bv()

bool is_bv ( ) const
inline

Return true if this is a Bit-vector expression.

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

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

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

◆ is_const()

bool is_const ( ) const
inline

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

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

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

Referenced by solver::add().

◆ is_datatype()

bool is_datatype ( ) const
inline

Return true if this is a Datatype expression.

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

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

◆ is_digit()

expr is_digit ( ) const
inline

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

1557 {
1558 Z3_ast r = Z3_mk_char_is_digit(ctx(), *this);
1559 check_error();
1560 return expr(ctx(), r);
1561 }
Z3_mk_char_is_digit
Z3_ast Z3_API Z3_mk_char_is_digit(Z3_context c, Z3_ast ch)
Create a check if the character is a digit.

◆ is_distinct()

bool is_distinct ( ) const
inline

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

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

◆ is_eq()

bool is_eq ( ) const
inline

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

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

◆ is_exists()

bool is_exists ( ) const
inline

Return true if this expression is an existential quantifier.

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

933{ 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 1312 of file z3++.h.

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

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

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

◆ is_forall()

bool is_forall ( ) const
inline

Return true if this expression is a universal quantifier.

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

929{ 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 891 of file z3++.h.

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

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

◆ is_implies()

bool is_implies ( ) const
inline

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

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

◆ is_int()

bool is_int ( ) const
inline

Return true if this is an integer expression.

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

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

Referenced by abs.

◆ is_ite()

bool is_ite ( ) const
inline

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

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

◆ is_lambda()

bool is_lambda ( ) const
inline

Return true if this expression is a lambda expression.

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

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

◆ is_not()

bool is_not ( ) const
inline

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

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

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

898{ return kind() == Z3_NUMERAL_AST; }

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

◆ is_numeral() [2/4]

bool is_numeral ( double & d) const
inline

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

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

Referenced by is_numeral().

◆ is_numeral() [3/4]

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

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

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

Referenced by is_numeral().

◆ is_numeral() [4/4]

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

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

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

Referenced by is_numeral().

◆ is_numeral_i()

bool is_numeral_i ( int & i) const
inline

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

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

Referenced by get_numeral_int().

◆ is_numeral_i64()

bool is_numeral_i64 ( int64_t & i) const
inline

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

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

Referenced by as_int64(), and get_numeral_int64().

◆ is_numeral_u()

bool is_numeral_u ( unsigned & i) const
inline

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

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

Referenced by get_numeral_uint().

◆ is_numeral_u64()

bool is_numeral_u64 ( uint64_t & i) const
inline

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

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

Referenced by as_uint64(), and get_numeral_uint64().

◆ is_or()

bool is_or ( ) const
inline

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

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

◆ is_quantifier()

bool is_quantifier ( ) const
inline

Return true if this expression is a quantifier.

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

924{ return kind() == Z3_QUANTIFIER_AST; }
Z3_QUANTIFIER_AST
@ Z3_QUANTIFIER_AST
Definition z3_api.h:146

Referenced by body().

◆ is_re()

bool is_re ( ) const
inline

Return true if this is a regular expression.

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

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

Referenced by operator+.

◆ is_real()

bool is_real ( ) const
inline

Return true if this is a real expression.

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

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

Referenced by abs.

◆ is_relation()

bool is_relation ( ) const
inline

Return true if this is a Relation expression.

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

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

◆ is_seq()

bool is_seq ( ) const
inline

Return true if this is a sequence expression.

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

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

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

◆ is_string_value()

bool is_string_value ( ) const
inline

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

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

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

Referenced by get_string(), and get_u32string().

◆ is_true()

bool is_true ( ) const
inline

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

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

◆ is_var()

bool is_var ( ) const
inline

Return true if this expression is a variable.

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

942{ return kind() == Z3_VAR_AST; }
Z3_VAR_AST
@ Z3_VAR_AST
Definition z3_api.h:145

◆ is_well_sorted()

bool is_well_sorted ( ) const
inline

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

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

951{ 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 1316 of file z3++.h.

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

◆ itos()

expr itos ( ) const
inline

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

1527 {
1528 Z3_ast r = Z3_mk_int_to_str(ctx(), *this);
1529 check_error();
1530 return expr(ctx(), r);
1531 }
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 1517 of file z3++.h.

1517 {
1518 Z3_ast r = Z3_mk_seq_length(ctx(), *this);
1519 check_error();
1520 return expr(ctx(), r);
1521 }
Z3_mk_seq_length
Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s)
Return the length of the sequence s.

Referenced by extract().

◆ lo()

unsigned lo ( ) const
inline

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

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

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

◆ loop() [1/2]

expr loop ( unsigned lo)
inline

create a looping regular expression.

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

1567 {
1568 Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, 0);
1569 check_error();
1570 return expr(ctx(), r);
1571 }
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 1572 of file z3++.h.

1572 {
1573 Z3_ast r = Z3_mk_re_loop(ctx(), m_ast, lo, hi);
1574 check_error();
1575 return expr(ctx(), r);
1576 }

◆ mk_from_ieee_bv()

expr mk_from_ieee_bv ( sort const & s) const
inline

Convert this IEEE BV into a fpa.

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

1016 {
1017 assert(is_bv());
1018 Z3_ast r = Z3_mk_fpa_to_fp_bv(ctx(), m_ast, s);
1019 check_error();
1020 return expr(ctx(), r);
1021 }
Z3_mk_fpa_to_fp_bv
Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(Z3_context c, Z3_ast bv, Z3_sort s)
Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
z3py.is_bv
is_bv(a)
Definition z3py.py:4055

◆ mk_is_inf()

expr mk_is_inf ( ) const
inline

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

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

956 {
957 assert(is_fpa());
958 Z3_ast r = Z3_mk_fpa_is_infinite(ctx(), m_ast);
959 check_error();
960 return expr(ctx(), r);
961 }
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 966 of file z3++.h.

966 {
967 assert(is_fpa());
968 Z3_ast r = Z3_mk_fpa_is_nan(ctx(), m_ast);
969 check_error();
970 return expr(ctx(), r);
971 }
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 976 of file z3++.h.

976 {
977 assert(is_fpa());
978 Z3_ast r = Z3_mk_fpa_is_normal(ctx(), m_ast);
979 check_error();
980 return expr(ctx(), r);
981 }
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 986 of file z3++.h.

986 {
987 assert(is_fpa());
988 Z3_ast r = Z3_mk_fpa_is_subnormal(ctx(), m_ast);
989 check_error();
990 return expr(ctx(), r);
991 }
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 996 of file z3++.h.

996 {
997 assert(is_fpa());
998 Z3_ast r = Z3_mk_fpa_is_zero(ctx(), m_ast);
999 check_error();
1000 return expr(ctx(), r);
1001 }
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 1006 of file z3++.h.

1006 {
1007 assert(is_fpa());
1008 Z3_ast r = Z3_mk_fpa_to_ieee_bv(ctx(), m_ast);
1009 check_error();
1010 return expr(ctx(), r);
1011 }
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 1511 of file z3++.h.

1511 {
1512 check_context(*this, index);
1513 Z3_ast r = Z3_mk_seq_nth(ctx(), *this, index);
1514 check_error();
1515 return expr(ctx(), r);
1516 }
Z3_mk_seq_nth
Z3_ast Z3_API Z3_mk_seq_nth(Z3_context c, Z3_ast s, Z3_ast index)
Retrieve from s the element positioned at position index. The function is under-specified if the inde...

Referenced by operator[]().

◆ num_args()

unsigned num_args ( ) const
inline

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

Precondition
is_app()

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

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

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

◆ numerator()

expr numerator ( ) const
inline

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

1154 {
1155 assert(is_numeral());
1156 Z3_ast r = Z3_get_numerator(ctx(), m_ast);
1157 check_error();
1158 return expr(ctx(),r);
1159 }
Z3_get_numerator
Z3_ast Z3_API Z3_get_numerator(Z3_context c, Z3_ast a)
Return the numerator (as a numeral AST) of a numeral AST of sort Real.

◆ operator Z3_app()

operator Z3_app ( ) const
inline

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

1202{ 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 1581 of file z3++.h.

1581 {
1582 assert(is_array() || is_seq());
1583 if (is_array()) {
1584 return select(*this, index);
1585 }
1586 return nth(index);
1587 }
z3::select
expr select(expr const &a, expr const &i)
forward declarations
Definition z3++.h:3996
z3py.is_array
bool is_array(Any a)
Definition z3py.py:4745
z3py.is_seq
is_seq(a)
Definition z3py.py:11201

◆ operator[]() [2/2]

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

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

1589 {
1590 return select(*this, index);
1591 }

◆ repeat()

expr repeat ( unsigned i) const
inline

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

1424{ 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 1488 of file z3++.h.

1488 {
1489 check_context(*this, src); check_context(src, dst);
1490 Z3_ast r = Z3_mk_seq_replace(ctx(), *this, src, dst);
1491 check_error();
1492 return expr(ctx(), r);
1493 }
Z3_mk_seq_replace
Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst)
Replace the first occurrence of src with dst in s.

◆ rotate_left()

expr rotate_left ( unsigned i) const
inline

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

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

◆ rotate_right()

expr rotate_right ( unsigned i) const
inline

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

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

◆ sbvtos()

expr sbvtos ( ) const
inline

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

1537 {
1538 Z3_ast r = Z3_mk_sbv_to_str(ctx(), *this);
1539 check_error();
1540 return expr(ctx(), r);
1541 }
Z3_mk_sbv_to_str
Z3_ast Z3_API Z3_mk_sbv_to_str(Z3_context c, Z3_ast s)
Signed bit-vector to string conversion.

◆ simplify() [1/2]

expr simplify ( ) const
inline

Return a simplified version of this expression.

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

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

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

1522 {
1523 Z3_ast r = Z3_mk_str_to_int(ctx(), *this);
1524 check_error();
1525 return expr(ctx(), r);
1526 }
Z3_mk_str_to_int
Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s)
Convert string to integer.

◆ substitute() [1/3]

expr substitute ( expr_vector const & dst)
inline

Apply substitution. Replace bound variables by expressions.

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

4284 {
4285 array<Z3_ast> _dst(dst.size());
4286 for (unsigned i = 0; i < dst.size(); ++i) {
4287 _dst[i] = dst[i];
4288 }
4289 Z3_ast r = Z3_substitute_vars(ctx(), m_ast, dst.size(), _dst.ptr());
4290 check_error();
4291 return expr(ctx(), r);
4292 }
Z3_substitute_vars
Z3_ast Z3_API Z3_substitute_vars(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const to[])
Substitute the variables in a with the expressions in to. For every i smaller than num_exprs,...

◆ substitute() [2/3]

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

Apply substitution. Replace src expressions by dst.

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

4271 {
4272 assert(src.size() == dst.size());
4273 array<Z3_ast> _src(src.size());
4274 array<Z3_ast> _dst(dst.size());
4275 for (unsigned i = 0; i < src.size(); ++i) {
4276 _src[i] = src[i];
4277 _dst[i] = dst[i];
4278 }
4279 Z3_ast r = Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
4280 check_error();
4281 return expr(ctx(), r);
4282 }
Z3_substitute
Z3_ast Z3_API Z3_substitute(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const from[], Z3_ast const to[])
Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs....

◆ substitute() [3/3]

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

Apply function substitution by macro definitions.

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

4294 {
4295 array<Z3_ast> _dst(dst.size());
4296 array<Z3_func_decl> _funs(funs.size());
4297 if (dst.size() != funs.size()) {
4298 Z3_THROW(exception("length of argument lists don't align"));
4299 return expr(ctx(), nullptr);
4300 }
4301 for (unsigned i = 0; i < dst.size(); ++i) {
4302 _dst[i] = dst[i];
4303 _funs[i] = funs[i];
4304 }
4305 Z3_ast r = Z3_substitute_funs(ctx(), m_ast, dst.size(), _funs.ptr(), _dst.ptr());
4306 check_error();
4307 return expr(ctx(), r);
4308 }
Z3_substitute_funs
Z3_ast Z3_API Z3_substitute_funs(Z3_context c, Z3_ast a, unsigned num_funs, Z3_func_decl const from[], Z3_ast const to[])
Substitute functions in from with new expressions in to.

◆ ubvtos()

expr ubvtos ( ) const
inline

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

1532 {
1533 Z3_ast r = Z3_mk_ubv_to_str(ctx(), *this);
1534 check_error();
1535 return expr(ctx(), r);
1536 }
Z3_mk_ubv_to_str
Z3_ast Z3_API Z3_mk_ubv_to_str(Z3_context c, Z3_ast s)
Unsigned bit-vector to string conversion.

◆ unit()

expr unit ( ) const
inline

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

1494 {
1495 Z3_ast r = Z3_mk_seq_unit(ctx(), *this);
1496 check_error();
1497 return expr(ctx(), r);
1498 }
Z3_mk_seq_unit
Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a)
Create a unit sequence of a.

◆ abs

expr abs ( expr const & a)
friend

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

2012 {
2013 Z3_ast r;
2014 if (a.is_int()) {
2015 expr zero = a.ctx().int_val(0);
2016 expr ge = a >= zero;
2017 expr na = -a;
2018 r = Z3_mk_ite(a.ctx(), ge, a, na);
2019 }
2020 else if (a.is_real()) {
2021 expr zero = a.ctx().real_val(0);
2022 expr ge = a >= zero;
2023 expr na = -a;
2024 r = Z3_mk_ite(a.ctx(), ge, a, na);
2025 }
2026 else {
2027 r = Z3_mk_fpa_abs(a.ctx(), a);
2028 }
2029 a.check_error();
2030 return expr(a.ctx(), r);
2031 }
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 2455 of file z3++.h.

2455 {
2456 assert(es.size() > 0);
2457 context& ctx = es[0u].ctx();
2458 array<Z3_ast> _es(es);
2459 Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
2460 ctx.check_error();
2461 return expr(ctx, r);
2462 }
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 2447 of file z3++.h.

2447 {
2448 assert(es.size() > 0);
2449 context& ctx = es[0u].ctx();
2450 array<Z3_ast> _es(es);
2451 Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
2452 ctx.check_error();
2453 return expr(ctx, r);
2454 }
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 2258 of file z3++.h.

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

2264 {
2265 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);
2266 }
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 2267 of file z3++.h.

2267 {
2268 check_context(a, b); Z3_ast r = Z3_mk_bvadd_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2269 }
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 2282 of file z3++.h.

2282 {
2283 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);
2284 }
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 2285 of file z3++.h.

2285 {
2286 check_context(a, b); Z3_ast r = Z3_mk_bvmul_no_underflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2287 }
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 2279 of file z3++.h.

2279 {
2280 Z3_ast r = Z3_mk_bvneg_no_overflow(a.ctx(), a); a.check_error(); return expr(a.ctx(), r);
2281 }
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 2006 of file z3++.h.

2006 {
2007 assert(a.is_bv());
2008 Z3_ast r = Z3_mk_bvredand(a.ctx(), a);
2009 a.check_error();
2010 return expr(a.ctx(), r);
2011 }
Z3_mk_bvredand
Z3_ast Z3_API Z3_mk_bvredand(Z3_context c, Z3_ast t1)
Take conjunction of bits in vector, return vector of length 1.

◆ bvredor

expr bvredor ( expr const & a)
friend

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

2000 {
2001 assert(a.is_bv());
2002 Z3_ast r = Z3_mk_bvredor(a.ctx(), a);
2003 a.check_error();
2004 return expr(a.ctx(), r);
2005 }
Z3_mk_bvredor
Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1)
Take disjunction of bits in vector, return vector of length 1.

◆ bvsdiv_no_overflow

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

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

2276 {
2277 check_context(a, b); Z3_ast r = Z3_mk_bvsdiv_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2278 }
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 2270 of file z3++.h.

2270 {
2271 check_context(a, b); Z3_ast r = Z3_mk_bvsub_no_overflow(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r);
2272 }
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 2273 of file z3++.h.

2273 {
2274 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);
2275 }
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 2481 of file z3++.h.

2481 {
2482 check_context(a, b);
2483 Z3_ast r;
2484 if (Z3_is_seq_sort(a.ctx(), a.get_sort())) {
2485 Z3_ast _args[2] = { a, b };
2486 r = Z3_mk_seq_concat(a.ctx(), 2, _args);
2487 }
2488 else if (Z3_is_re_sort(a.ctx(), a.get_sort())) {
2489 Z3_ast _args[2] = { a, b };
2490 r = Z3_mk_re_concat(a.ctx(), 2, _args);
2491 }
2492 else {
2493 r = Z3_mk_concat(a.ctx(), a, b);
2494 }
2495 a.ctx().check_error();
2496 return expr(a.ctx(), r);
2497 }
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 2499 of file z3++.h.

2499 {
2500 Z3_ast r;
2501 assert(args.size() > 0);
2502 if (args.size() == 1) {
2503 return args[0u];
2504 }
2505 context& ctx = args[0u].ctx();
2506 array<Z3_ast> _args(args);
2507 if (Z3_is_seq_sort(ctx, args[0u].get_sort())) {
2508 r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
2509 }
2510 else if (Z3_is_re_sort(ctx, args[0u].get_sort())) {
2511 r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
2512 }
2513 else {
2514 r = _args[args.size()-1];
2515 for (unsigned i = args.size()-1; i > 0; ) {
2516 --i;
2517 r = Z3_mk_concat(ctx, _args[i], r);
2518 ctx.check_error();
2519 }
2520 }
2521 ctx.check_error();
2522 return expr(ctx, r);
2523 }

◆ distinct

expr distinct ( expr_vector const & args)
friend

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

2472 {
2473 assert(args.size() > 0);
2474 context& ctx = args[0u].ctx();
2475 array<Z3_ast> _args(args);
2476 Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
2477 ctx.check_error();
2478 return expr(ctx, r);
2479 }
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 2048 of file z3++.h.

2048 {
2049 check_context(a, b); check_context(a, c); check_context(a, rm);
2050 assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
2051 Z3_ast r = Z3_mk_fpa_fma(a.ctx(), rm, a, b, c);
2052 a.check_error();
2053 return expr(a.ctx(), r);
2054 }
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 2039 of file z3++.h.

2039 {
2040 check_context(a, b);
2041 assert(a.is_fpa());
2042 Z3_ast r = Z3_mk_fpa_eq(a.ctx(), a, b);
2043 a.check_error();
2044 return expr(a.ctx(), r);
2045 }
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 2056 of file z3++.h.

2056 {
2057 check_context(sgn, exp); check_context(exp, sig);
2058 assert(sgn.is_bv() && exp.is_bv() && sig.is_bv());
2059 Z3_ast r = Z3_mk_fpa_fp(sgn.ctx(), sgn, exp, sig);
2060 sgn.check_error();
2061 return expr(sgn.ctx(), r);
2062 }

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

2092 {
2093 assert(t.is_fpa());
2094 Z3_ast r = Z3_mk_fpa_to_fp_float(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2095 t.check_error();
2096 return expr(t.ctx(), r);
2097 }
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 2064 of file z3++.h.

2064 {
2065 assert(t.is_fpa());
2066 Z3_ast r = Z3_mk_fpa_to_sbv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
2067 t.check_error();
2068 return expr(t.ctx(), r);
2069 }
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 2071 of file z3++.h.

2071 {
2072 assert(t.is_fpa());
2073 Z3_ast r = Z3_mk_fpa_to_ubv(t.ctx(), t.ctx().fpa_rounding_mode(), t, sz);
2074 t.check_error();
2075 return expr(t.ctx(), r);
2076 }
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 1651 of file z3++.h.

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

◆ implies [2/3]

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

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

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

◆ implies [3/3]

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

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

1646 {
1647 assert(a.is_bool() && b.is_bool());
1648 _Z3_MK_BIN_(a, b, Z3_mk_implies);
1649 }
Z3_mk_implies
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
_Z3_MK_BIN_
#define _Z3_MK_BIN_(a, b, binop)
Definition z3++.h:1639

◆ int2bv

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

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

2259{ 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 1694 of file z3++.h.

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

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

2111 {
2112 check_context(c, t); check_context(c, e);
2113 assert(c.is_bool());
2114 Z3_ast r = Z3_mk_ite(c.ctx(), c, t, e);
2115 c.check_error();
2116 return expr(c.ctx(), r);
2117 }

◆ max

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

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

1984 {
1985 check_context(a, b);
1986 Z3_ast r;
1987 if (a.is_arith()) {
1988 r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), a, b);
1989 }
1990 else if (a.is_bv()) {
1991 r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), a, b);
1992 }
1993 else {
1994 assert(a.is_fpa());
1995 r = Z3_mk_fpa_max(a.ctx(), a, b);
1996 }
1997 a.check_error();
1998 return expr(a.ctx(), r);
1999 }
Z3_mk_ge
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
Z3_mk_fpa_max
Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2)
Maximum of floating-point numbers.
Z3_mk_bvuge
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.

◆ min

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

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

1968 {
1969 check_context(a, b);
1970 Z3_ast r;
1971 if (a.is_arith()) {
1972 r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, b), b, a);
1973 }
1974 else if (a.is_bv()) {
1975 r = Z3_mk_ite(a.ctx(), Z3_mk_bvuge(a.ctx(), a, b), b, a);
1976 }
1977 else {
1978 assert(a.is_fpa());
1979 r = Z3_mk_fpa_min(a.ctx(), a, b);
1980 }
1981 a.check_error();
1982 return expr(a.ctx(), r);
1983 }
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 2559 of file z3++.h.

2559 {
2560 array<Z3_ast> _args(args);
2561 Z3_ast r = Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2562 args.check_error();
2563 return expr(args.ctx(), r);
2564 }
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 2553 of file z3++.h.

2553 {
2554 array<Z3_ast> _args(args);
2555 Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2556 args.check_error();
2557 return expr(args.ctx(), r);
2558 }
Z3_mk_or
Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] or ... or args[num_args-1].

◆ mk_xor

expr mk_xor ( expr_vector const & args)
friend

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

2565 {
2566 if (args.empty())
2567 return args.ctx().bool_val(false);
2568 expr r = args[0u];
2569 for (unsigned i = 1; i < args.size(); ++i)
2570 r = r ^ args[i];
2571 return r;
2572 }

◆ mod [1/3]

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

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

1658 {
1659 if (a.is_bv()) {
1660 _Z3_MK_BIN_(a, b, Z3_mk_bvsmod);
1661 }
1662 else {
1663 _Z3_MK_BIN_(a, b, Z3_mk_mod);
1664 }
1665 }
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 1666 of file z3++.h.

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

◆ mod [3/3]

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

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

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

◆ nand

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

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

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

◆ nor

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

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

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

◆ operator!

expr operator! ( expr const & a)
friend

Return an expression representing not(a).

Precondition
a.is_bool()

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

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

1734 {
1735 check_context(a, b);
1736 Z3_ast args[2] = { a, b };
1737 Z3_ast r = Z3_mk_distinct(a.ctx(), 2, args);
1738 a.check_error();
1739 return expr(a.ctx(), r);
1740 }

◆ operator!= [2/3]

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

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

1741{ 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 1742 of file z3++.h.

1742{ 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 1953 of file z3++.h.

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

◆ operator& [2/3]

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

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

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

◆ operator& [3/3]

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

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

1955{ 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 1708 of file z3++.h.

1708{ 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 1707 of file z3++.h.

1707{ 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 1698 of file z3++.h.

1698 {
1699 check_context(a, b);
1700 assert(a.is_bool() && b.is_bool());
1701 Z3_ast args[2] = { a, b };
1702 Z3_ast r = Z3_mk_and(a.ctx(), 2, args);
1703 a.check_error();
1704 return expr(a.ctx(), r);
1705 }

◆ operator* [1/3]

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

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

1776 {
1777 check_context(a, b);
1778 Z3_ast r = 0;
1779 if (a.is_arith() && b.is_arith()) {
1780 Z3_ast args[2] = { a, b };
1781 r = Z3_mk_mul(a.ctx(), 2, args);
1782 }
1783 else if (a.is_bv() && b.is_bv()) {
1784 r = Z3_mk_bvmul(a.ctx(), a, b);
1785 }
1786 else if (a.is_fpa() && b.is_fpa()) {
1787 r = Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1788 }
1789 else {
1790 // operator is not supported by given arguments.
1791 assert(false);
1792 }
1793 a.check_error();
1794 return expr(a.ctx(), r);
1795 }
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 1796 of file z3++.h.

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

◆ operator* [3/3]

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

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

1797{ 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 1746 of file z3++.h.

1746 {
1747 check_context(a, b);
1748 Z3_ast r = 0;
1749 if (a.is_arith() && b.is_arith()) {
1750 Z3_ast args[2] = { a, b };
1751 r = Z3_mk_add(a.ctx(), 2, args);
1752 }
1753 else if (a.is_bv() && b.is_bv()) {
1754 r = Z3_mk_bvadd(a.ctx(), a, b);
1755 }
1756 else if (a.is_seq() && b.is_seq()) {
1757 return concat(a, b);
1758 }
1759 else if (a.is_re() && b.is_re()) {
1760 Z3_ast _args[2] = { a, b };
1761 r = Z3_mk_re_union(a.ctx(), 2, _args);
1762 }
1763 else if (a.is_fpa() && b.is_fpa()) {
1764 r = Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1765 }
1766 else {
1767 // operator is not supported by given arguments.
1768 assert(false);
1769 }
1770 a.check_error();
1771 return expr(a.ctx(), r);
1772 }
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_fpa_add
Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point addition.
Z3_mk_add
Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] + ... + args[num_args-1].
z3::concat
expr concat(expr const &a, expr const &b)
Definition z3++.h:2481

◆ operator+ [2/3]

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

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

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

◆ operator+ [3/3]

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

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

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

◆ operator- [1/4]

expr operator- ( expr const & a)
friend

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

1842 {
1843 Z3_ast r = 0;
1844 if (a.is_arith()) {
1845 r = Z3_mk_unary_minus(a.ctx(), a);
1846 }
1847 else if (a.is_bv()) {
1848 r = Z3_mk_bvneg(a.ctx(), a);
1849 }
1850 else if (a.is_fpa()) {
1851 r = Z3_mk_fpa_neg(a.ctx(), a);
1852 }
1853 else {
1854 // operator is not supported by given arguments.
1855 assert(false);
1856 }
1857 a.check_error();
1858 return expr(a.ctx(), r);
1859 }
Z3_mk_unary_minus
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
Z3_mk_fpa_neg
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.
Z3_mk_bvneg
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.

◆ operator- [2/4]

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

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

1861 {
1862 check_context(a, b);
1863 Z3_ast r = 0;
1864 if (a.is_arith() && b.is_arith()) {
1865 Z3_ast args[2] = { a, b };
1866 r = Z3_mk_sub(a.ctx(), 2, args);
1867 }
1868 else if (a.is_bv() && b.is_bv()) {
1869 r = Z3_mk_bvsub(a.ctx(), a, b);
1870 }
1871 else if (a.is_fpa() && b.is_fpa()) {
1872 r = Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1873 }
1874 else {
1875 // operator is not supported by given arguments.
1876 assert(false);
1877 }
1878 a.check_error();
1879 return expr(a.ctx(), r);
1880 }
Z3_mk_fpa_sub
Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point subtraction.
Z3_mk_bvsub
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
Z3_mk_sub
Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] - ... - args[num_args - 1].

◆ operator- [3/4]

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

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

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

◆ operator- [4/4]

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

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

1882{ 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 1820 of file z3++.h.

1820 {
1821 check_context(a, b);
1822 Z3_ast r = 0;
1823 if (a.is_arith() && b.is_arith()) {
1824 r = Z3_mk_div(a.ctx(), a, b);
1825 }
1826 else if (a.is_bv() && b.is_bv()) {
1827 r = Z3_mk_bvsdiv(a.ctx(), a, b);
1828 }
1829 else if (a.is_fpa() && b.is_fpa()) {
1830 r = Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1831 }
1832 else {
1833 // operator is not supported by given arguments.
1834 assert(false);
1835 }
1836 a.check_error();
1837 return expr(a.ctx(), r);
1838 }
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 1839 of file z3++.h.

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

◆ operator/ [3/3]

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

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

1840{ 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 1909 of file z3++.h.

1909 {
1910 check_context(a, b);
1911 Z3_ast r = 0;
1912 if (a.is_arith() && b.is_arith()) {
1913 r = Z3_mk_lt(a.ctx(), a, b);
1914 }
1915 else if (a.is_bv() && b.is_bv()) {
1916 r = Z3_mk_bvslt(a.ctx(), a, b);
1917 }
1918 else if (a.is_fpa() && b.is_fpa()) {
1919 r = Z3_mk_fpa_lt(a.ctx(), a, b);
1920 }
1921 else {
1922 // operator is not supported by given arguments.
1923 assert(false);
1924 }
1925 a.check_error();
1926 return expr(a.ctx(), r);
1927 }
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 1928 of file z3++.h.

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

◆ operator< [3/3]

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

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

1929{ 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 1884 of file z3++.h.

1884 {
1885 check_context(a, b);
1886 Z3_ast r = 0;
1887 if (a.is_arith() && b.is_arith()) {
1888 r = Z3_mk_le(a.ctx(), a, b);
1889 }
1890 else if (a.is_bv() && b.is_bv()) {
1891 r = Z3_mk_bvsle(a.ctx(), a, b);
1892 }
1893 else if (a.is_fpa() && b.is_fpa()) {
1894 r = Z3_mk_fpa_leq(a.ctx(), a, b);
1895 }
1896 else {
1897 // operator is not supported by given arguments.
1898 assert(false);
1899 }
1900 a.check_error();
1901 return expr(a.ctx(), r);
1902 }
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 1903 of file z3++.h.

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

◆ operator<= [3/3]

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

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

1904{ 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 1723 of file z3++.h.

1723 {
1724 check_context(a, b);
1725 Z3_ast r = Z3_mk_eq(a.ctx(), a, b);
1726 a.check_error();
1727 return expr(a.ctx(), r);
1728 }
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 1729 of file z3++.h.

1729{ 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 1730 of file z3++.h.

1730{ 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 1931 of file z3++.h.

1931 {
1932 check_context(a, b);
1933 Z3_ast r = 0;
1934 if (a.is_arith() && b.is_arith()) {
1935 r = Z3_mk_gt(a.ctx(), a, b);
1936 }
1937 else if (a.is_bv() && b.is_bv()) {
1938 r = Z3_mk_bvsgt(a.ctx(), a, b);
1939 }
1940 else if (a.is_fpa() && b.is_fpa()) {
1941 r = Z3_mk_fpa_gt(a.ctx(), a, b);
1942 }
1943 else {
1944 // operator is not supported by given arguments.
1945 assert(false);
1946 }
1947 a.check_error();
1948 return expr(a.ctx(), r);
1949 }
Z3_mk_bvsgt
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than.
Z3_mk_fpa_gt
Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than.
Z3_mk_gt
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.

◆ operator> [2/3]

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

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

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

◆ operator> [3/3]

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

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

1951{ 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 1800 of file z3++.h.

1800 {
1801 check_context(a, b);
1802 Z3_ast r = 0;
1803 if (a.is_arith() && b.is_arith()) {
1804 r = Z3_mk_ge(a.ctx(), a, b);
1805 }
1806 else if (a.is_bv() && b.is_bv()) {
1807 r = Z3_mk_bvsge(a.ctx(), a, b);
1808 }
1809 else if (a.is_fpa() && b.is_fpa()) {
1810 r = Z3_mk_fpa_geq(a.ctx(), a, b);
1811 }
1812 else {
1813 // operator is not supported by given arguments.
1814 assert(false);
1815 }
1816 a.check_error();
1817 return expr(a.ctx(), r);
1818 }
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 1906 of file z3++.h.

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

◆ operator>= [3/3]

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

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

1907{ 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 1957 of file z3++.h.

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

◆ operator^ [2/3]

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

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

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

◆ operator^ [3/3]

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

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

1959{ 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 1961 of file z3++.h.

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

◆ operator| [2/3]

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

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

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

◆ operator| [3/3]

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

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

1963{ 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 1721 of file z3++.h.

1721{ 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 1719 of file z3++.h.

1719{ 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 1710 of file z3++.h.

1710 {
1711 check_context(a, b);
1712 assert(a.is_bool() && b.is_bool());
1713 Z3_ast args[2] = { a, b };
1714 Z3_ast r = Z3_mk_or(a.ctx(), 2, args);
1715 a.check_error();
1716 return expr(a.ctx(), r);
1717 }

◆ operator~

expr operator~ ( expr const & a)
friend

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

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

2439 {
2440 assert(es.size() > 0);
2441 context& ctx = es[0u].ctx();
2442 array<Z3_ast> _es(es);
2443 Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
2444 ctx.check_error();
2445 return expr(ctx, r);
2446 }
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 2431 of file z3++.h.

2431 {
2432 assert(es.size() > 0);
2433 context& ctx = es[0u].ctx();
2434 array<Z3_ast> _es(es);
2435 Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
2436 ctx.check_error();
2437 return expr(ctx, r);
2438 }
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 2423 of file z3++.h.

2423 {
2424 assert(es.size() > 0);
2425 context& ctx = es[0u].ctx();
2426 array<Z3_ast> _es(es);
2427 Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
2428 ctx.check_error();
2429 return expr(ctx, r);
2430 }
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 1654 of file z3++.h.

1654{ _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 1655 of file z3++.h.

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

◆ pw [3/3]

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

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

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

◆ range

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

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

4178 {
4179 check_context(lo, hi);
4180 Z3_ast r = Z3_mk_re_range(lo.ctx(), lo, hi);
4181 lo.check_error();
4182 return expr(lo.ctx(), r);
4183 }
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 1674 of file z3++.h.

1674 {
1675 if (a.is_fpa() && b.is_fpa()) {
1676 _Z3_MK_BIN_(a, b, Z3_mk_fpa_rem);
1677 } else {
1678 _Z3_MK_BIN_(a, b, Z3_mk_rem);
1679 }
1680 }
Z3_mk_fpa_rem
Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point remainder.
Z3_mk_rem
Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 rem arg2.

◆ rem [2/3]

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

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

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

◆ rem [3/3]

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

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

1682{ 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 2099 of file z3++.h.

2099 {
2100 assert(t.is_fpa());
2101 Z3_ast r = Z3_mk_fpa_round_to_integral(t.ctx(), t.ctx().fpa_rounding_mode(), t);
2102 t.check_error();
2103 return expr(t.ctx(), r);
2104 }
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 2078 of file z3++.h.

2078 {
2079 assert(t.is_bv());
2080 Z3_ast r = Z3_mk_fpa_to_fp_signed(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2081 t.check_error();
2082 return expr(t.ctx(), r);
2083 }
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 2032 of file z3++.h.

2032 {
2033 check_context(a, rm);
2034 assert(a.is_fpa());
2035 Z3_ast r = Z3_mk_fpa_sqrt(a.ctx(), rm, a);
2036 a.check_error();
2037 return expr(a.ctx(), r);
2038 }
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 2463 of file z3++.h.

2463 {
2464 assert(args.size() > 0);
2465 context& ctx = args[0u].ctx();
2466 array<Z3_ast> _args(args);
2467 Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
2468 ctx.check_error();
2469 return expr(ctx, r);
2470 }

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

2085 {
2086 assert(t.is_bv());
2087 Z3_ast r = Z3_mk_fpa_to_fp_unsigned(t.ctx(), t.ctx().fpa_rounding_mode(), t, s);
2088 t.check_error();
2089 return expr(t.ctx(), r);
2090 }
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 1967 of file z3++.h.

1967{ if (a.is_bool()) return !(a ^ b); check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
Z3_mk_bvxnor
Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise xnor.
Generated on for Z3 by doxygen 1.15.0