Fix expressions simplification (#144)

* Runner: fix child process termination * Core: avoid explosive flattening * Upgrade version to 0.5.14
UnitTestBot · Nov 3, 2023 · 3769986 · 3769986
1 parent d848167
commit 3769986
Show file tree

Hide file tree

Showing 13 changed files with 54 additions and 26 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.13)
+[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.14)
 [![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.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
@@ -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
@@ -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
@@ -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
@@ -953,7 +953,7 @@ interface KArrayExprSimplifier : KExprSimplifierBase {
         val original: KExpr<A>,
         val base: KExpr<A>,
         val values: List<KExpr<R>>
-    ) : KExpr<A>(ctx) {
+    ) : KExpr<A>(ctx), KSimplifierAuxExpr {
         override val sort: A
             get() = base.sort
 
@@ -1146,7 +1146,7 @@ interface KArrayExprSimplifier : KExprSimplifierBase {
     private sealed class SimplifierArraySelectBaseExpr<A : KArraySortBase<R>, R : KSort>(
         ctx: KContext,
         val array: KExpr<A>
-    ) : KExpr<R>(ctx) {
+    ) : KExpr<R>(ctx), KSimplifierAuxExpr {
         override val sort: R
             get() = array.sort.range
 
@@ -1217,7 +1217,7 @@ interface KArrayExprSimplifier : KExprSimplifierBase {
     private sealed class SelectFromStoreExprBase<A : KArraySortBase<R>, R : KSort>(
         ctx: KContext,
         array: KArrayStoreBase<A, R>
-    ) : KExpr<R>(ctx) {
+    ) : KExpr<R>(ctx), KSimplifierAuxExpr {
         val storeValue: KExpr<R> = 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
@@ -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<KBoolSort>,
         val trueBranch: KExpr<T>,
         val falseBranch: KExpr<T>
-    ) : KApp<T, KBoolSort>(ctx) {
+    ) : KApp<T, KBoolSort>(ctx), KSimplifierAuxExpr {
 
         override val decl: KDecl<T>
             get() = ctx.mkIteDecl(trueBranch.sort)
@@ -240,7 +241,7 @@ interface KBoolExprSimplifier : KExprSimplifierBase {
         val simplifiedCondition: KExpr<KBoolSort>,
         val trueBranch: KExpr<T>,
         val falseBranch: KExpr<T>
-    ) : KApp<T, T>(ctx) {
+    ) : KApp<T, T>(ctx), KSimplifierAuxExpr {
 
         override val decl: KDecl<T>
             get() = ctx.mkIteDecl(trueBranch.sort)
@@ -272,7 +273,7 @@ interface KBoolExprSimplifier : KExprSimplifierBase {
         val neutralElement: KExpr<KBoolSort>,
         val zeroElement: KExpr<KBoolSort>,
         override val args: List<KExpr<KBoolSort>>
-    ) : KApp<KBoolSort, KBoolSort>(ctx) {
+    ) : KApp<KBoolSort, KBoolSort>(ctx), KSimplifierAuxExpr {
         override val sort: KBoolSort = ctx.boolSort
         override val decl: KDecl<KBoolSort>
             get() = when (operation) {
@@ -287,6 +288,7 @@ interface KBoolExprSimplifier : KExprSimplifierBase {
 
         val simplifiedArgs = arrayListOf<KExpr<KBoolSort>>()
 
+        private val visitedArgs = IdentityHashMap<KExpr<*>, Unit>()
         private val argsIteratorStack = arrayListOf(args.iterator())
         private var currentArgument: KExpr<KBoolSort>? = 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
@@ -1083,7 +1083,7 @@ interface KBvExprSimplifier : KExprSimplifierBase {
     private class SimplifierFlatBvAddExpr<T : KBvSort>(
         ctx: KContext,
         override val args: List<KExpr<T>>
-    ) : KApp<T, T>(ctx) {
+    ) : KApp<T, T>(ctx), KSimplifierAuxExpr {
 
         override val decl: KDecl<T>
             get() = ctx.mkBvAddDecl(sort, sort)
@@ -1104,7 +1104,7 @@ interface KBvExprSimplifier : KExprSimplifierBase {
     private class SimplifierFlatBvMulExpr<T : KBvSort>(
         ctx: KContext,
         override val args: List<KExpr<T>>
-    ) : KApp<T, T>(ctx) {
+    ) : KApp<T, T>(ctx), KSimplifierAuxExpr {
 
         override val decl: KDecl<T>
             get() = ctx.mkBvMulDecl(sort, sort)
@@ -1125,7 +1125,7 @@ interface KBvExprSimplifier : KExprSimplifierBase {
     private class SimplifierFlatBvOrExpr<T : KBvSort>(
         ctx: KContext,
         override val args: List<KExpr<T>>
-    ) : KApp<T, T>(ctx) {
+    ) : KApp<T, T>(ctx), KSimplifierAuxExpr {
 
         override val decl: KDecl<T>
             get() = ctx.mkBvOrDecl(sort, sort)
@@ -1146,7 +1146,7 @@ interface KBvExprSimplifier : KExprSimplifierBase {
     private class SimplifierFlatBvAndExpr<T : KBvSort>(
         ctx: KContext,
         override val args: List<KExpr<T>>
-    ) : KApp<T, T>(ctx) {
+    ) : KApp<T, T>(ctx), KSimplifierAuxExpr {
 
         override val decl: KDecl<T>
             get() = ctx.mkBvAndDecl(sort, sort)
@@ -1167,7 +1167,7 @@ interface KBvExprSimplifier : KExprSimplifierBase {
     private class SimplifierFlatBvXorExpr<T : KBvSort>(
         ctx: KContext,
         override val args: List<KExpr<T>>
-    ) : KApp<T, T>(ctx) {
+    ) : KApp<T, T>(ctx), KSimplifierAuxExpr {
 
         override val decl: KDecl<T>
             get() = ctx.mkBvXorDecl(sort, sort)
@@ -1189,7 +1189,7 @@ interface KBvExprSimplifier : KExprSimplifierBase {
         ctx: KContext,
         override val sort: KBvSort,
         override val args: List<KExpr<KBvSort>>
-    ) : KApp<KBvSort, KBvSort>(ctx) {
+    ) : KApp<KBvSort, KBvSort>(ctx), KSimplifierAuxExpr {
 
         // We have no decl, but we don't care since decl is unused
         override val decl: KDecl<KBvSort>

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
@@ -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
@@ -46,6 +46,11 @@ interface KExprSimplifierBase : KTransformer {
 @JvmInline
 internal value class SimplifierAuxExpression<T : KSort>(val expr: KExpr<T>)
 
+/**
+ * Mark simplifier auxiliary expressions.
+ * */
+internal interface KSimplifierAuxExpr
+
 internal inline fun <T : KSort> auxExpr(builder: () -> KExpr<T>): SimplifierAuxExpression<T> =
     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
@@ -128,6 +128,14 @@ abstract class KNonRecursiveTransformerBase: KTransformer {
         return transformed[expr] as? KExpr<T>
     }
 
+    /**
+     * 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
@@ -29,7 +29,7 @@ abstract class ChildProcessBase<Model> {
     private val synchronizer = Channel<State>(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<String>): KsmtWorkerArgs
 
     fun start(args: Array<String>) = runBlocking {
@@ -84,7 +84,7 @@ abstract class ChildProcessBase<Model> {
             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
@@ -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<SolverProtocolModel>() {
         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<SolverProtocolModel>() {
         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
@@ -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<TestProtocolModel>() {
         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