diff --git a/README.md b/README.md
index c245d52f8..f61001d5f 100644
--- a/README.md
+++ b/README.md
@@ -14,9 +14,9 @@ repositories {
}
// core
-implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.5.0")
+implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.5.1")
// z3 solver
-implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.5.0")
+implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.5.1")
```
## Usage
diff --git a/buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts b/buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts
index ef65d7a5f..a27e674aa 100644
--- a/buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts
+++ b/buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts
@@ -9,7 +9,7 @@ plugins {
}
group = "org.ksmt"
-version = "0.5.0"
+version = "0.5.1"
repositories {
mavenCentral()
diff --git a/docs/custom-expressions.md b/docs/custom-expressions.md
index 67ab8a745..e38242978 100644
--- a/docs/custom-expressions.md
+++ b/docs/custom-expressions.md
@@ -216,8 +216,8 @@ class CustomSolver(
solver.assert(transformer.apply(expr))
// expr can contain custom expressions -> rewrite
- override fun assertAndTrack(expr: KExpr, trackVar: KConstDecl) =
- solver.assertAndTrack(transformer.apply(expr), trackVar)
+ override fun assertAndTrack(expr: KExpr) =
+ solver.assertAndTrack(transformer.apply(expr))
// assumptions can contain custom expressions -> rewrite
override fun checkWithAssumptions(assumptions: List>, timeout: Duration): KSolverStatus =
@@ -262,10 +262,10 @@ class CustomModel(
override val uninterpretedSorts: Set
get() = model.uninterpretedSorts
- override fun interpretation(decl: KDecl): KModel.KFuncInterp? =
+ override fun interpretation(decl: KDecl): KFuncInterp? =
model.interpretation(decl)
- override fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set>? =
+ override fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set? =
model.uninterpretedSortUniverse(sort)
override fun detach(): KModel = CustomModel(model.detach(), transformer)
diff --git a/docs/getting-started.md b/docs/getting-started.md
index 55a66e543..ddbf983a7 100644
--- a/docs/getting-started.md
+++ b/docs/getting-started.md
@@ -18,7 +18,7 @@ repositories {
```kotlin
dependencies {
// core
- implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.5.0")
+ implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.5.1")
}
```
@@ -26,9 +26,9 @@ dependencies {
```kotlin
dependencies {
// z3
- implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.5.0")
+ implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.5.1")
// bitwuzla
- implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.5.0")
+ implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.5.1")
}
```
SMT solver specific packages are provided with solver native binaries.
@@ -315,9 +315,9 @@ with(ctx) {
/**
* Assert and track e2
- * Track variable e2Track will appear in unsat core
+ * e2 will appear in unsat core
* */
- val e2Track = solver.assertAndTrack(e2)
+ solver.assertAndTrack(e2)
/**
* Check satisfiability with e3 assumed.
@@ -328,18 +328,15 @@ with(ctx) {
// retrieve unsat core
val core = solver.unsatCore()
- println("unsat core = $core") // [track!fresh!0, (not c)]
+ println("unsat core = $core") // [(not (and b a)), (not c)]
// simply asserted expression cannot be in unsat core
println("e1 in core = ${e1 in core}") // false
- /**
- * An expression added with assertAndTrack cannot be in unsat core.
- * The corresponding track variable is used instead of the expression itself.
- */
- println("e2 in core = ${e2 in core}") // false
- println("e2Track in core = ${e2Track in core}") // true
- //the assumed expression appears in unsat core as is
+ // an expression added with assertAndTrack appears in unsat core as is.
+ println("e2 in core = ${e2 in core}") // true
+
+ // the assumed expression appears in unsat core as is
println("e3 in core = ${e3 in core}") // true
}
}
diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts
index b82ed11eb..7046946d5 100644
--- a/examples/build.gradle.kts
+++ b/examples/build.gradle.kts
@@ -10,9 +10,9 @@ repositories {
dependencies {
// core
- implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.5.0")
+ implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.5.1")
// z3 solver
- implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.5.0")
+ implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.5.1")
}
java {
diff --git a/examples/src/main/kotlin/CustomExpressions.kt b/examples/src/main/kotlin/CustomExpressions.kt
index 1bac4f248..e228d828a 100644
--- a/examples/src/main/kotlin/CustomExpressions.kt
+++ b/examples/src/main/kotlin/CustomExpressions.kt
@@ -1,7 +1,6 @@
import org.ksmt.KContext
import org.ksmt.cache.hash
import org.ksmt.cache.structurallyEqual
-import org.ksmt.decl.KConstDecl
import org.ksmt.decl.KDecl
import org.ksmt.expr.KExpr
import org.ksmt.expr.KUninterpretedSortValue
@@ -13,6 +12,7 @@ import org.ksmt.solver.KModel
import org.ksmt.solver.KSolver
import org.ksmt.solver.KSolverConfiguration
import org.ksmt.solver.KSolverStatus
+import org.ksmt.solver.model.KFuncInterp
import org.ksmt.sort.KBoolSort
import org.ksmt.sort.KBvSort
import org.ksmt.sort.KSort
@@ -174,8 +174,8 @@ class CustomSolver(
solver.assert(transformer.apply(expr))
// expr can contain custom expressions -> rewrite
- override fun assertAndTrack(expr: KExpr, trackVar: KConstDecl) =
- solver.assertAndTrack(transformer.apply(expr), trackVar)
+ override fun assertAndTrack(expr: KExpr) =
+ solver.assertAndTrack(transformer.apply(expr))
// assumptions can contain custom expressions -> rewrite
override fun checkWithAssumptions(assumptions: List>, timeout: Duration): KSolverStatus =
@@ -219,7 +219,7 @@ class CustomModel(
override val uninterpretedSorts: Set
get() = model.uninterpretedSorts
- override fun interpretation(decl: KDecl): KModel.KFuncInterp? =
+ override fun interpretation(decl: KDecl): KFuncInterp? =
model.interpretation(decl)
override fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set? =
diff --git a/examples/src/main/kotlin/GettingStartedExample.kt b/examples/src/main/kotlin/GettingStartedExample.kt
index 32e617973..f33d8d501 100644
--- a/examples/src/main/kotlin/GettingStartedExample.kt
+++ b/examples/src/main/kotlin/GettingStartedExample.kt
@@ -231,9 +231,9 @@ private fun unsatCoreGenerationExample(ctx: KContext) =
/**
* Assert and track e2
- * Track variable e2Track will appear in unsat core
+ * e2 will appear in unsat core
* */
- val e2Track = solver.assertAndTrack(e2)
+ solver.assertAndTrack(e2)
/**
* Check satisfiability with e3 assumed.
@@ -244,18 +244,15 @@ private fun unsatCoreGenerationExample(ctx: KContext) =
// retrieve unsat core
val core = solver.unsatCore()
- println("unsat core = $core") // [track!fresh!0, (not c)]
+ println("unsat core = $core") // [(not (and b a)), (not c)]
// simply asserted expression cannot be in unsat core
println("e1 in core = ${e1 in core}") // false
- /**
- * An expression added with assertAndTrack cannot be in unsat core.
- * The corresponding track variable is used instead of the expression itself.
- */
- println("e2 in core = ${e2 in core}") // false
- println("e2Track in core = ${e2Track in core}") // true
- //the assumed expression appears in unsat core as is
+ // an expression added with assertAndTrack appears in unsat core as is.
+ println("e2 in core = ${e2 in core}") // true
+
+ // the assumed expression appears in unsat core as is
println("e3 in core = ${e3 in core}") // true
}
}
diff --git a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaSolver.kt b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaSolver.kt
index abd7ef2a0..084c8cc67 100644
--- a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaSolver.kt
+++ b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaSolver.kt
@@ -1,14 +1,16 @@
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.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 org.ksmt.sort.KBoolSort
import kotlin.time.Duration
@@ -21,15 +23,19 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver, BitwuzlaTerm>>()
- private val trackVarsAssertionFrames = arrayListOf(trackVars)
+ private var trackedAssertions = mutableListOf, BitwuzlaTerm>>()
+ private val trackVarsAssertionFrames = arrayListOf(trackedAssertions)
override fun configure(configurator: KBitwuzlaSolverConfiguration.() -> Unit) {
KBitwuzlaSolverConfigurationImpl(bitwuzlaCtx.bitwuzla).configurator()
@@ -46,23 +52,23 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver, trackVar: KConstDecl) = bitwuzlaCtx.bitwuzlaTry {
- ctx.ensureContextMatch(expr, trackVar)
+ override fun assertAndTrack(expr: KExpr) = 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()
}
@@ -80,7 +86,7 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver, BitwuzlaTerm>>()
-
- private fun assumeExpr(expr: KExpr, term: BitwuzlaTerm) {
- lastAssumptions += expr to term
- Native.bitwuzlaAssume(bitwuzlaCtx.bitwuzla, term)
- }
-
override fun checkWithAssumptions(assumptions: List>, timeout: Duration): KSolverStatus =
- bitwuzlaCtx.bitwuzlaTry {
+ bitwuzlaTryCheck {
ctx.ensureContextMatch(assumptions)
- invalidatePreviousModel()
- lastAssumptions.clear()
+ 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()
@@ -120,16 +119,6 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver> = 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 {
@@ -154,7 +142,7 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver 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/test/kotlin/org/ksmt/solver/bitwuzla/SolverTest.kt b/ksmt-bitwuzla/src/test/kotlin/org/ksmt/solver/bitwuzla/SolverTest.kt
index 8ba4ea5dc..aee9e4588 100644
--- a/ksmt-bitwuzla/src/test/kotlin/org/ksmt/solver/bitwuzla/SolverTest.kt
+++ b/ksmt-bitwuzla/src/test/kotlin/org/ksmt/solver/bitwuzla/SolverTest.kt
@@ -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)
}
@@ -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
@@ -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()
@@ -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()
@@ -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)
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/solver/KSolver.kt b/ksmt-core/src/main/kotlin/org/ksmt/solver/KSolver.kt
index a06d5343f..fa2d8e2fa 100644
--- a/ksmt-core/src/main/kotlin/org/ksmt/solver/KSolver.kt
+++ b/ksmt-core/src/main/kotlin/org/ksmt/solver/KSolver.kt
@@ -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
@@ -22,28 +21,12 @@ interface KSolver : AutoCloseable {
fun assert(expr: KExpr)
/**
- * 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): KExpr {
- 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, trackVar: KConstDecl)
+ fun assertAndTrack(expr: KExpr)
/**
* Create a backtracking point for assertion stack.
@@ -97,7 +80,7 @@ interface KSolver : 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>
diff --git a/ksmt-cvc5/src/main/kotlin/org.ksmt.solver.cvc5/KCvc5Solver.kt b/ksmt-cvc5/src/main/kotlin/org.ksmt.solver.cvc5/KCvc5Solver.kt
index f330e5866..66495f34e 100644
--- a/ksmt-cvc5/src/main/kotlin/org.ksmt.solver.cvc5/KCvc5Solver.kt
+++ b/ksmt-cvc5/src/main/kotlin/org.ksmt.solver.cvc5/KCvc5Solver.kt
@@ -4,9 +4,7 @@ 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.decl.KConstDecl
import org.ksmt.expr.KExpr
import org.ksmt.solver.KModel
import org.ksmt.solver.KSolver
@@ -14,7 +12,7 @@ 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
@@ -23,19 +21,19 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver>? = null
- private var cvc5CurrentLevelTrackedAssertions = mutableListOf()
+ private var cvc5CurrentLevelTrackedAssertions = TreeMap>()
private val cvc5TrackedAssertions = mutableListOf(cvc5CurrentLevelTrackedAssertions)
- private var cvc5LastAssumptions = TreeSet()
-
init {
solver.setOption("produce-models", "true")
solver.setOption("produce-unsat-cores", "true")
@@ -48,8 +46,6 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver Unit) {
KCvc5SolverConfigurationImpl(solver).configurator()
}
@@ -63,21 +59,21 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver, trackVar: KConstDecl) {
- ctx.ensureContextMatch(expr, trackVar)
+ override fun assertAndTrack(expr: KExpr) {
+ 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()
@@ -99,39 +95,36 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver>, timeout: Duration): KSolverStatus = cvc5Try {
+ override fun checkWithAssumptions(
+ assumptions: List>,
+ timeout: Duration
+ ): KSolverStatus = cvc5TryCheck {
ctx.ensureContextMatch(assumptions)
- invalidatePreviousModel()
- val cvc5Assumptions = with(exprInternalizer) {
- assumptions.map { it.internalizeExpr() }
- }.toTypedArray()
+ val lastAssumptions = TreeMap>().also { cvc5LastAssumptions = it }
+ val cvc5Assumptions = Array(assumptions.size) { idx ->
+ val assumedExpr = assumptions[idx]
+ with(exprInternalizer) {
+ assumedExpr.internalizeExpr().also {
+ lastAssumptions[it] = assumedExpr
+ }
+ }
+ }
- cvc5LastAssumptions = cvc5Assumptions.toCollection(TreeSet())
solver.updateTimeout(timeout)
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 {
@@ -150,12 +143,16 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver> = 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>()
+ cvc5TrackedAssertions.forEach { frame ->
+ trackedTerms.putAll(frame)
+ }
+ cvc5LastAssumptions?.also { trackedTerms.putAll(it) }
+
+ cvc5FullCore.mapNotNull { trackedTerms[it] }
}
override fun close() {
@@ -179,7 +176,9 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver 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) {
@@ -193,6 +192,27 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver 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") {
diff --git a/ksmt-cvc5/src/test/kotlin/org/ksmt/solver/cvc5/IncrementalApiTest.kt b/ksmt-cvc5/src/test/kotlin/org/ksmt/solver/cvc5/IncrementalApiTest.kt
index 63715790f..9dee21f9d 100644
--- a/ksmt-cvc5/src/test/kotlin/org/ksmt/solver/cvc5/IncrementalApiTest.kt
+++ b/ksmt-cvc5/src/test/kotlin/org/ksmt/solver/cvc5/IncrementalApiTest.kt
@@ -142,12 +142,12 @@ class IncrementalApiTest {
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)
}
@@ -160,12 +160,12 @@ class IncrementalApiTest {
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
@@ -173,12 +173,12 @@ class IncrementalApiTest {
val a = boolSort.mkConst("a")
solver.assert(a)
solver.push()
- val track = solver.assertAndTrack(!a)
+ solver.assertAndTrack(!a)
var status = solver.check()
assertEquals(KSolverStatus.UNSAT, status)
val core = solver.unsatCore()
assertEquals(1, core.size)
- assertTrue(track in core)
+ assertTrue(!a in core)
solver.pop()
status = solver.check()
assertEquals(KSolverStatus.SAT, status)
diff --git a/ksmt-runner/src/main/kotlin/org/ksmt/runner/generated/models/SolverProtocolModel.Generated.kt b/ksmt-runner/src/main/kotlin/org/ksmt/runner/generated/models/SolverProtocolModel.Generated.kt
index 197d8f31a..9cd0df660 100644
--- a/ksmt-runner/src/main/kotlin/org/ksmt/runner/generated/models/SolverProtocolModel.Generated.kt
+++ b/ksmt-runner/src/main/kotlin/org/ksmt/runner/generated/models/SolverProtocolModel.Generated.kt
@@ -22,7 +22,7 @@ class SolverProtocolModel private constructor(
private val _deleteSolver: RdCall,
private val _configure: RdCall, Unit>,
private val _assert: RdCall,
- private val _assertAndTrack: RdCall,
+ private val _assertAndTrack: RdCall,
private val _push: RdCall,
private val _pop: RdCall,
private val _check: RdCall,
@@ -40,7 +40,6 @@ class SolverProtocolModel private constructor(
serializers.register(CreateSolverParams)
serializers.register(SolverConfigurationParam)
serializers.register(AssertParams)
- serializers.register(AssertAndTrackParams)
serializers.register(PopParams)
serializers.register(CheckParams)
serializers.register(CheckResult)
@@ -78,7 +77,7 @@ class SolverProtocolModel private constructor(
private val __SolverConfigurationParamListSerializer = SolverConfigurationParam.list()
- const val serializationHash = 6654719566694323594L
+ const val serializationHash = 9141130720080102681L
}
override val serializersOwner: ISerializersOwner get() = SolverProtocolModel
@@ -109,7 +108,7 @@ class SolverProtocolModel private constructor(
/**
* Assert and track expression
*/
- val assertAndTrack: RdCall get() = _assertAndTrack
+ val assertAndTrack: RdCall get() = _assertAndTrack
/**
* Solver push
@@ -191,7 +190,7 @@ class SolverProtocolModel private constructor(
RdCall(FrameworkMarshallers.Void, FrameworkMarshallers.Void),
RdCall, Unit>(__SolverConfigurationParamListSerializer, FrameworkMarshallers.Void),
RdCall(AssertParams, FrameworkMarshallers.Void),
- RdCall(AssertAndTrackParams, FrameworkMarshallers.Void),
+ RdCall(AssertParams, FrameworkMarshallers.Void),
RdCall(FrameworkMarshallers.Void, FrameworkMarshallers.Void),
RdCall(PopParams, FrameworkMarshallers.Void),
RdCall(CheckParams, CheckResult),
@@ -248,69 +247,6 @@ val IProtocol.solverProtocolModel get() = getOrCreateExtension(SolverProtocolMod
-/**
- * #### Generated from [SolverProtocolModel.kt:51]
- */
-data class AssertAndTrackParams (
- val expression: org.ksmt.KAst,
- val trackVar: org.ksmt.KAst
-) : IPrintable {
- //companion
-
- companion object : IMarshaller {
- override val _type: KClass = AssertAndTrackParams::class
-
- @Suppress("UNCHECKED_CAST")
- override fun read(ctx: SerializationCtx, buffer: AbstractBuffer): AssertAndTrackParams {
- val expression = (ctx.serializers.get(org.ksmt.runner.serializer.AstSerializationCtx.marshallerId)!! as IMarshaller).read(ctx, buffer)
- val trackVar = (ctx.serializers.get(org.ksmt.runner.serializer.AstSerializationCtx.marshallerId)!! as IMarshaller).read(ctx, buffer)
- return AssertAndTrackParams(expression, trackVar)
- }
-
- override fun write(ctx: SerializationCtx, buffer: AbstractBuffer, value: AssertAndTrackParams) {
- (ctx.serializers.get(org.ksmt.runner.serializer.AstSerializationCtx.marshallerId)!! as IMarshaller).write(ctx,buffer, value.expression)
- (ctx.serializers.get(org.ksmt.runner.serializer.AstSerializationCtx.marshallerId)!! as IMarshaller).write(ctx,buffer, value.trackVar)
- }
-
-
- }
- //fields
- //methods
- //initializer
- //secondary constructor
- //equals trait
- override fun equals(other: Any?): Boolean {
- if (this === other) return true
- if (other == null || other::class != this::class) return false
-
- other as AssertAndTrackParams
-
- if (expression != other.expression) return false
- if (trackVar != other.trackVar) return false
-
- return true
- }
- //hash code trait
- override fun hashCode(): Int {
- var __r = 0
- __r = __r*31 + expression.hashCode()
- __r = __r*31 + trackVar.hashCode()
- return __r
- }
- //pretty print
- override fun print(printer: PrettyPrinter) {
- printer.println("AssertAndTrackParams (")
- printer.indent {
- print("expression = "); expression.print(printer); println()
- print("trackVar = "); trackVar.print(printer); println()
- }
- printer.print(")")
- }
- //deepClone
- //contexts
-}
-
-
/**
* #### Generated from [SolverProtocolModel.kt:47]
*/
@@ -369,7 +305,7 @@ data class AssertParams (
/**
- * #### Generated from [SolverProtocolModel.kt:60]
+ * #### Generated from [SolverProtocolModel.kt:55]
*/
data class CheckParams (
val timeout: Long
@@ -426,7 +362,7 @@ data class CheckParams (
/**
- * #### Generated from [SolverProtocolModel.kt:64]
+ * #### Generated from [SolverProtocolModel.kt:59]
*/
data class CheckResult (
val status: org.ksmt.solver.KSolverStatus
@@ -483,7 +419,7 @@ data class CheckResult (
/**
- * #### Generated from [SolverProtocolModel.kt:68]
+ * #### Generated from [SolverProtocolModel.kt:63]
*/
data class CheckWithAssumptionsParams (
val assumptions: List,
@@ -651,7 +587,7 @@ data class CreateSolverParams (
/**
- * #### Generated from [SolverProtocolModel.kt:87]
+ * #### Generated from [SolverProtocolModel.kt:82]
*/
data class ModelEntry (
val decl: org.ksmt.KAst,
@@ -726,7 +662,7 @@ data class ModelEntry (
/**
- * #### Generated from [SolverProtocolModel.kt:81]
+ * #### Generated from [SolverProtocolModel.kt:76]
*/
data class ModelFuncInterpEntry (
val hasVars: Boolean,
@@ -795,7 +731,7 @@ data class ModelFuncInterpEntry (
/**
- * #### Generated from [SolverProtocolModel.kt:99]
+ * #### Generated from [SolverProtocolModel.kt:94]
*/
data class ModelResult (
val declarations: List,
@@ -864,7 +800,7 @@ data class ModelResult (
/**
- * #### Generated from [SolverProtocolModel.kt:94]
+ * #### Generated from [SolverProtocolModel.kt:89]
*/
data class ModelUninterpretedSortUniverse (
val sort: org.ksmt.KAst,
@@ -927,7 +863,7 @@ data class ModelUninterpretedSortUniverse (
/**
- * #### Generated from [SolverProtocolModel.kt:56]
+ * #### Generated from [SolverProtocolModel.kt:51]
*/
data class PopParams (
val levels: UInt
@@ -984,7 +920,7 @@ data class PopParams (
/**
- * #### Generated from [SolverProtocolModel.kt:77]
+ * #### Generated from [SolverProtocolModel.kt:72]
*/
data class ReasonUnknownResult (
val reasonUnknown: String
@@ -1127,7 +1063,7 @@ enum class SolverType {
/**
- * #### Generated from [SolverProtocolModel.kt:73]
+ * #### Generated from [SolverProtocolModel.kt:68]
*/
data class UnsatCoreResult (
val core: List
diff --git a/ksmt-runner/src/main/kotlin/org/ksmt/solver/async/KAsyncSolver.kt b/ksmt-runner/src/main/kotlin/org/ksmt/solver/async/KAsyncSolver.kt
index 585c03a5e..526c2af47 100644
--- a/ksmt-runner/src/main/kotlin/org/ksmt/solver/async/KAsyncSolver.kt
+++ b/ksmt-runner/src/main/kotlin/org/ksmt/solver/async/KAsyncSolver.kt
@@ -1,6 +1,5 @@
package org.ksmt.solver.async
-import org.ksmt.decl.KConstDecl
import org.ksmt.expr.KExpr
import org.ksmt.solver.KModel
import org.ksmt.solver.KSolver
@@ -15,7 +14,7 @@ interface KAsyncSolver : KSolver {
suspend fun assertAsync(expr: KExpr)
- suspend fun assertAndTrackAsync(expr: KExpr, trackVar: KConstDecl)
+ suspend fun assertAndTrackAsync(expr: KExpr)
suspend fun pushAsync()
diff --git a/ksmt-runner/src/main/kotlin/org/ksmt/solver/portfolio/KPortfolioSolver.kt b/ksmt-runner/src/main/kotlin/org/ksmt/solver/portfolio/KPortfolioSolver.kt
index fdc2410d2..54a137274 100644
--- a/ksmt-runner/src/main/kotlin/org/ksmt/solver/portfolio/KPortfolioSolver.kt
+++ b/ksmt-runner/src/main/kotlin/org/ksmt/solver/portfolio/KPortfolioSolver.kt
@@ -11,7 +11,6 @@ import kotlinx.coroutines.joinAll
import kotlinx.coroutines.launch
import kotlinx.coroutines.newSingleThreadContext
import kotlinx.coroutines.runBlocking
-import org.ksmt.decl.KConstDecl
import org.ksmt.expr.KExpr
import org.ksmt.solver.KModel
import org.ksmt.solver.KSolver
@@ -107,8 +106,8 @@ class KPortfolioSolver(
assertAsync(expr)
}
- override fun assertAndTrack(expr: KExpr, trackVar: KConstDecl) = runBlocking {
- assertAndTrackAsync(expr, trackVar)
+ override fun assertAndTrack(expr: KExpr) = runBlocking {
+ assertAndTrackAsync(expr)
}
override fun push() = runBlocking {
@@ -154,10 +153,9 @@ class KPortfolioSolver(
assertAsync(expr)
}
- override suspend fun assertAndTrackAsync(expr: KExpr, trackVar: KConstDecl) =
- solverOperation {
- assertAndTrackAsync(expr, trackVar)
- }
+ override suspend fun assertAndTrackAsync(expr: KExpr) = solverOperation {
+ assertAndTrackAsync(expr)
+ }
override suspend fun pushAsync() = solverOperation {
pushAsync()
diff --git a/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverRunner.kt b/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverRunner.kt
index f0ab06390..ed82d43f8 100644
--- a/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverRunner.kt
+++ b/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverRunner.kt
@@ -4,7 +4,6 @@ import com.jetbrains.rd.util.AtomicReference
import com.jetbrains.rd.util.threading.SpinWait
import kotlinx.coroutines.sync.Mutex
import org.ksmt.KContext
-import org.ksmt.decl.KConstDecl
import org.ksmt.expr.KExpr
import org.ksmt.runner.generated.ConfigurationBuilder
import org.ksmt.runner.generated.models.SolverConfigurationParam
@@ -102,31 +101,28 @@ class KSolverRunner(
}
}
- override suspend fun assertAndTrackAsync(expr: KExpr, trackVar: KConstDecl) =
- assertAndTrack(expr, trackVar) { e, track ->
- ensureInitializedAndExecuteAsync(onException = {}) {
- assertAndTrackAsync(e, track)
- }
+ override suspend fun assertAndTrackAsync(expr: KExpr) = assertAndTrack(expr) { e ->
+ ensureInitializedAndExecuteAsync(onException = {}) {
+ assertAndTrackAsync(e)
}
+ }
- override fun assertAndTrack(expr: KExpr, trackVar: KConstDecl) =
- assertAndTrack(expr, trackVar) { e, track ->
- ensureInitializedAndExecuteSync(onException = {}) {
- assertAndTrackSync(e, track)
- }
+ override fun assertAndTrack(expr: KExpr) = assertAndTrack(expr) { e ->
+ ensureInitializedAndExecuteSync(onException = {}) {
+ assertAndTrackSync(e)
}
+ }
private inline fun assertAndTrack(
expr: KExpr,
- trackVar: KConstDecl,
- execute: (KExpr, KConstDecl) -> Unit
+ execute: (KExpr) -> Unit
) {
- ctx.ensureContextMatch(expr, trackVar)
+ ctx.ensureContextMatch(expr)
try {
- execute(expr, trackVar)
+ execute(expr)
} finally {
- solverState.assertAndTrack(expr, trackVar)
+ solverState.assertAndTrack(expr)
}
}
diff --git a/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverRunnerExecutor.kt b/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverRunnerExecutor.kt
index 82d3a346b..a4668486a 100644
--- a/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverRunnerExecutor.kt
+++ b/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverRunnerExecutor.kt
@@ -11,12 +11,10 @@ import com.jetbrains.rd.util.threading.SynchronousScheduler
import kotlinx.coroutines.TimeoutCancellationException
import kotlinx.coroutines.withTimeout
import org.ksmt.KContext
-import org.ksmt.decl.KConstDecl
import org.ksmt.decl.KDecl
import org.ksmt.expr.KExpr
import org.ksmt.expr.KUninterpretedSortValue
import org.ksmt.runner.core.KsmtWorkerSession
-import org.ksmt.runner.generated.models.AssertAndTrackParams
import org.ksmt.runner.generated.models.AssertParams
import org.ksmt.runner.generated.models.CheckParams
import org.ksmt.runner.generated.models.CheckResult
@@ -94,27 +92,21 @@ class KSolverRunnerExecutor(
query(AssertParams(expr))
}
- fun assertAndTrackSync(expr: KExpr, trackVar: KConstDecl) =
- assertAndTrack(expr, trackVar) { params ->
- queryWithTimeoutAndExceptionHandlingSync {
- assertAndTrack.querySync(params)
- }
+ fun assertAndTrackSync(expr: KExpr) = assertAndTrack(expr) { params ->
+ queryWithTimeoutAndExceptionHandlingSync {
+ assertAndTrack.querySync(params)
}
+ }
- suspend fun assertAndTrackAsync(expr: KExpr, trackVar: KConstDecl) =
- assertAndTrack(expr, trackVar) { params ->
- queryWithTimeoutAndExceptionHandlingAsync {
- assertAndTrack.queryAsync(params)
- }
+ suspend fun assertAndTrackAsync(expr: KExpr) = assertAndTrack(expr) { params ->
+ queryWithTimeoutAndExceptionHandlingAsync {
+ assertAndTrack.queryAsync(params)
}
+ }
- private inline fun assertAndTrack(
- expr: KExpr,
- trackVar: KConstDecl,
- query: (AssertAndTrackParams) -> Unit
- ) {
+ private inline fun assertAndTrack(expr: KExpr, query: (AssertParams) -> Unit) {
ensureActive()
- query(AssertAndTrackParams(expr, trackVar))
+ query(AssertParams(expr))
}
fun pushSync() = push {
diff --git a/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverState.kt b/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverState.kt
index 22226265d..aa132cabf 100644
--- a/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverState.kt
+++ b/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverState.kt
@@ -1,6 +1,5 @@
package org.ksmt.solver.runner
-import org.ksmt.decl.KConstDecl
import org.ksmt.expr.KExpr
import org.ksmt.runner.generated.models.SolverConfigurationParam
import org.ksmt.sort.KBoolSort
@@ -21,10 +20,7 @@ import java.util.concurrent.ConcurrentLinkedQueue
class KSolverState {
private sealed interface AssertFrame
private data class ExprAssertFrame(val expr: KExpr) : AssertFrame
- private data class AssertAndTrackFrame(
- val expr: KExpr,
- val trackVar: KConstDecl
- ) : AssertFrame
+ private data class AssertAndTrackFrame(val expr: KExpr) : AssertFrame
private val configuration = ConcurrentLinkedQueue()
@@ -47,8 +43,8 @@ class KSolverState {
assertFrames.last.add(ExprAssertFrame(expr))
}
- fun assertAndTrack(expr: KExpr, trackVar: KConstDecl) {
- assertFrames.last.add(AssertAndTrackFrame(expr, trackVar))
+ fun assertAndTrack(expr: KExpr) {
+ assertFrames.last.add(AssertAndTrackFrame(expr))
}
fun push() {
@@ -65,14 +61,14 @@ class KSolverState {
configureSolver = { executor.configureAsync(it) },
pushScope = { executor.pushAsync() },
assertExpr = { executor.assertAsync(it) },
- assertExprAndTrack = { expr, trackVar -> executor.assertAndTrackAsync(expr, trackVar) }
+ assertExprAndTrack = { expr -> executor.assertAndTrackAsync(expr) }
)
fun applySync(executor: KSolverRunnerExecutor) = replayState(
configureSolver = { executor.configureSync(it) },
pushScope = { executor.pushSync() },
assertExpr = { executor.assertSync(it) },
- assertExprAndTrack = { expr, trackVar -> executor.assertAndTrackSync(expr, trackVar) }
+ assertExprAndTrack = { expr -> executor.assertAndTrackSync(expr) }
)
/**
@@ -83,7 +79,7 @@ class KSolverState {
configureSolver: (List) -> Unit,
pushScope: () -> Unit,
assertExpr: (KExpr) -> Unit,
- assertExprAndTrack: (KExpr, KConstDecl) -> Unit
+ assertExprAndTrack: (KExpr) -> Unit
) {
if (configuration.isNotEmpty()) {
configureSolver(configuration.toList())
@@ -100,7 +96,7 @@ class KSolverState {
for (assertion in frame) {
when (assertion) {
is ExprAssertFrame -> assertExpr(assertion.expr)
- is AssertAndTrackFrame -> assertExprAndTrack(assertion.expr, assertion.trackVar)
+ is AssertAndTrackFrame -> assertExprAndTrack(assertion.expr)
}
}
}
diff --git a/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverWorkerProcess.kt b/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverWorkerProcess.kt
index afa654c3e..273bde0eb 100644
--- a/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverWorkerProcess.kt
+++ b/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverWorkerProcess.kt
@@ -2,7 +2,6 @@ package org.ksmt.solver.runner
import com.jetbrains.rd.framework.IProtocol
import org.ksmt.KContext
-import org.ksmt.decl.KConstDecl
import org.ksmt.expr.KExpr
import org.ksmt.runner.core.ChildProcessBase
import org.ksmt.runner.core.KsmtWorkerArgs
@@ -88,7 +87,7 @@ class KSolverWorkerProcess : ChildProcessBase() {
}
assertAndTrack.measureExecutionForTermination { params ->
@Suppress("UNCHECKED_CAST")
- solver.assertAndTrack(params.expression as KExpr, params.trackVar as KConstDecl)
+ solver.assertAndTrack(params.expression as KExpr)
}
push.measureExecutionForTermination {
solver.push()
diff --git a/ksmt-runner/src/main/rdgen/org/ksmt/runner/models/SolverProtocolModel.kt b/ksmt-runner/src/main/rdgen/org/ksmt/runner/models/SolverProtocolModel.kt
index b03fa96c9..0d80adc6a 100644
--- a/ksmt-runner/src/main/rdgen/org/ksmt/runner/models/SolverProtocolModel.kt
+++ b/ksmt-runner/src/main/rdgen/org/ksmt/runner/models/SolverProtocolModel.kt
@@ -48,11 +48,6 @@ object SolverProtocolModel : Ext(SolverProtocolRoot) {
field("expression", kastType)
}
- private val assertAndTrackParams = structdef {
- field("expression", kastType)
- field("trackVar", kastType)
- }
-
private val popParams = structdef {
field("levels", PredefinedType.uint)
}
@@ -119,7 +114,7 @@ object SolverProtocolModel : Ext(SolverProtocolRoot) {
async
documentation = "Assert expression"
}
- call("assertAndTrack", assertAndTrackParams, PredefinedType.void).apply {
+ call("assertAndTrack", assertParams, PredefinedType.void).apply {
async
documentation = "Assert and track expression"
}
diff --git a/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/CustomSolverTest.kt b/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/CustomSolverTest.kt
index 34a8b2838..c514dc32f 100644
--- a/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/CustomSolverTest.kt
+++ b/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/CustomSolverTest.kt
@@ -1,7 +1,6 @@
package org.ksmt.solver.runner
import org.ksmt.KContext
-import org.ksmt.decl.KConstDecl
import org.ksmt.expr.KExpr
import org.ksmt.solver.KModel
import org.ksmt.solver.KSolver
@@ -54,7 +53,7 @@ class CustomSolverTest {
override fun assert(expr: KExpr) {
}
- override fun assertAndTrack(expr: KExpr, trackVar: KConstDecl) {
+ override fun assertAndTrack(expr: KExpr) {
}
override fun push() {
diff --git a/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/PortfolioSolverTest.kt b/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/PortfolioSolverTest.kt
index 64de3bf82..98df1dc57 100644
--- a/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/PortfolioSolverTest.kt
+++ b/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/PortfolioSolverTest.kt
@@ -58,7 +58,7 @@ class PortfolioSolverTest {
val e3 = !c
solver.assert(e1)
- val e2Track = solver.assertAndTrack(e2)
+ solver.assertAndTrack(e2)
val status = solver.checkWithAssumptions(listOf(e3))
assertEquals(KSolverStatus.UNSAT, status)
@@ -66,7 +66,7 @@ class PortfolioSolverTest {
val core = solver.unsatCore()
assertEquals(2, core.size)
- assertTrue(e2Track in core)
+ assertTrue(e2 in core)
assertTrue(e3 in core)
}
@@ -79,7 +79,7 @@ class PortfolioSolverTest {
val e2 = !(a and b)
solver.assert(e1)
- val e2Track = solver.assertAndTrack(e2)
+ solver.assertAndTrack(e2)
val status = solver.check()
assertEquals(KSolverStatus.UNSAT, status)
@@ -87,7 +87,7 @@ class PortfolioSolverTest {
val core = solver.unsatCore()
assertEquals(1, core.size)
- assertTrue(e2Track in core)
+ assertTrue(e2 in core)
}
@Test
@@ -96,7 +96,7 @@ class PortfolioSolverTest {
solver.assert(a)
solver.push()
- val track = solver.assertAndTrack(!a)
+ solver.assertAndTrack(!a)
var status = solver.check()
assertEquals(KSolverStatus.UNSAT, status)
@@ -104,7 +104,7 @@ class PortfolioSolverTest {
val core = solver.unsatCore()
assertEquals(1, core.size)
- assertTrue(track in core)
+ assertTrue(!a in core)
solver.pop()
status = solver.check()
diff --git a/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/SolverRunnerTest.kt b/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/SolverRunnerTest.kt
index 966159423..168b5e8b5 100644
--- a/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/SolverRunnerTest.kt
+++ b/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/SolverRunnerTest.kt
@@ -62,12 +62,12 @@ class SolverRunnerTest {
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)
}
@@ -80,12 +80,12 @@ class SolverRunnerTest {
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
@@ -93,12 +93,12 @@ class SolverRunnerTest {
val a = boolSort.mkConst("a")
solver.assert(a)
solver.push()
- val track = solver.assertAndTrack(!a)
+ solver.assertAndTrack(!a)
var status = solver.check()
assertEquals(KSolverStatus.UNSAT, status)
val core = solver.unsatCore()
assertEquals(1, core.size)
- assertTrue(track in core)
+ assertTrue(!a in core)
solver.pop()
status = solver.check()
assertEquals(KSolverStatus.SAT, status)
diff --git a/ksmt-test/src/test/kotlin/org/ksmt/test/CheckWithAssumptionsTest.kt b/ksmt-test/src/test/kotlin/org/ksmt/test/CheckWithAssumptionsTest.kt
new file mode 100644
index 000000000..881a0248c
--- /dev/null
+++ b/ksmt-test/src/test/kotlin/org/ksmt/test/CheckWithAssumptionsTest.kt
@@ -0,0 +1,79 @@
+package org.ksmt.test
+
+import org.ksmt.KContext
+import org.ksmt.solver.KSolver
+import org.ksmt.solver.KSolverStatus
+import org.ksmt.solver.bitwuzla.KBitwuzlaSolver
+import org.ksmt.solver.cvc5.KCvc5Solver
+import org.ksmt.solver.yices.KYicesSolver
+import org.ksmt.solver.z3.KZ3Solver
+import org.ksmt.utils.getValue
+import kotlin.test.Test
+import kotlin.test.assertEquals
+import kotlin.test.assertTrue
+
+class CheckWithAssumptionsTest {
+
+ @Test
+ fun testComplexAssumptionZ3() = testComplexAssumption { KZ3Solver(it) }
+
+ @Test
+ fun testComplexAssumptionBitwuzla() = testComplexAssumption { KBitwuzlaSolver(it) }
+
+ @Test
+ fun testComplexAssumptionYices() = testComplexAssumption { KYicesSolver(it) }
+
+ @Test
+ fun testComplexAssumptionCvc() = testComplexAssumption { KCvc5Solver(it) }
+
+ @Test
+ fun testUnsatCoreGenerationZ3() = testUnsatCoreGeneration { KZ3Solver(it) }
+
+ @Test
+ fun testUnsatCoreGenerationBitwuzla() = testUnsatCoreGeneration { KBitwuzlaSolver(it) }
+
+ @Test
+ fun testUnsatCoreGenerationYices() = testUnsatCoreGeneration { KYicesSolver(it) }
+
+ @Test
+ fun testUnsatCoreGenerationCvc() = testUnsatCoreGeneration { KCvc5Solver(it) }
+
+ private fun testComplexAssumption(mkSolver: (KContext) -> KSolver<*>) = with(KContext()) {
+ mkSolver(this).use { solver ->
+ val a by bv32Sort
+ val b by bv32Sort
+
+ solver.assert(a eq mkBv(0))
+ solver.assert(b eq mkBv(0))
+
+ val expr = mkBvUnsignedGreaterExpr(a, b)
+ val status = solver.checkWithAssumptions(listOf(expr))
+
+ assertEquals(KSolverStatus.UNSAT, status)
+ }
+ }
+
+ private fun testUnsatCoreGeneration(mkSolver: (KContext) -> KSolver<*>) = with(KContext()) {
+ mkSolver(this).use { solver ->
+ val a by boolSort
+ val b by boolSort
+ val c by boolSort
+
+ val e1 = (a and b) or c
+ val e2 = !(a and b)
+ val e3 = !c
+
+ solver.assert(e1)
+ solver.assertAndTrack(e2)
+
+ val status = solver.checkWithAssumptions(listOf(e3))
+ assertEquals(KSolverStatus.UNSAT, status)
+
+ val core = solver.unsatCore()
+ assertEquals(2, core.size)
+
+ assertTrue(e2 in core)
+ assertTrue(e3 in core)
+ }
+ }
+}
diff --git a/ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesSolver.kt b/ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesSolver.kt
index 364ef6010..7ab561d80 100644
--- a/ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesSolver.kt
+++ b/ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesSolver.kt
@@ -4,8 +4,9 @@ import com.sri.yices.Config
import com.sri.yices.Context
import com.sri.yices.Status
import com.sri.yices.YicesException
+import it.unimi.dsi.fastutil.ints.IntArrayList
+import it.unimi.dsi.fastutil.ints.IntOpenHashSet
import org.ksmt.KContext
-import org.ksmt.decl.KConstDecl
import org.ksmt.expr.KExpr
import org.ksmt.solver.KModel
import org.ksmt.solver.KSolver
@@ -33,9 +34,11 @@ class KYicesSolver(private val ctx: KContext) : KSolver()
+ private var currentLevelTrackedAssertions = mutableListOf, YicesTerm>>()
private val trackedAssertions = mutableListOf(currentLevelTrackedAssertions)
private val timer = Timer()
@@ -55,16 +58,16 @@ class KYicesSolver(private val ctx: KContext) : KSolver, trackVar: KConstDecl) = yicesTry {
+ override fun assertAndTrack(expr: KExpr) = yicesTry {
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 yicesTrackVar = with(exprInternalizer) { trackVarExpr.internalize() }
- currentLevelTrackedAssertions += yicesTrackVar
+ currentLevelTrackedAssertions += expr to yicesTrackVar
}
override fun push(): Unit = yicesTry {
@@ -89,12 +92,12 @@ class KYicesSolver(private val ctx: KContext) : KSolver>,
timeout: Duration
- ): KSolverStatus {
+ ): KSolverStatus = yicesTryCheck {
ctx.ensureContextMatch(assumptions)
- val yicesAssumptions = mutableListOf()
- trackedAssertions.flatMapTo(yicesAssumptions) { it }
+ val yicesAssumptions = TrackedAssumptions().also { lastAssumptions = it }
+
+ trackedAssertions.forEach { frame ->
+ frame.forEach { assertion ->
+ yicesAssumptions.assumeTrackedAssertion(assertion)
+ }
+ }
+
with(exprInternalizer) {
- assumptions.mapTo(yicesAssumptions) { it.internalize() }
+ assumptions.forEach { assumedExpr ->
+ yicesAssumptions.assumeAssumption(assumedExpr, assumedExpr.internalize())
+ }
}
- return withTimer(timeout) {
- nativeContext.checkWithAssumptions(yicesAssumptions.toIntArray())
+ checkWithTimer(timeout) {
+ nativeContext.checkWithAssumptions(yicesAssumptions.assumedTerms())
}.processCheckResult()
}
@@ -130,9 +141,7 @@ class KYicesSolver(private val ctx: KContext) : KSolver withTimer(timeout: Duration, body: () -> T): T {
+ private inline fun checkWithTimer(timeout: Duration, body: () -> T): T {
val task = StopSearchTask()
if (timeout.isFinite()) {
@@ -157,8 +166,6 @@ class KYicesSolver(private val ctx: KContext) : KSolver 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
@@ -187,4 +208,27 @@ class KYicesSolver(private val ctx: KContext) : KSolver, YicesTerm>>()
+ private val assumedTerms = IntArrayList()
+
+ fun assumeTrackedAssertion(trackedAssertion: Pair, YicesTerm>) {
+ assumedExprs.add(trackedAssertion)
+ assumedTerms.add(trackedAssertion.second)
+ }
+
+ fun assumeAssumption(expr: KExpr, term: YicesTerm) =
+ assumeTrackedAssertion(expr to term)
+
+ fun assumedTerms(): YicesTermArray {
+ assumedTerms.trim() // Elements length now equal to size
+ return assumedTerms.elements()
+ }
+
+ fun resolveUnsatCore(yicesUnsatCore: YicesTermArray): List> {
+ val unsatCoreTerms = IntOpenHashSet(yicesUnsatCore)
+ return assumedExprs.mapNotNull { (expr, term) -> expr.takeIf { unsatCoreTerms.contains(term) } }
+ }
+ }
}
diff --git a/ksmt-yices/src/test/kotlin/org/ksmt/solver/yices/SolverTest.kt b/ksmt-yices/src/test/kotlin/org/ksmt/solver/yices/SolverTest.kt
index 9a8b114a8..e52717dc0 100644
--- a/ksmt-yices/src/test/kotlin/org/ksmt/solver/yices/SolverTest.kt
+++ b/ksmt-yices/src/test/kotlin/org/ksmt/solver/yices/SolverTest.kt
@@ -41,12 +41,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)
}
@@ -60,12 +60,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
@@ -80,17 +80,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()
@@ -100,7 +100,7 @@ class SolverTest {
assertEquals(KSolverStatus.UNSAT, status)
core = solver.unsatCore()
assertEquals(1, core.size)
- assertTrue(track1 in core)
+ assertTrue(!a in core)
solver.pop()
diff --git a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3Solver.kt b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3Solver.kt
index 6e933da5e..062a453ed 100644
--- a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3Solver.kt
+++ b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3Solver.kt
@@ -7,8 +7,8 @@ import com.microsoft.z3.solverAssert
import com.microsoft.z3.solverAssertAndTrack
import com.microsoft.z3.solverCheckAssumptions
import com.microsoft.z3.solverGetUnsatCore
+import it.unimi.dsi.fastutil.longs.Long2ObjectOpenHashMap
import org.ksmt.KContext
-import org.ksmt.decl.KConstDecl
import org.ksmt.expr.KExpr
import org.ksmt.solver.KModel
import org.ksmt.solver.KSolver
@@ -26,6 +26,7 @@ open class KZ3Solver(private val ctx: KContext) : KSolver, trackVar: KConstDecl) = z3Try {
- ctx.ensureContextMatch(expr, trackVar)
+ private val trackedAssertions = Long2ObjectOpenHashMap>()
+ override fun assertAndTrack(expr: KExpr) = z3Try {
+ ctx.ensureContextMatch(expr)
+
+ val trackExpr = ctx.mkFreshConst("track", ctx.boolSort)
val z3Expr = with(exprInternalizer) { expr.internalizeExpr() }
- val z3TrackVar = with(exprInternalizer) { trackVar.apply().internalizeExpr() }
+ val z3TrackVar = with(exprInternalizer) { trackExpr.internalizeExpr() }
+
+ trackedAssertions.put(z3TrackVar, expr)
solver.solverAssertAndTrack(z3Expr, z3TrackVar)
}
- override fun check(timeout: Duration): KSolverStatus = z3Try {
+ override fun check(timeout: Duration): KSolverStatus = z3TryCheck {
solver.updateTimeout(timeout)
solver.check().processCheckResult()
}
@@ -94,7 +100,7 @@ open class KZ3Solver(private val ctx: KContext) : KSolver>,
timeout: Duration
- ): KSolverStatus = z3Try {
+ ): KSolverStatus = z3TryCheck {
ctx.ensureContextMatch(assumptions)
val z3Assumptions = with(exprInternalizer) {
@@ -115,20 +121,19 @@ open class KZ3Solver(private val ctx: KContext) : KSolver> = z3Try {
require(lastCheckStatus == KSolverStatus.UNSAT) { "Unsat cores are only available after UNSAT checks" }
val unsatCore = solver.solverGetUnsatCore()
with(exprConverter) {
- unsatCore.map { it.convertExpr() }
+ unsatCore.map { trackedAssertions.get(it) ?: it.convertExpr() }
}
}
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 {
@@ -165,6 +170,19 @@ open class KZ3Solver(private val ctx: KContext) : KSolver KSolverStatus): KSolverStatus = try {
+ invalidateSolverState()
+ body()
+ } catch (ex: Z3Exception) {
+ lastReasonOfUnknown = ex.message
+ KSolverStatus.UNKNOWN.also { lastCheckStatus = it }
+ }
+
companion object {
init {
System.setProperty("z3.skipLibraryLoad", "true")
diff --git a/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/IncrementalApiTest.kt b/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/IncrementalApiTest.kt
index c309169f6..274fb3bcc 100644
--- a/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/IncrementalApiTest.kt
+++ b/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/IncrementalApiTest.kt
@@ -23,12 +23,12 @@ class IncrementalApiTest {
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)
}
@@ -41,12 +41,12 @@ class IncrementalApiTest {
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
@@ -54,12 +54,12 @@ class IncrementalApiTest {
val a = boolSort.mkConst("a")
solver.assert(a)
solver.push()
- val track = solver.assertAndTrack(!a)
+ solver.assertAndTrack(!a)
var status = solver.check()
assertEquals(KSolverStatus.UNSAT, status)
val core = solver.unsatCore()
assertEquals(1, core.size)
- assertTrue(track in core)
+ assertTrue(!a in core)
solver.pop()
status = solver.check()
assertEquals(KSolverStatus.SAT, status)