Struct FloatingPoint 

pub struct FloatingPoint<'st, const EB: usize, const SB: usize>(/* private fields */);

A floating-point number, parameterized by exponent bits (EB) and significand bits (SB). Significand bits include the sign bit.

Implementations

impl<'st, const EB: usize, const SB: usize> FloatingPoint<'st, EB, SB>

pub fn new( st: &'st Storage, value: impl IntoWithStorage<'st, FloatingPoint<'st, EB, SB>>, ) -> FloatingPoint<'st, EB, SB>

Construct a new bit-vec.

pub fn fp<const SB_1: usize>( st: &'st Storage, sign: BitVec<'st, 1>, exponent: BitVec<'st, EB>, significand: BitVec<'st, SB_1>, ) -> Self

Creates a floating-point value from sign, exponent, and significand bit-vectors. i = sb - 1

Note: The SB_1 parameter is a workaround for #![feature(generic_const_exprs)].

pub fn plus_oo(st: &'st Storage) -> Self

Positive infinity

pub fn minus_oo(st: &'st Storage) -> Self

Negative infinity

pub fn plus_zero(st: &'st Storage) -> Self

Positive zero

pub fn minus_zero(st: &'st Storage) -> Self

Negative zero

pub fn nan(st: &'st Storage) -> Self

Not a Number

pub fn fp_abs(self) -> Self

Absolute value (fp.abs)

pub fn fp_neg(self) -> Self

Negation (fp.neg)

pub fn fp_add(self, rm: RoundingMode<'st>, other: Self) -> Self

Addition (fp.add)

pub fn fp_sub(self, rm: RoundingMode<'st>, other: Self) -> Self

Subtraction (fp.sub)

pub fn fp_mul(self, rm: RoundingMode<'st>, other: Self) -> Self

Multiplication (fp.mul)

pub fn fp_div(self, rm: RoundingMode<'st>, other: Self) -> Self

Division (fp.div)

pub fn fp_fma(self, rm: RoundingMode<'st>, other1: Self, other2: Self) -> Self

Fused multiplication and addition: (self * other1) + other2 (fp.fma)

pub fn fp_sqrt(self, rm: RoundingMode<'st>) -> Self

Square root (fp.sqrt)

pub fn fp_rem(self, other: Self) -> Self

Remainder: self - other * n, where n in Z is nearest to self/other (fp.rem)

pub fn fp_round_to_integral(self, rm: RoundingMode<'st>) -> Self

Rounding to integral (fp.roundToIntegral)

pub fn fp_min(self, other: Self) -> Self

Minimum (fp.min)

pub fn fp_max(self, other: Self) -> Self

Maximum (fp.max)

pub fn fp_leq(self, other: Self) -> Bool<'st>

Less than or equal (fp.leq)

pub fn fp_lt(self, other: Self) -> Bool<'st>

Less than (fp.lt)

pub fn fp_geq(self, other: Self) -> Bool<'st>

Greater than or equal (fp.geq)

pub fn fp_gt(self, other: Self) -> Bool<'st>

Greater than (fp.gt)

pub fn fp_eq(self, other: Self) -> Bool<'st>

IEEE 754-2008 equality (fp.eq)

pub fn fp_is_normal(self) -> Bool<'st>

Is normal (fp.isNormal)

pub fn fp_is_subnormal(self) -> Bool<'st>

Is subnormal (fp.isSubnormal)

pub fn fp_is_zero(self) -> Bool<'st>

Is zero (fp.isZero)

pub fn fp_is_infinite(self) -> Bool<'st>

Is infinite (fp.isInfinite)

pub fn fp_is_nan(self) -> Bool<'st>

Is NaN (fp.isNaN)

pub fn fp_is_negative(self) -> Bool<'st>

Is negative (fp.isNegative)

pub fn fp_is_positive(self) -> Bool<'st>

Is positive (fp.isPositive)

pub fn to_fp_from_bits<const M: usize>( st: &'st Storage, bv: BitVec<'st, M>, ) -> Self

From single bitstring representation in IEEE 754-2008 interchange format. M = EB + SB (to_fp)

pub fn to_fp_from_fp<const MB: usize, const NB: usize>( st: &'st Storage, rm: RoundingMode<'st>, fp_other: FloatingPoint<'st, MB, NB>, ) -> Self

From another floating point sort (to_fp)

pub fn to_fp_from_real( st: &'st Storage, rm: RoundingMode<'st>, real: Real<'st>, ) -> Self

From real (to_fp)

pub fn to_fp_from_signed_bit_vec<const M: usize>( st: &'st Storage, rm: RoundingMode<'st>, bv: BitVec<'st, M>, ) -> Self

From signed machine integer, represented as a 2’s complement bit vector (to_fp)

pub fn to_fp_from_unsigned_bit_vec<const M: usize>( st: &'st Storage, rm: RoundingMode<'st>, bv: BitVec<'st, M>, ) -> Self

From unsigned machine integer, represented as bit vector (to_fp_unsigned)

pub fn fp_to_ubv<const M: usize>(self, rm: RoundingMode<'st>) -> BitVec<'st, M>

To unsigned machine integer, represented as a bit vector (fp.to_ubv)

pub fn fp_to_sbv<const M: usize>(self, rm: RoundingMode<'st>) -> BitVec<'st, M>

To signed machine integer, represented as a 2’s complement bit vector (fp.to_sbv)

pub fn fp_to_real(self) -> Real<'st>

To real (fp.to_real)

Trait Implementations

impl<'st, const EB: usize, const SB: usize> Clone for FloatingPoint<'st, EB, SB>

fn clone(&self) -> Self

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<'st, const EB: usize, const SB: usize> Copy for FloatingPoint<'st, EB, SB>

impl<'st, const EB: usize, const SB: usize> Debug for FloatingPoint<'st, EB, SB>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<const EB: usize, const SB: usize> Display for FloatingPoint<'_, EB, SB>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'st, const EB: usize, const SB: usize> From<(STerm<'st>, Sort<'st>)> for FloatingPoint<'st, EB, SB>

fn from((t, _): (STerm<'st>, Sort<'st>)) -> Self

Converts to this type from the input type.

impl<'st, const EB: usize, const SB: usize> From<Const<'st, FloatingPoint<'st, EB, SB>>> for FloatingPoint<'st, EB, SB>

fn from(c: Const<'st, FloatingPoint<'st, EB, SB>>) -> Self

Converts to this type from the input type.

impl<'st, const EB: usize, const SB: usize> From<FloatingPoint<'st, EB, SB>> for Dynamic<'st>

fn from(i: FloatingPoint<'st, EB, SB>) -> Self

Converts to this type from the input type.

impl<'st, const EB: usize, const SB: usize> From<FloatingPoint<'st, EB, SB>> for STerm<'st>

fn from(i: FloatingPoint<'st, EB, SB>) -> Self

Converts to this type from the input type.

impl<'st, const EB: usize, const SB: usize> From<STerm<'st>> for FloatingPoint<'st, EB, SB>

fn from(t: STerm<'st>) -> Self

Converts to this type from the input type.

impl<'st> IntoWithStorage<'st, FloatingPoint<'st, 8, 24>> for f32

fn into_with_storage(self, st: &'st Storage) -> Float32<'st>

Construct a STerm with the presence of Storage

impl<'st> IntoWithStorage<'st, FloatingPoint<'st, 11, 53>> for f64

fn into_with_storage(self, st: &'st Storage) -> Float64<'st>

Construct a STerm with the presence of Storage

impl<'st, const EB: usize, const SB: usize> StaticSorted<'st> for FloatingPoint<'st, EB, SB>

const AST_SORT: Sort<'static>

The sort of this sort.

type Inner = FloatingPoint<'st, EB, SB>

The inner type of the term. This is used for Const<'st, T> where the inner type is T.

fn static_st(&self) -> &'st Storage

The storage associated with the term.

fn sort() -> Sort<'st>

The sort of this sort.

fn new_const(st: &'st Storage, name: &str) -> Const<'st, Self>

Construct a new constante of this sort.

impl<'st> TryFrom<FloatingPoint<'st, 8, 24>> for f32

type Error = ParseIntError

The type returned in the event of a conversion error.

fn try_from(value: Float32<'st>) -> Result<Self, Self::Error>

Performs the conversion.

impl<'st> TryFrom<FloatingPoint<'st, 11, 53>> for f64

type Error = ParseIntError

The type returned in the event of a conversion error.

fn try_from(value: Float64<'st>) -> Result<Self, Self::Error>

Performs the conversion.