Symfpu model fix

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.6)
+[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.7)
 [![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.6")
+implementation("io.ksmt:ksmt-core:0.5.7")
 // z3 solver
-implementation("io.ksmt:ksmt-z3:0.5.6")
+implementation("io.ksmt:ksmt-z3:0.5.7")
 ```
 
 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.5.6"
+version = "0.5.7"
 
 repositories {
     mavenCentral()

docs/getting-started.md

@@ -34,7 +34,7 @@ repositories {
 ```kotlin
 dependencies {
     // core 
-    implementation("io.ksmt:ksmt-core:0.5.6")    
+    implementation("io.ksmt:ksmt-core:0.5.7")    
 }
 ```
 
@@ -43,9 +43,9 @@ dependencies {
 ```kotlin
 dependencies {
     // z3 
-    implementation("io.ksmt:ksmt-z3:0.5.6")
+    implementation("io.ksmt:ksmt-z3:0.5.7")
     // bitwuzla
-    implementation("io.ksmt:ksmt-bitwuzla:0.5.6")
+    implementation("io.ksmt:ksmt-bitwuzla:0.5.7")
 }
 ```
 

examples/build.gradle.kts

@@ -9,11 +9,11 @@ repositories {
 
 dependencies {
     // core
-    implementation("io.ksmt:ksmt-core:0.5.6")
+    implementation("io.ksmt:ksmt-core:0.5.7")
     // z3 solver
-    implementation("io.ksmt:ksmt-z3:0.5.6")
+    implementation("io.ksmt:ksmt-z3:0.5.7")
     // Runner and portfolio solver
-    implementation("io.ksmt:ksmt-runner:0.5.6")
+    implementation("io.ksmt:ksmt-runner:0.5.7")
 }
 
 java {

ksmt-core/src/main/kotlin/io/ksmt/solver/model/KModelImpl.kt

@@ -60,12 +60,13 @@ open class KModelImpl(
 
     override fun equals(other: Any?): Boolean {
         if (this === other) return true
-        if (javaClass != other?.javaClass) return false
 
-        other as KModelImpl
+        if (other !is KModel) return false
+        val detachedOther = other.detach() as KModelImpl
 
-        if (ctx != other.ctx) return false
-        if (interpretations != other.interpretations) return false
+        if (ctx != detachedOther.ctx) return false
+        if (interpretations != detachedOther.interpretations) return false
+        if (uninterpretedSortsUniverses != detachedOther.uninterpretedSortsUniverses) return false
 
         return true
     }

ksmt-symfpu/build.gradle.kts

@@ -1,6 +1,5 @@
 plugins {
     id("io.ksmt.ksmt-base")
-    id("com.github.johnrengelman.shadow") version "7.1.2"
 }
 
 repositories {

ksmt-symfpu/src/main/kotlin/io/ksmt/symfpu/solver/SymFpuModel.kt → ksmt-symfpu/src/main/kotlin/io/ksmt/symfpu/solver/KSymFpuModel.kt

@@ -8,6 +8,8 @@ import io.ksmt.expr.KArrayStoreBase
 import io.ksmt.expr.KExpr
 import io.ksmt.expr.KFunctionAsArray
 import io.ksmt.expr.KUninterpretedSortValue
+import io.ksmt.expr.transformer.KExprVisitResult
+import io.ksmt.expr.transformer.KNonRecursiveVisitor
 import io.ksmt.solver.KModel
 import io.ksmt.solver.model.KFuncInterp
 import io.ksmt.solver.model.KFuncInterpEntryVarsFree
@@ -29,7 +31,7 @@ import io.ksmt.symfpu.operations.pack
 import io.ksmt.utils.asExpr
 import io.ksmt.utils.uncheckedCast
 
-class SymFpuModel(private val kModel: KModel, val ctx: KContext, val transformer: FpToBvTransformer) : KModel {
+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 }
 
@@ -38,6 +40,7 @@ class SymFpuModel(private val kModel: KModel, val ctx: KContext, val transformer
 
     private val evaluatorWithModelCompletion by lazy { KModelEvaluator(ctx, this, isComplete = true) }
     private val evaluatorWithoutModelCompletion by lazy { KModelEvaluator(ctx, this, isComplete = false) }
+    private val functionAsArrayVisitor = FunctionAsArrayVisitor()
     private val interpretations: MutableMap<KDecl<*>, KFuncInterp<*>> = hashMapOf()
 
     override fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set<KUninterpretedSortValue>? =
@@ -55,7 +58,9 @@ class SymFpuModel(private val kModel: KModel, val ctx: KContext, val transformer
         return interpretations.getOrPut(decl) {
             val mappedDecl = transformer.findMappedDeclForFpDecl(decl)
             if (mappedDecl == null) {
-                return@getOrPut kModel.interpretation<T>(decl) ?: return null
+                val interpretation = kModel.interpretation<T>(decl)
+                interpretation?.let { functionAsArrayVisitor.visitInterpretation(it) }
+                return@getOrPut interpretation ?: return null
             }
 
             val interpretation = kModel.interpretation(mappedDecl) ?: return null
@@ -257,4 +262,30 @@ class SymFpuModel(private val kModel: KModel, val ctx: KContext, val transformer
 
         return KModelImpl(ctx, interpretations.toMap(), 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
+    }
+
+    private inner class FunctionAsArrayVisitor : KNonRecursiveVisitor<Unit>(ctx) {
+        override fun <T : KSort> defaultValue(expr: KExpr<T>) = Unit
+        override fun mergeResults(left: Unit, right: Unit) = Unit
+
+        override fun <A : KArraySortBase<R>, R : KSort> visit(expr: KFunctionAsArray<A, R>): KExprVisitResult<Unit> {
+            interpretation(expr.function)
+            return saveVisitResult(expr, Unit)
+        }
+
+        fun <T : KSort> visitInterpretation(interpretation: KFuncInterp<T>) {
+            // Non-array expression cannot contain function-as-array
+            if (interpretation.sort !is KArraySortBase<*>) return
+
+            interpretation.default?.let { applyVisitor(it) }
+            interpretation.entries.forEach { applyVisitor(it.value) }
+        }
+    }
 }

ksmt-symfpu/src/main/kotlin/io/ksmt/symfpu/solver/SymFpuSolver.kt → ksmt-symfpu/src/main/kotlin/io/ksmt/symfpu/solver/KSymFpuSolver.kt

@@ -9,7 +9,7 @@ import io.ksmt.solver.KSolverStatus
 import io.ksmt.sort.KBoolSort
 import kotlin.time.Duration
 
-open class SymFpuSolver<Config : KSolverConfiguration>(
+open class KSymFpuSolver<Config : KSolverConfiguration>(
     val solver: KSolver<Config>,
     val ctx: KContext,
     packedBvOptimizationEnabled: Boolean = true
@@ -32,7 +32,7 @@ open class SymFpuSolver<Config : KSolverConfiguration>(
             transformer.applyAndGetExpr(expr).also { mapTransformedToOriginalAssertions[it] = expr }
         }, timeout)
 
-    override fun model(): KModel = SymFpuModel(solver.model(), ctx, transformer)
+    override fun model(): KModel = KSymFpuModel(solver.model(), ctx, transformer)
 
     override fun unsatCore(): List<KExpr<KBoolSort>> = solver.unsatCore().map {
         mapTransformedToOriginalAssertions[it]

ksmt-symfpu/src/test/kotlin/io/ksmt/symfpu/ArraySymFpuTest.kt

@@ -5,14 +5,14 @@ import io.ksmt.expr.KFpRoundingMode
 import io.ksmt.solver.KSolverStatus
 import io.ksmt.solver.z3.KZ3Solver
 import io.ksmt.solver.z3.KZ3SolverConfiguration
-import io.ksmt.symfpu.solver.SymFpuSolver
+import io.ksmt.symfpu.solver.KSymFpuSolver
 import io.ksmt.utils.getValue
 import io.ksmt.utils.mkConst
 import org.junit.jupiter.api.Test
 import kotlin.test.assertEquals
 
 class ArraySymFpuTest {
-    class SymFpuZ3Solver(ctx: KContext) : SymFpuSolver<KZ3SolverConfiguration>(KZ3Solver(ctx), ctx)
+    class SymFpuZ3Solver(ctx: KContext) : KSymFpuSolver<KZ3SolverConfiguration>(KZ3Solver(ctx), ctx)
 
     @Test
     fun testFpArrayExpr() = with(KContext(simplificationMode = KContext.SimplificationMode.NO_SIMPLIFY)) {

ksmt-symfpu/src/test/kotlin/io/ksmt/symfpu/ModelTest.kt

@@ -0,0 +1,82 @@
+package io.ksmt.symfpu
+
+import io.ksmt.KContext
+import io.ksmt.decl.KDecl
+import io.ksmt.expr.KExpr
+import io.ksmt.expr.KFunctionAsArray
+import io.ksmt.expr.KUninterpretedSortValue
+import io.ksmt.solver.KModel
+import io.ksmt.solver.model.KFuncInterp
+import io.ksmt.solver.model.KFuncInterpVarsFree
+import io.ksmt.solver.model.KModelImpl
+import io.ksmt.sort.KSort
+import io.ksmt.sort.KUninterpretedSort
+import io.ksmt.symfpu.solver.FpToBvTransformer
+import io.ksmt.symfpu.solver.KSymFpuModel
+import io.ksmt.utils.uncheckedCast
+import kotlin.test.Test
+import kotlin.test.assertEquals
+import kotlin.test.assertNotNull
+
+class ModelTest {
+
+    @Test
+    fun testModelInterpretationPropagation() = with(KContext()) {
+        val baseModel = ModelStub(this)
+        val symFpuModel = KSymFpuModel(baseModel, this, FpToBvTransformer(this, packedBvOptimization = true))
+
+        val aInterp = symFpuModel.interpretation(baseModel.aDecl)
+        assertEquals(aInterp, baseModel.interpretation(baseModel.aDecl))
+
+        val aFunction = aInterp?.default as? KFunctionAsArray<*, *>
+        assertNotNull(aFunction)
+        assertEquals(baseModel.fDecl, aFunction.function)
+
+        val fInterp = symFpuModel.interpretation(aFunction.function)
+        assertEquals(baseModel.interpretation(aFunction.function), fInterp)
+    }
+
+    @Test
+    fun testModelDetachPropagation() = with(KContext()) {
+        val baseModel = ModelStub(this)
+        val symFpuModel = KSymFpuModel(baseModel, this, FpToBvTransformer(this, packedBvOptimization = true))
+        assertEquals(baseModel.detach(), symFpuModel)
+    }
+
+    class ModelStub(val ctx: KContext) : KModel {
+        val aDecl = ctx.mkFreshConstDecl("a", ctx.mkArraySort(ctx.intSort, ctx.intSort))
+        val fDecl = ctx.mkFreshFuncDecl("f", ctx.intSort, listOf(ctx.intSort))
+
+        override val declarations: Set<KDecl<*>>
+            get() = setOf(aDecl)
+
+        private val interpretations = mutableMapOf<KDecl<*>, KFuncInterp<*>>()
+
+        override fun <T : KSort> interpretation(decl: KDecl<T>): KFuncInterp<T>? =
+            interpretations.getOrPut(decl) {
+                when (decl) {
+                    aDecl -> {
+                        interpretations[fDecl] = KFuncInterpVarsFree(decl, emptyList(), ctx.mkIntNum(0).uncheckedCast())
+                        KFuncInterpVarsFree(decl, emptyList(), ctx.mkFunctionAsArray(aDecl.sort, fDecl).uncheckedCast())
+                    }
+
+                    else -> {
+                        error("Unexpected decl: $decl")
+                    }
+                }
+            }.uncheckedCast()
+
+        override fun detach(): KModel {
+            declarations.forEach { interpretation(it) }
+            return KModelImpl(ctx, interpretations.toMap(), emptyMap())
+        }
+
+        override val uninterpretedSorts: Set<KUninterpretedSort> = emptySet()
+
+        override fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set<KUninterpretedSortValue>? = null
+
+        override fun <T : KSort> eval(expr: KExpr<T>, isComplete: Boolean): KExpr<T> {
+            error("Unused")
+        }
+    }
+}

ksmt-test/src/test/kotlin/io/ksmt/test/benchmarks/FpBenchmarks.kt

@@ -15,7 +15,7 @@ import io.ksmt.solver.z3.KZ3SMTLibParser
 import io.ksmt.solver.z3.KZ3Solver
 import io.ksmt.solver.z3.KZ3SolverConfiguration
 import io.ksmt.sort.KBoolSort
-import io.ksmt.symfpu.solver.SymFpuSolver
+import io.ksmt.symfpu.solver.KSymFpuSolver
 import org.junit.jupiter.api.parallel.Execution
 import org.junit.jupiter.api.parallel.ExecutionMode
 import java.nio.file.Path
@@ -39,7 +39,7 @@ class BitwuzlaFpBenchmarks : FpBenchmarks() {
         measureKsmtAssertionTime(name, samplePath, "Bitwuzla") { ctx -> KBitwuzlaSolver(ctx) }
 }
 
-class SymFpuZ3Solver(ctx: KContext) : SymFpuSolver<KZ3SolverConfiguration>(KZ3Solver(ctx), ctx)
+class SymFpuZ3Solver(ctx: KContext) : KSymFpuSolver<KZ3SolverConfiguration>(KZ3Solver(ctx), ctx)
 
 class Z3WithSymFpuFpBenchmarks : FpBenchmarks() {
     @Execution(ExecutionMode.SAME_THREAD)
@@ -49,7 +49,7 @@ class Z3WithSymFpuFpBenchmarks : FpBenchmarks() {
         measureKsmtAssertionTime(name, samplePath, "SymfpuZ3") { ctx -> SymFpuZ3Solver(ctx) }
 }
 
-class SymFpuBitwuzlaSolver(ctx: KContext) : SymFpuSolver<KBitwuzlaSolverConfiguration>(KBitwuzlaSolver(ctx), ctx)
+class SymFpuBitwuzlaSolver(ctx: KContext) : KSymFpuSolver<KBitwuzlaSolverConfiguration>(KBitwuzlaSolver(ctx), ctx)
 
 class BitwuzlaWithSymFpuFpBenchmarks : FpBenchmarks() {
     @Execution(ExecutionMode.SAME_THREAD)
@@ -59,7 +59,7 @@ class BitwuzlaWithSymFpuFpBenchmarks : FpBenchmarks() {
         measureKsmtAssertionTime(name, samplePath, "SymfpuBitwuzla") { ctx -> SymFpuBitwuzlaSolver(ctx) }
 }
 
-class SymFpuYicesSolver(ctx: KContext) : SymFpuSolver<KYicesSolverConfiguration>(KYicesSolver(ctx), ctx)
+class SymFpuYicesSolver(ctx: KContext) : KSymFpuSolver<KYicesSolverConfiguration>(KYicesSolver(ctx), ctx)
 
 class YicesWithSymFpuFpBenchmarks : FpBenchmarks() {
     @Execution(ExecutionMode.SAME_THREAD)

ksmt-test/src/test/kotlin/io/ksmt/test/benchmarks/SymFpuBenchmarksBasedTest.kt

@@ -4,7 +4,7 @@ import io.ksmt.KContext
 import io.ksmt.solver.z3.KZ3Solver
 import io.ksmt.solver.z3.KZ3SolverConfiguration
 import io.ksmt.solver.z3.KZ3SolverUniversalConfiguration
-import io.ksmt.symfpu.solver.SymFpuSolver
+import io.ksmt.symfpu.solver.KSymFpuSolver
 import org.junit.jupiter.api.parallel.Execution
 import org.junit.jupiter.api.parallel.ExecutionMode
 import org.junit.jupiter.params.ParameterizedTest
@@ -13,7 +13,7 @@ import java.nio.file.Path
 
 class SymFpuBenchmarksBasedTest : BenchmarksBasedTest() {
 
-    class SymFpuZ3Solver(ctx: KContext) : SymFpuSolver<KZ3SolverConfiguration>(KZ3Solver(ctx), ctx)
+    class SymFpuZ3Solver(ctx: KContext) : KSymFpuSolver<KZ3SolverConfiguration>(KZ3Solver(ctx), ctx)
 
     @Execution(ExecutionMode.CONCURRENT)
     @ParameterizedTest(name = "{0}")