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...
Public Member Functions | |
expr (context &c) | |
expr (context &c, Z3_ast n) | |
expr (expr const &n) | |
expr & | operator= (expr const &n) |
sort | get_sort () const |
Return the sort of this expression. More... | |
bool | is_bool () const |
Return true if this is a Boolean expression. More... | |
bool | is_int () const |
Return true if this is an integer expression. More... | |
bool | is_real () const |
Return true if this is a real expression. More... | |
bool | is_arith () const |
Return true if this is an integer or real expression. More... | |
bool | is_bv () const |
Return true if this is a Bit-vector expression. More... | |
bool | is_array () const |
Return true if this is a Array expression. More... | |
bool | is_datatype () const |
Return true if this is a Datatype expression. More... | |
bool | is_relation () const |
Return true if this is a Relation expression. More... | |
bool | is_seq () const |
Return true if this is a sequence expression. More... | |
bool | is_re () const |
Return true if this is a regular expression. More... | |
bool | is_finite_domain () const |
Return true if this is a Finite-domain expression. More... | |
bool | is_numeral () const |
Return true if this expression is a numeral. Specialized functions also return representations for the numerals as small integers, 64 bit integers or rational or decimal strings. More... | |
bool | is_numeral_i64 (__int64 &i) const |
bool | is_numeral_u64 (__uint64 &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_app () const |
Return true if this expression is an application. More... | |
bool | is_const () const |
Return true if this expression is a constant (i.e., an application with 0 arguments). More... | |
bool | is_quantifier () const |
Return true if this expression is a quantifier. More... | |
bool | is_var () const |
Return true if this expression is a variable. More... | |
bool | is_algebraic () const |
Return true if expression is an algebraic number. More... | |
bool | is_well_sorted () const |
Return true if this expression is well sorted (aka type correct). More... | |
std::string | get_decimal_string (int precision) const |
Return string representation of numeral or algebraic number This method assumes the expression is numeral or algebraic. More... | |
int | get_numeral_int () const |
Return int value of numeral, throw if result cannot fit in machine int. More... | |
unsigned | get_numeral_uint () const |
Return uint value of numeral, throw if result cannot fit in machine uint. More... | |
__int64 | get_numeral_int64 () const |
Return __int64 value of numeral, throw if result cannot fit in __int64. More... | |
__uint64 | get_numeral_uint64 () const |
Return __uint64 value of numeral, throw if result cannot fit in __uint64. More... | |
operator Z3_app () const | |
func_decl | decl () const |
Return the declaration associated with this application. This method assumes the expression is an application. More... | |
unsigned | num_args () const |
Return the number of arguments in this application. This method assumes the expression is an application. More... | |
expr | arg (unsigned i) const |
Return the i-th argument of this application. This method assumes the expression is an application. More... | |
expr | body () const |
Return the 'body' of this quantifier. More... | |
expr | extract (unsigned hi, unsigned lo) const |
unsigned | lo () const |
unsigned | hi () const |
expr | extract (expr const &offset, expr const &length) const |
sequence and regular expression operations. More... | |
expr | replace (expr const &src, expr const &dst) const |
expr | unit () const |
expr | contains (expr const &s) |
expr | at (expr const &index) const |
expr | length () const |
expr | simplify () const |
Return a simplified version of this expression. More... | |
expr | simplify (params const &p) const |
Return a simplified version of this expression. The parameter p is a set of parameters for the Z3 simplifier. More... | |
expr | substitute (expr_vector const &src, expr_vector const &dst) |
Apply substitution. Replace src expressions by dst. More... | |
expr | substitute (expr_vector const &dst) |
Apply substitution. Replace bound variables by expressions. More... | |
![]() | |
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 |
![]() | |
object (context &c) | |
object (object const &s) | |
context & | ctx () const |
void | check_error () const |
Friends | |
expr | operator! (expr const &a) |
Return an expression representing not(a) . More... | |
expr | operator && (expr const &a, expr const &b) |
Return an expression representing a and b . More... | |
expr | operator && (expr const &a, bool b) |
Return an expression representing a and b . The C++ Boolean value b is automatically converted into a Z3 Boolean constant. More... | |
expr | operator && (bool a, expr const &b) |
Return an expression representing a and b . The C++ Boolean value a is automatically converted into a Z3 Boolean constant. More... | |
expr | operator|| (expr const &a, expr const &b) |
Return an expression representing a or b . More... | |
expr | operator|| (expr const &a, bool b) |
Return an expression representing a or b . The C++ Boolean value b is automatically converted into a Z3 Boolean constant. More... | |
expr | operator|| (bool a, expr const &b) |
Return an expression representing a or b . The C++ Boolean value a is automatically converted into a Z3 Boolean constant. More... | |
expr | implies (expr const &a, expr const &b) |
expr | implies (expr const &a, bool b) |
expr | implies (bool a, expr const &b) |
expr | mk_or (expr_vector const &args) |
expr | mk_and (expr_vector const &args) |
expr | ite (expr const &c, expr const &t, expr const &e) |
Create the if-then-else expression ite(c, t, e) More... | |
expr | distinct (expr_vector const &args) |
expr | concat (expr const &a, expr const &b) |
expr | concat (expr_vector const &args) |
expr | operator== (expr const &a, expr const &b) |
expr | operator== (expr const &a, int b) |
expr | operator== (int a, expr const &b) |
expr | operator!= (expr const &a, expr const &b) |
expr | operator!= (expr const &a, int b) |
expr | operator!= (int a, expr const &b) |
expr | operator+ (expr const &a, expr const &b) |
expr | operator+ (expr const &a, int b) |
expr | operator+ (int a, expr const &b) |
expr | 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) |
Power operator. More... | |
expr | pw (expr const &a, int b) |
expr | pw (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 | 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 | wasoperator (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 | 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) |
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 the i-th argument of this application. This method assumes the expression is an application.
Definition at line 755 of file z3++.h.
Referenced by AstRef::__bool__(), and ExprRef::children().
Definition at line 926 of file z3++.h.
|
inline |
Return the 'body' of this quantifier.
Definition at line 762 of file z3++.h.
Referenced by QuantifierRef::children().
Definition at line 920 of file z3++.h.
|
inline |
|
inline |
Definition at line 896 of file z3++.h.
sequence and regular expression operations.
Definition at line 905 of file z3++.h.
|
inline |
Return string representation of numeral or algebraic number This method assumes the expression is numeral or algebraic.
Definition at line 667 of file z3++.h.
|
inline |
Return int value of numeral, throw if result cannot fit in machine int.
Definition at line 678 of file z3++.h.
|
inline |
Return __int64 value of numeral, throw if result cannot fit in __int64.
Definition at line 707 of file z3++.h.
|
inline |
Return uint value of numeral, throw if result cannot fit in machine uint.
Definition at line 692 of file z3++.h.
|
inline |
Return __uint64 value of numeral, throw if result cannot fit in __uint64.
Definition at line 722 of file z3++.h.
|
inline |
Return the sort of this expression.
Definition at line 570 of file z3++.h.
Referenced by z3::ashr(), z3::concat(), z3::lshr(), z3::operator &(), z3::operator!=(), z3::operator*(), z3::operator+(), z3::operator-(), z3::operator/(), z3::operator<(), z3::operator<=(), z3::operator==(), z3::operator>(), z3::operator>=(), z3::operator^(), z3::operator|(), z3::pw(), z3::select(), z3::shl(), z3::srem(), z3::store(), z3::udiv(), z3::uge(), z3::ugt(), z3::ule(), z3::ult(), and z3::urem().
|
inline |
Definition at line 898 of file z3++.h.
|
inline |
|
inline |
Return true if this expression is an application.
Definition at line 638 of file z3++.h.
|
inline |
Return true if this is an integer or real expression.
Definition at line 587 of file z3++.h.
Referenced by z3::operator!=(), z3::operator*(), z3::operator+(), z3::operator-(), z3::operator/(), z3::operator<(), z3::operator<=(), z3::operator==(), z3::operator>(), z3::operator>=(), and z3::pw().
|
inline |
Return true if this is a Array expression.
Definition at line 595 of file z3++.h.
|
inline |
Return true if this is a Boolean expression.
Definition at line 575 of file z3++.h.
Referenced by solver::add(), optimize::add(), z3::implies(), z3::ite(), z3::operator &&(), z3::operator!(), and z3::operator||().
|
inline |
Return true if this is a Bit-vector expression.
Definition at line 591 of file z3++.h.
Referenced by z3::operator!=(), z3::operator*(), z3::operator+(), z3::operator-(), z3::operator/(), z3::operator<(), z3::operator<=(), z3::operator==(), z3::operator>(), and z3::operator>=().
|
inline |
Return true if this expression is a constant (i.e., an application with 0 arguments).
Definition at line 642 of file z3++.h.
Referenced by solver::add().
|
inline |
Return true if this is a Datatype expression.
Definition at line 599 of file z3++.h.
|
inline |
Return true if this is a Finite-domain expression.
Definition at line 621 of file z3++.h.
|
inline |
Return true if this is an integer expression.
Definition at line 579 of file z3++.h.
|
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 628 of file z3++.h.
|
inline |
Definition at line 633 of file z3++.h.
Referenced by expr::is_numeral().
|
inline |
Definition at line 634 of file z3++.h.
Referenced by expr::is_numeral().
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Return true if this expression is a quantifier.
Definition at line 646 of file z3++.h.
|
inline |
Return true if this is a regular expression.
Definition at line 611 of file z3++.h.
Referenced by z3::operator+().
|
inline |
Return true if this is a real expression.
Definition at line 583 of file z3++.h.
|
inline |
Return true if this is a Relation expression.
Definition at line 603 of file z3++.h.
|
inline |
Return true if this is a sequence expression.
Definition at line 607 of file z3++.h.
Referenced by z3::operator+().
|
inline |
Return true if this expression is a variable.
Definition at line 650 of file z3++.h.
|
inline |
|
inline |
Definition at line 897 of file z3++.h.
|
inline |
Return the number of arguments in this application. This method assumes the expression is an application.
Definition at line 747 of file z3++.h.
Referenced by AstRef::__bool__(), ExprRef::arg(), and ExprRef::children().
|
inline |
Definition at line 732 of file z3++.h.
Definition at line 909 of file z3++.h.
|
inline |
|
inline |
Apply substitution. Replace src expressions by dst.
Definition at line 2535 of file z3++.h.
|
inline |
Definition at line 1478 of file z3++.h.
|
friend |
|
friend |
Definition at line 961 of file z3++.h.
Create the if-then-else expression ite(c, t, e)
Definition at line 1237 of file z3++.h.
|
friend |
|
friend |
Definition at line 1214 of file z3++.h.
Return an expression representing a and b
.
Definition at line 990 of file z3++.h.
Return an expression representing a and b
. The C++ Boolean value b
is automatically converted into a Z3 Boolean constant.
Return an expression representing a and b
. The C++ Boolean value a
is automatically converted into a Z3 Boolean constant.
Return an expression representing not(a)
.
Definition at line 983 of file z3++.h.
Definition at line 1024 of file z3++.h.
Definition at line 1061 of file z3++.h.
Definition at line 1034 of file z3++.h.
Definition at line 1134 of file z3++.h.
Definition at line 1099 of file z3++.h.
Definition at line 1176 of file z3++.h.
Definition at line 1154 of file z3++.h.
Definition at line 1015 of file z3++.h.
Definition at line 1195 of file z3++.h.
Definition at line 1082 of file z3++.h.
Definition at line 1218 of file z3++.h.
Definition at line 1222 of file z3++.h.
Return an expression representing a or b
.
Definition at line 1002 of file z3++.h.
Return an expression representing a or b
. The C++ Boolean value b
is automatically converted into a Z3 Boolean constant.
Return an expression representing a or b
. The C++ Boolean value a
is automatically converted into a Z3 Boolean constant.
Power operator.
Definition at line 972 of file z3++.h.