java.lang.Object
- org.sosy_lab.java_smt.api.FloatingPointNumber

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

Field Summary

Fields
Modifier and Type	Field	Description
`static int`	`DOUBLE_PRECISION_EXPONENT_SIZE`
`static int`	`DOUBLE_PRECISION_MANTISSA_SIZE`
`static int`	`SINGLE_PRECISION_EXPONENT_SIZE`
`static int`	`SINGLE_PRECISION_MANTISSA_SIZE`

Constructor Summary

Constructors
Constructor Description

FloatingPointNumber()

Method Summary

All Methods Static Methods Instance Methods Abstract Methods Concrete Methods
Modifier and Type	Method	Description
`double`	`doubleValue()`	compute a representation as Java-based double value, if possible.
`float`	`floatValue()`	compute a representation as Java-based float value, if possible.
`abstract BigInteger`	`getExponent()`	The exponent of the floating-point number, given as numeric value.
`abstract int`	`getExponentSize()`
`abstract BigInteger`	`getMantissa()`	The mantissa (aka significand) of the floating-point number, given as numeric value.
`abstract int`	`getMantissaSize()`
`abstract boolean`	`getSign()`	Whether the number is positive (TRUE) or negative (FALSE).
`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.
`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.
`static FloatingPointNumber`	`of(boolean sign, BigInteger exponent, BigInteger mantissa, int exponentSize, int mantissaSize)`
`static FloatingPointNumber`	`of(String bits, int exponentSize, int mantissaSize)`
`String`	`toString()`	Return a bit-representation of sign-bit, exponent, and mantissa, i.e., a concatenation of their bit-representations in this exact ordering.

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

- 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
```
public abstract boolean getSign()
```
    Whether the number is positive (TRUE) or negative (FALSE).
  - getExponent
```
public abstract BigInteger getExponent()
```
    The exponent of the floating-point number, given as numeric value.
  - getMantissa
```
public abstract BigInteger getMantissa()
```
    The mantissa (aka significand) of the floating-point number, given as numeric value.
  - getExponentSize
```
public abstract int getExponentSize()
```
  - getMantissaSize
```
public abstract int getMantissaSize()
```
  - of
```
public static FloatingPointNumber of(boolean sign,
                                     BigInteger exponent,
                                     BigInteger mantissa,
                                     int exponentSize,
                                     int mantissaSize)
```
  - of
```
public static FloatingPointNumber of(String bits,
                                     int exponentSize,
                                     int mantissaSize)
```
  - 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

Class FloatingPointNumber

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

SINGLE_PRECISION_EXPONENT_SIZE

SINGLE_PRECISION_MANTISSA_SIZE

DOUBLE_PRECISION_EXPONENT_SIZE

DOUBLE_PRECISION_MANTISSA_SIZE

Constructor Detail

FloatingPointNumber

Method Detail

getSign

getExponent

getMantissa

getExponentSize

getMantissaSize

of

of

isIEEE754SinglePrecision

isIEEE754DoublePrecision

floatValue

doubleValue

toString