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>
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_fpa () const |
Return true if this is a FloatingPoint 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_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 | 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_forall () const |
Return true if this expression is a universal quantifier. More... | |
bool | is_exists () const |
Return true if this expression is an existential quantifier. More... | |
bool | is_lambda () const |
Return true if this expression is a lambda expression. 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... | |
unsigned | id () const |
retrieve unique identifier for expression. 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_t | get_numeral_int64 () const |
Return int64_t value of numeral, throw if result cannot fit in int64_t . More... | |
uint64_t | get_numeral_uint64 () const |
Return uint64_t value of numeral, throw if result cannot fit in uint64_t . More... | |
Z3_lbool | bool_value () const |
expr | numerator () const |
expr | denominator () const |
std::string | get_escaped_string () const |
for a string value expression return an escaped or unescaped string value. More... | |
std::string | get_string () const |
operator Z3_app () const | |
sort | fpa_rounding_mode () |
Return a RoundingMode sort. More... | |
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... | |
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) |
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 | nth (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 | operator[] (expr const &index) const |
expr | operator[] (expr_vector const &index) 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 |
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 | 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. More... | |
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 More... | |
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 | abs (expr const &a) |
expr | sqrt (expr const &a, expr const &rm) |
expr | operator~ (expr const &a) |
expr | fma (expr const &a, expr const &b, expr const &c) |
FloatingPoint fused multiply-add. More... | |
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 669 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::nth(), 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 949 of file z3++.h.
Referenced by AstRef::__bool__(), and ExprRef::children().
Definition at line 1175 of file z3++.h.
|
inline |
Return the 'body' of this quantifier.
Definition at line 956 of file z3++.h.
Referenced by QuantifierRef::children().
|
inline |
Definition at line 1169 of file z3++.h.
|
inline |
Return the declaration associated with this application. This method assumes the expression is an application.
Definition at line 934 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 890 of file z3++.h.
Referenced by RatNumRef::denominator_as_long(), and RatNumRef::is_int_value().
sequence and regular expression operations.
Definition at line 1154 of file z3++.h.
|
inline |
Definition at line 1140 of file z3++.h.
|
inline |
Return a RoundingMode sort.
Definition at line 920 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 793 of file z3++.h.
|
inline |
for a string value expression return an escaped or unescaped string value.
Definition at line 902 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.
|
inline |
Return int64_t
value of numeral, throw if result cannot fit in int64_t
.
Definition at line 850 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 833 of file z3++.h.
|
inline |
Return uint64_t
value of numeral, throw if result cannot fit in uint64_t
.
Definition at line 867 of file z3++.h.
|
inline |
Return the sort of this expression.
Definition at line 677 of file z3++.h.
Referenced by z3::ashr(), 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(), z3::lshr(), z3::select(), z3::shl(), z3::sle(), z3::slt(), z3::smod(), ModelRef::sorts(), z3::srem(), z3::store(), z3::udiv(), z3::uge(), z3::ugt(), z3::ule(), z3::ult(), and z3::urem().
|
inline |
Definition at line 908 of file z3++.h.
|
inline |
Definition at line 1142 of file z3++.h.
Referenced by expr::extract(), and expr::loop().
|
inline |
|
inline |
Return true if expression is an algebraic number.
Definition at line 780 of file z3++.h.
Referenced by expr::get_decimal_string().
|
inline |
Return true if this expression is an application.
Definition at line 750 of file z3++.h.
Referenced by 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 694 of file z3++.h.
|
inline |
Return true if this is a Array expression.
Definition at line 702 of file z3++.h.
Referenced by expr::operator[]().
|
inline |
Return true if this is a Boolean expression.
Definition at line 682 of file z3++.h.
Referenced by solver::add(), and optimize::add().
|
inline |
Return true if this is a Bit-vector expression.
Definition at line 698 of file z3++.h.
|
inline |
Return true if this expression is a constant (i.e., an application with 0 arguments).
Definition at line 754 of file z3++.h.
Referenced by solver::add().
|
inline |
Return true if this is a Datatype expression.
Definition at line 706 of file z3++.h.
|
inline |
|
inline |
|
inline |
Return true if this is a Finite-domain expression.
Definition at line 728 of file z3++.h.
|
inline |
|
inline |
Return true if this is a FloatingPoint expression. .
Definition at line 732 of file z3++.h.
Referenced by z3::fma(), and expr::fpa_rounding_mode().
|
inline |
Return true if this is an integer expression.
Definition at line 686 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 771 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 739 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 746 of file z3++.h.
Referenced by expr::is_numeral().
|
inline |
Definition at line 744 of file z3++.h.
Referenced by expr::is_numeral().
|
inline |
Definition at line 745 of file z3++.h.
Referenced by expr::is_numeral().
|
inline |
Definition at line 742 of file z3++.h.
Referenced by expr::get_numeral_int().
|
inline |
Definition at line 740 of file z3++.h.
Referenced by expr::get_numeral_int64().
|
inline |
Definition at line 743 of file z3++.h.
Referenced by expr::get_numeral_uint().
|
inline |
Definition at line 741 of file z3++.h.
Referenced by expr::get_numeral_uint64().
|
inline |
|
inline |
Return true if this expression is a quantifier.
Definition at line 758 of file z3++.h.
Referenced by expr::body().
|
inline |
Return true if this is a regular expression.
Definition at line 718 of file z3++.h.
|
inline |
Return true if this is a real expression.
Definition at line 690 of file z3++.h.
|
inline |
Return true if this is a Relation expression.
Definition at line 710 of file z3++.h.
|
inline |
Return true if this is a sequence expression.
Definition at line 714 of file z3++.h.
Referenced by expr::operator[]().
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Definition at line 1187 of file z3++.h.
Referenced by expr::extract().
|
inline |
Definition at line 1141 of file z3++.h.
Referenced by expr::extract(), and expr::loop().
|
inline |
create a looping regular expression.
Definition at line 1207 of file z3++.h.
|
inline |
Definition at line 1181 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 941 of file z3++.h.
Referenced by AstRef::__bool__(), ExprRef::arg(), FuncEntry::arg_value(), FuncEntry::as_list(), ExprRef::children(), and expr::is_const().
|
inline |
Definition at line 882 of file z3++.h.
Referenced by RatNumRef::numerator_as_long().
|
inline |
index operator defined on arrays and sequences.
Definition at line 1221 of file z3++.h.
|
inline |
|
inline |
Definition at line 1158 of file z3++.h.
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Apply substitution. Replace bound variables by expressions.
Definition at line 3501 of file z3++.h.
|
inline |
Apply substitution. Replace src expressions by dst.
Definition at line 3488 of file z3++.h.
|
inline |
Definition at line 1606 of file z3++.h.
|
friend |
|
friend |
bit-vector overflow/underflow checks
Definition at line 1778 of file z3++.h.
Definition at line 1781 of file z3++.h.
Definition at line 1796 of file z3++.h.
Definition at line 1799 of file z3++.h.
Definition at line 1790 of file z3++.h.
Definition at line 1784 of file z3++.h.
Definition at line 1787 of file z3++.h.
Definition at line 2066 of file z3++.h.
|
friend |
Definition at line 2084 of file z3++.h.
|
friend |
Definition at line 2057 of file z3++.h.
FloatingPoint fused multiply-add.
Definition at line 1309 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 1645 of file z3++.h.
Definition at line 1591 of file z3++.h.
Definition at line 1576 of file z3++.h.
|
friend |
Definition at line 2116 of file z3++.h.
|
friend |
Definition at line 2110 of file z3++.h.
Definition at line 1273 of file z3++.h.
Return an expression representing not(a)
.
Definition at line 1307 of file z3++.h.
Definition at line 1347 of file z3++.h.
Return an expression representing a and b
. The C++ Boolean value a
is automatically converted into a Z3 Boolean constant.
Definition at line 1323 of file z3++.h.
Return an expression representing a and b
. The C++ Boolean value b
is automatically converted into a Z3 Boolean constant.
Definition at line 1322 of file z3++.h.
Return an expression representing a and b
.
Definition at line 1313 of file z3++.h.
Definition at line 1387 of file z3++.h.
Definition at line 1357 of file z3++.h.
Definition at line 1450 of file z3++.h.
Definition at line 1469 of file z3++.h.
Definition at line 1428 of file z3++.h.
Definition at line 1517 of file z3++.h.
Definition at line 1492 of file z3++.h.
Definition at line 1539 of file z3++.h.
Definition at line 1411 of file z3++.h.
Return an expression representing a or b
. The C++ Boolean value a
is automatically converted into a Z3 Boolean constant.
Definition at line 1336 of file z3++.h.
Return an expression representing a or b
. The C++ Boolean value b
is automatically converted into a Z3 Boolean constant.
Definition at line 1334 of file z3++.h.
Return an expression representing a or b
.
Definition at line 1325 of file z3++.h.
|
friend |
|
friend |
|
friend |
Definition at line 1289 of file z3++.h.
Definition at line 1622 of file z3++.h.
|
friend |