Rework model detach (#151)

* Rework model detach * Upgrade version to 0.5.18
UnitTestBot · Feb 1, 2024 · 5a18458 · 5a18458
1 parent eaedb86
commit 5a18458
Show file tree

Hide file tree

Showing 19 changed files with 159 additions and 71 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.17)
+[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.18)
 [![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.17")
+implementation("io.ksmt:ksmt-core:0.5.18")
 // z3 solver
-implementation("io.ksmt:ksmt-z3:0.5.17")
+implementation("io.ksmt:ksmt-z3:0.5.18")
 ```
 
 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.17"
+version = "0.5.18"
 
 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.17")    
+    implementation("io.ksmt:ksmt-core:0.5.18")    
 }
 ```
 
@@ -43,9 +43,9 @@ dependencies {
 ```kotlin
 dependencies {
     // z3 
-    implementation("io.ksmt:ksmt-z3:0.5.17")
+    implementation("io.ksmt:ksmt-z3:0.5.18")
     // bitwuzla
-    implementation("io.ksmt:ksmt-bitwuzla:0.5.17")
+    implementation("io.ksmt:ksmt-bitwuzla:0.5.18")
 }
 ```
 

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.17")
+    implementation("io.ksmt:ksmt-core:0.5.18")
     // z3 solver
-    implementation("io.ksmt:ksmt-z3:0.5.17")
+    implementation("io.ksmt:ksmt-z3:0.5.18")
     // Runner and portfolio solver
-    implementation("io.ksmt:ksmt-runner:0.5.17")
+    implementation("io.ksmt:ksmt-runner:0.5.18")
 }
 
 java {

diff --git a/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaModel.kt b/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaModel.kt
@@ -31,7 +31,6 @@ open class KBitwuzlaModel(
     assertedDeclarations: Set<KDecl<*>>,
     private val uninterpretedSortDependency: Map<KUninterpretedSort, Set<KDecl<*>>>
 ) : KModel {
-
     private val modelDeclarations = assertedDeclarations.toHashSet()
 
     override val declarations: Set<KDecl<*>>
@@ -263,15 +262,14 @@ open class KBitwuzlaModel(
             interpretation(it) ?: error("missed interpretation for $it")
         }
 
+        // The model is detached from the solver and therefore invalid
+        markInvalid()
+
         return KModelImpl(ctx, interpretations, uninterpretedSortsUniverses)
     }
 
-    override fun toString(): String = detach().toString()
-    override fun hashCode(): Int = detach().hashCode()
-    override fun equals(other: Any?): Boolean {
-        if (this === other) return true
-        if (other !is KModel) return false
-        return detach() == other
+    override fun close() {
+        markInvalid()
     }
 
     /**

diff --git a/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaSolver.kt b/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaSolver.kt
@@ -6,6 +6,7 @@ import io.ksmt.expr.KExpr
 import io.ksmt.solver.KModel
 import io.ksmt.solver.KSolver
 import io.ksmt.solver.KSolverStatus
+import io.ksmt.solver.model.KNativeSolverModel
 import org.ksmt.solver.bitwuzla.bindings.BitwuzlaNativeException
 import org.ksmt.solver.bitwuzla.bindings.BitwuzlaOption
 import org.ksmt.solver.bitwuzla.bindings.BitwuzlaResult
@@ -27,7 +28,8 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver<KBitwuzlaSolverC
     private var lastCheckStatus = KSolverStatus.UNKNOWN
     private var lastReasonOfUnknown: String? = null
     private var lastAssumptions: TrackedAssumptions? = null
-    private var lastModel: KBitwuzlaModel? = null
+    private var lastBitwuzlaModel: KBitwuzlaModel? = null
+    private var lastModel: KModel? = null
 
     init {
         Native.bitwuzlaSetOption(bitwuzlaCtx.bitwuzla, BitwuzlaOption.BITWUZLA_OPT_INCREMENTAL, value = 1)
@@ -121,13 +123,17 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver<KBitwuzlaSolverC
 
     override fun model(): KModel = bitwuzlaCtx.bitwuzlaTry {
         require(lastCheckStatus == KSolverStatus.SAT) { "Model are only available after SAT checks" }
-        val model = lastModel ?: KBitwuzlaModel(
+        lastModel?.let { return it }
+
+        val bitwuzlaModel = KBitwuzlaModel(
             ctx, bitwuzlaCtx, exprConverter,
             bitwuzlaCtx.declarations(),
             bitwuzlaCtx.uninterpretedSortsWithRelevantDecls()
         )
-        lastModel = model
-        model
+        return KNativeSolverModel(bitwuzlaModel).also {
+            lastBitwuzlaModel = bitwuzlaModel
+            lastModel = it
+        }
     }
 
     override fun unsatCore(): List<KExpr<KBoolSort>> = bitwuzlaCtx.bitwuzlaTry {
@@ -163,7 +169,8 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver<KBitwuzlaSolverC
         /**
          * Bitwuzla model is only valid until the next check-sat call.
          * */
-        lastModel?.markInvalid()
+        lastBitwuzlaModel?.markInvalid()
+        lastBitwuzlaModel = null
         lastModel = null
 
         lastCheckStatus = KSolverStatus.UNKNOWN

diff --git a/ksmt-bitwuzla/ksmt-bitwuzla-core/src/test/kotlin/io/ksmt/solver/bitwuzla/Example.kt b/ksmt-bitwuzla/ksmt-bitwuzla-core/src/test/kotlin/io/ksmt/solver/bitwuzla/Example.kt
@@ -6,7 +6,6 @@ import io.ksmt.sort.KArraySort
 import io.ksmt.utils.mkConst
 import kotlin.test.Test
 import kotlin.test.assertEquals
-import kotlin.test.assertFailsWith
 import kotlin.test.assertNotNull
 import kotlin.test.assertTrue
 
@@ -63,7 +62,6 @@ class Example {
 
         solver.close()
 
-        assertFailsWith(IllegalStateException::class) { model.interpretation(b) }
         assertEquals(aValue, detachedModel.eval(a))
         assertEquals(cValue, detachedModel.eval(c))
     }

diff --git a/ksmt-core/src/main/kotlin/io/ksmt/solver/KModel.kt b/ksmt-core/src/main/kotlin/io/ksmt/solver/KModel.kt
@@ -7,7 +7,7 @@ import io.ksmt.solver.model.KFuncInterp
 import io.ksmt.sort.KSort
 import io.ksmt.sort.KUninterpretedSort
 
-interface KModel {
+interface KModel : AutoCloseable {
     val declarations: Set<KDecl<*>>
 
     val uninterpretedSorts: Set<KUninterpretedSort>
@@ -21,5 +21,13 @@ interface KModel {
      * */
     fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set<KUninterpretedSortValue>?
 
+    /**
+     * Detach model from the solver and release native resources.
+     * */
     fun detach(): KModel
+
+    /**
+     * Close model and release acquired native resources.
+     * */
+    override fun close()
 }
diff --git a/ksmt-core/src/main/kotlin/io/ksmt/solver/model/KModelImpl.kt b/ksmt-core/src/main/kotlin/io/ksmt/solver/model/KModelImpl.kt
@@ -72,4 +72,8 @@ open class KModelImpl(
     }
 
     override fun hashCode(): Int = interpretations.hashCode()
+
+    override fun close() {
+        // nothing to close
+    }
 }
diff --git a/ksmt-core/src/main/kotlin/io/ksmt/solver/model/KNativeSolverModel.kt b/ksmt-core/src/main/kotlin/io/ksmt/solver/model/KNativeSolverModel.kt
@@ -0,0 +1,42 @@
+package io.ksmt.solver.model
+
+import io.ksmt.decl.KDecl
+import io.ksmt.expr.KExpr
+import io.ksmt.expr.KUninterpretedSortValue
+import io.ksmt.solver.KModel
+import io.ksmt.sort.KSort
+import io.ksmt.sort.KUninterpretedSort
+
+class KNativeSolverModel(nativeModel: KModel): KModel {
+    private var model: KModel = nativeModel
+
+    override val declarations: Set<KDecl<*>> get() = model.declarations
+
+    override val uninterpretedSorts: Set<KUninterpretedSort> get() = model.uninterpretedSorts
+
+    override fun <T : KSort> eval(expr: KExpr<T>, isComplete: Boolean): KExpr<T> =
+        model.eval(expr, isComplete)
+
+    override fun <T : KSort> interpretation(decl: KDecl<T>): KFuncInterp<T>? =
+        model.interpretation(decl)
+
+    override fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set<KUninterpretedSortValue>? =
+        model.uninterpretedSortUniverse(sort)
+
+    override fun detach(): KModel {
+        model = model.detach()
+        return model
+    }
+
+    override fun close() {
+        model.close()
+    }
+
+    override fun toString(): String = detach().toString()
+    override fun hashCode(): Int = detach().hashCode()
+    override fun equals(other: Any?): Boolean {
+        if (this === other) return true
+        if (other !is KModel) return false
+        return detach() == other
+    }
+}
diff --git a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Model.kt b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Model.kt
@@ -108,19 +108,17 @@ open class KCvc5Model(
             uninterpretedSortUniverse(it) ?: error("missed sort universe for $it")
         }
 
+        // The model is detached from the solver and therefore invalid
+        markInvalid()
+
         return KModelImpl(ctx, interpretations, uninterpretedSortsUniverses)
     }
 
-    private fun ensureContextActive() = check(cvc5Ctx.isActive) { "Context already closed" }
-
-    override fun toString(): String = detach().toString()
-    override fun hashCode(): Int = detach().hashCode()
-    override fun equals(other: Any?): Boolean {
-        if (this === other) return true
-        if (other !is KModel) return false
-        return detach() == other
+    override fun close() {
+        markInvalid()
     }
 
+    private fun ensureContextActive() = check(cvc5Ctx.isActive) { "Context already closed" }
 
     private fun getUninterpretedSortContext(sort: KUninterpretedSort): UninterpretedSortValueContext =
         uninterpretedSortValues.getOrPut(sort) { UninterpretedSortValueContext(sort) }

diff --git a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Solver.kt b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Solver.kt
@@ -10,6 +10,7 @@ import io.ksmt.solver.KModel
 import io.ksmt.solver.KSolver
 import io.ksmt.solver.KSolverException
 import io.ksmt.solver.KSolverStatus
+import io.ksmt.solver.model.KNativeSolverModel
 import io.ksmt.sort.KBoolSort
 import io.ksmt.utils.library.NativeLibraryLoaderUtils
 import java.util.TreeMap
@@ -27,7 +28,8 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver<KCvc5SolverConfigura
 
     private var lastCheckStatus = KSolverStatus.UNKNOWN
     private var lastReasonOfUnknown: String? = null
-    private var lastModel: KCvc5Model? = null
+    private var lastCvcModel: KCvc5Model? = null
+    private var lastModel: KModel? = null
 
     // we need TreeMap here (hashcode not implemented in Term)
     private var cvc5LastAssumptions: TreeMap<Term, KExpr<KBoolSort>>? = null
@@ -130,16 +132,20 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver<KCvc5SolverConfigura
 
     override fun model(): KModel = cvc5Try {
         require(lastCheckStatus == KSolverStatus.SAT) { "Models are only available after SAT checks" }
-        val model = lastModel ?: KCvc5Model(
+        lastModel?.let { return it }
+
+        val cvcModel = KCvc5Model(
             ctx,
             cvc5Ctx,
             exprInternalizer,
             cvc5Ctx.declarations().flatMapTo(hashSetOf()) { it },
             cvc5Ctx.uninterpretedSorts().flatMapTo(hashSetOf()) { it },
         )
-        lastModel = model
 
-        model
+        return KNativeSolverModel(cvcModel).also {
+            lastCvcModel = cvcModel
+            lastModel = it
+        }
     }
 
     override fun unsatCore(): List<KExpr<KBoolSort>> = cvc5Try {
@@ -205,7 +211,8 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver<KCvc5SolverConfigura
         /**
          * Cvc5 model is only valid until the next check-sat call.
          * */
-        lastModel?.markInvalid()
+        lastCvcModel?.markInvalid()
+        lastCvcModel = null
         lastModel = null
 
         lastCheckStatus = KSolverStatus.UNKNOWN

diff --git a/ksmt-symfpu/src/main/kotlin/io/ksmt/symfpu/solver/KSymFpuModel.kt b/ksmt-symfpu/src/main/kotlin/io/ksmt/symfpu/solver/KSymFpuModel.kt
@@ -31,9 +31,12 @@ import io.ksmt.symfpu.operations.pack
 import io.ksmt.utils.asExpr
 import io.ksmt.utils.uncheckedCast
 
-class KSymFpuModel(private val kModel: KModel, val ctx: KContext, val transformer: FpToBvTransformer) : KModel {
-    override val declarations: Set<KDecl<*>>
-        get() = kModel.declarations.mapTo(hashSetOf()) { transformer.findFpDeclByMappedDecl(it) ?: it }
+class KSymFpuModel(underlyingModel: KModel, val ctx: KContext, val transformer: FpToBvTransformer) : KModel {
+    private var kModel: KModel = underlyingModel
+
+    override val declarations: Set<KDecl<*>> by lazy {
+        kModel.declarations.mapTo(hashSetOf()) { transformer.findFpDeclByMappedDecl(it) ?: it }
+    }
 
     override val uninterpretedSorts
         get() = kModel.uninterpretedSorts
@@ -252,6 +255,8 @@ class KSymFpuModel(private val kModel: KModel, val ctx: KContext, val transforme
     }
 
     override fun detach(): KModel {
+        kModel = kModel.detach()
+
         declarations.forEach {
             interpretation(it) ?: error("missed interpretation for $it")
         }
@@ -263,6 +268,10 @@ class KSymFpuModel(private val kModel: KModel, val ctx: KContext, val transforme
         return KModelImpl(ctx, interpretations.toMap(), uninterpretedSortsUniverses)
     }
 
+    override fun close() {
+        kModel.close()
+    }
+
     override fun toString(): String = detach().toString()
     override fun hashCode(): Int = detach().hashCode()
     override fun equals(other: Any?): Boolean {

diff --git a/ksmt-symfpu/src/test/kotlin/io/ksmt/symfpu/ModelTest.kt b/ksmt-symfpu/src/test/kotlin/io/ksmt/symfpu/ModelTest.kt
@@ -71,6 +71,10 @@ class ModelTest {
             return KModelImpl(ctx, interpretations.toMap(), emptyMap())
         }
 
+        override fun close() {
+            // ignored
+        }
+
         override val uninterpretedSorts: Set<KUninterpretedSort> = emptySet()
 
         override fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set<KUninterpretedSortValue>? = null