ksmt-core/io.ksmt.utils/BvUtils

BvUtils

object BvUtils

Functions

addMaxValueSigned

fun <T : KBvSort> KBitVecValue<T>.addMaxValueSigned(): KBitVecValue<T>

fun KBitVecValue<*>.bigIntValue(): BigInteger

fun <T : KBvSort> KBitVecValue<T>.bitwiseAnd(other: KBitVecValue<T>): KBitVecValue<T>

fun <T : KBvSort> KBitVecValue<T>.bitwiseNot(): KBitVecValue<T>

fun <T : KBvSort> KBitVecValue<T>.bitwiseOr(other: KBitVecValue<T>): KBitVecValue<T>

fun <T : KBvSort> KBitVecValue<T>.bitwiseXor(other: KBitVecValue<T>): KBitVecValue<T>

bvMaxValueSigned

fun <T : KBvSort> KContext.bvMaxValueSigned(size: UInt): KBitVecValue<T>

bvMaxValueUnsigned

fun <T : KBvSort> KContext.bvMaxValueUnsigned(size: UInt): KBitVecValue<T>

bvMinValueSigned

fun <T : KBvSort> KContext.bvMinValueSigned(size: UInt): KBitVecValue<T>

fun <T : KBvSort> KContext.bvOne(size: UInt): KBitVecValue<T>

fun <T : KBvSort> KContext.bvValue(size: UInt, value: Int): KBitVecValue<T>

fun KBitVecValue<*>.bvValueIs(value: Int): Boolean

fun <T : KBvSort> KContext.bvZero(size: UInt): KBitVecValue<T>

fun concatBv(lhs: KBitVecValue<*>, rhs: KBitVecValue<*>): KBitVecValue<*>

fun KBitVecValue<*>.extractBv(high: Int, low: Int): KBitVecValue<*>

fun KBitVecValue<*>.getBit(bit: UInt): Boolean

isBvMaxValueSigned

fun KBitVecValue<*>.isBvMaxValueSigned(): Boolean

isBvMaxValueUnsigned

fun KBitVecValue<*>.isBvMaxValueUnsigned(): Boolean

isBvMinValueSigned

fun KBitVecValue<*>.isBvMinValueSigned(): Boolean

fun KBitVecValue<*>.isBvOne(): Boolean

fun KBitVecValue<*>.isBvZero(): Boolean

operator fun <T : KBvSort> KBitVecValue<T>.minus(other: KBitVecValue<T>): KBitVecValue<T>

operator fun <T : KBvSort> KBitVecValue<T>.plus(other: KBitVecValue<T>): KBitVecValue<T>

powerOfTwoOrNull

fun KBitVecValue<*>.powerOfTwoOrNull(): Int?

fun <T : KBvSort> KBitVecValue<T>.shiftLeft(other: KBitVecValue<T>): KBitVecValue<T>

shiftRightArith

fun <T : KBvSort> KBitVecValue<T>.shiftRightArith(other: KBitVecValue<T>): KBitVecValue<T>

shiftRightLogical

fun <T : KBvSort> KBitVecValue<T>.shiftRightLogical(other: KBitVecValue<T>): KBitVecValue<T>

fun KBitVecValue<*>.signBit(): Boolean

fun <T : KBvSort> KBitVecValue<T>.signedDivide(other: KBitVecValue<T>): KBitVecValue<T>

fun KBitVecValue<*>.signedGreater(other: KBitVecValue<*>): Boolean

signedGreaterOrEqual

fun KBitVecValue<*>.signedGreaterOrEqual(other: KBitVecValue<*>): Boolean

fun KBitVecValue<*>.signedGreaterOrEqual(other: Int): Boolean

fun KBitVecValue<*>.signedLess(other: KBitVecValue<*>): Boolean

signedLessOrEqual

fun KBitVecValue<*>.signedLessOrEqual(other: KBitVecValue<*>): Boolean

fun <T : KBvSort> KBitVecValue<T>.signedMod(other: KBitVecValue<T>): KBitVecValue<T>

fun <T : KBvSort> KBitVecValue<T>.signedRem(other: KBitVecValue<T>): KBitVecValue<T>

fun KBitVecValue<*>.signExtension(extensionSize: UInt): KBitVecValue<*>

subMaxValueSigned

fun <T : KBvSort> KBitVecValue<T>.subMaxValueSigned(): KBitVecValue<T>

operator fun <T : KBvSort> KBitVecValue<T>.times(other: KBitVecValue<T>): KBitVecValue<T>

toBigIntegerSigned

fun KBitVecValue<*>.toBigIntegerSigned(): BigInteger

toBigIntegerUnsigned

fun KBitVecValue<*>.toBigIntegerUnsigned(): BigInteger

operator fun <T : KBvSort> KBitVecValue<T>.unaryMinus(): KBitVecValue<T>

fun <T : KBvSort> KBitVecValue<T>.unsignedDivide(other: KBitVecValue<T>): KBitVecValue<T>

unsignedGreater

fun KBitVecValue<*>.unsignedGreater(other: KBitVecValue<*>): Boolean

unsignedGreaterOrEqual

fun KBitVecValue<*>.unsignedGreaterOrEqual(other: KBitVecValue<*>): Boolean

fun KBitVecValue<*>.unsignedLess(other: KBitVecValue<*>): Boolean

unsignedLessOrEqual

fun KBitVecValue<*>.unsignedLessOrEqual(other: KBitVecValue<*>): Boolean

fun <T : KBvSort> KBitVecValue<T>.unsignedRem(other: KBitVecValue<T>): KBitVecValue<T>

fun KBitVecValue<*>.zeroExtension(extensionSize: UInt): KBitVecValue<*>