|
Z3
|
|
|
Z3
|
|
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... | |
1.9.1