ksmt-core/io.ksmt.solver/KSolver

KSolver

interface KSolver<Config : KSolverConfiguration> : AutoCloseable

Functions

assert

@JvmName(name = "assertExpr")

abstract fun assert(expr: KExpr<KBoolSort>)

Assert an expression into solver.

@JvmName(name = "assertExprs")

open fun assert(exprs: List<KExpr<KBoolSort>>)

Assert multiple expressions into solver.

assertAndTrack

abstract fun assertAndTrack(expr: KExpr<KBoolSort>)

Assert an expression into solver and track it in unsat cores.

open fun assertAndTrack(exprs: List<KExpr<KBoolSort>>)

Assert multiple expressions into solver and track them in unsat cores.

check

@JvmOverloads

@JvmName(name = "check")

abstract fun check(timeout: Duration = Duration.INFINITE): KSolverStatus

Performs satisfiability check of currently asserted expressions.

checkWithAssumptions

@JvmOverloads

@JvmName(name = "checkWithAssumptions")

abstract fun checkWithAssumptions(assumptions: List<KExpr<KBoolSort>>, timeout: Duration = Duration.INFINITE): KSolverStatus

Performs satisfiability check of currently asserted expressions and provided assumptions.

abstract override fun close()

Close solver and release acquired native resources.

configure

abstract fun configure(configurator: Config.() -> Unit)

Set solver specific options.

interrupt

abstract fun interrupt()

Cancel currently performing check-sat.

model

abstract fun model(): KModel

Retrieve the model for the last check or checkWithAssumptions.

pop

@JvmOverloads

@JvmName(name = "pop")

abstract fun pop(n: UInt)

Revert solver assertions state to previously created backtracking point.

push

abstract fun push()

Create a backtracking point for assertion stack.

reasonOfUnknown

abstract fun reasonOfUnknown(): String

Retrieve a brief explanation of an KSolverStatus.UNKNOWN result. The format of resulting string is solver implementation dependent.

unsatCore

abstract fun unsatCore(): List<KExpr<KBoolSort>>

Retrieve the unsat core for the last check or checkWithAssumptions.