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... | |
Z3_lbool | bool_value () const |
expr | numerator () const |
expr | denominator () const |
operator Z3_app () const | |
func_decl | decl () const |
Return the declaration associated with this application. This method assumes the expression is an application. More... | |
unsigned | num_args () const |
Return the number of arguments in this application. This method assumes the expression is an application. More... | |
expr | arg (unsigned i) const |
Return the i-th argument of this application. This method assumes the expression is an application. More... | |
expr | body () const |
Return the 'body' of this quantifier. More... | |
expr | rotate_left (unsigned i) |
expr | rotate_right (unsigned i) |
expr | repeat (unsigned i) |
expr | extract (unsigned hi, unsigned lo) const |
unsigned | lo () const |
unsigned | hi () const |
expr | extract (expr const &offset, expr const &length) const |
sequence and regular expression operations. More... | |
expr | replace (expr const &src, expr const &dst) const |
expr | unit () const |
expr | contains (expr const &s) |
expr | at (expr const &index) const |
expr | length () const |
expr | stoi () const |
expr | itos () const |
expr | loop (unsigned lo) |
create a looping regular expression. More... | |
expr | loop (unsigned lo, unsigned hi) |
expr | 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 |
std::string | to_string () const |
![]() | |
object (context &c) | |
object (object const &s) | |
context & | ctx () const |
Z3_error_code | check_error () const |
Friends | |
expr | operator! (expr const &a) |
Return an expression representing not(a) . More... | |
expr | operator && (expr const &a, expr const &b) |
Return an expression representing a and b . More... | |
expr | operator && (expr const &a, bool b) |
Return an expression representing a and b . The C++ Boolean value b is automatically converted into a Z3 Boolean constant. More... | |
expr | operator && (bool a, expr const &b) |
Return an expression representing a and b . The C++ Boolean value a is automatically converted into a Z3 Boolean constant. More... | |
expr | operator|| (expr const &a, expr const &b) |
Return an expression representing a or b . More... | |
expr | operator|| (expr const &a, bool b) |
Return an expression representing a or b . The C++ Boolean value b is automatically converted into a Z3 Boolean constant. More... | |
expr | operator|| (bool a, expr const &b) |
Return an expression representing a or b . The C++ Boolean value a is automatically converted into a Z3 Boolean constant. More... | |
expr | implies (expr const &a, expr const &b) |
expr | implies (expr const &a, bool b) |
expr | implies (bool a, expr const &b) |
expr | mk_or (expr_vector const &args) |
expr | mk_and (expr_vector const &args) |
expr | ite (expr const &c, expr const &t, expr const &e) |
Create the if-then-else expression ite(c, t, e) More... | |
expr | distinct (expr_vector const &args) |
expr | concat (expr const &a, expr const &b) |
expr | concat (expr_vector const &args) |
expr | operator== (expr const &a, expr const &b) |
expr | operator== (expr const &a, int b) |
expr | operator== (int a, expr const &b) |
expr | operator!= (expr const &a, expr const &b) |
expr | operator!= (expr const &a, int b) |
expr | operator!= (int a, expr const &b) |
expr | operator+ (expr const &a, expr const &b) |
expr | operator+ (expr const &a, int b) |
expr | operator+ (int a, expr const &b) |
expr | sum (expr_vector const &args) |
expr | operator* (expr const &a, expr const &b) |
expr | operator* (expr const &a, int b) |
expr | operator* (int a, expr const &b) |
expr | pw (expr const &a, expr const &b) |
expr | pw (expr const &a, int b) |
expr | pw (int a, expr const &b) |
expr | mod (expr const &a, expr const &b) |
expr | mod (expr const &a, int b) |
expr | mod (int a, expr const &b) |
expr | rem (expr const &a, expr const &b) |
expr | rem (expr const &a, int b) |
expr | rem (int a, expr const &b) |
expr | is_int (expr const &e) |
expr | operator/ (expr const &a, expr const &b) |
expr | operator/ (expr const &a, int b) |
expr | operator/ (int a, expr const &b) |
expr | operator- (expr const &a) |
expr | operator- (expr const &a, expr const &b) |
expr | operator- (expr const &a, int b) |
expr | operator- (int a, expr const &b) |
expr | operator<= (expr const &a, expr const &b) |
expr | operator<= (expr const &a, int b) |
expr | operator<= (int a, expr const &b) |
expr | operator>= (expr const &a, expr const &b) |
expr | operator>= (expr const &a, int b) |
expr | operator>= (int a, expr const &b) |
expr | operator< (expr const &a, expr const &b) |
expr | operator< (expr const &a, int b) |
expr | operator< (int a, expr const &b) |
expr | operator> (expr const &a, expr const &b) |
expr | operator> (expr const &a, int b) |
expr | operator> (int a, expr const &b) |
expr | pble (expr_vector const &es, int const *coeffs, int bound) |
expr | pbge (expr_vector const &es, int const *coeffs, int bound) |
expr | pbeq (expr_vector const &es, int const *coeffs, int bound) |
expr | atmost (expr_vector const &es, unsigned bound) |
expr | atleast (expr_vector const &es, unsigned bound) |
expr | operator & (expr const &a, expr const &b) |
expr | operator & (expr const &a, int b) |
expr | operator & (int a, expr const &b) |
expr | operator^ (expr const &a, expr const &b) |
expr | operator^ (expr const &a, int b) |
expr | operator^ (int a, expr const &b) |
expr | operator| (expr const &a, expr const &b) |
expr | operator| (expr const &a, int b) |
expr | operator| (int a, expr const &b) |
expr | nand (expr const &a, expr const &b) |
expr | nor (expr const &a, expr const &b) |
expr | xnor (expr const &a, expr const &b) |
expr | operator~ (expr const &a) |
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 596 of file z3++.h.
Referenced by expr::arg(), expr::at(), expr::body(), expr::contains(), expr::denominator(), expr::extract(), expr::itos(), expr::length(), expr::loop(), expr::numerator(), expr::repeat(), expr::replace(), expr::rotate_left(), expr::rotate_right(), expr::simplify(), expr::stoi(), expr::substitute(), and expr::unit().
|
inline |
Return the i-th argument of this application. This method assumes the expression is an application.
Definition at line 822 of file z3++.h.
Referenced by AstRef::__bool__().
Definition at line 1016 of file z3++.h.
|
inline |
Return the 'body' of this quantifier.
Definition at line 829 of file z3++.h.
|
inline |
Definition at line 1010 of file z3++.h.
|
inline |
Return the declaration associated with this application. This method assumes the expression is an application.
Definition at line 807 of file z3++.h.
Referenced by expr::hi(), and expr::lo().
|
inline |
Definition at line 792 of file z3++.h.
|
inline |
Definition at line 986 of file z3++.h.
sequence and regular expression operations.
Definition at line 995 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 701 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 the is_numeral_i function.
Definition at line 716 of file z3++.h.
|
inline |
Return __int64 value of numeral, throw if result cannot fit in __int64.
Definition at line 752 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 the is_numeral_u function.
Definition at line 735 of file z3++.h.
|
inline |
Return __uint64 value of numeral, throw if result cannot fit in __uint64.
Definition at line 769 of file z3++.h.
|
inline |
Return the sort of this expression.
Definition at line 604 of file z3++.h.
Referenced by z3::ashr(), z3::concat(), expr::is_arith(), expr::is_array(), expr::is_bool(), expr::is_bv(), expr::is_datatype(), expr::is_finite_domain(), expr::is_int(), expr::is_re(), expr::is_real(), expr::is_relation(), expr::is_seq(), z3::lshr(), z3::mod(), 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::rem(), z3::select(), z3::shl(), z3::smod(), z3::srem(), z3::store(), z3::udiv(), z3::uge(), z3::ugt(), z3::ule(), z3::ult(), and z3::urem().
|
inline |
Definition at line 988 of file z3++.h.
Referenced by expr::extract(), and expr::loop().
|
inline |
Return true if expression is an algebraic number.
Definition at line 688 of file z3++.h.
Referenced by expr::get_decimal_string().
|
inline |
Return true if this expression is an application.
Definition at line 672 of file z3++.h.
Referenced by expr::hi(), expr::is_const(), expr::lo(), and expr::operator Z3_app().
|
inline |
Return true if this is an integer or real expression.
Definition at line 621 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 is a Array expression.
Definition at line 629 of file z3++.h.
|
inline |
Return true if this is a Boolean expression.
Definition at line 609 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 625 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 676 of file z3++.h.
Referenced by solver::add().
|
inline |
Return true if this is a Datatype expression.
Definition at line 633 of file z3++.h.
|
inline |
Return true if this is a Finite-domain expression.
Definition at line 655 of file z3++.h.
|
inline |
Return true if this is an integer expression.
Definition at line 613 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 662 of file z3++.h.
Referenced by 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 667 of file z3++.h.
Referenced by expr::is_numeral().
|
inline |
Definition at line 668 of file z3++.h.
Referenced by expr::is_numeral().
|
inline |
Definition at line 665 of file z3++.h.
Referenced by expr::get_numeral_int().
|
inline |
Definition at line 663 of file z3++.h.
Referenced by expr::get_numeral_int64().
|
inline |
Definition at line 666 of file z3++.h.
Referenced by expr::get_numeral_uint().
|
inline |
Definition at line 664 of file z3++.h.
Referenced by expr::get_numeral_uint64().
|
inline |
Return true if this expression is a quantifier.
Definition at line 680 of file z3++.h.
Referenced by expr::body().
|
inline |
Return true if this is a regular expression.
Definition at line 645 of file z3++.h.
Referenced by z3::operator+().
|
inline |
Return true if this is a real expression.
Definition at line 617 of file z3++.h.
|
inline |
Return true if this is a Relation expression.
Definition at line 637 of file z3++.h.
|
inline |
Return true if this is a sequence expression.
Definition at line 641 of file z3++.h.
Referenced by z3::operator+().
|
inline |
Return true if this expression is a variable.
Definition at line 684 of file z3++.h.
|
inline |
|
inline |
Definition at line 1022 of file z3++.h.
Referenced by expr::extract().
|
inline |
Definition at line 987 of file z3++.h.
Referenced by expr::extract(), and expr::loop().
|
inline |
|
inline |
|
inline |
Return the number of arguments in this application. This method assumes the expression is an application.
Definition at line 814 of file z3++.h.
Referenced by AstRef::__bool__(), and expr::is_const().
|
inline |
Definition at line 784 of file z3++.h.
|
inline |
Definition at line 799 of file z3++.h.
|
inline |
Definition at line 983 of file z3++.h.
Definition at line 999 of file z3++.h.
|
inline |
Definition at line 981 of file z3++.h.
|
inline |
Definition at line 982 of file z3++.h.
|
inline |
|
inline |
Apply substitution. Replace src expressions by dst.
Definition at line 2893 of file z3++.h.
|
inline |
|
friend |
Definition at line 1667 of file z3++.h.
|
friend |
Definition at line 1659 of file z3++.h.
Definition at line 1693 of file z3++.h.
|
friend |
Definition at line 1711 of file z3++.h.
|
friend |
Definition at line 1684 of file z3++.h.
Create the if-then-else expression ite(c, t, e)
Definition at line 1366 of file z3++.h.
|
friend |
|
friend |
Definition at line 1352 of file z3++.h.
Definition at line 1353 of file z3++.h.
Definition at line 1340 of file z3++.h.
Return an expression representing a and b
.
Definition at line 1116 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 1110 of file z3++.h.
Definition at line 1150 of file z3++.h.
Definition at line 1187 of file z3++.h.
Definition at line 1160 of file z3++.h.
Definition at line 1260 of file z3++.h.
Definition at line 1225 of file z3++.h.
Definition at line 1302 of file z3++.h.
Definition at line 1280 of file z3++.h.
Definition at line 1141 of file z3++.h.
Definition at line 1321 of file z3++.h.
Definition at line 1208 of file z3++.h.
Definition at line 1344 of file z3++.h.
Definition at line 1348 of file z3++.h.
Return an expression representing a or b
.
Definition at line 1128 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.
|
friend |
Definition at line 1651 of file z3++.h.
|
friend |
Definition at line 1643 of file z3++.h.
|
friend |
Definition at line 1635 of file z3++.h.
Definition at line 2813 of file z3++.h.
|
friend |
Definition at line 1675 of file z3++.h.
Definition at line 1354 of file z3++.h.