Resolve track vars in unsat cores (#105)

* Get rid of track vars in unsat cores

* Handle check-sat errors as unknowns

* Update examples

* Upgrade version to 0.5.1

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

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()

docs/custom-expressions.md

@@ -216,8 +216,8 @@ class CustomSolver<C : KSolverConfiguration>(
         solver.assert(transformer.apply(expr))
 
     // expr can contain custom expressions -> rewrite
-    override fun assertAndTrack(expr: KExpr<KBoolSort>, trackVar: KConstDecl<KBoolSort>) =
-        solver.assertAndTrack(transformer.apply(expr), trackVar)
+    override fun assertAndTrack(expr: KExpr<KBoolSort>) =
+        solver.assertAndTrack(transformer.apply(expr))
 
     // assumptions can contain custom expressions -> rewrite
     override fun checkWithAssumptions(assumptions: List<KExpr<KBoolSort>>, timeout: Duration): KSolverStatus =
@@ -262,10 +262,10 @@ class CustomModel(
     override val uninterpretedSorts: Set<KUninterpretedSort>
         get() = model.uninterpretedSorts
 
-    override fun <T : KSort> interpretation(decl: KDecl<T>): KModel.KFuncInterp<T>? =
+    override fun <T : KSort> interpretation(decl: KDecl<T>): KFuncInterp<T>? =
         model.interpretation(decl)
 
-    override fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set<KExpr<KUninterpretedSort>>? =
+    override fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set<KUninterpretedSortValue>? =
         model.uninterpretedSortUniverse(sort)
 
     override fun detach(): KModel = CustomModel(model.detach(), transformer)

docs/getting-started.md

@@ -18,17 +18,17 @@ repositories {
 ```kotlin
 dependencies {
     // core 
-    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.5.0")    
+    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.5.1")    
 }
 ```
 
 #### 3. Add one or more SMT solver 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
     }
 }

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 {

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<C : KSolverConfiguration>(
         solver.assert(transformer.apply(expr))
 
     // expr can contain custom expressions -> rewrite
-    override fun assertAndTrack(expr: KExpr<KBoolSort>, trackVar: KConstDecl<KBoolSort>) =
-        solver.assertAndTrack(transformer.apply(expr), trackVar)
+    override fun assertAndTrack(expr: KExpr<KBoolSort>) =
+        solver.assertAndTrack(transformer.apply(expr))
 
     // assumptions can contain custom expressions -> rewrite
     override fun checkWithAssumptions(assumptions: List<KExpr<KBoolSort>>, timeout: Duration): KSolverStatus =
@@ -219,7 +219,7 @@ class CustomModel(
     override val uninterpretedSorts: Set<KUninterpretedSort>
         get() = model.uninterpretedSorts
 
-    override fun <T : KSort> interpretation(decl: KDecl<T>): KModel.KFuncInterp<T>? =
+    override fun <T : KSort> interpretation(decl: KDecl<T>): KFuncInterp<T>? =
         model.interpretation(decl)
 
     override fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set<KUninterpretedSortValue>? =

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
         }
     }

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<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)
         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()
@@ -46,23 +52,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()
     }
@@ -80,35 +86,28 @@ 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)
-    }
-
     override fun checkWithAssumptions(assumptions: List<KExpr<KBoolSort>>, 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<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(
@@ -143,9 +132,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 {
@@ -154,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 {
@@ -170,4 +158,42 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver<KBitwuzlaSolverC
         BitwuzlaResult.BITWUZLA_UNSAT -> KSolverStatus.UNSAT
         BitwuzlaResult.BITWUZLA_UNKNOWN -> KSolverStatus.UNKNOWN
     }.also { lastCheckStatus = it }
+
+    private fun invalidateSolverState() {
+        /**
+         * Bitwuzla model is only valid until the next check-sat call.
+         * */
+        lastModel?.markInvalid()
+        lastModel = null
+
+        lastCheckStatus = KSolverStatus.UNKNOWN
+        lastReasonOfUnknown = null
+
+        lastAssumptions = null
+    }
+
+    private inline fun bitwuzlaTryCheck(body: () -> KSolverStatus): KSolverStatus = try {
+        invalidateSolverState()
+        body()
+    } catch (ex: BitwuzlaNativeException) {
+        lastReasonOfUnknown = ex.message
+        KSolverStatus.UNKNOWN.also { lastCheckStatus = it }
+    }
+
+    private inner class TrackedAssumptions {
+        private val assumedExprs = arrayListOf<Pair<KExpr<KBoolSort>, BitwuzlaTerm>>()
+
+        fun assumeTrackedAssertion(trackedAssertion: Pair<KExpr<KBoolSort>, BitwuzlaTerm>) {
+            assumedExprs.add(trackedAssertion)
+            Native.bitwuzlaAssume(bitwuzlaCtx.bitwuzla, trackedAssertion.second)
+        }
+
+        fun assumeAssumption(expr: KExpr<KBoolSort>, term: BitwuzlaTerm) =
+            assumeTrackedAssertion(expr to term)
+
+        fun resolveUnsatCore(unsatAssumptions: BitwuzlaTermArray): List<KExpr<KBoolSort>> {
+            val unsatCoreTerms = LongOpenHashSet(unsatAssumptions)
+            return assumedExprs.mapNotNull { (expr, term) -> expr.takeIf { unsatCoreTerms.contains(term) } }
+        }
+    }
 }