z3_fpa.h File Reference

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

Generated on Sat Jan 14 2023 14:44:08 for Z3 by 1.9.1