unittestbot/ksmt

Kotlin/Java API for various SMT solvers

KSMT

Meet the unified Kotlin/Java API for various SMT solvers.

Get the most out of SMT solving with KSMT features:

• Supporting more solvers and theories — for all popular operating systems
• Solver-agnostic formula representation and easy-to-use DSL
• Utilities to simplify and transform your expressions
• Switching between solvers and support for portfolio mode
• Running solvers in a separate process to reduce timeout-related crashes
• Streamlined solver delivery with no need for building a solver or implementing JVM bindings

Get started

To start using KSMT, install it via Gradle:

// core 
implementation("io.ksmt:ksmt-core:0.5.24")
// z3 solver
implementation("io.ksmt:ksmt-z3:0.5.24")

Find basic instructions in the Getting started guide and try it out with the Kotlin or Java examples.

To go beyond the basic scenarios, proceed to the Advanced usage guide and try the advanced example.

To get guided experience in KSMT, step through the detailed scenario for creating custom expressions.

Find more on KSMT features

Check the Roadmap to know more about current feature support and plans for the nearest future.

Supported solvers and theories

KSMT provides support for various solvers:

SMT solver	Linux-x64	Windows-x64	macOS-aarch64	macOS-x64
Z3	✔️	✔️	✔️	✔️
Bitwuzla	✔️	✔️	✔️
Yices2	✔️	✔️	✔️
cvc5	✔️	✔️	✔️

You can also use SMT solvers across multiple theories:

Theory	Z3	Bitwuzla	Yices2	cvc5
Bitvectors	✔️	✔️	✔️	✔️
Arrays	✔️	✔️	✔️	✔️
IEEE Floats	✔️	✔️	✔️ 1	✔️
Uninterpreted Functions	✔️	✔️	✔️	✔️
Arithmetic	✔️		✔️	✔️

Solver-agnostic formula representation

Various scenarios are available for using SMT solvers: you can use a single solver to determine whether a formula is satisfiable, or you can apply several solvers to the same expression successively. In the latter case, you need a solver-agnostic formula representation.

We implemented it in KSMT, so you can

• transform expressions from the solver native representation to KSMT representation and vice versa,
• use formula introspection,
• manipulate expressions without involving a solver,
• use expressions even if the solver is freed.

Expression interning (hash consing) affords faster expression comparison: we do not need to compare the expression trees. Expressions are deduplicated, so we avoid redundant memory allocation.

Kotlin-based DSL for SMT formulas

KSMT provides you with a unified DSL for SMT expressions:

val array by mkArraySort(intSort, intSort)
val index by intSort
val value by intSort

val expr = (array.select(index - 1.expr) lt value) and
        (array.select(index + 1.expr) gt value)

Utilities to simplify and transform expressions

KSMT provides a simplification engine applicable to all supported expressions for all supported theories:

• reduce expression size and complexity
• evaluate expressions (including those with free variables) — reduce your expression to a constant
• perform formula transformations
• substitute expressions

KSMT simplification engine implements more than 200 rules. By default, it attempts to apply simplifications when you create the expressions, but you can turn this feature off, if necessary. You can also simplify an arbitrary expression manually.

Using multiple solvers (portfolio mode)

SMT solvers may differ in performance across different formulas: see the International Satisfiability Modulo Theories Competition.

With KSMT portfolio solving, you can run multiple solvers in parallel on the same formula — until you get the first (the fastest) result.

For detailed instructions on running multiple solvers, see Advanced usage.

Running solvers in separate processes

Most of the SMT solvers are research projects — they are implemented via native libraries and are sometimes not production ready:

• they may ignore timeouts — they sometimes hang in a long-running operation, and you cannot interrupt it;
• they may suddenly crash interrupting the entire process — because of a pointer issue, for example.

KSMT runs each solver in a separate process, which adds to stability of your application and provides support for portfolio mode.

KSMT distribution

Many solvers do not have prebuilt binaries, or binaries are for Linux only.

KSMT is distributed as JVM library with solver binaries provided. The library has been tested against the SMT-LIB benchmarks. Documentation and examples are also available.

Footnotes

1. IEEE Floats are supported in Yices2 using ksmt-symfpu ↩

ksmt's Issues

Documentation on how to implement and use custom expressions

It's a bit unclear where should I extend KSMT in order to use my hierarchy of expressions which are inheritors of KExpr<T>.

Particularly, I'm interested in these questions:

• What should the accept function in my expressions do?
• How should I define the transformer for my expressions and what should it do?
• I would like to use KSolver::assert and KModel::eval with my expressions, how to achieve it?
• What if I want my expressions to be interned?

It would be great if KSMT documentation has a small step-by-step example covering all needed extension points.

Java compatibility

• KSolver.assert is not availiable in Java because assert is a keyword.
• Methods with default arguments (e.g. KSolver.check) are not availiable in Java.

DefaultValueSampler fails when creating values for custom size bitvectors

DefaultValueSimpler uses following code to create a default value for bitvectors:

override fun <S : KBvSort> visit(sort: S): KExpr<T> = with(ctx) {
    mkBv("0", sort.sizeBits).asExpr([email protected])
}

I.e. it creates a single-character length string. If the size of bitvector is not standard (i.e. not 1, 8, 16, 32, 64), KContext creates a KBitVecCustomValue.

However, constructor of KBitVecCustomValue contains a check that ensures that the length of a string is equal to the bitsize of a bitvector sort:

require(binaryStringValue.length.toUInt() == sizeBits) {
    "Provided string $binaryStringValue consist of ${binaryStringValue.length} " +
            "symbols, but $sizeBits were expected"
}

So this results in IllegalArgumentException being thrown in the KBitVecCustomValue constructor.

Example for reproducing the error:

val solverManager: KSolverRunnerManager by lazy {
    KSolverRunnerManager(
        workerPoolSize = 1,
        hardTimeout = 10.seconds * 2,
        workerProcessIdleTimeout = 10.seconds,
    )
}
val ctx = KContext()
with(ctx) {
    val bv32Sort = ctx.mkBv32Sort()
    val customSort = ctx.mkBvSort(2U)
    val arraySort = ctx.mkArraySort(bv32Sort, customSort)

    val decl = ctx.mkConstDecl("a", arraySort)
    val index by bv32Sort
    val a by customSort

    val constraint = a eq decl.apply().store(ctx.mkBv(12), ctx.mkBv("11", 2U)).select(index)

    val solver = solverManager.createSolver(ctx, KZ3Solver::class)
    solver.assert(constraint)
    solver.assert(index eq ctx.mkBv(12))
    solver.check(1.seconds)
    val model = solver.model()
    println(model.eval(a, true))
    println(model.eval(decl.apply(), true))
}

Value classes instead of Longs in Z3 API

Currently, we use long to represent all Z3 native objects: sorts, expressions, declarations.
Also, all Z3.Native methods accept raw longs without any clarification whether it is sort, expr, or whatever else.

The idea is to provide wrappers for Z3.native methods with different value classes for different object kinds.

Z3: support fp.to_sbv internal decl

io.ksmt.solver.KSolverUnsupportedFeatureException: Z3 internal decl fp.to_sbv is not supported
	at app//io.ksmt.solver.z3.KZ3ExprConverter.tryConvertInternalAppExpr-aM00XZQ(KZ3ExprConverter.kt:591)
	at app//io.ksmt.solver.z3.KZ3ExprConverter.convertApp-h_aMM1A(KZ3ExprConverter.kt:413)
	at app//io.ksmt.solver.z3.KZ3ExprConverter.convertNativeExpr-h_aMM1A(KZ3ExprConverter.kt:163)
	at app//io.ksmt.solver.util.KExprLongConverterBase.convertFromNative(KExprLongConverterBase.kt:27)
	at app//io.ksmt.solver.z3.KZ3ExprConverter.convertExpr(KZ3ExprConverter.kt:85)
	at app//io.ksmt.solver.z3.KZ3Model.funcInterp(KZ3Model.kt:342)
	at app//io.ksmt.solver.z3.KZ3Model.interpretation(KZ3Model.kt:101)
	at app//io.ksmt.solver.z3.KZ3Model.detach(KZ3Model.kt:164)

Fix Z3 model detach

io.ksmt.solver.KSolverUnsupportedFeatureException: Z3 internal decl Z3_OP_INTERNAL is not supported
	at app//io.ksmt.solver.z3.KZ3ExprConverter.convertApp-h_aMM1A(KZ3ExprConverter.kt:414)
	at app//io.ksmt.solver.z3.KZ3ExprConverter.convertNativeExpr-h_aMM1A(KZ3ExprConverter.kt:163)
	at app//io.ksmt.solver.util.KExprLongConverterBase.convertFromNative(KExprLongConverterBase.kt:27)
	at app//io.ksmt.solver.z3.KZ3ExprConverter.convertExpr(KZ3ExprConverter.kt:85)
	at app//io.ksmt.solver.z3.KZ3Model.funcInterp(KZ3Model.kt:342)
	at app//io.ksmt.solver.z3.KZ3Model.interpretation(KZ3Model.kt:101)
	at app//io.ksmt.solver.z3.KZ3Model.detach(KZ3Model.kt:164)

Incomplete FP support

For now, there are a few severe drawbacks in the FP implementation:

1. Doesn't work float to double transformation and vise versa:
   mkFp(someFloat, sort) and mkFp(someFloat.toDouble(), sort return different FP values since toDouble changes the bits. We need to detect it somehow and make fp creation consistent.
2. There is no overload for fp creation from int value
3. There are no tests for mkFp(BV, BV, BV)
4. Multiple bugs in custom size FP: some combinations don't work, choose masks carefully for tests, add limits and checks in the constructors
5. Operation implemented as part of the KFpValue: isNaN, isInfinity, isNormal, etc.
6. Add support for the FP in Bitwuzla
7. Replace Long values in KFpDecl with Bv
8. KFp128 should have BV instead of long values for its significand
9. Replace numbers with bit-vectors where it's possible (for example, in creation, in the internal storage, etc.)
10. Additional tests for operations (along with extra methods, like fpToFp)
11. Documentations for implemented classes and methods

Thread safety

Prepare KSMT for use in a multi-threaded environment:

• Use concurrent data structures in KContext
• Guard solver native APIs with locks

Yices model doesn't collect all uninterpreted sort values

In the following example sortValues doesn't contain value

with(KContext()) {
    KYicesSolver(this).use { solver ->
        val sort = mkUninterpretedSort("sort")

        val value = mkUninterpretedSortValue(sort, 0)
        val a by sort

        solver.assert(a neq value)
        solver.check()

        val model = solver.model()
        val sortValues = model.uninterpretedSortUniverse(sort)!!

        println(value in sortValues)
    }
}

Empty unsatCore for simple contradictions in assumptions

If we have a simple contradiction (e.g., 2 > 3 or false) in constraints passed into io.ksmt.solver.KSolver#checkWithAssumptions function, for Z3 we've got an empty unsat core. Looks like it is a problem with Z3 API that returns empty cores for such simple situations, but as a result, we don't have information about contradicting assertions in the solver.

Example to reproduce:

    @Test
    fun testUnsatCore(): Unit = with(context) {
        context = KContext()
        z3Solver = KZ3Solver(context)
        yicesSolver = KYicesSolver(context)

        val z3Status = z3Solver.checkWithAssumptions(listOf(mkFalse()))
        val z3UnsatCore = z3Solver.unsatCore()

        val yicesStatus = yicesSolver.checkWithAssumptions(listOf(mkFalse()))
        val yicesUnsatCore = yicesSolver.unsatCore()

        println(z3Status to z3UnsatCore)
        println(yicesStatus to yicesUnsatCore)
    }

Portfolio solver cancellation

I have a suggestion (probably I can make a PR, but I'm not very familiar with the code).

KSolverRunner unlike KPortfolioSolver allowed us to cancel suspending methods from the outside, for KPortfolioSolver it doesn't work as far as I tried to investigate the reason is awaitFirstSolver function.

This line throws an exception on cancellation

ksmt/ksmt-runner/src/main/kotlin/io/ksmt/solver/portfolio/KPortfolioSolver.kt

Line 319 in 6803209

return resultFuture.await()

, and the exception is not handled.

I suggest to catch the exception inside awaitFirstSolver and kill all active inner solvers.

(If you think this is doable and can be done straightforwardly, I will create a PR)

Check all solvers on glibc 2.31

Various performance issues

Overview

This issue contains a list of known performance problems

Z3

• Don't create intermediate Expr objects. Use Z3 native pointers directly

Bitwuzla

• Faster JNI bidings

Misc

• KSmt benchmarks

Bulk assert solver API

`KZ3SMTLibParser` should be faster

After some profiling, I found that KZ3SMTLibParser is running 40% of the time on these tests.

I think that it can be fixed :)

Some reproduction code:

package org.ksmt.solver.z3

import org.junit.jupiter.api.Test
import org.ksmt.KContext
import java.nio.file.Path
import java.nio.file.Paths
import kotlin.io.path.listDirectoryEntries


class Test {
    @Test
    fun test() {
        val paths = PathsProvider.paths()
        repeat(times = 10) {
            for (path in paths) {
                val solver = KZ3Solver(KContext())
                val expr = KZ3SMTLibParser(KContext()).parse(path).first()
                with(solver) { assert(expr) }
                solver.close()
            }
        }
    }
}

object PathsProvider {

    @JvmStatic
    fun paths() = testDataLocation().listDirectoryEntries("*.smt2")

    @JvmStatic
    private fun testDataLocation(): Path = this::class.java.classLoader
        .getResource("tests")
        ?.toURI()
        ?.let { Paths.get(it) }
        ?: error("No test data")
}

Fix docs for extensions of bitvectors

For now, the docs for io.ksmt.KContext#mkBvSignExtensionExpr is literally equal to the docs for io.ksmt.KContext#mkBvZeroExtensionExpr, that is a bit confusing.