Skip to content

Commit 10e4502

Browse files
dee-treedee-tree
committed
cvc5 expressions lifetime fix via native mkExprSolver;
added lifetime test
1 parent e69dd81 commit 10e4502

12 files changed

Lines changed: 194 additions & 76 deletions

File tree

‎ksmt-cvc5/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Context.kt‎

Lines changed: 18 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -34,14 +34,18 @@ import java.util.TreeMap
3434

3535
class KCvc5Context private constructor(
3636
private val solver: Solver,
37+
val mkExprSolver: Solver,
3738
private val ctx: KContext,
3839
parent: KCvc5Context?,
39-
isForking: Boolean
40+
val isForking: Boolean
4041
) : AutoCloseable {
41-
constructor(solver: Solver, ctx: KContext, isForking: Boolean = false) : this(solver, ctx, null, isForking)
42+
constructor(solver: Solver, mkExprSolver: Solver, ctx: KContext, isForking: Boolean = false)
43+
: this(solver, mkExprSolver, ctx, null, isForking)
44+
45+
constructor(solver: Solver, ctx: KContext, isForking: Boolean = false)
46+
: this(solver, solver, ctx, null, isForking)
4247

4348
private var isClosed = false
44-
private val isChild = parent != null
4549

4650
private val uninterpretedSortCollector = KUninterpretedSortCollector(this)
4751
private var exprCurrentLevelCacheRestorer = KCurrentScopeExprCacheRestorer(uninterpretedSortCollector, ctx)
@@ -71,7 +75,12 @@ class KCvc5Context private constructor(
7175
private val currentAccumulatedScopeExpressions: HashMap<KExpr<*>, Term>
7276
private val expressions: HashMap<KExpr<*>, Term>
7377

74-
// we can't use HashMap with Term and Sort (hashcode is not implemented)
78+
/**
79+
* We can't use HashMap with Term and Sort (hashcode is not implemented)
80+
*
81+
* Avoid to close cache explicitly due to its sharing between forking hierarchy.
82+
* It will be garbage collected on last solver close in forking hierarchy
83+
*/
7584
private val cvc5Expressions: TreeMap<Term, KExpr<*>>
7685
private val sorts: HashMap<KSort, Sort>
7786
private val cvc5Sorts: TreeMap<Sort, KSort>
@@ -146,11 +155,12 @@ class KCvc5Context private constructor(
146155
val isActive: Boolean
147156
get() = !isClosed
148157

149-
fun fork(solver: Solver): KCvc5Context = KCvc5Context(solver, ctx, this, true).also { forkCtx ->
150-
repeat(assertedConstraintLevels.size) {
151-
forkCtx.pushAssertionLevel()
158+
fun fork(solver: Solver, mkExprSolver: Solver): KCvc5Context =
159+
KCvc5Context(solver, mkExprSolver, ctx, this, true).also { forkCtx ->
160+
repeat(assertedConstraintLevels.size) {
161+
forkCtx.pushAssertionLevel()
162+
}
152163
}
153-
}
154164

155165
fun push() {
156166
declarations.push()
@@ -399,23 +409,11 @@ class KCvc5Context private constructor(
399409
return converted
400410
}
401411

402-
403412
override fun close() {
404413
if (isClosed) return
405414
isClosed = true
406415

407416
currentAccumulatedScopeExpressions.clear()
408-
409-
if (isChild) {
410-
expressions.clear()
411-
cvc5Expressions.clear()
412-
413-
sorts.clear()
414-
cvc5Sorts.clear()
415-
416-
decls.clear()
417-
cvc5Decls.clear()
418-
}
419417
}
420418

421419
class KUninterpretedSortCollector(private val cvc5Ctx: KCvc5Context) : KSortVisitor<Unit> {

‎ksmt-cvc5/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5DeclInternalizer.kt‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ open class KCvc5DeclInternalizer(
1818
val domainSorts = decl.argSorts.map { it.accept(sortInternalizer) }
1919
val rangeSort = decl.sort.accept(sortInternalizer)
2020

21-
cvc5Ctx.nativeSolver.declareFun(
21+
cvc5Ctx.mkExprSolver.declareFun(
2222
decl.name,
2323
domainSorts.toTypedArray(),
2424
rangeSort
@@ -29,6 +29,6 @@ open class KCvc5DeclInternalizer(
2929
cvc5Ctx.addDeclaration(decl)
3030

3131
val sort = decl.sort.accept(sortInternalizer)
32-
cvc5Ctx.nativeSolver.mkConst(sort, decl.name)
32+
cvc5Ctx.mkExprSolver.mkConst(sort, decl.name)
3333
}
3434
}

‎ksmt-cvc5/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprConverter.kt‎

Lines changed: 23 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -24,9 +24,10 @@ import io.ksmt.expr.KExpr
2424
import io.ksmt.expr.KFpRoundingMode
2525
import io.ksmt.expr.KInterpretedValue
2626
import io.ksmt.solver.KSolverUnsupportedFeatureException
27-
import io.ksmt.solver.util.KExprConverterBase
2827
import io.ksmt.solver.util.ExprConversionResult
28+
import io.ksmt.solver.util.KExprConverterBase
2929
import io.ksmt.solver.util.KExprConverterUtils.argumentsConversionRequired
30+
import io.ksmt.solver.util.conversionLoop
3031
import io.ksmt.sort.KArithSort
3132
import io.ksmt.sort.KArray2Sort
3233
import io.ksmt.sort.KArray3Sort
@@ -42,7 +43,7 @@ import io.ksmt.sort.KRealSort
4243
import io.ksmt.sort.KSort
4344
import io.ksmt.utils.asExpr
4445
import io.ksmt.utils.uncheckedCast
45-
import java.util.*
46+
import java.util.TreeMap
4647

4748
@Suppress("LargeClass")
4849
open class KCvc5ExprConverter(
@@ -734,6 +735,26 @@ open class KCvc5ExprConverter(
734735
}
735736
}
736737

738+
fun <T : KSort> Term.convertExprWithMkExprSolver(): KExpr<T> = convertExprWithoutCacheSave<T>().also {
739+
with(internalizer) {
740+
it.internalizeExpr()
741+
}
742+
}
743+
744+
fun <T : KSort> Term.convertExprWithoutCacheSave(): KExpr<T> {
745+
val wasteCache = TreeMap<Term, KExpr<*>>()
746+
return conversionLoop(
747+
stack = exprStack,
748+
native = this,
749+
stackPush = { stack, element -> stack.add(element) },
750+
stackPop = { stack -> stack.removeLast() },
751+
stackIsNotEmpty = { stack -> stack.isNotEmpty() },
752+
convertNative = { expr -> convertNativeExpr(expr) },
753+
findConverted = { expr -> wasteCache[expr] ?: findConvertedNative(expr) },
754+
saveConverted = { expr, converted -> wasteCache[expr] = converted }
755+
)
756+
}
757+
737758
fun <T : KSort> Term.convertExpr(): KExpr<T> = convertFromNative()
738759

739760
@Suppress("UNCHECKED_CAST")

‎ksmt-cvc5/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprInternalizer.kt‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -160,11 +160,11 @@ import io.ksmt.expr.KXorExpr
160160
import io.ksmt.expr.rewrite.simplify.rewriteBvAddNoOverflowExpr
161161
import io.ksmt.expr.rewrite.simplify.rewriteBvAddNoUnderflowExpr
162162
import io.ksmt.expr.rewrite.simplify.rewriteBvDivNoOverflowExpr
163+
import io.ksmt.expr.rewrite.simplify.rewriteBvMulNoOverflowExpr
164+
import io.ksmt.expr.rewrite.simplify.rewriteBvMulNoUnderflowExpr
163165
import io.ksmt.expr.rewrite.simplify.rewriteBvNegNoOverflowExpr
164166
import io.ksmt.expr.rewrite.simplify.rewriteBvSubNoOverflowExpr
165167
import io.ksmt.expr.rewrite.simplify.rewriteBvSubNoUnderflowExpr
166-
import io.ksmt.expr.rewrite.simplify.rewriteBvMulNoOverflowExpr
167-
import io.ksmt.expr.rewrite.simplify.rewriteBvMulNoUnderflowExpr
168168
import io.ksmt.expr.rewrite.simplify.simplifyBvRotateLeftExpr
169169
import io.ksmt.expr.rewrite.simplify.simplifyBvRotateRightExpr
170170
import io.ksmt.solver.KSolverUnsupportedFeatureException
@@ -203,7 +203,7 @@ class KCvc5ExprInternalizer(
203203
}
204204

205205
private val nsolver: Solver
206-
get() = cvc5Ctx.nativeSolver
206+
get() = cvc5Ctx.mkExprSolver
207207

208208
private val zeroIntValueTerm: Term by lazy { nsolver.mkInteger(0L) }
209209

‎ksmt-cvc5/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ForkingSolver.kt‎

Lines changed: 27 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
package io.ksmt.solver.cvc5
22

3+
import io.github.cvc5.Solver
34
import io.github.cvc5.Term
45
import io.ksmt.KContext
56
import io.ksmt.expr.KExpr
@@ -14,28 +15,29 @@ import kotlin.time.Duration
1415
open class KCvc5ForkingSolver internal constructor(
1516
ctx: KContext,
1617
private val manager: KCvc5ForkingSolverManager,
17-
parent: KCvc5ForkingSolver?
18+
/** store reference on Solver to separate lifetime of native expressions */
19+
private val mkExprSolver: Solver,
20+
parent: KCvc5ForkingSolver? = null
1821
) : KCvc5SolverBase(ctx), KForkingSolver<KCvc5SolverConfiguration>, KSolver<KCvc5SolverConfiguration> {
1922

2023
final override val cvc5Ctx: KCvc5Context
2124
private val isChild = parent != null
2225
private var assertionsInitiated = !isChild
2326

24-
private val _trackedAssertions: ScopedLinkedFrame<TreeMap<Term, KExpr<KBoolSort>>>
25-
26-
override val trackedAssertions: ScopedFrame<TreeMap<Term, KExpr<KBoolSort>>>
27-
get() = _trackedAssertions
28-
27+
private val trackedAssertions: ScopedLinkedFrame<TreeMap<Term, KExpr<KBoolSort>>>
2928
private val cvc5Assertions: ScopedLinkedFrame<TreeSet<Term>>
3029

30+
override val currentScope: UInt
31+
get() = trackedAssertions.currentScope
32+
3133
init {
3234
if (parent != null) {
33-
cvc5Ctx = parent.cvc5Ctx.fork(solver)
34-
_trackedAssertions = parent._trackedAssertions.fork()
35+
cvc5Ctx = parent.cvc5Ctx.fork(solver, this.mkExprSolver)
36+
trackedAssertions = parent.trackedAssertions.fork()
3537
cvc5Assertions = parent.cvc5Assertions.fork()
3638
} else {
37-
cvc5Ctx = KCvc5Context(solver, ctx, true)
38-
_trackedAssertions = ScopedLinkedFrame(::TreeMap, ::TreeMap)
39+
cvc5Ctx = KCvc5Context(solver, this.mkExprSolver, ctx, true)
40+
trackedAssertions = ScopedLinkedFrame(::TreeMap, ::TreeMap)
3941
cvc5Assertions = ScopedLinkedFrame(::TreeSet, ::TreeSet)
4042
}
4143
}
@@ -44,6 +46,10 @@ open class KCvc5ForkingSolver internal constructor(
4446
parent?.config?.fork(solver) ?: KCvc5ForkingSolverConfigurationImpl(solver)
4547
}
4648

49+
init {
50+
if (isChild) config // initialize child config
51+
}
52+
4753
override fun configure(configurator: KCvc5SolverConfiguration.() -> Unit) {
4854
config.configurator()
4955
}
@@ -54,7 +60,7 @@ open class KCvc5ForkingSolver internal constructor(
5460
if (assertionsInitiated) return
5561

5662
cvc5Assertions.stacked()
57-
.zip(_trackedAssertions.stacked())
63+
.zip(trackedAssertions.stacked())
5864
.asReversed()
5965
.forEachIndexed { scope, (cvc5AssertionFrame, trackedFrame) ->
6066
if (scope > 0) solver.push()
@@ -66,6 +72,12 @@ open class KCvc5ForkingSolver internal constructor(
6672
assertionsInitiated = true
6773
}
6874

75+
override fun saveTrackedAssertion(track: Term, trackedExpr: KExpr<KBoolSort>) {
76+
trackedAssertions.currentFrame[track] = trackedExpr
77+
}
78+
79+
override fun findTrackedExprByTrack(track: Term): KExpr<KBoolSort>? = trackedAssertions.find { it[track] }
80+
6981
override fun assert(expr: KExpr<KBoolSort>): Unit = cvc5Try {
7082
ctx.ensureContextMatch(expr)
7183
ensureAssertionsInitiated()
@@ -84,12 +96,14 @@ open class KCvc5ForkingSolver internal constructor(
8496
override fun push() {
8597
cvc5Try { ensureAssertionsInitiated() }
8698
super.push()
99+
trackedAssertions.push()
87100
cvc5Assertions.push()
88101
}
89102

90103
override fun pop(n: UInt) {
91104
cvc5Try { ensureAssertionsInitiated() }
92105
super.pop(n)
106+
trackedAssertions.pop(n)
93107
cvc5Assertions.pop(n)
94108
}
95109

@@ -105,22 +119,9 @@ open class KCvc5ForkingSolver internal constructor(
105119
return super.checkWithAssumptions(assumptions, timeout)
106120
}
107121

108-
override fun unsatCore(): List<KExpr<KBoolSort>> {
109-
val cvc5FullCore = cvc5UnsatCore()
110-
111-
val unsatCore = mutableListOf<KExpr<KBoolSort>>()
112-
113-
cvc5FullCore.forEach { unsatCoreTerm ->
114-
lastCvc5Assumptions?.get(unsatCoreTerm)?.also { unsatCore += it }
115-
?: trackedAssertions.find { trackedAssertion ->
116-
trackedAssertion[unsatCoreTerm]?.let { unsatCore += it; true } ?: false
117-
}
118-
}
119-
return unsatCore
120-
}
121-
122122
override fun close() {
123123
manager.close(this)
124-
super.close()
124+
solver.close()
125+
cvc5Ctx.close()
125126
}
126127
}

‎ksmt-cvc5/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ForkingSolverManager.kt‎

Lines changed: 44 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,30 +1,72 @@
11
package io.ksmt.solver.cvc5
22

3+
import io.github.cvc5.Solver
34
import io.ksmt.KContext
45
import io.ksmt.solver.KForkingSolver
56
import io.ksmt.solver.KForkingSolverManager
7+
import java.util.IdentityHashMap
68
import java.util.concurrent.ConcurrentHashMap
79

810
open class KCvc5ForkingSolverManager(private val ctx: KContext) : KForkingSolverManager<KCvc5SolverConfiguration> {
911

1012
private val solvers: MutableSet<KCvc5ForkingSolver> = ConcurrentHashMap.newKeySet()
1113

14+
/**
15+
* for each parent to child hierarchy created only one mkExprSolver,
16+
* which is responsible for native expressions lifetime
17+
*/
18+
private val forkingSolverToMkExprSolver = IdentityHashMap<KCvc5ForkingSolver, Solver>()
19+
private val mkExprSolverReferences = IdentityHashMap<Solver, Int>()
20+
1221
override fun mkForkingSolver(): KForkingSolver<KCvc5SolverConfiguration> {
13-
return KCvc5ForkingSolver(ctx, this, null).also { solvers += it }
22+
val mkExprSolver = Solver()
23+
incRef(mkExprSolver)
24+
return KCvc5ForkingSolver(ctx, this, mkExprSolver, null).also {
25+
solvers += it
26+
forkingSolverToMkExprSolver[it] = mkExprSolver
27+
}
1428
}
1529

1630
internal fun mkForkingSolver(parent: KCvc5ForkingSolver): KForkingSolver<KCvc5SolverConfiguration> {
17-
return KCvc5ForkingSolver(ctx, this, parent).also { solvers += it }
31+
val mkExprSolver = forkingSolverToMkExprSolver.getValue(parent)
32+
incRef(mkExprSolver)
33+
return KCvc5ForkingSolver(ctx, this, mkExprSolver, parent).also {
34+
solvers += it
35+
forkingSolverToMkExprSolver[it] = mkExprSolver
36+
}
1837
}
1938

2039
/**
2140
* unregister [solver] for this manager
2241
*/
2342
internal fun close(solver: KCvc5ForkingSolver) {
2443
solvers -= solver
44+
val mkExprSolver = forkingSolverToMkExprSolver.getValue(solver)
45+
forkingSolverToMkExprSolver -= solver
46+
decRef(mkExprSolver)
2547
}
2648

2749
override fun close() {
2850
solvers.forEach(KCvc5ForkingSolver::close)
2951
}
52+
53+
private fun incRef(mkExprSolver: Solver) {
54+
mkExprSolverReferences[mkExprSolver] = mkExprSolverReferences.getOrDefault(mkExprSolver, 0) + 1
55+
}
56+
57+
private fun decRef(mkExprSolver: Solver) {
58+
val referencesAfterDec = mkExprSolverReferences.getValue(mkExprSolver) - 1
59+
if (referencesAfterDec == 0) {
60+
mkExprSolverReferences -= mkExprSolver
61+
mkExprSolver.close()
62+
} else {
63+
mkExprSolverReferences[mkExprSolver] = referencesAfterDec
64+
}
65+
}
66+
67+
companion object {
68+
init {
69+
KCvc5SolverBase.ensureCvc5LibLoaded()
70+
}
71+
}
3072
}

‎ksmt-cvc5/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Model.kt‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -81,14 +81,18 @@ open class KCvc5Model(
8181
val cvc5InterpArgs = cvc5Interp.getChild(0).getChildren()
8282
val cvc5FreshVarsInterp = cvc5Interp.substitute(cvc5InterpArgs, cvc5Vars)
8383

84-
val defaultBody = cvc5FreshVarsInterp.getChild(1).convertExpr<T>()
84+
// in case of forking solver, save in cache mkExprSolver's terms
85+
val defaultBody = cvc5FreshVarsInterp.getChild(1).let {
86+
if (cvc5Ctx.isForking) it.convertExprWithMkExprSolver() else it.convertExpr<T>()
87+
}
8588

8689
KFuncInterpWithVars(decl, vars.map { it.decl }, emptyList(), defaultBody)
8790
}
8891

8992
private fun <T : KSort> constInterp(decl: KDecl<T>, const: Term): KFuncInterp<T> = with(converter) {
9093
val cvc5Interp = cvc5Ctx.nativeSolver.getValue(const)
91-
val interp = cvc5Interp.convertExpr<T>()
94+
// in case of forking solver, save in cache mkExprSolver's terms
95+
val interp = if (cvc5Ctx.isForking) cvc5Interp.convertExprWithMkExprSolver() else cvc5Interp.convertExpr<T>()
9296

9397
KFuncInterpVarsFree(decl = decl, entries = emptyList(), default = interp)
9498
}

0 commit comments

Comments
 (0)