java.lang.Object
- org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>

All Implemented Interfaces:

FloatingPointFormulaManager
```
public abstract class AbstractFloatingPointFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>
extends Object
implements FloatingPointFormulaManager
```
Similar to the other Abstract*FormulaManager classes in this package, this class serves as a helper for implementing FloatingPointFormulaManager. It handles all the unwrapping and wrapping from and to the Formula instances, such that the concrete class needs to handle only its own internal types.
For multiply(FloatingPointFormula, FloatingPointFormula), and divide(FloatingPointFormula, FloatingPointFormula) this class even offers an implementation based on UFs. Subclasses are supposed to override them if they can implement these operations more precisely (for example multiplication with constants should be supported by all solvers and implemented by all subclasses).

Nested Class Summary

Nested Classes
Modifier and Type Class Description

static class AbstractFloatingPointFormulaManager.BitvectorFormulaAndBooleanFormula

Field Summary

Fields
Modifier and Type Field Description

protected FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> formulaCreator

Constructor Summary

Constructors
Modifier	Constructor	Description
`protected`	`AbstractFloatingPointFormulaManager(FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> pCreator, AbstractBitvectorFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> pBvMgr, AbstractBooleanFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> pBMgr)`

Method Summary

All Methods Static Methods Instance Methods Abstract Methods Concrete Methods
Modifier and Type	Method	Description
`FloatingPointFormula`	`abs(FloatingPointFormula pNumber)`
`protected abstract TFormulaInfo`	`abs(TFormulaInfo pParam1)`
`FloatingPointFormula`	`add(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2)`
`FloatingPointFormula`	`add(FloatingPointFormula number1, FloatingPointFormula number2, FloatingPointRoundingMode pFloatingPointRoundingMode)`
`protected abstract TFormulaInfo`	`add(TFormulaInfo pParam1, TFormulaInfo pParam2, TFormulaInfo pRoundingMode)`
`BooleanFormula`	`assignment(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2)`	Create a term for assigning one floating-point term to another.
`protected abstract TFormulaInfo`	`assignment(TFormulaInfo pParam1, TFormulaInfo pParam2)`
`FloatingPointFormula`	`castFrom(Formula pNumber, boolean pSigned, FormulaType.FloatingPointType pTargetType)`	Build a `FloatingPointFormula` from another compatible formula.
`FloatingPointFormula`	`castFrom(Formula number, boolean signed, FormulaType.FloatingPointType targetType, FloatingPointRoundingMode pFloatingPointRoundingMode)`	Build a `FloatingPointFormula` from another compatible formula.
`protected abstract TFormulaInfo`	`castFromImpl(TFormulaInfo pNumber, boolean pSigned, FormulaType.FloatingPointType pTargetType, TFormulaInfo pRoundingMode)`
`<T extends Formula> T`	`castTo(FloatingPointFormula pNumber, boolean pSigned, FormulaType<T> pTargetType)`	Build a formula of compatible type from a `FloatingPointFormula`.
`<T extends Formula> T`	`castTo(FloatingPointFormula number, boolean pSigned, FormulaType<T> targetType, FloatingPointRoundingMode pFloatingPointRoundingMode)`	Build a formula of compatible type from a `FloatingPointFormula`.
`protected abstract TFormulaInfo`	`castToImpl(TFormulaInfo pNumber, boolean pSigned, FormulaType<?> pTargetType, TFormulaInfo pRoundingMode)`
`FloatingPointFormula`	`divide(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2)`
`FloatingPointFormula`	`divide(FloatingPointFormula number1, FloatingPointFormula number2, FloatingPointRoundingMode pFloatingPointRoundingMode)`
`protected abstract TFormulaInfo`	`divide(TFormulaInfo pParam1, TFormulaInfo pParam2, TFormulaInfo pFloatingPointRoundingMode)`
`BooleanFormula`	`equalWithFPSemantics(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2)`	Create a term for comparing the equality of two floating-point terms, according to standard floating-point semantics (i.e., `NaN != NaN` and `0.0 == -0.0`).
`protected abstract TFormulaInfo`	`equalWithFPSemantics(TFormulaInfo pParam1, TFormulaInfo pParam2)`
`protected TFormulaInfo`	`extractInfo(Formula pBits)`
`FloatingPointFormula`	`fromIeeeBitvector(BitvectorFormula pNumber, FormulaType.FloatingPointType pTargetType)`	Create a formula that interprets the given bitvector as a floating-point value in the IEEE format, according to the given type.
`protected abstract TFormulaInfo`	`fromIeeeBitvectorImpl(TFormulaInfo pNumber, FormulaType.FloatingPointType pTargetType)`
`protected static String`	`getBvRepresentation(BigInteger integer, int size)`
`protected abstract TFormulaInfo`	`getDefaultRoundingMode()`
`int`	`getExponentSize(FloatingPointFormula f)`	Returns the size of the exponent for the given `FloatingPointFormula`.
`protected abstract int`	`getExponentSizeImpl(TFormulaInfo f)`
`protected FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl>`	`getFormulaCreator()`
`int`	`getMantissaSizeWithSignBit(FloatingPointFormula f)`	Returns the size of the mantissa (also called a coefficient or significant), including the sign bit, for the given `FloatingPointFormula`.
`protected abstract int`	`getMantissaSizeWithSignBitImpl(TFormulaInfo f)`
`protected abstract TFormulaInfo`	`getRoundingModeImpl(FloatingPointRoundingMode pFloatingPointRoundingMode)`
`BooleanFormula`	`greaterOrEquals(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2)`	Returns whether an FP number is greater or equal than another FP number.
`protected abstract TFormulaInfo`	`greaterOrEquals(TFormulaInfo pParam1, TFormulaInfo pParam2)`
`BooleanFormula`	`greaterThan(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2)`	Returns whether an FP number is greater than another FP number.
`protected abstract TFormulaInfo`	`greaterThan(TFormulaInfo pParam1, TFormulaInfo pParam2)`
`BooleanFormula`	`isInfinity(FloatingPointFormula pNumber)`	Checks whether a formula is positive or negative infinity.
`protected abstract TFormulaInfo`	`isInfinity(TFormulaInfo pParam)`
`BooleanFormula`	`isNaN(FloatingPointFormula pNumber)`	Check whether a floating-point number is NaN.
`protected abstract TFormulaInfo`	`isNaN(TFormulaInfo pParam)`
`BooleanFormula`	`isNegative(FloatingPointFormula pNumber)`	Checks whether a formula is negative, including -0.0.
`protected abstract TFormulaInfo`	`isNegative(TFormulaInfo pParam)`
`protected static boolean`	`isNegativeZero(Double pN)`
`BooleanFormula`	`isNormal(FloatingPointFormula pNumber)`	Checks whether a formula is normal FP number.
`protected abstract TFormulaInfo`	`isNormal(TFormulaInfo pParam)`
`BooleanFormula`	`isSubnormal(FloatingPointFormula pNumber)`	Checks whether a formula is subnormal FP number.
`protected abstract TFormulaInfo`	`isSubnormal(TFormulaInfo pParam)`
`BooleanFormula`	`isZero(FloatingPointFormula pNumber)`	Checks whether a formula is positive or negative zero.
`protected abstract TFormulaInfo`	`isZero(TFormulaInfo pParam)`
`BooleanFormula`	`lessOrEquals(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2)`	Returns whether an FP number is less or equal than another FP number.
`protected abstract TFormulaInfo`	`lessOrEquals(TFormulaInfo pParam1, TFormulaInfo pParam2)`
`BooleanFormula`	`lessThan(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2)`	Returns whether an FP number is less than another FP number.
`protected abstract TFormulaInfo`	`lessThan(TFormulaInfo pParam1, TFormulaInfo pParam2)`
`FloatingPointFormula`	`makeMinusInfinity(FormulaType.FloatingPointType pType)`
`protected abstract TFormulaInfo`	`makeMinusInfinityImpl(FormulaType.FloatingPointType pType)`
`FloatingPointFormula`	`makeNaN(FormulaType.FloatingPointType pType)`
`protected abstract TFormulaInfo`	`makeNaNImpl(FormulaType.FloatingPointType pType)`
`FloatingPointFormula`	`makeNumber(double n, FormulaType.FloatingPointType type)`	Creates a floating point formula representing the given double value with the specified type.
`FloatingPointFormula`	`makeNumber(double n, FormulaType.FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode)`	Creates a floating point formula representing the given double value with the specified type and rounding mode.
`FloatingPointFormula`	`makeNumber(String n, FormulaType.FloatingPointType type)`	Creates a floating point formula representing the given string value with the specified type.
`FloatingPointFormula`	`makeNumber(String n, FormulaType.FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode)`	Creates a floating point formula representing the given string value with the specified type and rounding mode.
`FloatingPointFormula`	`makeNumber(BigDecimal n, FormulaType.FloatingPointType type)`	Creates a floating point formula representing the given BigDecimal value with the specified type.
`FloatingPointFormula`	`makeNumber(BigDecimal n, FormulaType.FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode)`	Creates a floating point formula representing the given BigDecimal value with the specified type and rounding mode.
`FloatingPointFormula`	`makeNumber(BigInteger exponent, BigInteger mantissa, FloatingPointNumber.Sign sign, FormulaType.FloatingPointType type)`	Creates a floating point formula from the given exponent, mantissa, and sign with the specified type.
`FloatingPointFormula`	`makeNumber(Rational n, FormulaType.FloatingPointType type)`	Creates a floating point formula representing the given Rational value with the specified type.
`FloatingPointFormula`	`makeNumber(Rational n, FormulaType.FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode)`	Creates a floating point formula representing the given Rational value with the specified type and rounding mode.
`protected abstract TFormulaInfo`	`makeNumberAndRound(String pN, FormulaType.FloatingPointType pType, TFormulaInfo pFloatingPointRoundingMode)`	Parses the provided string and converts it into a floating-point formula.
`protected abstract TFormulaInfo`	`makeNumberImpl(double n, FormulaType.FloatingPointType type, TFormulaInfo pFloatingPointRoundingMode)`
`protected TFormulaInfo`	`makeNumberImpl(String n, FormulaType.FloatingPointType type, TFormulaInfo pFloatingPointRoundingMode)`	directly catch the most common special String constants.
`protected TFormulaInfo`	`makeNumberImpl(BigDecimal n, FormulaType.FloatingPointType type, TFormulaInfo pFloatingPointRoundingMode)`
`protected abstract TFormulaInfo`	`makeNumberImpl(BigInteger exponent, BigInteger mantissa, FloatingPointNumber.Sign sign, FormulaType.FloatingPointType type)`
`FloatingPointFormula`	`makePlusInfinity(FormulaType.FloatingPointType pType)`
`protected abstract TFormulaInfo`	`makePlusInfinityImpl(FormulaType.FloatingPointType pType)`
`FloatingPointFormula`	`makeVariable(String pVar, FormulaType.FloatingPointType pType)`	Creates a variable with exactly the given name.
`protected abstract TFormulaInfo`	`makeVariableImpl(String pVar, FormulaType.FloatingPointType pType)`
`FloatingPointFormula`	`max(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2)`	Returns the maximum value of the two given floating-point numbers.
`protected abstract TFormulaInfo`	`max(TFormulaInfo pParam1, TFormulaInfo pParam2)`
`FloatingPointFormula`	`min(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2)`	Returns the minimum value of the two given floating-point numbers.
`protected abstract TFormulaInfo`	`min(TFormulaInfo pParam1, TFormulaInfo pParam2)`
`FloatingPointFormula`	`multiply(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2)`
`FloatingPointFormula`	`multiply(FloatingPointFormula number1, FloatingPointFormula number2, FloatingPointRoundingMode pFloatingPointRoundingMode)`
`protected abstract TFormulaInfo`	`multiply(TFormulaInfo pParam1, TFormulaInfo pParam2, TFormulaInfo pFloatingPointRoundingMode)`
`FloatingPointFormula`	`negate(FloatingPointFormula pNumber)`
`protected abstract TFormulaInfo`	`negate(TFormulaInfo pParam1)`
`FloatingPointFormula`	`remainder(FloatingPointFormula number1, FloatingPointFormula number2)`	remainder: x - y * n, where n in Z is nearest to x/y.
`protected abstract TFormulaInfo`	`remainder(TFormulaInfo pParam1, TFormulaInfo pParam2)`
`FloatingPointFormula`	`round(FloatingPointFormula pFormula, FloatingPointRoundingMode pRoundingMode)`
`protected abstract TFormulaInfo`	`round(TFormulaInfo pFormula, FloatingPointRoundingMode pRoundingMode)`
`FloatingPointFormula`	`sqrt(FloatingPointFormula pNumber)`
`FloatingPointFormula`	`sqrt(FloatingPointFormula number, FloatingPointRoundingMode pFloatingPointRoundingMode)`
`protected abstract TFormulaInfo`	`sqrt(TFormulaInfo pNumber, TFormulaInfo pRoundingMode)`
`FloatingPointFormula`	`subtract(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2)`
`FloatingPointFormula`	`subtract(FloatingPointFormula number1, FloatingPointFormula number2, FloatingPointRoundingMode pFloatingPointRoundingMode)`
`protected abstract TFormulaInfo`	`subtract(TFormulaInfo pParam1, TFormulaInfo pParam2, TFormulaInfo pFloatingPointRoundingMode)`
`BitvectorFormula`	`toIeeeBitvector(FloatingPointFormula pNumber)`	Create a formula that produces a representation of the given floating-point value as a bitvector conforming to the IEEE 754-2008 format.
`AbstractFloatingPointFormulaManager.BitvectorFormulaAndBooleanFormula`	`toIeeeBitvector(FloatingPointFormula f, String bitvectorConstantName)`	Create a formula that produces a representation of the given floating-point value as a bitvector conforming to the IEEE 754-2008 format.
`AbstractFloatingPointFormulaManager.BitvectorFormulaAndBooleanFormula`	`toIeeeBitvector(FloatingPointFormula f, String bitvectorConstantName, Map<FloatingPointFormula,BitvectorFormula> specialFPConstantHandling)`	Create a formula that produces a representation of the given floating-point value as a bitvector conforming to the IEEE 754-2008 format.
`protected TFormulaInfo`	`toIeeeBitvectorImpl(TFormulaInfo pNumber)`
`protected TType`	`toSolverType(FormulaType<?> formulaType)`
`protected FloatingPointFormula`	`wrap(TFormulaInfo pTerm)`

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

Methods inherited from interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager
castTo, castTo, makeNumber, makeNumber

Field Detail

formulaCreator

protected final FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> formulaCreator

Constructor Detail

AbstractFloatingPointFormulaManager

protected AbstractFloatingPointFormulaManager(FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> pCreator,
                                              AbstractBitvectorFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> pBvMgr,
                                              AbstractBooleanFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> pBMgr)

Method Detail
- getDefaultRoundingMode
```
protected abstract TFormulaInfo getDefaultRoundingMode()
```
- getRoundingModeImpl
```
protected abstract TFormulaInfo getRoundingModeImpl(FloatingPointRoundingMode pFloatingPointRoundingMode)
```
- wrap
```
protected FloatingPointFormula wrap(TFormulaInfo pTerm)
```
- makeNumber
```
public FloatingPointFormula makeNumber(Rational n,
                                       FormulaType.FloatingPointType type)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Creates a floating point formula representing the given Rational value with the specified type.
  
  Specified by:
  
  makeNumber in interface FloatingPointFormulaManager
- makeNumber
```
public FloatingPointFormula makeNumber(Rational n,
                                       FormulaType.FloatingPointType type,
                                       FloatingPointRoundingMode pFloatingPointRoundingMode)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Creates a floating point formula representing the given Rational value with the specified type and rounding mode.
  
  Specified by:
  
  makeNumber in interface FloatingPointFormulaManager
- makeNumber
```
public FloatingPointFormula makeNumber(double n,
                                       FormulaType.FloatingPointType type)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Creates a floating point formula representing the given double value with the specified type.
  
  Specified by:
  
  makeNumber in interface FloatingPointFormulaManager
- makeNumber
```
public FloatingPointFormula makeNumber(double n,
                                       FormulaType.FloatingPointType type,
                                       FloatingPointRoundingMode pFloatingPointRoundingMode)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Creates a floating point formula representing the given double value with the specified type and rounding mode.
  
  Specified by:
  
  makeNumber in interface FloatingPointFormulaManager
- makeNumberImpl
```
protected abstract TFormulaInfo makeNumberImpl(double n,
                                               FormulaType.FloatingPointType type,
                                               TFormulaInfo pFloatingPointRoundingMode)
```
- makeNumber
```
public FloatingPointFormula makeNumber(BigDecimal n,
                                       FormulaType.FloatingPointType type)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Creates a floating point formula representing the given BigDecimal value with the specified type.
  
  Specified by:
  
  makeNumber in interface FloatingPointFormulaManager
- makeNumber
```
public FloatingPointFormula makeNumber(BigDecimal n,
                                       FormulaType.FloatingPointType type,
                                       FloatingPointRoundingMode pFloatingPointRoundingMode)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Creates a floating point formula representing the given BigDecimal value with the specified type and rounding mode.
  
  Specified by:
  
  makeNumber in interface FloatingPointFormulaManager
- makeNumberImpl
```
protected TFormulaInfo makeNumberImpl(BigDecimal n,
                                      FormulaType.FloatingPointType type,
                                      TFormulaInfo pFloatingPointRoundingMode)
```
- makeNumber
```
public FloatingPointFormula makeNumber(String n,
                                       FormulaType.FloatingPointType type)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Creates a floating point formula representing the given string value with the specified type.
  The string can be any valid floating-point number, e.g., "1.0", "1.0e-3", but also special values like "NaN", "Infinity", or "-0.0", etc. A leading "+" sign or "-" sign is allowed.
  
  Specified by:
  
  makeNumber in interface FloatingPointFormulaManager
- makeNumber
```
public FloatingPointFormula makeNumber(String n,
                                       FormulaType.FloatingPointType type,
                                       FloatingPointRoundingMode pFloatingPointRoundingMode)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Creates a floating point formula representing the given string value with the specified type and rounding mode.
  The string can be any valid floating-point number, e.g., "1.0", "1.0e-3", but also special values like "NaN", "Infinity", or "-0.0", etc. A leading "+" sign or "-" sign is allowed.
  
  Specified by:
  
  makeNumber in interface FloatingPointFormulaManager
- makeNumberImpl
```
protected TFormulaInfo makeNumberImpl(String n,
                                      FormulaType.FloatingPointType type,
                                      TFormulaInfo pFloatingPointRoundingMode)
```
  directly catch the most common special String constants.
- makeNumber
```
public FloatingPointFormula makeNumber(BigInteger exponent,
                                       BigInteger mantissa,
                                       FloatingPointNumber.Sign sign,
                                       FormulaType.FloatingPointType type)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Creates a floating point formula from the given exponent, mantissa, and sign with the specified type.
  
  Specified by:
  
  makeNumber in interface FloatingPointFormulaManager
  
  Parameters:
  
  exponent - the exponent part of the floating point number
  
  mantissa - the mantissa part of the floating point number
  
  sign - the sign of the floating point number
- makeNumberImpl
```
protected abstract TFormulaInfo makeNumberImpl(BigInteger exponent,
                                               BigInteger mantissa,
                                               FloatingPointNumber.Sign sign,
                                               FormulaType.FloatingPointType type)
```
- isNegativeZero
```
protected static boolean isNegativeZero(Double pN)
```
- makeNumberAndRound
```
protected abstract TFormulaInfo makeNumberAndRound(String pN,
                                                   FormulaType.FloatingPointType pType,
                                                   TFormulaInfo pFloatingPointRoundingMode)
```
  Parses the provided string and converts it into a floating-point formula.
  The input string must represent a valid finite floating-point number. Values such as NaN, Infinity, or -Infinity are not allowed and should be handled before calling this method.
- makeVariable
```
public FloatingPointFormula makeVariable(String pVar,
                                         FormulaType.FloatingPointType pType)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Creates a variable with exactly the given name.
  Please make sure that the given name is valid in SMT-LIB2. Take a look at FormulaManager.isValidName(java.lang.String) for further information.
  This method does not quote or unquote the given name, but uses the plain name "AS IS". Formula.toString() can return a different String than the given one.
  
  Specified by:
  
  makeVariable in interface FloatingPointFormulaManager
- makeVariableImpl
```
protected abstract TFormulaInfo makeVariableImpl(String pVar,
                                                 FormulaType.FloatingPointType pType)
```
- makePlusInfinity
```
public FloatingPointFormula makePlusInfinity(FormulaType.FloatingPointType pType)
```
  Specified by:
  
  makePlusInfinity in interface FloatingPointFormulaManager
- makePlusInfinityImpl
```
protected abstract TFormulaInfo makePlusInfinityImpl(FormulaType.FloatingPointType pType)
```
- makeMinusInfinity
```
public FloatingPointFormula makeMinusInfinity(FormulaType.FloatingPointType pType)
```
  Specified by:
  
  makeMinusInfinity in interface FloatingPointFormulaManager
- makeMinusInfinityImpl
```
protected abstract TFormulaInfo makeMinusInfinityImpl(FormulaType.FloatingPointType pType)
```
- makeNaN
```
public FloatingPointFormula makeNaN(FormulaType.FloatingPointType pType)
```
  Specified by:
  
  makeNaN in interface FloatingPointFormulaManager
- makeNaNImpl
```
protected abstract TFormulaInfo makeNaNImpl(FormulaType.FloatingPointType pType)
```
- castTo
```
public <T extends Formula> T castTo(FloatingPointFormula pNumber,
                                    boolean pSigned,
                                    FormulaType<T> pTargetType)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Build a formula of compatible type from a FloatingPointFormula. This method uses the default rounding mode.
  Compatible formula types are all numeral types and (signed/unsigned) bitvector types. It is also possible to cast a floating-point number into another floating-point type. We do not support casting from boolean or array types. We try to keep an exact representation, however fall back to rounding if needed.
  
  Specified by:
  
  castTo in interface FloatingPointFormulaManager
  
  Parameters:
  
  pNumber - the source formula of floating-point type
  
  pSigned - if a BitvectorFormula is given as target, we additionally use this flag. Otherwise, we ignore it.
  
  pTargetType - the type of the resulting formula
- castTo
```
public <T extends Formula> T castTo(FloatingPointFormula number,
                                    boolean pSigned,
                                    FormulaType<T> targetType,
                                    FloatingPointRoundingMode pFloatingPointRoundingMode)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Build a formula of compatible type from a FloatingPointFormula.
  Compatible formula types are all numeral types and (signed/unsigned) bitvector types. It is also possible to cast a floating-point number into another floating-point type. We do not support casting from boolean or array types. We try to keep an exact representation, however fall back to rounding if needed.
  
  Specified by:
  
  castTo in interface FloatingPointFormulaManager
  
  Parameters:
  
  number - the source formula of floating-point type
  
  pSigned - if a BitvectorFormula is given as target, we additionally use this flag. Otherwise, we ignore it.
  
  targetType - the type of the resulting formula
  
  pFloatingPointRoundingMode - if rounding is needed, we apply the rounding mode.
- castToImpl
```
protected abstract TFormulaInfo castToImpl(TFormulaInfo pNumber,
                                           boolean pSigned,
                                           FormulaType<?> pTargetType,
                                           TFormulaInfo pRoundingMode)
```
- castFrom
```
public FloatingPointFormula castFrom(Formula pNumber,
                                     boolean pSigned,
                                     FormulaType.FloatingPointType pTargetType)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Build a FloatingPointFormula from another compatible formula. This method uses the default rounding mode.
  Compatible formula types are all numeral types and (signed/unsigned) bitvector types. It is also possible to cast a floating-point number into another floating-point type. We do not support casting from boolean or array types. We try to keep an exact representation, however fall back to rounding if needed.
  
  Specified by:
  
  castFrom in interface FloatingPointFormulaManager
  
  Parameters:
  
  pNumber - the source formula of compatible type
  
  pSigned - if a BitvectorFormula is given as source, we additionally use this flag. Otherwise, we ignore it.
  
  pTargetType - the type of the resulting formula
- castFrom
```
public FloatingPointFormula castFrom(Formula number,
                                     boolean signed,
                                     FormulaType.FloatingPointType targetType,
                                     FloatingPointRoundingMode pFloatingPointRoundingMode)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Build a FloatingPointFormula from another compatible formula.
  Compatible formula types are all numeral types and (signed/unsigned) bitvector types. It is also possible to cast a floating-point number into another floating-point type. We do not support casting from boolean or array types. We try to keep an exact representation, however fall back to rounding if needed.
  
  Specified by:
  
  castFrom in interface FloatingPointFormulaManager
  
  Parameters:
  
  number - the source formula of compatible type
  
  signed - if a BitvectorFormula is given as source, we additionally use this flag. Otherwise, we ignore it.
  
  targetType - the type of the resulting formula
  
  pFloatingPointRoundingMode - if rounding is needed, we apply the rounding mode.
- castFromImpl
```
protected abstract TFormulaInfo castFromImpl(TFormulaInfo pNumber,
                                             boolean pSigned,
                                             FormulaType.FloatingPointType pTargetType,
                                             TFormulaInfo pRoundingMode)
```
- fromIeeeBitvector
```
public FloatingPointFormula fromIeeeBitvector(BitvectorFormula pNumber,
                                              FormulaType.FloatingPointType pTargetType)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Create a formula that interprets the given bitvector as a floating-point value in the IEEE format, according to the given type. The sum of the sizes of exponent and mantissa of the target type plus 1 (for the sign bit) needs to be equal to the size of the bitvector.
  Note: This method will return a value that is (numerically) far away from the original value. This method is completely different from FloatingPointFormulaManager.castFrom(org.sosy_lab.java_smt.api.Formula, boolean, org.sosy_lab.java_smt.api.FormulaType.FloatingPointType), which will produce a floating-point value close to the numeral value.
  
  Specified by:
  
  fromIeeeBitvector in interface FloatingPointFormulaManager
- fromIeeeBitvectorImpl
```
protected abstract TFormulaInfo fromIeeeBitvectorImpl(TFormulaInfo pNumber,
                                                      FormulaType.FloatingPointType pTargetType)
```
- toIeeeBitvector
```
public BitvectorFormula toIeeeBitvector(FloatingPointFormula pNumber)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Create a formula that produces a representation of the given floating-point value as a bitvector conforming to the IEEE 754-2008 format. The size of the resulting bitvector is the sum of the sizes of the exponent and mantissa of the input formula plus 1 (for the sign bit).
  
  Specified by:
  
  toIeeeBitvector in interface FloatingPointFormulaManager
- toIeeeBitvectorImpl
```
protected TFormulaInfo toIeeeBitvectorImpl(TFormulaInfo pNumber)
```
- toIeeeBitvector
```
public AbstractFloatingPointFormulaManager.BitvectorFormulaAndBooleanFormula toIeeeBitvector(FloatingPointFormula f,
                                                                                             String bitvectorConstantName)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Create a formula that produces a representation of the given floating-point value as a bitvector conforming to the IEEE 754-2008 format. The size of the resulting bitvector is the sum of the sizes of the exponent and mantissa of the input formula plus 1 (for the sign bit). This implementation can be used independently of FloatingPointFormulaManager.toIeeeBitvector(FloatingPointFormula), as it does not rely on an SMT solvers support for FloatingPointFormulaManager.toIeeeBitvector(FloatingPointFormula). Behavior for special FP values (NaN, Inf, etc.) is not defined, and returned values are solver dependent. In case you want to define how to handle those values, please use FloatingPointFormulaManager.toIeeeBitvector(FloatingPointFormula, String, Map). This method is based on a suggestion in the SMTLib2 standard (source) implementation:
  (declare-fun b () (_ BitVec m))
  (assert (= ((_ to_fp eb sb) b) f))
  Note: SMTLIB2 output of this method uses the SMTLIB2 keyword 'to_fp' as described above and no keyword variation for floating-point to bitvector conversion like 'fp.as_ieee_bv'.
  
  Specified by:
  
  toIeeeBitvector in interface FloatingPointFormulaManager
  
  Parameters:
  
  f - the FloatingPointFormula to be converted into an IEEE bitvector.
  
  bitvectorConstantName - the name of the returned BitvectorFormula.
  
  Returns:
  
  AbstractFloatingPointFormulaManager.BitvectorFormulaAndBooleanFormula consisting of the transformed input floating-point as a BitvectorFormula and the additional constraint as BooleanFormula.
- toIeeeBitvector
```
public AbstractFloatingPointFormulaManager.BitvectorFormulaAndBooleanFormula toIeeeBitvector(FloatingPointFormula f,
                                                                                             String bitvectorConstantName,
                                                                                             Map<FloatingPointFormula,BitvectorFormula> specialFPConstantHandling)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Create a formula that produces a representation of the given floating-point value as a bitvector conforming to the IEEE 754-2008 format. The size of the resulting bitvector is the sum of the sizes of the exponent and mantissa of the input formula plus 1 (for the sign bit). This implementation can be used independently of FloatingPointFormulaManager.toIeeeBitvector(FloatingPointFormula), as it does not rely on an SMT solvers support for FloatingPointFormulaManager.toIeeeBitvector(FloatingPointFormula). Behavior for special FP values (NaN, Inf, etc.) can be defined using the specialFPConstantHandling parameter. This method is based on a suggestion in the SMTLib2 standard (source) implementation:
  (declare-fun b () (_ BitVec m))
  (assert (= ((_ to_fp eb sb) b) f))
  Note: SMTLIB2 output of this method uses the SMTLIB2 keyword 'to_fp' as described above and no keyword variation for floating-point to bitvector conversion like 'fp.as_ieee_bv'.
  
  Specified by:
  
  toIeeeBitvector in interface FloatingPointFormulaManager
  
  Parameters:
  
  f - the FloatingPointFormula to be converted into an IEEE bitvector.
  
  bitvectorConstantName - the name of the returned BitvectorFormula.
  
  specialFPConstantHandling - a Map defining the returned BitvectorFormula for special FloatingPointFormula constant numbers. You are only allowed to specify a mapping for special FP numbers with more than one well-defined bitvector representation, i.e. NaN and +/- Infinity. The width of the mapped bitvector values has to match the expected width of the bitvector return value. The FormulaType.FloatingPointType, i.e. precision, of the key FP numbers has to match the FormulaType.FloatingPointType of the parameter number. For an empty Map, or missing mappings, this method behaves like FloatingPointFormulaManager.toIeeeBitvector(FloatingPointFormula, String).
  
  Returns:
  
  AbstractFloatingPointFormulaManager.BitvectorFormulaAndBooleanFormula consisting of the transformed input floating-point as a BitvectorFormula and the additional constraint as BooleanFormula.
- getMantissaSizeWithSignBit
```
public int getMantissaSizeWithSignBit(FloatingPointFormula f)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Returns the size of the mantissa (also called a coefficient or significant), including the sign bit, for the given FloatingPointFormula.
  
  Specified by:
  
  getMantissaSizeWithSignBit in interface FloatingPointFormulaManager
- getMantissaSizeWithSignBitImpl
```
protected abstract int getMantissaSizeWithSignBitImpl(TFormulaInfo f)
```
- getExponentSize
```
public int getExponentSize(FloatingPointFormula f)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Returns the size of the exponent for the given FloatingPointFormula.
  
  Specified by:
  
  getExponentSize in interface FloatingPointFormulaManager
- getExponentSizeImpl
```
protected abstract int getExponentSizeImpl(TFormulaInfo f)
```
- negate
```
public FloatingPointFormula negate(FloatingPointFormula pNumber)
```
  Specified by:
  
  negate in interface FloatingPointFormulaManager
- negate
```
protected abstract TFormulaInfo negate(TFormulaInfo pParam1)
```
- abs
```
public FloatingPointFormula abs(FloatingPointFormula pNumber)
```
  Specified by:
  
  abs in interface FloatingPointFormulaManager
- abs
```
protected abstract TFormulaInfo abs(TFormulaInfo pParam1)
```
- max
```
public FloatingPointFormula max(FloatingPointFormula pNumber1,
                                FloatingPointFormula pNumber2)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Returns the maximum value of the two given floating-point numbers. If one of the numbers is NaN, the other number is returned.
  
  Specified by:
  
  max in interface FloatingPointFormulaManager
- max
```
protected abstract TFormulaInfo max(TFormulaInfo pParam1,
                                    TFormulaInfo pParam2)
```
- min
```
public FloatingPointFormula min(FloatingPointFormula pNumber1,
                                FloatingPointFormula pNumber2)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Returns the minimum value of the two given floating-point numbers. If one of the numbers is NaN, the other number is returned.
  
  Specified by:
  
  min in interface FloatingPointFormulaManager
- min
```
protected abstract TFormulaInfo min(TFormulaInfo pParam1,
                                    TFormulaInfo pParam2)
```
- sqrt
```
public FloatingPointFormula sqrt(FloatingPointFormula pNumber)
```
  Specified by:
  
  sqrt in interface FloatingPointFormulaManager
- sqrt
```
public FloatingPointFormula sqrt(FloatingPointFormula number,
                                 FloatingPointRoundingMode pFloatingPointRoundingMode)
```
  Specified by:
  
  sqrt in interface FloatingPointFormulaManager
- sqrt
```
protected abstract TFormulaInfo sqrt(TFormulaInfo pNumber,
                                     TFormulaInfo pRoundingMode)
```
- add
```
public FloatingPointFormula add(FloatingPointFormula pNumber1,
                                FloatingPointFormula pNumber2)
```
  Specified by:
  
  add in interface FloatingPointFormulaManager
- add
```
public FloatingPointFormula add(FloatingPointFormula number1,
                                FloatingPointFormula number2,
                                FloatingPointRoundingMode pFloatingPointRoundingMode)
```
  Specified by:
  
  add in interface FloatingPointFormulaManager
- add
```
protected abstract TFormulaInfo add(TFormulaInfo pParam1,
                                    TFormulaInfo pParam2,
                                    TFormulaInfo pRoundingMode)
```
- subtract
```
public FloatingPointFormula subtract(FloatingPointFormula pNumber1,
                                     FloatingPointFormula pNumber2)
```
  Specified by:
  
  subtract in interface FloatingPointFormulaManager
- subtract
```
public FloatingPointFormula subtract(FloatingPointFormula number1,
                                     FloatingPointFormula number2,
                                     FloatingPointRoundingMode pFloatingPointRoundingMode)
```
  Specified by:
  
  subtract in interface FloatingPointFormulaManager
- subtract
```
protected abstract TFormulaInfo subtract(TFormulaInfo pParam1,
                                         TFormulaInfo pParam2,
                                         TFormulaInfo pFloatingPointRoundingMode)
```
- divide
```
public FloatingPointFormula divide(FloatingPointFormula pNumber1,
                                   FloatingPointFormula pNumber2)
```
  Specified by:
  
  divide in interface FloatingPointFormulaManager
- divide
```
public FloatingPointFormula divide(FloatingPointFormula number1,
                                   FloatingPointFormula number2,
                                   FloatingPointRoundingMode pFloatingPointRoundingMode)
```
  Specified by:
  
  divide in interface FloatingPointFormulaManager
- divide
```
protected abstract TFormulaInfo divide(TFormulaInfo pParam1,
                                       TFormulaInfo pParam2,
                                       TFormulaInfo pFloatingPointRoundingMode)
```
- multiply
```
public FloatingPointFormula multiply(FloatingPointFormula pNumber1,
                                     FloatingPointFormula pNumber2)
```
  Specified by:
  
  multiply in interface FloatingPointFormulaManager
- multiply
```
public FloatingPointFormula multiply(FloatingPointFormula number1,
                                     FloatingPointFormula number2,
                                     FloatingPointRoundingMode pFloatingPointRoundingMode)
```
  Specified by:
  
  multiply in interface FloatingPointFormulaManager
- multiply
```
protected abstract TFormulaInfo multiply(TFormulaInfo pParam1,
                                         TFormulaInfo pParam2,
                                         TFormulaInfo pFloatingPointRoundingMode)
```
- remainder
```
public FloatingPointFormula remainder(FloatingPointFormula number1,
                                      FloatingPointFormula number2)
```
  Description copied from interface: FloatingPointFormulaManager
  
  remainder: x - y * n, where n in Z is nearest to x/y. The result can be negative even for two positive arguments, e.g. "rem(5, 4) == 1" and "rem(5, 6) == -1", as opposed to integer modulo operators.
  
  Specified by:
  
  remainder in interface FloatingPointFormulaManager
- remainder
```
protected abstract TFormulaInfo remainder(TFormulaInfo pParam1,
                                          TFormulaInfo pParam2)
```
- assignment
```
public BooleanFormula assignment(FloatingPointFormula pNumber1,
                                 FloatingPointFormula pNumber2)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Create a term for assigning one floating-point term to another. This means both terms are considered equal afterward, based on their bit pattern (i.e., 0.0 != -0 .0 and NaN ==/!= NaN, depending on the bit pattern of each NaN). This method is the same as the method equal for other theories.
  
  Specified by:
  
  assignment in interface FloatingPointFormulaManager
- assignment
```
protected abstract TFormulaInfo assignment(TFormulaInfo pParam1,
                                           TFormulaInfo pParam2)
```
- equalWithFPSemantics
```
public BooleanFormula equalWithFPSemantics(FloatingPointFormula pNumber1,
                                           FloatingPointFormula pNumber2)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Create a term for comparing the equality of two floating-point terms, according to standard floating-point semantics (i.e., NaN != NaN and 0.0 == -0.0). Be careful to not use this method when you really need FloatingPointFormulaManager.assignment(FloatingPointFormula, FloatingPointFormula).
  
  Specified by:
  
  equalWithFPSemantics in interface FloatingPointFormulaManager
- equalWithFPSemantics
```
protected abstract TFormulaInfo equalWithFPSemantics(TFormulaInfo pParam1,
                                                     TFormulaInfo pParam2)
```
- greaterThan
```
public BooleanFormula greaterThan(FloatingPointFormula pNumber1,
                                  FloatingPointFormula pNumber2)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Returns whether an FP number is greater than another FP number. If one of the numbers is NaN, the result is always false.
  
  Specified by:
  
  greaterThan in interface FloatingPointFormulaManager
- greaterThan
```
protected abstract TFormulaInfo greaterThan(TFormulaInfo pParam1,
                                            TFormulaInfo pParam2)
```
- greaterOrEquals
```
public BooleanFormula greaterOrEquals(FloatingPointFormula pNumber1,
                                      FloatingPointFormula pNumber2)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Returns whether an FP number is greater or equal than another FP number. If one of the numbers is NaN, the result is always false.
  
  Specified by:
  
  greaterOrEquals in interface FloatingPointFormulaManager
- greaterOrEquals
```
protected abstract TFormulaInfo greaterOrEquals(TFormulaInfo pParam1,
                                                TFormulaInfo pParam2)
```
- lessThan
```
public BooleanFormula lessThan(FloatingPointFormula pNumber1,
                               FloatingPointFormula pNumber2)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Returns whether an FP number is less than another FP number. If one of the numbers is NaN, the result is always false.
  
  Specified by:
  
  lessThan in interface FloatingPointFormulaManager
- lessThan
```
protected abstract TFormulaInfo lessThan(TFormulaInfo pParam1,
                                         TFormulaInfo pParam2)
```
- lessOrEquals
```
public BooleanFormula lessOrEquals(FloatingPointFormula pNumber1,
                                   FloatingPointFormula pNumber2)
```
  Description copied from interface: FloatingPointFormulaManager
  
  Returns whether an FP number is less or equal than another FP number. If one of the numbers is NaN, the result is always false.
  
  Specified by:
  
  lessOrEquals in interface FloatingPointFormulaManager
- lessOrEquals
```
protected abstract TFormulaInfo lessOrEquals(TFormulaInfo pParam1,
                                             TFormulaInfo pParam2)
```
- isNaN
```
public BooleanFormula isNaN(FloatingPointFormula pNumber)
```
  Description copied from interface: FloatingPointFormulaManager
  Check whether a floating-point number is NaN.
  The bit patterns for NaN in SMTLIB are identical to IEEE 754:
  - sign=? (irrelevant for NaN)
  - exponent=11...11 (all bits are 1)
  - mantissa!=00...00 (mantissa is not all 0)
  Specified by:
  
  isNaN in interface FloatingPointFormulaManager
- isNaN
```
protected abstract TFormulaInfo isNaN(TFormulaInfo pParam)
```
- isInfinity
```
public BooleanFormula isInfinity(FloatingPointFormula pNumber)
```
  Description copied from interface: FloatingPointFormulaManager
  Checks whether a formula is positive or negative infinity.
  The bit patterns for infinity in SMTLIB are identical to IEEE 754:
  - sign=? (0 for +Inf, 1 for -Inf)
  - exponent=11...11 (all bits are 1)
  - mantissa=00...00 (all bits are 0)
  Specified by:
  
  isInfinity in interface FloatingPointFormulaManager
- isInfinity
```
protected abstract TFormulaInfo isInfinity(TFormulaInfo pParam)
```
- isZero
```
public BooleanFormula isZero(FloatingPointFormula pNumber)
```
  Description copied from interface: FloatingPointFormulaManager
  Checks whether a formula is positive or negative zero.
  The bit patterns for zero in SMTLIB are identical to IEEE 754:
  - sign=? (0 for +0, 1 for -0)
  - exponent=00...00 (all bits are 0)
  - mantissa=00...00 (all bits are 0)
  Specified by:
  
  isZero in interface FloatingPointFormulaManager
- isZero
```
protected abstract TFormulaInfo isZero(TFormulaInfo pParam)
```
- isSubnormal
```
public BooleanFormula isSubnormal(FloatingPointFormula pNumber)
```
  Description copied from interface: FloatingPointFormulaManager
  Checks whether a formula is subnormal FP number.
  The bit patterns for subnormal FP numbers in SMTLIB are identical to IEEE 754:
  - sign=? (0 for positive numbers, 1 for negative numbers)
  - exponent=00...00 (exponent is all 0)
  - mantissa!=00...00 (mantissa is not all 0)
  Specified by:
  
  isSubnormal in interface FloatingPointFormulaManager
- isSubnormal
```
protected abstract TFormulaInfo isSubnormal(TFormulaInfo pParam)
```
- isNormal
```
public BooleanFormula isNormal(FloatingPointFormula pNumber)
```
  Description copied from interface: FloatingPointFormulaManager
  Checks whether a formula is normal FP number.
  The bit patterns for normal FP numbers in SMTLIB are identical to IEEE 754:
  - sign=? (0 for positive numbers, 1 for negative numbers)
  - exponent!=00...00 and exponent!=11...11 (exponent is not all 0 or all 1)
  - mantissa=? (mantissa is irrelevant)
  Specified by:
  
  isNormal in interface FloatingPointFormulaManager
- isNormal
```
protected abstract TFormulaInfo isNormal(TFormulaInfo pParam)
```
- isNegative
```
public BooleanFormula isNegative(FloatingPointFormula pNumber)
```
  Description copied from interface: FloatingPointFormulaManager
  Checks whether a formula is negative, including -0.0.
  The bit patterns for negative FP numbers in SMTLIB are identical to IEEE 754:
  - sign=1 (1 for negative numbers)
  - number is not NaN, i.e., exponent=11...11 implies mantissa=00...00
  Specified by:
  
  isNegative in interface FloatingPointFormulaManager
- isNegative
```
protected abstract TFormulaInfo isNegative(TFormulaInfo pParam)
```
- round
```
public FloatingPointFormula round(FloatingPointFormula pFormula,
                                  FloatingPointRoundingMode pRoundingMode)
```
  Specified by:
  
  round in interface FloatingPointFormulaManager
- round
```
protected abstract TFormulaInfo round(TFormulaInfo pFormula,
                                      FloatingPointRoundingMode pRoundingMode)
```
- getBvRepresentation
```
protected static String getBvRepresentation(BigInteger integer,
                                            int size)
```
- getFormulaCreator
```
protected final FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> getFormulaCreator()
```
- extractInfo
```
protected final TFormulaInfo extractInfo(Formula pBits)
```
- toSolverType
```
protected final TType toSolverType(FormulaType<?> formulaType)
```

Class AbstractFloatingPointFormulaManager<TFormulaInfo,​TType,​TEnv,​TFuncDecl>

Nested Class Summary

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Methods inherited from interface org.sosy_lab.java_smt.api.FloatingPointFormulaManager

Field Detail

formulaCreator

Constructor Detail

AbstractFloatingPointFormulaManager

Method Detail

getDefaultRoundingMode

getRoundingModeImpl

wrap

makeNumber

makeNumber

makeNumber

makeNumber

makeNumberImpl

makeNumber

makeNumber

makeNumberImpl

makeNumber

makeNumber

makeNumberImpl

makeNumber

makeNumberImpl

isNegativeZero

makeNumberAndRound

makeVariable

makeVariableImpl

makePlusInfinity

makePlusInfinityImpl

makeMinusInfinity

makeMinusInfinityImpl

makeNaN

makeNaNImpl

castTo

castTo

castToImpl

castFrom

castFrom

castFromImpl

fromIeeeBitvector

fromIeeeBitvectorImpl

toIeeeBitvector

toIeeeBitvectorImpl

toIeeeBitvector

toIeeeBitvector

getMantissaSizeWithSignBit

getMantissaSizeWithSignBitImpl

getExponentSize

getExponentSizeImpl

negate

negate

abs

abs

max

max

min

min

sqrt

sqrt

sqrt

add

add

add

subtract

subtract

subtract

divide

divide

divide

multiply

multiply

multiply

remainder

remainder

assignment

Class AbstractFloatingPointFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>