Class DebuggingFloatingPointFormulaManager
- java.lang.Object
-
- org.sosy_lab.java_smt.delegate.debugging.DebuggingFloatingPointFormulaManager
-
- All Implemented Interfaces:
FloatingPointFormulaManager
public class DebuggingFloatingPointFormulaManager extends Object implements FloatingPointFormulaManager
-
-
Constructor Summary
Constructors Constructor Description DebuggingFloatingPointFormulaManager(FloatingPointFormulaManager pDelegate, org.sosy_lab.java_smt.delegate.debugging.DebuggingAssertions pDebugging)
-
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 aFloatingPointFormula
from another compatible formula.FloatingPointFormula
castFrom(Formula source, boolean signed, FormulaType.FloatingPointType targetType, FloatingPointRoundingMode pFloatingPointRoundingMode)
Build aFloatingPointFormula
from another compatible formula.<T extends Formula>
TcastTo(FloatingPointFormula source, boolean signed, FormulaType<T> targetType)
Build a formula of compatible type from aFloatingPointFormula
.<T extends Formula>
TcastTo(FloatingPointFormula source, boolean signed, FormulaType<T> targetType, FloatingPointRoundingMode pFloatingPointRoundingMode)
Build a formula of compatible type from aFloatingPointFormula
.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
and0.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.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 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
-
-
-
-
Constructor Detail
-
DebuggingFloatingPointFormulaManager
public DebuggingFloatingPointFormulaManager(FloatingPointFormulaManager pDelegate, org.sosy_lab.java_smt.delegate.debugging.DebuggingAssertions pDebugging)
-
-
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 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
-
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
-
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
-
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(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
-
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 interfaceFloatingPointFormulaManager
-
makePlusInfinity
public FloatingPointFormula makePlusInfinity(FormulaType.FloatingPointType type)
- Specified by:
makePlusInfinity
in interfaceFloatingPointFormulaManager
-
makeMinusInfinity
public FloatingPointFormula makeMinusInfinity(FormulaType.FloatingPointType type)
- Specified by:
makeMinusInfinity
in interfaceFloatingPointFormulaManager
-
makeNaN
public FloatingPointFormula makeNaN(FormulaType.FloatingPointType type)
- Specified by:
makeNaN
in interfaceFloatingPointFormulaManager
-
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 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:
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
-
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 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:
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.
-
castFrom
public FloatingPointFormula castFrom(Formula source, boolean signed, FormulaType.FloatingPointType targetType)
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:
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
-
castFrom
public FloatingPointFormula castFrom(Formula source, 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:
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.
-
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 interfaceFloatingPointFormulaManager
-
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 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
-
round
public FloatingPointFormula round(FloatingPointFormula formula, FloatingPointRoundingMode roundingMode)
- Specified by:
round
in interfaceFloatingPointFormulaManager
-
negate
public FloatingPointFormula negate(FloatingPointFormula number)
- Specified by:
negate
in interfaceFloatingPointFormulaManager
-
abs
public FloatingPointFormula abs(FloatingPointFormula number)
- Specified by:
abs
in interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
sqrt
public FloatingPointFormula sqrt(FloatingPointFormula number)
- Specified by:
sqrt
in interfaceFloatingPointFormulaManager
-
sqrt
public FloatingPointFormula sqrt(FloatingPointFormula number, FloatingPointRoundingMode roundingMode)
- Specified by:
sqrt
in interfaceFloatingPointFormulaManager
-
add
public FloatingPointFormula add(FloatingPointFormula number1, FloatingPointFormula number2)
- Specified by:
add
in interfaceFloatingPointFormulaManager
-
add
public FloatingPointFormula add(FloatingPointFormula number1, FloatingPointFormula number2, FloatingPointRoundingMode pFloatingPointRoundingMode)
- Specified by:
add
in interfaceFloatingPointFormulaManager
-
subtract
public FloatingPointFormula subtract(FloatingPointFormula number1, FloatingPointFormula number2)
- Specified by:
subtract
in interfaceFloatingPointFormulaManager
-
subtract
public FloatingPointFormula subtract(FloatingPointFormula number1, FloatingPointFormula number2, FloatingPointRoundingMode pFloatingPointRoundingMode)
- Specified by:
subtract
in interfaceFloatingPointFormulaManager
-
divide
public FloatingPointFormula divide(FloatingPointFormula number1, FloatingPointFormula number2)
- Specified by:
divide
in interfaceFloatingPointFormulaManager
-
divide
public FloatingPointFormula divide(FloatingPointFormula number1, FloatingPointFormula number2, FloatingPointRoundingMode pFloatingPointRoundingMode)
- Specified by:
divide
in interfaceFloatingPointFormulaManager
-
multiply
public FloatingPointFormula multiply(FloatingPointFormula number1, FloatingPointFormula number2)
- Specified by:
multiply
in interfaceFloatingPointFormulaManager
-
multiply
public FloatingPointFormula multiply(FloatingPointFormula number1, FloatingPointFormula number2, FloatingPointRoundingMode pFloatingPointRoundingMode)
- Specified by:
multiply
in interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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
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
-
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
and0.0 == -0.0
). Be careful to not use this method when you really needFloatingPointFormulaManager.assignment(FloatingPointFormula, FloatingPointFormula)
.- Specified by:
equalWithFPSemantics
in interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
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 interfaceFloatingPointFormulaManager
-
-