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

        @Deprecated(since="6.0",
            forRemoval=true)
public static final int SINGLE_PRECISION_EXPONENT_SIZE
        Deprecated, for removal: This API element is subject to removal in a future version.
        See Also:
        Constant Field Values

      • SINGLE_PRECISION_MANTISSA_SIZE

        @Deprecated(since="6.0",
            forRemoval=true)
public static final int SINGLE_PRECISION_MANTISSA_SIZE
        Deprecated, for removal: This API element is subject to removal in a future version.
        this constant can be confusing, as the SMTLIB2 standard expects the mantissa to include the hidden bit, but this constant does not.
        See Also:
        Constant Field Values

      • SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT

        protected static final int SINGLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT
        See Also:
        Constant Field Values

      • DOUBLE_PRECISION_EXPONENT_SIZE

        @Deprecated(since="6.0",
            forRemoval=true)
public static final int DOUBLE_PRECISION_EXPONENT_SIZE
        Deprecated, for removal: This API element is subject to removal in a future version.
        See Also:
        Constant Field Values

      • DOUBLE_PRECISION_MANTISSA_SIZE

        @Deprecated(since="6.0",
            forRemoval=true)
public static final int DOUBLE_PRECISION_MANTISSA_SIZE
        Deprecated, for removal: This API element is subject to removal in a future version.
        this constant can be confusing, as the SMTLIB2 standard expects the mantissa to include the hidden bit, but this constant does not.
        See Also:
        Constant Field Values

      • DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT

        protected static final int DOUBLE_PRECISION_MANTISSA_SIZE_WITHOUT_HIDDEN_BIT
        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

        @Deprecated(since="6.0",
            forRemoval=true)
public final int getMantissaSize()
        Deprecated, for removal: This API element is subject to removal in a future version.
        this method can be confusing, as the SMTLIB2 standard expects the mantissa to include the hidden bit, but this does not. Use getMantissaSizeWithoutHiddenBit() instead if you want the mantissa without the hidden bit, and getMantissaSizeWithHiddenBit() if you want it to include the hidden bit.
        Returns the size of the mantissa (also called a coefficient or significant), excluding the sign bit.

      • getMantissaSizeWithoutHiddenBit

        public abstract int getMantissaSizeWithoutHiddenBit()
        Returns the size of the mantissa (also called a coefficient or significant), excluding the hidden bit.

      • getMantissaSizeWithHiddenBit

        public int getMantissaSizeWithHiddenBit()
        Returns the size of the mantissa (also called a coefficient or significant), including the hidden bit.

      • getTotalSize

        public int getTotalSize()
        Returns the size of the precision, i.e. the single sign bit + the size of the exponent + the size of the mantissa (excluding the hidden bit).

      • 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, mantissaSizeWithoutHiddenBit)",
          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 mantissaSizeWithoutHiddenBit)
        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
        mantissaSizeWithoutHiddenBit - the (maximum) size of the mantissa in bits (excluding the hidden bit)
        See Also:
        of(Sign, BigInteger, BigInteger, int, int)

      • of

        public static FloatingPointNumber of​(FloatingPointNumber.Sign sign,
                                     BigInteger exponent,
                                     BigInteger mantissa,
                                     int exponentSize,
                                     int mantissaSizeWithoutHiddenBit)
        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
        mantissaSizeWithoutHiddenBit - the (maximum) size of the mantissa in bits (excluding the hidden bit)

      • of

        public static FloatingPointNumber of​(String bits,
                                     int exponentSize,
                                     int mantissaSizeWithoutHiddenBit)
        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
        mantissaSizeWithoutHiddenBit - the size of the mantissa in bits (excluding the hidden bit)

      • 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 24 bit mantissa (including the hidden 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 53 bit mantissa (including the hidden 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