Skip to content

Commit

Permalink
Handle check-sat errors as unknowns
Browse files Browse the repository at this point in the history
  • Loading branch information
@Saloed
Saloed committed Apr 27, 2023
1 parent 829e6f9 commit b91228f
Show file tree
Hide file tree
Showing 4 changed files with 105 additions and 70 deletions.
48 changes: 28 additions & 20 deletions ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaSolver.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ import org.ksmt.expr.KExpr
import org.ksmt.solver.KModel
import org.ksmt.solver.KSolver
import org.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
Expand All @@ -22,7 +23,11 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver<KBitwuzlaSolverC
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)
Expand Down Expand Up @@ -89,18 +94,10 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver<KBitwuzlaSolverC
override fun check(timeout: Duration): KSolverStatus =
checkWithAssumptions(emptyList(), timeout)

private var lastAssumptions: TrackedAssumptions? = null
private fun invalidateAssumptions() {
lastAssumptions = null
}

override fun checkWithAssumptions(assumptions: List<KExpr<KBoolSort>>, timeout: Duration): KSolverStatus =
bitwuzlaCtx.bitwuzlaTry {
bitwuzlaTryCheck {
ctx.ensureContextMatch(assumptions)

invalidatePreviousModel()
invalidateAssumptions()

val currentAssumptions = TrackedAssumptions().also { lastAssumptions = it }

trackedAssertions.forEach {
Expand All @@ -122,16 +119,6 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver<KBitwuzlaSolverC
Native.bitwuzlaCheckSatTimeoutResult(bitwuzlaCtx.bitwuzla, timeout.inWholeMilliseconds)
}

private var lastModel: KBitwuzlaModel? = null

/**
* Bitwuzla model is only valid until the next check-sat call.
* */
private fun invalidatePreviousModel() {
lastModel?.markInvalid()
lastModel = null
}

override fun model(): KModel = bitwuzlaCtx.bitwuzlaTry {
require(lastCheckStatus == KSolverStatus.SAT) { "Model are only available after SAT checks" }
val model = lastModel ?: KBitwuzlaModel(
Expand All @@ -155,7 +142,7 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver<KBitwuzlaSolverC
}

// There is no way to retrieve reason of unknown from Bitwuzla in general case.
return "unknown"
return lastReasonOfUnknown ?: "unknown"
}

override fun interrupt() = bitwuzlaCtx.bitwuzlaTry {
Expand All @@ -172,6 +159,27 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver<KBitwuzlaSolverC
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>>()

Expand Down
69 changes: 38 additions & 31 deletions ksmt-cvc5/src/main/kotlin/org.ksmt.solver.cvc5/KCvc5Solver.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@ import io.github.cvc5.CVC5ApiException
import io.github.cvc5.Result
import io.github.cvc5.Solver
import io.github.cvc5.Term
import io.github.cvc5.UnknownExplanation
import org.ksmt.KContext
import org.ksmt.expr.KExpr
import org.ksmt.solver.KModel
Expand All @@ -27,7 +26,10 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver<KCvc5SolverConfigura
get() = cvc5TrackedAssertions.lastIndex.toUInt()

private var lastCheckStatus = KSolverStatus.UNKNOWN
private var cvc5LastUnknownExplanation: UnknownExplanation? = null
private var lastReasonOfUnknown: String? = null
private var lastModel: KCvc5Model? = null
// we need TreeMap here (hashcode not implemented in Term)
private var cvc5LastAssumptions: TreeMap<Term, KExpr<KBoolSort>>? = null

private var cvc5CurrentLevelTrackedAssertions = TreeMap<Term, KExpr<KBoolSort>>()
private val cvc5TrackedAssertions = mutableListOf(cvc5CurrentLevelTrackedAssertions)
Expand All @@ -44,8 +46,6 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver<KCvc5SolverConfigura

open fun createExprInternalizer(cvc5Ctx: KCvc5Context): KCvc5ExprInternalizer = KCvc5ExprInternalizer(cvc5Ctx)

open fun createExprConverter(cvc5Ctx: KCvc5Context): KCvc5ExprConverter = KCvc5ExprConverter(ctx, cvc5Ctx)

override fun configure(configurator: KCvc5SolverConfiguration.() -> Unit) {
KCvc5SolverConfigurationImpl(solver).configurator()
}
Expand Down Expand Up @@ -95,29 +95,16 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver<KCvc5SolverConfigura
solver.pop(n.toInt())
}

// we need TreeMap here (hashcode not implemented in Term)
private var cvc5LastAssumptions: TreeMap<Term, KExpr<KBoolSort>>? = null
private fun invalidateAssumptions() {
cvc5LastAssumptions = null
}

override fun check(timeout: Duration): KSolverStatus = cvc5Try {
invalidatePreviousModel()
invalidateAssumptions()

override fun check(timeout: Duration): KSolverStatus = cvc5TryCheck {
solver.updateTimeout(timeout)
solver.checkSat().processCheckResult()
}

override fun reasonOfUnknown(): String = cvc5Try {
require(lastCheckStatus == KSolverStatus.UNKNOWN) { "Unknown reason is only available after UNKNOWN checks" }
cvc5LastUnknownExplanation?.name ?: "no explanation"
}

override fun checkWithAssumptions(assumptions: List<KExpr<KBoolSort>>, timeout: Duration): KSolverStatus = cvc5Try {
override fun checkWithAssumptions(
assumptions: List<KExpr<KBoolSort>>,
timeout: Duration
): KSolverStatus = cvc5TryCheck {
ctx.ensureContextMatch(assumptions)
invalidatePreviousModel()
invalidateAssumptions()

val lastAssumptions = TreeMap<Term, KExpr<KBoolSort>>().also { cvc5LastAssumptions = it }
val cvc5Assumptions = Array(assumptions.size) { idx ->
Expand All @@ -133,14 +120,11 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver<KCvc5SolverConfigura
solver.checkSatAssuming(cvc5Assumptions).processCheckResult()
}

private var lastModel: KCvc5Model? = null

/**
* Cvc5 model is only valid until the next check-sat call.
* */
private fun invalidatePreviousModel() {
lastModel?.markInvalid()
lastModel = null
override fun reasonOfUnknown(): String = cvc5Try {
require(lastCheckStatus == KSolverStatus.UNKNOWN) {
"Unknown reason is only available after UNKNOWN checks"
}
lastReasonOfUnknown ?: "no explanation"
}

override fun model(): KModel = cvc5Try {
Expand Down Expand Up @@ -192,7 +176,9 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver<KCvc5SolverConfigura
else -> KSolverStatus.UNKNOWN
}.also {
lastCheckStatus = it
if (it == KSolverStatus.UNKNOWN) cvc5LastUnknownExplanation = this.unknownExplanation
if (it == KSolverStatus.UNKNOWN) {
lastReasonOfUnknown = this.unknownExplanation?.name
}
}

private fun Solver.updateTimeout(timeout: Duration) {
Expand All @@ -206,6 +192,27 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver<KCvc5SolverConfigura
throw KSolverException(ex)
}

private inline fun cvc5TryCheck(body: () -> KSolverStatus): KSolverStatus = try {
invalidateSolverState()
body()
} catch (ex: CVC5ApiException) {
lastReasonOfUnknown = ex.message
KSolverStatus.UNKNOWN.also { lastCheckStatus = it }
}

private fun invalidateSolverState() {
/**
* Cvc5 model is only valid until the next check-sat call.
* */
lastModel?.markInvalid()
lastModel = null

lastCheckStatus = KSolverStatus.UNKNOWN
lastReasonOfUnknown = null

cvc5LastAssumptions = null
}

companion object {
init {
if (System.getProperty("cvc5.skipLibraryLoad") != "true") {
Expand Down
38 changes: 22 additions & 16 deletions ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesSolver.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,9 @@ class KYicesSolver(private val ctx: KContext) : KSolver<KYicesSolverConfiguratio
KYicesExprConverter(ctx, yicesCtx)
}

private var lastAssumptions: TrackedAssumptions? = null
private var lastCheckStatus = KSolverStatus.UNKNOWN
private var lastReasonOfUnknown: String? = null

private var currentLevelTrackedAssertions = mutableListOf<Pair<KExpr<KBoolSort>, YicesTerm>>()
private val trackedAssertions = mutableListOf(currentLevelTrackedAssertions)
Expand Down Expand Up @@ -90,30 +92,22 @@ class KYicesSolver(private val ctx: KContext) : KSolver<KYicesSolverConfiguratio
currentLevelTrackedAssertions = trackedAssertions.last()
}

private var lastAssumptions: TrackedAssumptions? = null
private fun invalidateAssumptions() {
lastAssumptions = null
}

override fun check(timeout: Duration): KSolverStatus {
invalidateAssumptions()

override fun check(timeout: Duration): KSolverStatus = yicesTryCheck {
if (trackedAssertions.any { it.isNotEmpty() }) {
return checkWithAssumptions(emptyList(), timeout)
}

return withTimer(timeout) {
checkWithTimer(timeout) {
nativeContext.check()
}.processCheckResult()
}

override fun checkWithAssumptions(
assumptions: List<KExpr<KBoolSort>>,
timeout: Duration
): KSolverStatus {
): KSolverStatus = yicesTryCheck {
ctx.ensureContextMatch(assumptions)

invalidateAssumptions()
val yicesAssumptions = TrackedAssumptions().also { lastAssumptions = it }

trackedAssertions.forEach { frame ->
Expand All @@ -128,7 +122,7 @@ class KYicesSolver(private val ctx: KContext) : KSolver<KYicesSolverConfiguratio
}
}

return withTimer(timeout) {
checkWithTimer(timeout) {
nativeContext.checkWithAssumptions(yicesAssumptions.assumedTerms())
}.processCheckResult()
}
Expand Down Expand Up @@ -156,14 +150,14 @@ class KYicesSolver(private val ctx: KContext) : KSolver<KYicesSolverConfiguratio
}

// There is no way to retrieve reason of unknown from Yices in general case.
return "unknown"
return lastReasonOfUnknown ?: "unknown"
}

override fun interrupt() = yicesTry {
nativeContext.stopSearch()
}

private inline fun <T> withTimer(timeout: Duration, body: () -> T): T {
private inline fun <T> checkWithTimer(timeout: Duration, body: () -> T): T {
val task = StopSearchTask()

if (timeout.isFinite()) {
Expand All @@ -172,8 +166,6 @@ class KYicesSolver(private val ctx: KContext) : KSolver<KYicesSolverConfiguratio

return try {
body()
} catch (ex: YicesException) {
throw KSolverException(ex)
} finally {
task.cancel()
}
Expand All @@ -185,6 +177,20 @@ class KYicesSolver(private val ctx: KContext) : KSolver<KYicesSolverConfiguratio
throw KSolverException(ex)
}

private inline fun yicesTryCheck(body: () -> KSolverStatus): KSolverStatus = try {
invalidateSolverState()
body()
} catch (ex: YicesException) {
lastReasonOfUnknown = ex.message
KSolverStatus.UNKNOWN.also { lastCheckStatus = it }
}

private fun invalidateSolverState() {
lastCheckStatus = KSolverStatus.UNKNOWN
lastReasonOfUnknown = null
lastAssumptions = null
}

private fun Status.processCheckResult() = when (this) {
Status.SAT -> KSolverStatus.SAT
Status.UNSAT -> KSolverStatus.UNSAT
Expand Down
20 changes: 17 additions & 3 deletions ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3Solver.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ open class KZ3Solver(private val ctx: KContext) : KSolver<KZ3SolverConfiguration
private val z3Ctx = KZ3Context(ctx)
private val solver = createSolver()
private var lastCheckStatus = KSolverStatus.UNKNOWN
private var lastReasonOfUnknown: String? = null
private var currentScope: UInt = 0u

@Suppress("LeakingThis")
Expand Down Expand Up @@ -91,15 +92,15 @@ open class KZ3Solver(private val ctx: KContext) : KSolver<KZ3SolverConfiguration
solver.solverAssertAndTrack(z3Expr, z3TrackVar)
}

override fun check(timeout: Duration): KSolverStatus = z3Try {
override fun check(timeout: Duration): KSolverStatus = z3TryCheck {
solver.updateTimeout(timeout)
solver.check().processCheckResult()
}

override fun checkWithAssumptions(
assumptions: List<KExpr<KBoolSort>>,
timeout: Duration
): KSolverStatus = z3Try {
): KSolverStatus = z3TryCheck {
ctx.ensureContextMatch(assumptions)

val z3Assumptions = with(exprInternalizer) {
Expand Down Expand Up @@ -132,7 +133,7 @@ open class KZ3Solver(private val ctx: KContext) : KSolver<KZ3SolverConfiguration

override fun reasonOfUnknown(): String = z3Try {
require(lastCheckStatus == KSolverStatus.UNKNOWN) { "Unknown reason is only available after UNKNOWN checks" }
solver.reasonUnknown
lastReasonOfUnknown ?: solver.reasonUnknown
}

override fun interrupt() = z3Try {
Expand Down Expand Up @@ -169,6 +170,19 @@ open class KZ3Solver(private val ctx: KContext) : KSolver<KZ3SolverConfiguration
throw KSolverException(ex)
}

private fun invalidateSolverState() {
lastReasonOfUnknown = null
lastCheckStatus = KSolverStatus.UNKNOWN
}

private inline fun z3TryCheck(body: () -> KSolverStatus): KSolverStatus = try {
invalidateSolverState()
body()
} catch (ex: Z3Exception) {
lastReasonOfUnknown = ex.message
KSolverStatus.UNKNOWN.also { lastCheckStatus = it }
}

companion object {
init {
System.setProperty("z3.skipLibraryLoad", "true")
Expand Down

0 comments on commit b91228f

Please sign in to comment.