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...
|
| expr (context &c) |
|
| expr (context &c, Z3_ast 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 | 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. 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...
|
|
expr | mk_is_inf () const |
| Return Boolean expression to test for whether an FP expression is inf. More...
|
|
expr | mk_is_nan () const |
| Return Boolean expression to test for whether an FP expression is a NaN. More...
|
|
expr | mk_is_normal () const |
| Return Boolean expression to test for whether an FP expression is a normal. More...
|
|
expr | mk_is_subnormal () const |
| Return Boolean expression to test for whether an FP expression is a subnormal. More...
|
|
expr | mk_is_zero () const |
| Return Boolean expression to test for whether an FP expression is a zero. More...
|
|
expr | mk_to_ieee_bv () const |
| Convert this fpa into an IEEE BV. More...
|
|
expr | mk_from_ieee_bv (sort const &s) const |
| Convert this IEEE BV into a fpa. 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...
|
|
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) More...
|
|
unsigned | algebraic_i () const |
| Return i of an algebraic number (root-obj p i) 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 |
|
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() More...
|
|
std::string | get_string () const |
| for a string value expression return an escaped string value. More...
|
|
std::u32string | get_u32string () const |
| for a string value expression return an unespaced string value. 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_vector | args () const |
| Return a vector of all the arguments 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) 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. More...
|
|
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. 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...
|
|
expr | substitute (func_decl_vector const &funs, expr_vector const &bodies) |
| Apply function substitution by macro definitions.
More...
|
|
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 |
|
|
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_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) 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 | 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. More...
|
|
expr | fpa_fp (expr const &sgn, expr const &exp, expr const &sig) |
| Create an expression of FloatingPoint sort from three bit-vector expressions. More...
|
|
expr | fpa_to_sbv (expr const &t, unsigned sz) |
| Conversion of a floating-point term into a signed bit-vector. More...
|
|
expr | fpa_to_ubv (expr const &t, unsigned sz) |
| Conversion of a floating-point term into an unsigned bit-vector. More...
|
|
expr | sbv_to_fpa (expr const &t, sort s) |
| Conversion of a signed bit-vector term into a floating-point. More...
|
|
expr | ubv_to_fpa (expr const &t, sort s) |
| Conversion of an unsigned bit-vector term into a floating-point. More...
|
|
expr | fpa_to_fpa (expr const &t, sort s) |
| Conversion of a floating-point term into another floating-point. More...
|
|
expr | round_fpa_to_closest_integer (expr const &t) |
| Round a floating-point term into its closest integer. More...
|
|
expr | range (expr const &lo, expr const &hi) |
|
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 811 of file z3++.h.