From 4ed4a9e5600c7bccad15e168b06a088270874865 Mon Sep 17 00:00:00 2001 From: Valentine Sobol Date: Tue, 20 Sep 2022 18:28:13 +0300 Subject: [PATCH] Readme (#27) * Sudoku example * Update README.md * Fix review issues --- README.md | 35 ++++++++++- examples/Sudoku.kt | 147 +++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 181 insertions(+), 1 deletion(-) create mode 100644 examples/Sudoku.kt diff --git a/README.md b/README.md index 5d495200f..366df699c 100644 --- a/README.md +++ b/README.md @@ -1,2 +1,35 @@ -# kotlin-smt +# KSMT Kotlin API for various SMT solvers + +[![KSMT: build](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml/badge.svg)](https://github.com/UnitTestBot/UTBotJava/ksmt/workflows/build-and-run-tests.yml) + +# Getting started +Install via JitPack and Gradle + +```kotlin +// core +implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.1.0") +// z3 solver +implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.1.0") +``` + +## Usage +See [examples](examples) + +# Features +Currently KSMT supports the following SMT solvers: + +| SMT Solver | Linux-x64 | Windows-x64 | MacOS-x64 | +|--------------------------------------------------|:------------------:|:------------------:|:------------------:| +| [Z3](https://github.com/Z3Prover/z3) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | +| [Bitwuzla](https://github.com/bitwuzla/bitwuzla) | :heavy_check_mark: | :heavy_check_mark: | | + +KSMT can express formulas in the following theories: + +| Theory | Z3 | Bitwuzla | +|-------------------------|:------------------:|:------------------:| +| Bitvectors | :heavy_check_mark: | :heavy_check_mark: | +| Arrays | :heavy_check_mark: | :heavy_check_mark: | +| IEEE Floats | :heavy_check_mark: | | +| Uninterpreted Functions | :heavy_check_mark: | :heavy_check_mark: | +| Arithmetic | :heavy_check_mark: | | diff --git a/examples/Sudoku.kt b/examples/Sudoku.kt new file mode 100644 index 000000000..29b08dbd4 --- /dev/null +++ b/examples/Sudoku.kt @@ -0,0 +1,147 @@ +package org.ksmt.solver.z3 + +import org.ksmt.KContext +import org.ksmt.expr.KExpr +import org.ksmt.expr.KInt32NumExpr +import org.ksmt.solver.KModel +import org.ksmt.solver.KSolverStatus +import org.ksmt.sort.KBoolSort +import org.ksmt.sort.KIntSort +import kotlin.time.Duration.Companion.seconds + +const val BLOCK_SIZE = 3 +const val SIZE = 9 +const val EMPTY_CELL_VALUE = 0 + +val sudokuIndices = 0 until SIZE + +val sudokuTask = """ + 2 * * | 9 * 6 | * * 1 + * * 6 | * 4 * | * * 9 + * * * | 5 2 * | 4 * * + ------ ------- ------ + 3 * 2 | * * 7 | * 5 * + * * * | 2 * * | 1 * * + * 9 * | 3 * * | 7 * * + ------ ------- ------ + * 8 7 | * 5 * | 3 1 * + 6 * 3 | * 1 * | 8 * * + 4 * * | * * 9 | * * * +""".trimIndent() + +fun main() = KContext().useWith { + + // Parse and display a given Sudoku grid. + val initialGrid = parseSudoku(sudokuTask) + println("Task:") + println(printSudokuGrid(initialGrid)) + + // Create symbolic variables for each cell of the Sudoku grid. + val symbols = sudokuIndices.map { row -> + sudokuIndices.map { col -> + intSort.mkConst("x_${row}_${col}") + } + } + + // Create symbolic variables constraints according to the Sudoku rules. + val rules = sudokuRules(symbols) + + // Create variable constraints from the filled cells of the Sudoku grid. + val symbolAssignments = assignSymbols(symbols, initialGrid) + + // Create Z3 SMT solver instance. + val solution = KZ3Solver(this).useWith { + + // Assert all constraints. + rules.forEach { assert(it) } + symbolAssignments.forEach { assert(it) } + + // Solve Sudoku. + val status = check(timeout = 1.seconds) + check(status == KSolverStatus.SAT) { "Sudoku is unsolvable" } + + // Get the SMT model and convert it to a Sudoku solution. + buildSolution(symbols, model()) + } + + println("Solution:") + println(printSudokuGrid(solution)) +} + +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) } + + // Each row contains distinct numbers. + val rowDistinctConstraints = symbols.map { row -> mkDistinct(row) } + + // Each column contains distinct numbers. + val colDistinctConstraints = sudokuIndices.map { col -> + val colSymbols = sudokuIndices.map { row -> symbols[row][col] } + mkDistinct(colSymbols) + } + + // Each 3x3 block contains distinct numbers. + val blockDistinctConstraints = (0 until SIZE step BLOCK_SIZE).flatMap { blockRow -> + (0 until SIZE step BLOCK_SIZE).map { blockCol -> + val block = (blockRow until blockRow + BLOCK_SIZE).flatMap { row -> + (blockCol until blockCol + BLOCK_SIZE).map { col -> + symbols[row][col] + } + } + mkDistinct(block) + } + } + + return symbolConstraints + rowDistinctConstraints + colDistinctConstraints + blockDistinctConstraints +} + +private fun KContext.assignSymbols( + symbols: List>>, + grid: List> +): List> = + sudokuIndices.flatMap { row -> + sudokuIndices.mapNotNull { col -> + val value = grid[row][col] + if (value != EMPTY_CELL_VALUE) symbols[row][col] eq value.intExpr else null + } + } + +private fun KContext.buildSolution(symbols: List>>, model: KModel): List> = + symbols.map { row -> + row.map { symbol -> + val value = model.eval(symbol) + value as KInt32NumExpr + value.value + } + } + +private fun parseSudoku(task: String): List> = + task.lines() + .map { row -> row.mapNotNull { it.cellValueOrNull() } } + .filterNot { it.isEmpty() } + +private fun Char.cellValueOrNull(): Int? = when { + isDigit() -> digitToInt() + this == '*' -> 0 + else -> null +} + +private fun printSudokuGrid(grid: List>) = buildString { + for ((rowIdx, row) in grid.withIndex()) { + for ((colIdx, cell) in row.withIndex()) { + append(if (cell == EMPTY_CELL_VALUE) "*" else cell) + append(" ") + if ((colIdx + 1) % BLOCK_SIZE == 0 && (colIdx + 1) != SIZE) { + append("| ") + } + } + appendLine() + if ((rowIdx + 1) % BLOCK_SIZE == 0 && (rowIdx + 1) != SIZE) { + appendLine("-".repeat((SIZE + 2) * 2)) + } + } +} + +private inline fun T.useWith(block: T.() -> R): R = use { it.block() }