Fix custom bv values support (#149)

* Optimize bv values and support custom bv values

* Upgrade version to 0.5.16

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.15)
+[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.16)
 [![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.15")
+implementation("io.ksmt:ksmt-core:0.5.16")
 // z3 solver
-implementation("io.ksmt:ksmt-z3:0.5.15")
+implementation("io.ksmt:ksmt-z3:0.5.16")
 ```
 
 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.15"
+version = "0.5.16"
 
 repositories {
     mavenCentral()

docs/getting-started.md

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

examples/build.gradle.kts

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

ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt

@@ -493,24 +493,21 @@ open class KBitwuzlaExprInternalizer(val bitwuzlaCtx: KBitwuzlaContext) : KExprL
         transform { if (value) bitwuzlaCtx.trueTerm else bitwuzlaCtx.falseTerm }
     }
 
-    override fun transform(expr: KBitVec8Value): KExpr<KBv8Sort> = transformBv32Number(expr)
-    override fun transform(expr: KBitVec16Value): KExpr<KBv16Sort> = transformBv32Number(expr)
-    override fun transform(expr: KBitVec32Value): KExpr<KBv32Sort> = transformBv32Number(expr)
-    override fun transform(expr: KBitVec64Value): KExpr<KBv64Sort> = transformBv64Number(expr)
+    override fun transform(expr: KBitVec8Value): KExpr<KBv8Sort> = transformBv32Number(expr, expr.byteValue.toInt())
+    override fun transform(expr: KBitVec16Value): KExpr<KBv16Sort> = transformBv32Number(expr, expr.shortValue.toInt())
+    override fun transform(expr: KBitVec32Value): KExpr<KBv32Sort> = transformBv32Number(expr, expr.intValue)
+    override fun transform(expr: KBitVec64Value): KExpr<KBv64Sort> = transformBv64Number(expr, expr.longValue)
 
-    fun <T : KBitVecNumberValue<S, *>, S : KBvSort> transformBv32Number(expr: T): T = with(expr) {
+    fun <T : KBitVecNumberValue<S, *>, S : KBvSort> transformBv32Number(expr: T, value: Int): T = with(expr) {
         transform {
-            Native.bitwuzlaMkBvValueUint32(
-                bitwuzla,
-                sort.internalizeSort(),
-                numberValue.toInt()
-            ).also { bitwuzlaCtx.saveInternalizedValue(expr, it) }
+            Native.bitwuzlaMkBvValueUint32(bitwuzla, sort.internalizeSort(), value)
+                .also { bitwuzlaCtx.saveInternalizedValue(expr, it) }
         }
     }
 
-    fun <T : KBitVecNumberValue<S, *>, S : KBvSort> transformBv64Number(expr: T): T = with(expr) {
+    fun <T : KBitVecNumberValue<S, *>, S : KBvSort> transformBv64Number(expr: T, value: Long): T = with(expr) {
         transform {
-            transformBvLongNumber(numberValue.toLong(), sort.sizeBits.toInt())
+            transformBvLongNumber(value, sort.sizeBits.toInt())
                 .also { bitwuzlaCtx.saveInternalizedValue(expr, it) }
         }
     }

ksmt-core/src/main/kotlin/io/ksmt/expr/KBitVecExprs.kt

@@ -22,7 +22,7 @@ abstract class KBitVecValue<S : KBvSort>(ctx: KContext) : KInterpretedValue<S>(c
 
 class KBitVec1Value internal constructor(
     ctx: KContext,
-    val value: Boolean
+    @JvmField val value: Boolean
 ) : KBitVecValue<KBv1Sort>(ctx) {
     override fun accept(transformer: KTransformerBase): KExpr<KBv1Sort> = transformer.transform(this)
 
@@ -50,15 +50,15 @@ abstract class KBitVecNumberValue<S : KBvSort, N : Number>(ctx: KContext) : KBit
 
 class KBitVec8Value internal constructor(
     ctx: KContext,
-    val byteValue: Byte
+    @JvmField val byteValue: Byte
 ) : KBitVecNumberValue<KBv8Sort, Byte>(ctx) {
     override fun accept(transformer: KTransformerBase): KExpr<KBv8Sort> = transformer.transform(this)
 
     override val numberValue: Byte
         get() = byteValue
 
     override val decl: KDecl<KBv8Sort>
-        get() = ctx.mkBvDecl(numberValue)
+        get() = ctx.mkBvDecl(byteValue)
 
     override val sort: KBv8Sort = ctx.bv8Sort
 
@@ -68,15 +68,15 @@ class KBitVec8Value internal constructor(
 
 class KBitVec16Value internal constructor(
     ctx: KContext,
-    val shortValue: Short
+    @JvmField val shortValue: Short
 ) : KBitVecNumberValue<KBv16Sort, Short>(ctx) {
     override fun accept(transformer: KTransformerBase): KExpr<KBv16Sort> = transformer.transform(this)
 
     override val numberValue: Short
         get() = shortValue
 
     override val decl: KDecl<KBv16Sort>
-        get() = ctx.mkBvDecl(numberValue)
+        get() = ctx.mkBvDecl(shortValue)
 
     override val sort: KBv16Sort = ctx.bv16Sort
 
@@ -86,15 +86,15 @@ class KBitVec16Value internal constructor(
 
 class KBitVec32Value internal constructor(
     ctx: KContext,
-    val intValue: Int
+    @JvmField val intValue: Int
 ) : KBitVecNumberValue<KBv32Sort, Int>(ctx) {
     override fun accept(transformer: KTransformerBase): KExpr<KBv32Sort> = transformer.transform(this)
 
     override val numberValue: Int
         get() = intValue
 
     override val decl: KDecl<KBv32Sort>
-        get() = ctx.mkBvDecl(numberValue)
+        get() = ctx.mkBvDecl(intValue)
 
     override val sort: KBv32Sort = ctx.bv32Sort
 
@@ -104,15 +104,15 @@ class KBitVec32Value internal constructor(
 
 class KBitVec64Value internal constructor(
     ctx: KContext,
-    val longValue: Long
+    @JvmField val longValue: Long
 ) : KBitVecNumberValue<KBv64Sort, Long>(ctx) {
     override fun accept(transformer: KTransformerBase): KExpr<KBv64Sort> = transformer.transform(this)
 
     override val numberValue: Long
         get() = longValue
 
     override val decl: KDecl<KBv64Sort>
-        get() = ctx.mkBvDecl(numberValue)
+        get() = ctx.mkBvDecl(longValue)
 
     override val sort: KBv64Sort = ctx.bv64Sort