Open KContext to allow sort customization (#157)

UnitTestBot · Apr 10, 2024 · d941124 · d941124
1 parent b0cff63
commit d941124
Show file tree

Hide file tree

Showing 6 changed files with 16 additions and 16 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -189,11 +189,11 @@ class KBv64Sort internal constructor(ctx: KContext) : KBvSort(ctx) {
     override fun <T> accept(visitor: KSortVisitor<T>): 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 <T> accept(visitor: KSortVisitor<T>): 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 <T> accept(visitor: KSortVisitor<T>): 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