Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Resolve track vars in unsat cores #105

Merged
merged 4 commits into from
Apr 27, 2023
Merged

Resolve track vars in unsat cores #105

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
6e47999
Get rid of track vars in unsat cores
Saloed Apr 26, 2023
cefbf11
Handle check-sat errors as unknowns
Saloed Apr 27, 2023
3376ec0
Update examples
Saloed Apr 27, 2023
3956e36
Upgrade version to 0.5.1
Saloed Apr 27, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Next Next commit
Get rid of track vars in unsat cores
  • Loading branch information
@Saloed
Saloed committed Apr 27, 2023
commit 6e47999d3a44e039e7bcbe16a02b32fe9b055ce0
66 changes: 42 additions & 24 deletions ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaSolver.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,14 +1,15 @@
package org.ksmt.solver.bitwuzla

import it.unimi.dsi.fastutil.longs.LongOpenHashSet
import org.ksmt.KContext
import org.ksmt.decl.KConstDecl
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.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 org.ksmt.sort.KBoolSort
import kotlin.time.Duration
Expand All @@ -28,8 +29,8 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver<KBitwuzlaSolverC
Native.bitwuzlaSetOption(bitwuzlaCtx.bitwuzla, BitwuzlaOption.BITWUZLA_OPT_PRODUCE_MODELS, value = 1)
}

private var trackVars = mutableListOf<Pair<KExpr<KBoolSort>, BitwuzlaTerm>>()
private val trackVarsAssertionFrames = arrayListOf(trackVars)
private var trackedAssertions = mutableListOf<Pair<KExpr<KBoolSort>, BitwuzlaTerm>>()
private val trackVarsAssertionFrames = arrayListOf(trackedAssertions)

override fun configure(configurator: KBitwuzlaSolverConfiguration.() -> Unit) {
KBitwuzlaSolverConfigurationImpl(bitwuzlaCtx.bitwuzla).configurator()
Expand All @@ -46,23 +47,23 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver<KBitwuzlaSolverC
Native.bitwuzlaAssert(bitwuzlaCtx.bitwuzla, assertionWithAxioms.assertion)
}

override fun assertAndTrack(expr: KExpr<KBoolSort>, trackVar: KConstDecl<KBoolSort>) = bitwuzlaCtx.bitwuzlaTry {
ctx.ensureContextMatch(expr, trackVar)
override fun assertAndTrack(expr: KExpr<KBoolSort>) = bitwuzlaCtx.bitwuzlaTry {
ctx.ensureContextMatch(expr)

val trackVarExpr = ctx.mkConstApp(trackVar)
val trackVarExpr = ctx.mkFreshConst("track", ctx.boolSort)
val trackedExpr = with(ctx) { !trackVarExpr or expr }

assert(trackedExpr)

val trackVarTerm = with(exprInternalizer) { trackVarExpr.internalize() }
trackVars += trackVarExpr to trackVarTerm
trackedAssertions += expr to trackVarTerm
}

override fun push(): Unit = bitwuzlaCtx.bitwuzlaTry {
Native.bitwuzlaPush(bitwuzlaCtx.bitwuzla, nlevels = 1)

trackVars = trackVars.toMutableList()
trackVarsAssertionFrames.add(trackVars)
trackedAssertions = trackedAssertions.toMutableList()
trackVarsAssertionFrames.add(trackedAssertions)

bitwuzlaCtx.createNestedDeclarationScope()
}
Expand All @@ -80,35 +81,36 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver<KBitwuzlaSolverC
bitwuzlaCtx.popDeclarationScope()
}

trackVars = trackVarsAssertionFrames.last()
trackedAssertions = trackVarsAssertionFrames.last()

Native.bitwuzlaPop(bitwuzlaCtx.bitwuzla, n.toInt())
}

override fun check(timeout: Duration): KSolverStatus =
checkWithAssumptions(emptyList(), timeout)

private val lastAssumptions = arrayListOf<Pair<KExpr<KBoolSort>, BitwuzlaTerm>>()

private fun assumeExpr(expr: KExpr<KBoolSort>, term: BitwuzlaTerm) {
lastAssumptions += expr to term
Native.bitwuzlaAssume(bitwuzlaCtx.bitwuzla, term)
private var lastAssumptions: TrackedAssumptions? = null
private fun invalidateAssumptions() {
lastAssumptions = null
}

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

invalidatePreviousModel()
lastAssumptions.clear()
invalidateAssumptions()

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

trackVars.forEach {
assumeExpr(it.first, it.second)
trackedAssertions.forEach {
currentAssumptions.assumeTrackedAssertion(it)
}

assumptions.forEach {
val assumptionTerm = with(exprInternalizer) { it.internalize() }
assumeExpr(it, assumptionTerm)
with(exprInternalizer) {
assumptions.forEach {
currentAssumptions.assumeAssumption(it, it.internalize())
}
}

checkWithTimeout(timeout).processCheckResult()
Expand Down Expand Up @@ -143,9 +145,8 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver<KBitwuzlaSolverC

override fun unsatCore(): List<KExpr<KBoolSort>> = bitwuzlaCtx.bitwuzlaTry {
require(lastCheckStatus == KSolverStatus.UNSAT) { "Unsat cores are only available after UNSAT checks" }
val unsatCore = Native.bitwuzlaGetUnsatAssumptions(bitwuzlaCtx.bitwuzla).toSet()

return lastAssumptions.filter { it.second in unsatCore }.map { it.first }
val unsatAssumptions = Native.bitwuzlaGetUnsatAssumptions(bitwuzlaCtx.bitwuzla)
lastAssumptions?.resolveUnsatCore(unsatAssumptions) ?: emptyList()
}

override fun reasonOfUnknown(): String = bitwuzlaCtx.bitwuzlaTry {
Expand All @@ -170,4 +171,21 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver<KBitwuzlaSolverC
BitwuzlaResult.BITWUZLA_UNSAT -> KSolverStatus.UNSAT
BitwuzlaResult.BITWUZLA_UNKNOWN -> 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) } }
}
}
}
20 changes: 10 additions & 10 deletions ksmt-bitwuzla/src/test/kotlin/org/ksmt/solver/bitwuzla/SolverTest.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,12 +39,12 @@ class SolverTest {
val e3 = !c

solver.assert(e1)
val e2Track = solver.assertAndTrack(e2)
solver.assertAndTrack(e2)
val status = solver.checkWithAssumptions(listOf(e3))
assertEquals(KSolverStatus.UNSAT, status)
val core = solver.unsatCore()
assertEquals(2, core.size)
assertTrue(e2Track in core)
assertTrue(e2 in core)
assertTrue(e3 in core)
}

Expand All @@ -57,12 +57,12 @@ class SolverTest {
val e2 = !(a and b)

solver.assert(e1)
val e2Track = solver.assertAndTrack(e2)
solver.assertAndTrack(e2)
val status = solver.check()
assertEquals(KSolverStatus.UNSAT, status)
val core = solver.unsatCore()
assertEquals(1, core.size)
assertTrue(e2Track in core)
assertTrue(e2 in core)
}

@Test
Expand All @@ -76,17 +76,17 @@ class SolverTest {

solver.push()

val track1 = solver.assertAndTrack(!a)
solver.assertAndTrack(!a)

solver.push()

val track2 = solver.assertAndTrack(!b)
solver.assertAndTrack(!b)

var status = solver.check()
assertEquals(KSolverStatus.UNSAT, status)
var core = solver.unsatCore()
assertEquals(2, core.size)
assertTrue(track1 in core && track2 in core)
assertTrue(!a in core && !b in core)

solver.pop()

Expand All @@ -96,7 +96,7 @@ class SolverTest {
assertEquals(KSolverStatus.UNSAT, status)
core = solver.unsatCore()
assertEquals(1, core.size)
assertTrue(track1 in core)
assertTrue(!a in core)

solver.pop()

Expand All @@ -109,12 +109,12 @@ class SolverTest {
val a by boolSort
solver.assert(a)
solver.push()
val track = solver.assertAndTrack(!a)
solver.assertAndTrack(!a)
var status = solver.checkWithAssumptions(listOf(a))
assertEquals(KSolverStatus.UNSAT, status)
val core = solver.unsatCore()
assertEquals(1, core.size)
assertTrue(track in core || a in core)
assertTrue(!a in core || a in core)
solver.pop()
status = solver.check()
assertEquals(KSolverStatus.SAT, status)
Expand Down
23 changes: 3 additions & 20 deletions ksmt-core/src/main/kotlin/org/ksmt/solver/KSolver.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
package org.ksmt.solver

import org.ksmt.decl.KConstDecl
import org.ksmt.expr.KExpr
import org.ksmt.sort.KBoolSort
import kotlin.time.Duration
Expand All @@ -22,28 +21,12 @@ interface KSolver<Config: KSolverConfiguration> : AutoCloseable {
fun assert(expr: KExpr<KBoolSort>)

/**
* Assert an expression into solver.
*
* @return [KBoolSort] constant which is used to track a given assertion
* in unsat cores.
* @see checkWithAssumptions
* @see unsatCore
* */
fun assertAndTrack(expr: KExpr<KBoolSort>): KExpr<KBoolSort> {
val trackVar = expr.ctx.mkFreshConstDecl("track", expr.ctx.boolSort)
assertAndTrack(expr, trackVar)
return trackVar.apply()
}

/**
* Assert an expression into solver.
* Assert an expression into solver and track it in unsat cores.
*
* [trackVar] constant which is used to track a given assertion
* in unsat cores.
* @see checkWithAssumptions
* @see unsatCore
* */
fun assertAndTrack(expr: KExpr<KBoolSort>, trackVar: KConstDecl<KBoolSort>)
fun assertAndTrack(expr: KExpr<KBoolSort>)

/**
* Create a backtracking point for assertion stack.
Expand Down Expand Up @@ -97,7 +80,7 @@ interface KSolver<Config: KSolverConfiguration> : AutoCloseable {
*
* Unsat core consists only of:
* 1. assumptions provided in [checkWithAssumptions]
* 2. track variables corresponding to expressions asserted with [assertAndTrack]
* 2. expressions asserted with [assertAndTrack]
* */
fun unsatCore(): List<KExpr<KBoolSort>>

Expand Down
55 changes: 34 additions & 21 deletions ksmt-cvc5/src/main/kotlin/org.ksmt.solver.cvc5/KCvc5Solver.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,15 +6,14 @@ import io.github.cvc5.Solver
import io.github.cvc5.Term
import io.github.cvc5.UnknownExplanation
import org.ksmt.KContext
import org.ksmt.decl.KConstDecl
import org.ksmt.expr.KExpr
import org.ksmt.solver.KModel
import org.ksmt.solver.KSolver
import org.ksmt.solver.KSolverException
import org.ksmt.solver.KSolverStatus
import org.ksmt.sort.KBoolSort
import org.ksmt.utils.NativeLibraryLoader
import java.util.TreeSet
import java.util.TreeMap
import kotlin.time.Duration
import kotlin.time.DurationUnit

Expand All @@ -23,19 +22,16 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver<KCvc5SolverConfigura
private val cvc5Ctx = KCvc5Context(solver, ctx)

private val exprInternalizer by lazy { createExprInternalizer(cvc5Ctx) }
private val exprConverter: KCvc5ExprConverter by lazy { createExprConverter(cvc5Ctx) }

private val currentScope: UInt
get() = cvc5TrackedAssertions.lastIndex.toUInt()

private var lastCheckStatus = KSolverStatus.UNKNOWN
private var cvc5LastUnknownExplanation: UnknownExplanation? = null

private var cvc5CurrentLevelTrackedAssertions = mutableListOf<Term>()
private var cvc5CurrentLevelTrackedAssertions = TreeMap<Term, KExpr<KBoolSort>>()
private val cvc5TrackedAssertions = mutableListOf(cvc5CurrentLevelTrackedAssertions)

private var cvc5LastAssumptions = TreeSet<Term>()

init {
solver.setOption("produce-models", "true")
solver.setOption("produce-unsat-cores", "true")
Expand Down Expand Up @@ -63,21 +59,21 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver<KCvc5SolverConfigura
cvc5Ctx.assertPendingAxioms(solver)
}

override fun assertAndTrack(expr: KExpr<KBoolSort>, trackVar: KConstDecl<KBoolSort>) {
ctx.ensureContextMatch(expr, trackVar)
override fun assertAndTrack(expr: KExpr<KBoolSort>) {
ctx.ensureContextMatch(expr)

val trackVarApp = trackVar.apply()
val trackVarApp = ctx.mkFreshConst("track", ctx.boolSort)
val cvc5TrackVar = with(exprInternalizer) { trackVarApp.internalizeExpr() }
val trackedExpr = with(ctx) { trackVarApp implies expr }

cvc5CurrentLevelTrackedAssertions.add(cvc5TrackVar)
cvc5CurrentLevelTrackedAssertions[cvc5TrackVar] = expr

assert(trackedExpr)
solver.assertFormula(cvc5TrackVar)
}

override fun push() = solver.push().also {
cvc5CurrentLevelTrackedAssertions = mutableListOf()
cvc5CurrentLevelTrackedAssertions = TreeMap()
cvc5TrackedAssertions.add(cvc5CurrentLevelTrackedAssertions)

cvc5Ctx.push()
Expand All @@ -99,9 +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()
cvc5LastAssumptions = TreeSet()
invalidateAssumptions()

solver.updateTimeout(timeout)
solver.checkSat().processCheckResult()
}
Expand All @@ -114,12 +117,18 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver<KCvc5SolverConfigura
override fun checkWithAssumptions(assumptions: List<KExpr<KBoolSort>>, timeout: Duration): KSolverStatus = cvc5Try {
ctx.ensureContextMatch(assumptions)
invalidatePreviousModel()
invalidateAssumptions()

val lastAssumptions = TreeMap<Term, KExpr<KBoolSort>>().also { cvc5LastAssumptions = it }
val cvc5Assumptions = Array(assumptions.size) { idx ->
val assumedExpr = assumptions[idx]
with(exprInternalizer) {
assumedExpr.internalizeExpr().also {
lastAssumptions[it] = assumedExpr
}
}
}

val cvc5Assumptions = with(exprInternalizer) {
assumptions.map { it.internalizeExpr() }
}.toTypedArray()

cvc5LastAssumptions = cvc5Assumptions.toCollection(TreeSet())
solver.updateTimeout(timeout)
solver.checkSatAssuming(cvc5Assumptions).processCheckResult()
}
Expand Down Expand Up @@ -150,12 +159,16 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver<KCvc5SolverConfigura

override fun unsatCore(): List<KExpr<KBoolSort>> = cvc5Try {
require(lastCheckStatus == KSolverStatus.UNSAT) { "Unsat cores are only available after UNSAT checks" }
// we need TreeSet here (hashcode not implemented in Term)
val cvc5TrackedVars = cvc5TrackedAssertions.flatten().toSortedSet()

val cvc5FullCore = solver.unsatCore
val cvc5UnsatCore = cvc5FullCore.filter { it in cvc5TrackedVars || it in cvc5LastAssumptions }

with(exprConverter) { cvc5UnsatCore.map { it.convertExpr() } }
val trackedTerms = TreeMap<Term, KExpr<KBoolSort>>()
cvc5TrackedAssertions.forEach { frame ->
trackedTerms.putAll(frame)
}
cvc5LastAssumptions?.also { trackedTerms.putAll(it) }

cvc5FullCore.mapNotNull { trackedTerms[it] }
}

override fun close() {
Expand Down
Loading