856 #endif // __cplusplus
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.
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.
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.
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.
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.
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...
Z3_sort Z3_API Z3_mk_fpa_rounding_mode_sort(__in Z3_context c)
Create the RoundingMode sort.
Z3_sort Z3_API Z3_mk_fpa_sort_32(__in Z3_context c)
Create the single-precision (32-bit) FloatingPoint sort.
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. ...
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.
int Z3_bool
Z3 Boolean type. It is just an alias for int.
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.
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.
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.
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.
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.
Z3_sort Z3_API Z3_mk_fpa_sort(__in Z3_context c, __in unsigned ebits, __in unsigned sbits)
Create a FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_rna(__in Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode...
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.
Z3_ast Z3_API Z3_mk_fpa_nan(__in Z3_context c, __in Z3_sort s)
Create a floating-point NaN of sort s.
Z3_ast Z3_API Z3_mk_fpa_eq(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Floating-point equality.
Z3_ast Z3_API Z3_mk_fpa_is_nan(__in Z3_context c, __in Z3_ast t)
Predicate indicating whether t is a NaN.
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.
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.
Z3_sort Z3_API Z3_mk_fpa_sort_64(__in Z3_context c)
Create the double-precision (64-bit) FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_rtn(__in Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode...
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.
Z3_sort Z3_API Z3_mk_fpa_sort_half(__in Z3_context c)
Create the half-precision (16-bit) FloatingPoint sort.
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.
Z3_sort Z3_API Z3_mk_fpa_sort_128(__in Z3_context c)
Create the quadruple-precision (128-bit) FloatingPoint sort.
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.
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...
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...
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...
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.
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.
Z3_ast Z3_API Z3_mk_fpa_sqrt(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t)
Floating-point square root.
Z3_ast Z3_API Z3_mk_fpa_rne(__in Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode...
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.
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.
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.
Z3_ast Z3_API Z3_mk_fpa_rtp(__in Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode...
Z3_sort Z3_API Z3_mk_fpa_sort_single(__in Z3_context c)
Create the single-precision (32-bit) FloatingPoint sort.
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.
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.
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.
Z3_ast Z3_API Z3_mk_fpa_rem(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Floating-point remainder.
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.
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.
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.
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.
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.
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.
Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(__in Z3_context c)
Create the quadruple-precision (128-bit) FloatingPoint sort.
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.
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.
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...
Z3_ast Z3_API Z3_mk_fpa_neg(__in Z3_context c, __in Z3_ast t)
Floating-point negation.
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 s...
Z3_ast Z3_API Z3_mk_fpa_rtz(__in Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
Z3_sort Z3_API Z3_mk_fpa_sort_double(__in Z3_context c)
Create the double-precision (64-bit) FloatingPoint sort.
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...
Z3_ast Z3_API Z3_mk_fpa_lt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Floating-point less than.
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.
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.
Z3_sort Z3_API Z3_mk_fpa_sort_16(__in Z3_context c)
Create the half-precision (16-bit) FloatingPoint sort.
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...
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.
Z3_ast Z3_API Z3_mk_fpa_gt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2)
Floating-point greater than.
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Z3_ast Z3_API Z3_mk_fpa_abs(__in Z3_context c, __in Z3_ast t)
Floating-point absolute value.