ksmt-core/io.ksmt.expr/KBitVecValue

KBitVecValue

abstract class KBitVecValue<S : KBvSort>(ctx: KContext) : KInterpretedValue<S>

Constructors

fun KBitVecValue(ctx: KContext)

Functions

abstract fun accept(transformer: KTransformerBase): KExpr<S>

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

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

open override fun hashCode(): Int

open override fun internEquals(other: Any): Boolean

Any.equals analogue for interning purposes.

open override fun internHashCode(): Int

Any.hashCode analogue for interning purposes.

open override fun print(printer: ExpressionPrinter)

open override fun print(builder: StringBuilder)

open override fun toString(): String

Properties

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

val ctx: KContext

abstract val decl: KDecl<S>

abstract val sort: S

abstract val stringValue: String

Inheritors

KBitVecNumberValue

KBitVecCustomValue

Extensions

addMaxValueSigned

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

fun <T : KSort> KExpr<*>.asExpr(sort: T): KExpr<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>

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

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

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

fun KBitVecValue<*>.isMaxValue(signed: Boolean): Boolean

fun KBitVecValue<*>.isMinValue(signed: Boolean): 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: Int): Boolean

fun KBitVecValue<*>.signedGreaterOrEqual(other: KBitVecValue<*>): 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

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

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<*>