Class AbstractFloatingPointFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>
- 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 implementingFloatingPointFormulaManager
. It handles all the unwrapping and wrapping from and to theFormula
instances, such that the concrete class needs to handle only its own internal types.For
multiply(FloatingPointFormula, FloatingPointFormula)
, anddivide(FloatingPointFormula, FloatingPointFormula)
this class even offers an implementation based on UFs. Sub-classes 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 sub-classes).
-
-
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)
-
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 aFloatingPointFormula
from another compatible formula.FloatingPointFormula
castFrom(Formula number, boolean signed, FormulaType.FloatingPointType targetType, FloatingPointRoundingMode pFloatingPointRoundingMode)
Build aFloatingPointFormula
from another compatible formula.protected abstract TFormulaInfo
castFromImpl(TFormulaInfo pNumber, boolean pSigned, FormulaType.FloatingPointType pTargetType, TFormulaInfo pRoundingMode)
<T extends Formula>
TcastTo(FloatingPointFormula pNumber, boolean pSigned, FormulaType<T> pTargetType)
Build a formula of compatible type from aFloatingPointFormula
.<T extends Formula>
TcastTo(FloatingPointFormula number, boolean pSigned, FormulaType<T> targetType, FloatingPointRoundingMode pFloatingPointRoundingMode)
Build a formula of compatible type from aFloatingPointFormula
.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
and0.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()
protected FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl>
getFormulaCreator()
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 format.protected abstract 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)
-
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
- Parameters:
exponent
- the exponent part of the floating point numbermantissa
- the mantissa part of the floating point numbersign
- 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 interfaceFloatingPointFormulaManager
-
makeVariableImpl
protected abstract TFormulaInfo makeVariableImpl(String pVar, FormulaType.FloatingPointType pType)
-
makePlusInfinity
public FloatingPointFormula makePlusInfinity(FormulaType.FloatingPointType pType)
- Specified by:
makePlusInfinity
in interfaceFloatingPointFormulaManager
-
makePlusInfinityImpl
protected abstract TFormulaInfo makePlusInfinityImpl(FormulaType.FloatingPointType pType)
-
makeMinusInfinity
public FloatingPointFormula makeMinusInfinity(FormulaType.FloatingPointType pType)
- Specified by:
makeMinusInfinity
in interfaceFloatingPointFormulaManager
-
makeMinusInfinityImpl
protected abstract TFormulaInfo makeMinusInfinityImpl(FormulaType.FloatingPointType pType)
-
makeNaN
public FloatingPointFormula makeNaN(FormulaType.FloatingPointType pType)
- Specified by:
makeNaN
in interfaceFloatingPointFormulaManager
-
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 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.
- Specified by:
castTo
in interfaceFloatingPointFormulaManager
- Parameters:
pNumber
- the source formula of floating-point typepSigned
- if aBitvectorFormula
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 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.
- Specified by:
castTo
in interfaceFloatingPointFormulaManager
- Parameters:
number
- the source formula of floating-point typepSigned
- 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.
-
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 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.
- Specified by:
castFrom
in interfaceFloatingPointFormulaManager
- Parameters:
pNumber
- the source formula of compatible typepSigned
- if aBitvectorFormula
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 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.
- Specified by:
castFrom
in interfaceFloatingPointFormulaManager
- Parameters:
number
- 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.
-
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 interfaceFloatingPointFormulaManager
-
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 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 interfaceFloatingPointFormulaManager
-
toIeeeBitvectorImpl
protected abstract TFormulaInfo toIeeeBitvectorImpl(TFormulaInfo pNumber)
-
negate
public FloatingPointFormula negate(FloatingPointFormula pNumber)
- Specified by:
negate
in interfaceFloatingPointFormulaManager
-
negate
protected abstract TFormulaInfo negate(TFormulaInfo pParam1)
-
abs
public FloatingPointFormula abs(FloatingPointFormula pNumber)
- Specified by:
abs
in interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
min
protected abstract TFormulaInfo min(TFormulaInfo pParam1, TFormulaInfo pParam2)
-
sqrt
public FloatingPointFormula sqrt(FloatingPointFormula pNumber)
- Specified by:
sqrt
in interfaceFloatingPointFormulaManager
-
sqrt
public FloatingPointFormula sqrt(FloatingPointFormula number, FloatingPointRoundingMode pFloatingPointRoundingMode)
- Specified by:
sqrt
in interfaceFloatingPointFormulaManager
-
sqrt
protected abstract TFormulaInfo sqrt(TFormulaInfo pNumber, TFormulaInfo pRoundingMode)
-
add
public FloatingPointFormula add(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2)
- Specified by:
add
in interfaceFloatingPointFormulaManager
-
add
public FloatingPointFormula add(FloatingPointFormula number1, FloatingPointFormula number2, FloatingPointRoundingMode pFloatingPointRoundingMode)
- Specified by:
add
in interfaceFloatingPointFormulaManager
-
add
protected abstract TFormulaInfo add(TFormulaInfo pParam1, TFormulaInfo pParam2, TFormulaInfo pRoundingMode)
-
subtract
public FloatingPointFormula subtract(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2)
- Specified by:
subtract
in interfaceFloatingPointFormulaManager
-
subtract
public FloatingPointFormula subtract(FloatingPointFormula number1, FloatingPointFormula number2, FloatingPointRoundingMode pFloatingPointRoundingMode)
- Specified by:
subtract
in interfaceFloatingPointFormulaManager
-
subtract
protected abstract TFormulaInfo subtract(TFormulaInfo pParam1, TFormulaInfo pParam2, TFormulaInfo pFloatingPointRoundingMode)
-
divide
public FloatingPointFormula divide(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2)
- Specified by:
divide
in interfaceFloatingPointFormulaManager
-
divide
public FloatingPointFormula divide(FloatingPointFormula number1, FloatingPointFormula number2, FloatingPointRoundingMode pFloatingPointRoundingMode)
- Specified by:
divide
in interfaceFloatingPointFormulaManager
-
divide
protected abstract TFormulaInfo divide(TFormulaInfo pParam1, TFormulaInfo pParam2, TFormulaInfo pFloatingPointRoundingMode)
-
multiply
public FloatingPointFormula multiply(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2)
- Specified by:
multiply
in interfaceFloatingPointFormulaManager
-
multiply
public FloatingPointFormula multiply(FloatingPointFormula number1, FloatingPointFormula number2, FloatingPointRoundingMode pFloatingPointRoundingMode)
- Specified by:
multiply
in interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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
andNaN ==/!= NaN
, depending on the bit pattern of each NaN). This method is the same as the methodequal
for other theories.- Specified by:
assignment
in interfaceFloatingPointFormulaManager
-
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
and0.0 == -0.0
). Be careful to not use this method when you really needFloatingPointFormulaManager.assignment(FloatingPointFormula, FloatingPointFormula)
.- Specified by:
equalWithFPSemantics
in interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
isNegative
protected abstract TFormulaInfo isNegative(TFormulaInfo pParam)
-
round
public FloatingPointFormula round(FloatingPointFormula pFormula, FloatingPointRoundingMode pRoundingMode)
- Specified by:
round
in interfaceFloatingPointFormulaManager
-
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)
-
-