KModelImpl

open class KModelImpl(val ctx: KContext, interpretations: Map<KDecl<*>, KFuncInterp<*>>, uninterpretedSortsUniverses: Map<KUninterpretedSort, Set<KUninterpretedSortValue>>) : KModel

Constructors

open override fun close()

Close model and release acquired native resources.

open override fun detach(): KModel

Detach model from the solver and release native resources.

open operator override fun equals(other: Any?): Boolean

open override fun <T : KSort> eval(expr: KExpr<T>, isComplete: Boolean): KExpr<T>

open override fun hashCode(): Int

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

open override fun toString(): String

Set of possible values of an Uninterpreted Sort.

open override val declarations: Set<KDecl<*>>