From becbf8824ea86fb1b3c37c70b1440b2660c7f755 Mon Sep 17 00:00:00 2001 From: Valentyn Sobol Date: Wed, 8 Oct 2025 13:56:12 +0300 Subject: [PATCH 1/2] Transformer cache extension points --- .../expr/transformer/KNonRecursiveTransformerBase.kt | 9 ++++++++- .../io/ksmt/expr/transformer/KNonRecursiveVisitorBase.kt | 7 ++++++- 2 files changed, 14 insertions(+), 2 deletions(-) diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveTransformerBase.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveTransformerBase.kt index feaf36820..a8c696f98 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveTransformerBase.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveTransformerBase.kt @@ -51,6 +51,9 @@ abstract class KNonRecursiveTransformerBase: KTransformer { if (exprWasTransformed) { transformed[e] = transformedExpr + + @Suppress("UNCHECKED_CAST") + onNewTransformedExpr(e as KExpr, transformedExpr as KExpr) } } } finally { @@ -121,13 +124,17 @@ abstract class KNonRecursiveTransformerBase: KTransformer { * Get [expr] transformation result or * null if expression was not transformed yet * */ - fun transformedExpr(expr: KExpr): KExpr? { + open fun transformedExpr(expr: KExpr): KExpr? { if (!exprTransformationRequired(expr)) return expr @Suppress("UNCHECKED_CAST") return transformed[expr] as? KExpr } + open fun onNewTransformedExpr(expr: KExpr, transformed: KExpr) { + // do nothing + } + /** * Erase [expr] transformation result. * Useful for transformer auxiliary expressions. diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveVisitorBase.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveVisitorBase.kt index 70a462833..da7a105da 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveVisitorBase.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveVisitorBase.kt @@ -63,9 +63,13 @@ abstract class KNonRecursiveVisitorBase : KVisitor> * Get [expr] visit result. * Returns null if expression was not visited. * */ - fun visitResult(expr: KExpr): V? = + open fun visitResult(expr: KExpr): V? = visitResults[expr] + open fun onNewVisitResult(expr: KExpr, result: V) { + // do nothing + } + fun result(expr: KExpr): V = visitResult(expr) ?: error("Expr $expr was not properly visited") @@ -87,6 +91,7 @@ abstract class KNonRecursiveVisitorBase : KVisitor> if (result.hasResult) { visitResults[e] = result.result + onNewVisitResult(e, result.result) } } } finally { From dee0803308dea9ec7db8c5acdc4f146857ed5c7b Mon Sep 17 00:00:00 2001 From: Valentyn Sobol Date: Wed, 8 Oct 2025 13:56:36 +0300 Subject: [PATCH 2/2] Upgrade version --- README.md | 6 +++--- buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts | 2 +- docs/getting-started.md | 6 +++--- examples/build.gradle.kts | 6 +++--- 4 files changed, 10 insertions(+), 10 deletions(-) diff --git a/README.md b/README.md index e8f55b231..9c31b6717 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.6.3) +[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.6.4) [![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.6.3") +implementation("io.ksmt:ksmt-core:0.6.4") // z3 solver -implementation("io.ksmt:ksmt-z3:0.6.3") +implementation("io.ksmt:ksmt-z3:0.6.4") ``` 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 77153c282..ddbee4c1a 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.6.3" +version = "0.6.4" repositories { mavenCentral() diff --git a/docs/getting-started.md b/docs/getting-started.md index 4a91a0d0f..df95b2959 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.6.3") + implementation("io.ksmt:ksmt-core:0.6.4") } ``` @@ -43,9 +43,9 @@ dependencies { ```kotlin dependencies { // z3 - implementation("io.ksmt:ksmt-z3:0.6.3") + implementation("io.ksmt:ksmt-z3:0.6.4") // bitwuzla - implementation("io.ksmt:ksmt-bitwuzla:0.6.3") + implementation("io.ksmt:ksmt-bitwuzla:0.6.4") } ``` diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts index 273babf1e..18c7bbad2 100644 --- a/examples/build.gradle.kts +++ b/examples/build.gradle.kts @@ -9,11 +9,11 @@ repositories { dependencies { // core - implementation("io.ksmt:ksmt-core:0.6.3") + implementation("io.ksmt:ksmt-core:0.6.4") // z3 solver - implementation("io.ksmt:ksmt-z3:0.6.3") + implementation("io.ksmt:ksmt-z3:0.6.4") // Runner and portfolio solver - implementation("io.ksmt:ksmt-runner:0.6.3") + implementation("io.ksmt:ksmt-runner:0.6.4") } java {