Package org.sosy_lab.java_smt.basicimpl

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 implementing FloatingPointFormulaManager. It handles all the unwrapping and wrapping from and to the Formula instances, such that the concrete class needs to handle only its own internal types.

For multiply(FloatingPointFormula, FloatingPointFormula), and divide(FloatingPointFormula, FloatingPointFormula) this class even offers an implementation based on UFs. Subclasses are supposed to override them if they can implement these operations more precisely (for example multiplication with constants should be supported by all solvers and implemented by all subclasses).

Field Summary

Fields

Modifier and Type	Field	Description
protected final FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl>	formulaCreator

Constructor Summary

Constructors

Modifier	Constructor	Description
protected	AbstractFloatingPointFormulaManager(FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> pCreator)

Method Summary

Modifier and Type	Method	Description
FloatingPointFormula	abs(FloatingPointFormula pNumber)
protected abstract TFormulaInfo	abs(TFormulaInfo pParam1)
FloatingPointFormula	add(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2)
FloatingPointFormula	add(FloatingPointFormula number1, FloatingPointFormula number2, FloatingPointRoundingMode pFloatingPointRoundingMode)
protected abstract TFormulaInfo	add(TFormulaInfo pParam1, TFormulaInfo pParam2, TFormulaInfo pRoundingMode)
BooleanFormula	assignment(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2)	Create a term for assigning one floating-point term to another.
protected abstract TFormulaInfo	assignment(TFormulaInfo pParam1, TFormulaInfo pParam2)
FloatingPointFormula	castFrom(Formula pNumber, boolean pSigned, FormulaType.FloatingPointType pTargetType)	Build a FloatingPointFormula from another compatible formula.
FloatingPointFormula	castFrom(Formula number, boolean signed, FormulaType.FloatingPointType targetType, FloatingPointRoundingMode pFloatingPointRoundingMode)	Build a FloatingPointFormula from another compatible formula.
protected abstract TFormulaInfo	castFromImpl(TFormulaInfo pNumber, boolean pSigned, FormulaType.FloatingPointType pTargetType, TFormulaInfo pRoundingMode)
<T extends Formula> T	castTo(FloatingPointFormula pNumber, boolean pSigned, FormulaType<T> pTargetType)	Build a formula of compatible type from a FloatingPointFormula.
<T extends Formula> T	castTo(FloatingPointFormula number, boolean pSigned, FormulaType<T> targetType, FloatingPointRoundingMode pFloatingPointRoundingMode)	Build a formula of compatible type from a FloatingPointFormula.
protected abstract TFormulaInfo	castToImpl(TFormulaInfo pNumber, boolean pSigned, FormulaType<?> pTargetType, TFormulaInfo pRoundingMode)
FloatingPointFormula	divide(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2)
FloatingPointFormula	divide(FloatingPointFormula number1, FloatingPointFormula number2, FloatingPointRoundingMode pFloatingPointRoundingMode)
protected abstract TFormulaInfo	divide(TFormulaInfo pParam1, TFormulaInfo pParam2, TFormulaInfo pFloatingPointRoundingMode)
BooleanFormula	equalWithFPSemantics(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2)	Create a term for comparing the equality of two floating-point terms, according to standard floating-point semantics (i.e., NaN != NaN and 0.0 == -0.0).
protected abstract TFormulaInfo	equalWithFPSemantics(TFormulaInfo pParam1, TFormulaInfo pParam2)
protected final 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)
FloatingPointRoundingMode	fromRoundingModeFormula(FloatingPointRoundingModeFormula pRoundingModeFormula)	Converts a rounding mode formula to the corresponding enum value.
protected static String	getBvRepresentation(BigInteger integer, int size)
protected abstract TFormulaInfo	getDefaultRoundingMode()
protected final 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)
FloatingPointRoundingModeFormula	makeRoundingMode(FloatingPointRoundingMode pRoundingMode)	Creates a formula for the given floating point rounding mode.
FloatingPointFormula	makeVariable(String pVar, FormulaType.FloatingPointType pType)	Creates a variable with exactly the given name.
protected abstract TFormulaInfo	makeVariableImpl(String pVar, FormulaType.FloatingPointType pType)
FloatingPointFormula	max(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2)	Returns the maximum value of the two given floating-point numbers.
protected abstract TFormulaInfo	max(TFormulaInfo pParam1, TFormulaInfo pParam2)
FloatingPointFormula	min(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2)	Returns the minimum value of the two given floating-point numbers.
protected abstract TFormulaInfo	min(TFormulaInfo pParam1, TFormulaInfo pParam2)
FloatingPointFormula	multiply(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2)
FloatingPointFormula	multiply(FloatingPointFormula number1, FloatingPointFormula number2, FloatingPointRoundingMode pFloatingPointRoundingMode)
protected abstract TFormulaInfo	multiply(TFormulaInfo pParam1, TFormulaInfo pParam2, TFormulaInfo pFloatingPointRoundingMode)
FloatingPointFormula	negate(FloatingPointFormula pNumber)
protected abstract TFormulaInfo	negate(TFormulaInfo pParam1)
FloatingPointFormula	remainder(FloatingPointFormula number1, FloatingPointFormula number2)	remainder: x - y * n, where n in Z is nearest to x/y.
protected abstract TFormulaInfo	remainder(TFormulaInfo pParam1, TFormulaInfo pParam2)
FloatingPointFormula	round(FloatingPointFormula pFormula, FloatingPointRoundingMode pRoundingMode)
protected abstract TFormulaInfo	round(TFormulaInfo pFormula, FloatingPointRoundingMode pRoundingMode)
FloatingPointFormula	sqrt(FloatingPointFormula pNumber)
FloatingPointFormula	sqrt(FloatingPointFormula number, FloatingPointRoundingMode pFloatingPointRoundingMode)
protected abstract TFormulaInfo	sqrt(TFormulaInfo pNumber, TFormulaInfo pRoundingMode)
FloatingPointFormula	subtract(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2)
FloatingPointFormula	subtract(FloatingPointFormula number1, FloatingPointFormula number2, FloatingPointRoundingMode pFloatingPointRoundingMode)
protected abstract TFormulaInfo	subtract(TFormulaInfo pParam1, TFormulaInfo pParam2, TFormulaInfo pFloatingPointRoundingMode)
BitvectorFormula	toIeeeBitvector(FloatingPointFormula pNumber)	Create a formula that produces a representation of the given floating-point value as a bitvector conforming to the IEEE 754-2008 FP format.
protected abstract TFormulaInfo	toIeeeBitvectorImpl(TFormulaInfo pNumber)
protected final 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 Details

formulaCreator

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

Constructor Details

AbstractFloatingPointFormulaManager

protected AbstractFloatingPointFormulaManager(FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> pCreator)

Method Details

getDefaultRoundingMode

protected abstract TFormulaInfo getDefaultRoundingMode()

getRoundingModeImpl

protected abstract TFormulaInfo getRoundingModeImpl(FloatingPointRoundingMode pFloatingPointRoundingMode)

makeRoundingMode

public FloatingPointRoundingModeFormula makeRoundingMode(FloatingPointRoundingMode pRoundingMode)

Description copied from interface: FloatingPointFormulaManager

Creates a formula for the given floating point rounding mode.

Specified by:

makeRoundingMode in interface FloatingPointFormulaManager

fromRoundingModeFormula

public FloatingPointRoundingMode fromRoundingModeFormula(FloatingPointRoundingModeFormula pRoundingModeFormula)

Description copied from interface: FloatingPointFormulaManager

Converts a rounding mode formula to the corresponding enum value. This method is the inverse of FloatingPointFormulaManager.makeRoundingMode(FloatingPointRoundingMode).

Specified by:

fromRoundingModeFormula in interface FloatingPointFormulaManager

wrap

protected FloatingPointFormula wrap(TFormulaInfo pTerm)

makeNumber

public FloatingPointFormula makeNumber(Rational n,
 FormulaType.FloatingPointType type)

Description copied from interface: FloatingPointFormulaManager

Creates a floating point formula representing the given Rational value with the specified type.

Specified by:

makeNumber in interface FloatingPointFormulaManager

makeNumber

public FloatingPointFormula makeNumber(Rational n,
 FormulaType.FloatingPointType type,
 FloatingPointRoundingMode pFloatingPointRoundingMode)

Description copied from interface: FloatingPointFormulaManager

Creates a floating point formula representing the given Rational value with the specified type and rounding mode.

Specified by:

makeNumber in interface FloatingPointFormulaManager

makeNumber

public FloatingPointFormula makeNumber(double n,
 FormulaType.FloatingPointType type)

Description copied from interface: FloatingPointFormulaManager

Creates a floating point formula representing the given double value with the specified type.

Specified by:

makeNumber in interface FloatingPointFormulaManager

makeNumber

public FloatingPointFormula makeNumber(double n,
 FormulaType.FloatingPointType type,
 FloatingPointRoundingMode pFloatingPointRoundingMode)

Description copied from interface: FloatingPointFormulaManager

Creates a floating point formula representing the given double value with the specified type and rounding mode.

Specified by:

makeNumber in interface FloatingPointFormulaManager

makeNumberImpl

protected abstract TFormulaInfo makeNumberImpl(double n,
 FormulaType.FloatingPointType type,
 TFormulaInfo pFloatingPointRoundingMode)

makeNumber

public FloatingPointFormula makeNumber(BigDecimal n,
 FormulaType.FloatingPointType type)

Description copied from interface: FloatingPointFormulaManager

Creates a floating point formula representing the given BigDecimal value with the specified type.

Specified by:

makeNumber in interface FloatingPointFormulaManager

makeNumber

public FloatingPointFormula makeNumber(BigDecimal n,
 FormulaType.FloatingPointType type,
 FloatingPointRoundingMode pFloatingPointRoundingMode)

Description copied from interface: FloatingPointFormulaManager

Creates a floating point formula representing the given BigDecimal value with the specified type and rounding mode.

Specified by:

makeNumber in interface FloatingPointFormulaManager

makeNumberImpl

protected TFormulaInfo makeNumberImpl(BigDecimal n,
 FormulaType.FloatingPointType type,
 TFormulaInfo pFloatingPointRoundingMode)

makeNumber

public FloatingPointFormula makeNumber(String n,
 FormulaType.FloatingPointType type)

Description copied from interface: FloatingPointFormulaManager

Creates a floating point formula representing the given string value with the specified type.

The string can be any valid floating-point number, e.g., "1.0", "1.0e-3", but also special values like "NaN", "Infinity", or "-0.0", etc. A leading "+" sign or "-" sign is allowed.

Specified by:

makeNumber in interface FloatingPointFormulaManager

makeNumber

public FloatingPointFormula makeNumber(String n,
 FormulaType.FloatingPointType type,
 FloatingPointRoundingMode pFloatingPointRoundingMode)

Description copied from interface: FloatingPointFormulaManager

Creates a floating point formula representing the given string value with the specified type and rounding mode.

The string can be any valid floating-point number, e.g., "1.0", "1.0e-3", but also special values like "NaN", "Infinity", or "-0.0", etc. A leading "+" sign or "-" sign is allowed.

Specified by:

makeNumber in interface FloatingPointFormulaManager

makeNumberImpl

protected TFormulaInfo makeNumberImpl(String n,
 FormulaType.FloatingPointType type,
 TFormulaInfo pFloatingPointRoundingMode)

directly catch the most common special String constants.

makeNumber

public FloatingPointFormula makeNumber(BigInteger exponent,
 BigInteger mantissa,
 FloatingPointNumber.Sign sign,
 FormulaType.FloatingPointType type)

Description copied from interface: FloatingPointFormulaManager

Creates a floating point formula from the given exponent, mantissa, and sign with the specified type.

Specified by:

makeNumber in interface FloatingPointFormulaManager

Parameters:

exponent - the exponent part of the floating point number

mantissa - the mantissa part of the floating point number

sign - the sign of the floating point number

makeNumberImpl

protected abstract TFormulaInfo makeNumberImpl(BigInteger exponent,
 BigInteger mantissa,
 FloatingPointNumber.Sign sign,
 FormulaType.FloatingPointType type)

isNegativeZero

protected static boolean isNegativeZero(Double pN)

makeNumberAndRound

protected abstract TFormulaInfo makeNumberAndRound(String pN,
 FormulaType.FloatingPointType pType,
 TFormulaInfo pFloatingPointRoundingMode)

Parses the provided string and converts it into a floating-point formula.

The input string must represent a valid finite floating-point number. Values such as NaN, Infinity, or -Infinity are not allowed and should be handled before calling this method.

makeVariable

public FloatingPointFormula makeVariable(String pVar,
 FormulaType.FloatingPointType pType)

Description copied from interface: FloatingPointFormulaManager

Creates a variable with exactly the given name.

Please make sure that the given name is valid in SMT-LIB2. Take a look at FormulaManager.isValidName(java.lang.String) for further information.

This method does not quote or unquote the given name, but uses the plain name "AS IS". Formula.toString() can return a different String than the given one.

Specified by:

makeVariable in interface FloatingPointFormulaManager

makeVariableImpl

protected abstract TFormulaInfo makeVariableImpl(String pVar,
 FormulaType.FloatingPointType pType)

makePlusInfinity

public FloatingPointFormula makePlusInfinity(FormulaType.FloatingPointType pType)

Specified by:

makePlusInfinity in interface FloatingPointFormulaManager

makePlusInfinityImpl

protected abstract TFormulaInfo makePlusInfinityImpl(FormulaType.FloatingPointType pType)

makeMinusInfinity

public FloatingPointFormula makeMinusInfinity(FormulaType.FloatingPointType pType)

Specified by:

makeMinusInfinity in interface FloatingPointFormulaManager

makeMinusInfinityImpl

protected abstract TFormulaInfo makeMinusInfinityImpl(FormulaType.FloatingPointType pType)

makeNaN

public FloatingPointFormula makeNaN(FormulaType.FloatingPointType pType)

Specified by:

makeNaN in interface FloatingPointFormulaManager

makeNaNImpl

protected abstract TFormulaInfo makeNaNImpl(FormulaType.FloatingPointType pType)

castTo

public <T extends Formula> T castTo(FloatingPointFormula pNumber,
 boolean pSigned,
 FormulaType<T> pTargetType)

Description copied from interface: FloatingPointFormulaManager

Build a formula of compatible type from a FloatingPointFormula. This method uses the default rounding mode.

Compatible formula types are all numeral types and (signed/unsigned) bitvector types. It is also possible to cast a floating-point number into another floating-point type. We do not support casting from boolean or array types. We try to keep an exact representation, however fall back to rounding if needed.

Specified by:

castTo in interface FloatingPointFormulaManager

Parameters:

pNumber - the source formula of floating-point type

pSigned - if a BitvectorFormula is given as target, we additionally use this flag. Otherwise, we ignore it.

pTargetType - the type of the resulting formula

castTo

public <T extends Formula> T castTo(FloatingPointFormula number,
 boolean pSigned,
 FormulaType<T> targetType,
 FloatingPointRoundingMode pFloatingPointRoundingMode)

Description copied from interface: FloatingPointFormulaManager

Build a formula of compatible type from a FloatingPointFormula.

Compatible formula types are all numeral types and (signed/unsigned) bitvector types. It is also possible to cast a floating-point number into another floating-point type. We do not support casting from boolean or array types. We try to keep an exact representation, however fall back to rounding if needed.

Specified by:

castTo in interface FloatingPointFormulaManager

Parameters:

number - the source formula of floating-point type

pSigned - if a BitvectorFormula is given as target, we additionally use this flag. Otherwise, we ignore it.

targetType - the type of the resulting formula

pFloatingPointRoundingMode - if rounding is needed, we apply the rounding mode.

castToImpl

protected abstract TFormulaInfo castToImpl(TFormulaInfo pNumber,
 boolean pSigned,
 FormulaType<?> pTargetType,
 TFormulaInfo pRoundingMode)

castFrom

public FloatingPointFormula castFrom(Formula pNumber,
 boolean pSigned,
 FormulaType.FloatingPointType pTargetType)

Description copied from interface: FloatingPointFormulaManager

Build a FloatingPointFormula from another compatible formula. This method uses the default rounding mode.

Compatible formula types are all numeral types and (signed/unsigned) bitvector types. It is also possible to cast a floating-point number into another floating-point type. We do not support casting from boolean or array types. We try to keep an exact representation, however fall back to rounding if needed.

Specified by:

castFrom in interface FloatingPointFormulaManager

Parameters:

pNumber - the source formula of compatible type

pSigned - if a BitvectorFormula is given as source, we additionally use this flag. Otherwise, we ignore it.

pTargetType - the type of the resulting formula

castFrom

public FloatingPointFormula castFrom(Formula number,
 boolean signed,
 FormulaType.FloatingPointType targetType,
 FloatingPointRoundingMode pFloatingPointRoundingMode)

Description copied from interface: FloatingPointFormulaManager

Build a FloatingPointFormula from another compatible formula.

Compatible formula types are all numeral types and (signed/unsigned) bitvector types. It is also possible to cast a floating-point number into another floating-point type. We do not support casting from boolean or array types. We try to keep an exact representation, however fall back to rounding if needed.

Specified by:

castFrom in interface FloatingPointFormulaManager

Parameters:

number - the source formula of compatible type

signed - if a BitvectorFormula is given as source, we additionally use this flag. Otherwise, we ignore it.

targetType - the type of the resulting formula

pFloatingPointRoundingMode - if rounding is needed, we apply the rounding mode.

castFromImpl

protected abstract TFormulaInfo castFromImpl(TFormulaInfo pNumber,
 boolean pSigned,
 FormulaType.FloatingPointType pTargetType,
 TFormulaInfo pRoundingMode)

fromIeeeBitvector

public FloatingPointFormula fromIeeeBitvector(BitvectorFormula pNumber,
 FormulaType.FloatingPointType pTargetType)

Description copied from interface: FloatingPointFormulaManager

Create a formula that interprets the given bitvector as a floating-point value in the IEEE format, according to the given type. The sum of the sizes of exponent and mantissa (including the hidden bit) of the target type needs to be equal to the size of the bitvector.

Note: This method will return a value that is (numerically) far away from the original value. This method is completely different from FloatingPointFormulaManager.castFrom(org.sosy_lab.java_smt.api.Formula, boolean, org.sosy_lab.java_smt.api.FormulaType.FloatingPointType), which will produce a floating-point value close to the numeral value.

Specified by:

fromIeeeBitvector in interface FloatingPointFormulaManager

fromIeeeBitvectorImpl

protected abstract TFormulaInfo fromIeeeBitvectorImpl(TFormulaInfo pNumber,
 FormulaType.FloatingPointType pTargetType)

toIeeeBitvector

public BitvectorFormula toIeeeBitvector(FloatingPointFormula pNumber)

Description copied from interface: FloatingPointFormulaManager

Create a formula that produces a representation of the given floating-point value as a bitvector conforming to the IEEE 754-2008 FP format. The bit size of the resulting bitvector is equal to the total size of the FloatingPointNumbers precision.

Specified by:

toIeeeBitvector in interface FloatingPointFormulaManager

toIeeeBitvectorImpl

protected abstract TFormulaInfo toIeeeBitvectorImpl(TFormulaInfo pNumber)

negate

public FloatingPointFormula negate(FloatingPointFormula pNumber)

Specified by:

negate in interface FloatingPointFormulaManager

negate

protected abstract TFormulaInfo negate(TFormulaInfo pParam1)

abs

public FloatingPointFormula abs(FloatingPointFormula pNumber)

Specified by:

abs in interface FloatingPointFormulaManager

abs

protected abstract TFormulaInfo abs(TFormulaInfo pParam1)

max

public FloatingPointFormula max(FloatingPointFormula pNumber1,
 FloatingPointFormula pNumber2)

Description copied from interface: FloatingPointFormulaManager

Returns the maximum value of the two given floating-point numbers. If one of the numbers is NaN, the other number is returned.

Specified by:

max in interface FloatingPointFormulaManager

max

protected abstract TFormulaInfo max(TFormulaInfo pParam1,
 TFormulaInfo pParam2)

min

public FloatingPointFormula min(FloatingPointFormula pNumber1,
 FloatingPointFormula pNumber2)

Description copied from interface: FloatingPointFormulaManager

Returns the minimum value of the two given floating-point numbers. If one of the numbers is NaN, the other number is returned.

Specified by:

min in interface FloatingPointFormulaManager

min

protected abstract TFormulaInfo min(TFormulaInfo pParam1,
 TFormulaInfo pParam2)

sqrt

public FloatingPointFormula sqrt(FloatingPointFormula pNumber)

Specified by:

sqrt in interface FloatingPointFormulaManager

sqrt

public FloatingPointFormula sqrt(FloatingPointFormula number,
 FloatingPointRoundingMode pFloatingPointRoundingMode)

Specified by:

sqrt in interface FloatingPointFormulaManager

sqrt

protected abstract TFormulaInfo sqrt(TFormulaInfo pNumber,
 TFormulaInfo pRoundingMode)

add

public FloatingPointFormula add(FloatingPointFormula pNumber1,
 FloatingPointFormula pNumber2)

Specified by:

add in interface FloatingPointFormulaManager

add

public FloatingPointFormula add(FloatingPointFormula number1,
 FloatingPointFormula number2,
 FloatingPointRoundingMode pFloatingPointRoundingMode)

Specified by:

add in interface FloatingPointFormulaManager

add

protected abstract TFormulaInfo add(TFormulaInfo pParam1,
 TFormulaInfo pParam2,
 TFormulaInfo pRoundingMode)

subtract

public FloatingPointFormula subtract(FloatingPointFormula pNumber1,
 FloatingPointFormula pNumber2)

Specified by:

subtract in interface FloatingPointFormulaManager

subtract

public FloatingPointFormula subtract(FloatingPointFormula number1,
 FloatingPointFormula number2,
 FloatingPointRoundingMode pFloatingPointRoundingMode)

Specified by:

subtract in interface FloatingPointFormulaManager

subtract

protected abstract TFormulaInfo subtract(TFormulaInfo pParam1,
 TFormulaInfo pParam2,
 TFormulaInfo pFloatingPointRoundingMode)

divide

public FloatingPointFormula divide(FloatingPointFormula pNumber1,
 FloatingPointFormula pNumber2)

Specified by:

divide in interface FloatingPointFormulaManager

divide

public FloatingPointFormula divide(FloatingPointFormula number1,
 FloatingPointFormula number2,
 FloatingPointRoundingMode pFloatingPointRoundingMode)

Specified by:

divide in interface FloatingPointFormulaManager

divide

protected abstract TFormulaInfo divide(TFormulaInfo pParam1,
 TFormulaInfo pParam2,
 TFormulaInfo pFloatingPointRoundingMode)

multiply

public FloatingPointFormula multiply(FloatingPointFormula pNumber1,
 FloatingPointFormula pNumber2)

Specified by:

multiply in interface FloatingPointFormulaManager

multiply

public FloatingPointFormula multiply(FloatingPointFormula number1,
 FloatingPointFormula number2,
 FloatingPointRoundingMode pFloatingPointRoundingMode)

Specified by:

multiply in interface FloatingPointFormulaManager

multiply

protected abstract TFormulaInfo multiply(TFormulaInfo pParam1,
 TFormulaInfo pParam2,
 TFormulaInfo pFloatingPointRoundingMode)

remainder

public FloatingPointFormula remainder(FloatingPointFormula number1,
 FloatingPointFormula number2)

Description copied from interface: FloatingPointFormulaManager

remainder: x - y * n, where n in Z is nearest to x/y. The result can be negative even for two positive arguments, e.g. "rem(5, 4) == 1" and "rem(5, 6) == -1", as opposed to integer modulo operators.

Specified by:

remainder in interface FloatingPointFormulaManager

remainder

protected abstract TFormulaInfo remainder(TFormulaInfo pParam1,
 TFormulaInfo pParam2)

assignment

public BooleanFormula assignment(FloatingPointFormula pNumber1,
 FloatingPointFormula pNumber2)

Description copied from interface: FloatingPointFormulaManager

Create a term for assigning one floating-point term to another. This means both terms are considered equal afterward, based on their bit pattern (i.e., 0.0 != -0 .0 and NaN ==/!= NaN, depending on the bit pattern of each NaN). This method is the same as the method equal for other theories.

Specified by:

assignment in interface FloatingPointFormulaManager

assignment

protected abstract TFormulaInfo assignment(TFormulaInfo pParam1,
 TFormulaInfo pParam2)

equalWithFPSemantics

public BooleanFormula equalWithFPSemantics(FloatingPointFormula pNumber1,
 FloatingPointFormula pNumber2)

Description copied from interface: FloatingPointFormulaManager

Create a term for comparing the equality of two floating-point terms, according to standard floating-point semantics (i.e., NaN != NaN and 0.0 == -0.0). Be careful to not use this method when you really need FloatingPointFormulaManager.assignment(FloatingPointFormula, FloatingPointFormula).

Specified by:

equalWithFPSemantics in interface FloatingPointFormulaManager

equalWithFPSemantics

protected abstract TFormulaInfo equalWithFPSemantics(TFormulaInfo pParam1,
 TFormulaInfo pParam2)

greaterThan

public BooleanFormula greaterThan(FloatingPointFormula pNumber1,
 FloatingPointFormula pNumber2)

Description copied from interface: FloatingPointFormulaManager

Returns whether an FP number is greater than another FP number. If one of the numbers is NaN, the result is always false.

Specified by:

greaterThan in interface FloatingPointFormulaManager

greaterThan

protected abstract TFormulaInfo greaterThan(TFormulaInfo pParam1,
 TFormulaInfo pParam2)

greaterOrEquals

public BooleanFormula greaterOrEquals(FloatingPointFormula pNumber1,
 FloatingPointFormula pNumber2)

Description copied from interface: FloatingPointFormulaManager

Returns whether an FP number is greater or equal than another FP number. If one of the numbers is NaN, the result is always false.

Specified by:

greaterOrEquals in interface FloatingPointFormulaManager

greaterOrEquals

protected abstract TFormulaInfo greaterOrEquals(TFormulaInfo pParam1,
 TFormulaInfo pParam2)

lessThan

public BooleanFormula lessThan(FloatingPointFormula pNumber1,
 FloatingPointFormula pNumber2)

Description copied from interface: FloatingPointFormulaManager

Returns whether an FP number is less than another FP number. If one of the numbers is NaN, the result is always false.

Specified by:

lessThan in interface FloatingPointFormulaManager

lessThan

protected abstract TFormulaInfo lessThan(TFormulaInfo pParam1,
 TFormulaInfo pParam2)

lessOrEquals

public BooleanFormula lessOrEquals(FloatingPointFormula pNumber1,
 FloatingPointFormula pNumber2)

Description copied from interface: FloatingPointFormulaManager

Returns whether an FP number is less or equal than another FP number. If one of the numbers is NaN, the result is always false.

Specified by:

lessOrEquals in interface FloatingPointFormulaManager

lessOrEquals

protected abstract TFormulaInfo lessOrEquals(TFormulaInfo pParam1,
 TFormulaInfo pParam2)

isNaN

public BooleanFormula isNaN(FloatingPointFormula pNumber)

Description copied from interface: FloatingPointFormulaManager

Check whether a floating-point number is NaN.

The bit patterns for NaN in SMTLIB are identical to IEEE 754:

• sign=? (irrelevant for NaN)
• exponent=11...11 (all bits are 1)
• mantissa!=00...00 (mantissa is not all 0)

Specified by:

isNaN in interface FloatingPointFormulaManager

isNaN

protected abstract TFormulaInfo isNaN(TFormulaInfo pParam)

isInfinity

public BooleanFormula isInfinity(FloatingPointFormula pNumber)

Description copied from interface: FloatingPointFormulaManager

Checks whether a formula is positive or negative infinity.

The bit patterns for infinity in SMTLIB are identical to IEEE 754:

• sign=? (0 for +Inf, 1 for -Inf)
• exponent=11...11 (all bits are 1)
• mantissa=00...00 (all bits are 0)

Specified by:

isInfinity in interface FloatingPointFormulaManager

isInfinity

protected abstract TFormulaInfo isInfinity(TFormulaInfo pParam)

isZero

public BooleanFormula isZero(FloatingPointFormula pNumber)

Description copied from interface: FloatingPointFormulaManager

Checks whether a formula is positive or negative zero.

The bit patterns for zero in SMTLIB are identical to IEEE 754:

• sign=? (0 for +0, 1 for -0)
• exponent=00...00 (all bits are 0)
• mantissa=00...00 (all bits are 0)

Specified by:

isZero in interface FloatingPointFormulaManager

isZero

protected abstract TFormulaInfo isZero(TFormulaInfo pParam)

isSubnormal

public BooleanFormula isSubnormal(FloatingPointFormula pNumber)

Description copied from interface: FloatingPointFormulaManager

Checks whether a formula is subnormal FP number.

The bit patterns for subnormal FP numbers in SMTLIB are identical to IEEE 754:

• sign=? (0 for positive numbers, 1 for negative numbers)
• exponent=00...00 (exponent is all 0)
• mantissa!=00...00 (mantissa is not all 0)

Specified by:

isSubnormal in interface FloatingPointFormulaManager

isSubnormal

protected abstract TFormulaInfo isSubnormal(TFormulaInfo pParam)

isNormal

public BooleanFormula isNormal(FloatingPointFormula pNumber)

Description copied from interface: FloatingPointFormulaManager

Checks whether a formula is normal FP number.

The bit patterns for normal FP numbers in SMTLIB are identical to IEEE 754:

• sign=? (0 for positive numbers, 1 for negative numbers)
• exponent!=00...00 and exponent!=11...11 (exponent is not all 0 or all 1)
• mantissa=? (mantissa is irrelevant)

Specified by:

isNormal in interface FloatingPointFormulaManager

isNormal

protected abstract TFormulaInfo isNormal(TFormulaInfo pParam)

isNegative

public BooleanFormula isNegative(FloatingPointFormula pNumber)

Description copied from interface: FloatingPointFormulaManager

Checks whether a formula is negative, including -0.0.

The bit patterns for negative FP numbers in SMTLIB are identical to IEEE 754:

• sign=1 (1 for negative numbers)
• number is not NaN, i.e., exponent=11...11 implies mantissa=00...00

Specified by:

isNegative in interface FloatingPointFormulaManager

isNegative

protected abstract TFormulaInfo isNegative(TFormulaInfo pParam)

round

public FloatingPointFormula round(FloatingPointFormula pFormula,
 FloatingPointRoundingMode pRoundingMode)

Specified by:

round in interface FloatingPointFormulaManager

round

protected abstract TFormulaInfo round(TFormulaInfo pFormula,
 FloatingPointRoundingMode pRoundingMode)

getBvRepresentation

protected static String getBvRepresentation(BigInteger integer,
 int size)

getFormulaCreator

protected final FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> getFormulaCreator()

extractInfo

protected final TFormulaInfo extractInfo(Formula pBits)

toSolverType

protected final TType toSolverType(FormulaType<?> formulaType)