Module fp 

IEEE 754 floating point on bit-vectors.

A floating-point value is a BitVec holding an IEEE 754 interchange encoding of a format FpFormat (eb, sb): a sign bit, eb exponent bits and sb − 1 trailing significand bits (SMT-LIB’s convention: sb counts the hidden bit). Every operation is total and exact: it is defined for every input pattern and gives exactly one result pattern, as the book’s chapter on floating point specifies. In short:

• results are correctly rounded in the operation’s RoundingMode;
• every operation that produces a NaN produces the format’s canonical quiet NaN (sign 0, exponent all ones, only the top significand bit set); neg, abs and copysign change the sign bit only, of a NaN too;
• min and max are IEEE 754-2019’s minimumNumber and maximumNumber (a NaN operand is ignored, −0 < +0);
• conversions to integers saturate, and a NaN converts to 0.

use bitwright::fp::{FpFormat, RoundingMode};
use bitwright::BitVec;

let f = FpFormat::F32;
let (a, b) = (BitVec::from_f32(0.1), BitVec::from_f32(0.2));
let sum = f.add(RoundingMode::Rne, &a, &b)?;
assert_eq!(sum.to_f32(), Some(0.1f32 + 0.2f32));
// The exact sum lies 3/4 of the way to the next value up: to nearest (and toward +∞) it
// rounds up, toward zero one unit in the last place lower.
let down = f.add(RoundingMode::Rtz, &a, &b)?;
assert_eq!(down.to_f32(), Some(f32::from_bits((0.1f32 + 0.2f32).to_bits() - 1)));

Structs

FpArgs

The operands of a floating-point node (1 to 3).

FpFormat

A binary floating-point format: eb exponent bits and sb significand bits, the hidden bit included, so a value is eb + sb bits wide. 2 ≤ eb ≤ 31, sb ≥ 2, eb + sb ≤ 512.

Enums

FpCmpOp

A floating-point comparison; each is false when either operand is a NaN.

FpKind

A floating-point operation without its attributes (rounding mode, formats, integer width): what an FpOp is, and what a rule’s floating-point node names (FpNode).

FpOp

A floating-point operator, as an expression node holds it (see View::Fp). Its FpFormat is given separately: the format of the floating-point operands, or of the result for the conversions from integers.

FpTest

A classification test (SMT-LIB’s fp.isNaN, …).

RoundingMode

A rounding direction (IEEE 754 §4.3), named as in SMT-LIB.

Functions

x87_load

Loads an 80-bit x87 extended-precision encoding as a value of FpFormat::X87 (79 bits): the explicit integer bit is dropped; a pseudo-denormal becomes the normal value it stands for; an unnormal, a pseudo-infinity and a pseudo-NaN (which x87 rejects as invalid) become the canonical NaN; other NaNs keep their payload.

x87_store

Stores a value of FpFormat::X87 (79 bits) as its 80-bit x87 encoding: the explicit integer bit is 1 exactly when the exponent field is nonzero. NaN payloads are kept.