diff --git a/README.md b/README.md index c3077da68..6d0852183 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 [![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 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 434a8fbb7..9b096cccb 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.6" +version = "0.5.7" repositories { mavenCentral() diff --git a/docs/getting-started.md b/docs/getting-started.md index 78517c002..cd4393c5d 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.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") } ``` diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts index 59928efef..61be1f49b 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.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 { 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 index 22b4a9e15..ee5a5f578 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/solver/model/KModelImpl.kt +++ b/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 } diff --git a/ksmt-symfpu/build.gradle.kts b/ksmt-symfpu/build.gradle.kts index 274b3dd1e..57223afa3 100644 --- a/ksmt-symfpu/build.gradle.kts +++ b/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 { diff --git a/ksmt-symfpu/src/main/kotlin/io/ksmt/symfpu/solver/SymFpuModel.kt b/ksmt-symfpu/src/main/kotlin/io/ksmt/symfpu/solver/KSymFpuModel.kt similarity index 86% rename from ksmt-symfpu/src/main/kotlin/io/ksmt/symfpu/solver/SymFpuModel.kt rename to ksmt-symfpu/src/main/kotlin/io/ksmt/symfpu/solver/KSymFpuModel.kt index 07ce9dc42..bfcabefdc 100644 --- a/ksmt-symfpu/src/main/kotlin/io/ksmt/symfpu/solver/SymFpuModel.kt +++ b/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> 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, KFuncInterp<*>> = hashMapOf() override fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set? = @@ -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(decl) ?: return null + val interpretation = kModel.interpretation(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(ctx) { + override fun defaultValue(expr: KExpr) = Unit + override fun mergeResults(left: Unit, right: Unit) = Unit + + override fun , R : KSort> visit(expr: KFunctionAsArray): KExprVisitResult { + interpretation(expr.function) + return saveVisitResult(expr, Unit) + } + + fun visitInterpretation(interpretation: KFuncInterp) { + // 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) } + } + } } diff --git a/ksmt-symfpu/src/main/kotlin/io/ksmt/symfpu/solver/SymFpuSolver.kt b/ksmt-symfpu/src/main/kotlin/io/ksmt/symfpu/solver/KSymFpuSolver.kt similarity index 93% rename from ksmt-symfpu/src/main/kotlin/io/ksmt/symfpu/solver/SymFpuSolver.kt rename to ksmt-symfpu/src/main/kotlin/io/ksmt/symfpu/solver/KSymFpuSolver.kt index 8fb8f14b3..42d292f78 100644 --- a/ksmt-symfpu/src/main/kotlin/io/ksmt/symfpu/solver/SymFpuSolver.kt +++ b/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( +open class KSymFpuSolver( val solver: KSolver, val ctx: KContext, packedBvOptimizationEnabled: Boolean = true @@ -32,7 +32,7 @@ open class SymFpuSolver( 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> = solver.unsatCore().map { mapTransformedToOriginalAssertions[it] diff --git a/ksmt-symfpu/src/test/kotlin/io/ksmt/symfpu/ArraySymFpuTest.kt b/ksmt-symfpu/src/test/kotlin/io/ksmt/symfpu/ArraySymFpuTest.kt index 4fa7c3b1a..968fb8555 100644 --- a/ksmt-symfpu/src/test/kotlin/io/ksmt/symfpu/ArraySymFpuTest.kt +++ b/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(KZ3Solver(ctx), ctx) + class SymFpuZ3Solver(ctx: KContext) : KSymFpuSolver(KZ3Solver(ctx), ctx) @Test fun testFpArrayExpr() = with(KContext(simplificationMode = KContext.SimplificationMode.NO_SIMPLIFY)) { diff --git a/ksmt-symfpu/src/test/kotlin/io/ksmt/symfpu/ModelTest.kt b/ksmt-symfpu/src/test/kotlin/io/ksmt/symfpu/ModelTest.kt new file mode 100644 index 000000000..1fc5f1269 --- /dev/null +++ b/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> + get() = setOf(aDecl) + + private val interpretations = mutableMapOf, KFuncInterp<*>>() + + override fun interpretation(decl: KDecl): KFuncInterp? = + 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 = emptySet() + + override fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set? = null + + override fun eval(expr: KExpr, isComplete: Boolean): KExpr { + error("Unused") + } + } +} diff --git a/ksmt-test/src/test/kotlin/io/ksmt/test/benchmarks/FpBenchmarks.kt b/ksmt-test/src/test/kotlin/io/ksmt/test/benchmarks/FpBenchmarks.kt index d1257e9c7..ba74fc577 100644 --- a/ksmt-test/src/test/kotlin/io/ksmt/test/benchmarks/FpBenchmarks.kt +++ b/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(KZ3Solver(ctx), ctx) +class SymFpuZ3Solver(ctx: KContext) : KSymFpuSolver(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(KBitwuzlaSolver(ctx), ctx) +class SymFpuBitwuzlaSolver(ctx: KContext) : KSymFpuSolver(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(KYicesSolver(ctx), ctx) +class SymFpuYicesSolver(ctx: KContext) : KSymFpuSolver(KYicesSolver(ctx), ctx) class YicesWithSymFpuFpBenchmarks : FpBenchmarks() { @Execution(ExecutionMode.SAME_THREAD) diff --git a/ksmt-test/src/test/kotlin/io/ksmt/test/benchmarks/SymFpuBenchmarksBasedTest.kt b/ksmt-test/src/test/kotlin/io/ksmt/test/benchmarks/SymFpuBenchmarksBasedTest.kt index cc64cd02f..d9fd5f119 100644 --- a/ksmt-test/src/test/kotlin/io/ksmt/test/benchmarks/SymFpuBenchmarksBasedTest.kt +++ b/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(KZ3Solver(ctx), ctx) + class SymFpuZ3Solver(ctx: KContext) : KSymFpuSolver(KZ3Solver(ctx), ctx) @Execution(ExecutionMode.CONCURRENT) @ParameterizedTest(name = "{0}")