ksmt-core/io.ksmt.solver/KModel

KModel

interface KModel : AutoCloseable

Functions

abstract override fun close()

Close model and release acquired native resources.

abstract fun detach(): KModel

Detach model from the solver and release native resources.

abstract fun <T : KSort> eval(expr: KExpr<T>, isComplete: Boolean = false): KExpr<T>

abstract fun <T : KSort> interpretation(decl: KDecl<T>): KFuncInterp<T>?

uninterpretedSortUniverse

abstract fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set<KUninterpretedSortValue>?

Set of possible values of an Uninterpreted Sort.

Properties

abstract val declarations: Set<KDecl<*>>

uninterpretedSorts

abstract val uninterpretedSorts: Set<KUninterpretedSort>

Inheritors

KNativeSolverModel