Float package:sbv

A collection of arbitrary float operations.

A floating point value, indexed by its exponent and significand sizes. An IEEE SP is FloatingPoint 8 24 DP is FloatingPoint 11 53 etc. NB. Don't derive Ord for this type automatically, see notes below.

Several examples involving IEEE-754 floating point numbers, i.e., single precision Float (SFloat), double precision Double (SDouble), and the generic SFloatingPoint eb sb type where the user can specify the exponent and significand bit-widths. (Note that there is always an extra sign-bit, and the value of sb includes the hidden bit.) Arithmetic with floating point is full of surprises; due to precision issues associativity of arithmetic operations typically do not hold. Also, the presence of NaN is always something to look out for.

Reinterpret-casts a Float to a Word32.

Recognize a floating point number. The exponent part is optional if a fraction is present. The exponent may or may not have a sign.

>>> prove $ \(s :: SString) -> s `match` floating .=> length s .>= 3
Q.E.D.

Abbreviation for brain-float precision float, bit width 16 = 8 + 8.

Conversion to and from floats

A class of floating-point (IEEE754) operations, some of which behave differently based on rounding modes. Note that unless the rounding mode is concretely RoundNearestTiesToEven, we will not concretely evaluate these, but rather pass down to the SMT solver.

A symbolic brain-float precision float

IEEE-754 single-precision floating point numbers

A symbolic arbitrary precision floating point value

A valid float has restrictions on eb/sb values. NB. In the below encoding, I found that CPP is very finicky about substitution of the machine-dependent macros. If you try to put the conditionals in the same line, it fails to substitute for some reason. Hence the awkward spacing. Filed this as a bug report for CPPHS at https://github.com/malcolmwallace/cpphs/issues/25.

Extract the sign/exponent/mantissa of a single-precision float. The output will have 8 bits in the second argument for exponent, and 23 in the third for the mantissa.

Extract the sign/exponent/mantissa of an arbitrary precision float. The output will have eb bits in the second argument for exponent, and sb-1 bits in the third for mantissa.

Convert from an IEEE74 single precision float.

Convert from an arbitrary floating point.

Declare a named SFPBFloat NB. For a version which generalizes over the underlying monad, see SFPBFloat

Declare an unnamed SFPBFloat NB. For a version which generalizes over the underlying monad, see SFPBFloat

Declare a list of SFPQuads NB. For a version which generalizes over the underlying monad, see sFPBFloats

Declare a named SFloat NB. For a version which generalizes over the underlying monad, see sFloat

Convert an SFloat to an SWord32, preserving the bit-correspondence. Note that since the representation for NaNs are not unique, this function will return a symbolic value when given a concrete NaN. Implementation note: Since there's no corresponding function in SMTLib for conversion to bit-representation due to partiality, we use a translation trick by allocating a new word variable, converting it to float, and requiring it to be equivalent to the input. In code-generation mode, we simply map it to a simple conversion.

Declare an unnamed SFloat NB. For a version which generalizes over the underlying monad, see sFloat_

Declare a named 'SFloatingPoint eb sb' NB. For a version which generalizes over the underlying monad, see sFloatingPoint