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 () | |
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) | |
context & | ctx () const |
Z3_error_code | check_error () const |
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.
|
inline |
Return i of an algebraic number (root-obj p i)
Definition at line 1046 of file z3++.h.
|
inline |
Retrieve lower and upper bounds for algebraic numerals based on a decimal precision
Definition at line 1019 of file z3++.h.
|
inline |
Return coefficients for p of an algebraic number (root-obj p i)
Definition at line 1036 of file z3++.h.
|
inline |
Definition at line 1026 of file z3++.h.
|
inline |
Return the i-th argument of this application. This method assumes the expression is an application.
Definition at line 1207 of file z3++.h.
Referenced by AstRef::__bool__(), expr::args(), ExprRef::children(), 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 1214 of file z3++.h.
|
inline |
Definition at line 888 of file z3++.h.
Definition at line 1487 of file z3++.h.
|
inline |
|
inline |
Definition at line 1417 of file z3++.h.
|
inline |
Return the 'body' of this quantifier.
Definition at line 1227 of file z3++.h.
Referenced by QuantifierRef::children().
|
inline |
|
inline |
Definition at line 1534 of file z3++.h.
|
inline |
Definition at line 1529 of file z3++.h.
|
inline |
Definition at line 1524 of file z3++.h.
Definition at line 1481 of file z3++.h.
|
inline |
Return the declaration associated with this application. This method assumes the expression is an application.
Definition at line 1192 of file z3++.h.
Referenced by expr::hi(), expr::is_and(), expr::is_distinct(), expr::is_eq(), expr::is_false(), expr::is_implies(), expr::is_ite(), expr::is_not(), expr::is_or(), expr::is_true(), expr::is_xor(), expr::lo(), and ExprRef::params().
|
inline |
Definition at line 1144 of file z3++.h.
Referenced by RatNumRef::denominator_as_long(), and RatNumRef::is_int_value().
|
inline |
Definition at line 1617 of file z3++.h.
sequence and regular expression operations.
Definition at line 1466 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 1011 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 1068 of file z3++.h.
|
inline |
Return int64_t
value of numeral, throw if result cannot fit in int64_t
.
Definition at line 1104 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 1087 of file z3++.h.
|
inline |
Return uint64_t
value of numeral, throw if result cannot fit in uint64_t
.
Definition at line 1121 of file z3++.h.
|
inline |
Return the sort of this expression.
Definition at line 818 of file z3++.h.
Referenced by expr::is_arith(), expr::is_array(), expr::is_bool(), expr::is_bv(), expr::is_datatype(), expr::is_finite_domain(), expr::is_fpa(), expr::is_int(), expr::is_re(), expr::is_real(), expr::is_relation(), expr::is_seq(), and ModelRef::sorts().
|
inline |
for a string value expression return an escaped string value.
Definition at line 1163 of file z3++.h.
|
inline |
for a string value expression return an unespaced string value.
Definition at line 1175 of file z3++.h.
|
inline |
Definition at line 1419 of file z3++.h.
Referenced by expr::extract(), and expr::loop().
|
inline |
|
inline |
Return true if expression is an algebraic number.
Definition at line 928 of file z3++.h.
Referenced by expr::algebraic_i(), expr::algebraic_lower(), expr::algebraic_poly(), expr::algebraic_upper(), and expr::get_decimal_string().
|
inline |
Return true if this expression is an application.
Definition at line 898 of file z3++.h.
Referenced by expr::end(), expr::hi(), expr::is_and(), expr::is_const(), expr::is_distinct(), expr::is_eq(), expr::is_false(), expr::is_implies(), expr::is_ite(), expr::is_not(), expr::is_or(), expr::is_true(), expr::is_xor(), expr::lo(), and expr::operator Z3_app().
|
inline |
Return true if this is an integer or real expression.
Definition at line 835 of file z3++.h.
|
inline |
Return true if this is a Array expression.
Definition at line 843 of file z3++.h.
Referenced by expr::operator[]().
|
inline |
Return true if this is a Boolean expression.
Definition at line 823 of file z3++.h.
Referenced by solver::add(), optimize::add(), optimize::add(), solver::add(), optimize::add(), optimize::add_soft(), and optimize::add_soft().
|
inline |
Return true if this is a Bit-vector expression.
Definition at line 839 of file z3++.h.
Referenced by expr::mk_from_ieee_bv().
|
inline |
Return true if this expression is a constant (i.e., an application with 0 arguments).
Definition at line 902 of file z3++.h.
Referenced by solver::add().
|
inline |
Return true if this is a Datatype expression.
Definition at line 847 of file z3++.h.
|
inline |
Definition at line 1539 of file z3++.h.
|
inline |
|
inline |
|
inline |
Return true if this is a Finite-domain expression.
Definition at line 869 of file z3++.h.
|
inline |
|
inline |
Return true if this is a FloatingPoint expression. .
Definition at line 873 of file z3++.h.
Referenced by expr::mk_is_inf(), expr::mk_is_nan(), expr::mk_is_normal(), expr::mk_is_subnormal(), expr::mk_is_zero(), and expr::mk_to_ieee_bv().
|
inline |
Return true if this is an integer expression.
Definition at line 827 of file z3++.h.
Referenced by IntNumRef::as_long(), and ArithSortRef::subsort().
|
inline |
|
inline |
Return true if this expression is a lambda expression.
Definition at line 919 of file z3++.h.
Referenced by QuantifierRef::__getitem__(), and QuantifierRef::sort().
|
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 880 of file z3++.h.
Referenced by expr::as_binary(), expr::as_double(), expr::denominator(), expr::get_decimal_string(), expr::get_numeral_int64(), expr::get_numeral_uint(), expr::get_numeral_uint64(), and expr::numerator().
|
inline |
Definition at line 887 of file z3++.h.
Referenced by expr::is_numeral().
|
inline |
Definition at line 885 of file z3++.h.
Referenced by expr::is_numeral().
|
inline |
Definition at line 886 of file z3++.h.
Referenced by expr::is_numeral().
|
inline |
Definition at line 883 of file z3++.h.
Referenced by expr::get_numeral_int().
|
inline |
Definition at line 881 of file z3++.h.
Referenced by expr::as_int64(), and expr::get_numeral_int64().
|
inline |
Definition at line 884 of file z3++.h.
Referenced by expr::get_numeral_uint().
|
inline |
Definition at line 882 of file z3++.h.
Referenced by expr::as_uint64(), and expr::get_numeral_uint64().
|
inline |
|
inline |
Return true if this expression is a quantifier.
Definition at line 906 of file z3++.h.
Referenced by expr::body().
|
inline |
Return true if this is a regular expression.
Definition at line 859 of file z3++.h.
|
inline |
Return true if this is a real expression.
Definition at line 831 of file z3++.h.
|
inline |
Return true if this is a Relation expression.
Definition at line 851 of file z3++.h.
|
inline |
Return true if this is a sequence expression.
Definition at line 855 of file z3++.h.
Referenced by expr::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 1156 of file z3++.h.
Referenced by expr::get_string(), and expr::get_u32string().
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Definition at line 1499 of file z3++.h.
Referenced by expr::extract().
|
inline |
Definition at line 1418 of file z3++.h.
Referenced by expr::extract(), expr::loop(), and expr::loop().
|
inline |
create a looping regular expression.
Definition at line 1549 of file z3++.h.
|
inline |
Convert this IEEE BV into a fpa.
Definition at line 998 of file z3++.h.
|
inline |
Return Boolean expression to test for whether an FP expression is inf.
Definition at line 938 of file z3++.h.
|
inline |
Return Boolean expression to test for whether an FP expression is a NaN.
Definition at line 948 of file z3++.h.
|
inline |
Return Boolean expression to test for whether an FP expression is a normal.
Definition at line 958 of file z3++.h.
|
inline |
Return Boolean expression to test for whether an FP expression is a subnormal.
Definition at line 968 of file z3++.h.
|
inline |
Return Boolean expression to test for whether an FP expression is a zero.
Definition at line 978 of file z3++.h.
|
inline |
Convert this fpa into an IEEE BV.
Definition at line 988 of file z3++.h.
Definition at line 1493 of file z3++.h.
Referenced by expr::operator[]().
|
inline |
Return the number of arguments in this application. This method assumes the expression is an application.
Definition at line 1199 of file z3++.h.
Referenced by AstRef::__bool__(), ExprRef::arg(), FuncEntry::arg_value(), expr::args(), FuncEntry::as_list(), ExprRef::children(), expr::end(), and expr::is_const().
|
inline |
Definition at line 1136 of file z3++.h.
Referenced by RatNumRef::numerator_as_long().
index operator defined on arrays and sequences.
Definition at line 1563 of file z3++.h.
|
inline |
|
inline |
Definition at line 1470 of file z3++.h.
|
inline |
|
inline |
|
inline |
Definition at line 1519 of file z3++.h.
|
inline |
|
inline |
|
inline |
Apply substitution. Replace bound variables by expressions.
Definition at line 4191 of file z3++.h.
|
inline |
Apply substitution. Replace src expressions by dst.
Definition at line 4178 of file z3++.h.
|
inline |
Apply function substitution by macro definitions.
Definition at line 4201 of file z3++.h.
|
inline |
Definition at line 1514 of file z3++.h.
|
inline |
Definition at line 1994 of file z3++.h.
|
friend |
|
friend |
bit-vector overflow/underflow checks
Definition at line 2238 of file z3++.h.
Definition at line 2241 of file z3++.h.
Definition at line 2256 of file z3++.h.
Definition at line 2259 of file z3++.h.
Definition at line 1988 of file z3++.h.
Definition at line 1982 of file z3++.h.
Definition at line 2250 of file z3++.h.
Definition at line 2244 of file z3++.h.
Definition at line 2247 of file z3++.h.
Definition at line 2455 of file z3++.h.
|
friend |
Definition at line 2473 of file z3++.h.
|
friend |
FloatingPoint fused multiply-add.
Definition at line 2030 of file z3++.h.
Definition at line 2021 of file z3++.h.
Create an expression of FloatingPoint sort from three bit-vector expressions.
Definition at line 2038 of file z3++.h.
Conversion of a floating-point term into another floating-point.
Definition at line 2074 of file z3++.h.
Conversion of a floating-point term into a signed bit-vector.
Definition at line 2046 of file z3++.h.
Conversion of a floating-point term into an unsigned bit-vector.
Definition at line 2053 of file z3++.h.
Definition at line 1676 of file z3++.h.
Referenced by IntNumRef::as_long(), and ArithSortRef::subsort().
Create the if-then-else expression ite(c, t, e)
Definition at line 2093 of file z3++.h.
Definition at line 1966 of file z3++.h.
Definition at line 1950 of file z3++.h.
|
friend |
|
friend |
|
friend |
Definition at line 1640 of file z3++.h.
Definition at line 1947 of file z3++.h.
Definition at line 1948 of file z3++.h.
Definition at line 1935 of file z3++.h.
Return an expression representing a and b
.
Definition at line 1680 of file z3++.h.
Definition at line 1758 of file z3++.h.
Definition at line 1728 of file z3++.h.
Definition at line 1824 of file z3++.h.
Definition at line 1843 of file z3++.h.
Definition at line 1802 of file z3++.h.
Definition at line 1891 of file z3++.h.
Definition at line 1866 of file z3++.h.
Definition at line 1913 of file z3++.h.
Definition at line 1782 of file z3++.h.
Definition at line 1939 of file z3++.h.
Definition at line 1943 of file z3++.h.
Return an expression representing a or b
.
Definition at line 1692 of file z3++.h.
Definition at line 1656 of file z3++.h.
Round a floating-point term into its closest integer.
Definition at line 2081 of file z3++.h.
Conversion of a signed bit-vector term into a floating-point.
Definition at line 2060 of file z3++.h.
Definition at line 2014 of file z3++.h.
|
friend |
Conversion of an unsigned bit-vector term into a floating-point.
Definition at line 2067 of file z3++.h.
Definition at line 1949 of file z3++.h.