ksmt-core/io.ksmt.solver.model/KFuncInterpVarsFree

KFuncInterpVarsFree

data class KFuncInterpVarsFree<T : KSort>(val decl: KDecl<T>, val entries: List<KFuncInterpEntryVarsFree<T>>, val default: KExpr<T>?) : KFuncInterp<T>

Function interpretation, that does NOT contain variables in the body. For example, F(x) with interpreted values in entries and in a default branch.

Constructors

KFuncInterpVarsFree

fun <T : KSort> KFuncInterpVarsFree(decl: KDecl<T>, entries: List<KFuncInterpEntryVarsFree<T>>, default: KExpr<T>?)

Functions

open override fun toString(): String

Properties

open override val decl: KDecl<T>

open override val default: KExpr<T>?

open override val entries: List<KFuncInterpEntryVarsFree<T>>

open val sort: T

open override val vars: List<KDecl<*>>