Z3
 
Loading...
Searching...
No Matches
z3_fpa.h
Go to the documentation of this file.
1/*++
2Copyright (c) 2013 Microsoft Corporation
3
4Module Name:
5
6 z3_fpa.h
7
8Abstract:
9
10 Additional APIs for floating-point arithmetic (FP).
11
12Author:
13
14 Christoph M. Wintersteiger (cwinter) 2013-06-05
15
16Notes:
17
18--*/
19#pragma once
20
21#ifdef __cplusplus
22extern "C" {
23#endif // __cplusplus
24
42 Z3_sort Z3_API Z3_mk_fpa_rounding_mode_sort(Z3_context c);
43
58 Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_even(Z3_context c);
59
74 Z3_ast Z3_API Z3_mk_fpa_rne(Z3_context c);
75
90 Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_away(Z3_context c);
91
106 Z3_ast Z3_API Z3_mk_fpa_rna(Z3_context c);
107
122 Z3_ast Z3_API Z3_mk_fpa_round_toward_positive(Z3_context c);
123
138 Z3_ast Z3_API Z3_mk_fpa_rtp(Z3_context c);
139
154 Z3_ast Z3_API Z3_mk_fpa_round_toward_negative(Z3_context c);
155
170 Z3_ast Z3_API Z3_mk_fpa_rtn(Z3_context c);
171
186 Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(Z3_context c);
187
202 Z3_ast Z3_API Z3_mk_fpa_rtz(Z3_context c);
203
219 Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits);
220
234 Z3_sort Z3_API Z3_mk_fpa_sort_half(Z3_context c);
235
249 Z3_sort Z3_API Z3_mk_fpa_sort_16(Z3_context c);
250
264 Z3_sort Z3_API Z3_mk_fpa_sort_single(Z3_context c);
265
279 Z3_sort Z3_API Z3_mk_fpa_sort_32(Z3_context c);
280
294 Z3_sort Z3_API Z3_mk_fpa_sort_double(Z3_context c);
295
309 Z3_sort Z3_API Z3_mk_fpa_sort_64(Z3_context c);
310
324 Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(Z3_context c);
325
339 Z3_sort Z3_API Z3_mk_fpa_sort_128(Z3_context c);
340
352 Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s);
353
368 Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, bool negative);
369
384 Z3_ast Z3_API Z3_mk_fpa_zero(Z3_context c, Z3_sort s, bool negative);
385
408 Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig);
409
430 Z3_ast Z3_API Z3_mk_fpa_numeral_float(Z3_context c, float v, Z3_sort ty);
431
452 Z3_ast Z3_API Z3_mk_fpa_numeral_double(Z3_context c, double v, Z3_sort ty);
453
471 Z3_ast Z3_API Z3_mk_fpa_numeral_int(Z3_context c, signed v, Z3_sort ty);
472
492 Z3_ast Z3_API Z3_mk_fpa_numeral_int_uint(Z3_context c, bool sgn, signed exp, unsigned sig, Z3_sort ty);
493
513 Z3_ast Z3_API Z3_mk_fpa_numeral_int64_uint64(Z3_context c, bool sgn, int64_t exp, uint64_t sig, Z3_sort ty);
514
526 Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t);
527
539 Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t);
540
552 Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);
553
565 Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);
566
578 Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);
579
591 Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);
592
607 Z3_ast Z3_API Z3_mk_fpa_fma(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2, Z3_ast t3);
608
619 Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t);
620
631 Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2);
632
644 Z3_ast Z3_API Z3_mk_fpa_round_to_integral(Z3_context c, Z3_ast rm, Z3_ast t);
645
658 Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2);
659
672 Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2);
673
689 Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2);
690
706 Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2);
707
723 Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2);
724
740 Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2);
741
759 Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2);
760
775 Z3_ast Z3_API Z3_mk_fpa_is_normal(Z3_context c, Z3_ast t);
776
791 Z3_ast Z3_API Z3_mk_fpa_is_subnormal(Z3_context c, Z3_ast t);
792
808 Z3_ast Z3_API Z3_mk_fpa_is_zero(Z3_context c, Z3_ast t);
809
825 Z3_ast Z3_API Z3_mk_fpa_is_infinite(Z3_context c, Z3_ast t);
826
842 Z3_ast Z3_API Z3_mk_fpa_is_nan(Z3_context c, Z3_ast t);
843
857 Z3_ast Z3_API Z3_mk_fpa_is_negative(Z3_context c, Z3_ast t);
858
872 Z3_ast Z3_API Z3_mk_fpa_is_positive(Z3_context c, Z3_ast t);
873
889 Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(Z3_context c, Z3_ast bv, Z3_sort s);
890
906 Z3_ast Z3_API Z3_mk_fpa_to_fp_float(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s);
907
923 Z3_ast Z3_API Z3_mk_fpa_to_fp_real(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s);
924
941 Z3_ast Z3_API Z3_mk_fpa_to_fp_signed(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s);
942
959 Z3_ast Z3_API Z3_mk_fpa_to_fp_unsigned(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s);
960
974 Z3_ast Z3_API Z3_mk_fpa_to_ubv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz);
975
989 Z3_ast Z3_API Z3_mk_fpa_to_sbv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz);
990
1002 Z3_ast Z3_API Z3_mk_fpa_to_real(Z3_context c, Z3_ast t);
1003
1004
1016 unsigned Z3_API Z3_fpa_get_ebits(Z3_context c, Z3_sort s);
1017
1027 unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s);
1028
1041 bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t);
1042
1055 bool Z3_API Z3_fpa_is_numeral_inf(Z3_context c, Z3_ast t);
1056
1069 bool Z3_API Z3_fpa_is_numeral_zero(Z3_context c, Z3_ast t);
1070
1083 bool Z3_API Z3_fpa_is_numeral_normal(Z3_context c, Z3_ast t);
1084
1097 bool Z3_API Z3_fpa_is_numeral_subnormal(Z3_context c, Z3_ast t);
1098
1108 bool Z3_API Z3_fpa_is_numeral_positive(Z3_context c, Z3_ast t);
1109
1119 bool Z3_API Z3_fpa_is_numeral_negative(Z3_context c, Z3_ast t);
1120
1130 Z3_ast Z3_API Z3_fpa_get_numeral_sign_bv(Z3_context c, Z3_ast t);
1131
1141 Z3_ast Z3_API Z3_fpa_get_numeral_significand_bv(Z3_context c, Z3_ast t);
1142
1155 bool Z3_API Z3_fpa_get_numeral_sign(Z3_context c, Z3_ast t, int * sgn);
1156
1168 Z3_string Z3_API Z3_fpa_get_numeral_significand_string(Z3_context c, Z3_ast t);
1169
1182 bool Z3_API Z3_fpa_get_numeral_significand_uint64(Z3_context c, Z3_ast t, uint64_t * n);
1183
1196 Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t, bool biased);
1197
1211 bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, int64_t * n, bool biased);
1212
1224 Z3_ast Z3_API Z3_fpa_get_numeral_exponent_bv(Z3_context c, Z3_ast t, bool biased);
1225
1240 Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(Z3_context c, Z3_ast t);
1241
1258 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);
1263#ifdef __cplusplus
1264}
1265#endif // __cplusplus
1266
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.
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 s...
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.
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.
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.
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.
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.
bool Z3_API Z3_fpa_get_numeral_sign(Z3_context c, Z3_ast t, int *sgn)
Retrieves the sign of a floating-point literal.
Z3_ast Z3_API Z3_mk_fpa_rna(Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point subtraction.
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.
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.
Z3_sort Z3_API Z3_mk_fpa_sort_half(Z3_context c)
Create the half-precision (16-bit) FloatingPoint sort.
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.
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.
bool Z3_API Z3_fpa_is_numeral_positive(Z3_context c, Z3_ast t)
Checks whether a given floating-point numeral is positive.
Z3_ast Z3_API Z3_mk_fpa_rtn(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
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.
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.
Z3_ast Z3_API Z3_mk_fpa_rtp(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t)
Checks whether a given floating-point numeral is a NaN.
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.
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition z3_api.h:53
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.
Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2)
Maximum of floating-point numbers.
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.
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.
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.
Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, bool negative)
Create a floating-point infinity of sort s.
Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s)
Create a floating-point NaN of sort s.
bool Z3_API Z3_fpa_is_numeral_subnormal(Z3_context c, Z3_ast t)
Checks whether a given floating-point numeral is subnormal.
Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than.
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.
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.
Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point equality.
Z3_sort Z3_API Z3_mk_fpa_sort_16(Z3_context c)
Create the half-precision (16-bit) FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than or equal.
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.
Z3_ast Z3_API Z3_mk_fpa_rtz(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
bool Z3_API Z3_fpa_is_numeral_negative(Z3_context c, Z3_ast t)
Checks whether a given floating-point numeral is negative.
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.
Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(Z3_context c)
Create the quadruple-precision (128-bit) 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.
Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point remainder.
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.
Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2)
Minimum of floating-point numbers.
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,...
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.
Z3_sort Z3_API Z3_mk_fpa_sort_128(Z3_context c)
Create the quadruple-precision (128-bit) FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point addition.
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.
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.
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.
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.
Z3_ast Z3_API Z3_mk_fpa_is_nan(Z3_context c, Z3_ast t)
Predicate indicating whether t is a NaN.
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.
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.
Z3_sort Z3_API Z3_mk_fpa_sort_single(Z3_context c)
Create the single-precision (32-bit) FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.
Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than.
Z3_sort Z3_API Z3_mk_fpa_sort_32(Z3_context c)
Create the single-precision (32-bit) FloatingPoint sort.
Z3_sort Z3_API Z3_mk_fpa_sort_64(Z3_context c)
Create the double-precision (64-bit) FloatingPoint sort.
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.
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.
Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than or equal.
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.
Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point multiplication.
Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point division.
Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits)
Create a FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point square root.
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.
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.
bool Z3_API Z3_fpa_is_numeral_normal(Z3_context c, Z3_ast t)
Checks whether a given floating-point numeral is normal.
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.
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.
Z3_ast Z3_API Z3_mk_fpa_zero(Z3_context c, Z3_sort s, bool negative)
Create a floating-point zero of sort s.
Z3_sort Z3_API Z3_mk_fpa_rounding_mode_sort(Z3_context c)
Create the RoundingMode sort.
Z3_ast Z3_API Z3_mk_fpa_rne(Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
Z3_sort Z3_API Z3_mk_fpa_sort_double(Z3_context c)
Create the double-precision (64-bit) FloatingPoint sort.
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.
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.