For your first steps with KSMT, try our code examples.
To check OS compatibility, see Supported solvers and theories.
Find basic instructions to get use of KSMT:
Install KSMT via Gradle.
- Enable Maven Central repository in your build configuration:
repositories {
mavenCentral()
}- Add KSMT core dependency:
dependencies {
// core
implementation("io.ksmt:ksmt-core:0.5.11")
}- Add one or more SMT solver dependencies:
dependencies {
// z3
implementation("io.ksmt:ksmt-z3:0.5.11")
// bitwuzla
implementation("io.ksmt:ksmt-bitwuzla:0.5.11")
}SMT solver specific packages are provided with solver native binaries.
Create a KSMT context that manages expressions and solvers:
val ctx = KContext()Once the context is initialized, you can create expressions.
In the example below, we create an expression
a && (b >= c + 3)
over Boolean variable a and integer variables b and c:
import io.ksmt.utils.getValue
with(ctx) {
// create symbolic variables
val a by boolSort
val b by intSort
val c by intSort
// create an expression
val constraint = a and (b ge c + 3.expr)
}KSMT expressions are typed, and incorrect terms (e.g., and with integer arguments)
result in a compile-time error.
Note: import getValue is required when using the by keyword.
Alternatively, use mkConst(name, sort).
To check SMT formula satisfiability, we need to instantiate an SMT solver.
In this example, we use constraint from the previous step as an SMT formula. We use Z3 as an SMT solver.
with(ctx) {
KZ3Solver(this).use { solver -> // create a Z3 SMT solver instance
// assert expression
solver.assert(constraint)
// check assertions satisfiability with timeout
val satisfiability = solver.check(timeout = 1.seconds)
println(satisfiability) // SAT
// obtain model
val model = solver.model()
println("$a = ${model.eval(a)}") // a = true
println("$b = ${model.eval(b)}") // b = 0
println("$c = ${model.eval(c)}") // c = -3
}
}The formula in the example above is satisfiable, so we can get a model.
The model contains concrete values of the symbolic variables a, b, and c, which evaluate the formula to true.
Note: the Kotlin .use { } construction allows releasing the solver-consumed resources.
KSMT solver API provides two approaches to incremental formula solving: using push/pop operations and using assumptions.
Push and pop operations in the solver allow us to work with assertions as if we deal with a stack. The push operation puts the asserted expressions onto the stack, while the pop operation removes the pushed assertions.
with(ctx) {
// create symbolic variables
val cond1 by boolSort
val cond2 by boolSort
val a by bv32Sort
val b by bv32Sort
val c by bv32Sort
val goal by bv32Sort
KZ3Solver(this).use { solver ->
// a == 0
solver.assert(a eq mkBv(value = 0))
// goal == 2
solver.assert(goal eq mkBv(value = 2))
// push assertions onto stack
solver.push()
// a == goal
solver.assert(a eq goal)
/**
* Formula is unsatisfiable because we have
* a == 0 && goal == 2 && a == goal
*/
val check0 = solver.check(timeout = 1.seconds)
println("check0 = $check0") // UNSAT
// pop assertions from stack; a == goal is removed
solver.pop()
/**
* Formula is satisfiable now because we have
* a == 0 && goal == 2
*/
val check1 = solver.check(timeout = 1.seconds)
println("check1 = $check1") // SAT
// b == if (cond1) a + 1 else a
solver.assert(b eq mkIte(cond1, mkBvAddExpr(a, mkBv(value = 1)), a))
// push assertions onto stack
solver.push()
// b == goal
solver.assert(b eq goal)
/**
* Formula is unsatisfiable because we have
* a == 0 && goal == 2
* && b == if (cond1) a + 1 else a
* && goal == b
* where all possible values for b are only 0 and 1
*/
val check2 = solver.check(timeout = 1.seconds)
println("check2 = $check2") // UNSAT
// pop assertions from stack. b == goal is removed
solver.pop()
/**
* Formula is satisfiable now because we have
* a == 0 && goal == 2
* && b == if (cond1) a + 1 else a
*/
val check3 = solver.check(timeout = 1.seconds)
println("check3 = $check3") // SAT
// c == if (cond2) b + 1 else b
solver.assert(c eq mkIte(cond2, mkBvAddExpr(b, mkBv(value = 1)), b))
// push assertions stack
solver.push()
// c == goal
solver.assert(c eq goal)
/**
* Formula is satisfiable because we have
* a == 0 && goal == 2
* && b == if (cond1) a + 1 else a
* && c == if (cond2) b + 1 else b
* && goal == c
* where all possible values for b are 0 and 1
* and for c we have 0, 1 and 2
*/
val check4 = solver.check(timeout = 1.seconds)
println("check4 = $check4") // SAT
}
}Assumption mechanism allows us to assert an expression for a single check without actually adding it to assertions. The following example shows how to implement the previous example using assumptions instead of push and pop operations.
with(ctx) {
// create symbolic variables
val cond1 by boolSort
val cond2 by boolSort
val a by bv32Sort
val b by bv32Sort
val c by bv32Sort
val goal by bv32Sort
KZ3Solver(this).use { solver ->
// a == 0
solver.assert(a eq mkBv(value = 0))
// goal == 2
solver.assert(goal eq mkBv(value = 2))
/**
* Formula is unsatisfiable because we have
* a == 0 && goal == 2 && a == goal
* Expression a == goal is assumed for current check
*/
val check0 = solver.checkWithAssumptions(
assumptions = listOf(a eq goal),
timeout = 1.seconds
)
println("check0 = $check0") // UNSAT
/**
* Formula is satisfiable because we have
* a == 0 && goal == 2
*/
val check1 = solver.check(timeout = 1.seconds)
println("check1 = $check1") // SAT
// b == if (cond1) a + 1 else a
solver.assert(b eq mkIte(cond1, mkBvAddExpr(a, mkBv(value = 1)), a))
/**
* Formula is unsatisfiable because we have
* a == 0 && goal == 2
* && b == if (cond1) a + 1 else a
* && goal == b
* where all possible values for b are only 0 and 1
* Expression goal == b is assumed for current check
*/
val check2 = solver.checkWithAssumptions(
assumptions = listOf(b eq goal),
timeout = 1.seconds
)
println("check2 = $check2") // UNSAT
/**
* Formula is satisfiable now because we have
* a == 0 && goal == 2
* && b == if (cond1) a + 1 else a
*/
val check3 = solver.check(timeout = 1.seconds)
println("check3 = $check3") // SAT
// c == if (cond2) b + 1 else b
solver.assert(c eq mkIte(cond2, mkBvAddExpr(b, mkBv(value = 1)), b))
/**
* Formula is satisfiable because we have
* a == 0 && goal == 2
* && b == if (cond1) a + 1 else a
* && c == if (cond2) b + 1 else b
* && goal == c
* where all possible values for b are 0 and 1
* and for c we have 0, 1 and 2
* Expression goal == c is assumed for current check
*/
val check4 = solver.checkWithAssumptions(
assumptions = listOf(c eq goal),
timeout = 1.seconds
)
println("check4 = $check4") // SAT
}
}If the asserted SMT formula is unsatisfiable, we can extract the unsatisfiable core. The unsatisfiable core is a subset of inconsistent assertions and assumptions.
with(ctx) {
// create symbolic variables
val a by boolSort
val b by boolSort
val c by boolSort
val e1 = (a and b) or c
val e2 = !(a and b)
val e3 = !c
KZ3Solver(this).use { solver ->
// simply assert e1
solver.assert(e1)
/**
* Assert and track e2
* e2 will appear in unsat core
* */
solver.assertAndTrack(e2)
/**
* Check satisfiability with e3 assumed.
* Formula is unsatisfiable because e1 is inconsistent with e2 and e3
* */
val check = solver.checkWithAssumptions(assumptions = listOf(e3))
println("check = $check")
// retrieve unsat core
val core = solver.unsatCore()
println("unsat core = $core") // [(not (and b a)), (not c)]
// simply asserted expression cannot be in unsat core
println("e1 in core = ${e1 in core}") // false
// an expression added with `assertAndTrack` appears in unsat core as is
println("e2 in core = ${e2 in core}") // true
// the assumed expression appears in unsat core as is
println("e3 in core = ${e3 in core}") // true
}
}