diff --git a/README.md b/README.md
index d9fb8fc22..cefc4deb7 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
[](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml)
-[](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.13)
+[](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.14)
[](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.13")
+implementation("io.ksmt:ksmt-core:0.5.14")
// z3 solver
-implementation("io.ksmt:ksmt-z3:0.5.13")
+implementation("io.ksmt:ksmt-z3:0.5.14")
```
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 9f6a75210..749500ba0 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.13"
+version = "0.5.14"
repositories {
mavenCentral()
diff --git a/docs/getting-started.md b/docs/getting-started.md
index 41d76bbaa..f1eeb9141 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.13")
+ implementation("io.ksmt:ksmt-core:0.5.14")
}
```
@@ -43,9 +43,9 @@ dependencies {
```kotlin
dependencies {
// z3
- implementation("io.ksmt:ksmt-z3:0.5.13")
+ implementation("io.ksmt:ksmt-z3:0.5.14")
// bitwuzla
- implementation("io.ksmt:ksmt-bitwuzla:0.5.13")
+ implementation("io.ksmt:ksmt-bitwuzla:0.5.14")
}
```
diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts
index ec8a6ce6d..be8527bb7 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.13")
+ implementation("io.ksmt:ksmt-core:0.5.14")
// z3 solver
- implementation("io.ksmt:ksmt-z3:0.5.13")
+ implementation("io.ksmt:ksmt-z3:0.5.14")
// Runner and portfolio solver
- implementation("io.ksmt:ksmt-runner:0.5.13")
+ implementation("io.ksmt:ksmt-runner:0.5.14")
}
java {
diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KArrayExprSimplifier.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KArrayExprSimplifier.kt
index 3dcae72f4..886b37f5c 100644
--- a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KArrayExprSimplifier.kt
+++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KArrayExprSimplifier.kt
@@ -953,7 +953,7 @@ interface KArrayExprSimplifier : KExprSimplifierBase {
val original: KExpr,
val base: KExpr,
val values: List>
- ) : KExpr(ctx) {
+ ) : KExpr(ctx), KSimplifierAuxExpr {
override val sort: A
get() = base.sort
@@ -1146,7 +1146,7 @@ interface KArrayExprSimplifier : KExprSimplifierBase {
private sealed class SimplifierArraySelectBaseExpr, R : KSort>(
ctx: KContext,
val array: KExpr
- ) : KExpr(ctx) {
+ ) : KExpr(ctx), KSimplifierAuxExpr {
override val sort: R
get() = array.sort.range
@@ -1217,7 +1217,7 @@ interface KArrayExprSimplifier : KExprSimplifierBase {
private sealed class SelectFromStoreExprBase, R : KSort>(
ctx: KContext,
array: KArrayStoreBase
- ) : KExpr(ctx) {
+ ) : KExpr(ctx), KSimplifierAuxExpr {
val storeValue: KExpr = array.value
override val sort: R = storeValue.sort
diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KBoolExprSimplifier.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KBoolExprSimplifier.kt
index 81b012048..40540f921 100644
--- a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KBoolExprSimplifier.kt
+++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KBoolExprSimplifier.kt
@@ -15,6 +15,7 @@ import io.ksmt.expr.KXorExpr
import io.ksmt.expr.transformer.KTransformerBase
import io.ksmt.sort.KBoolSort
import io.ksmt.sort.KSort
+import java.util.IdentityHashMap
interface KBoolExprSimplifier : KExprSimplifierBase {
@@ -213,7 +214,7 @@ interface KBoolExprSimplifier : KExprSimplifierBase {
val condition: KExpr,
val trueBranch: KExpr,
val falseBranch: KExpr
- ) : KApp(ctx) {
+ ) : KApp(ctx), KSimplifierAuxExpr {
override val decl: KDecl
get() = ctx.mkIteDecl(trueBranch.sort)
@@ -240,7 +241,7 @@ interface KBoolExprSimplifier : KExprSimplifierBase {
val simplifiedCondition: KExpr,
val trueBranch: KExpr,
val falseBranch: KExpr
- ) : KApp(ctx) {
+ ) : KApp(ctx), KSimplifierAuxExpr {
override val decl: KDecl
get() = ctx.mkIteDecl(trueBranch.sort)
@@ -272,7 +273,7 @@ interface KBoolExprSimplifier : KExprSimplifierBase {
val neutralElement: KExpr,
val zeroElement: KExpr,
override val args: List>
- ) : KApp(ctx) {
+ ) : KApp(ctx), KSimplifierAuxExpr {
override val sort: KBoolSort = ctx.boolSort
override val decl: KDecl
get() = when (operation) {
@@ -287,6 +288,7 @@ interface KBoolExprSimplifier : KExprSimplifierBase {
val simplifiedArgs = arrayListOf>()
+ private val visitedArgs = IdentityHashMap, Unit>()
private val argsIteratorStack = arrayListOf(args.iterator())
private var currentArgument: KExpr? = null
@@ -309,6 +311,9 @@ interface KBoolExprSimplifier : KExprSimplifierBase {
while (hasUnprocessedArgument()) {
val argument = argsIteratorStack.last().next()
+
+ if (visitedArgs.put(argument, Unit) != null) continue
+
if (!tryFlatExpr(argument)) {
currentArgument = argument
return
diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KBvExprSimplifier.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KBvExprSimplifier.kt
index 779fd5eb1..f737f7b4d 100644
--- a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KBvExprSimplifier.kt
+++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KBvExprSimplifier.kt
@@ -1083,7 +1083,7 @@ interface KBvExprSimplifier : KExprSimplifierBase {
private class SimplifierFlatBvAddExpr(
ctx: KContext,
override val args: List>
- ) : KApp(ctx) {
+ ) : KApp(ctx), KSimplifierAuxExpr {
override val decl: KDecl
get() = ctx.mkBvAddDecl(sort, sort)
@@ -1104,7 +1104,7 @@ interface KBvExprSimplifier : KExprSimplifierBase {
private class SimplifierFlatBvMulExpr(
ctx: KContext,
override val args: List>
- ) : KApp(ctx) {
+ ) : KApp(ctx), KSimplifierAuxExpr {
override val decl: KDecl
get() = ctx.mkBvMulDecl(sort, sort)
@@ -1125,7 +1125,7 @@ interface KBvExprSimplifier : KExprSimplifierBase {
private class SimplifierFlatBvOrExpr(
ctx: KContext,
override val args: List>
- ) : KApp(ctx) {
+ ) : KApp(ctx), KSimplifierAuxExpr {
override val decl: KDecl
get() = ctx.mkBvOrDecl(sort, sort)
@@ -1146,7 +1146,7 @@ interface KBvExprSimplifier : KExprSimplifierBase {
private class SimplifierFlatBvAndExpr(
ctx: KContext,
override val args: List>
- ) : KApp(ctx) {
+ ) : KApp(ctx), KSimplifierAuxExpr {
override val decl: KDecl
get() = ctx.mkBvAndDecl(sort, sort)
@@ -1167,7 +1167,7 @@ interface KBvExprSimplifier : KExprSimplifierBase {
private class SimplifierFlatBvXorExpr(
ctx: KContext,
override val args: List>
- ) : KApp(ctx) {
+ ) : KApp(ctx), KSimplifierAuxExpr {
override val decl: KDecl
get() = ctx.mkBvXorDecl(sort, sort)
@@ -1189,7 +1189,7 @@ interface KBvExprSimplifier : KExprSimplifierBase {
ctx: KContext,
override val sort: KBvSort,
override val args: List>
- ) : KApp(ctx) {
+ ) : KApp(ctx), KSimplifierAuxExpr {
// We have no decl, but we don't care since decl is unused
override val decl: KDecl
diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KExprSimplifier.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KExprSimplifier.kt
index 3d1eda88f..0335f1a09 100644
--- a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KExprSimplifier.kt
+++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KExprSimplifier.kt
@@ -343,6 +343,10 @@ open class KExprSimplifier(override val ctx: KContext) :
val result = transformedExpr(rewriteFrame.rewritten)
?: error("Nested rewrite failed")
+ if (rewriteFrame.rewritten is KSimplifierAuxExpr) {
+ eraseTransformationResult(rewriteFrame.rewritten)
+ }
+
return result.uncheckedCast()
}
diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KExprSimplifierBase.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KExprSimplifierBase.kt
index 46c7b9698..38721ec46 100644
--- a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KExprSimplifierBase.kt
+++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KExprSimplifierBase.kt
@@ -46,6 +46,11 @@ interface KExprSimplifierBase : KTransformer {
@JvmInline
internal value class SimplifierAuxExpression(val expr: KExpr)
+/**
+ * Mark simplifier auxiliary expressions.
+ * */
+internal interface KSimplifierAuxExpr
+
internal inline fun auxExpr(builder: () -> KExpr): SimplifierAuxExpression =
SimplifierAuxExpression(builder())
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 00abc2a83..feaf36820 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
@@ -128,6 +128,14 @@ abstract class KNonRecursiveTransformerBase: KTransformer {
return transformed[expr] as? KExpr
}
+ /**
+ * Erase [expr] transformation result.
+ * Useful for transformer auxiliary expressions.
+ * */
+ fun eraseTransformationResult(expr: KExpr<*>) {
+ transformed.remove(expr)
+ }
+
/**
* Allows to skip expression transformation and stop deepening.
* */
diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/runner/core/ChildProcessBase.kt b/ksmt-runner/src/main/kotlin/io/ksmt/runner/core/ChildProcessBase.kt
index be7d8dc1c..dcb56e4c5 100644
--- a/ksmt-runner/src/main/kotlin/io/ksmt/runner/core/ChildProcessBase.kt
+++ b/ksmt-runner/src/main/kotlin/io/ksmt/runner/core/ChildProcessBase.kt
@@ -29,7 +29,7 @@ abstract class ChildProcessBase {
private val synchronizer = Channel(capacity = 1)
abstract fun initProtocolModel(protocol: IProtocol): Model
- abstract fun Model.setup(astSerializationCtx: AstSerializationCtx)
+ abstract fun Model.setup(astSerializationCtx: AstSerializationCtx, lifetime: Lifetime)
abstract fun parseArgs(args: Array): KsmtWorkerArgs
fun start(args: Array) = runBlocking {
@@ -84,7 +84,7 @@ abstract class ChildProcessBase {
initProtocolModel(clientProtocol)
}.await()
- protocolModel.setup(astSerializationCtx)
+ protocolModel.setup(astSerializationCtx, lifetime)
clientProtocol.syncProtocolModel.synchronizationSignal.let { sync ->
val answerFromMainProcess = sync.adviseForConditionAsync(lifetime) {
diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverWorkerProcess.kt b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverWorkerProcess.kt
index 2506d578a..48ff7c29b 100644
--- a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverWorkerProcess.kt
+++ b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverWorkerProcess.kt
@@ -1,6 +1,7 @@
package io.ksmt.solver.runner
import com.jetbrains.rd.framework.IProtocol
+import com.jetbrains.rd.util.lifetime.Lifetime
import io.ksmt.KContext
import io.ksmt.expr.KExpr
import io.ksmt.runner.core.ChildProcessBase
@@ -44,7 +45,7 @@ class KSolverWorkerProcess : ChildProcessBase() {
protocol.solverProtocolModel
@Suppress("LongMethod")
- override fun SolverProtocolModel.setup(astSerializationCtx: AstSerializationCtx) {
+ override fun SolverProtocolModel.setup(astSerializationCtx: AstSerializationCtx, lifetime: Lifetime) {
initSolver.measureExecutionForTermination { params ->
check(workerCtx == null) { "Solver is initialized" }
@@ -141,6 +142,10 @@ class KSolverWorkerProcess : ChildProcessBase() {
interrupt.measureExecutionForTermination {
solver.interrupt()
}
+ lifetime.onTermination {
+ workerSolver?.close()
+ workerCtx?.close()
+ }
}
private fun serializeFunctionInterpretation(interp: KFuncInterp<*>): ModelEntry {
diff --git a/ksmt-test/src/main/kotlin/io/ksmt/test/TestWorkerProcess.kt b/ksmt-test/src/main/kotlin/io/ksmt/test/TestWorkerProcess.kt
index d6308d7de..0a702df7d 100644
--- a/ksmt-test/src/main/kotlin/io/ksmt/test/TestWorkerProcess.kt
+++ b/ksmt-test/src/main/kotlin/io/ksmt/test/TestWorkerProcess.kt
@@ -1,6 +1,7 @@
package io.ksmt.test
import com.jetbrains.rd.framework.IProtocol
+import com.jetbrains.rd.util.lifetime.Lifetime
import com.microsoft.z3.AST
import com.microsoft.z3.BoolSort
import com.microsoft.z3.Context
@@ -236,7 +237,7 @@ class TestWorkerProcess : ChildProcessBase() {
protocol.testProtocolModel
@Suppress("LongMethod")
- override fun TestProtocolModel.setup(astSerializationCtx: AstSerializationCtx) {
+ override fun TestProtocolModel.setup(astSerializationCtx: AstSerializationCtx, lifetime: Lifetime) {
// Limit z3 native memory usage to avoid OOM
Native.globalParamSet("memory_high_watermark_mb", "2048") // 2048 megabytes