ksmt-core/io.ksmt.utils

Package-level declarations

Types

ArithUtils

object ArithUtils

BvUtils

object BvUtils

DefaultValueSampler

open class DefaultValueSampler(val ctx: KContext) : KSortVisitor<KExpr<*>>

FpUtils

object FpUtils

Functions

asExpr

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

cast

inline fun <T : Base, Base> Base.cast(): T

extendWithLeadingZeros

fun Int.extendWithLeadingZeros(): Long

Extends the given 32-bits value to a new 64-bits one with zeroes.

extractExponent

fun Double.extractExponent(sort: KFpSort, isBiased: Boolean): Long

Extracts an exponent of the specific sort from the fp64 value.

fun Float.extractExponent(sort: KFpSort, isBiased: Boolean): Int

Extracts an exponent of the specific sort from the fp32 value.

extractSignificand

fun Double.extractSignificand(sort: KFpSort): Long

Extracts a significand of the specific sort from a double value.

fun Float.extractSignificand(sort: KFpSort): Int

Extracts a significand of the specific sort from a float value.

getExponent

fun Double.getExponent(isBiased: Boolean): Long

fun Float.getExponent(isBiased: Boolean): Int

Extracts an exponent from the float value. Depending on the isBiased it can be either biased or not.

getHalfPrecisionExponent

fun Float.getHalfPrecisionExponent(isBiased: Boolean): Int

Take an exponent from the float value. Depending on the isBiased is can be either shifted by KFp16Sort.exponentShiftSize or not.

getValue

inline operator fun <T : KSort> T.getValue(thisRef: Any?, property: KProperty<*>): KApp<T, *>

mkConst

fun <T : KSort> T.mkConst(name: String): KApp<T, *>

mkConstDecl

fun <T : KSort> T.mkConstDecl(name: String): KUninterpretedConstDecl<T>

mkFreshConst

fun <T : KSort> T.mkFreshConst(name: String): KApp<T, *>

mkFreshConstDecl

fun <T : KSort> T.mkFreshConstDecl(name: String): KConstDecl<T>

normalizeValue

fun BigInteger.normalizeValue(size: UInt): BigInteger

Ensure that BigInteger value is suitable for representation of Bv with size bits.

powerOfTwo

fun powerOfTwo(power: UInt): BigInteger

sampleValue

fun <T : KSort> T.sampleValue(): KExpr<T>

toBigInteger

fun Number.toBigInteger(): BigInteger

fun String.toBigInteger(radix: Int): BigInteger

toBinary

fun Number.toBinary(): String

fun BigInteger.toBinary(size: UInt): String

toULongValue

fun Number.toULongValue(): ULong

toUnsignedBigInteger

fun Number.toUnsignedBigInteger(): BigInteger

uncheckedCast

inline fun <Base, T> Base.uncheckedCast(): T

Properties

booleanSignBit

val Float.booleanSignBit: Boolean

val Double.booleanSignBit: Boolean

halfPrecisionSignificand

val Float.halfPrecisionSignificand: Int

Significand for Fp16 takes 10 bits from the float value: from 14 to 23 bits

signBit

val Float.signBit: Int

val Double.signBit: Int

significand

val Float.significand: Int

Extracts a significand from the float value.

val Double.significand: Long

Extracts a significand from the float value.