Go to the source code of this file.
Functions | |
Floating-Point Arithmetic | |
Z3_sort Z3_API | Z3_mk_fpa_rounding_mode_sort (Z3_context c) |
Create the RoundingMode sort. More... | |
Z3_ast Z3_API | Z3_mk_fpa_round_nearest_ties_to_even (Z3_context c) |
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. More... | |
Z3_ast Z3_API | Z3_mk_fpa_rne (Z3_context c) |
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. More... | |
Z3_ast Z3_API | Z3_mk_fpa_round_nearest_ties_to_away (Z3_context c) |
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. More... | |
Z3_ast Z3_API | Z3_mk_fpa_rna (Z3_context c) |
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. More... | |
Z3_ast Z3_API | Z3_mk_fpa_round_toward_positive (Z3_context c) |
Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. More... | |
Z3_ast Z3_API | Z3_mk_fpa_rtp (Z3_context c) |
Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. More... | |
Z3_ast Z3_API | Z3_mk_fpa_round_toward_negative (Z3_context c) |
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. More... | |
Z3_ast Z3_API | Z3_mk_fpa_rtn (Z3_context c) |
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. More... | |
Z3_ast Z3_API | Z3_mk_fpa_round_toward_zero (Z3_context c) |
Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. More... | |
Z3_ast Z3_API | Z3_mk_fpa_rtz (Z3_context c) |
Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. More... | |
Z3_sort Z3_API | Z3_mk_fpa_sort (Z3_context c, unsigned ebits, unsigned sbits) |
Create a FloatingPoint sort. More... | |
Z3_sort Z3_API | Z3_mk_fpa_sort_half (Z3_context c) |
Create the half-precision (16-bit) FloatingPoint sort. More... | |
Z3_sort Z3_API | Z3_mk_fpa_sort_16 (Z3_context c) |
Create the half-precision (16-bit) FloatingPoint sort. More... | |
Z3_sort Z3_API | Z3_mk_fpa_sort_single (Z3_context c) |
Create the single-precision (32-bit) FloatingPoint sort. More... | |
Z3_sort Z3_API | Z3_mk_fpa_sort_32 (Z3_context c) |
Create the single-precision (32-bit) FloatingPoint sort. More... | |
Z3_sort Z3_API | Z3_mk_fpa_sort_double (Z3_context c) |
Create the double-precision (64-bit) FloatingPoint sort. More... | |
Z3_sort Z3_API | Z3_mk_fpa_sort_64 (Z3_context c) |
Create the double-precision (64-bit) FloatingPoint sort. More... | |
Z3_sort Z3_API | Z3_mk_fpa_sort_quadruple (Z3_context c) |
Create the quadruple-precision (128-bit) FloatingPoint sort. More... | |
Z3_sort Z3_API | Z3_mk_fpa_sort_128 (Z3_context c) |
Create the quadruple-precision (128-bit) FloatingPoint sort. More... | |
Z3_ast Z3_API | Z3_mk_fpa_nan (Z3_context c, Z3_sort s) |
Create a floating-point NaN of sort s . More... | |
Z3_ast Z3_API | Z3_mk_fpa_inf (Z3_context c, Z3_sort s, bool negative) |
Create a floating-point infinity of sort s . More... | |
Z3_ast Z3_API | Z3_mk_fpa_zero (Z3_context c, Z3_sort s, bool negative) |
Create a floating-point zero of sort s . More... | |
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. More... | |
Z3_ast Z3_API | Z3_mk_fpa_numeral_float (Z3_context c, float v, Z3_sort ty) |
Create a numeral of FloatingPoint sort from a float. More... | |
Z3_ast Z3_API | Z3_mk_fpa_numeral_double (Z3_context c, double v, Z3_sort ty) |
Create a numeral of FloatingPoint sort from a double. More... | |
Z3_ast Z3_API | Z3_mk_fpa_numeral_int (Z3_context c, signed v, Z3_sort ty) |
Create a numeral of FloatingPoint sort from a signed integer. More... | |
Z3_ast Z3_API | Z3_mk_fpa_numeral_int_uint (Z3_context c, bool sgn, signed exp, unsigned sig, Z3_sort ty) |
Create a numeral of FloatingPoint sort from a sign bit and two integers. More... | |
Z3_ast Z3_API | Z3_mk_fpa_numeral_int64_uint64 (Z3_context c, bool sgn, int64_t exp, uint64_t sig, Z3_sort ty) |
Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers. More... | |
Z3_ast Z3_API | Z3_mk_fpa_abs (Z3_context c, Z3_ast t) |
Floating-point absolute value. More... | |
Z3_ast Z3_API | Z3_mk_fpa_neg (Z3_context c, Z3_ast t) |
Floating-point negation. More... | |
Z3_ast Z3_API | Z3_mk_fpa_add (Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) |
Floating-point addition. More... | |
Z3_ast Z3_API | Z3_mk_fpa_sub (Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) |
Floating-point subtraction. More... | |
Z3_ast Z3_API | Z3_mk_fpa_mul (Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) |
Floating-point multiplication. More... | |
Z3_ast Z3_API | Z3_mk_fpa_div (Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) |
Floating-point division. More... | |
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. More... | |
Z3_ast Z3_API | Z3_mk_fpa_sqrt (Z3_context c, Z3_ast rm, Z3_ast t) |
Floating-point square root. More... | |
Z3_ast Z3_API | Z3_mk_fpa_rem (Z3_context c, Z3_ast t1, Z3_ast t2) |
Floating-point remainder. More... | |
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, again represented as a floating-point number. More... | |
Z3_ast Z3_API | Z3_mk_fpa_min (Z3_context c, Z3_ast t1, Z3_ast t2) |
Minimum of floating-point numbers. More... | |
Z3_ast Z3_API | Z3_mk_fpa_max (Z3_context c, Z3_ast t1, Z3_ast t2) |
Maximum of floating-point numbers. More... | |
Z3_ast Z3_API | Z3_mk_fpa_leq (Z3_context c, Z3_ast t1, Z3_ast t2) |
Floating-point less than or equal. More... | |
Z3_ast Z3_API | Z3_mk_fpa_lt (Z3_context c, Z3_ast t1, Z3_ast t2) |
Floating-point less than. More... | |
Z3_ast Z3_API | Z3_mk_fpa_geq (Z3_context c, Z3_ast t1, Z3_ast t2) |
Floating-point greater than or equal. More... | |
Z3_ast Z3_API | Z3_mk_fpa_gt (Z3_context c, Z3_ast t1, Z3_ast t2) |
Floating-point greater than. More... | |
Z3_ast Z3_API | Z3_mk_fpa_eq (Z3_context c, Z3_ast t1, Z3_ast t2) |
Floating-point equality. More... | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
Z3_ast Z3_API | Z3_mk_fpa_is_nan (Z3_context c, Z3_ast t) |
Predicate indicating whether t is a NaN. More... | |
Z3_ast Z3_API | Z3_mk_fpa_is_negative (Z3_context c, Z3_ast t) |
Predicate indicating whether t is a negative floating-point number. More... | |
Z3_ast Z3_API | Z3_mk_fpa_is_positive (Z3_context c, Z3_ast t) |
Predicate indicating whether t is a positive floating-point number. More... | |
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. More... | |
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. More... | |
Z3_ast Z3_API | Z3_mk_fpa_to_fp_real (Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s) |
Conversion of a term of real sort into a term of FloatingPoint sort. More... | |
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. More... | |
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. More... | |
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. More... | |
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. More... | |
Z3_ast Z3_API | Z3_mk_fpa_to_real (Z3_context c, Z3_ast t) |
Conversion of a floating-point term into a real-numbered term. More... | |
Z3-specific floating-point extensions | |
unsigned Z3_API | Z3_fpa_get_ebits (Z3_context c, Z3_sort s) |
Retrieves the number of bits reserved for the exponent in a FloatingPoint sort. More... | |
unsigned Z3_API | Z3_fpa_get_sbits (Z3_context c, Z3_sort s) |
Retrieves the number of bits reserved for the significand in a FloatingPoint sort. More... | |
bool Z3_API | Z3_fpa_is_numeral_nan (Z3_context c, Z3_ast t) |
Checks whether a given floating-point numeral is a NaN. More... | |
bool Z3_API | Z3_fpa_is_numeral_inf (Z3_context c, Z3_ast t) |
Checks whether a given floating-point numeral is a +oo or -oo. More... | |
bool Z3_API | Z3_fpa_is_numeral_zero (Z3_context c, Z3_ast t) |
Checks whether a given floating-point numeral is +zero or -zero. More... | |
bool Z3_API | Z3_fpa_is_numeral_normal (Z3_context c, Z3_ast t) |
Checks whether a given floating-point numeral is normal. More... | |
bool Z3_API | Z3_fpa_is_numeral_subnormal (Z3_context c, Z3_ast t) |
Checks whether a given floating-point numeral is subnormal. More... | |
bool Z3_API | Z3_fpa_is_numeral_positive (Z3_context c, Z3_ast t) |
Checks whether a given floating-point numeral is positive. More... | |
bool Z3_API | Z3_fpa_is_numeral_negative (Z3_context c, Z3_ast t) |
Checks whether a given floating-point numeral is negative. More... | |
Z3_ast Z3_API | Z3_fpa_get_numeral_sign_bv (Z3_context c, Z3_ast t) |
Retrieves the sign of a floating-point literal as a bit-vector expression. More... | |
Z3_ast Z3_API | Z3_fpa_get_numeral_significand_bv (Z3_context c, Z3_ast t) |
Retrieves the significand of a floating-point literal as a bit-vector expression. More... | |
bool Z3_API | Z3_fpa_get_numeral_sign (Z3_context c, Z3_ast t, int *sgn) |
Retrieves the sign of a floating-point literal. More... | |
Z3_string Z3_API | Z3_fpa_get_numeral_significand_string (Z3_context c, Z3_ast t) |
Return the significand value of a floating-point numeral as a string. More... | |
bool Z3_API | Z3_fpa_get_numeral_significand_uint64 (Z3_context c, Z3_ast t, uint64_t *n) |
Return the significand value of a floating-point numeral as a uint64. More... | |
Z3_string Z3_API | Z3_fpa_get_numeral_exponent_string (Z3_context c, Z3_ast t, bool biased) |
Return the exponent value of a floating-point numeral as a string. More... | |
bool Z3_API | Z3_fpa_get_numeral_exponent_int64 (Z3_context c, Z3_ast t, int64_t *n, bool biased) |
Return the exponent value of a floating-point numeral as a signed 64-bit integer. More... | |
Z3_ast Z3_API | Z3_fpa_get_numeral_exponent_bv (Z3_context c, Z3_ast t, bool biased) |
Retrieves the exponent of a floating-point literal as a bit-vector expression. More... | |
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. More... | |
Z3_ast Z3_API | Z3_mk_fpa_to_fp_int_real (Z3_context c, Z3_ast rm, Z3_ast exp, Z3_ast sig, Z3_sort s) |
Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort. More... | |
unsigned Z3_API Z3_fpa_get_ebits | ( | Z3_context | c, |
Z3_sort | s | ||
) |
Retrieves the number of bits reserved for the exponent in a FloatingPoint sort.
c | logical context |
s | FloatingPoint sort |
Referenced by FPSortRef::ebits(), and sort::fpa_ebits().
Z3_ast Z3_API Z3_fpa_get_numeral_exponent_bv | ( | Z3_context | c, |
Z3_ast | t, | ||
bool | biased | ||
) |
Retrieves the exponent of a floating-point literal as a bit-vector expression.
c | logical context |
t | a floating-point numeral |
biased | flag to indicate whether the result is in biased representation |
Remarks: This function extracts the exponent in t
, without normalization. NaN is an invalid arguments.
Referenced by FPNumRef::exponent_as_bv().
bool Z3_API Z3_fpa_get_numeral_exponent_int64 | ( | Z3_context | c, |
Z3_ast | t, | ||
int64_t * | n, | ||
bool | biased | ||
) |
Return the exponent value of a floating-point numeral as a signed 64-bit integer.
c | logical context |
t | a floating-point numeral |
n | exponent |
biased | flag to indicate whether the result is in biased representation |
Remarks: This function extracts the exponent in t
, without normalization. NaN is an invalid argument.
Referenced by FPNumRef::exponent_as_long().
Z3_string Z3_API Z3_fpa_get_numeral_exponent_string | ( | Z3_context | c, |
Z3_ast | t, | ||
bool | biased | ||
) |
Return the exponent value of a floating-point numeral as a string.
c | logical context |
t | a floating-point numeral |
biased | flag to indicate whether the result is in biased representation |
Remarks: This function extracts the exponent in t
, without normalization. NaN is an invalid argument.
Referenced by FPNumRef::exponent().
bool Z3_API Z3_fpa_get_numeral_sign | ( | Z3_context | c, |
Z3_ast | t, | ||
int * | sgn | ||
) |
Retrieves the sign of a floating-point literal.
c | logical context |
t | a floating-point numeral |
sgn | sign |
Remarks: sets sgn
to 0 if ‘t’ is positive and to 1 otherwise, except for NaN, which is an invalid argument.
Referenced by FPNumRef::sign().
Z3_ast Z3_API Z3_fpa_get_numeral_sign_bv | ( | Z3_context | c, |
Z3_ast | t | ||
) |
Retrieves the sign of a floating-point literal as a bit-vector expression.
c | logical context |
t | a floating-point numeral |
Remarks: NaN is an invalid argument.
Referenced by FPNumRef::sign_as_bv().
Z3_ast Z3_API Z3_fpa_get_numeral_significand_bv | ( | Z3_context | c, |
Z3_ast | t | ||
) |
Retrieves the significand of a floating-point literal as a bit-vector expression.
c | logical context |
t | a floating-point numeral |
Remarks: NaN is an invalid argument.
Referenced by FPNumRef::significand_as_bv().
Z3_string Z3_API Z3_fpa_get_numeral_significand_string | ( | Z3_context | c, |
Z3_ast | t | ||
) |
Return the significand value of a floating-point numeral as a string.
c | logical context |
t | a floating-point numeral |
Remarks: The significand s
is always 0.0 <= s < 2.0
; the resulting string is long enough to represent the real significand precisely.
Referenced by FPNumRef::significand().
bool Z3_API Z3_fpa_get_numeral_significand_uint64 | ( | Z3_context | c, |
Z3_ast | t, | ||
uint64_t * | n | ||
) |
Return the significand value of a floating-point numeral as a uint64.
c | logical context |
t | a floating-point numeral |
n | pointer to output uint64 |
Remarks: This function extracts the significand bits in t
, without the hidden bit or normalization. Sets the Z3_INVALID_ARG
error code if the significand does not fit into a uint64
. NaN is an invalid argument.
Referenced by FPNumRef::significand_as_long().
unsigned Z3_API Z3_fpa_get_sbits | ( | Z3_context | c, |
Z3_sort | s | ||
) |
Retrieves the number of bits reserved for the significand in a FloatingPoint sort.
c | logical context |
s | FloatingPoint sort |
Referenced by sort::fpa_sbits(), and FPSortRef::sbits().
bool Z3_API Z3_fpa_is_numeral_inf | ( | Z3_context | c, |
Z3_ast | t | ||
) |
Checks whether a given floating-point numeral is a +oo or -oo.
c | logical context |
t | a floating-point numeral |
Referenced by FPNumRef::isInf().
bool Z3_API Z3_fpa_is_numeral_nan | ( | Z3_context | c, |
Z3_ast | t | ||
) |
Checks whether a given floating-point numeral is a NaN.
c | logical context |
t | a floating-point numeral |
Referenced by FPNumRef::isNaN().
bool Z3_API Z3_fpa_is_numeral_negative | ( | Z3_context | c, |
Z3_ast | t | ||
) |
Checks whether a given floating-point numeral is negative.
c | logical context |
t | a floating-point numeral |
Referenced by FPNumRef::isNegative().
bool Z3_API Z3_fpa_is_numeral_normal | ( | Z3_context | c, |
Z3_ast | t | ||
) |
Checks whether a given floating-point numeral is normal.
c | logical context |
t | a floating-point numeral |
Referenced by FPNumRef::isNormal().
bool Z3_API Z3_fpa_is_numeral_positive | ( | Z3_context | c, |
Z3_ast | t | ||
) |
Checks whether a given floating-point numeral is positive.
c | logical context |
t | a floating-point numeral |
Referenced by FPNumRef::isPositive().
bool Z3_API Z3_fpa_is_numeral_subnormal | ( | Z3_context | c, |
Z3_ast | t | ||
) |
Checks whether a given floating-point numeral is subnormal.
c | logical context |
t | a floating-point numeral |
Referenced by FPNumRef::isSubnormal().
bool Z3_API Z3_fpa_is_numeral_zero | ( | Z3_context | c, |
Z3_ast | t | ||
) |
Checks whether a given floating-point numeral is +zero or -zero.
c | logical context |
t | a floating-point numeral |
Referenced by FPNumRef::isZero().
Z3_ast Z3_API Z3_mk_fpa_abs | ( | Z3_context | c, |
Z3_ast | t | ||
) |
Floating-point absolute value.
c | logical context |
t | term of FloatingPoint sort |
Referenced by z3py::fpAbs().
Z3_ast Z3_API Z3_mk_fpa_add | ( | Z3_context | c, |
Z3_ast | rm, | ||
Z3_ast | t1, | ||
Z3_ast | t2 | ||
) |
Floating-point addition.
c | logical context |
rm | term of RoundingMode sort |
t1 | term of FloatingPoint sort |
t2 | term of FloatingPoint sort |
rm
must be of RoundingMode sort, t1
and t2
must have the same FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_div | ( | Z3_context | c, |
Z3_ast | rm, | ||
Z3_ast | t1, | ||
Z3_ast | t2 | ||
) |
Floating-point division.
c | logical context |
rm | term of RoundingMode sort |
t1 | term of FloatingPoint sort. |
t2 | term of FloatingPoint sort |
The nodes rm
must be of RoundingMode sort, t1
and t2
must have the same FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_eq | ( | Z3_context | c, |
Z3_ast | t1, | ||
Z3_ast | t2 | ||
) |
Floating-point equality.
c | logical context |
t1 | term of FloatingPoint sort |
t2 | term of FloatingPoint sort |
Note that this is IEEE 754 equality (as opposed to SMT-LIB =
).
t1
and t2
must have the same FloatingPoint sort.
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.
c | logical context |
rm | term of RoundingMode sort |
t1 | term of FloatingPoint sort |
t2 | term of FloatingPoint sort |
t3 | term of FloatingPoint sort |
The result is round((t1 * t2) + t3)
.
rm
must be of RoundingMode sort, t1
, t2
, and t3
must have the same FloatingPoint sort.
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.
This is the operator named ‘fp’ in the SMT FP theory definition. Note that sgn
is required to be a bit-vector of size 1. Significand and exponent are required to be longer than 1 and 2 respectively. The FloatingPoint sort of the resulting expression is automatically determined from the bit-vector sizes of the arguments. The exponent is assumed to be in IEEE-754 biased representation.
c | logical context |
sgn | sign |
exp | exponent |
sig | significand |
Referenced by z3py::fpFP().
Z3_ast Z3_API Z3_mk_fpa_geq | ( | Z3_context | c, |
Z3_ast | t1, | ||
Z3_ast | t2 | ||
) |
Floating-point greater than or equal.
c | logical context |
t1 | term of FloatingPoint sort |
t2 | term of FloatingPoint sort |
t1
and t2
must have the same FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_gt | ( | Z3_context | c, |
Z3_ast | t1, | ||
Z3_ast | t2 | ||
) |
Floating-point greater than.
c | logical context |
t1 | term of FloatingPoint sort |
t2 | term of FloatingPoint sort |
t1
and t2
must have the same FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_inf | ( | Z3_context | c, |
Z3_sort | s, | ||
bool | negative | ||
) |
Create a floating-point infinity of sort s
.
c | logical context |
s | target sort |
negative | indicates whether the result should be negative |
When negative
is true
, -oo will be generated instead of +oo.
Referenced by z3py::fpInfinity(), z3py::fpMinusInfinity(), and z3py::fpPlusInfinity().
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.
c | logical context |
t | term of FloatingPoint sort |
t
must have FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_is_nan | ( | Z3_context | c, |
Z3_ast | t | ||
) |
Predicate indicating whether t
is a NaN.
c | logical context |
t | term of FloatingPoint sort |
t
must have FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_is_negative | ( | Z3_context | c, |
Z3_ast | t | ||
) |
Predicate indicating whether t
is a negative floating-point number.
c | logical context |
t | term of FloatingPoint sort |
t
must have FloatingPoint sort.
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.
c | logical context |
t | term of FloatingPoint sort |
t
must have FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_is_positive | ( | Z3_context | c, |
Z3_ast | t | ||
) |
Predicate indicating whether t
is a positive floating-point number.
c | logical context |
t | term of FloatingPoint sort |
t
must have FloatingPoint sort.
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.
c | logical context |
t | term of FloatingPoint sort |
t
must have FloatingPoint sort.
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.
c | logical context |
t | term of FloatingPoint sort |
t
must have FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_leq | ( | Z3_context | c, |
Z3_ast | t1, | ||
Z3_ast | t2 | ||
) |
Floating-point less than or equal.
c | logical context |
t1 | term of FloatingPoint sort |
t2 | term of FloatingPoint sort |
t1
and t2
must have the same FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_lt | ( | Z3_context | c, |
Z3_ast | t1, | ||
Z3_ast | t2 | ||
) |
Floating-point less than.
c | logical context |
t1 | term of FloatingPoint sort |
t2 | term of FloatingPoint sort |
t1
and t2
must have the same FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_max | ( | Z3_context | c, |
Z3_ast | t1, | ||
Z3_ast | t2 | ||
) |
Maximum of floating-point numbers.
c | logical context |
t1 | term of FloatingPoint sort |
t2 | term of FloatingPoint sort |
t1
, t2
must have the same FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_min | ( | Z3_context | c, |
Z3_ast | t1, | ||
Z3_ast | t2 | ||
) |
Minimum of floating-point numbers.
c | logical context |
t1 | term of FloatingPoint sort |
t2 | term of FloatingPoint sort |
t1
, t2
must have the same FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_mul | ( | Z3_context | c, |
Z3_ast | rm, | ||
Z3_ast | t1, | ||
Z3_ast | t2 | ||
) |
Floating-point multiplication.
c | logical context |
rm | term of RoundingMode sort |
t1 | term of FloatingPoint sort |
t2 | term of FloatingPoint sort |
rm
must be of RoundingMode sort, t1
and t2
must have the same FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_nan | ( | Z3_context | c, |
Z3_sort | s | ||
) |
Create a floating-point NaN of sort s
.
c | logical context |
s | target sort |
Referenced by z3py::fpNaN().
Z3_ast Z3_API Z3_mk_fpa_neg | ( | Z3_context | c, |
Z3_ast | t | ||
) |
Floating-point negation.
c | logical context |
t | term of FloatingPoint sort |
Referenced by z3py::fpNeg().
Z3_ast Z3_API Z3_mk_fpa_numeral_double | ( | Z3_context | c, |
double | v, | ||
Z3_sort | ty | ||
) |
Create a numeral of FloatingPoint sort from a double.
This function is used to create numerals that fit in a double value. It is slightly faster than Z3_mk_numeral since it is not necessary to parse a string.
c | logical context |
v | value |
ty | sort |
ty
must be a FloatingPoint sort
Referenced by context::fpa_val().
Z3_ast Z3_API Z3_mk_fpa_numeral_float | ( | Z3_context | c, |
float | v, | ||
Z3_sort | ty | ||
) |
Create a numeral of FloatingPoint sort from a float.
This function is used to create numerals that fit in a float value. It is slightly faster than Z3_mk_numeral since it is not necessary to parse a string.
c | logical context |
v | value |
ty | sort |
ty
must be a FloatingPoint sort
Referenced by context::fpa_val().
Z3_ast Z3_API Z3_mk_fpa_numeral_int | ( | Z3_context | c, |
signed | v, | ||
Z3_sort | ty | ||
) |
Create a numeral of FloatingPoint sort from a signed integer.
c | logical context |
v | value |
ty | result sort |
ty
must be a FloatingPoint sort
Z3_ast Z3_API Z3_mk_fpa_numeral_int64_uint64 | ( | Z3_context | c, |
bool | sgn, | ||
int64_t | exp, | ||
uint64_t | sig, | ||
Z3_sort | ty | ||
) |
Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
c | logical context |
sgn | sign bit (true == negative) |
sig | significand |
exp | exponent |
ty | result sort |
ty
must be a FloatingPoint sort
Z3_ast Z3_API Z3_mk_fpa_numeral_int_uint | ( | Z3_context | c, |
bool | sgn, | ||
signed | exp, | ||
unsigned | sig, | ||
Z3_sort | ty | ||
) |
Create a numeral of FloatingPoint sort from a sign bit and two integers.
c | logical context |
sgn | sign bit (true == negative) |
sig | significand |
exp | exponent |
ty | result sort |
ty
must be a FloatingPoint sort
Z3_ast Z3_API Z3_mk_fpa_rem | ( | Z3_context | c, |
Z3_ast | t1, | ||
Z3_ast | t2 | ||
) |
Floating-point remainder.
c | logical context |
t1 | term of FloatingPoint sort |
t2 | term of FloatingPoint sort |
t1
and t2
must have the same FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_rna | ( | Z3_context | c | ) |
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
c | logical context |
Referenced by context::fpa_rounding_mode().
Z3_ast Z3_API Z3_mk_fpa_rne | ( | Z3_context | c | ) |
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
c | logical context |
Referenced by context::fpa_rounding_mode().
Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_away | ( | Z3_context | c | ) |
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
c | logical context |
Referenced by z3py::RNA(), and z3py::RoundNearestTiesToAway().
Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_even | ( | Z3_context | c | ) |
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
c | logical context |
Referenced by z3py::RNE(), and z3py::RoundNearestTiesToEven().
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, again represented as a floating-point number.
c | logical context |
rm | term of RoundingMode sort |
t | term of FloatingPoint sort |
t
must be of FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_round_toward_negative | ( | Z3_context | c | ) |
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
c | logical context |
Referenced by z3py::RoundTowardNegative(), and z3py::RTN().
Z3_ast Z3_API Z3_mk_fpa_round_toward_positive | ( | Z3_context | c | ) |
Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
c | logical context |
Referenced by z3py::RoundTowardPositive(), and z3py::RTP().
Z3_ast Z3_API Z3_mk_fpa_round_toward_zero | ( | Z3_context | c | ) |
Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
c | logical context |
Referenced by z3py::RoundTowardZero(), and z3py::RTZ().
Z3_sort Z3_API Z3_mk_fpa_rounding_mode_sort | ( | Z3_context | c | ) |
Create the RoundingMode sort.
c | logical context |
Z3_ast Z3_API Z3_mk_fpa_rtn | ( | Z3_context | c | ) |
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
c | logical context |
Referenced by context::fpa_rounding_mode().
Z3_ast Z3_API Z3_mk_fpa_rtp | ( | Z3_context | c | ) |
Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
c | logical context |
Referenced by context::fpa_rounding_mode().
Z3_ast Z3_API Z3_mk_fpa_rtz | ( | Z3_context | c | ) |
Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
c | logical context |
Referenced by context::fpa_rounding_mode().
Z3_sort Z3_API Z3_mk_fpa_sort | ( | Z3_context | c, |
unsigned | ebits, | ||
unsigned | sbits | ||
) |
Create a FloatingPoint sort.
c | logical context |
ebits | number of exponent bits |
sbits | number of significand bits |
ebits
must be larger than 1 and sbits
must be larger than 2. Referenced by context::fpa_sort(), and z3py::FPSort().
Z3_sort Z3_API Z3_mk_fpa_sort_128 | ( | Z3_context | c | ) |
Create the quadruple-precision (128-bit) FloatingPoint sort.
c | logical context |
Referenced by z3py::Float128().
Z3_sort Z3_API Z3_mk_fpa_sort_16 | ( | Z3_context | c | ) |
Create the half-precision (16-bit) FloatingPoint sort.
c | logical context |
Referenced by z3py::Float16().
Z3_sort Z3_API Z3_mk_fpa_sort_32 | ( | Z3_context | c | ) |
Create the single-precision (32-bit) FloatingPoint sort.
c | logical context |
Referenced by z3py::Float32().
Z3_sort Z3_API Z3_mk_fpa_sort_64 | ( | Z3_context | c | ) |
Create the double-precision (64-bit) FloatingPoint sort.
c | logical context |
Referenced by z3py::Float64().
Z3_sort Z3_API Z3_mk_fpa_sort_double | ( | Z3_context | c | ) |
Create the double-precision (64-bit) FloatingPoint sort.
c | logical context |
Referenced by z3py::FloatDouble().
Z3_sort Z3_API Z3_mk_fpa_sort_half | ( | Z3_context | c | ) |
Create the half-precision (16-bit) FloatingPoint sort.
c | logical context |
Referenced by z3py::FloatHalf().
Z3_sort Z3_API Z3_mk_fpa_sort_quadruple | ( | Z3_context | c | ) |
Create the quadruple-precision (128-bit) FloatingPoint sort.
c | logical context |
Referenced by z3py::FloatQuadruple().
Z3_sort Z3_API Z3_mk_fpa_sort_single | ( | Z3_context | c | ) |
Create the single-precision (32-bit) FloatingPoint sort.
c | logical context. |
Referenced by z3py::FloatSingle().
Z3_ast Z3_API Z3_mk_fpa_sqrt | ( | Z3_context | c, |
Z3_ast | rm, | ||
Z3_ast | t | ||
) |
Floating-point square root.
c | logical context |
rm | term of RoundingMode sort |
t | term of FloatingPoint sort |
rm
must be of RoundingMode sort, t
must have FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_sub | ( | Z3_context | c, |
Z3_ast | rm, | ||
Z3_ast | t1, | ||
Z3_ast | t2 | ||
) |
Floating-point subtraction.
c | logical context |
rm | term of RoundingMode sort |
t1 | term of FloatingPoint sort |
t2 | term of FloatingPoint sort |
rm
must be of RoundingMode sort, t1
and t2
must have the same FloatingPoint sort.
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.
Produces a term that represents the conversion of a bit-vector term bv
to a floating-point term of sort s
.
c | logical context |
bv | a bit-vector term |
s | floating-point sort |
s
must be a FloatingPoint sort, t
must be of bit-vector sort, and the bit-vector size of bv
must be equal to ebits+sbits
of s
. The format of the bit-vector is as defined by the IEEE 754-2008 interchange format.
Referenced by z3py::fpBVToFP(), and z3py::fpToFP().
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.
Produces a term that represents the conversion of a floating-point term t
to a floating-point term of sort s
. If necessary, the result will be rounded according to rounding mode rm
.
c | logical context |
rm | term of RoundingMode sort |
t | term of FloatingPoint sort |
s | floating-point sort |
s
must be a FloatingPoint sort, rm
must be of RoundingMode sort, t
must be of floating-point sort.
Referenced by z3py::fpFPToFP(), and z3py::fpToFP().
Z3_ast Z3_API Z3_mk_fpa_to_fp_int_real | ( | Z3_context | c, |
Z3_ast | rm, | ||
Z3_ast | exp, | ||
Z3_ast | sig, | ||
Z3_sort | s | ||
) |
Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort.
Produces a term that represents the conversion of sig * 2^exp
into a floating-point term of sort s
. If necessary, the result will be rounded according to rounding mode rm
.
c | logical context |
rm | term of RoundingMode sort |
exp | exponent term of Int sort |
sig | significand term of Real sort |
s | FloatingPoint sort |
s
must be a FloatingPoint sort, rm
must be of RoundingMode sort, exp
must be of int sort, sig
must be of real sort.
Z3_ast Z3_API Z3_mk_fpa_to_fp_real | ( | Z3_context | c, |
Z3_ast | rm, | ||
Z3_ast | t, | ||
Z3_sort | s | ||
) |
Conversion of a term of real sort into a term of FloatingPoint sort.
Produces a term that represents the conversion of term t
of real sort into a floating-point term of sort s
. If necessary, the result will be rounded according to rounding mode rm
.
c | logical context |
rm | term of RoundingMode sort |
t | term of Real sort |
s | floating-point sort |
s
must be a FloatingPoint sort, rm
must be of RoundingMode sort, t
must be of real sort.
Referenced by z3py::fpRealToFP(), and z3py::fpToFP().
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.
Produces a term that represents the conversion of the bit-vector term t
into a floating-point term of sort s
. The bit-vector t
is taken to be in signed 2's complement format. If necessary, the result will be rounded according to rounding mode rm
.
c | logical context |
rm | term of RoundingMode sort |
t | term of bit-vector sort |
s | floating-point sort |
s
must be a FloatingPoint sort, rm
must be of RoundingMode sort, t
must be of bit-vector sort.
Referenced by z3py::fpSignedToFP(), and z3py::fpToFP().
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.
Produces a term that represents the conversion of the bit-vector term t
into a floating-point term of sort s
. The bit-vector t
is taken to be in unsigned 2's complement format. If necessary, the result will be rounded according to rounding mode rm
.
c | logical context |
rm | term of RoundingMode sort |
t | term of bit-vector sort |
s | floating-point sort |
s
must be a FloatingPoint sort, rm
must be of RoundingMode sort, t
must be of bit-vector sort.
Referenced by z3py::fpToFPUnsigned(), and z3py::fpUnsignedToFP().
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.
c | logical context |
t | term of FloatingPoint sort |
t
must have FloatingPoint sort. The size of the resulting bit-vector is automatically determined.
Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion knows only one NaN and it will always produce the same bit-vector representation of that NaN.
Referenced by z3py::fpToIEEEBV().
Z3_ast Z3_API Z3_mk_fpa_to_real | ( | Z3_context | c, |
Z3_ast | t | ||
) |
Conversion of a floating-point term into a real-numbered term.
Produces a term that represents the conversion of the floating-point term t
into a real number. Note that this type of conversion will often result in non-linear constraints over real terms.
c | logical context |
t | term of FloatingPoint sort |
Referenced by z3py::fpToReal().
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.
Produces a term that represents the conversion of the floating-point term t
into a bit-vector term of size sz
in signed 2's complement format. If necessary, the result will be rounded according to rounding mode rm
.
c | logical context |
rm | term of RoundingMode sort |
t | term of FloatingPoint sort |
sz | size of the resulting bit-vector |
Referenced by z3py::fpToSBV().
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.
Produces a term that represents the conversion of the floating-point term t
into a bit-vector term of size sz
in unsigned 2's complement format. If necessary, the result will be rounded according to rounding mode rm
.
c | logical context |
rm | term of RoundingMode sort |
t | term of FloatingPoint sort |
sz | size of the resulting bit-vector |
Referenced by z3py::fpToUBV().
Z3_ast Z3_API Z3_mk_fpa_zero | ( | Z3_context | c, |
Z3_sort | s, | ||
bool | negative | ||
) |
Create a floating-point zero of sort s
.
c | logical context |
s | target sort |
negative | indicates whether the result should be negative |
When negative
is true
, -zero will be generated instead of +zero.
Referenced by z3py::fpMinusZero(), z3py::fpPlusZero(), and z3py::fpZero().