Skip to content

Commit 86fc1cf

Browse files
SaloedSaloed
authored
Symfpu model fix (#128)
* Fix SymFpu model
1 parent 6803209 commit 86fc1cf

12 files changed

Lines changed: 140 additions & 27 deletions

File tree

‎README.md‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ Get the most out of SMT solving with KSMT features:
1111
* Streamlined [solver delivery](#ksmt-distribution) with no need for building a solver or implementing JVM bindings
1212

1313
[![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)
14-
[![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)
14+
[![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)
1515
[![javadoc](https://javadoc.io/badge2/io.ksmt/ksmt-core/javadoc.svg)](https://javadoc.io/doc/io.ksmt/ksmt-core)
1616

1717
## Get started
@@ -20,9 +20,9 @@ To start using KSMT, install it via [Gradle](https://gradle.org/):
2020

2121
```kotlin
2222
// core
23-
implementation("io.ksmt:ksmt-core:0.5.6")
23+
implementation("io.ksmt:ksmt-core:0.5.7")
2424
// z3 solver
25-
implementation("io.ksmt:ksmt-z3:0.5.6")
25+
implementation("io.ksmt:ksmt-z3:0.5.7")
2626
```
2727

2828
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‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ plugins {
1111
}
1212

1313
group = "io.ksmt"
14-
version = "0.5.6"
14+
version = "0.5.7"
1515

1616
repositories {
1717
mavenCentral()

‎docs/getting-started.md‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ repositories {
3434
```kotlin
3535
dependencies {
3636
// core
37-
implementation("io.ksmt:ksmt-core:0.5.6")
37+
implementation("io.ksmt:ksmt-core:0.5.7")
3838
}
3939
```
4040

@@ -43,9 +43,9 @@ dependencies {
4343
```kotlin
4444
dependencies {
4545
// z3
46-
implementation("io.ksmt:ksmt-z3:0.5.6")
46+
implementation("io.ksmt:ksmt-z3:0.5.7")
4747
// bitwuzla
48-
implementation("io.ksmt:ksmt-bitwuzla:0.5.6")
48+
implementation("io.ksmt:ksmt-bitwuzla:0.5.7")
4949
}
5050
```
5151

‎examples/build.gradle.kts‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,11 +9,11 @@ repositories {
99

1010
dependencies {
1111
// core
12-
implementation("io.ksmt:ksmt-core:0.5.6")
12+
implementation("io.ksmt:ksmt-core:0.5.7")
1313
// z3 solver
14-
implementation("io.ksmt:ksmt-z3:0.5.6")
14+
implementation("io.ksmt:ksmt-z3:0.5.7")
1515
// Runner and portfolio solver
16-
implementation("io.ksmt:ksmt-runner:0.5.6")
16+
implementation("io.ksmt:ksmt-runner:0.5.7")
1717
}
1818

1919
java {

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

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -60,12 +60,13 @@ open class KModelImpl(
6060

6161
override fun equals(other: Any?): Boolean {
6262
if (this === other) return true
63-
if (javaClass != other?.javaClass) return false
6463

65-
other as KModelImpl
64+
if (other !is KModel) return false
65+
val detachedOther = other.detach() as KModelImpl
6666

67-
if (ctx != other.ctx) return false
68-
if (interpretations != other.interpretations) return false
67+
if (ctx != detachedOther.ctx) return false
68+
if (interpretations != detachedOther.interpretations) return false
69+
if (uninterpretedSortsUniverses != detachedOther.uninterpretedSortsUniverses) return false
6970

7071
return true
7172
}

‎ksmt-symfpu/build.gradle.kts‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
11
plugins {
22
id("io.ksmt.ksmt-base")
3-
id("com.github.johnrengelman.shadow") version "7.1.2"
43
}
54

65
repositories {

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

Lines changed: 33 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,8 @@ import io.ksmt.expr.KArrayStoreBase
88
import io.ksmt.expr.KExpr
99
import io.ksmt.expr.KFunctionAsArray
1010
import io.ksmt.expr.KUninterpretedSortValue
11+
import io.ksmt.expr.transformer.KExprVisitResult
12+
import io.ksmt.expr.transformer.KNonRecursiveVisitor
1113
import io.ksmt.solver.KModel
1214
import io.ksmt.solver.model.KFuncInterp
1315
import io.ksmt.solver.model.KFuncInterpEntryVarsFree
@@ -29,7 +31,7 @@ import io.ksmt.symfpu.operations.pack
2931
import io.ksmt.utils.asExpr
3032
import io.ksmt.utils.uncheckedCast
3133

32-
class SymFpuModel(private val kModel: KModel, val ctx: KContext, val transformer: FpToBvTransformer) : KModel {
34+
class KSymFpuModel(private val kModel: KModel, val ctx: KContext, val transformer: FpToBvTransformer) : KModel {
3335
override val declarations: Set<KDecl<*>>
3436
get() = kModel.declarations.mapTo(hashSetOf()) { transformer.findFpDeclByMappedDecl(it) ?: it }
3537

@@ -38,6 +40,7 @@ class SymFpuModel(private val kModel: KModel, val ctx: KContext, val transformer
3840

3941
private val evaluatorWithModelCompletion by lazy { KModelEvaluator(ctx, this, isComplete = true) }
4042
private val evaluatorWithoutModelCompletion by lazy { KModelEvaluator(ctx, this, isComplete = false) }
43+
private val functionAsArrayVisitor = FunctionAsArrayVisitor()
4144
private val interpretations: MutableMap<KDecl<*>, KFuncInterp<*>> = hashMapOf()
4245

4346
override fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set<KUninterpretedSortValue>? =
@@ -55,7 +58,9 @@ class SymFpuModel(private val kModel: KModel, val ctx: KContext, val transformer
5558
return interpretations.getOrPut(decl) {
5659
val mappedDecl = transformer.findMappedDeclForFpDecl(decl)
5760
if (mappedDecl == null) {
58-
return@getOrPut kModel.interpretation<T>(decl) ?: return null
61+
val interpretation = kModel.interpretation<T>(decl)
62+
interpretation?.let { functionAsArrayVisitor.visitInterpretation(it) }
63+
return@getOrPut interpretation ?: return null
5964
}
6065

6166
val interpretation = kModel.interpretation(mappedDecl) ?: return null
@@ -257,4 +262,30 @@ class SymFpuModel(private val kModel: KModel, val ctx: KContext, val transformer
257262

258263
return KModelImpl(ctx, interpretations.toMap(), uninterpretedSortsUniverses)
259264
}
265+
266+
override fun toString(): String = detach().toString()
267+
override fun hashCode(): Int = detach().hashCode()
268+
override fun equals(other: Any?): Boolean {
269+
if (this === other) return true
270+
if (other !is KModel) return false
271+
return detach() == other
272+
}
273+
274+
private inner class FunctionAsArrayVisitor : KNonRecursiveVisitor<Unit>(ctx) {
275+
override fun <T : KSort> defaultValue(expr: KExpr<T>) = Unit
276+
override fun mergeResults(left: Unit, right: Unit) = Unit
277+
278+
override fun <A : KArraySortBase<R>, R : KSort> visit(expr: KFunctionAsArray<A, R>): KExprVisitResult<Unit> {
279+
interpretation(expr.function)
280+
return saveVisitResult(expr, Unit)
281+
}
282+
283+
fun <T : KSort> visitInterpretation(interpretation: KFuncInterp<T>) {
284+
// Non-array expression cannot contain function-as-array
285+
if (interpretation.sort !is KArraySortBase<*>) return
286+
287+
interpretation.default?.let { applyVisitor(it) }
288+
interpretation.entries.forEach { applyVisitor(it.value) }
289+
}
290+
}
260291
}

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ import io.ksmt.solver.KSolverStatus
99
import io.ksmt.sort.KBoolSort
1010
import kotlin.time.Duration
1111

12-
open class SymFpuSolver<Config : KSolverConfiguration>(
12+
open class KSymFpuSolver<Config : KSolverConfiguration>(
1313
val solver: KSolver<Config>,
1414
val ctx: KContext,
1515
packedBvOptimizationEnabled: Boolean = true
@@ -32,7 +32,7 @@ open class SymFpuSolver<Config : KSolverConfiguration>(
3232
transformer.applyAndGetExpr(expr).also { mapTransformedToOriginalAssertions[it] = expr }
3333
}, timeout)
3434

35-
override fun model(): KModel = SymFpuModel(solver.model(), ctx, transformer)
35+
override fun model(): KModel = KSymFpuModel(solver.model(), ctx, transformer)
3636

3737
override fun unsatCore(): List<KExpr<KBoolSort>> = solver.unsatCore().map {
3838
mapTransformedToOriginalAssertions[it]

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,14 +5,14 @@ import io.ksmt.expr.KFpRoundingMode
55
import io.ksmt.solver.KSolverStatus
66
import io.ksmt.solver.z3.KZ3Solver
77
import io.ksmt.solver.z3.KZ3SolverConfiguration
8-
import io.ksmt.symfpu.solver.SymFpuSolver
8+
import io.ksmt.symfpu.solver.KSymFpuSolver
99
import io.ksmt.utils.getValue
1010
import io.ksmt.utils.mkConst
1111
import org.junit.jupiter.api.Test
1212
import kotlin.test.assertEquals
1313

1414
class ArraySymFpuTest {
15-
class SymFpuZ3Solver(ctx: KContext) : SymFpuSolver<KZ3SolverConfiguration>(KZ3Solver(ctx), ctx)
15+
class SymFpuZ3Solver(ctx: KContext) : KSymFpuSolver<KZ3SolverConfiguration>(KZ3Solver(ctx), ctx)
1616

1717
@Test
1818
fun testFpArrayExpr() = with(KContext(simplificationMode = KContext.SimplificationMode.NO_SIMPLIFY)) {

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

Lines changed: 82 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,82 @@
1+
package io.ksmt.symfpu
2+
3+
import io.ksmt.KContext
4+
import io.ksmt.decl.KDecl
5+
import io.ksmt.expr.KExpr
6+
import io.ksmt.expr.KFunctionAsArray
7+
import io.ksmt.expr.KUninterpretedSortValue
8+
import io.ksmt.solver.KModel
9+
import io.ksmt.solver.model.KFuncInterp
10+
import io.ksmt.solver.model.KFuncInterpVarsFree
11+
import io.ksmt.solver.model.KModelImpl
12+
import io.ksmt.sort.KSort
13+
import io.ksmt.sort.KUninterpretedSort
14+
import io.ksmt.symfpu.solver.FpToBvTransformer
15+
import io.ksmt.symfpu.solver.KSymFpuModel
16+
import io.ksmt.utils.uncheckedCast
17+
import kotlin.test.Test
18+
import kotlin.test.assertEquals
19+
import kotlin.test.assertNotNull
20+
21+
class ModelTest {
22+
23+
@Test
24+
fun testModelInterpretationPropagation() = with(KContext()) {
25+
val baseModel = ModelStub(this)
26+
val symFpuModel = KSymFpuModel(baseModel, this, FpToBvTransformer(this, packedBvOptimization = true))
27+
28+
val aInterp = symFpuModel.interpretation(baseModel.aDecl)
29+
assertEquals(aInterp, baseModel.interpretation(baseModel.aDecl))
30+
31+
val aFunction = aInterp?.default as? KFunctionAsArray<*, *>
32+
assertNotNull(aFunction)
33+
assertEquals(baseModel.fDecl, aFunction.function)
34+
35+
val fInterp = symFpuModel.interpretation(aFunction.function)
36+
assertEquals(baseModel.interpretation(aFunction.function), fInterp)
37+
}
38+
39+
@Test
40+
fun testModelDetachPropagation() = with(KContext()) {
41+
val baseModel = ModelStub(this)
42+
val symFpuModel = KSymFpuModel(baseModel, this, FpToBvTransformer(this, packedBvOptimization = true))
43+
assertEquals(baseModel.detach(), symFpuModel)
44+
}
45+
46+
class ModelStub(val ctx: KContext) : KModel {
47+
val aDecl = ctx.mkFreshConstDecl("a", ctx.mkArraySort(ctx.intSort, ctx.intSort))
48+
val fDecl = ctx.mkFreshFuncDecl("f", ctx.intSort, listOf(ctx.intSort))
49+
50+
override val declarations: Set<KDecl<*>>
51+
get() = setOf(aDecl)
52+
53+
private val interpretations = mutableMapOf<KDecl<*>, KFuncInterp<*>>()
54+
55+
override fun <T : KSort> interpretation(decl: KDecl<T>): KFuncInterp<T>? =
56+
interpretations.getOrPut(decl) {
57+
when (decl) {
58+
aDecl -> {
59+
interpretations[fDecl] = KFuncInterpVarsFree(decl, emptyList(), ctx.mkIntNum(0).uncheckedCast())
60+
KFuncInterpVarsFree(decl, emptyList(), ctx.mkFunctionAsArray(aDecl.sort, fDecl).uncheckedCast())
61+
}
62+
63+
else -> {
64+
error("Unexpected decl: $decl")
65+
}
66+
}
67+
}.uncheckedCast()
68+
69+
override fun detach(): KModel {
70+
declarations.forEach { interpretation(it) }
71+
return KModelImpl(ctx, interpretations.toMap(), emptyMap())
72+
}
73+
74+
override val uninterpretedSorts: Set<KUninterpretedSort> = emptySet()
75+
76+
override fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set<KUninterpretedSortValue>? = null
77+
78+
override fun <T : KSort> eval(expr: KExpr<T>, isComplete: Boolean): KExpr<T> {
79+
error("Unused")
80+
}
81+
}
82+
}

0 commit comments

Comments
 (0)