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 |
| |
| uint64_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_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 |
| |
| 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) const |
| |
| 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 (ast &&s) noexcept |
| |
| | ~ast () |
| |
| | operator Z3_ast () const |
| |
| | operator bool () const |
| |
| ast & | operator= (ast const &s) |
| |
| ast & | operator= (ast &&s) noexcept |
| |
| 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 |
| |
|
| 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 | 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 757 of file z3++.h.
◆ expr() [1/2]
Definition at line 759 of file z3++.h.
Referenced by expr::algebraic_lower(), expr::algebraic_upper(), expr::arg(), expr::at(), expr::body(), expr::contains(), expr::denominator(), expr::extract(), expr::itos(), expr::length(), expr::loop(), expr::mk_from_ieee_bv(), expr::mk_is_inf(), expr::mk_is_nan(), expr::mk_is_normal(), expr::mk_is_subnormal(), expr::mk_is_zero(), expr::mk_to_ieee_bv(), expr::nth(), expr::numerator(), expr::repeat(), expr::replace(), expr::rotate_left(), expr::rotate_right(), expr::simplify(), expr::stoi(), expr::substitute(), and expr::unit().
◆ expr() [2/2]
Definition at line 760 of file z3++.h.
760 :
ast(c,
reinterpret_cast<Z3_ast
>(n)) {}
◆ algebraic_i()
| unsigned algebraic_i |
( |
| ) |
const |
|
inline |
Return i of an algebraic number (root-obj p i)
Definition at line 993 of file z3++.h.
◆ algebraic_lower()
| expr algebraic_lower |
( |
unsigned |
precision | ) |
const |
|
inline |
Retrieve lower and upper bounds for algebraic numerals based on a decimal precision
Definition at line 966 of file z3++.h.
◆ algebraic_poly()
Return coefficients for p of an algebraic number (root-obj p i)
Definition at line 983 of file z3++.h.
◆ algebraic_upper()
| expr algebraic_upper |
( |
unsigned |
precision | ) |
const |
|
inline |
◆ arg()
| expr arg |
( |
unsigned |
i | ) |
const |
|
inline |
◆ as_binary()
| bool as_binary |
( |
std::string & |
s | ) |
const |
|
inline |
◆ as_double()
| double as_double |
( |
| ) |
const |
|
inline |
◆ as_int64()
| uint64_t as_int64 |
( |
| ) |
const |
|
inline |
◆ as_uint64()
| uint64_t as_uint64 |
( |
| ) |
const |
|
inline |
◆ at()
◆ body()
◆ bool_value()
◆ contains()
◆ decl()
Return the declaration associated with this application. This method assumes the expression is an application.
- Precondition
- is_app()
Definition at line 1133 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(), and expr::lo().
◆ denominator()
| expr denominator |
( |
| ) |
const |
|
inline |
◆ extract() [1/2]
| expr extract |
( |
expr const & |
offset, |
|
|
expr const & |
length |
|
) |
| const |
|
inline |
sequence and regular expression operations.
- is overloaded as sequence concatenation and regular expression union. concat is overloaded to handle sequences and regular expressions
Definition at line 1392 of file z3++.h.
◆ extract() [2/2]
| expr extract |
( |
unsigned |
hi, |
|
|
unsigned |
lo |
|
) |
| const |
|
inline |
◆ get_decimal_string()
| std::string get_decimal_string |
( |
int |
precision | ) |
const |
|
inline |
Return string representation of numeral or algebraic number This method assumes the expression is numeral or algebraic.
- Precondition
- is_numeral() || is_algebraic()
Definition at line 958 of file z3++.h.
◆ get_escaped_string()
| std::string get_escaped_string |
( |
| ) |
const |
|
inline |
for a string value expression return an escaped or unescaped string value.
- Precondition
- expression is for a string value.
Definition at line 1110 of file z3++.h.
1114 return std::string(s);
◆ get_numeral_int()
| int get_numeral_int |
( |
| ) |
const |
|
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.
- Precondition
- is_numeral()
Definition at line 1015 of file z3++.h.
1018 assert(
ctx().enable_exceptions());
1019 if (!
ctx().enable_exceptions())
return 0;
1020 Z3_THROW(exception(
"numeral does not fit in machine int"));
◆ get_numeral_int64()
| int64_t get_numeral_int64 |
( |
| ) |
const |
|
inline |
Return int64_t value of numeral, throw if result cannot fit in int64_t.
- Precondition
- is_numeral()
Definition at line 1051 of file z3++.h.
1055 assert(
ctx().enable_exceptions());
1056 if (!
ctx().enable_exceptions())
return 0;
1057 Z3_THROW(exception(
"numeral does not fit in machine int64_t"));
◆ get_numeral_uint()
| unsigned get_numeral_uint |
( |
| ) |
const |
|
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.
- Precondition
- is_numeral()
Definition at line 1034 of file z3++.h.
1036 unsigned result = 0;
1038 assert(
ctx().enable_exceptions());
1039 if (!
ctx().enable_exceptions())
return 0;
1040 Z3_THROW(exception(
"numeral does not fit in machine uint"));
◆ get_numeral_uint64()
| uint64_t get_numeral_uint64 |
( |
| ) |
const |
|
inline |
Return uint64_t value of numeral, throw if result cannot fit in uint64_t.
- Precondition
- is_numeral()
Definition at line 1068 of file z3++.h.
1070 uint64_t result = 0;
1072 assert(
ctx().enable_exceptions());
1073 if (!
ctx().enable_exceptions())
return 0;
1074 Z3_THROW(exception(
"numeral does not fit in machine uint64_t"));
◆ get_sort()
Return the sort of this expression.
Definition at line 765 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_fpa(), 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::sge(), z3::sgt(), z3::shl(), z3::sle(), z3::slt(), z3::smod(), z3::srem(), z3::store(), z3::udiv(), z3::uge(), z3::ugt(), z3::ule(), z3::ult(), and z3::urem().
◆ get_string()
| std::string get_string |
( |
| ) |
const |
|
inline |
Definition at line 1117 of file z3++.h.
1122 return std::string(s, n);
◆ hi()
◆ id()
retrieve unique identifier for expression.
Definition at line 1003 of file z3++.h.
◆ is_algebraic()
| bool is_algebraic |
( |
| ) |
const |
|
inline |
◆ is_and()
◆ is_app()
Return true if this expression is an application.
Definition at line 845 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().
◆ is_arith()
Return true if this is an integer or real expression.
Definition at line 782 of file z3++.h.
Referenced by z3::max(), z3::min(), z3::operator!=(), z3::operator*(), z3::operator+(), z3::operator-(), z3::operator/(), z3::operator<(), z3::operator<=(), z3::operator==(), z3::operator>(), and z3::operator>=().
◆ is_array()
◆ is_bool()
Return true if this is a Boolean expression.
Definition at line 770 of file z3++.h.
Referenced by solver::add(), optimize::add(), optimize::add_soft(), z3::implies(), z3::ite(), z3::nand(), z3::nor(), z3::operator!(), z3::operator&(), z3::operator&&(), z3::operator^(), z3::operator|(), z3::operator||(), and z3::xnor().
◆ is_bv()
Return true if this is a Bit-vector expression.
Definition at line 786 of file z3++.h.
Referenced by z3::bvredand(), z3::bvredor(), z3::fpa_fp(), z3::max(), z3::min(), expr::mk_from_ieee_bv(), z3::mod(), z3::operator!=(), z3::operator*(), z3::operator+(), z3::operator-(), z3::operator/(), z3::operator<(), z3::operator<=(), z3::operator==(), z3::operator>(), z3::operator>=(), z3::sbv_to_fpa(), and z3::ubv_to_fpa().
◆ is_const()
Return true if this expression is a constant (i.e., an application with 0 arguments).
Definition at line 849 of file z3++.h.
Referenced by solver::add().
◆ is_datatype()
| bool is_datatype |
( |
| ) |
const |
|
inline |
Return true if this is a Datatype expression.
Definition at line 794 of file z3++.h.
◆ is_distinct()
| bool is_distinct |
( |
| ) |
const |
|
inline |
◆ is_eq()
◆ is_exists()
Return true if this expression is an existential quantifier.
Definition at line 862 of file z3++.h.
◆ is_false()
◆ is_finite_domain()
| bool is_finite_domain |
( |
| ) |
const |
|
inline |
Return true if this is a Finite-domain expression.
Definition at line 816 of file z3++.h.
◆ is_forall()
Return true if this expression is a universal quantifier.
Definition at line 858 of file z3++.h.
◆ is_fpa()
Return true if this is a FloatingPoint expression. .
Definition at line 820 of file z3++.h.
Referenced by z3::fma(), z3::fp_eq(), z3::fpa_to_fpa(), z3::fpa_to_sbv(), z3::fpa_to_ubv(), z3::max(), z3::min(), expr::mk_is_inf(), expr::mk_is_nan(), expr::mk_is_normal(), expr::mk_is_subnormal(), expr::mk_is_zero(), expr::mk_to_ieee_bv(), z3::operator!=(), z3::operator*(), z3::operator+(), z3::operator-(), z3::operator/(), z3::operator<(), z3::operator<=(), z3::operator==(), z3::operator>(), z3::operator>=(), z3::rem(), z3::round_fpa_to_closest_integer(), and z3::sqrt().
◆ is_implies()
| bool is_implies |
( |
| ) |
const |
|
inline |
◆ is_int()
Return true if this is an integer expression.
Definition at line 774 of file z3++.h.
Referenced by z3::abs().
◆ is_ite()
◆ is_lambda()
Return true if this expression is a lambda expression.
Definition at line 866 of file z3++.h.
◆ is_not()
◆ is_numeral() [1/4]
| bool is_numeral |
( |
| ) |
const |
|
inline |
◆ is_numeral() [2/4]
| bool is_numeral |
( |
double & |
d | ) |
const |
|
inline |
◆ is_numeral() [3/4]
| bool is_numeral |
( |
std::string & |
s | ) |
const |
|
inline |
◆ is_numeral() [4/4]
| bool is_numeral |
( |
std::string & |
s, |
|
|
unsigned |
precision |
|
) |
| const |
|
inline |
◆ is_numeral_i()
| bool is_numeral_i |
( |
int & |
i | ) |
const |
|
inline |
◆ is_numeral_i64()
| bool is_numeral_i64 |
( |
int64_t & |
i | ) |
const |
|
inline |
◆ is_numeral_u()
| bool is_numeral_u |
( |
unsigned & |
i | ) |
const |
|
inline |
◆ is_numeral_u64()
| bool is_numeral_u64 |
( |
uint64_t & |
i | ) |
const |
|
inline |
◆ is_or()
◆ is_quantifier()
| bool is_quantifier |
( |
| ) |
const |
|
inline |
Return true if this expression is a quantifier.
Definition at line 853 of file z3++.h.
Referenced by expr::body().
◆ is_re()
◆ is_real()
Return true if this is a real expression.
Definition at line 778 of file z3++.h.
Referenced by z3::abs().
◆ is_relation()
| bool is_relation |
( |
| ) |
const |
|
inline |
Return true if this is a Relation expression.
Definition at line 798 of file z3++.h.
◆ is_seq()
◆ is_string_value()
| bool is_string_value |
( |
| ) |
const |
|
inline |
◆ is_true()
◆ is_var()
Return true if this expression is a variable.
Definition at line 871 of file z3++.h.
◆ is_well_sorted()
| bool is_well_sorted |
( |
| ) |
const |
|
inline |
Return true if this expression is well sorted (aka type correct).
Definition at line 880 of file z3++.h.
◆ is_xor()
◆ itos()
◆ length()
◆ lo()
◆ loop() [1/2]
create a looping regular expression.
Definition at line 1445 of file z3++.h.
◆ loop() [2/2]
| expr loop |
( |
unsigned |
lo, |
|
|
unsigned |
hi |
|
) |
| |
|
inline |
◆ mk_from_ieee_bv()
| expr mk_from_ieee_bv |
( |
sort const & |
s | ) |
const |
|
inline |
Convert this IEEE BV into a fpa.
Definition at line 945 of file z3++.h.
◆ mk_is_inf()
Return Boolean expression to test for whether an FP expression is inf.
Definition at line 885 of file z3++.h.
◆ mk_is_nan()
Return Boolean expression to test for whether an FP expression is a NaN.
Definition at line 895 of file z3++.h.
◆ mk_is_normal()
| expr mk_is_normal |
( |
| ) |
const |
|
inline |
Return Boolean expression to test for whether an FP expression is a normal.
Definition at line 905 of file z3++.h.
◆ mk_is_subnormal()
| expr mk_is_subnormal |
( |
| ) |
const |
|
inline |
Return Boolean expression to test for whether an FP expression is a subnormal.
Definition at line 915 of file z3++.h.
◆ mk_is_zero()
| expr mk_is_zero |
( |
| ) |
const |
|
inline |
Return Boolean expression to test for whether an FP expression is a zero.
Definition at line 925 of file z3++.h.
◆ mk_to_ieee_bv()
| expr mk_to_ieee_bv |
( |
| ) |
const |
|
inline |
Convert this fpa into an IEEE BV.
Definition at line 935 of file z3++.h.
◆ nth()
◆ num_args()
| unsigned num_args |
( |
| ) |
const |
|
inline |
◆ numerator()
◆ operator Z3_app()
| operator Z3_app |
( |
| ) |
const |
|
inline |
Definition at line 1125 of file z3++.h.
1125 { assert(
is_app());
return reinterpret_cast<Z3_app
>(
m_ast); }
◆ operator[]() [1/2]
| expr operator[] |
( |
expr const & |
index | ) |
const |
|
inline |
index operator defined on arrays and sequences.
Definition at line 1459 of file z3++.h.
1462 return select(*
this, index);
◆ operator[]() [2/2]
◆ repeat()
| expr repeat |
( |
unsigned |
i | ) |
|
|
inline |
◆ replace()
◆ rotate_left()
| expr rotate_left |
( |
unsigned |
i | ) |
|
|
inline |
◆ rotate_right()
| expr rotate_right |
( |
unsigned |
i | ) |
|
|
inline |
◆ simplify() [1/2]
Return a simplified version of this expression.
Definition at line 1474 of file z3++.h.
◆ simplify() [2/2]
Return a simplified version of this expression. The parameter p is a set of parameters for the Z3 simplifier.
Definition at line 1478 of file z3++.h.
◆ stoi()
◆ substitute() [1/2]
Apply substitution. Replace bound variables by expressions.
Definition at line 3795 of file z3++.h.
3796 array<Z3_ast> _dst(dst.size());
3797 for (
unsigned i = 0; i < dst.size(); ++i) {
◆ substitute() [2/2]
Apply substitution. Replace src expressions by dst.
Definition at line 3782 of file z3++.h.
3783 assert(src.size() == dst.size());
3784 array<Z3_ast> _src(src.size());
3785 array<Z3_ast> _dst(dst.size());
3786 for (
unsigned i = 0; i < src.size(); ++i) {
◆ unit()
◆ abs
Definition at line 1863 of file z3++.h.
1866 expr zero = a.ctx().int_val(0);
1869 else if (a.is_real()) {
1870 expr zero = a.ctx().real_val(0);
1877 return expr(a.ctx(), r);
◆ atleast
Definition at line 2294 of file z3++.h.
2295 assert(es.size() > 0);
2296 context&
ctx = es[0].ctx();
2297 array<Z3_ast> _es(es);
◆ atmost
Definition at line 2286 of file z3++.h.
2287 assert(es.size() > 0);
2288 context&
ctx = es[0].ctx();
2289 array<Z3_ast> _es(es);
◆ bv2int
| expr bv2int |
( |
expr const & |
a, |
|
|
bool |
is_signed |
|
) |
| |
|
friend |
bit-vector and integer conversions.
Definition at line 2097 of file z3++.h.
2097 { Z3_ast r =
Z3_mk_bv2int(a.ctx(), a, is_signed); a.check_error();
return expr(a.ctx(), r); }
◆ bvadd_no_overflow
| expr bvadd_no_overflow |
( |
expr const & |
a, |
|
|
expr const & |
b, |
|
|
bool |
is_signed |
|
) |
| |
|
friend |
bit-vector overflow/underflow checks
Definition at line 2103 of file z3++.h.
◆ bvadd_no_underflow
◆ bvmul_no_overflow
| expr bvmul_no_overflow |
( |
expr const & |
a, |
|
|
expr const & |
b, |
|
|
bool |
is_signed |
|
) |
| |
|
friend |
◆ bvmul_no_underflow
◆ bvneg_no_overflow
| expr bvneg_no_overflow |
( |
expr const & |
a | ) |
|
|
friend |
◆ bvredand
◆ bvredor
◆ bvsdiv_no_overflow
◆ bvsub_no_overflow
◆ bvsub_no_underflow
| expr bvsub_no_underflow |
( |
expr const & |
a, |
|
|
expr const & |
b, |
|
|
bool |
is_signed |
|
) |
| |
|
friend |
◆ concat [1/2]
Definition at line 2320 of file z3++.h.
2324 Z3_ast _args[2] = { a, b };
2328 Z3_ast _args[2] = { a, b };
2334 a.ctx().check_error();
2335 return expr(a.ctx(), r);
◆ concat [2/2]
Definition at line 2338 of file z3++.h.
2340 assert(args.size() > 0);
2341 if (args.size() == 1) {
2344 context&
ctx = args[0].ctx();
2345 array<Z3_ast> _args(args);
2353 r = _args[args.size()-1];
2354 for (
unsigned i = args.size()-1; i > 0; ) {
◆ distinct
Definition at line 2311 of file z3++.h.
2312 assert(args.size() > 0);
2313 context&
ctx = args[0].ctx();
2314 array<Z3_ast> _args(args);
◆ fma
FloatingPoint fused multiply-add.
Definition at line 1895 of file z3++.h.
1897 assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
1900 return expr(a.ctx(), r);
◆ fp_eq
◆ fpa_fp
Create an expression of FloatingPoint sort from three bit-vector expressions.
Definition at line 1903 of file z3++.h.
1905 assert(sgn.is_bv() && exp.is_bv() && sig.is_bv());
1908 return expr(sgn.ctx(), r);
◆ fpa_to_fpa
Conversion of a floating-point term into another floating-point.
Definition at line 1939 of file z3++.h.
1943 return expr(t.ctx(), r);
◆ fpa_to_sbv
| expr fpa_to_sbv |
( |
expr const & |
t, |
|
|
unsigned |
sz |
|
) |
| |
|
friend |
Conversion of a floating-point term into a signed bit-vector.
Definition at line 1911 of file z3++.h.
1915 return expr(t.ctx(), r);
◆ fpa_to_ubv
| expr fpa_to_ubv |
( |
expr const & |
t, |
|
|
unsigned |
sz |
|
) |
| |
|
friend |
Conversion of a floating-point term into an unsigned bit-vector.
Definition at line 1918 of file z3++.h.
1922 return expr(t.ctx(), r);
◆ implies [1/3]
Definition at line 1504 of file z3++.h.
1504 {
return implies(b.ctx().bool_val(a), b); }
◆ implies [2/3]
Definition at line 1503 of file z3++.h.
1503 {
return implies(a, a.ctx().bool_val(b)); }
◆ implies [3/3]
Definition at line 1499 of file z3++.h.
1500 assert(a.is_bool() && b.is_bool());
◆ int2bv
| expr int2bv |
( |
unsigned |
n, |
|
|
expr const & |
a |
|
) |
| |
|
friend |
Definition at line 2098 of file z3++.h.
2098 { Z3_ast r =
Z3_mk_int2bv(a.ctx(), n, a); a.check_error();
return expr(a.ctx(), r); }
◆ is_int
◆ ite
Create the if-then-else expression ite(c, t, e)
- Precondition
- c.is_bool()
Definition at line 1958 of file z3++.h.
1960 assert(c.is_bool());
1963 return expr(c.ctx(), r);
◆ max
Definition at line 1836 of file z3++.h.
1842 else if (a.is_bv()) {
1849 return expr(a.ctx(), r);
◆ min
Definition at line 1821 of file z3++.h.
1827 else if (a.is_bv()) {
1834 return expr(a.ctx(), r);
◆ mk_and
Definition at line 2370 of file z3++.h.
2371 array<Z3_ast> _args(args);
2372 Z3_ast r =
Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2374 return expr(args.ctx(), r);
◆ mk_or
Definition at line 2364 of file z3++.h.
2365 array<Z3_ast> _args(args);
2366 Z3_ast r =
Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2368 return expr(args.ctx(), r);
◆ mod [1/3]
◆ mod [2/3]
Definition at line 1519 of file z3++.h.
1519 {
return mod(a, a.ctx().num_val(b, a.get_sort())); }
◆ mod [3/3]
Definition at line 1520 of file z3++.h.
1520 {
return mod(b.ctx().num_val(a, b.get_sort()), b); }
◆ nand
◆ nor
◆ operator!
Return an expression representing not(a).
- Precondition
- a.is_bool()
Definition at line 1545 of file z3++.h.
◆ operator!= [1/3]
Definition at line 1587 of file z3++.h.
1589 Z3_ast args[2] = { a, b };
1592 return expr(a.ctx(), r);
◆ operator!= [2/3]
Definition at line 1594 of file z3++.h.
1594 { assert(a.is_arith() || a.is_bv() || a.is_fpa());
return a != a.ctx().num_val(b, a.get_sort()); }
◆ operator!= [3/3]
Definition at line 1595 of file z3++.h.
1595 { assert(b.is_arith() || b.is_bv() || b.is_fpa());
return b.ctx().num_val(a, b.get_sort()) != b; }
◆ operator& [1/3]
◆ operator& [2/3]
| expr operator& |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1807 of file z3++.h.
1807 {
return a & a.ctx().num_val(b, a.get_sort()); }
◆ operator& [3/3]
| expr operator& |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1808 of file z3++.h.
1808 {
return b.ctx().num_val(a, b.get_sort()) & b; }
◆ operator&& [1/3]
| expr operator&& |
( |
bool |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Return an expression representing a and b. The C++ Boolean value a is automatically converted into a Z3 Boolean constant.
- Precondition
- b.is_bool()
Definition at line 1561 of file z3++.h.
1561 {
return b.ctx().bool_val(a) && b; }
◆ operator&& [2/3]
| expr operator&& |
( |
expr const & |
a, |
|
|
bool |
b |
|
) |
| |
|
friend |
Return an expression representing a and b. The C++ Boolean value b is automatically converted into a Z3 Boolean constant.
- Precondition
- a.is_bool()
Definition at line 1560 of file z3++.h.
1560 {
return a && a.ctx().bool_val(b); }
◆ operator&& [3/3]
Return an expression representing a and b.
- Precondition
- a.is_bool()
-
b.is_bool()
Definition at line 1551 of file z3++.h.
1553 assert(a.is_bool() && b.is_bool());
1554 Z3_ast args[2] = { a, b };
1557 return expr(a.ctx(), r);
◆ operator* [1/3]
Definition at line 1629 of file z3++.h.
1632 if (a.is_arith() && b.is_arith()) {
1633 Z3_ast args[2] = { a, b };
1636 else if (a.is_bv() && b.is_bv()) {
1639 else if (a.is_fpa() && b.is_fpa()) {
1640 r =
Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1647 return expr(a.ctx(), r);
◆ operator* [2/3]
| expr operator* |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1649 of file z3++.h.
1649 {
return a * a.ctx().num_val(b, a.get_sort()); }
◆ operator* [3/3]
| expr operator* |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1650 of file z3++.h.
1650 {
return b.ctx().num_val(a, b.get_sort()) * b; }
◆ operator+ [1/3]
Definition at line 1599 of file z3++.h.
1602 if (a.is_arith() && b.is_arith()) {
1603 Z3_ast args[2] = { a, b };
1606 else if (a.is_bv() && b.is_bv()) {
1609 else if (a.is_seq() && b.is_seq()) {
1612 else if (a.is_re() && b.is_re()) {
1613 Z3_ast _args[2] = { a, b };
1616 else if (a.is_fpa() && b.is_fpa()) {
1617 r =
Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1624 return expr(a.ctx(), r);
◆ operator+ [2/3]
| expr operator+ |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1626 of file z3++.h.
1626 {
return a + a.ctx().num_val(b, a.get_sort()); }
◆ operator+ [3/3]
| expr operator+ |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1627 of file z3++.h.
1627 {
return b.ctx().num_val(a, b.get_sort()) + b; }
◆ operator- [1/4]
Definition at line 1695 of file z3++.h.
1700 else if (a.is_bv()) {
1703 else if (a.is_fpa()) {
1711 return expr(a.ctx(), r);
◆ operator- [2/4]
Definition at line 1714 of file z3++.h.
1717 if (a.is_arith() && b.is_arith()) {
1718 Z3_ast args[2] = { a, b };
1721 else if (a.is_bv() && b.is_bv()) {
1724 else if (a.is_fpa() && b.is_fpa()) {
1725 r =
Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1732 return expr(a.ctx(), r);
◆ operator- [3/4]
| expr operator- |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1734 of file z3++.h.
1734 {
return a - a.ctx().num_val(b, a.get_sort()); }
◆ operator- [4/4]
| expr operator- |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1735 of file z3++.h.
1735 {
return b.ctx().num_val(a, b.get_sort()) - b; }
◆ operator/ [1/3]
Definition at line 1673 of file z3++.h.
1676 if (a.is_arith() && b.is_arith()) {
1679 else if (a.is_bv() && b.is_bv()) {
1682 else if (a.is_fpa() && b.is_fpa()) {
1683 r =
Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1690 return expr(a.ctx(), r);
◆ operator/ [2/3]
| expr operator/ |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1692 of file z3++.h.
1692 {
return a / a.ctx().num_val(b, a.get_sort()); }
◆ operator/ [3/3]
| expr operator/ |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1693 of file z3++.h.
1693 {
return b.ctx().num_val(a, b.get_sort()) / b; }
◆ operator< [1/3]
Definition at line 1762 of file z3++.h.
1765 if (a.is_arith() && b.is_arith()) {
1768 else if (a.is_bv() && b.is_bv()) {
1771 else if (a.is_fpa() && b.is_fpa()) {
1779 return expr(a.ctx(), r);
◆ operator< [2/3]
| expr operator< |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1781 of file z3++.h.
1781 {
return a < a.ctx().num_val(b, a.get_sort()); }
◆ operator< [3/3]
| expr operator< |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1782 of file z3++.h.
1782 {
return b.ctx().num_val(a, b.get_sort()) < b; }
◆ operator<= [1/3]
Definition at line 1737 of file z3++.h.
1740 if (a.is_arith() && b.is_arith()) {
1743 else if (a.is_bv() && b.is_bv()) {
1746 else if (a.is_fpa() && b.is_fpa()) {
1754 return expr(a.ctx(), r);
◆ operator<= [2/3]
| expr operator<= |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1756 of file z3++.h.
1756 {
return a <= a.ctx().num_val(b, a.get_sort()); }
◆ operator<= [3/3]
| expr operator<= |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1757 of file z3++.h.
1757 {
return b.ctx().num_val(a, b.get_sort()) <= b; }
◆ operator== [1/3]
Definition at line 1576 of file z3++.h.
1578 Z3_ast r =
Z3_mk_eq(a.ctx(), a, b);
1580 return expr(a.ctx(), r);
◆ operator== [2/3]
| expr operator== |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1582 of file z3++.h.
1582 { assert(a.is_arith() || a.is_bv() || a.is_fpa());
return a == a.ctx().num_val(b, a.get_sort()); }
◆ operator== [3/3]
| expr operator== |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1583 of file z3++.h.
1583 { assert(b.is_arith() || b.is_bv() || b.is_fpa());
return b.ctx().num_val(a, b.get_sort()) == b; }
◆ operator> [1/3]
Definition at line 1784 of file z3++.h.
1787 if (a.is_arith() && b.is_arith()) {
1790 else if (a.is_bv() && b.is_bv()) {
1793 else if (a.is_fpa() && b.is_fpa()) {
1801 return expr(a.ctx(), r);
◆ operator> [2/3]
| expr operator> |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1803 of file z3++.h.
1803 {
return a > a.ctx().num_val(b, a.get_sort()); }
◆ operator> [3/3]
| expr operator> |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1804 of file z3++.h.
1804 {
return b.ctx().num_val(a, b.get_sort()) > b; }
◆ operator>= [1/3]
Definition at line 1653 of file z3++.h.
1656 if (a.is_arith() && b.is_arith()) {
1659 else if (a.is_bv() && b.is_bv()) {
1662 else if (a.is_fpa() && b.is_fpa()) {
1670 return expr(a.ctx(), r);
◆ operator>= [2/3]
| expr operator>= |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1759 of file z3++.h.
1759 {
return a >= a.ctx().num_val(b, a.get_sort()); }
◆ operator>= [3/3]
| expr operator>= |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1760 of file z3++.h.
1760 {
return b.ctx().num_val(a, b.get_sort()) >= b; }
◆ operator^ [1/3]
◆ operator^ [2/3]
| expr operator^ |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1811 of file z3++.h.
1811 {
return a ^ a.ctx().num_val(b, a.get_sort()); }
◆ operator^ [3/3]
| expr operator^ |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1812 of file z3++.h.
1812 {
return b.ctx().num_val(a, b.get_sort()) ^ b; }
◆ operator| [1/3]
◆ operator| [2/3]
| expr operator| |
( |
expr const & |
a, |
|
|
int |
b |
|
) |
| |
|
friend |
Definition at line 1815 of file z3++.h.
1815 {
return a | a.ctx().num_val(b, a.get_sort()); }
◆ operator| [3/3]
| expr operator| |
( |
int |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Definition at line 1816 of file z3++.h.
1816 {
return b.ctx().num_val(a, b.get_sort()) | b; }
◆ operator|| [1/3]
| expr operator|| |
( |
bool |
a, |
|
|
expr const & |
b |
|
) |
| |
|
friend |
Return an expression representing a or b. The C++ Boolean value a is automatically converted into a Z3 Boolean constant.
- Precondition
- b.is_bool()
Definition at line 1574 of file z3++.h.
1574 {
return b.ctx().bool_val(a) || b; }
◆ operator|| [2/3]
| expr operator|| |
( |
expr const & |
a, |
|
|
bool |
b |
|
) |
| |
|
friend |
Return an expression representing a or b. The C++ Boolean value b is automatically converted into a Z3 Boolean constant.
- Precondition
- a.is_bool()
Definition at line 1572 of file z3++.h.
1572 {
return a || a.ctx().bool_val(b); }
◆ operator|| [3/3]
Return an expression representing a or b.
- Precondition
- a.is_bool()
-
b.is_bool()
Definition at line 1563 of file z3++.h.
1565 assert(a.is_bool() && b.is_bool());
1566 Z3_ast args[2] = { a, b };
1567 Z3_ast r =
Z3_mk_or(a.ctx(), 2, args);
1569 return expr(a.ctx(), r);
◆ operator~
◆ pbeq
Definition at line 2278 of file z3++.h.
2279 assert(es.size() > 0);
2280 context&
ctx = es[0].ctx();
2281 array<Z3_ast> _es(es);
2282 Z3_ast r =
Z3_mk_pbeq(
ctx, _es.size(), _es.ptr(), coeffs, bound);
◆ pbge
Definition at line 2270 of file z3++.h.
2271 assert(es.size() > 0);
2272 context&
ctx = es[0].ctx();
2273 array<Z3_ast> _es(es);
2274 Z3_ast r =
Z3_mk_pbge(
ctx, _es.size(), _es.ptr(), coeffs, bound);
◆ pble
Definition at line 2262 of file z3++.h.
2263 assert(es.size() > 0);
2264 context&
ctx = es[0].ctx();
2265 array<Z3_ast> _es(es);
2266 Z3_ast r =
Z3_mk_pble(
ctx, _es.size(), _es.ptr(), coeffs, bound);
◆ pw [1/3]
◆ pw [2/3]
Definition at line 1508 of file z3++.h.
1508 {
return pw(a, a.ctx().num_val(b, a.get_sort())); }
◆ pw [3/3]
Definition at line 1509 of file z3++.h.
1509 {
return pw(b.ctx().num_val(a, b.get_sort()), b); }
◆ range
◆ rem [1/3]
Definition at line 1527 of file z3++.h.
1528 if (a.is_fpa() && b.is_fpa()) {
◆ rem [2/3]
Definition at line 1534 of file z3++.h.
1534 {
return rem(a, a.ctx().num_val(b, a.get_sort())); }
◆ rem [3/3]
Definition at line 1535 of file z3++.h.
1535 {
return rem(b.ctx().num_val(a, b.get_sort()), b); }
◆ round_fpa_to_closest_integer
| expr round_fpa_to_closest_integer |
( |
expr const & |
t | ) |
|
|
friend |
Round a floating-point term into its closest integer.
Definition at line 1946 of file z3++.h.
1950 return expr(t.ctx(), r);
◆ sbv_to_fpa
Conversion of a signed bit-vector term into a floating-point.
Definition at line 1925 of file z3++.h.
1929 return expr(t.ctx(), r);
◆ sqrt
◆ sum
Definition at line 2302 of file z3++.h.
2303 assert(args.size() > 0);
2304 context&
ctx = args[0].ctx();
2305 array<Z3_ast> _args(args);
◆ ubv_to_fpa
Conversion of an unsigned bit-vector term into a floating-point.
Definition at line 1932 of file z3++.h.
1936 return expr(t.ctx(), r);
◆ xnor
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(Z3_context c, Z3_ast bv, Z3_sort s)
Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
bool is_fpa() const
Return true if this sort is a Floating point sort.
Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s)
Integer to string conversion.
bool is_relation() const
Return true if this sort is a Relation sort.
Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2)
Minimum of floating-point numbers.
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than.
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflo...
Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.
Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point remainder.
#define _Z3_MK_BIN_(a, b, binop)
bool is_numeral_i(int &i) const
bool is_re() const
Return true if this sort is a regular expression sort.
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
Z3_ast Z3_API Z3_mk_fpa_to_ubv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)
Conversion of a floating-point term into an unsigned bit-vector.
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
Z3_ast Z3_API Z3_mk_fpa_is_nan(Z3_context c, Z3_ast t)
Predicate indicating whether t is a NaN.
Z3_ast Z3_API Z3_mk_fpa_fma(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Floating-point fused multiply-add.
unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a)
Return the number of argument of an application. If t is an constant, then the number of arguments is...
Z3_ast Z3_API Z3_mk_rotate_left(Z3_context c, unsigned i, Z3_ast t1)
Rotate bits of t1 to the left i times.
Z3_func_decl Z3_API Z3_get_app_decl(Z3_context c, Z3_app a)
Return the declaration of a constant or function application.
Z3_ast Z3_API Z3_mk_bv2int(Z3_context c, Z3_ast t1, bool is_signed)
Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 is t...
Z3_char_ptr Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned *length)
Retrieve the unescaped string constant stored in s.
Z3_string Z3_API Z3_get_numeral_binary_string(Z3_context c, Z3_ast a)
Return numeral value, as a binary string of a numeric constant term.
Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].
Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point square root.
bool is_numeral_u(unsigned &i) const
int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the integer value associated with an integer parameter.
expr select(expr const &a, expr const &i)
forward declarations
friend expr rem(expr const &a, expr const &b)
bool is_array() const
Return true if this sort is a Array sort.
Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 xor t2.
Z3_ast Z3_API Z3_mk_bvneg_no_overflow(Z3_context c, Z3_ast t1)
Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector.
Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig)
Create an expression of FloatingPoint sort from three bit-vector expressions.
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] or ... or args[num_args-1].
unsigned Z3_API Z3_algebraic_get_i(Z3_context c, Z3_ast a)
Return which root of the polynomial the algebraic number represents.
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).
Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)
Interface to simplifier.
Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nor.
Z3_string Z3_API Z3_get_numeral_string(Z3_context c, Z3_ast a)
Return numeral value, as a decimal string of a numeric constant term.
unsigned num_args() const
Return the number of arguments in this application. This method assumes the expression is an applicat...
Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi)
Create a regular expression loop. The supplied regular expression r is repeated between lo and hi tim...
Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than or equal.
Z3_ast Z3_API Z3_mk_fpa_to_sbv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)
Conversion of a floating-point term into a signed bit-vector.
bool is_bv() const
Return true if this sort is a Bit-vector sort.
Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] + ... + args[num_args-1].
bool Z3_API Z3_is_quantifier_forall(Z3_context c, Z3_ast a)
Determine if an ast is a universal quantifier.
bool Z3_API Z3_is_string(Z3_context c, Z3_ast s)
Determine if s is a string constant.
Z3_ast Z3_API Z3_get_algebraic_number_upper(Z3_context c, Z3_ast a, unsigned precision)
Return a upper bound for the given real algebraic number. The interval isolating the number is smalle...
Z3_ast Z3_API Z3_mk_fpa_to_fp_signed(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t)
Return true if the given expression t is well sorted.
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 rem arg2.
Z3_ast_vector Z3_API Z3_algebraic_get_poly(Z3_context c, Z3_ast a)
Return the coefficients of the defining polynomial.
Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a)
Create a unit sequence of a.
Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.
#define _Z3_MK_UN_(a, mkun)
Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1)
Take disjunction of bits in vector, return vector of length 1.
Z3_ast Z3_API Z3_mk_fpa_to_fp_unsigned(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort.
bool is_quantifier() const
Return true if this expression is a quantifier.
Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s)
Return the length of the sequence s.
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.
bool is_seq() const
Return true if this is a sequence expression.
Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than.
Z3_string Z3_API Z3_get_string(Z3_context c, Z3_ast s)
Retrieve the string constant stored in s.
Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point subtraction.
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.
Z3_ast Z3_API Z3_get_denominator(Z3_context c, Z3_ast a)
Return the denominator (as a numeral AST) of a numeral AST of sort Real.
Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than or equal to.
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement addition.
bool Z3_API Z3_is_quantifier_exists(Z3_context c, Z3_ast a)
Determine if ast is an existential quantifier.
Z3_decl_kind decl_kind() const
Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(Z3_context c, Z3_ast t)
Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than or equal.
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.
Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s)
Convert string to integer.
bool is_datatype() const
Return true if this sort is a Datatype sort.
Z3_ast Z3_API Z3_get_numerator(Z3_context c, Z3_ast a)
Return the numerator (as a numeral AST) of a numeral AST of sort Real.
Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1)
Repeat the given bit-vector up length i.
unsigned Z3_API Z3_get_ast_id(Z3_context c, Z3_ast t)
Return a unique identifier for t. The identifier is unique up to structural equality....
Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi)
Create the range regular expression over two sequences of length 1.
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
Z3_ast Z3_API Z3_mk_extract(Z3_context c, unsigned high, unsigned low, Z3_ast t1)
Extract the bits high down to low from a bit-vector of size m to yield a new bit-vector of size n,...
friend expr implies(expr const &a, expr const &b)
bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a)
Return true if the given AST is a real algebraic number.
Z3_ast Z3_API Z3_mk_fpa_is_infinite(Z3_context c, Z3_ast t)
Predicate indicating whether t is a floating-point number representing +oo or -oo.
bool is_numeral() const
Return true if this expression is a numeral. Specialized functions also return representations for th...
bool Z3_API Z3_get_numeral_uint64(Z3_context c, Z3_ast v, uint64_t *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine uint64_t int....
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 ^ arg2.
Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point division.
Z3_ast Z3_API Z3_mk_fpa_is_subnormal(Z3_context c, Z3_ast t)
Predicate indicating whether t is a subnormal floating-point number.
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d)
Return the number of parameters associated with a declaration.
Z3_ast Z3_API Z3_mk_fpa_is_normal(Z3_context c, Z3_ast t)
Predicate indicating whether t is a normal floating-point number.
Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.
bool Z3_API Z3_get_numeral_uint(Z3_context c, Z3_ast v, unsigned *u)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine unsigned int....
Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows divisor).
Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst)
Replace the first occurrence of src with dst in s.
friend expr pw(expr const &a, expr const &b)
Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee)
Check if container contains containee.
bool is_finite_domain() const
Return true if this sort is a Finite domain sort.
bool is_algebraic() const
Return true if expression is an algebraic number.
func_decl decl() const
Return the declaration associated with this application. This method assumes the expression is an app...
bool Z3_API Z3_get_numeral_int64(Z3_context c, Z3_ast v, int64_t *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int64_t int....
bool is_int() const
Return true if this sort is the Integer sort.
Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.
ast_vector_tpl< expr > expr_vector
bool is_seq() const
Return true if this sort is a Sequence sort.
friend expr concat(expr const &a, expr const &b)
bool Z3_API Z3_is_lambda(Z3_context c, Z3_ast a)
Determine if ast is a lambda expression.
Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than or equal to.
Z3_ast Z3_API Z3_mk_int2bv(Z3_context c, unsigned n, Z3_ast t1)
Create an n bit bit-vector from the integer argument t1.
bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
Z3_string Z3_API Z3_get_numeral_decimal_string(Z3_context c, Z3_ast a, unsigned precision)
Return numeral as a string in decimal notation. The result has at most precision decimal places.
bool Z3_API Z3_get_numeral_int(Z3_context c, Z3_ast v, int *i)
Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int....
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nand.
bool is_arith() const
Return true if this sort is the Integer or Real sort.
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.
Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i)
Return the i-th argument of the given application.
Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point equality.
Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than.
friend void check_context(object const &a, object const &b)
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
friend expr mod(expr const &a, expr const &b)
Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[])
Create the union of the regular languages.
bool is_bv() const
Return true if this is a Bit-vector expression.
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
bool is_array() const
Return true if this is a Array expression.
Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.
Z3_ast Z3_API Z3_substitute(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const from[], Z3_ast const to[])
Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs....
Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise xnor.
Z3_lbool Z3_API Z3_get_bool_value(Z3_context c, Z3_ast a)
Return Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF otherwise.
bool is_real() const
Return true if this sort is the Real sort.
Z3_ast Z3_API Z3_get_algebraic_number_lower(Z3_context c, Z3_ast a, unsigned precision)
Return a lower bound for the given real algebraic number. The interval isolating the number is smalle...
expr nth(expr const &index) const
Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.
Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2)
Maximum of floating-point numbers.
bool is_bool() const
Return true if this sort is the Boolean sort.
Z3_ast Z3_API Z3_mk_rotate_right(Z3_context c, unsigned i, Z3_ast t1)
Rotate bits of t1 to the right i times.
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).
Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point multiplication.
Z3_ast Z3_API Z3_substitute_vars(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const to[])
Substitute the free variables in a with the expressions in to. For every i smaller than num_exprs,...
Z3_ast Z3_API Z3_mk_fpa_to_fp_float(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point addition.
bool is_numeral_i64(int64_t &i) const
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.
Z3_ast Z3_API Z3_mk_fpa_round_to_integral(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point roundToIntegral. Rounds a floating-point number to the closest integer,...
Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1)
Check if a real number is an integer.
Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
double Z3_API Z3_get_numeral_double(Z3_context c, Z3_ast a)
Return numeral as a double.
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.
Z3_ast Z3_API Z3_get_quantifier_body(Z3_context c, Z3_ast a)
Return body of quantifier.
Z3_ast Z3_API Z3_mk_seq_at(Z3_context c, Z3_ast s, Z3_ast index)
Retrieve from s the unit sequence positioned at position index. The sequence is empty if the index is...
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.
Z3_ast Z3_API Z3_mk_fpa_is_zero(Z3_context c, Z3_ast t)
Predicate indicating whether t is a floating-point number with zero value, i.e., +zero or -zero.
Z3_error_code check_error() const
Z3_error_code check_error() const
Auxiliary method used to check for API usage errors.
bool is_fpa() const
Return true if this is a FloatingPoint expression. .
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than.
Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] - ... - args[num_args - 1].
Z3_ast Z3_API Z3_mk_seq_nth(Z3_context c, Z3_ast s, Z3_ast index)
Retrieve from s the element positioned at position index. The function is under-specified if the inde...
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])
Create the concatenation of the regular languages.
Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] * ... * args[num_args-1].
Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length)
Extract subsequence starting at offset of length.
bool is_app() const
Return true if this expression is an application.
bool is_string_value() const
Return true if this expression is a string literal. The string can be accessed using get_string() and...
bool is_numeral_u64(uint64_t &i) const
sort get_sort() const
Return the sort of this expression.
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.
Inheritance diagram for expr:
1.8.20
