Z3 |

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

## Function Documentation

## ◆ Z3_fpa_get_ebits()

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.

Parameters

  c | logical context
  s | FloatingPoint sort

Referenced by FPSortRef::ebits(), and sort::fpa_ebits().

## ◆ Z3_fpa_get_numeral_exponent_bv()

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.

Parameters

  c | logical context
  t | a floating-point numeral
  biased | flag to indicate whether the result is in biased representation

Remarks: This function extracts the exponent in `t`, without normalization. NaN is an invalid arguments.

Referenced by FPNumRef::exponent_as_bv().

## ◆ Z3_fpa_get_numeral_exponent_int64()

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.

Parameters

  c | logical context
  t | a floating-point numeral
  n | exponent
  biased | flag to indicate whether the result is in biased representation

Returns
  true if `t` corresponds to a floating point numeral, otherwise invokes exception handler or returns false

Remarks: This function extracts the exponent in `t`, without normalization. NaN is an invalid argument.

Referenced by FPNumRef::exponent_as_long().

## ◆ Z3_fpa_get_numeral_exponent_string()

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.

Parameters

  c | logical context
  t | a floating-point numeral
  biased | flag to indicate whether the result is in biased representation

Returns
  true if `t` corresponds to a floating point numeral, otherwise invokes exception handler or returns false

Remarks: This function extracts the exponent in `t`, without normalization. NaN is an invalid argument.

Referenced by FPNumRef::exponent().

## ◆ Z3_fpa_get_numeral_sign()

bool Z3_API Z3_fpa_get_numeral_sign | ( | Z3_context | c,
|  | Z3_ast | t,
|  | int * | sgn
| ) |  |

Retrieves the sign of a floating-point literal.

Parameters

  c | logical context
  t | a floating-point numeral
  sgn | the retrieved sign

Returns
  true if `t` corresponds to a floating point numeral, otherwise invokes exception handler or returns false

Remarks: sets `sgn` to 0 if ‘t’ is positive and to 1 otherwise, except for NaN, which is an invalid argument.

Referenced by FPNumRef::sign().

## ◆ Z3_fpa_get_numeral_sign_bv()

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.

Parameters

  c | logical context
  t | a floating-point numeral

Remarks: NaN is an invalid argument.

Referenced by FPNumRef::sign_as_bv().

## ◆ Z3_fpa_get_numeral_significand_bv()

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.

Parameters

  c | logical context
  t | a floating-point numeral

Remarks: NaN is an invalid argument.

Referenced by FPNumRef::significand_as_bv().

## ◆ Z3_fpa_get_numeral_significand_string()

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.

Parameters

  c | logical context
  t | a floating-point numeral

Returns
  true if `t` corresponds to a floating point numeral, otherwise invokes exception handler or returns false

Remarks: The significand `s` is always `0.0 <= s < 2.0`; the resulting string is long enough to represent the real significand precisely.

Referenced by FPNumRef::significand().

## ◆ Z3_fpa_get_numeral_significand_uint64()

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.

Parameters

  c | logical context
  t | a floating-point numeral
  n | pointer to output uint64

Remarks: This function extracts the significand bits in `t`, without the hidden bit or normalization. Sets the `Z3_INVALID_ARG` error code if the significand does not fit into a `uint64`. NaN is an invalid argument.

Referenced by FPNumRef::significand_as_long().

## ◆ Z3_fpa_get_sbits()

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.

Parameters

  c | logical context
  s | FloatingPoint sort

Referenced by sort::fpa_sbits(), and FPSortRef::sbits().

## ◆ Z3_fpa_is_numeral_inf()

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.

Parameters

  c | logical context
  t | a floating-point numeral

Referenced by FPNumRef::isInf().

## ◆ Z3_fpa_is_numeral_nan()

bool Z3_API Z3_fpa_is_numeral_nan | ( | Z3_context | c,
|  | Z3_ast | t
| ) |  |

Checks whether a given floating-point numeral is a NaN.

Parameters

  c | logical context
  t | a floating-point numeral

Referenced by FPNumRef::isNaN().

## ◆ Z3_fpa_is_numeral_negative()

bool Z3_API Z3_fpa_is_numeral_negative | ( | Z3_context | c,
|  | Z3_ast | t
| ) |  |

Checks whether a given floating-point numeral is negative.

Parameters

  c | logical context
  t | a floating-point numeral

Referenced by FPNumRef::isNegative().

## ◆ Z3_fpa_is_numeral_normal()

bool Z3_API Z3_fpa_is_numeral_normal | ( | Z3_context | c,
|  | Z3_ast | t
| ) |  |

Checks whether a given floating-point numeral is normal.

Parameters

  c | logical context
  t | a floating-point numeral

Referenced by FPNumRef::isNormal().

## ◆ Z3_fpa_is_numeral_positive()

bool Z3_API Z3_fpa_is_numeral_positive | ( | Z3_context | c,
|  | Z3_ast | t
| ) |  |

Checks whether a given floating-point numeral is positive.

Parameters

  c | logical context
  t | a floating-point numeral

Referenced by FPNumRef::isPositive().

## ◆ Z3_fpa_is_numeral_subnormal()

bool Z3_API Z3_fpa_is_numeral_subnormal | ( | Z3_context | c,
|  | Z3_ast | t
| ) |  |

Checks whether a given floating-point numeral is subnormal.

Parameters

  c | logical context
  t | a floating-point numeral

Referenced by FPNumRef::isSubnormal().

## ◆ Z3_fpa_is_numeral_zero()

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.

Parameters

  c | logical context
  t | a floating-point numeral

Referenced by FPNumRef::isZero().

## ◆ Z3_mk_fpa_abs()

Z3_ast Z3_API Z3_mk_fpa_abs | ( | Z3_context | c,
|  | Z3_ast | t
| ) |  |

Floating-point absolute value.

Parameters

  c | logical context
  t | term of FloatingPoint sort

Referenced by z3py::fpAbs().

## ◆ Z3_mk_fpa_add()

Z3_ast Z3_API Z3_mk_fpa_add | ( | Z3_context | c,
|  | Z3_ast | rm,
|  | Z3_ast | t1,
|  | Z3_ast | t2
| ) |  |

Floating-point addition.

Parameters

  c | logical context
  rm | term of RoundingMode sort
  t1 | term of FloatingPoint sort
  t2 | term of FloatingPoint sort

`rm` must be of RoundingMode sort, `t1` and `t2` must have the same FloatingPoint sort.

## ◆ Z3_mk_fpa_div()

Z3_ast Z3_API Z3_mk_fpa_div | ( | Z3_context | c,
|  | Z3_ast | rm,
|  | Z3_ast | t1,
|  | Z3_ast | t2
| ) |  |

Floating-point division.

Parameters

  c | logical context
  rm | term of RoundingMode sort
  t1 | term of FloatingPoint sort.
  t2 | term of FloatingPoint sort

The nodes `rm` must be of RoundingMode sort, `t1` and `t2` must have the same FloatingPoint sort.

## ◆ Z3_mk_fpa_eq()

Z3_ast Z3_API Z3_mk_fpa_eq | ( | Z3_context | c,
|  | Z3_ast | t1,
|  | Z3_ast | t2
| ) |  |

Floating-point equality.

Parameters

  c | logical context
  t1 | term of FloatingPoint sort
  t2 | term of FloatingPoint sort

Note that this is IEEE 754 equality (as opposed to SMT-LIB `=`).

`t1` and `t2` must have the same FloatingPoint sort.

## ◆ Z3_mk_fpa_fma()

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.

Parameters

  c | logical context
  rm | term of RoundingMode sort
  t1 | term of FloatingPoint sort
  t2 | term of FloatingPoint sort
  t3 | term of FloatingPoint sort

The result is `round((t1 * t2) + t3)`.

`rm` must be of RoundingMode sort, `t1`, `t2`, and `t3` must have the same FloatingPoint sort.

## ◆ Z3_mk_fpa_fp()

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.

This is the operator named ‘fp’ in the SMT FP theory definition. Note that `sgn` is required to be a bit-vector of size 1. Significand and exponent are required to be longer than 1 and 2 respectively. The FloatingPoint sort of the resulting expression is automatically determined from the bit-vector sizes of the arguments. The exponent is assumed to be in IEEE-754 biased representation.

Parameters

  c | logical context
  sgn | sign
  exp | exponent
  sig | significand

See also
  Z3_mk_fpa_numeral_double
  Z3_mk_fpa_numeral_float
  Z3_mk_fpa_numeral_int
  Z3_mk_fpa_numeral_int_uint
  Z3_mk_fpa_numeral_int64_uint64
  Z3_mk_numeral

Referenced by z3py::fpFP().

## ◆ Z3_mk_fpa_geq()

Z3_ast Z3_API Z3_mk_fpa_geq | ( | Z3_context | c,
|  | Z3_ast | t1,
|  | Z3_ast | t2
| ) |  |

Floating-point greater than or equal.

Parameters

  c | logical context
  t1 | term of FloatingPoint sort
  t2 | term of FloatingPoint sort

`t1` and `t2` must have the same FloatingPoint sort.

## ◆ Z3_mk_fpa_gt()

Z3_ast Z3_API Z3_mk_fpa_gt | ( | Z3_context | c,
|  | Z3_ast | t1,
|  | Z3_ast | t2
| ) |  |

Floating-point greater than.

Parameters

  c | logical context
  t1 | term of FloatingPoint sort
  t2 | term of FloatingPoint sort

`t1` and `t2` must have the same FloatingPoint sort.

## ◆ Z3_mk_fpa_inf()

Z3_ast Z3_API Z3_mk_fpa_inf | ( | Z3_context | c,
|  | Z3_sort | s,
|  | bool | negative
| ) |  |

Create a floating-point infinity of sort `s`.

Parameters

  c | logical context
  s | target sort
  negative | indicates whether the result should be negative

When `negative` is `true`, -oo will be generated instead of +oo.

See also
  Z3_mk_fpa_nan
  Z3_mk_fpa_zero

Referenced by context::fpa_inf(), z3py::fpInfinity(), z3py::fpMinusInfinity(), and z3py::fpPlusInfinity().

## ◆ Z3_mk_fpa_is_infinite()

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.

Parameters

  c | logical context
  t | term of FloatingPoint sort

`t` must have FloatingPoint sort.

Referenced by expr::mk_is_inf().

## ◆ Z3_mk_fpa_is_nan()

Z3_ast Z3_API Z3_mk_fpa_is_nan | ( | Z3_context | c,
|  | Z3_ast | t
| ) |  |

Predicate indicating whether `t` is a NaN.

Parameters

  c | logical context
  t | term of FloatingPoint sort

`t` must have FloatingPoint sort.

Referenced by expr::mk_is_nan().

## ◆ Z3_mk_fpa_is_negative()

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.

Parameters

  c | logical context
  t | term of FloatingPoint sort

`t` must have FloatingPoint sort.

## ◆ Z3_mk_fpa_is_normal()

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.

Parameters

  c | logical context
  t | term of FloatingPoint sort

`t` must have FloatingPoint sort.

Referenced by expr::mk_is_normal().

## ◆ Z3_mk_fpa_is_positive()

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.

Parameters

  c | logical context
  t | term of FloatingPoint sort

`t` must have FloatingPoint sort.

## ◆ Z3_mk_fpa_is_subnormal()

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.

Parameters

  c | logical context
  t | term of FloatingPoint sort

`t` must have FloatingPoint sort.

Referenced by expr::mk_is_subnormal().

## ◆ Z3_mk_fpa_is_zero()

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.

Parameters

  c | logical context
  t | term of FloatingPoint sort

`t` must have FloatingPoint sort.

Referenced by expr::mk_is_zero().

## ◆ Z3_mk_fpa_leq()

Z3_ast Z3_API Z3_mk_fpa_leq | ( | Z3_context | c,
|  | Z3_ast | t1,
|  | Z3_ast | t2
| ) |  |

Floating-point less than or equal.

Parameters

  c | logical context
  t1 | term of FloatingPoint sort
  t2 | term of FloatingPoint sort

`t1` and `t2` must have the same FloatingPoint sort.

## ◆ Z3_mk_fpa_lt()

Z3_ast Z3_API Z3_mk_fpa_lt | ( | Z3_context | c,
|  | Z3_ast | t1,
|  | Z3_ast | t2
| ) |  |

Floating-point less than.

Parameters

  c | logical context
  t1 | term of FloatingPoint sort
  t2 | term of FloatingPoint sort

`t1` and `t2` must have the same FloatingPoint sort.

## ◆ Z3_mk_fpa_max()

Z3_ast Z3_API Z3_mk_fpa_max | ( | Z3_context | c,
|  | Z3_ast | t1,
|  | Z3_ast | t2
| ) |  |

Maximum of floating-point numbers.

Parameters

  c | logical context
  t1 | term of FloatingPoint sort
  t2 | term of FloatingPoint sort

`t1`, `t2` must have the same FloatingPoint sort.

## ◆ Z3_mk_fpa_min()

Z3_ast Z3_API Z3_mk_fpa_min | ( | Z3_context | c,
|  | Z3_ast | t1,
|  | Z3_ast | t2
| ) |  |

Minimum of floating-point numbers.

Parameters

  c | logical context
  t1 | term of FloatingPoint sort
  t2 | term of FloatingPoint sort

`t1`, `t2` must have the same FloatingPoint sort.

## ◆ Z3_mk_fpa_mul()

Z3_ast Z3_API Z3_mk_fpa_mul | ( | Z3_context | c,
|  | Z3_ast | rm,
|  | Z3_ast | t1,
|  | Z3_ast | t2
| ) |  |

Floating-point multiplication.

Parameters

  c | logical context
  rm | term of RoundingMode sort
  t1 | term of FloatingPoint sort
  t2 | term of FloatingPoint sort

`rm` must be of RoundingMode sort, `t1` and `t2` must have the same FloatingPoint sort.

## ◆ Z3_mk_fpa_nan()

Z3_ast Z3_API Z3_mk_fpa_nan | ( | Z3_context | c,
|  | Z3_sort | s
| ) |  |

Create a floating-point NaN of sort `s`.

Parameters

  c | logical context
  s | target sort

See also
  Z3_mk_fpa_inf
  Z3_mk_fpa_zero

Referenced by context::fpa_nan(), and z3py::fpNaN().

## ◆ Z3_mk_fpa_neg()

Z3_ast Z3_API Z3_mk_fpa_neg | ( | Z3_context | c,
|  | Z3_ast | t
| ) |  |

Floating-point negation.

Parameters

  c | logical context
  t | term of FloatingPoint sort

Referenced by z3py::fpNeg().

## ◆ Z3_mk_fpa_numeral_double()

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.

This function is used to create numerals that fit in a double value. It is slightly faster than Z3_mk_numeral since it is not necessary to parse a string.

Parameters

  c | logical context
  v | value
  ty | sort

`ty` must be a FloatingPoint sort

See also
  Z3_mk_fpa_fp
  Z3_mk_fpa_numeral_float
  Z3_mk_fpa_numeral_int
  Z3_mk_fpa_numeral_int_uint
  Z3_mk_fpa_numeral_int64_uint64
  Z3_mk_numeral

Referenced by context::fpa_val().

## ◆ Z3_mk_fpa_numeral_float()

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.

This function is used to create numerals that fit in a float value. It is slightly faster than Z3_mk_numeral since it is not necessary to parse a string.

Parameters

  c | logical context
  v | value
  ty | sort

`ty` must be a FloatingPoint sort

See also
  Z3_mk_fpa_fp
  Z3_mk_fpa_numeral_double
  Z3_mk_fpa_numeral_int
  Z3_mk_fpa_numeral_int_uint
  Z3_mk_fpa_numeral_int64_uint64
  Z3_mk_numeral

Referenced by context::fpa_val().

## ◆ Z3_mk_fpa_numeral_int()

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.

Parameters

  c | logical context
  v | value
  ty | result sort

`ty` must be a FloatingPoint sort

See also
  Z3_mk_fpa_fp
  Z3_mk_fpa_numeral_double
  Z3_mk_fpa_numeral_float
  Z3_mk_fpa_numeral_int_uint
  Z3_mk_fpa_numeral_int64_uint64
  Z3_mk_numeral

## ◆ Z3_mk_fpa_numeral_int64_uint64()

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.

Parameters

  c | logical context
  sgn | sign bit (true == negative)
  sig | significand
  exp | exponent
  ty | result sort

`ty` must be a FloatingPoint sort

See also
  Z3_mk_fpa_fp
  Z3_mk_fpa_numeral_double
  Z3_mk_fpa_numeral_float
  Z3_mk_fpa_numeral_int
  Z3_mk_fpa_numeral_int_uint
  Z3_mk_numeral

## ◆ Z3_mk_fpa_numeral_int_uint()

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.

Parameters

  c | logical context
  sgn | sign bit (true == negative)
  sig | significand
  exp | exponent
  ty | result sort

`ty` must be a FloatingPoint sort

See also
  Z3_mk_fpa_fp
  Z3_mk_fpa_numeral_double
  Z3_mk_fpa_numeral_float
  Z3_mk_fpa_numeral_int
  Z3_mk_fpa_numeral_int64_uint64
  Z3_mk_numeral

## ◆ Z3_mk_fpa_rem()

Z3_ast Z3_API Z3_mk_fpa_rem | ( | Z3_context | c,
|  | Z3_ast | t1,
|  | Z3_ast | t2
| ) |  |

Floating-point remainder.

Parameters

  c | logical context
  t1 | term of FloatingPoint sort
  t2 | term of FloatingPoint sort

`t1` and `t2` must have the same FloatingPoint sort.

## ◆ Z3_mk_fpa_rna()

Z3_ast Z3_API Z3_mk_fpa_rna | ( | Z3_context | c | ) |

Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.

Parameters

  c | logical context

Referenced by context::fpa_rounding_mode().

## ◆ Z3_mk_fpa_rne()

Z3_ast Z3_API Z3_mk_fpa_rne | ( | Z3_context | c | ) |

Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.

Parameters

  c | logical context

Referenced by context::fpa_rounding_mode().

## ◆ Z3_mk_fpa_round_nearest_ties_to_away()

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.

Parameters

  c | logical context

Referenced by z3py::RNA(), and z3py::RoundNearestTiesToAway().

## ◆ Z3_mk_fpa_round_nearest_ties_to_even()

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.

Parameters

  c | logical context

Referenced by z3py::RNE(), and z3py::RoundNearestTiesToEven().

## ◆ Z3_mk_fpa_round_to_integral()

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.

Parameters

  c | logical context
  rm | term of RoundingMode sort
  t | term of FloatingPoint sort

`t` must be of FloatingPoint sort.

## ◆ Z3_mk_fpa_round_toward_negative()

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.

Parameters

  c | logical context

Referenced by z3py::RoundTowardNegative(), and z3py::RTN().

## ◆ Z3_mk_fpa_round_toward_positive()

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.

Parameters

  c | logical context

Referenced by z3py::RoundTowardPositive(), and z3py::RTP().

## ◆ Z3_mk_fpa_round_toward_zero()

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.

Parameters

  c | logical context

Referenced by z3py::RoundTowardZero(), and z3py::RTZ().

## ◆ Z3_mk_fpa_rounding_mode_sort()

Z3_sort Z3_API Z3_mk_fpa_rounding_mode_sort | ( | Z3_context | c | ) |

Create the RoundingMode sort.

Parameters

  c | logical context

Referenced by context::fpa_rounding_mode_sort().

## ◆ Z3_mk_fpa_rtn()

Z3_ast Z3_API Z3_mk_fpa_rtn | ( | Z3_context | c | ) |

Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.

Parameters

  c | logical context

Referenced by context::fpa_rounding_mode().

## ◆ Z3_mk_fpa_rtp()

Z3_ast Z3_API Z3_mk_fpa_rtp | ( | Z3_context | c | ) |

Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.

Parameters

  c | logical context

Referenced by context::fpa_rounding_mode().

## ◆ Z3_mk_fpa_rtz()

Z3_ast Z3_API Z3_mk_fpa_rtz | ( | Z3_context | c | ) |

Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.

Parameters

  c | logical context

Referenced by context::fpa_rounding_mode().

## ◆ Z3_mk_fpa_sort()

Z3_sort Z3_API Z3_mk_fpa_sort | ( | Z3_context | c,
|  | unsigned | ebits,
|  | unsigned | sbits
| ) |  |

Create a FloatingPoint sort.

Parameters

  c | logical context
  ebits | number of exponent bits
  sbits | number of significand bits

Remarks
  `ebits` must be larger than 1 and `sbits` must be larger than 2.

Referenced by context::fpa_sort(), and z3py::FPSort().

## ◆ Z3_mk_fpa_sort_128()

Z3_sort Z3_API Z3_mk_fpa_sort_128 | ( | Z3_context | c | ) |

Create the quadruple-precision (128-bit) FloatingPoint sort.

Parameters

  c | logical context

Referenced by z3py::Float128().

## ◆ Z3_mk_fpa_sort_16()

Z3_sort Z3_API Z3_mk_fpa_sort_16 | ( | Z3_context | c | ) |

Create the half-precision (16-bit) FloatingPoint sort.

Parameters

  c | logical context

Referenced by z3py::Float16().

## ◆ Z3_mk_fpa_sort_32()

Z3_sort Z3_API Z3_mk_fpa_sort_32 | ( | Z3_context | c | ) |

Create the single-precision (32-bit) FloatingPoint sort.

Parameters

  c | logical context

Referenced by z3py::Float32().

## ◆ Z3_mk_fpa_sort_64()

Z3_sort Z3_API Z3_mk_fpa_sort_64 | ( | Z3_context | c | ) |

Create the double-precision (64-bit) FloatingPoint sort.

Parameters

  c | logical context

Referenced by z3py::Float64().

## ◆ Z3_mk_fpa_sort_double()

Z3_sort Z3_API Z3_mk_fpa_sort_double | ( | Z3_context | c | ) |

Create the double-precision (64-bit) FloatingPoint sort.

Parameters

  c | logical context

Referenced by z3py::FloatDouble().

## ◆ Z3_mk_fpa_sort_half()

Z3_sort Z3_API Z3_mk_fpa_sort_half | ( | Z3_context | c | ) |

Create the half-precision (16-bit) FloatingPoint sort.

Parameters

  c | logical context

Referenced by z3py::FloatHalf().

## ◆ Z3_mk_fpa_sort_quadruple()

Z3_sort Z3_API Z3_mk_fpa_sort_quadruple | ( | Z3_context | c | ) |

Create the quadruple-precision (128-bit) FloatingPoint sort.

Parameters

  c | logical context

Referenced by z3py::FloatQuadruple().

## ◆ Z3_mk_fpa_sort_single()

Z3_sort Z3_API Z3_mk_fpa_sort_single | ( | Z3_context | c | ) |

Create the single-precision (32-bit) FloatingPoint sort.

Parameters

  c | logical context.

Referenced by z3py::FloatSingle().

## ◆ Z3_mk_fpa_sqrt()

Z3_ast Z3_API Z3_mk_fpa_sqrt | ( | Z3_context | c,
|  | Z3_ast | rm,
|  | Z3_ast | t
| ) |  |

Floating-point square root.

Parameters

  c | logical context
  rm | term of RoundingMode sort
  t | term of FloatingPoint sort

`rm` must be of RoundingMode sort, `t` must have FloatingPoint sort.

## ◆ Z3_mk_fpa_sub()

Z3_ast Z3_API Z3_mk_fpa_sub | ( | Z3_context | c,
|  | Z3_ast | rm,
|  | Z3_ast | t1,
|  | Z3_ast | t2
| ) |  |

Floating-point subtraction.

Parameters

  c | logical context
  rm | term of RoundingMode sort
  t1 | term of FloatingPoint sort
  t2 | term of FloatingPoint sort

`rm` must be of RoundingMode sort, `t1` and `t2` must have the same FloatingPoint sort.

## ◆ Z3_mk_fpa_to_fp_bv()

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.

Produces a term that represents the conversion of a bit-vector term `bv` to a floating-point term of sort `s`.

Parameters

  c | logical context
  bv | a bit-vector term
  s | floating-point sort

`s` must be a FloatingPoint sort, `t` must be of bit-vector sort, and the bit-vector size of `bv` must be equal to `ebits+sbits` of `s`. The format of the bit-vector is as defined by the IEEE 754-2008 interchange format.

Referenced by z3py::fpBVToFP(), z3py::fpToFP(), and expr::mk_from_ieee_bv().

## ◆ Z3_mk_fpa_to_fp_float()

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.

Produces a term that represents the conversion of a floating-point term `t` to a floating-point term of sort `s`. If necessary, the result will be rounded according to rounding mode `rm`.

Parameters

  c | logical context
  rm | term of RoundingMode sort
  t | term of FloatingPoint sort
  s | floating-point sort

`s` must be a FloatingPoint sort, `rm` must be of RoundingMode sort, `t` must be of floating-point sort.

Referenced by z3py::fpFPToFP(), and z3py::fpToFP().

## ◆ Z3_mk_fpa_to_fp_int_real()

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.

Produces a term that represents the conversion of `sig * 2^exp` into a floating-point term of sort `s`. If necessary, the result will be rounded according to rounding mode `rm`.

Parameters

  c | logical context
  rm | term of RoundingMode sort
  exp | exponent term of Int sort
  sig | significand term of Real sort
  s | FloatingPoint sort

`s` must be a FloatingPoint sort, `rm` must be of RoundingMode sort, `exp` must be of int sort, `sig` must be of real sort.

## ◆ Z3_mk_fpa_to_fp_real()

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.

Produces a term that represents the conversion of term `t` of real sort into a floating-point term of sort `s`. If necessary, the result will be rounded according to rounding mode `rm`.

Parameters

  c | logical context
  rm | term of RoundingMode sort
  t | term of Real sort
  s | floating-point sort

`s` must be a FloatingPoint sort, `rm` must be of RoundingMode sort, `t` must be of real sort.

Referenced by z3py::fpRealToFP(), and z3py::fpToFP().

## ◆ Z3_mk_fpa_to_fp_signed()

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.

Produces a term that represents the conversion of the bit-vector term `t` into a floating-point term of sort `s`. The bit-vector `t` is taken to be in signed 2's complement format. If necessary, the result will be rounded according to rounding mode `rm`.

Parameters

  c | logical context
  rm | term of RoundingMode sort
  t | term of bit-vector sort
  s | floating-point sort

`s` must be a FloatingPoint sort, `rm` must be of RoundingMode sort, `t` must be of bit-vector sort.

Referenced by z3py::fpSignedToFP(), and z3py::fpToFP().

## ◆ Z3_mk_fpa_to_fp_unsigned()

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.

Produces a term that represents the conversion of the bit-vector term `t` into a floating-point term of sort `s`. The bit-vector `t` is taken to be in unsigned 2's complement format. If necessary, the result will be rounded according to rounding mode `rm`.

Parameters

  c | logical context
  rm | term of RoundingMode sort
  t | term of bit-vector sort
  s | floating-point sort

`s` must be a FloatingPoint sort, `rm` must be of RoundingMode sort, `t` must be of bit-vector sort.

Referenced by z3py::fpToFPUnsigned(), and z3py::fpUnsignedToFP().

## ◆ Z3_mk_fpa_to_ieee_bv()

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.

Parameters

  c | logical context
  t | term of FloatingPoint sort

`t` must have FloatingPoint sort. The size of the resulting bit-vector is automatically determined.

Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion knows only one NaN and it will always produce the same bit-vector representation of that NaN.

Referenced by z3py::fpToIEEEBV(), and expr::mk_to_ieee_bv().

## ◆ Z3_mk_fpa_to_real()

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.

Produces a term that represents the conversion of the floating-point term `t` into a real number. Note that this type of conversion will often result in non-linear constraints over real terms.

Parameters

  c | logical context
  t | term of FloatingPoint sort

Referenced by z3py::fpToReal().

## ◆ Z3_mk_fpa_to_sbv()

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.

Produces a term that represents the conversion of the floating-point term `t` into a bit-vector term of size `sz` in signed 2's complement format. If necessary, the result will be rounded according to rounding mode `rm`.

Parameters

  c | logical context
  rm | term of RoundingMode sort
  t | term of FloatingPoint sort
  sz | size of the resulting bit-vector

Referenced by z3py::fpToSBV().

## ◆ Z3_mk_fpa_to_ubv()

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.

Produces a term that represents the conversion of the floating-point term `t` into a bit-vector term of size `sz` in unsigned 2's complement format. If necessary, the result will be rounded according to rounding mode `rm`.

Parameters

  c | logical context
  rm | term of RoundingMode sort
  t | term of FloatingPoint sort
  sz | size of the resulting bit-vector

Referenced by z3py::fpToUBV().

## ◆ Z3_mk_fpa_zero()

Z3_ast Z3_API Z3_mk_fpa_zero | ( | Z3_context | c,
|  | Z3_sort | s,
|  | bool | negative
| ) |  |

Create a floating-point zero of sort `s`.

Parameters

  c | logical context
  s | target sort
  negative | indicates whether the result should be negative

When `negative` is `true`, -zero will be generated instead of +zero.

See also
  Z3_mk_fpa_inf
  Z3_mk_fpa_nan

Referenced by z3py::fpMinusZero(), z3py::fpPlusZero(), and z3py::fpZero().