From edae365372025b98327cee937c1d12f9c187ad40 Mon Sep 17 00:00:00 2001 From: Valentyn Sobol Date: Tue, 24 Oct 2023 09:54:27 +0300 Subject: [PATCH] Bulk assert solver API (#134) * Solver bulk assert API * Fix transformer cache * Transformer cache reset API --- README.md | 6 +- .../main/kotlin/io.ksmt.ksmt-base.gradle.kts | 2 +- docs/getting-started.md | 6 +- examples/build.gradle.kts | 6 +- .../rewrite/simplify/KBoolExprSimplifier.kt | 2 + .../KNonRecursiveTransformerBase.kt | 12 ++- .../transformer/KNonRecursiveVisitorBase.kt | 10 +- .../src/main/kotlin/io/ksmt/solver/KSolver.kt | 17 +++ .../models/SolverProtocolModel.Generated.kt | 102 ++++++++++++++++-- .../io/ksmt/solver/async/KAsyncSolver.kt | 4 + .../ksmt/solver/portfolio/KPortfolioSolver.kt | 16 +++ .../io/ksmt/solver/runner/KSolverRunner.kt | 70 ++++++++++-- .../solver/runner/KSolverRunnerExecutor.kt | 39 +++++++ .../io/ksmt/solver/runner/KSolverState.kt | 39 ++++--- .../solver/runner/KSolverWorkerProcess.kt | 8 ++ .../ksmt/runner/models/SolverProtocolModel.kt | 12 +++ .../io/ksmt/solver/runner/SolverRunnerTest.kt | 23 ++++ 17 files changed, 322 insertions(+), 52 deletions(-) diff --git a/README.md b/README.md index 2fc051b9b..db5a1d4db 100644 --- a/README.md +++ b/README.md @@ -11,7 +11,7 @@ Get the most out of SMT solving with KSMT features: * Streamlined [solver delivery](#ksmt-distribution) with no need for building a solver or implementing JVM bindings [![KSMT: build](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml/badge.svg)](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml) -[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.9) +[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.10) [![javadoc](https://javadoc.io/badge2/io.ksmt/ksmt-core/javadoc.svg)](https://javadoc.io/doc/io.ksmt/ksmt-core) ## Get started @@ -20,9 +20,9 @@ To start using KSMT, install it via [Gradle](https://gradle.org/): ```kotlin // core -implementation("io.ksmt:ksmt-core:0.5.9") +implementation("io.ksmt:ksmt-core:0.5.10") // z3 solver -implementation("io.ksmt:ksmt-z3:0.5.9") +implementation("io.ksmt:ksmt-z3:0.5.10") ``` Find basic instructions in the [Getting started](docs/getting-started.md) guide and try it out with the diff --git a/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts b/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts index fca1322f7..ea4191eeb 100644 --- a/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts +++ b/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts @@ -11,7 +11,7 @@ plugins { } group = "io.ksmt" -version = "0.5.9" +version = "0.5.10" repositories { mavenCentral() diff --git a/docs/getting-started.md b/docs/getting-started.md index 5a93254f3..0319e4d2d 100644 --- a/docs/getting-started.md +++ b/docs/getting-started.md @@ -34,7 +34,7 @@ repositories { ```kotlin dependencies { // core - implementation("io.ksmt:ksmt-core:0.5.9") + implementation("io.ksmt:ksmt-core:0.5.10") } ``` @@ -43,9 +43,9 @@ dependencies { ```kotlin dependencies { // z3 - implementation("io.ksmt:ksmt-z3:0.5.9") + implementation("io.ksmt:ksmt-z3:0.5.10") // bitwuzla - implementation("io.ksmt:ksmt-bitwuzla:0.5.9") + implementation("io.ksmt:ksmt-bitwuzla:0.5.10") } ``` diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts index 88bfe3edd..68c07f90e 100644 --- a/examples/build.gradle.kts +++ b/examples/build.gradle.kts @@ -9,11 +9,11 @@ repositories { dependencies { // core - implementation("io.ksmt:ksmt-core:0.5.9") + implementation("io.ksmt:ksmt-core:0.5.10") // z3 solver - implementation("io.ksmt:ksmt-z3:0.5.9") + implementation("io.ksmt:ksmt-z3:0.5.10") // Runner and portfolio solver - implementation("io.ksmt:ksmt-runner:0.5.9") + implementation("io.ksmt:ksmt-runner:0.5.10") } java { diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KBoolExprSimplifier.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KBoolExprSimplifier.kt index 7933c0f45..81b012048 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KBoolExprSimplifier.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KBoolExprSimplifier.kt @@ -78,6 +78,7 @@ interface KBoolExprSimplifier : KExprSimplifierBase { // Simplify argument and retry expr simplification if (simplifiedArgument == null) { + markExpressionAsNotTransformed() expr.transformAfter(argument) return expr } @@ -92,6 +93,7 @@ interface KBoolExprSimplifier : KExprSimplifierBase { expr.processNextArgument() // Repeat simplification with next argument + markExpressionAsNotTransformed() retryExprTransformation(expr) return expr diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveTransformerBase.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveTransformerBase.kt index 288280cee..00abc2a83 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveTransformerBase.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveTransformerBase.kt @@ -27,7 +27,7 @@ import java.util.IdentityHashMap * a [transformExprAfterTransformed] method. * */ abstract class KNonRecursiveTransformerBase: KTransformer { - private val transformed = IdentityHashMap, KExpr<*>>() + private var transformed = IdentityHashMap, KExpr<*>>() private val exprStack = ArrayList>() private var exprWasTransformed = false @@ -41,7 +41,7 @@ abstract class KNonRecursiveTransformerBase: KTransformer { while (exprStack.size > initialStackSize) { val e = exprStack.removeLast() - val cachedExpr = transformedExpr(expr) + val cachedExpr = transformedExpr(e) if (cachedExpr != null) { continue } @@ -63,6 +63,14 @@ abstract class KNonRecursiveTransformerBase: KTransformer { return transformedExpr(expr) ?: error("expr was not properly transformed: $expr") } + /** + * Reset transformer expression cache. + * */ + fun resetCache() { + check(exprStack.isEmpty()) { "Can not reset cache during expression transformation" } + transformed = IdentityHashMap() + } + /** * Disable [KTransformer] transformApp implementation since it is incorrect * for non-recursive usage. diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveVisitorBase.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveVisitorBase.kt index 4e453bfc3..70a462833 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveVisitorBase.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveVisitorBase.kt @@ -22,7 +22,7 @@ import java.util.IdentityHashMap * a [visitExprAfterVisited] method. * */ abstract class KNonRecursiveVisitorBase : KVisitor> { - private val visitResults = IdentityHashMap, V>() + private var visitResults = IdentityHashMap, V>() private val exprStack = ArrayList>() private var lastVisitedExpr: KExpr<*>? = null @@ -100,6 +100,14 @@ abstract class KNonRecursiveVisitorBase : KVisitor> return expr } + /** + * Reset visitor expression cache. + * */ + fun resetCache() { + check(exprStack.isEmpty()) { "Can not reset cache during expression visit" } + visitResults = IdentityHashMap() + } + /** * Disable [KVisitor] visitApp implementation since it is incorrect * for non-recursive usage. diff --git a/ksmt-core/src/main/kotlin/io/ksmt/solver/KSolver.kt b/ksmt-core/src/main/kotlin/io/ksmt/solver/KSolver.kt index 21a641d68..1efda992f 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/solver/KSolver.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/solver/KSolver.kt @@ -20,6 +20,15 @@ interface KSolver : AutoCloseable { @JvmName("assertExpr") fun assert(expr: KExpr) + + /** + * Assert multiple expressions into solver. + * + * @see check + * */ + @JvmName("assertExprs") + fun assert(exprs: List>) = exprs.forEach { assert(it) } + /** * Assert an expression into solver and track it in unsat cores. * @@ -28,6 +37,14 @@ interface KSolver : AutoCloseable { * */ fun assertAndTrack(expr: KExpr) + /** + * Assert multiple expressions into solver and track them in unsat cores. + * + * @see checkWithAssumptions + * @see unsatCore + * */ + fun assertAndTrack(exprs: List>) = exprs.forEach { assertAndTrack(it) } + /** * Create a backtracking point for assertion stack. * diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/runner/generated/models/SolverProtocolModel.Generated.kt b/ksmt-runner/src/main/kotlin/io/ksmt/runner/generated/models/SolverProtocolModel.Generated.kt index 3e06be7f2..89b598d49 100644 --- a/ksmt-runner/src/main/kotlin/io/ksmt/runner/generated/models/SolverProtocolModel.Generated.kt +++ b/ksmt-runner/src/main/kotlin/io/ksmt/runner/generated/models/SolverProtocolModel.Generated.kt @@ -22,7 +22,9 @@ class SolverProtocolModel private constructor( private val _deleteSolver: RdCall, private val _configure: RdCall, Unit>, private val _assert: RdCall, + private val _bulkAssert: RdCall, private val _assertAndTrack: RdCall, + private val _bulkAssertAndTrack: RdCall, private val _push: RdCall, private val _pop: RdCall, private val _check: RdCall, @@ -40,6 +42,7 @@ class SolverProtocolModel private constructor( serializers.register(CreateSolverParams) serializers.register(SolverConfigurationParam) serializers.register(AssertParams) + serializers.register(BulkAssertParams) serializers.register(PopParams) serializers.register(CheckParams) serializers.register(CheckResult) @@ -77,7 +80,7 @@ class SolverProtocolModel private constructor( private val __SolverConfigurationParamListSerializer = SolverConfigurationParam.list() - const val serializationHash = 9141130720080102681L + const val serializationHash = 6588187342629653927L } override val serializersOwner: ISerializersOwner get() = SolverProtocolModel @@ -105,11 +108,21 @@ class SolverProtocolModel private constructor( */ val assert: RdCall get() = _assert + /** + * Assert multiple expressions + */ + val bulkAssert: RdCall get() = _bulkAssert + /** * Assert and track expression */ val assertAndTrack: RdCall get() = _assertAndTrack + /** + * Assert and track multiple expressions + */ + val bulkAssertAndTrack: RdCall get() = _bulkAssertAndTrack + /** * Solver push */ @@ -156,7 +169,9 @@ class SolverProtocolModel private constructor( _deleteSolver.async = true _configure.async = true _assert.async = true + _bulkAssert.async = true _assertAndTrack.async = true + _bulkAssertAndTrack.async = true _push.async = true _pop.async = true _check.async = true @@ -172,7 +187,9 @@ class SolverProtocolModel private constructor( bindableChildren.add("deleteSolver" to _deleteSolver) bindableChildren.add("configure" to _configure) bindableChildren.add("assert" to _assert) + bindableChildren.add("bulkAssert" to _bulkAssert) bindableChildren.add("assertAndTrack" to _assertAndTrack) + bindableChildren.add("bulkAssertAndTrack" to _bulkAssertAndTrack) bindableChildren.add("push" to _push) bindableChildren.add("pop" to _pop) bindableChildren.add("check" to _check) @@ -190,7 +207,9 @@ class SolverProtocolModel private constructor( RdCall(FrameworkMarshallers.Void, FrameworkMarshallers.Void), RdCall, Unit>(__SolverConfigurationParamListSerializer, FrameworkMarshallers.Void), RdCall(AssertParams, FrameworkMarshallers.Void), + RdCall(BulkAssertParams, FrameworkMarshallers.Void), RdCall(AssertParams, FrameworkMarshallers.Void), + RdCall(BulkAssertParams, FrameworkMarshallers.Void), RdCall(FrameworkMarshallers.Void, FrameworkMarshallers.Void), RdCall(PopParams, FrameworkMarshallers.Void), RdCall(CheckParams, CheckResult), @@ -211,7 +230,9 @@ class SolverProtocolModel private constructor( print("deleteSolver = "); _deleteSolver.print(printer); println() print("configure = "); _configure.print(printer); println() print("assert = "); _assert.print(printer); println() + print("bulkAssert = "); _bulkAssert.print(printer); println() print("assertAndTrack = "); _assertAndTrack.print(printer); println() + print("bulkAssertAndTrack = "); _bulkAssertAndTrack.print(printer); println() print("push = "); _push.print(printer); println() print("pop = "); _pop.print(printer); println() print("check = "); _check.print(printer); println() @@ -230,7 +251,9 @@ class SolverProtocolModel private constructor( _deleteSolver.deepClonePolymorphic(), _configure.deepClonePolymorphic(), _assert.deepClonePolymorphic(), + _bulkAssert.deepClonePolymorphic(), _assertAndTrack.deepClonePolymorphic(), + _bulkAssertAndTrack.deepClonePolymorphic(), _push.deepClonePolymorphic(), _pop.deepClonePolymorphic(), _check.deepClonePolymorphic(), @@ -305,7 +328,64 @@ data class AssertParams ( /** - * #### Generated from [SolverProtocolModel.kt:55] + * #### Generated from [SolverProtocolModel.kt:51] + */ +data class BulkAssertParams ( + val expressions: List +) : IPrintable { + //companion + + companion object : IMarshaller { + override val _type: KClass = BulkAssertParams::class + + @Suppress("UNCHECKED_CAST") + override fun read(ctx: SerializationCtx, buffer: AbstractBuffer): BulkAssertParams { + val expressions = buffer.readList { (ctx.serializers.get(io.ksmt.runner.serializer.AstSerializationCtx.marshallerId)!! as IMarshaller).read(ctx, buffer) } + return BulkAssertParams(expressions) + } + + override fun write(ctx: SerializationCtx, buffer: AbstractBuffer, value: BulkAssertParams) { + buffer.writeList(value.expressions) { v -> (ctx.serializers.get(io.ksmt.runner.serializer.AstSerializationCtx.marshallerId)!! as IMarshaller).write(ctx,buffer, v) } + } + + + } + //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 BulkAssertParams + + if (expressions != other.expressions) return false + + return true + } + //hash code trait + override fun hashCode(): Int { + var __r = 0 + __r = __r*31 + expressions.hashCode() + return __r + } + //pretty print + override fun print(printer: PrettyPrinter) { + printer.println("BulkAssertParams (") + printer.indent { + print("expressions = "); expressions.print(printer); println() + } + printer.print(")") + } + //deepClone + //contexts +} + + +/** + * #### Generated from [SolverProtocolModel.kt:59] */ data class CheckParams ( val timeout: Long @@ -362,7 +442,7 @@ data class CheckParams ( /** - * #### Generated from [SolverProtocolModel.kt:59] + * #### Generated from [SolverProtocolModel.kt:63] */ data class CheckResult ( val status: io.ksmt.solver.KSolverStatus @@ -419,7 +499,7 @@ data class CheckResult ( /** - * #### Generated from [SolverProtocolModel.kt:63] + * #### Generated from [SolverProtocolModel.kt:67] */ data class CheckWithAssumptionsParams ( val assumptions: List, @@ -587,7 +667,7 @@ data class CreateSolverParams ( /** - * #### Generated from [SolverProtocolModel.kt:82] + * #### Generated from [SolverProtocolModel.kt:86] */ data class ModelEntry ( val decl: io.ksmt.KAst, @@ -662,7 +742,7 @@ data class ModelEntry ( /** - * #### Generated from [SolverProtocolModel.kt:76] + * #### Generated from [SolverProtocolModel.kt:80] */ data class ModelFuncInterpEntry ( val hasVars: Boolean, @@ -731,7 +811,7 @@ data class ModelFuncInterpEntry ( /** - * #### Generated from [SolverProtocolModel.kt:94] + * #### Generated from [SolverProtocolModel.kt:98] */ data class ModelResult ( val declarations: List, @@ -800,7 +880,7 @@ data class ModelResult ( /** - * #### Generated from [SolverProtocolModel.kt:89] + * #### Generated from [SolverProtocolModel.kt:93] */ data class ModelUninterpretedSortUniverse ( val sort: io.ksmt.KAst, @@ -863,7 +943,7 @@ data class ModelUninterpretedSortUniverse ( /** - * #### Generated from [SolverProtocolModel.kt:51] + * #### Generated from [SolverProtocolModel.kt:55] */ data class PopParams ( val levels: UInt @@ -920,7 +1000,7 @@ data class PopParams ( /** - * #### Generated from [SolverProtocolModel.kt:72] + * #### Generated from [SolverProtocolModel.kt:76] */ data class ReasonUnknownResult ( val reasonUnknown: String @@ -1063,7 +1143,7 @@ enum class SolverType { /** - * #### Generated from [SolverProtocolModel.kt:68] + * #### Generated from [SolverProtocolModel.kt:72] */ data class UnsatCoreResult ( val core: List diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/solver/async/KAsyncSolver.kt b/ksmt-runner/src/main/kotlin/io/ksmt/solver/async/KAsyncSolver.kt index 6728916ef..7287091de 100644 --- a/ksmt-runner/src/main/kotlin/io/ksmt/solver/async/KAsyncSolver.kt +++ b/ksmt-runner/src/main/kotlin/io/ksmt/solver/async/KAsyncSolver.kt @@ -14,8 +14,12 @@ interface KAsyncSolver : KSolver { suspend fun assertAsync(expr: KExpr) + suspend fun assertAsync(exprs: List>) = exprs.forEach { assertAsync(it) } + suspend fun assertAndTrackAsync(expr: KExpr) + suspend fun assertAndTrackAsync(exprs: List>) = exprs.forEach { assertAndTrackAsync(it) } + suspend fun pushAsync() suspend fun popAsync(n: UInt) diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/solver/portfolio/KPortfolioSolver.kt b/ksmt-runner/src/main/kotlin/io/ksmt/solver/portfolio/KPortfolioSolver.kt index 7b3c8810e..161a5b1ef 100644 --- a/ksmt-runner/src/main/kotlin/io/ksmt/solver/portfolio/KPortfolioSolver.kt +++ b/ksmt-runner/src/main/kotlin/io/ksmt/solver/portfolio/KPortfolioSolver.kt @@ -106,10 +106,18 @@ class KPortfolioSolver( assertAsync(expr) } + override fun assert(exprs: List>) = runBlocking { + assertAsync(exprs) + } + override fun assertAndTrack(expr: KExpr) = runBlocking { assertAndTrackAsync(expr) } + override fun assertAndTrack(exprs: List>) = runBlocking { + assertAndTrackAsync(exprs) + } + override fun push() = runBlocking { pushAsync() } @@ -153,10 +161,18 @@ class KPortfolioSolver( assertAsync(expr) } + override suspend fun assertAsync(exprs: List>) = solverOperation { + assertAsync(exprs) + } + override suspend fun assertAndTrackAsync(expr: KExpr) = solverOperation { assertAndTrackAsync(expr) } + override suspend fun assertAndTrackAsync(exprs: List>) = solverOperation { + assertAndTrackAsync(exprs) + } + override suspend fun pushAsync() = solverOperation { pushAsync() } diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunner.kt b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunner.kt index 418a47505..e77ee03f7 100644 --- a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunner.kt +++ b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunner.kt @@ -101,18 +101,47 @@ class KSolverRunner( } } - override suspend fun assertAndTrackAsync(expr: KExpr) = assertAndTrack(expr) { e -> - ensureInitializedAndExecuteAsync(onException = {}) { - assertAndTrackAsync(e) + override suspend fun assertAsync(exprs: List>) = + bulkAssert(exprs) { e -> + ensureInitializedAndExecuteAsync(onException = {}) { + bulkAssertAsync(e) + } } - } - override fun assertAndTrack(expr: KExpr) = assertAndTrack(expr) { e -> - ensureInitializedAndExecuteSync(onException = {}) { - assertAndTrackSync(e) + override fun assert(exprs: List>) = + bulkAssert(exprs) { e -> + ensureInitializedAndExecuteSync(onException = {}) { + bulkAssertSync(e) + } + } + + private inline fun bulkAssert( + exprs: List>, + execute: (List>) -> Unit + ) { + ctx.ensureContextMatch(exprs) + + try { + execute(exprs) + } finally { + exprs.forEach { solverState.assert(it) } } } + override suspend fun assertAndTrackAsync(expr: KExpr) = + assertAndTrack(expr) { e -> + ensureInitializedAndExecuteAsync(onException = {}) { + assertAndTrackAsync(e) + } + } + + override fun assertAndTrack(expr: KExpr) = + assertAndTrack(expr) { e -> + ensureInitializedAndExecuteSync(onException = {}) { + assertAndTrackSync(e) + } + } + private inline fun assertAndTrack( expr: KExpr, execute: (KExpr) -> Unit @@ -126,6 +155,33 @@ class KSolverRunner( } } + override suspend fun assertAndTrackAsync(exprs: List>) = + bulkAssertAndTrack(exprs) { e -> + ensureInitializedAndExecuteAsync(onException = {}) { + bulkAssertAndTrackAsync(e) + } + } + + override fun assertAndTrack(exprs: List>) = + bulkAssertAndTrack(exprs) { e -> + ensureInitializedAndExecuteSync(onException = {}) { + bulkAssertAndTrackSync(e) + } + } + + private inline fun bulkAssertAndTrack( + exprs: List>, + execute: (List>) -> Unit + ) { + ctx.ensureContextMatch(exprs) + + try { + execute(exprs) + } finally { + exprs.forEach { solverState.assertAndTrack(it) } + } + } + override suspend fun pushAsync() = push { executeIfInitialized(onException = {}) { pushAsync() diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunnerExecutor.kt b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunnerExecutor.kt index d24eb5383..328cc9cbf 100644 --- a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunnerExecutor.kt +++ b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverRunnerExecutor.kt @@ -16,6 +16,7 @@ import io.ksmt.expr.KExpr import io.ksmt.expr.KUninterpretedSortValue import io.ksmt.runner.core.KsmtWorkerSession import io.ksmt.runner.generated.models.AssertParams +import io.ksmt.runner.generated.models.BulkAssertParams import io.ksmt.runner.generated.models.CheckParams import io.ksmt.runner.generated.models.CheckResult import io.ksmt.runner.generated.models.CheckWithAssumptionsParams @@ -92,6 +93,25 @@ class KSolverRunnerExecutor( query(AssertParams(expr)) } + fun bulkAssertSync(exprs: List>) = bulkAssert(exprs) { params -> + queryWithTimeoutAndExceptionHandlingSync { + bulkAssert.querySync(params) + } + } + + suspend fun bulkAssertAsync(exprs: List>) = bulkAssert(exprs) { params -> + queryWithTimeoutAndExceptionHandlingAsync { + bulkAssert.queryAsync(params) + } + } + + private inline fun bulkAssert(exprs: List>, query: (BulkAssertParams) -> Unit) { + if (exprs.isEmpty()) return + + ensureActive() + query(BulkAssertParams(exprs)) + } + fun assertAndTrackSync(expr: KExpr) = assertAndTrack(expr) { params -> queryWithTimeoutAndExceptionHandlingSync { assertAndTrack.querySync(params) @@ -109,6 +129,25 @@ class KSolverRunnerExecutor( query(AssertParams(expr)) } + fun bulkAssertAndTrackSync(exprs: List>) = bulkAssertAndTrack(exprs) { params -> + queryWithTimeoutAndExceptionHandlingSync { + bulkAssertAndTrack.querySync(params) + } + } + + suspend fun bulkAssertAndTrackAsync(exprs: List>) = bulkAssertAndTrack(exprs) { params -> + queryWithTimeoutAndExceptionHandlingAsync { + bulkAssertAndTrack.queryAsync(params) + } + } + + private inline fun bulkAssertAndTrack(exprs: List>, query: (BulkAssertParams) -> Unit) { + if (exprs.isEmpty()) return + + ensureActive() + query(BulkAssertParams(exprs)) + } + fun pushSync() = push { queryWithTimeoutAndExceptionHandlingSync { push.querySync(Unit) diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverState.kt b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverState.kt index 5afa0d518..23ad6262a 100644 --- a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverState.kt +++ b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverState.kt @@ -18,21 +18,22 @@ import java.util.concurrent.ConcurrentLinkedQueue * We don't consider last check-sat result as a solver state. * */ class KSolverState { - private sealed interface AssertFrame - private data class ExprAssertFrame(val expr: KExpr) : AssertFrame - private data class AssertAndTrackFrame(val expr: KExpr) : AssertFrame + private class AssertionFrame( + val asserted: ConcurrentLinkedQueue> = ConcurrentLinkedQueue(), + val tracked: ConcurrentLinkedQueue> = ConcurrentLinkedQueue(), + ) private val configuration = ConcurrentLinkedQueue() /** * Asserted expressions. - * Each nested queue contains expressions of the + * Each nested assertion frame contains expressions of the * corresponding assertion level. * */ - private val assertFrames = ConcurrentLinkedDeque>() + private val assertFrames = ConcurrentLinkedDeque() init { - assertFrames.addLast(ConcurrentLinkedQueue()) + assertFrames.addLast(AssertionFrame()) } fun configure(config: List) { @@ -40,15 +41,15 @@ class KSolverState { } fun assert(expr: KExpr) { - assertFrames.last.add(ExprAssertFrame(expr)) + assertFrames.last.asserted.add(expr) } fun assertAndTrack(expr: KExpr) { - assertFrames.last.add(AssertAndTrackFrame(expr)) + assertFrames.last.tracked.add(expr) } fun push() { - assertFrames.addLast(ConcurrentLinkedQueue()) + assertFrames.addLast(AssertionFrame()) } fun pop(n: UInt) { @@ -60,15 +61,15 @@ class KSolverState { suspend fun applyAsync(executor: KSolverRunnerExecutor) = replayState( configureSolver = { executor.configureAsync(it) }, pushScope = { executor.pushAsync() }, - assertExpr = { executor.assertAsync(it) }, - assertExprAndTrack = { expr -> executor.assertAndTrackAsync(expr) } + assertExprs = { executor.bulkAssertAsync(it) }, + assertExprsAndTrack = { expr -> executor.bulkAssertAndTrackAsync(expr) } ) fun applySync(executor: KSolverRunnerExecutor) = replayState( configureSolver = { executor.configureSync(it) }, pushScope = { executor.pushSync() }, - assertExpr = { executor.assertSync(it) }, - assertExprAndTrack = { expr -> executor.assertAndTrackSync(expr) } + assertExprs = { executor.bulkAssertSync(it) }, + assertExprsAndTrack = { expr -> executor.bulkAssertAndTrackSync(expr) } ) /** @@ -78,8 +79,8 @@ class KSolverState { private inline fun replayState( configureSolver: (List) -> Unit, pushScope: () -> Unit, - assertExpr: (KExpr) -> Unit, - assertExprAndTrack: (KExpr) -> Unit + assertExprs: (List>) -> Unit, + assertExprsAndTrack: (List>) -> Unit ) { if (configuration.isNotEmpty()) { configureSolver(configuration.toList()) @@ -93,12 +94,8 @@ class KSolverState { } firstFrame = false - for (assertion in frame) { - when (assertion) { - is ExprAssertFrame -> assertExpr(assertion.expr) - is AssertAndTrackFrame -> assertExprAndTrack(assertion.expr) - } - } + assertExprs(frame.asserted.toList()) + assertExprsAndTrack(frame.tracked.toList()) } } } diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverWorkerProcess.kt b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverWorkerProcess.kt index b5f6125eb..2506d578a 100644 --- a/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverWorkerProcess.kt +++ b/ksmt-runner/src/main/kotlin/io/ksmt/solver/runner/KSolverWorkerProcess.kt @@ -85,10 +85,18 @@ class KSolverWorkerProcess : ChildProcessBase() { @Suppress("UNCHECKED_CAST") solver.assert(params.expression as KExpr) } + bulkAssert.measureExecutionForTermination { params -> + @Suppress("UNCHECKED_CAST") + solver.assert(params.expressions as List>) + } assertAndTrack.measureExecutionForTermination { params -> @Suppress("UNCHECKED_CAST") solver.assertAndTrack(params.expression as KExpr) } + bulkAssertAndTrack.measureExecutionForTermination { params -> + @Suppress("UNCHECKED_CAST") + solver.assertAndTrack(params.expressions as List>) + } push.measureExecutionForTermination { solver.push() } diff --git a/ksmt-runner/src/main/rdgen/io/ksmt/runner/models/SolverProtocolModel.kt b/ksmt-runner/src/main/rdgen/io/ksmt/runner/models/SolverProtocolModel.kt index d434b1fdc..f6c1dfa79 100644 --- a/ksmt-runner/src/main/rdgen/io/ksmt/runner/models/SolverProtocolModel.kt +++ b/ksmt-runner/src/main/rdgen/io/ksmt/runner/models/SolverProtocolModel.kt @@ -48,6 +48,10 @@ object SolverProtocolModel : Ext(SolverProtocolRoot) { field("expression", kastType) } + private val bulkAssertParams = structdef { + field("expressions", immutableList(kastType)) + } + private val popParams = structdef { field("levels", PredefinedType.uint) } @@ -114,10 +118,18 @@ object SolverProtocolModel : Ext(SolverProtocolRoot) { async documentation = "Assert expression" } + call("bulkAssert", bulkAssertParams, PredefinedType.void).apply { + async + documentation = "Assert multiple expressions" + } call("assertAndTrack", assertParams, PredefinedType.void).apply { async documentation = "Assert and track expression" } + call("bulkAssertAndTrack", bulkAssertParams, PredefinedType.void).apply { + async + documentation = "Assert and track multiple expressions" + } call("push", PredefinedType.void, PredefinedType.void).apply { async documentation = "Solver push" diff --git a/ksmt-runner/src/test/kotlin/io/ksmt/solver/runner/SolverRunnerTest.kt b/ksmt-runner/src/test/kotlin/io/ksmt/solver/runner/SolverRunnerTest.kt index f7c7625d1..92083faf8 100644 --- a/ksmt-runner/src/test/kotlin/io/ksmt/solver/runner/SolverRunnerTest.kt +++ b/ksmt-runner/src/test/kotlin/io/ksmt/solver/runner/SolverRunnerTest.kt @@ -153,6 +153,29 @@ class SolverRunnerTest { assertEquals(model1, model3) } + @Test + fun testBulkAssert(): Unit = with(context) { + val a = boolSort.mkConst("a") + val b = boolSort.mkConst("b") + val c = boolSort.mkConst("c") + + val e1 = (a and b) or c + val e2 = !(a and b) + val e3 = !c + + solver.push() + solver.assert(listOf(e1, e2, e3)) + assertEquals(KSolverStatus.UNSAT, solver.check()) + solver.pop() + + solver.push() + solver.assertAndTrack(listOf(e1, e2, e3)) + assertEquals(KSolverStatus.UNSAT, solver.check()) + + val core = solver.unsatCore() + assertTrue(core.isNotEmpty()) + } + @Test fun testSolverInstanceCreation(): Unit = with(context){ SolverType.Z3.createInstance(this)