ksmt-core/io.ksmt.expr/KBitVecCustomValue

KBitVecCustomValue

class KBitVecCustomValue : KBitVecValue<KBvSort>

Functions

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

decl

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

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

ctx

val ctx: KContext

decl

open override val decl: KDecl<KBvSort>

sizeBits

val sizeBits: UInt

sort

open override val sort: KBvSort

stringValue

open override val stringValue: String

value

val value: BigInteger

Extensions

addMaxValueSigned

@JvmStatic

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

asExpr

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

bigIntValue

@JvmStatic

fun KBitVecValue<*>.bigIntValue(): BigInteger

bitwiseAnd

@JvmStatic

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

bitwiseNot

@JvmStatic

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

bitwiseOr

@JvmStatic

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

bitwiseXor

@JvmStatic

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

bvValueIs

@JvmStatic

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

extractBv

@JvmStatic

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

getBit

@JvmStatic

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

isBvMaxValueSigned

@JvmStatic

fun KBitVecValue<*>.isBvMaxValueSigned(): Boolean

isBvMaxValueUnsigned

@JvmStatic

fun KBitVecValue<*>.isBvMaxValueUnsigned(): Boolean

isBvMinValueSigned

@JvmStatic

fun KBitVecValue<*>.isBvMinValueSigned(): Boolean

isBvOne

@JvmStatic

fun KBitVecValue<*>.isBvOne(): Boolean

isBvZero

@JvmStatic

fun KBitVecValue<*>.isBvZero(): Boolean

isComplement

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

isMaxValue

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

isMinValue

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

minus

@JvmStatic

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

plus

@JvmStatic

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

powerOfTwoOrNull

@JvmStatic

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

shiftLeft

@JvmStatic

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

shiftRightArith

@JvmStatic

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

shiftRightLogical

@JvmStatic

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

signBit

@JvmStatic

fun KBitVecValue<*>.signBit(): Boolean

signedDivide

@JvmStatic

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

signedGreater

@JvmStatic

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

signedGreaterOrEqual

@JvmStatic

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

@JvmStatic

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

signedLess

@JvmStatic

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

signedLessOrEqual

@JvmStatic

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

signedMod

@JvmStatic

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

signedRem

@JvmStatic

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

signExtension

@JvmStatic

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

subMaxValueSigned

@JvmStatic

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

times

@JvmStatic

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

toBigIntegerSigned

@JvmStatic

fun KBitVecValue<*>.toBigIntegerSigned(): BigInteger

toBigIntegerUnsigned

@JvmStatic

fun KBitVecValue<*>.toBigIntegerUnsigned(): BigInteger

toRealValue

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

unaryMinus

@JvmStatic

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

unsignedDivide

@JvmStatic

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

unsignedGreater

@JvmStatic

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

unsignedGreaterOrEqual

@JvmStatic

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

unsignedLess

@JvmStatic

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

unsignedLessOrEqual

@JvmStatic

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

unsignedRem

@JvmStatic

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

zeroExtension

@JvmStatic

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