-
Notifications
You must be signed in to change notification settings - Fork 14
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
bitwuzla - forking solver, scoped uninterpreted values tracking fix, …
…yices - forking solver init exceptions wrapper, forking solver close fix, all solvers - ScopedLinkedFrame.pop fix
- Loading branch information
Showing
12 changed files
with
482 additions
and
211 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
106 changes: 106 additions & 0 deletions
106
ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaForkingSolver.kt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,106 @@ | ||
| package io.ksmt.solver.bitwuzla | ||
|
|
||
| import io.ksmt.KContext | ||
| import io.ksmt.expr.KExpr | ||
| import io.ksmt.solver.KForkingSolver | ||
| import io.ksmt.solver.KSolverStatus | ||
| import io.ksmt.sort.KBoolSort | ||
| import kotlin.time.Duration | ||
|
|
||
| class KBitwuzlaForkingSolver( | ||
| private val ctx: KContext, | ||
| private val manager: KBitwuzlaForkingSolverManager, | ||
| parent: KBitwuzlaForkingSolver? | ||
| ) : KBitwuzlaSolverBase(ctx), | ||
| KForkingSolver<KBitwuzlaSolverConfiguration> { | ||
|
|
||
| private val assertions = ScopedLinkedFrame<MutableList<KExpr<KBoolSort>>>(::ArrayList, ::ArrayList) | ||
| private val trackToExprFrames = | ||
| ScopedLinkedFrame<MutableList<Pair<KExpr<KBoolSort>, KExpr<KBoolSort>>>>(::ArrayList, ::ArrayList) | ||
|
|
||
| private val config: KBitwuzlaForkingSolverConfigurationImpl | ||
|
|
||
| init { | ||
| if (parent != null) { | ||
| config = parent.config.fork(bitwuzlaCtx.bitwuzla) | ||
| assertions.fork(parent.assertions) | ||
| trackToExprFrames.fork(parent.trackToExprFrames) | ||
| } else { | ||
| config = KBitwuzlaForkingSolverConfigurationImpl(bitwuzlaCtx.bitwuzla) | ||
| } | ||
| } | ||
|
|
||
| override fun configure(configurator: KBitwuzlaSolverConfiguration.() -> Unit) { | ||
| config.configurator() | ||
| } | ||
|
|
||
| override fun fork(): KForkingSolver<KBitwuzlaSolverConfiguration> = manager.mkForkingSolver(this) | ||
|
|
||
| private var assertionsInitiated = parent == null | ||
|
|
||
| private fun ensureAssertionsInitiated() { | ||
| if (assertionsInitiated) return | ||
|
|
||
| assertions.stacked().zip(trackToExprFrames.stacked()) | ||
| .asReversed() | ||
| .forEachIndexed { scope, (assertionsFrame, trackedExprsFrame) -> | ||
| if (scope > 0) super.push() | ||
|
|
||
| assertionsFrame.forEach { assertion -> | ||
| internalizeAndAssertWithAxioms(assertion) | ||
| } | ||
|
|
||
| trackedExprsFrame.forEach { (track, trackedExpr) -> | ||
| super.registerTrackForExpr(trackedExpr, track) | ||
| } | ||
| } | ||
| assertionsInitiated = true | ||
| } | ||
|
|
||
| override fun assert(expr: KExpr<KBoolSort>) = bitwuzlaCtx.bitwuzlaTry { | ||
| ctx.ensureContextMatch(expr) | ||
| ensureAssertionsInitiated() | ||
|
|
||
| internalizeAndAssertWithAxioms(expr) | ||
| assertions.currentFrame += expr | ||
| } | ||
|
|
||
| override fun assertAndTrack(expr: KExpr<KBoolSort>) { | ||
| bitwuzlaCtx.bitwuzlaTry { ensureAssertionsInitiated() } | ||
| super.assertAndTrack(expr) | ||
| } | ||
|
|
||
| override fun registerTrackForExpr(expr: KExpr<KBoolSort>, track: KExpr<KBoolSort>) { | ||
| super.registerTrackForExpr(expr, track) | ||
| trackToExprFrames.currentFrame += track to expr | ||
| } | ||
|
|
||
| override fun push() { | ||
| bitwuzlaCtx.bitwuzlaTry { ensureAssertionsInitiated() } | ||
| super.push() | ||
| assertions.push() | ||
| trackToExprFrames.push() | ||
| } | ||
|
|
||
| override fun pop(n: UInt) { | ||
| bitwuzlaCtx.bitwuzlaTry { ensureAssertionsInitiated() } | ||
| super.pop(n) | ||
| assertions.pop(n) | ||
| trackToExprFrames.pop(n) | ||
| } | ||
|
|
||
| override fun check(timeout: Duration): KSolverStatus { | ||
| bitwuzlaCtx.bitwuzlaTry { ensureAssertionsInitiated() } | ||
| return super.check(timeout) | ||
| } | ||
|
|
||
| override fun checkWithAssumptions(assumptions: List<KExpr<KBoolSort>>, timeout: Duration): KSolverStatus { | ||
| bitwuzlaCtx.bitwuzlaTry { ensureAssertionsInitiated() } | ||
| return super.checkWithAssumptions(assumptions, timeout) | ||
| } | ||
|
|
||
| override fun close() { | ||
| super.close() | ||
| manager.close(this) | ||
| } | ||
| } |
28 changes: 28 additions & 0 deletions
28
ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaForkingSolverManager.kt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,28 @@ | ||
| package io.ksmt.solver.bitwuzla | ||
|
|
||
| import io.ksmt.KContext | ||
| import io.ksmt.solver.KForkingSolver | ||
| import io.ksmt.solver.KForkingSolverManager | ||
| import java.util.concurrent.ConcurrentHashMap | ||
|
|
||
| class KBitwuzlaForkingSolverManager(private val ctx: KContext) : KForkingSolverManager<KBitwuzlaSolverConfiguration> { | ||
| private val solvers = ConcurrentHashMap.newKeySet<KBitwuzlaForkingSolver>() | ||
|
|
||
| override fun mkForkingSolver(): KForkingSolver<KBitwuzlaSolverConfiguration> { | ||
| return KBitwuzlaForkingSolver(ctx, this, null).also { | ||
| solvers += it | ||
| } | ||
| } | ||
|
|
||
| internal fun mkForkingSolver(parent: KBitwuzlaForkingSolver) = KBitwuzlaForkingSolver(ctx, this, parent).also { | ||
| solvers += it | ||
| } | ||
|
|
||
| internal fun close(solver: KBitwuzlaForkingSolver) { | ||
| solvers -= solver | ||
| } | ||
|
|
||
| override fun close() { | ||
| solvers.forEach(KBitwuzlaForkingSolver::close) | ||
| } | ||
| } |
191 changes: 1 addition & 190 deletions
191
ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaSolver.kt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,199 +1,10 @@ | ||
| package io.ksmt.solver.bitwuzla | ||
|
|
||
| import it.unimi.dsi.fastutil.longs.LongOpenHashSet | ||
| import io.ksmt.KContext | ||
| import io.ksmt.expr.KExpr | ||
| import io.ksmt.solver.KModel | ||
| import io.ksmt.solver.KSolver | ||
| import io.ksmt.solver.KSolverStatus | ||
| import org.ksmt.solver.bitwuzla.bindings.BitwuzlaNativeException | ||
| import org.ksmt.solver.bitwuzla.bindings.BitwuzlaOption | ||
| import org.ksmt.solver.bitwuzla.bindings.BitwuzlaResult | ||
| import org.ksmt.solver.bitwuzla.bindings.BitwuzlaTerm | ||
| import org.ksmt.solver.bitwuzla.bindings.BitwuzlaTermArray | ||
| import org.ksmt.solver.bitwuzla.bindings.Native | ||
| import io.ksmt.sort.KBoolSort | ||
| import kotlin.time.Duration | ||
|
|
||
| open class KBitwuzlaSolver(private val ctx: KContext) : KSolver<KBitwuzlaSolverConfiguration> { | ||
| open val bitwuzlaCtx = KBitwuzlaContext(ctx) | ||
| open val exprInternalizer: KBitwuzlaExprInternalizer by lazy { | ||
| KBitwuzlaExprInternalizer(bitwuzlaCtx) | ||
| } | ||
| open val exprConverter: KBitwuzlaExprConverter by lazy { | ||
| KBitwuzlaExprConverter(ctx, bitwuzlaCtx) | ||
| } | ||
|
|
||
| private var lastCheckStatus = KSolverStatus.UNKNOWN | ||
| private var lastReasonOfUnknown: String? = null | ||
| private var lastAssumptions: TrackedAssumptions? = null | ||
| private var lastModel: KBitwuzlaModel? = null | ||
|
|
||
| init { | ||
| Native.bitwuzlaSetOption(bitwuzlaCtx.bitwuzla, BitwuzlaOption.BITWUZLA_OPT_INCREMENTAL, value = 1) | ||
| Native.bitwuzlaSetOption(bitwuzlaCtx.bitwuzla, BitwuzlaOption.BITWUZLA_OPT_PRODUCE_MODELS, value = 1) | ||
| } | ||
|
|
||
| private var trackedAssertions = mutableListOf<Pair<KExpr<KBoolSort>, BitwuzlaTerm>>() | ||
| private val trackVarsAssertionFrames = arrayListOf(trackedAssertions) | ||
| open class KBitwuzlaSolver(ctx: KContext) : KBitwuzlaSolverBase(ctx) { | ||
|
|
||
| override fun configure(configurator: KBitwuzlaSolverConfiguration.() -> Unit) { | ||
| KBitwuzlaSolverConfigurationImpl(bitwuzlaCtx.bitwuzla).configurator() | ||
| } | ||
|
|
||
| override fun assert(expr: KExpr<KBoolSort>) = bitwuzlaCtx.bitwuzlaTry { | ||
| ctx.ensureContextMatch(expr) | ||
|
|
||
| val assertionWithAxioms = with(exprInternalizer) { expr.internalizeAssertion() } | ||
|
|
||
| assertionWithAxioms.axioms.forEach { | ||
| Native.bitwuzlaAssert(bitwuzlaCtx.bitwuzla, it) | ||
| } | ||
| Native.bitwuzlaAssert(bitwuzlaCtx.bitwuzla, assertionWithAxioms.assertion) | ||
| } | ||
|
|
||
| override fun assertAndTrack(expr: KExpr<KBoolSort>) = bitwuzlaCtx.bitwuzlaTry { | ||
| ctx.ensureContextMatch(expr) | ||
|
|
||
| val trackVarExpr = ctx.mkFreshConst("track", ctx.boolSort) | ||
| val trackedExpr = with(ctx) { !trackVarExpr or expr } | ||
|
|
||
| assert(trackedExpr) | ||
|
|
||
| val trackVarTerm = with(exprInternalizer) { trackVarExpr.internalize() } | ||
| trackedAssertions += expr to trackVarTerm | ||
| } | ||
|
|
||
| override fun push(): Unit = bitwuzlaCtx.bitwuzlaTry { | ||
| Native.bitwuzlaPush(bitwuzlaCtx.bitwuzla, nlevels = 1) | ||
|
|
||
| trackedAssertions = trackedAssertions.toMutableList() | ||
| trackVarsAssertionFrames.add(trackedAssertions) | ||
|
|
||
| bitwuzlaCtx.createNestedDeclarationScope() | ||
| } | ||
|
|
||
| override fun pop(n: UInt): Unit = bitwuzlaCtx.bitwuzlaTry { | ||
| val currentLevel = trackVarsAssertionFrames.lastIndex.toUInt() | ||
| require(n <= currentLevel) { | ||
| "Cannot pop $n scope levels because current scope level is $currentLevel" | ||
| } | ||
|
|
||
| if (n == 0u) return | ||
|
|
||
| repeat(n.toInt()) { | ||
| trackVarsAssertionFrames.removeLast() | ||
| bitwuzlaCtx.popDeclarationScope() | ||
| } | ||
|
|
||
| trackedAssertions = trackVarsAssertionFrames.last() | ||
|
|
||
| Native.bitwuzlaPop(bitwuzlaCtx.bitwuzla, n.toInt()) | ||
| } | ||
|
|
||
| override fun check(timeout: Duration): KSolverStatus = | ||
| checkWithAssumptions(emptyList(), timeout) | ||
|
|
||
| override fun checkWithAssumptions(assumptions: List<KExpr<KBoolSort>>, timeout: Duration): KSolverStatus = | ||
| bitwuzlaTryCheck { | ||
| ctx.ensureContextMatch(assumptions) | ||
|
|
||
| val currentAssumptions = TrackedAssumptions().also { lastAssumptions = it } | ||
|
|
||
| trackedAssertions.forEach { | ||
| currentAssumptions.assumeTrackedAssertion(it) | ||
| } | ||
|
|
||
| with(exprInternalizer) { | ||
| assumptions.forEach { | ||
| currentAssumptions.assumeAssumption(it, it.internalize()) | ||
| } | ||
| } | ||
|
|
||
| checkWithTimeout(timeout).processCheckResult() | ||
| } | ||
|
|
||
| private fun checkWithTimeout(timeout: Duration): BitwuzlaResult = if (timeout.isInfinite()) { | ||
| Native.bitwuzlaCheckSatResult(bitwuzlaCtx.bitwuzla) | ||
| } else { | ||
| Native.bitwuzlaCheckSatTimeoutResult(bitwuzlaCtx.bitwuzla, timeout.inWholeMilliseconds) | ||
| } | ||
|
|
||
| override fun model(): KModel = bitwuzlaCtx.bitwuzlaTry { | ||
| require(lastCheckStatus == KSolverStatus.SAT) { "Model are only available after SAT checks" } | ||
| val model = lastModel ?: KBitwuzlaModel( | ||
| ctx, bitwuzlaCtx, exprConverter, | ||
| bitwuzlaCtx.declarations(), | ||
| bitwuzlaCtx.uninterpretedSortsWithRelevantDecls() | ||
| ) | ||
| lastModel = model | ||
| model | ||
| } | ||
|
|
||
| override fun unsatCore(): List<KExpr<KBoolSort>> = bitwuzlaCtx.bitwuzlaTry { | ||
| require(lastCheckStatus == KSolverStatus.UNSAT) { "Unsat cores are only available after UNSAT checks" } | ||
| val unsatAssumptions = Native.bitwuzlaGetUnsatAssumptions(bitwuzlaCtx.bitwuzla) | ||
| lastAssumptions?.resolveUnsatCore(unsatAssumptions) ?: emptyList() | ||
| } | ||
|
|
||
| override fun reasonOfUnknown(): String = bitwuzlaCtx.bitwuzlaTry { | ||
| require(lastCheckStatus == KSolverStatus.UNKNOWN) { | ||
| "Unknown reason is only available after UNKNOWN checks" | ||
| } | ||
|
|
||
| // There is no way to retrieve reason of unknown from Bitwuzla in general case. | ||
| return lastReasonOfUnknown ?: "unknown" | ||
| } | ||
|
|
||
| override fun interrupt() = bitwuzlaCtx.bitwuzlaTry { | ||
| Native.bitwuzlaForceTerminate(bitwuzlaCtx.bitwuzla) | ||
| } | ||
|
|
||
| override fun close() = bitwuzlaCtx.bitwuzlaTry { | ||
| bitwuzlaCtx.close() | ||
| } | ||
|
|
||
| private fun BitwuzlaResult.processCheckResult() = when (this) { | ||
| BitwuzlaResult.BITWUZLA_SAT -> KSolverStatus.SAT | ||
| BitwuzlaResult.BITWUZLA_UNSAT -> KSolverStatus.UNSAT | ||
| BitwuzlaResult.BITWUZLA_UNKNOWN -> KSolverStatus.UNKNOWN | ||
| }.also { lastCheckStatus = it } | ||
|
|
||
| private fun invalidateSolverState() { | ||
| /** | ||
| * Bitwuzla model is only valid until the next check-sat call. | ||
| * */ | ||
| lastModel?.markInvalid() | ||
| lastModel = null | ||
|
|
||
| lastCheckStatus = KSolverStatus.UNKNOWN | ||
| lastReasonOfUnknown = null | ||
|
|
||
| lastAssumptions = null | ||
| } | ||
|
|
||
| private inline fun bitwuzlaTryCheck(body: () -> KSolverStatus): KSolverStatus = try { | ||
| invalidateSolverState() | ||
| body() | ||
| } catch (ex: BitwuzlaNativeException) { | ||
| lastReasonOfUnknown = ex.message | ||
| KSolverStatus.UNKNOWN.also { lastCheckStatus = it } | ||
| } | ||
|
|
||
| private inner class TrackedAssumptions { | ||
| private val assumedExprs = arrayListOf<Pair<KExpr<KBoolSort>, BitwuzlaTerm>>() | ||
|
|
||
| fun assumeTrackedAssertion(trackedAssertion: Pair<KExpr<KBoolSort>, BitwuzlaTerm>) { | ||
| assumedExprs.add(trackedAssertion) | ||
| Native.bitwuzlaAssume(bitwuzlaCtx.bitwuzla, trackedAssertion.second) | ||
| } | ||
|
|
||
| fun assumeAssumption(expr: KExpr<KBoolSort>, term: BitwuzlaTerm) = | ||
| assumeTrackedAssertion(expr to term) | ||
|
|
||
| fun resolveUnsatCore(unsatAssumptions: BitwuzlaTermArray): List<KExpr<KBoolSort>> { | ||
| val unsatCoreTerms = LongOpenHashSet(unsatAssumptions) | ||
| return assumedExprs.mapNotNull { (expr, term) -> expr.takeIf { unsatCoreTerms.contains(term) } } | ||
| } | ||
| } | ||
| } |
Oops, something went wrong.