diff --git a/ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaContext.kt b/ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaContext.kt index 5fb618e35..5b845795c 100644 --- a/ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaContext.kt +++ b/ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaContext.kt @@ -1,8 +1,5 @@ package io.ksmt.solver.bitwuzla -import it.unimi.dsi.fastutil.longs.Long2ObjectOpenHashMap -import it.unimi.dsi.fastutil.objects.Object2IntOpenHashMap -import it.unimi.dsi.fastutil.objects.Object2LongOpenHashMap import io.ksmt.KContext import io.ksmt.decl.KDecl import io.ksmt.decl.KFuncDecl @@ -15,13 +12,10 @@ import io.ksmt.expr.KExistentialQuantifier import io.ksmt.expr.KExpr import io.ksmt.expr.KFunctionApp import io.ksmt.expr.KFunctionAsArray +import io.ksmt.expr.KUninterpretedSortValue import io.ksmt.expr.KUniversalQuantifier import io.ksmt.expr.transformer.KNonRecursiveTransformer import io.ksmt.solver.KSolverException -import org.ksmt.solver.bitwuzla.bindings.BitwuzlaNativeException -import org.ksmt.solver.bitwuzla.bindings.BitwuzlaSort -import org.ksmt.solver.bitwuzla.bindings.BitwuzlaTerm -import org.ksmt.solver.bitwuzla.bindings.Native import io.ksmt.solver.util.KExprLongInternalizerBase.Companion.NOT_INTERNALIZED import io.ksmt.sort.KArray2Sort import io.ksmt.sort.KArray3Sort @@ -37,6 +31,13 @@ import io.ksmt.sort.KRealSort import io.ksmt.sort.KSort import io.ksmt.sort.KSortVisitor import io.ksmt.sort.KUninterpretedSort +import it.unimi.dsi.fastutil.longs.Long2ObjectOpenHashMap +import it.unimi.dsi.fastutil.objects.Object2IntOpenHashMap +import it.unimi.dsi.fastutil.objects.Object2LongOpenHashMap +import org.ksmt.solver.bitwuzla.bindings.BitwuzlaNativeException +import org.ksmt.solver.bitwuzla.bindings.BitwuzlaSort +import org.ksmt.solver.bitwuzla.bindings.BitwuzlaTerm +import org.ksmt.solver.bitwuzla.bindings.Native open class KBitwuzlaContext(val ctx: KContext) : AutoCloseable { private var isClosed = false @@ -433,6 +434,11 @@ open class KBitwuzlaContext(val ctx: KContext) : AutoCloseable { return super.transform(expr) } + override fun transform(expr: KUninterpretedSortValue): KExpr { + registerDeclIfNotIgnored(expr.decl) + return super.transform(expr) + } + private val quantifiedVarsScopeOwner = arrayListOf>() private val quantifiedVarsScope = arrayListOf>?>() @@ -474,7 +480,7 @@ open class KBitwuzlaContext(val ctx: KContext) : AutoCloseable { override fun transform(expr: KExistentialQuantifier): KExpr = expr.transformQuantifier(expr.bounds, expr.body) - override fun transform(expr: KUniversalQuantifier): KExpr = + override fun transform(expr: KUniversalQuantifier): KExpr = expr.transformQuantifier(expr.bounds, expr.body) } diff --git a/ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaForkingSolver.kt b/ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaForkingSolver.kt new file mode 100644 index 000000000..845296cb3 --- /dev/null +++ b/ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaForkingSolver.kt @@ -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 { + + private val assertions = ScopedLinkedFrame>>(::ArrayList, ::ArrayList) + private val trackToExprFrames = + ScopedLinkedFrame, KExpr>>>(::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 = 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) = bitwuzlaCtx.bitwuzlaTry { + ctx.ensureContextMatch(expr) + ensureAssertionsInitiated() + + internalizeAndAssertWithAxioms(expr) + assertions.currentFrame += expr + } + + override fun assertAndTrack(expr: KExpr) { + bitwuzlaCtx.bitwuzlaTry { ensureAssertionsInitiated() } + super.assertAndTrack(expr) + } + + override fun registerTrackForExpr(expr: KExpr, track: KExpr) { + 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>, timeout: Duration): KSolverStatus { + bitwuzlaCtx.bitwuzlaTry { ensureAssertionsInitiated() } + return super.checkWithAssumptions(assumptions, timeout) + } + + override fun close() { + super.close() + manager.close(this) + } +} diff --git a/ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaForkingSolverManager.kt b/ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaForkingSolverManager.kt new file mode 100644 index 000000000..b941e94ec --- /dev/null +++ b/ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaForkingSolverManager.kt @@ -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 { + private val solvers = ConcurrentHashMap.newKeySet() + + override fun mkForkingSolver(): KForkingSolver { + 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) + } +} diff --git a/ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaSolver.kt b/ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaSolver.kt index 5d86b25b9..30c0b0f71 100644 --- a/ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaSolver.kt +++ b/ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaSolver.kt @@ -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 { - 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, 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) = 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) = 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>, 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> = 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, BitwuzlaTerm>>() - - fun assumeTrackedAssertion(trackedAssertion: Pair, BitwuzlaTerm>) { - assumedExprs.add(trackedAssertion) - Native.bitwuzlaAssume(bitwuzlaCtx.bitwuzla, trackedAssertion.second) - } - - fun assumeAssumption(expr: KExpr, term: BitwuzlaTerm) = - assumeTrackedAssertion(expr to term) - - fun resolveUnsatCore(unsatAssumptions: BitwuzlaTermArray): List> { - val unsatCoreTerms = LongOpenHashSet(unsatAssumptions) - return assumedExprs.mapNotNull { (expr, term) -> expr.takeIf { unsatCoreTerms.contains(term) } } - } - } } diff --git a/ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaSolverBase.kt b/ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaSolverBase.kt new file mode 100644 index 000000000..fa8ae269b --- /dev/null +++ b/ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaSolverBase.kt @@ -0,0 +1,201 @@ +package io.ksmt.solver.bitwuzla + +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 io.ksmt.sort.KBoolSort +import it.unimi.dsi.fastutil.longs.LongOpenHashSet +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 kotlin.time.Duration + +abstract class KBitwuzlaSolverBase(private val ctx: KContext) : KSolver { + 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, BitwuzlaTerm>>() + private val trackVarsAssertionFrames = arrayListOf(trackedAssertions) + + protected fun internalizeAndAssertWithAxioms(expr: KExpr) { + val assertionWithAxioms = with(exprInternalizer) { expr.internalizeAssertion() } + + assertionWithAxioms.axioms.forEach { + Native.bitwuzlaAssert(bitwuzlaCtx.bitwuzla, it) + } + Native.bitwuzlaAssert(bitwuzlaCtx.bitwuzla, assertionWithAxioms.assertion) + } + + override fun assert(expr: KExpr) = bitwuzlaCtx.bitwuzlaTry { + ctx.ensureContextMatch(expr) + internalizeAndAssertWithAxioms(expr) + } + + protected open fun registerTrackForExpr(expr: KExpr, track: KExpr) { + val trackVarTerm = with(exprInternalizer) { track.internalize() } + trackedAssertions += expr to trackVarTerm + } + + override fun assertAndTrack(expr: KExpr) = bitwuzlaCtx.bitwuzlaTry { + ctx.ensureContextMatch(expr) + + val trackVarExpr = ctx.mkFreshConst("track", ctx.boolSort) + val trackedExpr = with(ctx) { !trackVarExpr or expr } + + assert(trackedExpr) + registerTrackForExpr(expr, trackVarExpr) + } + + 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>, 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() + } + + protected 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> = 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() + } + + protected 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, BitwuzlaTerm>>() + + fun assumeTrackedAssertion(trackedAssertion: Pair, BitwuzlaTerm>) { + assumedExprs.add(trackedAssertion) + Native.bitwuzlaAssume(bitwuzlaCtx.bitwuzla, trackedAssertion.second) + } + + fun assumeAssumption(expr: KExpr, term: BitwuzlaTerm) = + assumeTrackedAssertion(expr to term) + + fun resolveUnsatCore(unsatAssumptions: BitwuzlaTermArray): List> { + val unsatCoreTerms = LongOpenHashSet(unsatAssumptions) + return assumedExprs.mapNotNull { (expr, term) -> expr.takeIf { unsatCoreTerms.contains(term) } } + } + } +} diff --git a/ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaSolverConfiguration.kt b/ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaSolverConfiguration.kt index a40ee8a60..5ee777c8f 100644 --- a/ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaSolverConfiguration.kt +++ b/ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaSolverConfiguration.kt @@ -6,6 +6,7 @@ import io.ksmt.solver.KSolverUnsupportedParameterException import org.ksmt.solver.bitwuzla.bindings.Bitwuzla import org.ksmt.solver.bitwuzla.bindings.BitwuzlaOption import org.ksmt.solver.bitwuzla.bindings.Native +import java.util.EnumMap interface KBitwuzlaSolverConfiguration : KSolverConfiguration { fun setBitwuzlaOption(option: BitwuzlaOption, value: Int) @@ -44,6 +45,25 @@ class KBitwuzlaSolverConfigurationImpl(private val bitwuzla: Bitwuzla) : KBitwuz } } +class KBitwuzlaForkingSolverConfigurationImpl(private val bitwuzla: Bitwuzla) : KBitwuzlaSolverConfiguration { + private val intOptions = EnumMap<_, Int>(BitwuzlaOption::class.java) + private val stringOptions = EnumMap<_, String>(BitwuzlaOption::class.java) + override fun setBitwuzlaOption(option: BitwuzlaOption, value: Int) { + Native.bitwuzlaSetOption(bitwuzla, option, value) + intOptions[option] = value + } + + override fun setBitwuzlaOption(option: BitwuzlaOption, value: String) { + Native.bitwuzlaSetOptionStr(bitwuzla, option, value) + stringOptions[option] = value + } + + fun fork(childBitwuzla: Bitwuzla) = KBitwuzlaForkingSolverConfigurationImpl(childBitwuzla).also { + intOptions.forEach { (option, value) -> it.setBitwuzlaOption(option, value) } + stringOptions.forEach { (option, value) -> it.setBitwuzlaOption(option, value) } + } +} + class KBitwuzlaSolverUniversalConfiguration( private val builder: KSolverUniversalConfigurationBuilder ) : KBitwuzlaSolverConfiguration { diff --git a/ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/ScopedLinkedFrame.kt b/ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/ScopedLinkedFrame.kt new file mode 100644 index 000000000..d3e4e5931 --- /dev/null +++ b/ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/ScopedLinkedFrame.kt @@ -0,0 +1,67 @@ +package io.ksmt.solver.bitwuzla + +internal class ScopedLinkedFrame private constructor( + private var current: LinkedFrame, + private inline val createNewFrame: () -> T, + private inline val copyFrame: (T) -> T +) { + constructor( + currentFrame: T, + createNewFrame: () -> T, + copyFrame: (T) -> T + ) : this(LinkedFrame(currentFrame), createNewFrame, copyFrame) + + constructor( + createNewFrame: () -> T, + copyFrame: (T) -> T + ) : this(createNewFrame(), createNewFrame, copyFrame) + + val currentFrame: T + get() = current.value + + val currentScope: UInt + get() = current.scope + + fun stacked(): ArrayDeque = ArrayDeque().also { stack -> + forEachReversed { frame -> + stack.addLast(frame) + } + } + + fun push() { + current = LinkedFrame(createNewFrame(), current) + } + + fun pop(n: UInt) { + repeat(n.toInt()) { + current = current.previous ?: throw IllegalStateException("Can't pop the bottom scope") + } + recreateTopFrame() + } + + private fun recreateTopFrame() { + val newTopFrame = copyFrame(currentFrame) + current = LinkedFrame(newTopFrame, current.previous) + } + + fun fork(parent: ScopedLinkedFrame) { + current = parent.current + recreateTopFrame() + } + + private inline fun forEachReversed(action: (T) -> Unit) { + var cur: LinkedFrame? = current + while (cur != null) { + action(cur.value) + cur = cur.previous + } + } + + private class LinkedFrame( + val value: E, + val previous: LinkedFrame? = null + ) { + val scope: UInt = previous?.scope?.plus(1u) ?: 0u + } + +} diff --git a/ksmt-cvc5/src/main/kotlin/io/ksmt/solver/cvc5/ScopedFrame.kt b/ksmt-cvc5/src/main/kotlin/io/ksmt/solver/cvc5/ScopedFrame.kt index e8fdcd351..1ee768826 100644 --- a/ksmt-cvc5/src/main/kotlin/io/ksmt/solver/cvc5/ScopedFrame.kt +++ b/ksmt-cvc5/src/main/kotlin/io/ksmt/solver/cvc5/ScopedFrame.kt @@ -97,7 +97,9 @@ internal class ScopedLinkedFrame private constructor( } override fun pop(n: UInt) { - current = current.previous ?: throw IllegalStateException("Can't pop the bottom scope") + repeat(n.toInt()) { + current = current.previous ?: throw IllegalStateException("Can't pop the bottom scope") + } recreateTopFrame() } diff --git a/ksmt-test/src/test/kotlin/io/ksmt/test/KForkingSolverTest.kt b/ksmt-test/src/test/kotlin/io/ksmt/test/KForkingSolverTest.kt index c019cbf94..edf9c9361 100644 --- a/ksmt-test/src/test/kotlin/io/ksmt/test/KForkingSolverTest.kt +++ b/ksmt-test/src/test/kotlin/io/ksmt/test/KForkingSolverTest.kt @@ -3,6 +3,7 @@ package io.ksmt.test import io.ksmt.KContext import io.ksmt.solver.KForkingSolverManager import io.ksmt.solver.KSolverStatus +import io.ksmt.solver.bitwuzla.KBitwuzlaForkingSolverManager import io.ksmt.solver.cvc5.KCvc5ForkingSolverManager import io.ksmt.solver.yices.KYicesForkingSolverManager import io.ksmt.solver.z3.KZ3ForkingSolverManager @@ -16,6 +17,29 @@ import kotlin.test.assertNotEquals import kotlin.test.assertTrue class KForkingSolverTest { + @Nested + inner class KForkingSolverTestBitwuzla { + @Test + fun testCheckSat() = testCheckSat(::mkBitwuzlaForkingSolverManager) + + @Test + fun testModel() = testModel(::mkBitwuzlaForkingSolverManager) + + @Test + fun testUnsatCore() = testUnsatCore(::mkBitwuzlaForkingSolverManager) + + @Test + fun testUninterpretedSort() = testUninterpretedSort(::mkBitwuzlaForkingSolverManager) + + @Test + fun testScopedAssertions() = testScopedAssertions(::mkBitwuzlaForkingSolverManager) + + @Test + fun testLifeTime() = testLifeTime(::mkBitwuzlaForkingSolverManager) + + private fun mkBitwuzlaForkingSolverManager(ctx: KContext) = KBitwuzlaForkingSolverManager(ctx) + } + @Nested inner class KForkingSolverTestCvc5 { @Test @@ -376,8 +400,8 @@ class KForkingSolverTest { mkForkingSolverManager(ctx).use { man -> with(ctx) { val parent = man.mkForkingSolver() - val x by intSort - val f = x gt 100.expr + val x by bv8Sort + val f = mkBvSignedGreaterExpr(x, mkBv(100, bv8Sort)) parent.assert(f) parent.check().also { require(it == KSolverStatus.SAT) } diff --git a/ksmt-yices/src/main/kotlin/io/ksmt/solver/yices/KYicesForkingSolver.kt b/ksmt-yices/src/main/kotlin/io/ksmt/solver/yices/KYicesForkingSolver.kt index d96be5c1d..0d75af7e1 100644 --- a/ksmt-yices/src/main/kotlin/io/ksmt/solver/yices/KYicesForkingSolver.kt +++ b/ksmt-yices/src/main/kotlin/io/ksmt/solver/yices/KYicesForkingSolver.kt @@ -73,7 +73,7 @@ class KYicesForkingSolver( get() = trackedAssertions.any { it.isNotEmpty() } override fun assert(expr: KExpr) = yicesTry { - ensureAssertionsInitiated() + yicesTry { ensureAssertionsInitiated() } ctx.ensureContextMatch(expr) val yicesExpr = with(exprInternalizer) { expr.internalize() } @@ -82,31 +82,36 @@ class KYicesForkingSolver( } override fun assertAndTrack(expr: KExpr) { - ensureAssertionsInitiated() + yicesTry { ensureAssertionsInitiated() } super.assertAndTrack(expr) } override fun push() { - ensureAssertionsInitiated() + yicesTry { ensureAssertionsInitiated() } super.push() trackedAssertions.push() yicesAssertions.push() } override fun pop(n: UInt) { - ensureAssertionsInitiated() + yicesTry { ensureAssertionsInitiated() } super.pop(n) trackedAssertions.pop(n) yicesAssertions.pop(n) } override fun check(timeout: Duration): KSolverStatus { - ensureAssertionsInitiated() + yicesTry { ensureAssertionsInitiated() } return super.check(timeout) } override fun checkWithAssumptions(assumptions: List>, timeout: Duration): KSolverStatus { - ensureAssertionsInitiated() + yicesTry { ensureAssertionsInitiated() } return super.checkWithAssumptions(assumptions, timeout) } + + override fun close() { + super.close() + manager.close(this) + } } diff --git a/ksmt-yices/src/main/kotlin/io/ksmt/solver/yices/KYicesForkingSolverManager.kt b/ksmt-yices/src/main/kotlin/io/ksmt/solver/yices/KYicesForkingSolverManager.kt index 04966037f..239b124ba 100644 --- a/ksmt-yices/src/main/kotlin/io/ksmt/solver/yices/KYicesForkingSolverManager.kt +++ b/ksmt-yices/src/main/kotlin/io/ksmt/solver/yices/KYicesForkingSolverManager.kt @@ -14,16 +14,15 @@ import io.ksmt.sort.KUninterpretedSort import it.unimi.dsi.fastutil.ints.Int2ObjectOpenHashMap import it.unimi.dsi.fastutil.ints.IntOpenHashSet import it.unimi.dsi.fastutil.objects.Object2IntOpenHashMap -import java.util.Collections.newSetFromMap -import java.util.Collections.synchronizedSet import java.util.IdentityHashMap +import java.util.concurrent.ConcurrentHashMap import java.util.concurrent.atomic.AtomicInteger class KYicesForkingSolverManager( private val ctx: KContext ) : KForkingSolverManager { - private val solvers = synchronizedSet(newSetFromMap(IdentityHashMap())) + private val solvers = ConcurrentHashMap.newKeySet() private val sharedCacheReferences = IdentityHashMap() private val expressionsCache = IdentityHashMap() diff --git a/ksmt-yices/src/main/kotlin/io/ksmt/solver/yices/ScopedFrame.kt b/ksmt-yices/src/main/kotlin/io/ksmt/solver/yices/ScopedFrame.kt index b5ed5f43c..93f757e6f 100644 --- a/ksmt-yices/src/main/kotlin/io/ksmt/solver/yices/ScopedFrame.kt +++ b/ksmt-yices/src/main/kotlin/io/ksmt/solver/yices/ScopedFrame.kt @@ -115,7 +115,9 @@ internal class ScopedLinkedFrame private constructor( } override fun pop(n: UInt) { - current = current.previous ?: throw IllegalStateException("Can't pop the bottom scope") + repeat(n.toInt()) { + current = current.previous ?: throw IllegalStateException("Can't pop the bottom scope") + } recreateTopFrame() }