Interface FloatingPointFormulaManager
-
- All Known Implementing Classes:
AbstractFloatingPointFormulaManager
,DebuggingFloatingPointFormulaManager
public interface FloatingPointFormulaManager
Floating point operations.Most operations are overloaded: there is an option of either using the default rounding mode (set via the option
solver.floatingPointRoundingMode
), or providing the rounding mode explicitly.
-
-
Method Summary
-
-
-
Method Detail
-
makeNumber
FloatingPointFormula makeNumber(double n, FormulaType.FloatingPointType type)
-
makeNumber
FloatingPointFormula makeNumber(double n, FormulaType.FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode)
-
makeNumber
FloatingPointFormula makeNumber(BigDecimal n, FormulaType.FloatingPointType type)
-
makeNumber
FloatingPointFormula makeNumber(BigDecimal n, FormulaType.FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode)
-
makeNumber
FloatingPointFormula makeNumber(String n, FormulaType.FloatingPointType type)
-
makeNumber
FloatingPointFormula makeNumber(String n, FormulaType.FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode)
-
makeNumber
FloatingPointFormula makeNumber(Rational n, FormulaType.FloatingPointType type)
-
makeNumber
FloatingPointFormula makeNumber(Rational n, FormulaType.FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode)
-
makeNumber
FloatingPointFormula makeNumber(BigInteger exponent, BigInteger mantissa, boolean signBit, FormulaType.FloatingPointType type)
-
makeVariable
FloatingPointFormula makeVariable(String pVar, FormulaType.FloatingPointType type)
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.
-
makePlusInfinity
FloatingPointFormula makePlusInfinity(FormulaType.FloatingPointType type)
-
makeMinusInfinity
FloatingPointFormula makeMinusInfinity(FormulaType.FloatingPointType type)
-
makeNaN
FloatingPointFormula makeNaN(FormulaType.FloatingPointType type)
-
castTo
<T extends Formula> T castTo(FloatingPointFormula source, boolean signed, FormulaType<T> targetType)
Build a formula of compatible type from aFloatingPointFormula
. 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.
- Parameters:
source
- the source formula of floating-point typesigned
- if aBitvectorFormula
is given as target, we additionally use this flag. Otherwise, we ignore it.targetType
- the type of the resulting formula- Throws:
IllegalArgumentException
- if an incompatible type is used, e.g. aFloatingPointFormula
cannot be cast toBooleanFormula
.
-
castTo
<T extends Formula> T castTo(FloatingPointFormula source, boolean signed, FormulaType<T> targetType, FloatingPointRoundingMode pFloatingPointRoundingMode)
Build a formula of compatible type from aFloatingPointFormula
.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.
- Parameters:
source
- the source formula of floating-point typesigned
- if aBitvectorFormula
is given as target, we additionally use this flag. Otherwise, we ignore it.targetType
- the type of the resulting formulapFloatingPointRoundingMode
- if rounding is needed, we apply the rounding mode.- Throws:
IllegalArgumentException
- if an incompatible type is used, e.g. aFloatingPointFormula
cannot be cast toBooleanFormula
.
-
castFrom
FloatingPointFormula castFrom(Formula source, boolean signed, FormulaType.FloatingPointType targetType)
Build aFloatingPointFormula
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.
- Parameters:
source
- the source formula of compatible typesigned
- if aBitvectorFormula
is given as source, we additionally use this flag. Otherwise, we ignore it.targetType
- the type of the resulting formula- Throws:
IllegalArgumentException
- if an incompatible type is used, e.g. aBooleanFormula
cannot be cast toFloatingPointFormula
.
-
castFrom
FloatingPointFormula castFrom(Formula source, boolean signed, FormulaType.FloatingPointType targetType, FloatingPointRoundingMode pFloatingPointRoundingMode)
Build aFloatingPointFormula
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.
- Parameters:
source
- the source formula of compatible typesigned
- if aBitvectorFormula
is given as source, we additionally use this flag. Otherwise, we ignore it.targetType
- the type of the resulting formulapFloatingPointRoundingMode
- if rounding is needed, we apply the rounding mode.- Throws:
IllegalArgumentException
- if an incompatible type is used, e.g. aBooleanFormula
cannot be cast toFloatingPointFormula
.
-
fromIeeeBitvector
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. 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
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.
-
toIeeeBitvector
BitvectorFormula toIeeeBitvector(FloatingPointFormula number)
Create a formula that produces a representation of the given floating-point value as a bitvector conforming to the IEEE 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).
-
round
FloatingPointFormula round(FloatingPointFormula formula, FloatingPointRoundingMode roundingMode)
-
negate
FloatingPointFormula negate(FloatingPointFormula number)
-
abs
FloatingPointFormula abs(FloatingPointFormula number)
-
max
FloatingPointFormula max(FloatingPointFormula number1, FloatingPointFormula number2)
-
min
FloatingPointFormula min(FloatingPointFormula number1, FloatingPointFormula number2)
-
sqrt
FloatingPointFormula sqrt(FloatingPointFormula number)
-
sqrt
FloatingPointFormula sqrt(FloatingPointFormula number, FloatingPointRoundingMode roundingMode)
-
add
FloatingPointFormula add(FloatingPointFormula number1, FloatingPointFormula number2)
-
add
FloatingPointFormula add(FloatingPointFormula number1, FloatingPointFormula number2, FloatingPointRoundingMode pFloatingPointRoundingMode)
-
subtract
FloatingPointFormula subtract(FloatingPointFormula number1, FloatingPointFormula number2)
-
subtract
FloatingPointFormula subtract(FloatingPointFormula number1, FloatingPointFormula number2, FloatingPointRoundingMode pFloatingPointRoundingMode)
-
divide
FloatingPointFormula divide(FloatingPointFormula number1, FloatingPointFormula number2)
-
divide
FloatingPointFormula divide(FloatingPointFormula number1, FloatingPointFormula number2, FloatingPointRoundingMode pFloatingPointRoundingMode)
-
multiply
FloatingPointFormula multiply(FloatingPointFormula number1, FloatingPointFormula number2)
-
multiply
FloatingPointFormula multiply(FloatingPointFormula number1, FloatingPointFormula number2, FloatingPointRoundingMode pFloatingPointRoundingMode)
-
remainder
FloatingPointFormula remainder(FloatingPointFormula dividend, FloatingPointFormula divisor)
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.
-
assignment
BooleanFormula assignment(FloatingPointFormula number1, FloatingPointFormula number2)
Create a term for assigning one floating-point term to another. This means both terms are considered equal afterwards. This method is the same as the methodequal
for other theories.
-
equalWithFPSemantics
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). Be careful to not use this method when you really needassignment(FloatingPointFormula, FloatingPointFormula)
.
-
greaterThan
BooleanFormula greaterThan(FloatingPointFormula number1, FloatingPointFormula number2)
-
greaterOrEquals
BooleanFormula greaterOrEquals(FloatingPointFormula number1, FloatingPointFormula number2)
-
lessThan
BooleanFormula lessThan(FloatingPointFormula number1, FloatingPointFormula number2)
-
lessOrEquals
BooleanFormula lessOrEquals(FloatingPointFormula number1, FloatingPointFormula number2)
-
isNaN
BooleanFormula isNaN(FloatingPointFormula number)
-
isInfinity
BooleanFormula isInfinity(FloatingPointFormula number)
-
isZero
BooleanFormula isZero(FloatingPointFormula number)
-
isNormal
BooleanFormula isNormal(FloatingPointFormula number)
-
isSubnormal
BooleanFormula isSubnormal(FloatingPointFormula number)
-
isNegative
BooleanFormula isNegative(FloatingPointFormula number)
checks whether a formula is negative, including -0.0.
-
-