ksmt-core/io.ksmt.expr/KBv2IntExpr

KBv2IntExpr

class KBv2IntExpr : KApp<KIntSort, KBvSort>

Creates an integer from the bit-vector argument value.

If isSigned is false, then the bit-vector value is treated as unsigned. So the reuslt is non-negative and in the range [0..2^(n - 1)], where N are the number of bits in value.

If isSigned is true, then value is treated as a signed bit-vector.

Functions

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

decl

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

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

ctx

val ctx: KContext

decl

open override val decl: KDecl<KIntSort>

isSigned

val isSigned: Boolean

sort

open override val sort: KIntSort

value

val value: KExpr<KBvSort>

Extensions

asExpr

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

isComplement

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

toRealValue

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