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>
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 () |
![]() | |
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 |
![]() | |
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 | |
![]() | |
Z3_ast | m_ast |
![]() | |
context * | m_ctx |
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 813 of file z3++.h.
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.
|
inline |
|
inline |
Retrieve lower and upper bounds for algebraic numerals based on a decimal precision
Definition at line 1020 of file z3++.h.
|
inline |
Return coefficients for p of an algebraic number (root-obj p i)
Definition at line 1037 of file z3++.h.
|
inline |
Definition at line 1027 of file z3++.h.
|
inline |
Return the i-th argument of this application. This method assumes the expression is an application.
Definition at line 1208 of file z3++.h.
Referenced by AstRef::__bool__(), args(), and expr::iterator::operator*().
|
inline |
Return a vector of all the arguments of this application. This method assumes the expression is an application.
Definition at line 1215 of file z3++.h.
Referenced by concat, distinct, mk_and, mk_or, mk_xor, operator!=, operator&&, operator*, operator+, operator-, operator||, and sum.
|
inline |
Definition at line 889 of file z3++.h.
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Return the 'body' of this quantifier.
Definition at line 1228 of file z3++.h.
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Return the declaration associated with this application. This method assumes the expression is an application.
Definition at line 1193 of file z3++.h.
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().
|
inline |
Definition at line 1145 of file z3++.h.
sequence and regular expression operations.
Definition at line 1467 of file z3++.h.
|
inline |
|
inline |
Return string representation of numeral or algebraic number This method assumes the expression is numeral or algebraic.
Definition at line 1012 of file z3++.h.
|
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.
Definition at line 1069 of file z3++.h.
|
inline |
Return int64_t
value of numeral, throw if result cannot fit in int64_t
.
Definition at line 1105 of file z3++.h.
|
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.
Definition at line 1088 of file z3++.h.
|
inline |
Return uint64_t
value of numeral, throw if result cannot fit in uint64_t
.
Definition at line 1122 of file z3++.h.
|
inline |
Return the sort of this expression.
Definition at line 819 of file z3++.h.
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::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().
|
inline |
for a string value expression return an escaped string value.
Definition at line 1164 of file z3++.h.
|
inline |
for a string value expression return an unespaced string value.
Definition at line 1176 of file z3++.h.
|
inline |
Definition at line 1420 of file z3++.h.
|
inline |
|
inline |
Return true if expression is an algebraic number.
Definition at line 929 of file z3++.h.
Referenced by algebraic_i(), algebraic_lower(), algebraic_poly(), algebraic_upper(), and get_decimal_string().
|
inline |
|
inline |
Return true if this expression is an application.
Definition at line 899 of file z3++.h.
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().
|
inline |
Return true if this is an integer or real expression.
Definition at line 836 of file z3++.h.
Referenced by max, min, operator!=, operator!=, operator*, operator+, operator-, operator-, operator/, operator<, operator<=, operator==, operator==, operator>, and operator>=.
|
inline |
Return true if this is a Array expression.
Definition at line 844 of file z3++.h.
Referenced by operator[]().
|
inline |
Return true if this is a Boolean expression.
Definition at line 824 of file z3++.h.
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.
|
inline |
Return true if this is a Bit-vector expression.
Definition at line 840 of file z3++.h.
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.
|
inline |
Return true if this expression is a constant (i.e., an application with 0 arguments).
Definition at line 903 of file z3++.h.
Referenced by solver::add().
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Return true if this is a Finite-domain expression.
Definition at line 870 of file z3++.h.
|
inline |
|
inline |
Return true if this is a FloatingPoint expression. .
Definition at line 874 of file z3++.h.
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.
|
inline |
|
inline |
|
inline |
|
inline |
|
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 881 of file z3++.h.
Referenced by as_binary(), as_double(), denominator(), get_decimal_string(), get_numeral_int64(), get_numeral_uint(), get_numeral_uint64(), and numerator().
|
inline |
Definition at line 888 of file z3++.h.
Referenced by is_numeral().
|
inline |
Definition at line 886 of file z3++.h.
Referenced by is_numeral().
|
inline |
Definition at line 887 of file z3++.h.
Referenced by is_numeral().
|
inline |
Definition at line 884 of file z3++.h.
Referenced by get_numeral_int().
|
inline |
Definition at line 882 of file z3++.h.
Referenced by as_int64(), and get_numeral_int64().
|
inline |
Definition at line 885 of file z3++.h.
Referenced by get_numeral_uint().
|
inline |
Definition at line 883 of file z3++.h.
Referenced by as_uint64(), and get_numeral_uint64().
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Return true if this is a sequence expression.
Definition at line 856 of file z3++.h.
Referenced by operator+, and operator[]().
|
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 1157 of file z3++.h.
Referenced by get_string(), and get_u32string().
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Definition at line 1419 of file z3++.h.
|
inline |
create a looping regular expression.
Definition at line 1550 of file z3++.h.
|
inline |
Definition at line 1555 of file z3++.h.
Convert this IEEE BV into a fpa.
Definition at line 999 of file z3++.h.
|
inline |
Return Boolean expression to test for whether an FP expression is inf.
Definition at line 939 of file z3++.h.
|
inline |
Return Boolean expression to test for whether an FP expression is a NaN.
Definition at line 949 of file z3++.h.
|
inline |
Return Boolean expression to test for whether an FP expression is a normal.
Definition at line 959 of file z3++.h.
|
inline |
Return Boolean expression to test for whether an FP expression is a subnormal.
Definition at line 969 of file z3++.h.
|
inline |
Return Boolean expression to test for whether an FP expression is a zero.
Definition at line 979 of file z3++.h.
|
inline |
Convert this fpa into an IEEE BV.
Definition at line 989 of file z3++.h.
Definition at line 1494 of file z3++.h.
Referenced by operator[]().
|
inline |
Return the number of arguments in this application. This method assumes the expression is an application.
Definition at line 1200 of file z3++.h.
Referenced by AstRef::__bool__(), args(), end(), and is_const().
|
inline |
Definition at line 1137 of file z3++.h.
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Apply substitution. Replace bound variables by expressions.
Definition at line 4242 of file z3++.h.
|
inline |
Apply substitution. Replace src expressions by dst.
Definition at line 4229 of file z3++.h.
|
inline |
Apply function substitution by macro definitions.
Definition at line 4252 of file z3++.h.
|
inline |
|
inline |
Definition at line 1995 of file z3++.h.
|
friend |
Definition at line 2430 of file z3++.h.
|
friend |
Definition at line 2422 of file z3++.h.
bit-vector overflow/underflow checks
Definition at line 2239 of file z3++.h.
Definition at line 2242 of file z3++.h.
Definition at line 2257 of file z3++.h.
Definition at line 2260 of file z3++.h.
Definition at line 1989 of file z3++.h.
Definition at line 1983 of file z3++.h.
Definition at line 2251 of file z3++.h.
Definition at line 2245 of file z3++.h.
Definition at line 2248 of file z3++.h.
Definition at line 2456 of file z3++.h.
|
friend |
Definition at line 2474 of file z3++.h.
|
friend |
Definition at line 2447 of file z3++.h.
FloatingPoint fused multiply-add.
Definition at line 2031 of file z3++.h.
Definition at line 2022 of file z3++.h.
Create an expression of FloatingPoint sort from three bit-vector expressions.
Definition at line 2039 of file z3++.h.
Conversion of a floating-point term into another floating-point.
Definition at line 2075 of file z3++.h.
Conversion of a floating-point term into a signed bit-vector.
Definition at line 2047 of file z3++.h.
Conversion of a floating-point term into an unsigned bit-vector.
Definition at line 2054 of file z3++.h.
Definition at line 1967 of file z3++.h.
Definition at line 1951 of file z3++.h.
|
friend |
Definition at line 2534 of file z3++.h.
|
friend |
Definition at line 2528 of file z3++.h.
|
friend |
Definition at line 1641 of file z3++.h.
Definition at line 1948 of file z3++.h.
Definition at line 1949 of file z3++.h.
Definition at line 1717 of file z3++.h.
Definition at line 1936 of file z3++.h.
Return an expression representing a and b
.
Definition at line 1681 of file z3++.h.
Definition at line 1759 of file z3++.h.
Definition at line 1729 of file z3++.h.
Definition at line 1825 of file z3++.h.
Definition at line 1844 of file z3++.h.
Definition at line 1803 of file z3++.h.
Definition at line 1892 of file z3++.h.
Definition at line 1867 of file z3++.h.
Definition at line 1706 of file z3++.h.
Definition at line 1914 of file z3++.h.
Definition at line 1783 of file z3++.h.
Definition at line 1940 of file z3++.h.
Definition at line 1944 of file z3++.h.
Return an expression representing a or b
.
Definition at line 1693 of file z3++.h.
|
friend |
Definition at line 2414 of file z3++.h.
|
friend |
Definition at line 2406 of file z3++.h.
|
friend |
Definition at line 2398 of file z3++.h.
Definition at line 4136 of file z3++.h.
Definition at line 1657 of file z3++.h.
Round a floating-point term into its closest integer.
Definition at line 2082 of file z3++.h.
Conversion of a signed bit-vector term into a floating-point.
Definition at line 2061 of file z3++.h.
Definition at line 2015 of file z3++.h.
|
friend |
Conversion of an unsigned bit-vector term into a floating-point.
Definition at line 2068 of file z3++.h.
Definition at line 1950 of file z3++.h.