ksmt-core/io.ksmt/KContext/mkBv

mkBv

fun mkBv(value: Boolean): KBitVec1Value

Create a BitVec value with 1 bit length.

fun mkBv(value: Boolean, sizeBits: UInt): KBitVecValue<KBvSort>

Create a BitVec value with sizeBits bit length.

Note: if sizeBits is greater than 1, the value bit will be repeated.

fun <T : KBvSort> mkBv(value: Boolean, sort: T): KBitVecValue<T>

Create a BitVec value of the BitVec sort.

Note: if sort size is greater than 1, the value bit will be repeated.

fun mkBv(value: Byte): KBitVec8Value

Create a BitVec value with 8 bit length.

fun mkBv(value: Byte, sizeBits: UInt): KBitVecValue<KBvSort>

Create a BitVec value with sizeBits bit length.

Note: if sizeBits is less than 8, the last sizeBits bits of the value will be taken.

At the same time, if sizeBits is greater than 8, binary representation of the value will be padded from the start with its sign bit.

fun <T : KBvSort> mkBv(value: Byte, sort: T): KBitVecValue<T>

Create a BitVec value of the BitVec sort.

Note: if sort size is less than 8, the last sort size bits of the value will be taken.

At the same time, if sort size is greater than 8, binary representation of the value will be padded from the start with its sign bit.

fun mkBv(value: Short): KBitVec16Value

Create a BitVec value with 16 bit length.

fun mkBv(value: Short, sizeBits: UInt): KBitVecValue<KBvSort>

Create a BitVec value with sizeBits bit length.

Note: if sizeBits is less than 16, the last sizeBits bits of the value will be taken.

At the same time, if sizeBits is greater than 16, binary representation of the value will be padded from the start with its sign bit.

fun <T : KBvSort> mkBv(value: Short, sort: T): KBitVecValue<T>

Create a BitVec value of the BitVec sort.

Note: if sort size is less than 16, the last sort size bits of the value will be taken.

At the same time, if sort size is greater than 16, binary representation of the value will be padded from the start with its sign bit.

fun mkBv(value: Int): KBitVec32Value

Create a BitVec value with 32 bit length.

fun mkBv(value: Int, sizeBits: UInt): KBitVecValue<KBvSort>

Create a BitVec value with sizeBits bit length.

Note: if sizeBits is less than 32, the last sizeBits bits of the value will be taken.

At the same time, if sizeBits is greater than 32, binary representation of the value will be padded from the start with its sign bit.

fun <T : KBvSort> mkBv(value: Int, sort: T): KBitVecValue<T>

Create a BitVec value of the BitVec sort.

Note: if sort size is less than 32, the last sort size bits of the value will be taken.

At the same time, if sort size is greater than 32, binary representation of the value will be padded from the start with its sign bit.

fun mkBv(value: Long): KBitVec64Value

Create a BitVec value with 64 bit length.

fun mkBv(value: Long, sizeBits: UInt): KBitVecValue<KBvSort>

Create a BitVec value with sizeBits bit length.

Note: if sizeBits is less than 64, the last sizeBits bits of the value will be taken.

At the same time, if sizeBits is greater than 64, binary representation of the value will be padded from the start with its sign bit.

fun <T : KBvSort> mkBv(value: Long, sort: T): KBitVecValue<T>

Create a BitVec value of the BitVec sort.

Note: if sort size is less than 64, the last sort size bits of the value will be taken.

At the same time, if sort size is greater than 64, binary representation of the value will be padded from the start with its sign bit.

fun mkBv(value: BigInteger, sizeBits: UInt): KBitVecValue<KBvSort>

Create a BitVec value with sizeBits bit length.

fun <T : KBvSort> mkBv(value: BigInteger, sort: T): KBitVecValue<T>

Create a BitVec value of the BitVec sort.

fun mkBv(value: String, sizeBits: UInt): KBitVecValue<KBvSort>

Create a BitVec value with sizeBits bit length from the given binary string value.