ksmt-core/io.ksmt.expr/KFp16Value

KFp16Value

Fp16 value. Note that value should has biased Fp32 exponent, but a constructed Fp16 will have an unbiased one.

Fp32 to Fp16 transformation: sign exponent significand 0 00000000 00000000000000000000000 (1 8 23) x x___xxxx xxxxxxxxxx_____________ (1 5 10)

Functions

open override fun accept(transformer: KTransformerBase): KExpr<KFp16Sort>

decl

fun ~~decl~~(): KDecl<KFp16Sort>

equals

open operator override fun equals(other: Any?): Boolean

hashCode

open override fun hashCode(): Int

internEquals

open override fun internEquals(other: Any): Boolean

Any.equals analogue for interning purposes.

internHashCode

open override fun internHashCode(): Int

Any.hashCode analogue for interning purposes.

open override fun print(printer: ExpressionPrinter)

open override fun print(builder: StringBuilder)

toString

open override fun toString(): String

Properties

args

open override val args: List<KExpr<KSort>>

biasedExponent

open override val biasedExponent: KBitVecValue<KBvSort>

ctx

val ctx: KContext

decl

open override val decl: KDecl<KFp16Sort>

signBit

open override val signBit: Boolean

significand

open override val significand: KBitVecValue<KBvSort>

sort

open override val sort: KFp16Sort

value

val value: Float

Extensions

asExpr

fun <T : KSort> KExpr<*>.asExpr(sort: T): KExpr<T>

isComplement

fun KExpr<KBoolSort>.isComplement(other: KExpr<KBoolSort>): Boolean

isInfinity

fun KFpValue<*>.isInfinity(): Boolean

isNaN

fun KFpValue<*>.isNaN(): Boolean

isNegative

fun KFpValue<*>.isNegative(): Boolean

isNormal

fun KFpValue<*>.isNormal(): Boolean

isPositive

fun KFpValue<*>.isPositive(): Boolean

isSubnormal

fun KFpValue<*>.isSubnormal(): Boolean

isZero

fun KFpValue<*>.isZero(): Boolean

toRealValue

fun <T : KArithSort> KExpr<T>.toRealValue(): ArithUtils.RealValue?