java.lang.Object
- org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager

All Implemented Interfaces:: FloatingPointFormulaManager

public class DebuggingFloatingPointFormulaManager
extends Object
implements FloatingPointFormulaManager

Method Summary

All Methods Instance Methods Concrete Methods
Modifier and Type	Method	Description
`FloatingPointFormula`	`abs(FloatingPointFormula number)`
`FloatingPointFormula`	`add(FloatingPointFormula number1, FloatingPointFormula number2)`
`FloatingPointFormula`	`add(FloatingPointFormula number1, FloatingPointFormula number2, FloatingPointRoundingMode pFloatingPointRoundingMode)`
`BooleanFormula`	`assignment(FloatingPointFormula number1, FloatingPointFormula number2)`	Create a term for assigning one floating-point term to another.
`FloatingPointFormula`	`castFrom(Formula source, boolean signed, FormulaType.FloatingPointType targetType)`	Build a `FloatingPointFormula` from another compatible formula.
`FloatingPointFormula`	`castFrom(Formula source, boolean signed, FormulaType.FloatingPointType targetType, FloatingPointRoundingMode pFloatingPointRoundingMode)`	Build a `FloatingPointFormula` from another compatible formula.
`<T extends Formula> T`	`castTo(FloatingPointFormula source, boolean signed, FormulaType<T> targetType)`	Build a formula of compatible type from a `FloatingPointFormula`.
`<T extends Formula> T`	`castTo(FloatingPointFormula source, boolean signed, FormulaType<T> targetType, FloatingPointRoundingMode pFloatingPointRoundingMode)`	Build a formula of compatible type from a `FloatingPointFormula`.
`FloatingPointFormula`	`divide(FloatingPointFormula number1, FloatingPointFormula number2)`
`FloatingPointFormula`	`divide(FloatingPointFormula number1, FloatingPointFormula number2, FloatingPointRoundingMode pFloatingPointRoundingMode)`
`BooleanFormula`	`equalWithFPSemantics(FloatingPointFormula number1, FloatingPointFormula number2)`	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`).
`FloatingPointFormula`	`fromIeeeBitvector(BitvectorFormula number, 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.
`int`	`getExponentSize(FloatingPointFormula number)`	Returns the size of the exponent for the given `FloatingPointFormula`.
`int`	`getMantissaSizeWithSignBit(FloatingPointFormula number)`	Returns the size of the mantissa (also called a coefficient or significant), including the sign bit, for the given `FloatingPointFormula`.
`BooleanFormula`	`greaterOrEquals(FloatingPointFormula number1, FloatingPointFormula number2)`	Returns whether an FP number is greater or equal than another FP number.
`BooleanFormula`	`greaterThan(FloatingPointFormula number1, FloatingPointFormula number2)`	Returns whether an FP number is greater than another FP number.
`BooleanFormula`	`isInfinity(FloatingPointFormula number)`	Checks whether a formula is positive or negative infinity.
`BooleanFormula`	`isNaN(FloatingPointFormula number)`	Check whether a floating-point number is NaN.
`BooleanFormula`	`isNegative(FloatingPointFormula number)`	Checks whether a formula is negative, including -0.0.
`BooleanFormula`	`isNormal(FloatingPointFormula number)`	Checks whether a formula is normal FP number.
`BooleanFormula`	`isSubnormal(FloatingPointFormula number)`	Checks whether a formula is subnormal FP number.
`BooleanFormula`	`isZero(FloatingPointFormula number)`	Checks whether a formula is positive or negative zero.
`BooleanFormula`	`lessOrEquals(FloatingPointFormula number1, FloatingPointFormula number2)`	Returns whether an FP number is less or equal than another FP number.
`BooleanFormula`	`lessThan(FloatingPointFormula number1, FloatingPointFormula number2)`	Returns whether an FP number is less than another FP number.
`FloatingPointFormula`	`makeMinusInfinity(FormulaType.FloatingPointType type)`
`FloatingPointFormula`	`makeNaN(FormulaType.FloatingPointType type)`
`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.
`FloatingPointFormula`	`makePlusInfinity(FormulaType.FloatingPointType type)`
`FloatingPointFormula`	`makeVariable(String pVar, FormulaType.FloatingPointType type)`	Creates a variable with exactly the given name.
`FloatingPointFormula`	`max(FloatingPointFormula number1, FloatingPointFormula number2)`	Returns the maximum value of the two given floating-point numbers.
`FloatingPointFormula`	`min(FloatingPointFormula number1, FloatingPointFormula number2)`	Returns the minimum value of the two given floating-point numbers.
`FloatingPointFormula`	`multiply(FloatingPointFormula number1, FloatingPointFormula number2)`
`FloatingPointFormula`	`multiply(FloatingPointFormula number1, FloatingPointFormula number2, FloatingPointRoundingMode pFloatingPointRoundingMode)`
`FloatingPointFormula`	`negate(FloatingPointFormula number)`
`FloatingPointFormula`	`remainder(FloatingPointFormula dividend, FloatingPointFormula divisor)`	remainder: x - y * n, where n in Z is nearest to x/y.
`FloatingPointFormula`	`round(FloatingPointFormula formula, FloatingPointRoundingMode roundingMode)`
`FloatingPointFormula`	`sqrt(FloatingPointFormula number)`
`FloatingPointFormula`	`sqrt(FloatingPointFormula number, FloatingPointRoundingMode roundingMode)`
`FloatingPointFormula`	`subtract(FloatingPointFormula number1, FloatingPointFormula number2)`
`FloatingPointFormula`	`subtract(FloatingPointFormula number1, FloatingPointFormula number2, FloatingPointRoundingMode pFloatingPointRoundingMode)`
`BitvectorFormula`	`toIeeeBitvector(FloatingPointFormula number)`	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 number, 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 number, 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.

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

- Method Detail
  - 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
  - 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
  - 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
  - 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(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
  - makeVariable
```
public FloatingPointFormula makeVariable(String pVar,
                                         FormulaType.FloatingPointType type)
```
    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
  - makePlusInfinity
```
public FloatingPointFormula makePlusInfinity(FormulaType.FloatingPointType type)
```
    Specified by:
    
    makePlusInfinity in interface FloatingPointFormulaManager
  - makeMinusInfinity
```
public FloatingPointFormula makeMinusInfinity(FormulaType.FloatingPointType type)
```
    Specified by:
    
    makeMinusInfinity in interface FloatingPointFormulaManager
  - makeNaN
```
public FloatingPointFormula makeNaN(FormulaType.FloatingPointType type)
```
    Specified by:
    
    makeNaN in interface FloatingPointFormulaManager
  - castTo
```
public <T extends Formula> T castTo(FloatingPointFormula source,
                                    boolean signed,
                                    FormulaType<T> targetType)
```
    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:
    
    source - the source formula of floating-point type
    
    signed - if a BitvectorFormula is given as target, we additionally use this flag. Otherwise, we ignore it.
    
    targetType - the type of the resulting formula
  - castTo
```
public <T extends Formula> T castTo(FloatingPointFormula source,
                                    boolean signed,
                                    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:
    
    source - the source formula of floating-point type
    
    signed - 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.
  - castFrom
```
public FloatingPointFormula castFrom(Formula source,
                                     boolean signed,
                                     FormulaType.FloatingPointType targetType)
```
    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:
    
    source - 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
  - castFrom
```
public FloatingPointFormula castFrom(Formula source,
                                     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:
    
    source - 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.
  - fromIeeeBitvector
```
public FloatingPointFormula fromIeeeBitvector(BitvectorFormula number,
                                              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
  - toIeeeBitvector
```
public BitvectorFormula toIeeeBitvector(FloatingPointFormula number)
```
    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
  - toIeeeBitvector
```
public AbstractFloatingPointFormulaManager.BitvectorFormulaAndBooleanFormula toIeeeBitvector(FloatingPointFormula number,
                                                                                             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:
    
    number - 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 number,
                                                                                             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:
    
    number - 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.
  - round
```
public FloatingPointFormula round(FloatingPointFormula formula,
                                  FloatingPointRoundingMode roundingMode)
```
    Specified by:
    
    round in interface FloatingPointFormulaManager
  - negate
```
public FloatingPointFormula negate(FloatingPointFormula number)
```
    Specified by:
    
    negate in interface FloatingPointFormulaManager
  - abs
```
public FloatingPointFormula abs(FloatingPointFormula number)
```
    Specified by:
    
    abs in interface FloatingPointFormulaManager
  - max
```
public FloatingPointFormula max(FloatingPointFormula number1,
                                FloatingPointFormula number2)
```
    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
  - min
```
public FloatingPointFormula min(FloatingPointFormula number1,
                                FloatingPointFormula number2)
```
    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
  - sqrt
```
public FloatingPointFormula sqrt(FloatingPointFormula number)
```
    Specified by:
    
    sqrt in interface FloatingPointFormulaManager
  - sqrt
```
public FloatingPointFormula sqrt(FloatingPointFormula number,
                                 FloatingPointRoundingMode roundingMode)
```
    Specified by:
    
    sqrt in interface FloatingPointFormulaManager
  - add
```
public FloatingPointFormula add(FloatingPointFormula number1,
                                FloatingPointFormula number2)
```
    Specified by:
    
    add in interface FloatingPointFormulaManager
  - add
```
public FloatingPointFormula add(FloatingPointFormula number1,
                                FloatingPointFormula number2,
                                FloatingPointRoundingMode pFloatingPointRoundingMode)
```
    Specified by:
    
    add in interface FloatingPointFormulaManager
  - subtract
```
public FloatingPointFormula subtract(FloatingPointFormula number1,
                                     FloatingPointFormula number2)
```
    Specified by:
    
    subtract in interface FloatingPointFormulaManager
  - subtract
```
public FloatingPointFormula subtract(FloatingPointFormula number1,
                                     FloatingPointFormula number2,
                                     FloatingPointRoundingMode pFloatingPointRoundingMode)
```
    Specified by:
    
    subtract in interface FloatingPointFormulaManager
  - divide
```
public FloatingPointFormula divide(FloatingPointFormula number1,
                                   FloatingPointFormula number2)
```
    Specified by:
    
    divide in interface FloatingPointFormulaManager
  - divide
```
public FloatingPointFormula divide(FloatingPointFormula number1,
                                   FloatingPointFormula number2,
                                   FloatingPointRoundingMode pFloatingPointRoundingMode)
```
    Specified by:
    
    divide in interface FloatingPointFormulaManager
  - multiply
```
public FloatingPointFormula multiply(FloatingPointFormula number1,
                                     FloatingPointFormula number2)
```
    Specified by:
    
    multiply in interface FloatingPointFormulaManager
  - multiply
```
public FloatingPointFormula multiply(FloatingPointFormula number1,
                                     FloatingPointFormula number2,
                                     FloatingPointRoundingMode pFloatingPointRoundingMode)
```
    Specified by:
    
    multiply in interface FloatingPointFormulaManager
  - remainder
```
public FloatingPointFormula remainder(FloatingPointFormula dividend,
                                      FloatingPointFormula divisor)
```
    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
  - assignment
```
public BooleanFormula assignment(FloatingPointFormula number1,
                                 FloatingPointFormula number2)
```
    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
  - equalWithFPSemantics
```
public BooleanFormula equalWithFPSemantics(FloatingPointFormula number1,
                                           FloatingPointFormula number2)
```
    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
  - greaterThan
```
public BooleanFormula greaterThan(FloatingPointFormula number1,
                                  FloatingPointFormula number2)
```
    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
  - greaterOrEquals
```
public BooleanFormula greaterOrEquals(FloatingPointFormula number1,
                                      FloatingPointFormula number2)
```
    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
  - lessThan
```
public BooleanFormula lessThan(FloatingPointFormula number1,
                               FloatingPointFormula number2)
```
    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
  - lessOrEquals
```
public BooleanFormula lessOrEquals(FloatingPointFormula number1,
                                   FloatingPointFormula number2)
```
    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
  - isNaN
```
public BooleanFormula isNaN(FloatingPointFormula number)
```
    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
  - isInfinity
```
public BooleanFormula isInfinity(FloatingPointFormula number)
```
    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
  - isZero
```
public BooleanFormula isZero(FloatingPointFormula number)
```
    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
  - isNormal
```
public BooleanFormula isNormal(FloatingPointFormula number)
```
    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
  - isSubnormal
```
public BooleanFormula isSubnormal(FloatingPointFormula number)
```
    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
  - isNegative
```
public BooleanFormula isNegative(FloatingPointFormula number)
```
    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
  - getMantissaSizeWithSignBit
```
public int getMantissaSizeWithSignBit(FloatingPointFormula number)
```
    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
  - getExponentSize
```
public int getExponentSize(FloatingPointFormula number)
```
    Description copied from interface: FloatingPointFormulaManager
    
    Returns the size of the exponent for the given FloatingPointFormula.
    
    Specified by:
    
    getExponentSize in interface FloatingPointFormulaManager

Class DebuggingFloatingPointFormulaManager

Method Summary

Methods inherited from class java.lang.Object

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

Method Detail

makeNumber

makeNumber

makeNumber

makeNumber

makeNumber

makeNumber

makeNumber

makeNumber

makeNumber

makeVariable

makePlusInfinity

makeMinusInfinity

makeNaN

castTo

castTo

castFrom

castFrom

fromIeeeBitvector

toIeeeBitvector

toIeeeBitvector

toIeeeBitvector

round

negate

abs

max

min

sqrt

sqrt

add

add

subtract

subtract

divide

divide

multiply

multiply

remainder

assignment

equalWithFPSemantics

greaterThan

greaterOrEquals

lessThan

lessOrEquals

isNaN

isInfinity

isZero

isNormal

isSubnormal

isNegative

getMantissaSizeWithSignBit

getExponentSize