Z3
z3_fpa.h
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2013 Microsoft Corporation
3 
4 Module Name:
5 
6  z3_fpa.h
7 
8 Abstract:
9 
10  Additional APIs for floating-point arithmetic (FP).
11 
12 Author:
13 
14  Christoph M. Wintersteiger (cwinter) 2013-06-05
15 
16 Notes:
17 
18 --*/
19 #ifndef _Z3_FPA_H_
20 #define _Z3_FPA_H_
21 
22 #ifdef __cplusplus
23 extern "C" {
24 #endif // __cplusplus
25 
32 
37 
45 
53 
60  Z3_ast Z3_API Z3_mk_fpa_rne(__in Z3_context c);
61 
69 
76  Z3_ast Z3_API Z3_mk_fpa_rna(__in Z3_context c);
77 
85 
92  Z3_ast Z3_API Z3_mk_fpa_rtp(__in Z3_context c);
93 
101 
108  Z3_ast Z3_API Z3_mk_fpa_rtn(__in Z3_context c);
109 
117 
124  Z3_ast Z3_API Z3_mk_fpa_rtz(__in Z3_context c);
125 
136  Z3_sort Z3_API Z3_mk_fpa_sort(__in Z3_context c, __in unsigned ebits, __in unsigned sbits);
137 
144  Z3_sort Z3_API Z3_mk_fpa_sort_half(__in Z3_context c);
145 
152  Z3_sort Z3_API Z3_mk_fpa_sort_16(__in Z3_context c);
153 
161 
168  Z3_sort Z3_API Z3_mk_fpa_sort_32(__in Z3_context c);
169 
177 
184  Z3_sort Z3_API Z3_mk_fpa_sort_64(__in Z3_context c);
185 
193 
200  Z3_sort Z3_API Z3_mk_fpa_sort_128(__in Z3_context c);
201 
209  Z3_ast Z3_API Z3_mk_fpa_nan(__in Z3_context c, __in Z3_sort s);
210 
221  Z3_ast Z3_API Z3_mk_fpa_inf(__in Z3_context c, __in Z3_sort s, __in Z3_bool negative);
222 
233  Z3_ast Z3_API Z3_mk_fpa_zero(__in Z3_context c, __in Z3_sort s, __in Z3_bool negative);
234 
250  Z3_ast Z3_API Z3_mk_fpa_fp(__in Z3_context c, __in Z3_ast sgn, __in Z3_ast exp, __in Z3_ast sig);
251 
267  Z3_ast Z3_API Z3_mk_fpa_numeral_float(__in Z3_context c, __in float v, __in Z3_sort ty);
268 
284  Z3_ast Z3_API Z3_mk_fpa_numeral_double(__in Z3_context c, __in double v, __in Z3_sort ty);
285 
298  Z3_ast Z3_API Z3_mk_fpa_numeral_int(__in Z3_context c, __in signed v, Z3_sort ty);
299 
314  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);
315 
330  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);
331 
339  Z3_ast Z3_API Z3_mk_fpa_abs(__in Z3_context c, __in Z3_ast t);
340 
348  Z3_ast Z3_API Z3_mk_fpa_neg(__in Z3_context c, __in Z3_ast t);
349 
361  Z3_ast Z3_API Z3_mk_fpa_add(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2);
362 
374  Z3_ast Z3_API Z3_mk_fpa_sub(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2);
375 
387  Z3_ast Z3_API Z3_mk_fpa_mul(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2);
388 
400  Z3_ast Z3_API Z3_mk_fpa_div(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2);
401 
416  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);
417 
428  Z3_ast Z3_API Z3_mk_fpa_sqrt(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t);
429 
440  Z3_ast Z3_API Z3_mk_fpa_rem(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
441 
453  Z3_ast Z3_API Z3_mk_fpa_round_to_integral(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t);
454 
465  Z3_ast Z3_API Z3_mk_fpa_min(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
466 
477  Z3_ast Z3_API Z3_mk_fpa_max(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
478 
489  Z3_ast Z3_API Z3_mk_fpa_leq(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
490 
501  Z3_ast Z3_API Z3_mk_fpa_lt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
502 
513  Z3_ast Z3_API Z3_mk_fpa_geq(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
514 
525  Z3_ast Z3_API Z3_mk_fpa_gt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
526 
539  Z3_ast Z3_API Z3_mk_fpa_eq(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
540 
550  Z3_ast Z3_API Z3_mk_fpa_is_normal(__in Z3_context c, __in Z3_ast t);
551 
561  Z3_ast Z3_API Z3_mk_fpa_is_subnormal(__in Z3_context c, __in Z3_ast t);
562 
572  Z3_ast Z3_API Z3_mk_fpa_is_zero(__in Z3_context c, __in Z3_ast t);
573 
583  Z3_ast Z3_API Z3_mk_fpa_is_infinite(__in Z3_context c, __in Z3_ast t);
584 
594  Z3_ast Z3_API Z3_mk_fpa_is_nan(__in Z3_context c, __in Z3_ast t);
595 
605  Z3_ast Z3_API Z3_mk_fpa_is_negative(__in Z3_context c, __in Z3_ast t);
606 
616  Z3_ast Z3_API Z3_mk_fpa_is_positive(__in Z3_context c, __in Z3_ast t);
617 
633  Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(__in Z3_context c, __in Z3_ast bv, __in Z3_sort s);
634 
650  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);
651 
667  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);
668 
685  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);
686 
703  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);
704 
718  Z3_ast Z3_API Z3_mk_fpa_to_ubv(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in unsigned sz);
719 
733  Z3_ast Z3_API Z3_mk_fpa_to_sbv(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in unsigned sz);
734 
746  Z3_ast Z3_API Z3_mk_fpa_to_real(__in Z3_context c, __in Z3_ast t);
747 
748 
753 
761  unsigned Z3_API Z3_fpa_get_ebits(__in Z3_context c, __in Z3_sort s);
762 
770  unsigned Z3_API Z3_fpa_get_sbits(__in Z3_context c, __in Z3_sort s);
771 
782  Z3_bool Z3_API Z3_fpa_get_numeral_sign(__in Z3_context c, __in Z3_ast t, __out int * sgn);
783 
795 
804 
813  Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(__in Z3_context c, __in Z3_ast t, __out __int64 * n);
814 
829  Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(__in Z3_context c, __in Z3_ast t);
830 
847  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);
848 
852 
854 #ifdef __cplusplus
855 };
856 #endif // __cplusplus
857 
858 #endif
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.
Definition: z3_api.h:102
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.
#define __uint64
Definition: z3_api.h:59
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.
#define __int64
Definition: z3_api.h:55
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 *.
Definition: z3_api.h:111
Z3_ast Z3_API Z3_mk_fpa_abs(__in Z3_context c, __in Z3_ast t)
Floating-point absolute value.