Faster bv creation (#152)

* Faster Bv value creation

* Upgrade version to 0.5.19

README.md

@@ -11,7 +11,7 @@ Get the most out of SMT solving with KSMT features:
 * Streamlined [solver delivery](#ksmt-distribution) with no need for building a solver or implementing JVM bindings
 
 [![KSMT: build](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml/badge.svg)](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml)
-[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.18)
+[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.19)
 [![javadoc](https://javadoc.io/badge2/io.ksmt/ksmt-core/javadoc.svg)](https://javadoc.io/doc/io.ksmt/ksmt-core)
 
 ## Get started
@@ -20,9 +20,9 @@ To start using KSMT, install it via [Gradle](https://gradle.org/):
 
 ```kotlin
 // core 
-implementation("io.ksmt:ksmt-core:0.5.18")
+implementation("io.ksmt:ksmt-core:0.5.19")
 // z3 solver
-implementation("io.ksmt:ksmt-z3:0.5.18")
+implementation("io.ksmt:ksmt-z3:0.5.19")
 ```
 
 Find basic instructions in the [Getting started](docs/getting-started.md) guide and try it out with the 

buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts

@@ -11,7 +11,7 @@ plugins {
 }
 
 group = "io.ksmt"
-version = "0.5.18"
+version = "0.5.19"
 
 repositories {
     mavenCentral()

docs/getting-started.md

@@ -34,7 +34,7 @@ repositories {
 ```kotlin
 dependencies {
     // core 
-    implementation("io.ksmt:ksmt-core:0.5.18")    
+    implementation("io.ksmt:ksmt-core:0.5.19")    
 }
 ```
 
@@ -43,9 +43,9 @@ dependencies {
 ```kotlin
 dependencies {
     // z3 
-    implementation("io.ksmt:ksmt-z3:0.5.18")
+    implementation("io.ksmt:ksmt-z3:0.5.19")
     // bitwuzla
-    implementation("io.ksmt:ksmt-bitwuzla:0.5.18")
+    implementation("io.ksmt:ksmt-bitwuzla:0.5.19")
 }
 ```
 

examples/build.gradle.kts

@@ -9,11 +9,11 @@ repositories {
 
 dependencies {
     // core
-    implementation("io.ksmt:ksmt-core:0.5.18")
+    implementation("io.ksmt:ksmt-core:0.5.19")
     // z3 solver
-    implementation("io.ksmt:ksmt-z3:0.5.18")
+    implementation("io.ksmt:ksmt-z3:0.5.19")
     // Runner and portfolio solver
-    implementation("io.ksmt:ksmt-runner:0.5.18")
+    implementation("io.ksmt:ksmt-runner:0.5.19")
 }
 
 java {

ksmt-core/src/main/kotlin/io/ksmt/KContext.kt

@@ -1884,6 +1884,7 @@ open class KContext(
      * Note: if [sizeBits] is greater than 1, the [value] bit will be repeated.
      * */
     fun mkBv(value: Boolean, sizeBits: UInt): KBitVecValue<KBvSort> {
+        if (sizeBits == bv1Sort.sizeBits) return mkBv(value).cast()
         val intValue = (if (value) 1 else 0) as Number
         return mkBv(intValue, sizeBits)
     }
@@ -1894,7 +1895,7 @@ open class KContext(
      * Note: if [sort] size is greater than 1, the [value] bit will be repeated.
      * */
     fun <T : KBvSort> mkBv(value: Boolean, sort: T): KBitVecValue<T> =
-        mkBv(value, sort.sizeBits).cast()
+        if (sort == bv1Sort) mkBv(value).cast() else mkBv(value, sort.sizeBits).cast()
 
     fun Boolean.toBv(): KBitVec1Value = mkBv(this)
     fun Boolean.toBv(sizeBits: UInt): KBitVecValue<KBvSort> = mkBv(this, sizeBits)
@@ -1914,7 +1915,8 @@ open class KContext(
      * 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 mkBv(value: Byte, sizeBits: UInt): KBitVecValue<KBvSort> = mkBv(value as Number, sizeBits)
+    fun mkBv(value: Byte, sizeBits: UInt): KBitVecValue<KBvSort> =
+        if (sizeBits == bv8Sort.sizeBits) mkBv(value).cast() else mkBv(value as Number, sizeBits)
 
     /**
      * Create a BitVec value of the BitVec [sort].
@@ -1925,7 +1927,8 @@ open class KContext(
      * 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 <T : KBvSort> mkBv(value: Byte, sort: T): KBitVecValue<T> = mkBv(value as Number, sort)
+    fun <T : KBvSort> mkBv(value: Byte, sort: T): KBitVecValue<T> =
+        if (sort == bv8Sort) mkBv(value).cast() else mkBv(value as Number, sort)
 
     fun Byte.toBv(): KBitVec8Value = mkBv(this)
     fun Byte.toBv(sizeBits: UInt): KBitVecValue<KBvSort> = mkBv(this, sizeBits)
@@ -1946,7 +1949,8 @@ open class KContext(
      * 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 mkBv(value: Short, sizeBits: UInt): KBitVecValue<KBvSort> = mkBv(value as Number, sizeBits)
+    fun mkBv(value: Short, sizeBits: UInt): KBitVecValue<KBvSort> =
+        if (sizeBits == bv16Sort.sizeBits) mkBv(value).cast() else mkBv(value as Number, sizeBits)
 
     /**
      * Create a BitVec value of the BitVec [sort].
@@ -1957,7 +1961,8 @@ open class KContext(
      * 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 <T : KBvSort> mkBv(value: Short, sort: T): KBitVecValue<T> = mkBv(value as Number, sort)
+    fun <T : KBvSort> mkBv(value: Short, sort: T): KBitVecValue<T>  =
+        if (sort == bv16Sort) mkBv(value).cast() else mkBv(value as Number, sort)
 
     fun Short.toBv(): KBitVec16Value = mkBv(this)
     fun Short.toBv(sizeBits: UInt): KBitVecValue<KBvSort> = mkBv(this, sizeBits)
@@ -1978,7 +1983,8 @@ open class KContext(
      * 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 mkBv(value: Int, sizeBits: UInt): KBitVecValue<KBvSort> = mkBv(value as Number, sizeBits)
+    fun mkBv(value: Int, sizeBits: UInt): KBitVecValue<KBvSort> =
+        if (sizeBits == bv32Sort.sizeBits) mkBv(value).cast() else mkBv(value as Number, sizeBits)
 
     /**
      * Create a BitVec value of the BitVec [sort].
@@ -1989,7 +1995,8 @@ open class KContext(
      * 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 <T : KBvSort> mkBv(value: Int, sort: T): KBitVecValue<T> = mkBv(value as Number, sort)
+    fun <T : KBvSort> mkBv(value: Int, sort: T): KBitVecValue<T> =
+        if (sort == bv32Sort) mkBv(value).cast() else mkBv(value as Number, sort)
 
     fun Int.toBv(): KBitVec32Value = mkBv(this)
     fun Int.toBv(sizeBits: UInt): KBitVecValue<KBvSort> = mkBv(this, sizeBits)
@@ -2010,7 +2017,8 @@ open class KContext(
      * 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 mkBv(value: Long, sizeBits: UInt): KBitVecValue<KBvSort> = mkBv(value as Number, sizeBits)
+    fun mkBv(value: Long, sizeBits: UInt): KBitVecValue<KBvSort> =
+        if (sizeBits == bv64Sort.sizeBits) mkBv(value).cast() else mkBv(value as Number, sizeBits)
 
     /**
      * Create a BitVec value of the BitVec [sort].
@@ -2021,7 +2029,8 @@ open class KContext(
      * 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 <T : KBvSort> mkBv(value: Long, sort: T): KBitVecValue<T> = mkBv(value as Number, sort)
+    fun <T : KBvSort> mkBv(value: Long, sort: T): KBitVecValue<T> =
+        if (sort == bv64Sort) mkBv(value).cast() else mkBv(value as Number, sort)
 
     fun Long.toBv(): KBitVec64Value = mkBv(this)
     fun Long.toBv(sizeBits: UInt): KBitVecValue<KBvSort> = mkBv(this, sizeBits)