Package org.sosy_lab.java_smt.api

Class FloatingPointNumber

  • @Immutable
public abstract class FloatingPointNumber
extends Object
    Represents a floating-point number with customizable precision, consisting of sign, exponent, and mantissa components.

    • Field Detail

      • SINGLE_PRECISION_EXPONENT_SIZE

        public static final int SINGLE_PRECISION_EXPONENT_SIZE
        See Also:
        Constant Field Values

      • SINGLE_PRECISION_MANTISSA_SIZE

        public static final int SINGLE_PRECISION_MANTISSA_SIZE
        See Also:
        Constant Field Values

      • DOUBLE_PRECISION_EXPONENT_SIZE

        public static final int DOUBLE_PRECISION_EXPONENT_SIZE
        See Also:
        Constant Field Values

      • DOUBLE_PRECISION_MANTISSA_SIZE

        public static final int DOUBLE_PRECISION_MANTISSA_SIZE
        See Also:
        Constant Field Values

    • Constructor Detail

      • FloatingPointNumber

        public FloatingPointNumber()

    • Method Detail

      • getSign

        @Deprecated(since="2025.01, because using a boolean flag as signBit is misleading",
            forRemoval=true)
@InlineMe(replacement="this.getMathSign() == Sign.NEGATIVE",
          imports="org.sosy_lab.java_smt.api.FloatingPointNumber.Sign")
public final boolean getSign()
        Deprecated, for removal: This API element is subject to removal in a future version.
        The sign of the floating-point number.
        Returns:
        whether the number is positive (FALSE) or negative (TRUE).

      • getMathSign

        public abstract FloatingPointNumber.Sign getMathSign()
        The sign of the floating-point number, i.e. whether it is positive or negative.

      • getExponent

        public abstract BigInteger getExponent()
        The exponent of the floating-point number, given as numeric value from binary representation. The number is unsigned (not negative) and includes a bias of 2^(exponentSize-1)-1 that is used in IEEE 754.

      • getMantissa

        public abstract BigInteger getMantissa()
        The mantissa (aka significand) of the floating-point number, given as numeric value from binary representation. The mantissa does not include the hidden bit that is used to denote normalized numbers in IEEE 754.

      • getExponentSize

        public abstract int getExponentSize()

      • getMantissaSize

        public abstract int getMantissaSize()

      • of

        @Deprecated(since="2025.01, because using a boolean flag as signBit is misleading",
            forRemoval=true)
@InlineMe(replacement="FloatingPointNumber.of(Sign.of(sign), exponent, mantissa, exponentSize, mantissaSize)",
          imports={"org.sosy_lab.java_smt.api.FloatingPointNumber","org.sosy_lab.java_smt.api.FloatingPointNumber.Sign"})
public static FloatingPointNumber of​(boolean sign,
                                     BigInteger exponent,
                                     BigInteger mantissa,
                                     int exponentSize,
                                     int mantissaSize)
        Deprecated, for removal: This API element is subject to removal in a future version.
        Get a floating-point number with the given sign, exponent, and mantissa.
        Parameters:
        sign - the sign-bit of the floating-point number as specified by IEEE 754, aka FALSE for positive and TRUE for negative
        exponent - the exponent of the floating-point number, given as unsigned (not negative) number, including a bias of 2^(exponentSize-1)-1
        mantissa - the mantissa of the floating-point number, given as unsigned (not negative) number without hidden bit
        exponentSize - the (maximum) size of the exponent in bits
        mantissaSize - the (maximum) size of the mantissa in bits
        See Also:
        of(Sign, BigInteger, BigInteger, int, int)

      • of

        public static FloatingPointNumber of​(FloatingPointNumber.Sign sign,
                                     BigInteger exponent,
                                     BigInteger mantissa,
                                     int exponentSize,
                                     int mantissaSize)
        Get a floating-point number with the given sign, exponent, and mantissa.
        Parameters:
        sign - the sign of the floating-point number
        exponent - the exponent of the floating-point number, given as unsigned (not negative) number, including a bias of 2^(exponentSize-1)-1
        mantissa - the mantissa of the floating-point number, given as unsigned (not negative) number without hidden bit
        exponentSize - the (maximum) size of the exponent in bits
        mantissaSize - the (maximum) size of the mantissa in bits

      • of

        public static FloatingPointNumber of​(String bits,
                                     int exponentSize,
                                     int mantissaSize)
        Get a floating-point number encoded as bitvector as defined by IEEE 754.
        Parameters:
        bits - the bit-representation of the floating-point number, consisting of sign bit, exponent (without bias) and mantissa (without hidden bit) in this exact ordering
        exponentSize - the size of the exponent in bits
        mantissaSize - the size of the mantissa in bits

      • isIEEE754SinglePrecision

        public boolean isIEEE754SinglePrecision()
        Returns true if this floating-point number is an IEEE-754-2008 single precision type with 32 bits length consisting of an 8 bit exponent, a 23 bit mantissa and a single sign bit.
        Returns:
        true for IEEE-754 single precision type, false otherwise.

      • isIEEE754DoublePrecision

        public boolean isIEEE754DoublePrecision()
        Returns true if this floating-point number is an IEEE-754-2008 double precision type with 64 bits length consisting of an 11 bit exponent, a 52 bit mantissa and a single sign bit.
        Returns:
        true for IEEE-754 double precision type, false otherwise.

      • floatValue

        public float floatValue()
        compute a representation as Java-based float value, if possible.

      • doubleValue

        public double doubleValue()
        compute a representation as Java-based double value, if possible.

      • toString

        public final String toString()
        Return a bit-representation of sign-bit, exponent, and mantissa, i.e., a concatenation of their bit-representations in this exact ordering.
        Overrides:
        toString in class Object