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) | |
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 |
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 | 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) |
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 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().
|
inline |
Return i of an algebraic number (root-obj p i)
Definition at line 993 of file z3++.h.
|
inline |
Retrieve lower and upper bounds for algebraic numerals based on a decimal precision
Definition at line 966 of file z3++.h.
|
inline |
Return coefficients for p of an algebraic number (root-obj p i)
Definition at line 983 of file z3++.h.
|
inline |
Definition at line 973 of file z3++.h.
|
inline |
Return the i-th argument of this application. This method assumes the expression is an application.
Definition at line 1148 of file z3++.h.
Referenced by AstRef::__bool__(), and ExprRef::children().
|
inline |
Definition at line 835 of file z3++.h.
Definition at line 1413 of file z3++.h.
|
inline |
Return the 'body' of this quantifier.
Definition at line 1155 of file z3++.h.
Referenced by QuantifierRef::children().
|
inline |
Definition at line 1407 of file z3++.h.
|
inline |
Return the declaration associated with this application. This method assumes the expression is an application.
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(), expr::lo(), and ExprRef::params().
|
inline |
Definition at line 1091 of file z3++.h.
Referenced by RatNumRef::denominator_as_long(), and RatNumRef::is_int_value().
sequence and regular expression operations.
Definition at line 1392 of file z3++.h.
|
inline |
Definition at line 1343 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 958 of file z3++.h.
|
inline |
for a string value expression return an escaped or unescaped string value.
Definition at line 1110 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.
Definition at line 1015 of file z3++.h.
|
inline |
Return int64_t
value of numeral, throw if result cannot fit in int64_t
.
Definition at line 1051 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 1034 of file z3++.h.
|
inline |
Return uint64_t
value of numeral, throw if result cannot fit in uint64_t
.
Definition at line 1068 of file z3++.h.
|
inline |
Return the sort of this expression.
Definition at line 765 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::sge(), z3::sgt(), 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 1117 of file z3++.h.
|
inline |
Definition at line 1345 of file z3++.h.
Referenced by expr::extract(), and expr::loop().
|
inline |
|
inline |
Return true if expression is an algebraic number.
Definition at line 875 of file z3++.h.
Referenced by expr::algebraic_i(), expr::algebraic_lower(), expr::algebraic_poly(), expr::algebraic_upper(), and expr::get_decimal_string().
|
inline |
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().
|
inline |
Return true if this is an integer or real expression.
Definition at line 782 of file z3++.h.
|
inline |
Return true if this is a Array expression.
Definition at line 790 of file z3++.h.
Referenced by expr::operator[]().
|
inline |
Return true if this is a Boolean expression.
Definition at line 770 of file z3++.h.
Referenced by solver::add(), optimize::add(), and optimize::add_soft().
|
inline |
Return true if this is a Bit-vector expression.
Definition at line 786 of file z3++.h.
Referenced by expr::mk_from_ieee_bv().
|
inline |
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().
|
inline |
Return true if this is a Datatype expression.
Definition at line 794 of file z3++.h.
|
inline |
|
inline |
|
inline |
Return true if this is a Finite-domain expression.
Definition at line 816 of file z3++.h.
|
inline |
|
inline |
Return true if this is a FloatingPoint expression. .
Definition at line 820 of file z3++.h.
Referenced by 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!=(), and z3::operator==().
|
inline |
Return true if this is an integer expression.
Definition at line 774 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 866 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 827 of file z3++.h.
Referenced by expr::as_binary(), expr::as_double(), 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 834 of file z3++.h.
Referenced by expr::is_numeral().
|
inline |
Definition at line 832 of file z3++.h.
Referenced by expr::is_numeral().
|
inline |
Definition at line 833 of file z3++.h.
Referenced by expr::is_numeral().
|
inline |
Definition at line 830 of file z3++.h.
Referenced by expr::get_numeral_int().
|
inline |
Definition at line 828 of file z3++.h.
Referenced by expr::as_int64(), and expr::get_numeral_int64().
|
inline |
Definition at line 831 of file z3++.h.
Referenced by expr::get_numeral_uint().
|
inline |
Definition at line 829 of file z3++.h.
Referenced by expr::as_uint64(), and expr::get_numeral_uint64().
|
inline |
|
inline |
Return true if this expression is a quantifier.
Definition at line 853 of file z3++.h.
Referenced by expr::body().
|
inline |
Return true if this is a regular expression.
Definition at line 806 of file z3++.h.
|
inline |
Return true if this is a real expression.
Definition at line 778 of file z3++.h.
|
inline |
Return true if this is a Relation expression.
Definition at line 798 of file z3++.h.
|
inline |
Return true if this is a sequence expression.
Definition at line 802 of file z3++.h.
Referenced by expr::operator[]().
|
inline |
Return true if this expression is a string literal. The string can be accessed using get_string()
and get_escaped_string()
Definition at line 1103 of file z3++.h.
Referenced by SeqRef::as_string(), expr::get_escaped_string(), and expr::get_string().
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Definition at line 1425 of file z3++.h.
Referenced by expr::extract().
|
inline |
Definition at line 1344 of file z3++.h.
Referenced by expr::extract(), and expr::loop().
|
inline |
create a looping regular expression.
Definition at line 1445 of file z3++.h.
|
inline |
Convert this IEEE BV into a fpa.
Definition at line 945 of file z3++.h.
|
inline |
Return Boolean expression to test for whether an FP expression is inf.
Definition at line 885 of file z3++.h.
|
inline |
Return Boolean expression to test for whether an FP expression is a NaN.
Definition at line 895 of file z3++.h.
|
inline |
Return Boolean expression to test for whether an FP expression is a normal.
Definition at line 905 of file z3++.h.
|
inline |
Return Boolean expression to test for whether an FP expression is a subnormal.
Definition at line 915 of file z3++.h.
|
inline |
Return Boolean expression to test for whether an FP expression is a zero.
Definition at line 925 of file z3++.h.
|
inline |
Convert this fpa into an IEEE BV.
Definition at line 935 of file z3++.h.
Definition at line 1419 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 1140 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 1083 of file z3++.h.
Referenced by RatNumRef::numerator_as_long().
|
inline |
index operator defined on arrays and sequences.
Definition at line 1459 of file z3++.h.
|
inline |
|
inline |
Definition at line 1396 of file z3++.h.
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Apply substitution. Replace bound variables by expressions.
Definition at line 3795 of file z3++.h.
|
inline |
Apply substitution. Replace src expressions by dst.
Definition at line 3782 of file z3++.h.
|
inline |
Definition at line 1863 of file z3++.h.
|
friend |
|
friend |
bit-vector overflow/underflow checks
Definition at line 2103 of file z3++.h.
Definition at line 2106 of file z3++.h.
Definition at line 2121 of file z3++.h.
Definition at line 2124 of file z3++.h.
Definition at line 1857 of file z3++.h.
Definition at line 1851 of file z3++.h.
Definition at line 2115 of file z3++.h.
Definition at line 2109 of file z3++.h.
Definition at line 2112 of file z3++.h.
Definition at line 2320 of file z3++.h.
|
friend |
Definition at line 2338 of file z3++.h.
|
friend |
Definition at line 2311 of file z3++.h.
FloatingPoint fused multiply-add.
Definition at line 1895 of file z3++.h.
Definition at line 1886 of file z3++.h.
Create an expression of FloatingPoint sort from three bit-vector expressions.
Definition at line 1903 of file z3++.h.
Conversion of a floating-point term into another floating-point.
Definition at line 1939 of file z3++.h.
Conversion of a floating-point term into a signed bit-vector.
Definition at line 1911 of file z3++.h.
Conversion of a floating-point term into an unsigned bit-vector.
Definition at line 1918 of file z3++.h.
Definition at line 1547 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 1958 of file z3++.h.
Definition at line 1836 of file z3++.h.
Definition at line 1821 of file z3++.h.
|
friend |
Definition at line 2370 of file z3++.h.
|
friend |
Definition at line 2364 of file z3++.h.
Definition at line 1511 of file z3++.h.
Definition at line 1818 of file z3++.h.
Definition at line 1819 of file z3++.h.
Return an expression representing not(a)
.
Definition at line 1545 of file z3++.h.
Definition at line 1587 of file z3++.h.
Definition at line 1806 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 1561 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 1560 of file z3++.h.
Return an expression representing a and b
.
Definition at line 1551 of file z3++.h.
Definition at line 1629 of file z3++.h.
Definition at line 1599 of file z3++.h.
Definition at line 1695 of file z3++.h.
Definition at line 1714 of file z3++.h.
Definition at line 1673 of file z3++.h.
Definition at line 1762 of file z3++.h.
Definition at line 1737 of file z3++.h.
Definition at line 1784 of file z3++.h.
Definition at line 1653 of file z3++.h.
Definition at line 1810 of file z3++.h.
Definition at line 1814 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 1574 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 1572 of file z3++.h.
Return an expression representing a or b
.
Definition at line 1563 of file z3++.h.
|
friend |
|
friend |
|
friend |
Definition at line 1527 of file z3++.h.
Round a floating-point term into its closest integer.
Definition at line 1946 of file z3++.h.
Conversion of a signed bit-vector term into a floating-point.
Definition at line 1925 of file z3++.h.
Definition at line 1879 of file z3++.h.
|
friend |
Conversion of an unsigned bit-vector term into a floating-point.
Definition at line 1932 of file z3++.h.
Definition at line 1820 of file z3++.h.