ksmt's Introduction

KSMT

Kotlin API for various SMT solvers.

Getting started

// JitPack repository
repositories {
    maven { url = uri("https://jitpack.io") }
}

// core 
implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.2.1")
// z3 solver
implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.2.1")

Usage

Check out our Getting started guide and the example project. Also, check out the Java examples.

Features

Currently, KSMT supports the following SMT solvers:

SMT Solver	Linux-x64	Windows-x64	MacOS-x64
Z3	✔️	✔️	✔️
Bitwuzla	✔️	✔️

KSMT can express formulas in the following theories:

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

Check out our roadmap for detailed description of features and future plans.

Why KSMT?

Kotlin based DSL for SMT formulas

KSMT provides simple and concise DSL for expressions.

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)

Check out our example project for more complicated examples.

Solver agnostic SMT formula representation

KSMT provides a solver-independent formula representation with back and forth transformations to the solver's native representation. Such representation allows introspection of formulas and transformation of formulas independent of the solver.

Process based solver runner

KSMT provides a high-performant API for running SMT solvers in separate processes. This feature is important for implementing hard timeouts and solving using multiple solvers in portfolio mode.

Recommend Projects