Package org.sosy_lab.java_smt.api

Record Class FloatingPointNumber

java.lang.Object
java.lang.Record
org.sosy_lab.java_smt.api.FloatingPointNumber
@Immutable public record FloatingPointNumber(FloatingPointNumber.Sign mathSign, BigInteger exponent, BigInteger mantissa, FormulaType.FloatingPointType floatingPointType) extends Record
Represents a floating-point number with customizable precision, consisting of sign, exponent, and mantissa components.

  • Field Details

    • 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:

    • 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:

    • 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:

    • 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:

  • Constructor Details

    • FloatingPointNumber

      public FloatingPointNumber(FloatingPointNumber.Sign mathSign, BigInteger exponent, BigInteger mantissa, FormulaType.FloatingPointType floatingPointType)
      Creates an instance of a FloatingPointNumber record class.
      Parameters:
      mathSign - the value for the mathSign record component
      exponent - the value for the exponent record component
      mantissa - the value for the mantissa record component
      floatingPointType - the value for the floatingPointType record component

  • Method Details

    • 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 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 FloatingPointNumber.Sign getMathSign()
      The sign of the floating-point number, i.e. whether it is positive or negative.

    • getExponent

      public 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 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.

    • getFloatingPointType

      public FormulaType.FloatingPointType getFloatingPointType()
      Returns the FormulaType.FloatingPointType of this FloatingPointNumber.

    • getExponentSize

      public 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 significand), excluding the sign bit.

    • getMantissaSizeWithoutHiddenBit

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

    • getMantissaSizeWithHiddenBit

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

    • getTotalSize

      public int getTotalSize()
      Returns the size of the precision as defined by the SMTLIB2 standard, i.e. 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) 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.
      Use of(Sign, BigInteger, BigInteger, FloatingPointType) instead.
      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)

    • of

      @Deprecated(since="2026.01, because mantissa arguments with/without sign bits can be misleading", forRemoval=true) public static FloatingPointNumber of(FloatingPointNumber.Sign sign, BigInteger exponent, BigInteger mantissa, int exponentSize, int mantissaSizeWithoutHiddenBit)
      Deprecated, for removal: This API element is subject to removal in a future version.
      Use of(Sign, BigInteger, BigInteger, FloatingPointType) instead.
      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(FloatingPointNumber.Sign sign, BigInteger exponent, BigInteger mantissa, FormulaType.FloatingPointType floatingPointType)
      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^(exponent size - 1) - 1.
      mantissa - the mantissa of the floating-point number, given as unsigned (not negative) number without hidden bit.
      floatingPointType - FormulaType.FloatingPointType to use. Mantissa and exponent sizes are used based on this type.

    • of

      @Deprecated(since="2026.01, because mantissa arguments with/without sign bits can be misleading", forRemoval=true) public static FloatingPointNumber of(String bits, int exponentSize, int mantissaSizeWithoutHiddenBit)
      Deprecated, for removal: This API element is subject to removal in a future version.
      Use of(String, FloatingPointType) instead.
      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)

    • of

      public static FloatingPointNumber of(String bits, FormulaType.FloatingPointType floatingPointType)
      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.
      floatingPointType - FormulaType.FloatingPointType to use. Mantissa and exponent sizes are used based on this type.

    • isIEEE754SinglePrecision

      public boolean isIEEE754SinglePrecision()
      Returns true if this floating-point number is an IEEE-754-2008 single precision type with 32 bits total length consisting of the sign bit, an 8 bit exponent, and a 23 bit mantissa (excluding 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 total length, consisting of the sign bit, an 11 bit exponent, and a 52 bit mantissa (excluding 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 String toString()
      Return a bit-representation of sign-bit, exponent, and mantissa, i.e., a concatenation of their bit-representations in this exact ordering.
      Specified by:
      toString in class Record

    • hashCode

      public final int hashCode()
      Returns a hash code value for this object. The value is derived from the hash code of each of the record components.
      Specified by:
      hashCode in class Record
      Returns:
      a hash code value for this object

    • equals

      public final boolean equals(Object o)
      Indicates whether some other object is "equal to" this one. The objects are equal if the other object is of the same class and if all the record components are equal. All components in this record class are compared with Objects::equals(Object,Object).
      Specified by:
      equals in class Record
      Parameters:
      o - the object with which to compare
      Returns:
      true if this object is the same as the o argument; false otherwise.

    • mathSign

      public FloatingPointNumber.Sign mathSign()
      Returns the value of the mathSign record component.
      Returns:
      the value of the mathSign record component

    • exponent

      public BigInteger exponent()
      Returns the value of the exponent record component.
      Returns:
      the value of the exponent record component

    • mantissa

      public BigInteger mantissa()
      Returns the value of the mantissa record component.
      Returns:
      the value of the mantissa record component

    • floatingPointType

      public FormulaType.FloatingPointType floatingPointType()
      Returns the value of the floatingPointType record component.
      Returns:
      the value of the floatingPointType record component