From fa2a997312627d7bc5afcaa3dfa1f1673221ce46 Mon Sep 17 00:00:00 2001 From: Valentyn Sobol Date: Mon, 5 Feb 2024 23:05:57 +0300 Subject: [PATCH] Faster bv creation (#152) * Faster Bv value creation * Upgrade version to 0.5.19 --- README.md | 6 ++--- .../main/kotlin/io.ksmt.ksmt-base.gradle.kts | 2 +- docs/getting-started.md | 6 ++--- examples/build.gradle.kts | 6 ++--- ksmt-core/src/main/kotlin/io/ksmt/KContext.kt | 27 ++++++++++++------- 5 files changed, 28 insertions(+), 19 deletions(-) diff --git a/README.md b/README.md index 5b5f6f0bb..186d7bb7d 100644 --- a/README.md +++ b/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 diff --git a/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts b/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts index a8a3bf688..708537b7a 100644 --- a/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts +++ b/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() diff --git a/docs/getting-started.md b/docs/getting-started.md index 68aac69b4..71fb1bf21 100644 --- a/docs/getting-started.md +++ b/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") } ``` diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts index 9f7c0e452..dfe2396ee 100644 --- a/examples/build.gradle.kts +++ b/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 { diff --git a/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt b/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt index c62a352ff..730e3903a 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt +++ b/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 { + 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 mkBv(value: Boolean, sort: T): KBitVecValue = - 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 = 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 = mkBv(value as Number, sizeBits) + fun mkBv(value: Byte, sizeBits: UInt): KBitVecValue = + 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 mkBv(value: Byte, sort: T): KBitVecValue = mkBv(value as Number, sort) + fun mkBv(value: Byte, sort: T): KBitVecValue = + if (sort == bv8Sort) mkBv(value).cast() else mkBv(value as Number, sort) fun Byte.toBv(): KBitVec8Value = mkBv(this) fun Byte.toBv(sizeBits: UInt): KBitVecValue = 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 = mkBv(value as Number, sizeBits) + fun mkBv(value: Short, sizeBits: UInt): KBitVecValue = + 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 mkBv(value: Short, sort: T): KBitVecValue = mkBv(value as Number, sort) + fun mkBv(value: Short, sort: T): KBitVecValue = + if (sort == bv16Sort) mkBv(value).cast() else mkBv(value as Number, sort) fun Short.toBv(): KBitVec16Value = mkBv(this) fun Short.toBv(sizeBits: UInt): KBitVecValue = 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 = mkBv(value as Number, sizeBits) + fun mkBv(value: Int, sizeBits: UInt): KBitVecValue = + 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 mkBv(value: Int, sort: T): KBitVecValue = mkBv(value as Number, sort) + fun mkBv(value: Int, sort: T): KBitVecValue = + if (sort == bv32Sort) mkBv(value).cast() else mkBv(value as Number, sort) fun Int.toBv(): KBitVec32Value = mkBv(this) fun Int.toBv(sizeBits: UInt): KBitVecValue = 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 = mkBv(value as Number, sizeBits) + fun mkBv(value: Long, sizeBits: UInt): KBitVecValue = + 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 mkBv(value: Long, sort: T): KBitVecValue = mkBv(value as Number, sort) + fun mkBv(value: Long, sort: T): KBitVecValue = + if (sort == bv64Sort) mkBv(value).cast() else mkBv(value as Number, sort) fun Long.toBv(): KBitVec64Value = mkBv(this) fun Long.toBv(sizeBits: UInt): KBitVecValue = mkBv(this, sizeBits)