diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index e991dc45e..bef5b9477 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -31,4 +31,5 @@ jobs: ksmt-core/build/release/**/ksmt-core-*.jar ksmt-z3/build/release/**/ksmt-z3-*.jar ksmt-bitwuzla/build/release/**/ksmt-bitwuzla-*.jar + ksmt-runner/build/release/**/ksmt-runner-*.jar diff --git a/.github/workflows/run-long-tests.yml b/.github/workflows/run-long-tests.yml index da248d381..056bd7c7e 100644 --- a/.github/workflows/run-long-tests.yml +++ b/.github/workflows/run-long-tests.yml @@ -20,6 +20,9 @@ on: type: number default: 170000 +env: + TEST_DATA_REVISION: 0.2.1 + jobs: setup: runs-on: ubuntu-latest @@ -58,35 +61,57 @@ jobs: TEST_ARRAY+="]" echo "tests=$TEST_ARRAY" >> $GITHUB_OUTPUT - run_tests: - needs: setup - continue-on-error: true + prepare_test_data: strategy: matrix: os: [ ubuntu-latest, windows-latest ] - test: ${{ fromJSON(needs.setup.outputs.matrix-tests) }} - chunk: ${{ fromJSON(needs.setup.outputs.matrix-chunks) }} - - name: Run ${{ matrix.test }}[${{ matrix.chunk }}] on ${{ matrix.os }} runs-on: ${{ matrix.os }} steps: - uses: actions/checkout@v3 + - name: Prepare test data (cache) + id: test-data-cache + uses: actions/cache@v3 + env: + cache-name: cache-test-data + with: + key: test-data-${{ env.TEST_DATA_REVISION }}-${{ matrix.os }} + path: ksmt-test/testData/testData.zip + - name: Set up JDK 1.8 + if: steps.test-data-cache.outputs.cache-hit != 'true' uses: actions/setup-java@v3 with: java-version: 8 distribution: 'zulu' cache: gradle - - name: Build project + - name: Prepare test data (download) + if: steps.test-data-cache.outputs.cache-hit != 'true' uses: gradle/gradle-build-action@v2 with: arguments: | - build + :ksmt-test:downloadPreparedSmtLibBenchmarkTestData --no-daemon + -PtestDataRevision=${{ env.TEST_DATA_REVISION }} + + run_tests: + needs: [setup, prepare_test_data] + continue-on-error: true + strategy: + matrix: + os: [ ubuntu-latest, windows-latest ] + test: ${{ fromJSON(needs.setup.outputs.matrix-tests) }} + chunk: ${{ fromJSON(needs.setup.outputs.matrix-chunks) }} + + name: Run ${{ matrix.test }}[${{ matrix.chunk }}] on ${{ matrix.os }} + + runs-on: ${{ matrix.os }} + + steps: + - uses: actions/checkout@v3 - name: Prepare test data (cache) id: test-data-cache @@ -94,17 +119,37 @@ jobs: env: cache-name: cache-test-data with: - key: test-data-0.2.1-${{ matrix.os }} - path: ksmt-test/testData + key: test-data-${{ env.TEST_DATA_REVISION }}-${{ matrix.os }} + path: ksmt-test/testData/testData.zip - - name: Prepare test data (download) + - name: Check test data downloaded if: steps.test-data-cache.outputs.cache-hit != 'true' + run: | + echo "Test data is not available" + exit 1 + + - name: Set up JDK 1.8 + uses: actions/setup-java@v3 + with: + java-version: 8 + distribution: 'zulu' + cache: gradle + + # Since ksmt-test/testData/testData.zip exists task will not download it again + - name: Prepare test data (unpack) uses: gradle/gradle-build-action@v2 with: arguments: | :ksmt-test:downloadPreparedSmtLibBenchmarkTestData --no-daemon - -PtestDataRevision=0.2.1 + -PtestDataRevision=${{ env.TEST_DATA_REVISION }} + + - name: Build project + uses: gradle/gradle-build-action@v2 + with: + arguments: | + build + --no-daemon - name: Run ${{ matrix.test }} uses: gradle/gradle-build-action@v2 diff --git a/README.md b/README.md index 82bc7e9da..c69bd7573 100644 --- a/README.md +++ b/README.md @@ -14,9 +14,9 @@ repositories { } // core -implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.2.1") +implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.3.0") // z3 solver -implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.2.1") +implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.3.0") ``` ## Usage @@ -52,8 +52,8 @@ val array by mkArraySort(intSort, intSort) val index by intSort val value by intSort -val expr = (array.select(index - 1.intExpr) lt value) and - (array.select(index + 1.intExpr) gt value) +val expr = (array.select(index - 1.expr) lt value) and + (array.select(index + 1.expr) gt value) ``` Check out our [example project](examples) for more complicated examples. diff --git a/Requirements.md b/Requirements.md index 0365871ba..2bd1ea5f8 100644 --- a/Requirements.md +++ b/Requirements.md @@ -13,7 +13,7 @@ | [CVC5 solver support](#cvc5-solver-support) | TODO | | [External process runner](#external-process-runner) | Done | | [Portfolio solver](#portfolio-solver) | TODO | -| [Solver configuration API](#solver-configuration-api) | In progress | +| [Solver configuration API](#solver-configuration-api) | Done | | [Deployment](#deployment) | Done partially | | [Expression simplification / evaluation](#expression-simplification--evaluation) | Done partially | | [Performance tests](#performance-tests) | TODO | diff --git a/buildSrc/src/main/kotlin/SmtLibBenchmarkUtil.kt b/buildSrc/src/main/kotlin/SmtLibBenchmarkUtil.kt index c198a2032..c30652026 100644 --- a/buildSrc/src/main/kotlin/SmtLibBenchmarkUtil.kt +++ b/buildSrc/src/main/kotlin/SmtLibBenchmarkUtil.kt @@ -54,19 +54,16 @@ fun Project.usePreparedSmtLibBenchmarkTestData(path: File) = tasks.register("smt } } -fun Project.downloadPreparedSmtLibBenchmarkTestData(path: File, version: String) = +fun Project.downloadPreparedSmtLibBenchmarkTestData(downloadPath: File, testDataPath: File, version: String) = tasks.register("downloadPreparedSmtLibBenchmarkTestData") { doLast { - path.mkdir() - val benchmarksUrl = "https://github.com/UnitTestBot/ksmt/releases/download/$version/benchmarks.zip" - val downloadPath = buildDir.resolve("benchmarks.zip") download(benchmarksUrl, downloadPath) copy { from(zipTree(downloadPath)) - into(path) + into(testDataPath) duplicatesStrategy = DuplicatesStrategy.EXCLUDE } } 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 3e9d97df4..6d55fe529 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.2.1" +version = "0.3.0" repositories { mavenCentral() diff --git a/docs/getting-started.md b/docs/getting-started.md index 779a88b6f..52949544e 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.2.1") + implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.3.0") } ``` @@ -26,9 +26,9 @@ dependencies { ```kotlin dependencies { // z3 - implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.2.1") + implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.3.0") // bitwuzla - implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.2.1") + implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.3.0") } ``` SMT solver specific packages are provided with solver native binaries. @@ -51,6 +51,8 @@ In this example, we want to create an expression over Boolean variable `a` and integer variables `b` and `c`. ```kotlin +import org.ksmt.utils.getValue + with(ctx) { // create symbolic variables val a by boolSort @@ -58,12 +60,15 @@ with(ctx) { val c by intSort // create expression - val constraint = a and (b ge c + 3.intExpr) + val constraint = a and (b ge c + 3.expr) } ``` All KSMT expressions are typed and incorrect terms (e.g. `and` with integer arguments) result in a compile-time error. +Note the use of `import getValue`, which is required for the `by` syntax. +Alternatively, `mkConst(name, sort)` can be used. + ### Working with SMT solvers To check SMT formula satisfiability we need to instantiate an SMT solver. @@ -112,10 +117,10 @@ with(ctx) { // create symbolic variables val cond1 by boolSort val cond2 by boolSort - val a by mkBv32Sort() - val b by mkBv32Sort() - val c by mkBv32Sort() - val goal by mkBv32Sort() + val a by bv32Sort + val b by bv32Sort + val c by bv32Sort + val goal by bv32Sort KZ3Solver(this).use { solver -> // a == 0 @@ -212,10 +217,10 @@ with(ctx) { // create symbolic variables val cond1 by boolSort val cond2 by boolSort - val a by mkBv32Sort() - val b by mkBv32Sort() - val c by mkBv32Sort() - val goal by mkBv32Sort() + val a by bv32Sort + val b by bv32Sort + val c by bv32Sort + val goal by bv32Sort KZ3Solver(this).use { solver -> // a == 0 @@ -357,3 +362,21 @@ with(ctx) { val assertions = KZ3SMTLibParser().parse(formula) } ``` + +### Solver configuration + +KSMT provides an API for modifying solver-specific parameters. +Since the parameters and their correct values are solver-specific +KSMT does not perform any checks. +See the corresponding solver documentation for a list of available options. + +```kotlin +with(ctx) { + KZ3Solver(this).use { solver -> + solver.configure { + // set Z3 solver parameter random_seed to 42 + setZ3Option("random_seed", 42) + } + } +} +``` diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts index ae5e8bd83..5559de3d3 100644 --- a/examples/build.gradle.kts +++ b/examples/build.gradle.kts @@ -1,6 +1,6 @@ plugins { kotlin("jvm") version "1.7.20" - `java-library` + java } repositories { @@ -10,9 +10,9 @@ repositories { dependencies { // core - implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.2.1") + implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.3.0") // z3 solver - implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.2.1") + implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.3.0") } java { diff --git a/examples/src/main/java/Sudoku.java b/examples/src/main/java/Sudoku.java index 9d9baa879..766cd7edf 100644 --- a/examples/src/main/java/Sudoku.java +++ b/examples/src/main/java/Sudoku.java @@ -53,7 +53,7 @@ public static void main(String[] args) { final List> symbolAssignments = assignSymbols(ctx, symbols, initialGrid); // Create Z3 SMT solver instance. - try (final KSolver solver = new KZ3Solver(ctx)) { + try (final KSolver solver = new KZ3Solver(ctx)) { // Assert all constraints. rules.forEach(solver::assertExpr); symbolAssignments.forEach(solver::assertExpr); @@ -79,7 +79,7 @@ private static List>> createSymbolicGrid(final KContext ctx for (int row = 0; row < SIZE; row++) { final List> gridRow = new ArrayList<>(); for (int col = 0; col < SIZE; col++) { - gridRow.add(ctx.mkConst(ctx.getIntSort(), "x_" + row + "_" + col)); + gridRow.add(ctx.mkConst("x_" + row + "_" + col, ctx.getIntSort())); } grid.add(gridRow); } @@ -93,8 +93,8 @@ private static List> sudokuRules(final KContext ctx, final Stream> symbolConstraints = symbols .stream().flatMap(Collection::stream) .map(cell -> ctx.and( - ctx.ge(cell, ctx.getIntExpr(1)), - ctx.le(cell, ctx.getIntExpr(9)))); + ctx.ge(cell, ctx.getExpr(1)), + ctx.le(cell, ctx.getExpr(9)))); // Each row contains distinct numbers. final Stream> rowDistinctConstraints = symbols.stream() @@ -138,7 +138,7 @@ private static List> assignSymbols(final KContext ctx, for (int col = 0; col < SIZE; col++) { int cell = grid.get(row).get(col); if (cell != EMPTY_CELL_VALUE) { - assignments.add(ctx.eq(symbols.get(row).get(col), ctx.getIntExpr(cell))); + assignments.add(ctx.eq(symbols.get(row).get(col), ctx.getExpr(cell))); } } } diff --git a/examples/src/main/kotlin/GettingStartedExample.kt b/examples/src/main/kotlin/GettingStartedExample.kt index 5b799ef2c..32e617973 100644 --- a/examples/src/main/kotlin/GettingStartedExample.kt +++ b/examples/src/main/kotlin/GettingStartedExample.kt @@ -1,5 +1,6 @@ import org.ksmt.KContext import org.ksmt.solver.z3.KZ3Solver +import org.ksmt.utils.getValue import kotlin.time.Duration.Companion.seconds fun main() { @@ -22,7 +23,7 @@ private fun basicSolverUsageExample(ctx: KContext) = val c by intSort // create expression - val constraint = a and (b ge c + 3.intExpr) + val constraint = a and (b ge c + 3.expr) KZ3Solver(this).use { solver -> // create s Z3 Smt solver instance // assert expression @@ -46,10 +47,10 @@ private fun pushPopIncrementalExample(ctx: KContext) = // create symbolic variables val cond1 by boolSort val cond2 by boolSort - val a by mkBv32Sort() - val b by mkBv32Sort() - val c by mkBv32Sort() - val goal by mkBv32Sort() + val a by bv32Sort + val b by bv32Sort + val c by bv32Sort + val goal by bv32Sort KZ3Solver(this).use { solver -> // a == 0 @@ -138,10 +139,10 @@ private fun assumptionsIncrementalExample(ctx: KContext) = // create symbolic variables val cond1 by boolSort val cond2 by boolSort - val a by mkBv32Sort() - val b by mkBv32Sort() - val c by mkBv32Sort() - val goal by mkBv32Sort() + val a by bv32Sort + val b by bv32Sort + val c by bv32Sort + val goal by bv32Sort KZ3Solver(this).use { solver -> // a == 0 diff --git a/examples/src/main/kotlin/Sudoku.kt b/examples/src/main/kotlin/Sudoku.kt index 08d7451a8..747a03735 100644 --- a/examples/src/main/kotlin/Sudoku.kt +++ b/examples/src/main/kotlin/Sudoku.kt @@ -6,6 +6,7 @@ import org.ksmt.solver.KSolverStatus import org.ksmt.solver.z3.KZ3Solver import org.ksmt.sort.KBoolSort import org.ksmt.sort.KIntSort +import org.ksmt.utils.mkConst import kotlin.system.measureTimeMillis import kotlin.time.Duration.Companion.seconds @@ -85,7 +86,7 @@ fun main() = KContext().useWith { private fun KContext.sudokuRules(symbols: List>>): List> { // Each cell has a value from 1 to 9. - val symbolConstraints = symbols.flatten().map { (it ge 1.intExpr) and (it le 9.intExpr) } + val symbolConstraints = symbols.flatten().map { (it ge 1.expr) and (it le 9.expr) } // Each row contains distinct numbers. val rowDistinctConstraints = symbols.map { row -> mkDistinct(row) } @@ -118,7 +119,7 @@ private fun KContext.assignSymbols( sudokuIndices.flatMap { row -> sudokuIndices.mapNotNull { col -> val value = grid[row][col] - if (value != EMPTY_CELL_VALUE) symbols[row][col] eq value.intExpr else null + if (value != EMPTY_CELL_VALUE) symbols[row][col] eq value.expr else null } } diff --git a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaModel.kt b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaModel.kt index 77ce39a0a..ffcbf58f2 100644 --- a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaModel.kt +++ b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaModel.kt @@ -165,4 +165,12 @@ open class KBitwuzlaModel( return super.transformApp(expr) } } + + override fun toString(): String = detach().toString() + override fun hashCode(): Int = detach().hashCode() + override fun equals(other: Any?): Boolean { + if (this === other) return true + if (other !is KModel) return false + return detach() == other + } } 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 f1f7a6d46..c4ae43327 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 @@ -13,7 +13,7 @@ import org.ksmt.sort.KBoolSort import org.ksmt.utils.mkFreshConst import kotlin.time.Duration -open class KBitwuzlaSolver(private val ctx: KContext) : KSolver { +open class KBitwuzlaSolver(private val ctx: KContext) : KSolver { open val bitwuzlaCtx = KBitwuzlaContext() open val exprInternalizer: KBitwuzlaExprInternalizer by lazy { KBitwuzlaExprInternalizer(ctx, bitwuzlaCtx) @@ -31,6 +31,10 @@ open class KBitwuzlaSolver(private val ctx: KContext) : KSolver { private var currentLevelTrackedAssertions = hashSetOf() private val trackedAssertions = mutableListOf(currentLevelTrackedAssertions) + override fun configure(configurator: KBitwuzlaSolverConfiguration.() -> Unit) { + KBitwuzlaSolverConfigurationImpl(bitwuzlaCtx.bitwuzla).configurator() + } + override fun assert(expr: KExpr) = bitwuzlaCtx.bitwuzlaTry { val term = with(exprInternalizer) { expr.internalize() } Native.bitwuzlaAssert(bitwuzlaCtx.bitwuzla, term) diff --git a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaSolverConfiguration.kt b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaSolverConfiguration.kt new file mode 100644 index 000000000..be5aff8ae --- /dev/null +++ b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaSolverConfiguration.kt @@ -0,0 +1,21 @@ +package org.ksmt.solver.bitwuzla + +import org.ksmt.solver.KSolverConfiguration +import org.ksmt.solver.bitwuzla.bindings.Bitwuzla +import org.ksmt.solver.bitwuzla.bindings.BitwuzlaOption +import org.ksmt.solver.bitwuzla.bindings.Native + +interface KBitwuzlaSolverConfiguration : KSolverConfiguration { + fun setBitwuzlaOption(option: BitwuzlaOption, value: Int) + fun setBitwuzlaOption(option: BitwuzlaOption, value: String) +} + +class KBitwuzlaSolverConfigurationImpl(private val bitwuzla: Bitwuzla) : KBitwuzlaSolverConfiguration { + override fun setBitwuzlaOption(option: BitwuzlaOption, value: Int) { + Native.bitwuzlaSetOption(bitwuzla, option, value) + } + + override fun setBitwuzlaOption(option: BitwuzlaOption, value: String) { + Native.bitwuzlaSetOptionStr(bitwuzla, option, value) + } +} diff --git a/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt b/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt index 50204b571..dbbbe76c1 100644 --- a/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt +++ b/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt @@ -290,6 +290,7 @@ import org.ksmt.expr.KFunctionAsArray import org.ksmt.expr.KRealToFpExpr import org.ksmt.sort.KFpRoundingModeSort import org.ksmt.utils.BvUtils.bvMaxValueSigned +import org.ksmt.utils.BvUtils.minus import org.ksmt.utils.BvUtils.plus import org.ksmt.utils.booleanSignBit import org.ksmt.utils.cast @@ -1515,9 +1516,15 @@ open class KContext : AutoCloseable { private fun biasFp128Exponent(exponent: KBitVecValue<*>): KBitVecValue<*> = exponent + bvMaxValueSigned(KFp128Sort.exponentBits) + private fun unbiasFp128Exponent(exponent: KBitVecValue<*>): KBitVecValue<*> = + exponent - bvMaxValueSigned(KFp128Sort.exponentBits) + private fun biasFpCustomSizeExponent(exponent: KBitVecValue<*>, exponentSize: UInt): KBitVecValue<*> = exponent + bvMaxValueSigned(exponentSize) + private fun unbiasFpCustomSizeExponent(exponent: KBitVecValue<*>, exponentSize: UInt): KBitVecValue<*> = + exponent - bvMaxValueSigned(exponentSize) + fun mkFp(value: Float, sort: T): KExpr { if (sort == mkFp32Sort()) { return mkFp32(value).cast() @@ -2572,6 +2579,16 @@ open class KContext : AutoCloseable { fun mkFp128Decl(significandBits: KBitVecValue<*>, unbiasedExponent: KBitVecValue<*>, signBit: Boolean): KFp128Decl = fp128DeclCache.createIfContextActive(significandBits, unbiasedExponent, signBit) + fun mkFp128DeclBiased( + significandBits: KBitVecValue<*>, + biasedExponent: KBitVecValue<*>, + signBit: Boolean + ): KFp128Decl = mkFp128Decl( + significandBits = significandBits, + unbiasedExponent = unbiasFp128Exponent(biasedExponent), + signBit = signBit + ) + private val fpCustomSizeDeclCache = mkClosableCache { significandSize: UInt, exponentSize: UInt, significand: KBitVecValue<*>, @@ -2622,6 +2639,20 @@ open class KContext : AutoCloseable { } } + fun mkFpCustomSizeDeclBiased( + significandSize: UInt, + exponentSize: UInt, + significand: KBitVecValue<*>, + biasedExponent: KBitVecValue<*>, + signBit: Boolean + ): KFpDecl = mkFpCustomSizeDecl( + significandSize = significandSize, + exponentSize = exponentSize, + significand = significand, + unbiasedExponent = unbiasFpCustomSizeExponent(biasedExponent, exponentSize), + signBit = signBit + ) + private val roundingModeDeclCache = mkClosableCache { value: KFpRoundingMode -> KFpRoundingModeDecl(this, value) } diff --git a/ksmt-core/src/main/kotlin/org/ksmt/expr/KFloatingPointExpr.kt b/ksmt-core/src/main/kotlin/org/ksmt/expr/KFloatingPointExpr.kt index bc12f3081..c5b007185 100644 --- a/ksmt-core/src/main/kotlin/org/ksmt/expr/KFloatingPointExpr.kt +++ b/ksmt-core/src/main/kotlin/org/ksmt/expr/KFloatingPointExpr.kt @@ -122,7 +122,11 @@ class KFp128Value internal constructor( } override val decl: KDecl - get() = ctx.mkFp128Decl(significand, biasedExponent, signBit) + get() = ctx.mkFp128DeclBiased( + significandBits = significand, + biasedExponent = biasedExponent, + signBit = signBit + ) override val sort: KFp128Sort get() = ctx.mkFp128Sort() @@ -156,12 +160,12 @@ class KFpCustomSizeValue internal constructor( } override val decl: KDecl - get() = ctx.mkFpCustomSizeDecl( - significandSize, - exponentSize, - significand, - biasedExponent, - signBit + get() = ctx.mkFpCustomSizeDeclBiased( + significandSize = significandSize, + exponentSize = exponentSize, + significand = significand, + biasedExponent = biasedExponent, + signBit = signBit ) override val sort: KFpSort diff --git a/ksmt-core/src/main/kotlin/org/ksmt/solver/KModel.kt b/ksmt-core/src/main/kotlin/org/ksmt/solver/KModel.kt index 4d9d49775..1b181e657 100644 --- a/ksmt-core/src/main/kotlin/org/ksmt/solver/KModel.kt +++ b/ksmt-core/src/main/kotlin/org/ksmt/solver/KModel.kt @@ -18,10 +18,24 @@ interface KModel { val vars: List>, val entries: List>, val default: KExpr? - ) + ){ + override fun toString(): String { + if (entries.isEmpty()) return default.toString() + return buildString { + appendLine('{') + entries.forEach { appendLine(it) } + append("else -> ") + appendLine(default) + append('}') + } + } + } data class KFuncInterpEntry( val args: List>, val value: KExpr - ) + ) { + override fun toString(): String = + args.joinToString(prefix = "(", postfix = ") -> $value") + } } 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 1405f3b13..06ed49e34 100644 --- a/ksmt-core/src/main/kotlin/org/ksmt/solver/KSolver.kt +++ b/ksmt-core/src/main/kotlin/org/ksmt/solver/KSolver.kt @@ -5,7 +5,12 @@ import org.ksmt.sort.KBoolSort import kotlin.time.Duration @Suppress("OVERLOADS_INTERFACE", "INAPPLICABLE_JVM_NAME") -interface KSolver : AutoCloseable { +interface KSolver : AutoCloseable { + + /** + * Set solver specific options. + * */ + fun configure(configurator: Config.() -> Unit) /** * Assert an expression into solver. diff --git a/ksmt-core/src/main/kotlin/org/ksmt/solver/KSolverConfiguration.kt b/ksmt-core/src/main/kotlin/org/ksmt/solver/KSolverConfiguration.kt new file mode 100644 index 000000000..bb6eb9e3f --- /dev/null +++ b/ksmt-core/src/main/kotlin/org/ksmt/solver/KSolverConfiguration.kt @@ -0,0 +1,3 @@ +package org.ksmt.solver + +interface KSolverConfiguration diff --git a/ksmt-core/src/main/kotlin/org/ksmt/solver/model/KModelImpl.kt b/ksmt-core/src/main/kotlin/org/ksmt/solver/model/KModelImpl.kt index 6a9be3e84..dfabbd52e 100644 --- a/ksmt-core/src/main/kotlin/org/ksmt/solver/model/KModelImpl.kt +++ b/ksmt-core/src/main/kotlin/org/ksmt/solver/model/KModelImpl.kt @@ -27,4 +27,27 @@ open class KModelImpl( ): KModel.KFuncInterp? = interpretations[decl] as? KModel.KFuncInterp override fun detach(): KModel = this + + override fun toString(): String = buildString { + interpretations.forEach { (decl, interp) -> + append(decl) + append(":=\n\t") + append(interp) + appendLine() + } + } + + override fun equals(other: Any?): Boolean { + if (this === other) return true + if (javaClass != other?.javaClass) return false + + other as KModelImpl + + if (ctx != other.ctx) return false + if (interpretations != other.interpretations) return false + + return true + } + + override fun hashCode(): Int = interpretations.hashCode() } diff --git a/ksmt-runner/src/main/kotlin/org/ksmt/runner/models/generated/SolverProtocolModel.Generated.kt b/ksmt-runner/src/main/kotlin/org/ksmt/runner/models/generated/SolverProtocolModel.Generated.kt index 31ee8727d..1cb8679d2 100644 --- a/ksmt-runner/src/main/kotlin/org/ksmt/runner/models/generated/SolverProtocolModel.Generated.kt +++ b/ksmt-runner/src/main/kotlin/org/ksmt/runner/models/generated/SolverProtocolModel.Generated.kt @@ -20,6 +20,7 @@ import kotlin.jvm.JvmStatic class SolverProtocolModel private constructor( private val _initSolver: RdCall, private val _deleteSolver: RdCall, + private val _configure: RdCall, Unit>, private val _assert: RdCall, private val _assertAndTrack: RdCall, private val _push: RdCall, @@ -36,6 +37,7 @@ class SolverProtocolModel private constructor( override fun registerSerializersCore(serializers: ISerializers) { serializers.register(CreateSolverParams) + serializers.register(SolverConfigurationParam) serializers.register(AssertParams) serializers.register(AssertAndTrackResult) serializers.register(PopParams) @@ -48,6 +50,7 @@ class SolverProtocolModel private constructor( serializers.register(ModelEntry) serializers.register(ModelResult) serializers.register(SolverType.marshaller) + serializers.register(ConfigurationParamKind.marshaller) } @@ -70,8 +73,9 @@ class SolverProtocolModel private constructor( } } + private val __SolverConfigurationParamListSerializer = SolverConfigurationParam.list() - const val serializationHash = 3612013452435752699L + const val serializationHash = 2376534082034507660L } override val serializersOwner: ISerializersOwner get() = SolverProtocolModel @@ -89,6 +93,11 @@ class SolverProtocolModel private constructor( */ val deleteSolver: RdCall get() = _deleteSolver + /** + * Configure solver with parameters + */ + val configure: RdCall, Unit> get() = _configure + /** * Assert expression */ @@ -138,6 +147,7 @@ class SolverProtocolModel private constructor( init { _initSolver.async = true _deleteSolver.async = true + _configure.async = true _assert.async = true _assertAndTrack.async = true _push.async = true @@ -152,6 +162,7 @@ class SolverProtocolModel private constructor( init { bindableChildren.add("initSolver" to _initSolver) bindableChildren.add("deleteSolver" to _deleteSolver) + bindableChildren.add("configure" to _configure) bindableChildren.add("assert" to _assert) bindableChildren.add("assertAndTrack" to _assertAndTrack) bindableChildren.add("push" to _push) @@ -168,6 +179,7 @@ class SolverProtocolModel private constructor( ) : this( RdCall(CreateSolverParams, FrameworkMarshallers.Void), RdCall(FrameworkMarshallers.Void, FrameworkMarshallers.Void), + RdCall, Unit>(__SolverConfigurationParamListSerializer, FrameworkMarshallers.Void), RdCall(AssertParams, FrameworkMarshallers.Void), RdCall(AssertParams, AssertAndTrackResult), RdCall(FrameworkMarshallers.Void, FrameworkMarshallers.Void), @@ -187,6 +199,7 @@ class SolverProtocolModel private constructor( printer.indent { print("initSolver = "); _initSolver.print(printer); println() print("deleteSolver = "); _deleteSolver.print(printer); println() + print("configure = "); _configure.print(printer); println() print("assert = "); _assert.print(printer); println() print("assertAndTrack = "); _assertAndTrack.print(printer); println() print("push = "); _push.print(printer); println() @@ -204,6 +217,7 @@ class SolverProtocolModel private constructor( return SolverProtocolModel( _initSolver.deepClonePolymorphic(), _deleteSolver.deepClonePolymorphic(), + _configure.deepClonePolymorphic(), _assert.deepClonePolymorphic(), _assertAndTrack.deepClonePolymorphic(), _push.deepClonePolymorphic(), @@ -222,7 +236,7 @@ val IProtocol.solverProtocolModel get() = getOrCreateExtension(SolverProtocolMod /** - * #### Generated from [SolverProtocolModel.kt:30] + * #### Generated from [SolverProtocolModel.kt:41] */ data class AssertAndTrackResult ( val expression: org.ksmt.KAst @@ -279,7 +293,7 @@ data class AssertAndTrackResult ( /** - * #### Generated from [SolverProtocolModel.kt:26] + * #### Generated from [SolverProtocolModel.kt:37] */ data class AssertParams ( val expression: org.ksmt.KAst @@ -336,7 +350,7 @@ data class AssertParams ( /** - * #### Generated from [SolverProtocolModel.kt:38] + * #### Generated from [SolverProtocolModel.kt:49] */ data class CheckParams ( val timeout: Long @@ -393,7 +407,7 @@ data class CheckParams ( /** - * #### Generated from [SolverProtocolModel.kt:42] + * #### Generated from [SolverProtocolModel.kt:53] */ data class CheckResult ( val status: org.ksmt.solver.KSolverStatus @@ -450,7 +464,7 @@ data class CheckResult ( /** - * #### Generated from [SolverProtocolModel.kt:46] + * #### Generated from [SolverProtocolModel.kt:57] */ data class CheckWithAssumptionsParams ( val assumptions: List, @@ -512,6 +526,22 @@ data class CheckWithAssumptionsParams ( } +/** + * #### Generated from [SolverProtocolModel.kt:27] + */ +enum class ConfigurationParamKind { + String, + Bool, + Int, + Double; + + companion object { + val marshaller = FrameworkMarshallers.enum() + + } +} + + /** * #### Generated from [SolverProtocolModel.kt:19] */ @@ -570,7 +600,7 @@ data class CreateSolverParams ( /** - * #### Generated from [SolverProtocolModel.kt:64] + * #### Generated from [SolverProtocolModel.kt:75] */ data class ModelEntry ( val sort: org.ksmt.KAst, @@ -645,7 +675,7 @@ data class ModelEntry ( /** - * #### Generated from [SolverProtocolModel.kt:59] + * #### Generated from [SolverProtocolModel.kt:70] */ data class ModelFuncInterpEntry ( val args: List, @@ -708,7 +738,7 @@ data class ModelFuncInterpEntry ( /** - * #### Generated from [SolverProtocolModel.kt:71] + * #### Generated from [SolverProtocolModel.kt:82] */ data class ModelResult ( val declarations: List, @@ -771,7 +801,7 @@ data class ModelResult ( /** - * #### Generated from [SolverProtocolModel.kt:34] + * #### Generated from [SolverProtocolModel.kt:45] */ data class PopParams ( val levels: UInt @@ -828,7 +858,7 @@ data class PopParams ( /** - * #### Generated from [SolverProtocolModel.kt:55] + * #### Generated from [SolverProtocolModel.kt:66] */ data class ReasonUnknownResult ( val reasonUnknown: String @@ -884,6 +914,75 @@ data class ReasonUnknownResult ( } +/** + * #### Generated from [SolverProtocolModel.kt:26] + */ +data class SolverConfigurationParam ( + val kind: ConfigurationParamKind, + val name: String, + val value: String +) : IPrintable { + //companion + + companion object : IMarshaller { + override val _type: KClass = SolverConfigurationParam::class + + @Suppress("UNCHECKED_CAST") + override fun read(ctx: SerializationCtx, buffer: AbstractBuffer): SolverConfigurationParam { + val kind = buffer.readEnum() + val name = buffer.readString() + val value = buffer.readString() + return SolverConfigurationParam(kind, name, value) + } + + override fun write(ctx: SerializationCtx, buffer: AbstractBuffer, value: SolverConfigurationParam) { + buffer.writeEnum(value.kind) + buffer.writeString(value.name) + buffer.writeString(value.value) + } + + + } + //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 SolverConfigurationParam + + if (kind != other.kind) return false + if (name != other.name) return false + if (value != other.value) return false + + return true + } + //hash code trait + override fun hashCode(): Int { + var __r = 0 + __r = __r*31 + kind.hashCode() + __r = __r*31 + name.hashCode() + __r = __r*31 + value.hashCode() + return __r + } + //pretty print + override fun print(printer: PrettyPrinter) { + printer.println("SolverConfigurationParam (") + printer.indent { + print("kind = "); kind.print(printer); println() + print("name = "); name.print(printer); println() + print("value = "); value.print(printer); println() + } + printer.print(")") + } + //deepClone + //contexts +} + + /** * #### Generated from [SolverProtocolModel.kt:20] */ @@ -899,7 +998,7 @@ enum class SolverType { /** - * #### Generated from [SolverProtocolModel.kt:51] + * #### Generated from [SolverProtocolModel.kt:62] */ data class UnsatCoreResult ( val core: List 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 6da8b22c6..9ef15fcf4 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 @@ -1,6 +1,8 @@ package org.ksmt.solver.runner +import com.jetbrains.rd.util.AtomicReference import com.jetbrains.rd.util.reactive.RdFault +import kotlinx.coroutines.TimeoutCancellationException import kotlinx.coroutines.runBlocking import kotlinx.coroutines.withTimeout import org.ksmt.decl.KDecl @@ -15,6 +17,7 @@ import org.ksmt.runner.models.generated.SolverProtocolModel import org.ksmt.runner.models.generated.SolverType import org.ksmt.solver.KModel import org.ksmt.solver.KSolver +import org.ksmt.solver.KSolverConfiguration import org.ksmt.solver.KSolverException import org.ksmt.solver.KSolverStatus import org.ksmt.solver.model.KModelImpl @@ -22,14 +25,19 @@ import org.ksmt.sort.KBoolSort import org.ksmt.sort.KSort import kotlin.time.Duration -class KSolverRunner( +class KSolverRunner( private val hardTimeout: Duration, private val worker: KsmtWorkerSession, -) : KSolver { + private val configurationBuilder: KSolverUniversalConfigurationBuilder, +) : KSolver { + + private val lastReasonOfUnknown = AtomicReference(null) override fun close() { runBlocking { - deleteSolver() + suppressAllRunnerExceptions { + deleteSolver() + } } worker.release() } @@ -44,6 +52,18 @@ class KSolverRunner( } } + override fun configure(configurator: Config.() -> Unit) = runBlocking { + configureAsync(configurator) + } + + suspend fun configureAsync(configurator: Config.() -> Unit) { + ensureActive() + val config = configurationBuilder.build { configurator() } + withTimeoutAndExceptionHandling { + worker.protocolModel.configure.startSuspending(worker.lifetime, config) + } + } + override fun assert(expr: KExpr) = runBlocking { assertAsync(expr) } @@ -101,10 +121,12 @@ class KSolverRunner( suspend fun checkAsync(timeout: Duration): KSolverStatus { ensureActive() val params = CheckParams(timeout.inWholeMilliseconds) - val result = withTimeoutAndExceptionHandling { - worker.protocolModel.check.startSuspending(worker.lifetime, params) + return handleCheckTimeoutAsUnknown { + val result = withTimeoutAndExceptionHandling { + worker.protocolModel.check.startSuspending(worker.lifetime, params) + } + result.status } - return result.status } override fun checkWithAssumptions( @@ -120,10 +142,12 @@ class KSolverRunner( ): KSolverStatus { ensureActive() val params = CheckWithAssumptionsParams(assumptions, timeout.inWholeMilliseconds) - val result = withTimeoutAndExceptionHandling { - worker.protocolModel.checkWithAssumptions.startSuspending(worker.lifetime, params) + return handleCheckTimeoutAsUnknown { + val result = withTimeoutAndExceptionHandling { + worker.protocolModel.checkWithAssumptions.startSuspending(worker.lifetime, params) + } + result.status } - return result.status } override fun model(): KModel = runBlocking { @@ -170,12 +194,12 @@ class KSolverRunner( reasonOfUnknownAsync() } - suspend fun reasonOfUnknownAsync(): String { + suspend fun reasonOfUnknownAsync(): String = lastReasonOfUnknown.updateIfNull { ensureActive() val result = withTimeoutAndExceptionHandling { worker.protocolModel.reasonOfUnknown.startSuspending(worker.lifetime, Unit) } - return result.reasonUnknown + result.reasonUnknown } internal suspend fun initSolver(solverType: SolverType) { @@ -205,4 +229,44 @@ class KSolverRunner( throw KSolverException(ex) } } + + @Suppress("TooGenericExceptionCaught") + private suspend inline fun suppressAllRunnerExceptions(crossinline body: suspend () -> Unit) { + try { + body() + } catch (ex: Exception) { + // Propagate exceptions caused by the exceptions on remote side. + if (ex is KSolverException && ex.cause is RdFault) { + throw ex + } + } + } + + private suspend inline fun handleCheckTimeoutAsUnknown( + crossinline body: suspend () -> KSolverStatus + ): KSolverStatus { + try { + lastReasonOfUnknown.getAndSet(null) + return body() + } catch (ex: KSolverException) { + val cause = ex.cause + if (cause is TimeoutCancellationException) { + lastReasonOfUnknown.getAndSet("timeout: ${cause.message}") + return KSolverStatus.UNKNOWN + } + throw ex + } + } + + private suspend inline fun AtomicReference.updateIfNull( + crossinline body: suspend () -> T + ): T { + val oldValue = get() + if (oldValue != null) return oldValue + + val newValue = body() + + getAndSet(newValue) + return newValue + } } diff --git a/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverRunnerManager.kt b/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverRunnerManager.kt index 3b8cbc468..c1af2d353 100644 --- a/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverRunnerManager.kt +++ b/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverRunnerManager.kt @@ -10,6 +10,7 @@ import org.ksmt.runner.core.RdServer import org.ksmt.runner.models.generated.SolverProtocolModel import org.ksmt.runner.models.generated.SolverType import org.ksmt.solver.KSolver +import org.ksmt.solver.KSolverConfiguration import org.ksmt.solver.KSolverException import org.ksmt.solver.bitwuzla.KBitwuzlaSolver import org.ksmt.solver.z3.KZ3Solver @@ -37,11 +38,15 @@ class KSolverRunnerManager( workers.terminate() } - fun createSolver(ctx: KContext, solver: KClass): KSolverRunner = runBlocking { - createSolverAsync(ctx, solver) - } + fun createSolver(ctx: KContext, solver: KClass>): KSolverRunner = + runBlocking { + createSolverAsync(ctx, solver) + } - suspend fun createSolverAsync(ctx: KContext, solver: KClass): KSolverRunner { + suspend fun createSolverAsync( + ctx: KContext, + solver: KClass> + ): KSolverRunner { if (workers.lifetime.isNotAlive) { throw KSolverException("Solver runner manager is terminated") } @@ -49,7 +54,8 @@ class KSolverRunnerManager( val worker = workers.getOrCreateFreeWorker() worker.astSerializationCtx.initCtx(ctx) worker.lifetime.onTermination { worker.astSerializationCtx.resetCtx() } - return KSolverRunner(hardTimeout, worker).also { + val configurationBuilder = solverConfigurationBuilder(solver) + return KSolverRunner(hardTimeout, worker, configurationBuilder).also { it.initSolver(solverType) } } @@ -59,5 +65,17 @@ class KSolverRunnerManager( KZ3Solver::class to SolverType.Z3, KBitwuzlaSolver::class to SolverType.Bitwuzla ) + + @Suppress("UNCHECKED_CAST") + private fun solverConfigurationBuilder( + solver: KClass> + ): KSolverUniversalConfigurationBuilder = + when (solver) { + KZ3Solver::class -> + KZ3SolverUniversalConfigurationBuilder() as KSolverUniversalConfigurationBuilder + KBitwuzlaSolver::class -> + KBitwuzlaSolverUniversalConfigurationBuilder() as KSolverUniversalConfigurationBuilder + else -> error("Unknown solver type: $solver") + } } } diff --git a/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverUniversalConfiguration.kt b/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverUniversalConfiguration.kt new file mode 100644 index 000000000..e4c19190e --- /dev/null +++ b/ksmt-runner/src/main/kotlin/org/ksmt/solver/runner/KSolverUniversalConfiguration.kt @@ -0,0 +1,73 @@ +package org.ksmt.solver.runner + +import org.ksmt.runner.models.generated.ConfigurationParamKind +import org.ksmt.runner.models.generated.SolverConfigurationParam +import org.ksmt.solver.KSolverConfiguration +import org.ksmt.solver.bitwuzla.KBitwuzlaSolverConfiguration +import org.ksmt.solver.bitwuzla.bindings.BitwuzlaOption +import org.ksmt.solver.z3.KZ3SolverConfiguration + +interface KSolverUniversalConfigurationBuilder { + fun build(body: Config.() -> Unit): List +} + +class KZ3SolverUniversalConfigurationBuilder : KSolverUniversalConfigurationBuilder { + override fun build(body: KZ3SolverConfiguration.() -> Unit): List = + buildList { KZ3SolverUniversalConfiguration(this).body() } +} + +class KBitwuzlaSolverUniversalConfigurationBuilder : + KSolverUniversalConfigurationBuilder { + override fun build(body: KBitwuzlaSolverConfiguration.() -> Unit): List = + buildList { KBitwuzlaSolverUniversalConfiguration(this).body() } +} + +private class KZ3SolverUniversalConfiguration( + private val config: MutableList +) : KZ3SolverConfiguration { + override fun setZ3Option(option: String, value: Boolean) { + config += SolverConfigurationParam(ConfigurationParamKind.Bool, option, "$value") + } + + override fun setZ3Option(option: String, value: Int) { + config += SolverConfigurationParam(ConfigurationParamKind.Int, option, "$value") + } + + override fun setZ3Option(option: String, value: Double) { + config += SolverConfigurationParam(ConfigurationParamKind.Double, option, "$value") + } + + override fun setZ3Option(option: String, value: String) { + config += SolverConfigurationParam(ConfigurationParamKind.String, option, value) + } +} + +private class KBitwuzlaSolverUniversalConfiguration( + private val config: MutableList +) : KBitwuzlaSolverConfiguration { + override fun setBitwuzlaOption(option: BitwuzlaOption, value: Int) { + config += SolverConfigurationParam(ConfigurationParamKind.Int, option.name, "$value") + } + + override fun setBitwuzlaOption(option: BitwuzlaOption, value: String) { + config += SolverConfigurationParam(ConfigurationParamKind.String, option.name, value) + } +} + +fun KZ3SolverConfiguration.addUniversalParam(param: SolverConfigurationParam): Unit = with(param) { + when (kind) { + ConfigurationParamKind.String -> setZ3Option(name, value) + ConfigurationParamKind.Bool -> setZ3Option(name, value.toBooleanStrict()) + ConfigurationParamKind.Int -> setZ3Option(name, value.toInt()) + ConfigurationParamKind.Double -> setZ3Option(name, value.toDouble()) + } +} + +fun KBitwuzlaSolverConfiguration.addUniversalParam(param: SolverConfigurationParam): Unit = with(param) { + val option = BitwuzlaOption.valueOf(name) + when (kind) { + ConfigurationParamKind.String -> setBitwuzlaOption(option, value) + ConfigurationParamKind.Int -> setBitwuzlaOption(option, value.toInt()) + else -> error("Unsupported option kind: $kind") + } +} 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 6e37f9a56..dc89d708a 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 @@ -18,18 +18,20 @@ import org.ksmt.runner.models.generated.solverProtocolModel import org.ksmt.runner.serializer.AstSerializationCtx import org.ksmt.solver.KSolver import org.ksmt.solver.bitwuzla.KBitwuzlaSolver +import org.ksmt.solver.bitwuzla.KBitwuzlaSolverConfiguration import org.ksmt.solver.z3.KZ3Solver +import org.ksmt.solver.z3.KZ3SolverConfiguration import org.ksmt.sort.KBoolSort import kotlin.time.Duration.Companion.milliseconds class KSolverWorkerProcess : ChildProcessBase() { private var workerCtx: KContext? = null - private var workerSolver: KSolver? = null + private var workerSolver: KSolver<*>? = null private val ctx: KContext get() = workerCtx ?: error("Solver is not initialized") - private val solver: KSolver + private val solver: KSolver<*> get() = workerSolver ?: error("Solver is not initialized") override fun parseArgs(args: Array) = KsmtWorkerArgs.fromList(args.toList()) @@ -55,6 +57,15 @@ class KSolverWorkerProcess : ChildProcessBase() { workerSolver = null workerCtx = null } + configure.measureExecutionForTermination { config -> + solver.configure { + when (this) { + is KZ3SolverConfiguration -> config.forEach { addUniversalParam(it) } + is KBitwuzlaSolverConfiguration -> config.forEach { addUniversalParam(it) } + else -> error("Unexpected configuration: ${this::class}") + } + } + } assert.measureExecutionForTermination { params -> @Suppress("UNCHECKED_CAST") solver.assert(params.expression as KExpr) 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 26c913f57..269c2e509 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 @@ -23,6 +23,17 @@ object SolverProtocolModel : Ext(SolverProtocolRoot) { }) } + private val solverConfigurationParam = structdef { + field("kind", enum("ConfigurationParamKind") { + +"String" + +"Bool" + +"Int" + +"Double" + }) + field("name", PredefinedType.string) + field("value", PredefinedType.string) + } + private val assertParams = structdef { field("expression", kastType) } @@ -82,6 +93,10 @@ object SolverProtocolModel : Ext(SolverProtocolRoot) { async documentation = "Delete solver" } + call("configure", immutableList(solverConfigurationParam), PredefinedType.void).apply { + async + documentation = "Configure solver with parameters" + } call("assert", assertParams, PredefinedType.void).apply { async documentation = "Assert expression" diff --git a/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/IncrementalApiTest.kt b/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/IncrementalApiTest.kt index 11c4a080c..847ca469e 100644 --- a/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/IncrementalApiTest.kt +++ b/ksmt-runner/src/test/kotlin/org/ksmt/solver/runner/IncrementalApiTest.kt @@ -8,15 +8,18 @@ import org.ksmt.KContext import org.ksmt.solver.KSolver import org.ksmt.solver.KSolverStatus import org.ksmt.solver.z3.KZ3Solver +import org.ksmt.solver.z3.KZ3SolverConfiguration +import org.ksmt.utils.getValue import org.ksmt.utils.mkConst import kotlin.test.Test import kotlin.test.assertEquals +import kotlin.test.assertNotEquals import kotlin.test.assertTrue import kotlin.time.Duration.Companion.milliseconds class IncrementalApiTest { private lateinit var context: KContext - private lateinit var solver: KSolver + private lateinit var solver: KSolver @BeforeEach fun createNewEnvironment() { @@ -118,6 +121,33 @@ class IncrementalApiTest { val status = solver.checkWithAssumptions(emptyList(), timeout = 1.milliseconds) assertEquals(KSolverStatus.UNKNOWN, status) - assertEquals("timeout", solver.reasonOfUnknown()) + assertTrue("timeout" in solver.reasonOfUnknown()) + } + + @Test + fun testSolverConfiguration(): Unit = with(context) { + val i by intSort + val j by intSort + + val expr = (i gt j) or (i lt j) + solver.assert(expr) + + solver.configure { setZ3Option("random_seed", 17) } + val status1 = solver.check() + assertEquals(KSolverStatus.SAT, status1) + val model1 = solver.model() + + solver.configure { setZ3Option("random_seed", 42) } + val status2 = solver.check() + assertEquals(KSolverStatus.SAT, status2) + val model2 = solver.model() + + solver.configure { setZ3Option("random_seed", 17) } + val status3 = solver.check() + assertEquals(KSolverStatus.SAT, status3) + val model3 = solver.model() + + assertNotEquals(model1, model2) + assertEquals(model1, model3) } } diff --git a/ksmt-test/build.gradle.kts b/ksmt-test/build.gradle.kts index 2e8867541..742b67ada 100644 --- a/ksmt-test/build.gradle.kts +++ b/ksmt-test/build.gradle.kts @@ -74,10 +74,12 @@ val smtLibBenchmarks = listOfNotNull( "QF_AUFNIA", //531K ) -val testDatDir = projectDir.resolve("testData") +val testDataDir = projectDir.resolve("testData") +val unpackedTestDataDir = testDataDir.resolve("data") +val downloadedTestData = testDataDir.resolve("testData.zip") val smtLibBenchmarkTestDataDownload = smtLibBenchmarks.map { mkSmtLibBenchmarkTestData(it) } -val smtLibBenchmarkTestDataPrepared = usePreparedSmtLibBenchmarkTestData(testDatDir) +val smtLibBenchmarkTestDataPrepared = usePreparedSmtLibBenchmarkTestData(unpackedTestDataDir) val prepareTestData by tasks.registering { tasks.withType().forEach { it.enabled = false } @@ -89,7 +91,11 @@ val prepareTestData by tasks.registering { } val testDataRevision = project.stringProperty("testDataRevision") ?: "no-revision" -val downloadPreparedBenchmarksTestData = downloadPreparedSmtLibBenchmarkTestData(testDatDir, testDataRevision) +val downloadPreparedBenchmarksTestData = downloadPreparedSmtLibBenchmarkTestData( + downloadPath = downloadedTestData, + testDataPath = unpackedTestDataDir, + version = testDataRevision +) tasks.withType { enabled = runBenchmarksBasedTests diff --git a/ksmt-test/src/test/kotlin/org/ksmt/test/BenchmarksBasedTest.kt b/ksmt-test/src/test/kotlin/org/ksmt/test/BenchmarksBasedTest.kt index 2b53c0a78..64fdb1ba8 100644 --- a/ksmt-test/src/test/kotlin/org/ksmt/test/BenchmarksBasedTest.kt +++ b/ksmt-test/src/test/kotlin/org/ksmt/test/BenchmarksBasedTest.kt @@ -18,9 +18,11 @@ import org.ksmt.runner.core.KsmtWorkerArgs import org.ksmt.runner.core.KsmtWorkerFactory import org.ksmt.runner.core.KsmtWorkerPool import org.ksmt.runner.core.RdServer +import org.ksmt.runner.core.WorkerInitializationFailedException import org.ksmt.runner.models.generated.TestProtocolModel import org.ksmt.solver.KModel import org.ksmt.solver.KSolver +import org.ksmt.solver.KSolverConfiguration import org.ksmt.solver.KSolverException import org.ksmt.solver.KSolverStatus import org.ksmt.solver.KSolverUnsupportedFeatureException @@ -66,10 +68,10 @@ abstract class BenchmarksBasedTest { } } - fun testModelConversion( + fun testModelConversion( name: String, samplePath: Path, - solverType: KClass + solverType: KClass> ) { val ctx = KContext() testWorkers.withWorker(ctx) { worker -> @@ -89,10 +91,10 @@ abstract class BenchmarksBasedTest { } } - fun testSolver( + fun testSolver( name: String, samplePath: Path, - solverType: KClass + solverType: KClass> ) { val ctx = KContext() testWorkers.withWorker(ctx) { worker -> @@ -133,7 +135,14 @@ abstract class BenchmarksBasedTest { ctx: KContext, body: suspend (TestRunner) -> Unit ) = runBlocking { - val worker = getOrCreateFreeWorker() + val worker = try { + getOrCreateFreeWorker() + } catch (ex: WorkerInitializationFailedException) { + val testIgnoreReason = "worker initialization failed -- ${ex.message}" + System.err.println(testIgnoreReason) + Assumptions.assumeTrue(false, testIgnoreReason) + error("ignored") + } worker.astSerializationCtx.initCtx(ctx) worker.lifetime.onTermination { worker.astSerializationCtx.resetCtx() @@ -177,8 +186,19 @@ abstract class BenchmarksBasedTest { .drop(testDataChunk * testDataChunkSize) .take(testDataChunkSize) .map { BenchmarkTestArguments(it.relativeTo(testDataLocation).toString(), it) } + .skipBadTestCases() } + private fun List.skipBadTestCases(): List = + /** + * Contains a declaration with an empty name. + * Normally, such declarations have special name in Z3, + * but in this case it is not true. After internalization via API, + * resulting declaration has name as excepted. + * Therefore, declarations are not equal, but this is not our issue. + * */ + filterNot { it.name == "QF_BV_symbols.smt2" } + @BeforeAll @JvmStatic fun initWorkerPools() { diff --git a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3Model.kt b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3Model.kt index 65368dbf4..740961c16 100644 --- a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3Model.kt +++ b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3Model.kt @@ -89,4 +89,13 @@ open class KZ3Model( } private fun ensureContextActive() = check(internCtx.isActive) { "Context already closed" } + + override fun toString(): String = detach().toString() + override fun hashCode(): Int = detach().hashCode() + override fun equals(other: Any?): Boolean { + if (this === other) return true + if (other !is KModel) return false + return detach() == other + } + } 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 4e71223a4..cd4bcdce0 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 @@ -19,7 +19,7 @@ import java.util.IdentityHashMap import kotlin.time.Duration import kotlin.time.DurationUnit -open class KZ3Solver(private val ctx: KContext) : KSolver { +open class KZ3Solver(private val ctx: KContext) : KSolver { private val z3Ctx = KZ3Context() private val solver = createSolver() private var lastCheckStatus = KSolverStatus.UNKNOWN @@ -41,6 +41,12 @@ open class KZ3Solver(private val ctx: KContext) : KSolver { private fun createSolver(): Solver = z3Ctx.nativeContext.mkSolver() + override fun configure(configurator: KZ3SolverConfiguration.() -> Unit) { + val params = z3Ctx.nativeContext.mkParams() + KZ3SolverConfigurationImpl(params).configurator() + solver.setParameters(params) + } + override fun push() { solver.push() currentScope++ diff --git a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3SolverConfiguration.kt b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3SolverConfiguration.kt new file mode 100644 index 000000000..5c85a0aa6 --- /dev/null +++ b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3SolverConfiguration.kt @@ -0,0 +1,29 @@ +package org.ksmt.solver.z3 + +import com.microsoft.z3.Params +import org.ksmt.solver.KSolverConfiguration + +interface KZ3SolverConfiguration : KSolverConfiguration { + fun setZ3Option(option: String, value: Boolean) + fun setZ3Option(option: String, value: Int) + fun setZ3Option(option: String, value: Double) + fun setZ3Option(option: String, value: String) +} + +class KZ3SolverConfigurationImpl(private val params: Params) : KZ3SolverConfiguration { + override fun setZ3Option(option: String, value: Boolean) { + params.add(option, value) + } + + override fun setZ3Option(option: String, value: Int) { + params.add(option, value) + } + + override fun setZ3Option(option: String, value: Double) { + params.add(option, value) + } + + override fun setZ3Option(option: String, value: String) { + params.add(option, value) + } +}