Advanced usage
For basic KSMT usage, please refer to Getting started guide.
Having tried the essential scenarios, find the advanced example and proceed to advanced usage.
Table of contents:
Working with SMT formulas
Learn how to parse, simplify, and substitute expressions.
Parsing formulas in SMT-LIB2 format
KSMT provides an API for parsing formulas in the SMT-LIB2 format.
Currently, KSMT provides a parser implemented on top of the Z3 solver API, and therefore ksmt-z3 module is
required for parsing.
val formula = """
(declare-fun x () Int)
(declare-fun y () Int)
(assert (>= x y))
(assert (>= y x))
"""
with(ctx) {
val assertions = KZ3SMTLibParser().parse(formula)
}
Default simplification
By default, KContext attempts to apply lightweight simplifications when you create an expression. If you do not
need simplifications, disable them using the KContext.simplificationMode parameter.
// Simplification is enabled by default
val simplifyingContext = KContext()
// Disable simplifications on a context level
val nonSimplifyingContext = KContext(simplificationMode = KContext.SimplificationMode.NO_SIMPLIFY)
val simplifiedExpr = with(simplifyingContext) {
val a by boolSort
!(a and falseExpr)
}
val nonSimplifiedExpr = with(nonSimplifyingContext) {
val a by boolSort
!(a and falseExpr)
}
println(nonSimplifiedExpr) // (not (and a false))
println(simplifiedExpr) // true
Manual simplification
KSMT provides KExprSimplifier, so you can manually simplify an arbitrary expression.
// Context does not simplify expressions during creation
val ctx = KContext(simplificationMode = KContext.SimplificationMode.NO_SIMPLIFY)
with(ctx) {
val a by boolSort
val nonSimplifiedExpr = !(a and falseExpr)
val simplifier = KExprSimplifier(ctx)
val simplifiedExpr = simplifier.apply(nonSimplifiedExpr)
println(nonSimplifiedExpr) // (not (and a false))
println(simplifiedExpr) // true
}
Expression substitution
KSMT provides KExprSubstitutor, so you can replace all the expression occurrences with another
expression.
val a by boolSort
val b by boolSort
val expr = !(a and b)
val substitutor = KExprSubstitutor(this).apply {
// Substitute all occurrences of `b` with `false`
substitute(b, falseExpr)
}
val exprAfterSubstitution = substitutor.apply(expr)
println(expr) // (not (and a b))
println(exprAfterSubstitution) // true
Working with SMT solvers
Learn how to configure and run solvers, get models, and switch to portfolio mode.
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 corresponding solver documentation for a list of available options.
with(ctx) {
KZ3Solver(this).use { solver ->
solver.configure {
// set Z3 solver `random_seed` parameter to 42
setZ3Option("random_seed", 42)
}
}
}
Solver-independent models
By default, SMT solver models are lazily initialized.
The values of the declared variables are loaded from the underlying solver native model on demand.
Therefore, models become invalid as soon as the solver closes. Moreover, solvers like Bitwuzla invalidate their models
each time check-sat is called.
To overcome these problems, KSMT provides the KModel.detach function that allows you to make the model independent of
the underlying native representation.
val a by boolSort
val b by boolSort
val expr = a and b
val (model, detachedModel) = KZ3Solver(this).use { solver ->
solver.assert(expr)
println(solver.check()) // SAT
val model = solver.model()
// Detach model from solver
val detachedModel = model.detach()
model to detachedModel
}
try {
model.eval(expr)
} catch (ex: Exception) {
println("Model no longer valid after solver close")
}
println(detachedModel.eval(expr)) // true
Note: it is recommended to use KModel.detach when you need to keep the model in a List, for example.
Solver runner
SMT solvers may ignore timeouts, or they suddenly crash, thus interrupting the entire application process. KSMT provides a process-based solver runner: it runs each solver in a separate process.
// Create a long-lived solver manager that manages a pool of solver workers
KSolverRunnerManager().use { solverManager ->
// Use solver API as usual
with(ctx) {
val a by boolSort
val b by boolSort
val expr = a and b
// Create solver using manager instead of direct constructor invocation
solverManager.createSolver(this, KZ3Solver::class).use { solver ->
solver.assert(expr)
println(solver.check()) // SAT
}
}
}
Using custom solvers in a runner
Solver runner also supports user-defined solvers. Custom solvers must be registered via registerSolver before being used in the runner.
// Create a long-lived solver manager that manages a pool of solver workers
KSolverRunnerManager().use { solverManager ->
// Register the user-defined solver in a current manager
solverManager.registerSolver(CustomZ3BasedSolver::class, KZ3SolverUniversalConfiguration::class)
// Use solver API as usual
with(ctx) {
val a by boolSort
val b by boolSort
val expr = a and b
// Create solver using manager instead of direct constructor invocation
solverManager.createSolver(this, CustomZ3BasedSolver::class).use { solver ->
solver.assert(expr)
println(solver.check()) // SAT
}
}
}
Solver portfolio
To run solvers in portfolio mode, i.e., to run them in parallel until you get the first result, try the following workflow, which is similar to using the solver runner:
// Create a long-lived portfolio solver manager that manages a pool of solver workers
KPortfolioSolverManager(
// Solvers to include in portfolio
listOf(KZ3Solver::class, CustomZ3BasedSolver::class)
).use { solverManager ->
// Since we use the user-defined solver in our portfolio, we must register it in the current manager
solverManager.registerSolver(CustomZ3BasedSolver::class, KZ3SolverUniversalConfiguration::class)
// Use solver API as usual
with(ctx) {
val a by boolSort
val b by boolSort
val expr = a and b
// Create portfolio solver using manager
solverManager.createPortfolioSolver(this).use { solver ->
solver.assert(expr)
println(solver.check()) // SAT
}
}
}