Transformer cache extension points

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 

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()

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")
 }
 ```
 

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 {

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<KSort>, transformedExpr as KExpr<KSort>)
                 }
             }
         } finally {
@@ -121,13 +124,17 @@ abstract class KNonRecursiveTransformerBase: KTransformer {
      *  Get [expr] transformation result or
      *  null if expression was not transformed yet
      * */
-    fun <T : KSort> transformedExpr(expr: KExpr<T>): KExpr<T>? {
+    open fun <T : KSort> transformedExpr(expr: KExpr<T>): KExpr<T>? {
         if (!exprTransformationRequired(expr)) return expr
 
         @Suppress("UNCHECKED_CAST")
         return transformed[expr] as? KExpr<T>
     }
 
+    open fun <T : KSort> onNewTransformedExpr(expr: KExpr<T>, transformed: KExpr<T>) {
+        // do nothing
+    }
+
     /**
      * Erase [expr] transformation result.
      * Useful for transformer auxiliary expressions.

ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveVisitorBase.kt

@@ -63,9 +63,13 @@ abstract class KNonRecursiveVisitorBase<V : Any> : KVisitor<KExprVisitResult<V>>
      *  Get [expr] visit result.
      *  Returns null if expression was not visited.
      * */
-    fun <T : KSort> visitResult(expr: KExpr<T>): V? =
+    open fun <T : KSort> visitResult(expr: KExpr<T>): V? =
         visitResults[expr]
 
+    open fun <T : KSort> onNewVisitResult(expr: KExpr<T>, result: V) {
+        // do nothing
+    }
+
     fun <T : KSort> result(expr: KExpr<T>): V =
         visitResult(expr) ?: error("Expr $expr was not properly visited")
 
@@ -87,6 +91,7 @@ abstract class KNonRecursiveVisitorBase<V : Any> : KVisitor<KExprVisitResult<V>>
 
                 if (result.hasResult) {
                     visitResults[e] = result.result
+                    onNewVisitResult(e, result.result)
                 }
             }
         } finally {