From d941124b39a82f1603c328c22a75d602d7d2654f Mon Sep 17 00:00:00 2001 From: Valentyn Sobol Date: Wed, 10 Apr 2024 20:20:03 +0300 Subject: [PATCH] Open KContext to allow sort customization (#157) --- README.md | 6 +++--- buildSrc/src/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 | 6 +++--- ksmt-core/src/main/kotlin/io/ksmt/sort/KSort.kt | 6 +++--- 6 files changed, 16 insertions(+), 16 deletions(-) diff --git a/README.md b/README.md index 9301bc36d..757eb1bd6 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.21) +[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.22) [![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.21") +implementation("io.ksmt:ksmt-core:0.5.22") // z3 solver -implementation("io.ksmt:ksmt-z3:0.5.21") +implementation("io.ksmt:ksmt-z3:0.5.22") ``` 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 7af2f7dfc..1dc00e0dc 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.21" +version = "0.5.22" repositories { mavenCentral() diff --git a/docs/getting-started.md b/docs/getting-started.md index 30038280b..36c82ce11 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.21") + implementation("io.ksmt:ksmt-core:0.5.22") } ``` @@ -43,9 +43,9 @@ dependencies { ```kotlin dependencies { // z3 - implementation("io.ksmt:ksmt-z3:0.5.21") + implementation("io.ksmt:ksmt-z3:0.5.22") // bitwuzla - implementation("io.ksmt:ksmt-bitwuzla:0.5.21") + implementation("io.ksmt:ksmt-bitwuzla:0.5.22") } ``` diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts index 8dd92027b..d4006a210 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.21") + implementation("io.ksmt:ksmt-core:0.5.22") // z3 solver - implementation("io.ksmt:ksmt-z3:0.5.21") + implementation("io.ksmt:ksmt-z3:0.5.22") // Runner and portfolio solver - implementation("io.ksmt:ksmt-runner:0.5.21") + implementation("io.ksmt:ksmt-runner:0.5.22") } java { diff --git a/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt b/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt index 730e3903a..942764c23 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt @@ -627,7 +627,7 @@ open class KContext( /** * Create a BitVec sort with [sizeBits] bits length (_ BitVec [sizeBits]). * */ - fun mkBvSort(sizeBits: UInt): KBvSort = ensureContextActive { + open fun mkBvSort(sizeBits: UInt): KBvSort = ensureContextActive { when (sizeBits.toInt()) { 1 -> mkBv1Sort() Byte.SIZE_BITS -> mkBv8Sort() @@ -643,7 +643,7 @@ open class KContext( /** * Create an uninterpreted sort named [name]. * */ - fun mkUninterpretedSort(name: String): KUninterpretedSort = + open fun mkUninterpretedSort(name: String): KUninterpretedSort = ensureContextActive { KUninterpretedSort(name, this) } @@ -678,7 +678,7 @@ open class KContext( /** * Create an arbitrary precision IEEE floating point sort (_ FloatingPoint [exponentBits] [significandBits]). * */ - fun mkFpSort(exponentBits: UInt, significandBits: UInt): KFpSort = + open fun mkFpSort(exponentBits: UInt, significandBits: UInt): KFpSort = ensureContextActive { val eb = exponentBits val sb = significandBits diff --git a/ksmt-core/src/main/kotlin/io/ksmt/sort/KSort.kt b/ksmt-core/src/main/kotlin/io/ksmt/sort/KSort.kt index 4229acb16..75f00a0b4 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/sort/KSort.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/sort/KSort.kt @@ -189,11 +189,11 @@ class KBv64Sort internal constructor(ctx: KContext) : KBvSort(ctx) { override fun accept(visitor: KSortVisitor): T = visitor.visit(this) } -class KBvCustomSizeSort internal constructor(ctx: KContext, override val sizeBits: UInt) : KBvSort(ctx) { +open class KBvCustomSizeSort(ctx: KContext, override val sizeBits: UInt) : KBvSort(ctx) { override fun accept(visitor: KSortVisitor): T = visitor.visit(this) } -class KUninterpretedSort internal constructor(val name: String, ctx: KContext) : KSort(ctx) { +open class KUninterpretedSort(val name: String, ctx: KContext) : KSort(ctx) { override fun accept(visitor: KSortVisitor): T = visitor.visit(this) override fun print(builder: StringBuilder) { @@ -264,7 +264,7 @@ class KFp128Sort(ctx: KContext) : KFpSort(ctx, exponentBits, significandBits) { } } -class KFpCustomSizeSort( +open class KFpCustomSizeSort( ctx: KContext, exponentBits: UInt, significandBits: UInt