Go to the source code of this file.
Functions | |
Floating-Point API | |
Z3_sort Z3_API | Z3_mk_fpa_rounding_mode_sort (__in Z3_context c) |
Create the RoundingMode sort. More... | |
Z3_ast Z3_API | Z3_mk_fpa_round_nearest_ties_to_even (__in Z3_context c) |
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. More... | |
Z3_ast Z3_API | Z3_mk_fpa_rne (__in 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 (__in Z3_context c) |
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. More... | |
Z3_ast Z3_API | Z3_mk_fpa_rna (__in 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 (__in Z3_context c) |
Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. More... | |
Z3_ast Z3_API | Z3_mk_fpa_rtp (__in 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 (__in Z3_context c) |
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. More... | |
Z3_ast Z3_API | Z3_mk_fpa_rtn (__in 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 (__in Z3_context c) |
Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. More... | |
Z3_ast Z3_API | Z3_mk_fpa_rtz (__in Z3_context c) |
Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. More... | |
Z3_sort Z3_API | Z3_mk_fpa_sort (__in Z3_context c, __in unsigned ebits, __in unsigned sbits) |
Create a FloatingPoint sort. More... | |
Z3_sort Z3_API | Z3_mk_fpa_sort_half (__in Z3_context c) |
Create the half-precision (16-bit) FloatingPoint sort. More... | |
Z3_sort Z3_API | Z3_mk_fpa_sort_16 (__in Z3_context c) |
Create the half-precision (16-bit) FloatingPoint sort. More... | |
Z3_sort Z3_API | Z3_mk_fpa_sort_single (__in Z3_context c) |
Create the single-precision (32-bit) FloatingPoint sort. More... | |
Z3_sort Z3_API | Z3_mk_fpa_sort_32 (__in Z3_context c) |
Create the single-precision (32-bit) FloatingPoint sort. More... | |
Z3_sort Z3_API | Z3_mk_fpa_sort_double (__in Z3_context c) |
Create the double-precision (64-bit) FloatingPoint sort. More... | |
Z3_sort Z3_API | Z3_mk_fpa_sort_64 (__in Z3_context c) |
Create the double-precision (64-bit) FloatingPoint sort. More... | |
Z3_sort Z3_API | Z3_mk_fpa_sort_quadruple (__in Z3_context c) |
Create the quadruple-precision (128-bit) FloatingPoint sort. More... | |
Z3_sort Z3_API | Z3_mk_fpa_sort_128 (__in Z3_context c) |
Create the quadruple-precision (128-bit) FloatingPoint sort. More... | |
Z3_ast Z3_API | Z3_mk_fpa_nan (__in Z3_context c, __in Z3_sort s) |
Create a floating-point NaN of sort s. More... | |
Z3_ast Z3_API | Z3_mk_fpa_inf (__in Z3_context c, __in Z3_sort s, __in Z3_bool negative) |
Create a floating-point infinity of sort s. More... | |
Z3_ast Z3_API | Z3_mk_fpa_zero (__in Z3_context c, __in Z3_sort s, __in Z3_bool negative) |
Create a floating-point zero of sort s. More... | |
Z3_ast Z3_API | Z3_mk_fpa_fp (__in Z3_context c, __in Z3_ast sgn, __in Z3_ast exp, __in Z3_ast sig) |
Create an expression of FloatingPoint sort from three bit-vector expressions. More... | |
Z3_ast Z3_API | Z3_mk_fpa_numeral_float (__in Z3_context c, __in float v, __in Z3_sort ty) |
Create a numeral of FloatingPoint sort from a float. More... | |
Z3_ast Z3_API | Z3_mk_fpa_numeral_double (__in Z3_context c, __in double v, __in Z3_sort ty) |
Create a numeral of FloatingPoint sort from a double. More... | |
Z3_ast Z3_API | Z3_mk_fpa_numeral_int (__in Z3_context c, __in 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 (__in Z3_context c, __in Z3_bool sgn, __in signed exp, __in 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 (__in Z3_context c, __in Z3_bool sgn, __in __int64 exp, __in __uint64 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 (__in Z3_context c, __in Z3_ast t) |
Floating-point absolute value. More... | |
Z3_ast Z3_API | Z3_mk_fpa_neg (__in Z3_context c, __in Z3_ast t) |
Floating-point negation. More... | |
Z3_ast Z3_API | Z3_mk_fpa_add (__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2) |
Floating-point addition. More... | |
Z3_ast Z3_API | Z3_mk_fpa_sub (__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2) |
Floating-point subtraction. More... | |
Z3_ast Z3_API | Z3_mk_fpa_mul (__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2) |
Floating-point multiplication. More... | |
Z3_ast Z3_API | Z3_mk_fpa_div (__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2) |
Floating-point division. More... | |
Z3_ast Z3_API | Z3_mk_fpa_fma (__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2, __in Z3_ast t3) |
Floating-point fused multiply-add. More... | |
Z3_ast Z3_API | Z3_mk_fpa_sqrt (__in Z3_context c, __in Z3_ast rm, __in Z3_ast t) |
Floating-point square root. More... | |
Z3_ast Z3_API | Z3_mk_fpa_rem (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2) |
Floating-point remainder. More... | |
Z3_ast Z3_API | Z3_mk_fpa_round_to_integral (__in Z3_context c, __in Z3_ast rm, __in 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 (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2) |
Minimum of floating-point numbers. More... | |
Z3_ast Z3_API | Z3_mk_fpa_max (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2) |
Maximum of floating-point numbers. More... | |
Z3_ast Z3_API | Z3_mk_fpa_leq (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2) |
Floating-point less than or equal. More... | |
Z3_ast Z3_API | Z3_mk_fpa_lt (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2) |
Floating-point less than. More... | |
Z3_ast Z3_API | Z3_mk_fpa_geq (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2) |
Floating-point greater than or equal. More... | |
Z3_ast Z3_API | Z3_mk_fpa_gt (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2) |
Floating-point greater than. More... | |
Z3_ast Z3_API | Z3_mk_fpa_eq (__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2) |
Floating-point equality. More... | |
Z3_ast Z3_API | Z3_mk_fpa_is_normal (__in Z3_context c, __in Z3_ast t) |
Predicate indicating whether t is a normal floating-point number. More... | |
Z3_ast Z3_API | Z3_mk_fpa_is_subnormal (__in Z3_context c, __in Z3_ast t) |
Predicate indicating whether t is a subnormal floating-point number. More... | |
Z3_ast Z3_API | Z3_mk_fpa_is_zero (__in Z3_context c, __in 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 (__in Z3_context c, __in 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 (__in Z3_context c, __in Z3_ast t) |
Predicate indicating whether t is a NaN. More... | |
Z3_ast Z3_API | Z3_mk_fpa_is_negative (__in Z3_context c, __in Z3_ast t) |
Predicate indicating whether t is a negative floating-point number. More... | |
Z3_ast Z3_API | Z3_mk_fpa_is_positive (__in Z3_context c, __in Z3_ast t) |
Predicate indicating whether t is a positive floating-point number. More... | |
Z3_ast Z3_API | Z3_mk_fpa_to_fp_bv (__in Z3_context c, __in Z3_ast bv, __in 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 (__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in 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 (__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in 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 (__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in 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 (__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in 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 (__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in unsigned sz) |
Conversion of a floating-point term into an unsigned bit-vector. More... | |
Z3_ast Z3_API | Z3_mk_fpa_to_sbv (__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in unsigned sz) |
Conversion of a floating-point term into a signed bit-vector. More... | |
Z3_ast Z3_API | Z3_mk_fpa_to_real (__in Z3_context c, __in 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 (__in Z3_context c, __in Z3_sort s) |
Retrieves the number of bits reserved for the exponent in a FloatingPoint sort. More... | |
unsigned Z3_API | Z3_fpa_get_sbits (__in Z3_context c, __in Z3_sort s) |
Retrieves the number of bits reserved for the significand in a FloatingPoint sort. More... | |
Z3_bool Z3_API | Z3_fpa_get_numeral_sign (__in Z3_context c, __in Z3_ast t, __out int *sgn) |
Retrieves the sign of a floating-point literal. More... | |
Z3_string Z3_API | Z3_fpa_get_numeral_significand_string (__in Z3_context c, __in Z3_ast t) |
Return the significand value of a floating-point numeral as a string. More... | |
Z3_string Z3_API | Z3_fpa_get_numeral_exponent_string (__in Z3_context c, __in Z3_ast t) |
Return the exponent value of a floating-point numeral as a string. More... | |
Z3_bool Z3_API | Z3_fpa_get_numeral_exponent_int64 (__in Z3_context c, __in Z3_ast t, __out __int64 *n) |
Return the exponent value of a floating-point numeral as a signed 64-bit integer. More... | |
Z3_ast Z3_API | Z3_mk_fpa_to_ieee_bv (__in Z3_context c, __in 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 (__in Z3_context c, __in Z3_ast rm, __in Z3_ast exp, __in Z3_ast sig, __in Z3_sort s) |
Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort. More... | |