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
clogical context
sFloatingPoint 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
clogical context
ta floating-point numeral
biasedflag 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
clogical context
ta floating-point numeral
nexponent
biasedflag to indicate whether the result is in biased representation

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
clogical context
ta floating-point numeral
biasedflag to indicate whether the result is in biased representation

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
clogical context
ta floating-point numeral
sgnsign

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
clogical context
ta 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
clogical context
ta 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
clogical context
ta floating-point numeral

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
clogical context
ta floating-point numeral
npointer 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
clogical context
sFloatingPoint 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
clogical context
ta 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
clogical context
ta 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
clogical context
ta 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
clogical context
ta 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
clogical context
ta 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
clogical context
ta 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
clogical context
ta 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
clogical context
tterm 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
clogical context
rmterm of RoundingMode sort
t1term of FloatingPoint sort
t2term 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
clogical context
rmterm of RoundingMode sort
t1term of FloatingPoint sort.
t2term 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
clogical context
t1term of FloatingPoint sort
t2term 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
clogical context
rmterm of RoundingMode sort
t1term of FloatingPoint sort
t2term of FloatingPoint sort
t3term 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.

Referenced by z3::fma().

◆ 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
clogical context
sgnsign
expexponent
sigsignificand
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
clogical context
t1term of FloatingPoint sort
t2term 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
clogical context
t1term of FloatingPoint sort
t2term 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
clogical context
starget sort
negativeindicates 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 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
clogical context
tterm of FloatingPoint sort

t must have FloatingPoint sort.

◆ 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
clogical context
tterm of FloatingPoint sort

t must have FloatingPoint sort.

◆ 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
clogical context
tterm 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
clogical context
tterm of FloatingPoint sort

t must have FloatingPoint sort.

◆ 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
clogical context
tterm 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
clogical context
tterm of FloatingPoint sort

t must have FloatingPoint sort.

◆ 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
clogical context
tterm of FloatingPoint sort

t must have FloatingPoint sort.

◆ 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
clogical context
t1term of FloatingPoint sort
t2term 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
clogical context
t1term of FloatingPoint sort
t2term 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
clogical context
t1term of FloatingPoint sort
t2term 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
clogical context
t1term of FloatingPoint sort
t2term 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
clogical context
rmterm of RoundingMode sort
t1term of FloatingPoint sort
t2term 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
clogical context
starget sort
See also
Z3_mk_fpa_inf
Z3_mk_fpa_zero

Referenced by z3py::fpNaN().

◆ Z3_mk_fpa_neg()

Z3_ast Z3_API Z3_mk_fpa_neg ( Z3_context  c,
Z3_ast  t 
)

Floating-point negation.

Parameters
clogical context
tterm 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
clogical context
vvalue
tysort

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
clogical context
vvalue
tysort

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
clogical context
vvalue
tyresult 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
clogical context
sgnsign bit (true == negative)
sigsignificand
expexponent
tyresult 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
clogical context
sgnsign bit (true == negative)
sigsignificand
expexponent
tyresult 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
clogical context
t1term of FloatingPoint sort
t2term 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
clogical 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
clogical 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
clogical 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
clogical 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
clogical context
rmterm of RoundingMode sort
tterm 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
clogical 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
clogical 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
clogical 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
clogical context

◆ 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
clogical 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
clogical 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
clogical 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
clogical context
ebitsnumber of exponent bits
sbitsnumber 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
clogical 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
clogical 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
clogical 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
clogical 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
clogical 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
clogical 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
clogical 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
clogical 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
clogical context
rmterm of RoundingMode sort
tterm 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
clogical context
rmterm of RoundingMode sort
t1term of FloatingPoint sort
t2term 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
clogical context
bva bit-vector term
sfloating-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(), and z3py::fpToFP().

◆ 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
clogical context
rmterm of RoundingMode sort
tterm of FloatingPoint sort
sfloating-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
clogical context
rmterm of RoundingMode sort
expexponent term of Int sort
sigsignificand term of Real sort
sFloatingPoint 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
clogical context
rmterm of RoundingMode sort
tterm of Real sort
sfloating-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
clogical context
rmterm of RoundingMode sort
tterm of bit-vector sort
sfloating-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
clogical context
rmterm of RoundingMode sort
tterm of bit-vector sort
sfloating-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
clogical context
tterm 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().

◆ 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
clogical context
tterm 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
clogical context
rmterm of RoundingMode sort
tterm of FloatingPoint sort
szsize 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
clogical context
rmterm of RoundingMode sort
tterm of FloatingPoint sort
szsize 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
clogical context
starget sort
negativeindicates 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().