Skip to content

Commit 837c567

Browse files
dee-treedee-tree
committed
bitwuzla - forking solver, scoped uninterpreted values tracking fix, yices - forking solver init exceptions wrapper, forking solver close fix,
all solvers - ScopedLinkedFrame.pop fix
1 parent 92a96da commit 837c567

File tree

12 files changed

+482
-211
lines changed

12 files changed

+482
-211
lines changed

‎ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaContext.kt‎

Lines changed: 14 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,5 @@
11
package io.ksmt.solver.bitwuzla
22

3-
import it.unimi.dsi.fastutil.longs.Long2ObjectOpenHashMap
4-
import it.unimi.dsi.fastutil.objects.Object2IntOpenHashMap
5-
import it.unimi.dsi.fastutil.objects.Object2LongOpenHashMap
63
import io.ksmt.KContext
74
import io.ksmt.decl.KDecl
85
import io.ksmt.decl.KFuncDecl
@@ -15,13 +12,10 @@ import io.ksmt.expr.KExistentialQuantifier
1512
import io.ksmt.expr.KExpr
1613
import io.ksmt.expr.KFunctionApp
1714
import io.ksmt.expr.KFunctionAsArray
15+
import io.ksmt.expr.KUninterpretedSortValue
1816
import io.ksmt.expr.KUniversalQuantifier
1917
import io.ksmt.expr.transformer.KNonRecursiveTransformer
2018
import io.ksmt.solver.KSolverException
21-
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaNativeException
22-
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaSort
23-
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaTerm
24-
import org.ksmt.solver.bitwuzla.bindings.Native
2519
import io.ksmt.solver.util.KExprLongInternalizerBase.Companion.NOT_INTERNALIZED
2620
import io.ksmt.sort.KArray2Sort
2721
import io.ksmt.sort.KArray3Sort
@@ -37,6 +31,13 @@ import io.ksmt.sort.KRealSort
3731
import io.ksmt.sort.KSort
3832
import io.ksmt.sort.KSortVisitor
3933
import io.ksmt.sort.KUninterpretedSort
34+
import it.unimi.dsi.fastutil.longs.Long2ObjectOpenHashMap
35+
import it.unimi.dsi.fastutil.objects.Object2IntOpenHashMap
36+
import it.unimi.dsi.fastutil.objects.Object2LongOpenHashMap
37+
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaNativeException
38+
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaSort
39+
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaTerm
40+
import org.ksmt.solver.bitwuzla.bindings.Native
4041

4142
open class KBitwuzlaContext(val ctx: KContext) : AutoCloseable {
4243
private var isClosed = false
@@ -433,6 +434,11 @@ open class KBitwuzlaContext(val ctx: KContext) : AutoCloseable {
433434
return super.transform(expr)
434435
}
435436

437+
override fun transform(expr: KUninterpretedSortValue): KExpr<KUninterpretedSort> {
438+
registerDeclIfNotIgnored(expr.decl)
439+
return super.transform(expr)
440+
}
441+
436442
private val quantifiedVarsScopeOwner = arrayListOf<KExpr<*>>()
437443
private val quantifiedVarsScope = arrayListOf<Set<KDecl<*>>?>()
438444

@@ -474,7 +480,7 @@ open class KBitwuzlaContext(val ctx: KContext) : AutoCloseable {
474480
override fun transform(expr: KExistentialQuantifier): KExpr<KBoolSort> =
475481
expr.transformQuantifier(expr.bounds, expr.body)
476482

477-
override fun transform(expr: KUniversalQuantifier): KExpr<KBoolSort> =
483+
override fun transform(expr: KUniversalQuantifier): KExpr<KBoolSort> =
478484
expr.transformQuantifier(expr.bounds, expr.body)
479485
}
480486

‎ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaForkingSolver.kt‎

Lines changed: 106 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,106 @@
1+
package io.ksmt.solver.bitwuzla
2+
3+
import io.ksmt.KContext
4+
import io.ksmt.expr.KExpr
5+
import io.ksmt.solver.KForkingSolver
6+
import io.ksmt.solver.KSolverStatus
7+
import io.ksmt.sort.KBoolSort
8+
import kotlin.time.Duration
9+
10+
class KBitwuzlaForkingSolver(
11+
private val ctx: KContext,
12+
private val manager: KBitwuzlaForkingSolverManager,
13+
parent: KBitwuzlaForkingSolver?
14+
) : KBitwuzlaSolverBase(ctx),
15+
KForkingSolver<KBitwuzlaSolverConfiguration> {
16+
17+
private val assertions = ScopedLinkedFrame<MutableList<KExpr<KBoolSort>>>(::ArrayList, ::ArrayList)
18+
private val trackToExprFrames =
19+
ScopedLinkedFrame<MutableList<Pair<KExpr<KBoolSort>, KExpr<KBoolSort>>>>(::ArrayList, ::ArrayList)
20+
21+
private val config: KBitwuzlaForkingSolverConfigurationImpl
22+
23+
init {
24+
if (parent != null) {
25+
config = parent.config.fork(bitwuzlaCtx.bitwuzla)
26+
assertions.fork(parent.assertions)
27+
trackToExprFrames.fork(parent.trackToExprFrames)
28+
} else {
29+
config = KBitwuzlaForkingSolverConfigurationImpl(bitwuzlaCtx.bitwuzla)
30+
}
31+
}
32+
33+
override fun configure(configurator: KBitwuzlaSolverConfiguration.() -> Unit) {
34+
config.configurator()
35+
}
36+
37+
override fun fork(): KForkingSolver<KBitwuzlaSolverConfiguration> = manager.mkForkingSolver(this)
38+
39+
private var assertionsInitiated = parent == null
40+
41+
private fun ensureAssertionsInitiated() {
42+
if (assertionsInitiated) return
43+
44+
assertions.stacked().zip(trackToExprFrames.stacked())
45+
.asReversed()
46+
.forEachIndexed { scope, (assertionsFrame, trackedExprsFrame) ->
47+
if (scope > 0) super.push()
48+
49+
assertionsFrame.forEach { assertion ->
50+
internalizeAndAssertWithAxioms(assertion)
51+
}
52+
53+
trackedExprsFrame.forEach { (track, trackedExpr) ->
54+
super.registerTrackForExpr(trackedExpr, track)
55+
}
56+
}
57+
assertionsInitiated = true
58+
}
59+
60+
override fun assert(expr: KExpr<KBoolSort>) = bitwuzlaCtx.bitwuzlaTry {
61+
ctx.ensureContextMatch(expr)
62+
ensureAssertionsInitiated()
63+
64+
internalizeAndAssertWithAxioms(expr)
65+
assertions.currentFrame += expr
66+
}
67+
68+
override fun assertAndTrack(expr: KExpr<KBoolSort>) {
69+
bitwuzlaCtx.bitwuzlaTry { ensureAssertionsInitiated() }
70+
super.assertAndTrack(expr)
71+
}
72+
73+
override fun registerTrackForExpr(expr: KExpr<KBoolSort>, track: KExpr<KBoolSort>) {
74+
super.registerTrackForExpr(expr, track)
75+
trackToExprFrames.currentFrame += track to expr
76+
}
77+
78+
override fun push() {
79+
bitwuzlaCtx.bitwuzlaTry { ensureAssertionsInitiated() }
80+
super.push()
81+
assertions.push()
82+
trackToExprFrames.push()
83+
}
84+
85+
override fun pop(n: UInt) {
86+
bitwuzlaCtx.bitwuzlaTry { ensureAssertionsInitiated() }
87+
super.pop(n)
88+
assertions.pop(n)
89+
trackToExprFrames.pop(n)
90+
}
91+
92+
override fun check(timeout: Duration): KSolverStatus {
93+
bitwuzlaCtx.bitwuzlaTry { ensureAssertionsInitiated() }
94+
return super.check(timeout)
95+
}
96+
97+
override fun checkWithAssumptions(assumptions: List<KExpr<KBoolSort>>, timeout: Duration): KSolverStatus {
98+
bitwuzlaCtx.bitwuzlaTry { ensureAssertionsInitiated() }
99+
return super.checkWithAssumptions(assumptions, timeout)
100+
}
101+
102+
override fun close() {
103+
super.close()
104+
manager.close(this)
105+
}
106+
}

‎ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaForkingSolverManager.kt‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
package io.ksmt.solver.bitwuzla
2+
3+
import io.ksmt.KContext
4+
import io.ksmt.solver.KForkingSolver
5+
import io.ksmt.solver.KForkingSolverManager
6+
import java.util.concurrent.ConcurrentHashMap
7+
8+
class KBitwuzlaForkingSolverManager(private val ctx: KContext) : KForkingSolverManager<KBitwuzlaSolverConfiguration> {
9+
private val solvers = ConcurrentHashMap.newKeySet<KBitwuzlaForkingSolver>()
10+
11+
override fun mkForkingSolver(): KForkingSolver<KBitwuzlaSolverConfiguration> {
12+
return KBitwuzlaForkingSolver(ctx, this, null).also {
13+
solvers += it
14+
}
15+
}
16+
17+
internal fun mkForkingSolver(parent: KBitwuzlaForkingSolver) = KBitwuzlaForkingSolver(ctx, this, parent).also {
18+
solvers += it
19+
}
20+
21+
internal fun close(solver: KBitwuzlaForkingSolver) {
22+
solvers -= solver
23+
}
24+
25+
override fun close() {
26+
solvers.forEach(KBitwuzlaForkingSolver::close)
27+
}
28+
}

‎ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaSolver.kt‎

Lines changed: 1 addition & 190 deletions
Original file line numberDiff line numberDiff line change
@@ -1,199 +1,10 @@
11
package io.ksmt.solver.bitwuzla
22

3-
import it.unimi.dsi.fastutil.longs.LongOpenHashSet
43
import io.ksmt.KContext
5-
import io.ksmt.expr.KExpr
6-
import io.ksmt.solver.KModel
7-
import io.ksmt.solver.KSolver
8-
import io.ksmt.solver.KSolverStatus
9-
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaNativeException
10-
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaOption
11-
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaResult
12-
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaTerm
13-
import org.ksmt.solver.bitwuzla.bindings.BitwuzlaTermArray
14-
import org.ksmt.solver.bitwuzla.bindings.Native
15-
import io.ksmt.sort.KBoolSort
16-
import kotlin.time.Duration
174

18-
open class KBitwuzlaSolver(private val ctx: KContext) : KSolver<KBitwuzlaSolverConfiguration> {
19-
open val bitwuzlaCtx = KBitwuzlaContext(ctx)
20-
open val exprInternalizer: KBitwuzlaExprInternalizer by lazy {
21-
KBitwuzlaExprInternalizer(bitwuzlaCtx)
22-
}
23-
open val exprConverter: KBitwuzlaExprConverter by lazy {
24-
KBitwuzlaExprConverter(ctx, bitwuzlaCtx)
25-
}
26-
27-
private var lastCheckStatus = KSolverStatus.UNKNOWN
28-
private var lastReasonOfUnknown: String? = null
29-
private var lastAssumptions: TrackedAssumptions? = null
30-
private var lastModel: KBitwuzlaModel? = null
31-
32-
init {
33-
Native.bitwuzlaSetOption(bitwuzlaCtx.bitwuzla, BitwuzlaOption.BITWUZLA_OPT_INCREMENTAL, value = 1)
34-
Native.bitwuzlaSetOption(bitwuzlaCtx.bitwuzla, BitwuzlaOption.BITWUZLA_OPT_PRODUCE_MODELS, value = 1)
35-
}
36-
37-
private var trackedAssertions = mutableListOf<Pair<KExpr<KBoolSort>, BitwuzlaTerm>>()
38-
private val trackVarsAssertionFrames = arrayListOf(trackedAssertions)
5+
open class KBitwuzlaSolver(ctx: KContext) : KBitwuzlaSolverBase(ctx) {
396

407
override fun configure(configurator: KBitwuzlaSolverConfiguration.() -> Unit) {
418
KBitwuzlaSolverConfigurationImpl(bitwuzlaCtx.bitwuzla).configurator()
429
}
43-
44-
override fun assert(expr: KExpr<KBoolSort>) = bitwuzlaCtx.bitwuzlaTry {
45-
ctx.ensureContextMatch(expr)
46-
47-
val assertionWithAxioms = with(exprInternalizer) { expr.internalizeAssertion() }
48-
49-
assertionWithAxioms.axioms.forEach {
50-
Native.bitwuzlaAssert(bitwuzlaCtx.bitwuzla, it)
51-
}
52-
Native.bitwuzlaAssert(bitwuzlaCtx.bitwuzla, assertionWithAxioms.assertion)
53-
}
54-
55-
override fun assertAndTrack(expr: KExpr<KBoolSort>) = bitwuzlaCtx.bitwuzlaTry {
56-
ctx.ensureContextMatch(expr)
57-
58-
val trackVarExpr = ctx.mkFreshConst("track", ctx.boolSort)
59-
val trackedExpr = with(ctx) { !trackVarExpr or expr }
60-
61-
assert(trackedExpr)
62-
63-
val trackVarTerm = with(exprInternalizer) { trackVarExpr.internalize() }
64-
trackedAssertions += expr to trackVarTerm
65-
}
66-
67-
override fun push(): Unit = bitwuzlaCtx.bitwuzlaTry {
68-
Native.bitwuzlaPush(bitwuzlaCtx.bitwuzla, nlevels = 1)
69-
70-
trackedAssertions = trackedAssertions.toMutableList()
71-
trackVarsAssertionFrames.add(trackedAssertions)
72-
73-
bitwuzlaCtx.createNestedDeclarationScope()
74-
}
75-
76-
override fun pop(n: UInt): Unit = bitwuzlaCtx.bitwuzlaTry {
77-
val currentLevel = trackVarsAssertionFrames.lastIndex.toUInt()
78-
require(n <= currentLevel) {
79-
"Cannot pop $n scope levels because current scope level is $currentLevel"
80-
}
81-
82-
if (n == 0u) return
83-
84-
repeat(n.toInt()) {
85-
trackVarsAssertionFrames.removeLast()
86-
bitwuzlaCtx.popDeclarationScope()
87-
}
88-
89-
trackedAssertions = trackVarsAssertionFrames.last()
90-
91-
Native.bitwuzlaPop(bitwuzlaCtx.bitwuzla, n.toInt())
92-
}
93-
94-
override fun check(timeout: Duration): KSolverStatus =
95-
checkWithAssumptions(emptyList(), timeout)
96-
97-
override fun checkWithAssumptions(assumptions: List<KExpr<KBoolSort>>, timeout: Duration): KSolverStatus =
98-
bitwuzlaTryCheck {
99-
ctx.ensureContextMatch(assumptions)
100-
101-
val currentAssumptions = TrackedAssumptions().also { lastAssumptions = it }
102-
103-
trackedAssertions.forEach {
104-
currentAssumptions.assumeTrackedAssertion(it)
105-
}
106-
107-
with(exprInternalizer) {
108-
assumptions.forEach {
109-
currentAssumptions.assumeAssumption(it, it.internalize())
110-
}
111-
}
112-
113-
checkWithTimeout(timeout).processCheckResult()
114-
}
115-
116-
private fun checkWithTimeout(timeout: Duration): BitwuzlaResult = if (timeout.isInfinite()) {
117-
Native.bitwuzlaCheckSatResult(bitwuzlaCtx.bitwuzla)
118-
} else {
119-
Native.bitwuzlaCheckSatTimeoutResult(bitwuzlaCtx.bitwuzla, timeout.inWholeMilliseconds)
120-
}
121-
122-
override fun model(): KModel = bitwuzlaCtx.bitwuzlaTry {
123-
require(lastCheckStatus == KSolverStatus.SAT) { "Model are only available after SAT checks" }
124-
val model = lastModel ?: KBitwuzlaModel(
125-
ctx, bitwuzlaCtx, exprConverter,
126-
bitwuzlaCtx.declarations(),
127-
bitwuzlaCtx.uninterpretedSortsWithRelevantDecls()
128-
)
129-
lastModel = model
130-
model
131-
}
132-
133-
override fun unsatCore(): List<KExpr<KBoolSort>> = bitwuzlaCtx.bitwuzlaTry {
134-
require(lastCheckStatus == KSolverStatus.UNSAT) { "Unsat cores are only available after UNSAT checks" }
135-
val unsatAssumptions = Native.bitwuzlaGetUnsatAssumptions(bitwuzlaCtx.bitwuzla)
136-
lastAssumptions?.resolveUnsatCore(unsatAssumptions) ?: emptyList()
137-
}
138-
139-
override fun reasonOfUnknown(): String = bitwuzlaCtx.bitwuzlaTry {
140-
require(lastCheckStatus == KSolverStatus.UNKNOWN) {
141-
"Unknown reason is only available after UNKNOWN checks"
142-
}
143-
144-
// There is no way to retrieve reason of unknown from Bitwuzla in general case.
145-
return lastReasonOfUnknown ?: "unknown"
146-
}
147-
148-
override fun interrupt() = bitwuzlaCtx.bitwuzlaTry {
149-
Native.bitwuzlaForceTerminate(bitwuzlaCtx.bitwuzla)
150-
}
151-
152-
override fun close() = bitwuzlaCtx.bitwuzlaTry {
153-
bitwuzlaCtx.close()
154-
}
155-
156-
private fun BitwuzlaResult.processCheckResult() = when (this) {
157-
BitwuzlaResult.BITWUZLA_SAT -> KSolverStatus.SAT
158-
BitwuzlaResult.BITWUZLA_UNSAT -> KSolverStatus.UNSAT
159-
BitwuzlaResult.BITWUZLA_UNKNOWN -> KSolverStatus.UNKNOWN
160-
}.also { lastCheckStatus = it }
161-
162-
private fun invalidateSolverState() {
163-
/**
164-
* Bitwuzla model is only valid until the next check-sat call.
165-
* */
166-
lastModel?.markInvalid()
167-
lastModel = null
168-
169-
lastCheckStatus = KSolverStatus.UNKNOWN
170-
lastReasonOfUnknown = null
171-
172-
lastAssumptions = null
173-
}
174-
175-
private inline fun bitwuzlaTryCheck(body: () -> KSolverStatus): KSolverStatus = try {
176-
invalidateSolverState()
177-
body()
178-
} catch (ex: BitwuzlaNativeException) {
179-
lastReasonOfUnknown = ex.message
180-
KSolverStatus.UNKNOWN.also { lastCheckStatus = it }
181-
}
182-
183-
private inner class TrackedAssumptions {
184-
private val assumedExprs = arrayListOf<Pair<KExpr<KBoolSort>, BitwuzlaTerm>>()
185-
186-
fun assumeTrackedAssertion(trackedAssertion: Pair<KExpr<KBoolSort>, BitwuzlaTerm>) {
187-
assumedExprs.add(trackedAssertion)
188-
Native.bitwuzlaAssume(bitwuzlaCtx.bitwuzla, trackedAssertion.second)
189-
}
190-
191-
fun assumeAssumption(expr: KExpr<KBoolSort>, term: BitwuzlaTerm) =
192-
assumeTrackedAssertion(expr to term)
193-
194-
fun resolveUnsatCore(unsatAssumptions: BitwuzlaTermArray): List<KExpr<KBoolSort>> {
195-
val unsatCoreTerms = LongOpenHashSet(unsatAssumptions)
196-
return assumedExprs.mapNotNull { (expr, term) -> expr.takeIf { unsatCoreTerms.contains(term) } }
197-
}
198-
}
19910
}

0 commit comments

Comments
 (0)