ksmt-core/io.ksmt.utils/FpUtils

FpUtils

object FpUtils

Functions

fun biasFpExponent(exponent: KBitVecValue<*>, exponentSize: UInt): KBitVecValue<*>

fun fpAdd(rm: KFpRoundingMode, lhs: KFpValue<*>, rhs: KFpValue<*>): KFpValue<*>

fpBvValueOrNull

fun <T : KBvSort> fpBvValueOrNull(value: KFpValue<*>, rm: KFpRoundingMode, bvSort: T, signed: Boolean): KBitVecValue<T>?

fun fpDiv(rm: KFpRoundingMode, lhs: KFpValue<*>, rhs: KFpValue<*>): KFpValue<*>

fun fpEq(lhs: KFpValue<*>, rhs: KFpValue<*>): Boolean

fun fpFma(rm: KFpRoundingMode, x: KFpValue<*>, y: KFpValue<*>, z: KFpValue<*>): KFpValue<*>

fun fpGeq(lhs: KFpValue<*>, rhs: KFpValue<*>): Boolean

fun fpGt(lhs: KFpValue<*>, rhs: KFpValue<*>): Boolean

fpInfExponentBiased

fun KContext.fpInfExponentBiased(sort: KFpSort): KBitVecValue<KBvSort>

fpInfSignificand

fun KContext.fpInfSignificand(sort: KFpSort): KBitVecValue<KBvSort>

fun fpLeq(lhs: KFpValue<*>, rhs: KFpValue<*>): Boolean

fun fpLt(lhs: KFpValue<*>, rhs: KFpValue<*>): Boolean

fun fpMax(lhs: KFpValue<*>, rhs: KFpValue<*>): KFpValue<*>

fun fpMin(lhs: KFpValue<*>, rhs: KFpValue<*>): KFpValue<*>

fun fpMul(rm: KFpRoundingMode, lhs: KFpValue<*>, rhs: KFpValue<*>): KFpValue<*>

fpNaNExponentBiased

fun KContext.fpNaNExponentBiased(sort: KFpSort): KBitVecValue<KBvSort>

fpNaNSignificand

fun KContext.fpNaNSignificand(sort: KFpSort): KBitVecValue<KBvSort>

fun fpNegate(expr: KFpValue<*>): KFpValue<*>

fpRealValueOrNull

fun fpRealValueOrNull(value: KFpValue<*>): KRealNumExpr?

fun fpRem(lhs: KFpValue<*>, rhs: KFpValue<*>): KFpValue<*>

fpRoundToIntegral

fun fpRoundToIntegral(rm: KFpRoundingMode, value: KFpValue<*>): KFpValue<*>

fun fpSqrt(rm: KFpRoundingMode, value: KFpValue<*>): KFpValue<*>

fpStructurallyEqual

fun fpStructurallyEqual(lhs: KFpValue<*>, rhs: KFpValue<*>): Boolean

fun <T : KFpSort> fpToFp(rm: KFpRoundingMode, value: KFpValue<*>, toFpSort: T): KFpValue<T>

fun <T : KFpSort> fpValueFromBv(rm: KFpRoundingMode, value: KBitVecValue<*>, signed: Boolean, sort: T): KFpValue<T>

fpValueFromReal

fun <T : KFpSort> fpValueFromReal(rm: KFpRoundingMode, value: KRealNumExpr, sort: T): KFpValue<T>

fpZeroExponentBiased

fun KContext.fpZeroExponentBiased(sort: KFpSort): KBitVecValue<KBvSort>

fpZeroSignificand

fun KContext.fpZeroSignificand(sort: KFpSort): KBitVecValue<KBvSort>

fun KFpValue<*>.isInfinity(): Boolean

fun KFpValue<*>.isNaN(): Boolean

fun KFpValue<*>.isNegative(): Boolean

fun KFpValue<*>.isNormal(): Boolean

fun KFpValue<*>.isPositive(): Boolean

fun KFpValue<*>.isSubnormal(): Boolean

fun KFpValue<*>.isZero(): Boolean

fun <T : KFpSort> KContext.mkFpMaxValue(sort: T, signBit: Boolean): KFpValue<T>

fun <T : KFpSort> KContext.mkFpOne(sort: T, signBit: Boolean): KFpValue<T>

unbiasFpExponent

fun unbiasFpExponent(exponent: KBitVecValue<*>, exponentSize: UInt): KBitVecValue<*>