ksmt-core/io.ksmt.solver.model

Package-level declarations

Types

KFuncInterp

interface KFuncInterp<T : KSort>

KFuncInterpEntry

interface KFuncInterpEntry<T : KSort>

KFuncInterpEntryNAry

interface KFuncInterpEntryNAry<T : KSort> : KFuncInterpEntry<T>

KFuncInterpEntryOneAry

interface KFuncInterpEntryOneAry<T : KSort> : KFuncInterpEntry<T>

KFuncInterpEntryThreeAry

interface KFuncInterpEntryThreeAry<T : KSort> : KFuncInterpEntry<T>

KFuncInterpEntryTwoAry

interface KFuncInterpEntryTwoAry<T : KSort> : KFuncInterpEntry<T>

KFuncInterpEntryVarsFree

interface KFuncInterpEntryVarsFree<T : KSort> : KFuncInterpEntry<T>

Function interpretation entry, that does NOT contain variables in arguments and in a value. For example, arguments and a value are interpreted values.

KFuncInterpEntryVarsFreeNAry

data class KFuncInterpEntryVarsFreeNAry<T : KSort> : KFuncInterpEntryVarsFree<T> , KFuncInterpEntryNAry<T>

KFuncInterpEntryVarsFreeOneAry

data class KFuncInterpEntryVarsFreeOneAry<T : KSort>(val arg: KExpr<*>, val value: KExpr<T>) : KFuncInterpEntryVarsFree<T> , KFuncInterpEntryOneAry<T>

KFuncInterpEntryVarsFreeThreeAry

data class KFuncInterpEntryVarsFreeThreeAry<T : KSort>(val arg0: KExpr<*>, val arg1: KExpr<*>, val arg2: KExpr<*>, val value: KExpr<T>) : KFuncInterpEntryVarsFree<T> , KFuncInterpEntryThreeAry<T>

KFuncInterpEntryVarsFreeTwoAry

data class KFuncInterpEntryVarsFreeTwoAry<T : KSort>(val arg0: KExpr<*>, val arg1: KExpr<*>, val value: KExpr<T>) : KFuncInterpEntryVarsFree<T> , KFuncInterpEntryTwoAry<T>

KFuncInterpEntryWithVars

interface KFuncInterpEntryWithVars<T : KSort> : KFuncInterpEntry<T>

Function interpretation entry, that may contain variables in arguments or in a value.

KFuncInterpEntryWithVarsNAry

data class KFuncInterpEntryWithVarsNAry<T : KSort> : KFuncInterpEntryWithVars<T> , KFuncInterpEntryNAry<T>

KFuncInterpEntryWithVarsOneAry

data class KFuncInterpEntryWithVarsOneAry<T : KSort>(val arg: KExpr<*>, val value: KExpr<T>) : KFuncInterpEntryWithVars<T> , KFuncInterpEntryOneAry<T>

KFuncInterpEntryWithVarsThreeAry

data class KFuncInterpEntryWithVarsThreeAry<T : KSort>(val arg0: KExpr<*>, val arg1: KExpr<*>, val arg2: KExpr<*>, val value: KExpr<T>) : KFuncInterpEntryWithVars<T> , KFuncInterpEntryThreeAry<T>

KFuncInterpEntryWithVarsTwoAry

data class KFuncInterpEntryWithVarsTwoAry<T : KSort>(val arg0: KExpr<*>, val arg1: KExpr<*>, val value: KExpr<T>) : KFuncInterpEntryWithVars<T> , KFuncInterpEntryTwoAry<T>

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.

KFuncInterpWithVars

data class KFuncInterpWithVars<T : KSort>(val decl: KDecl<T>, val vars: List<KDecl<*>>, val entries: List<KFuncInterpEntry<T>>, val default: KExpr<T>?) : KFuncInterp<T>

Function interpretation, that contains variables in the body. For example, F(x) with default value (+ x 1).

KModelEvaluator

open class KModelEvaluator(val ctx: KContext, model: KModel, isComplete: Boolean, quantifiedVars: Set<KDecl<*>> = emptySet()) : KExprSimplifier

KModelImpl

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

KNativeSolverModel

class KNativeSolverModel(nativeModel: KModel) : KModel