ksmt-core/io.ksmt.decl

Package-level declarations

Types

class KAndDecl : KFuncDeclChain<KBoolSort, KBoolSort>

class KArithAddDecl<T : KArithSort> : KFuncDeclChain<T, T>

class KArithDivDecl<T : KArithSort> : KFuncDecl2<T, T, T>

class KArithGeDecl<T : KArithSort> : KFuncDecl2<KBoolSort, T, T>

class KArithGtDecl<T : KArithSort> : KFuncDecl2<KBoolSort, T, T>

class KArithLeDecl<T : KArithSort> : KFuncDecl2<KBoolSort, T, T>

class KArithLtDecl<T : KArithSort> : KFuncDecl2<KBoolSort, T, T>

class KArithMulDecl<T : KArithSort> : KFuncDeclChain<T, T>

KArithPowerDecl

class KArithPowerDecl<T : KArithSort> : KFuncDecl2<T, T, T>

class KArithSubDecl<T : KArithSort> : KFuncDeclChain<T, T>

KArithUnaryMinusDecl

class KArithUnaryMinusDecl<T : KArithSort> : KFuncDecl1<T, T>

KArray2SelectDecl

class KArray2SelectDecl<D0 : KSort, D1 : KSort, R : KSort> : KArraySelectDeclBase<KArray2Sort<D0, D1, R>, R>

KArray2StoreDecl

class KArray2StoreDecl<D0 : KSort, D1 : KSort, R : KSort> : KArrayStoreDeclBase<KArray2Sort<D0, D1, R>, R>

KArray3SelectDecl

class KArray3SelectDecl<D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> : KArraySelectDeclBase<KArray3Sort<D0, D1, D2, R>, R>

KArray3StoreDecl

class KArray3StoreDecl<D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> : KArrayStoreDeclBase<KArray3Sort<D0, D1, D2, R>, R>

KArrayConstDecl

class KArrayConstDecl<A : KArraySortBase<R>, R : KSort>(ctx: KContext, sort: A) : KFuncDecl1<A, R>

KArrayNSelectDecl

class KArrayNSelectDecl<R : KSort> : KArraySelectDeclBase<KArrayNSort<R>, R>

KArrayNStoreDecl

class KArrayNStoreDecl<R : KSort> : KArrayStoreDeclBase<KArrayNSort<R>, R>

KArraySelectDecl

class KArraySelectDecl<D : KSort, R : KSort> : KArraySelectDeclBase<KArraySort<D, R>, R>

KArraySelectDeclBase

sealed class KArraySelectDeclBase<A : KArraySortBase<R>, R : KSort> : KFuncDecl<R>

KArrayStoreDecl

class KArrayStoreDecl<D : KSort, R : KSort> : KArrayStoreDeclBase<KArraySort<D, R>, R>

KArrayStoreDeclBase

sealed class KArrayStoreDeclBase<A : KArraySortBase<R>, R : KSort> : KFuncDecl<A>

KBitVec16ValueDecl

class KBitVec16ValueDecl : KBitVecValueDecl<KBv16Sort>

KBitVec1ValueDecl

class KBitVec1ValueDecl : KBitVecValueDecl<KBv1Sort>

KBitVec32ValueDecl

class KBitVec32ValueDecl : KBitVecValueDecl<KBv32Sort>

KBitVec64ValueDecl

class KBitVec64ValueDecl : KBitVecValueDecl<KBv64Sort>

KBitVec8ValueDecl

class KBitVec8ValueDecl : KBitVecValueDecl<KBv8Sort>

KBitVecCustomSizeValueDecl

class KBitVecCustomSizeValueDecl : KBitVecValueDecl<KBvSort>

KBitVecValueDecl

abstract class KBitVecValueDecl<T : KBvSort> : KConstDecl<T>

class KBv2IntDecl : KFuncDecl1<KIntSort, KBvSort> , KParameterizedFuncDecl

class KBvAddDecl<T : KBvSort> : KFuncDecl2<T, T, T>

KBvAddNoOverflowDecl

class KBvAddNoOverflowDecl<T : KBvSort> : KFuncDecl2<KBoolSort, T, T> , KParameterizedFuncDecl

KBvAddNoUnderflowDecl

class KBvAddNoUnderflowDecl<T : KBvSort> : KFuncDecl2<KBoolSort, T, T>

class KBvAndDecl<T : KBvSort> : KFuncDecl2<T, T, T>

KBvArithShiftRightDecl

class KBvArithShiftRightDecl<T : KBvSort> : KFuncDecl2<T, T, T>

class KBvConcatDecl : KFuncDecl2<KBvSort, KBvSort, KBvSort>

KBvDivNoOverflowDecl

class KBvDivNoOverflowDecl<T : KBvSort> : KFuncDecl2<KBoolSort, T, T>

class KBvExtractDecl : KFuncDecl1<KBvSort, KBvSort> , KParameterizedFuncDecl

KBvLogicalShiftRightDecl

class KBvLogicalShiftRightDecl<T : KBvSort> : KFuncDecl2<T, T, T>

class KBvMulDecl<T : KBvSort> : KFuncDecl2<T, T, T>

KBvMulNoOverflowDecl

class KBvMulNoOverflowDecl<T : KBvSort> : KFuncDecl2<KBoolSort, T, T> , KParameterizedFuncDecl

KBvMulNoUnderflowDecl

class KBvMulNoUnderflowDecl<T : KBvSort> : KFuncDecl2<KBoolSort, T, T>

class KBvNAndDecl<T : KBvSort> : KFuncDecl2<T, T, T>

KBvNegationDecl

class KBvNegationDecl<T : KBvSort> : KFuncDecl1<T, T>

KBvNegNoOverflowDecl

class KBvNegNoOverflowDecl<T : KBvSort> : KFuncDecl1<KBoolSort, T>

class KBvNorDecl<T : KBvSort> : KFuncDecl2<T, T, T>

class KBvNotDecl<T : KBvSort> : KFuncDecl1<T, T>

class KBvOrDecl<T : KBvSort> : KFuncDecl2<T, T, T>

KBvReductionAndDecl

class KBvReductionAndDecl<T : KBvSort> : KFuncDecl1<KBv1Sort, T>

KBvReductionOrDecl

class KBvReductionOrDecl<T : KBvSort> : KFuncDecl1<KBv1Sort, T>

class KBvRepeatDecl : KFuncDecl1<KBvSort, KBvSort> , KParameterizedFuncDecl

KBvRotateLeftDecl

class KBvRotateLeftDecl<T : KBvSort> : KFuncDecl2<T, T, T>

KBvRotateLeftIndexedDecl

class KBvRotateLeftIndexedDecl<T : KBvSort> : KFuncDecl1<T, T> , KParameterizedFuncDecl

KBvRotateRightDecl

class KBvRotateRightDecl<T : KBvSort> : KFuncDecl2<T, T, T>

KBvRotateRightIndexedDecl

class KBvRotateRightIndexedDecl<T : KBvSort> : KFuncDecl1<T, T> , KParameterizedFuncDecl

KBvShiftLeftDecl

class KBvShiftLeftDecl<T : KBvSort> : KFuncDecl2<T, T, T>

KBvSignedDivDecl

class KBvSignedDivDecl<T : KBvSort> : KFuncDecl2<T, T, T>

KBvSignedGreaterDecl

class KBvSignedGreaterDecl<T : KBvSort> : KFuncDecl2<KBoolSort, T, T>

KBvSignedGreaterOrEqualDecl

class KBvSignedGreaterOrEqualDecl<T : KBvSort> : KFuncDecl2<KBoolSort, T, T>

KBvSignedLessDecl

class KBvSignedLessDecl<T : KBvSort> : KFuncDecl2<KBoolSort, T, T>

KBvSignedLessOrEqualDecl

class KBvSignedLessOrEqualDecl<T : KBvSort> : KFuncDecl2<KBoolSort, T, T>

KBvSignedModDecl

class KBvSignedModDecl<T : KBvSort> : KFuncDecl2<T, T, T>

KBvSignedRemDecl

class KBvSignedRemDecl<T : KBvSort> : KFuncDecl2<T, T, T>

class KBvSubDecl<T : KBvSort> : KFuncDecl2<T, T, T>

KBvSubNoOverflowDecl

class KBvSubNoOverflowDecl<T : KBvSort> : KFuncDecl2<KBoolSort, T, T>

KBvSubNoUnderflowDecl

class KBvSubNoUnderflowDecl<T : KBvSort> : KFuncDecl2<KBoolSort, T, T> , KParameterizedFuncDecl

class KBvToFpDecl<T : KFpSort> : KToFpDecl<T, KBvSort>

KBvUnsignedDivDecl

class KBvUnsignedDivDecl<T : KBvSort> : KFuncDecl2<T, T, T>

KBvUnsignedGreaterDecl

class KBvUnsignedGreaterDecl<T : KBvSort> : KFuncDecl2<KBoolSort, T, T>

KBvUnsignedGreaterOrEqualDecl

class KBvUnsignedGreaterOrEqualDecl<T : KBvSort> : KFuncDecl2<KBoolSort, T, T>

KBvUnsignedLessDecl

class KBvUnsignedLessDecl<T : KBvSort> : KFuncDecl2<KBoolSort, T, T>

KBvUnsignedLessOrEqualDecl

class KBvUnsignedLessOrEqualDecl<T : KBvSort> : KFuncDecl2<KBoolSort, T, T>

KBvUnsignedRemDecl

class KBvUnsignedRemDecl<T : KBvSort> : KFuncDecl2<T, T, T>

class KBvXNorDecl<T : KBvSort> : KFuncDecl2<T, T, T>

class KBvXorDecl<T : KBvSort> : KFuncDecl2<T, T, T>

abstract class KConstDecl<T : KSort>(ctx: KContext, name: String, sort: T) : KFuncDecl<T>

abstract class KDecl<T : KSort>(val ctx: KContext, val name: String, val sort: T, val argSorts: List<KSort>) : KAst

interface KDeclVisitor<T>

class KDistinctDecl<T : KSort> : KFuncDeclChain<KBoolSort, T>

class KEqDecl<T : KSort> : KFuncDecl2<KBoolSort, T, T>

class KFalseDecl : KConstDecl<KBoolSort>

class KFp128Decl : KFpDecl<KFp128Sort>

class KFp16Decl : KFpDecl<KFp16Sort>

class KFp32Decl : KFpDecl<KFp32Sort>

class KFp64Decl : KFpDecl<KFp64Sort>

class KFpAbsDecl<T : KFpSort> : KFuncDecl1<T, T>

class KFpAddDecl<T : KFpSort> : KFuncDecl3<T, KFpRoundingModeSort, T, T>

KFpCustomSizeDecl

class KFpCustomSizeDecl : KFpDecl<KFpSort>

abstract class KFpDecl<T : KFpSort> : KConstDecl<T>

class KFpDivDecl<T : KFpSort> : KFuncDecl3<T, KFpRoundingModeSort, T, T>

class KFpEqualDecl<T : KFpSort> : KFuncDecl2<KBoolSort, T, T>

class KFpFromBvDecl<T : KFpSort> : KFuncDecl3<T, KBv1Sort, KBvSort, KBvSort>

KFpFusedMulAddDecl

class KFpFusedMulAddDecl<T : KFpSort> : KFuncDecl4<T, KFpRoundingModeSort, T, T, T>

class KFpGreaterDecl<T : KFpSort> : KFuncDecl2<KBoolSort, T, T>

KFpGreaterOrEqualDecl

class KFpGreaterOrEqualDecl<T : KFpSort> : KFuncDecl2<KBoolSort, T, T>

KFpIsInfiniteDecl

class KFpIsInfiniteDecl<T : KFpSort> : KFuncDecl1<KBoolSort, T>

class KFpIsNaNDecl<T : KFpSort> : KFuncDecl1<KBoolSort, T>

KFpIsNegativeDecl

class KFpIsNegativeDecl<T : KFpSort> : KFuncDecl1<KBoolSort, T>

KFpIsNormalDecl

class KFpIsNormalDecl<T : KFpSort> : KFuncDecl1<KBoolSort, T>

KFpIsPositiveDecl

class KFpIsPositiveDecl<T : KFpSort> : KFuncDecl1<KBoolSort, T>

KFpIsSubnormalDecl

class KFpIsSubnormalDecl<T : KFpSort> : KFuncDecl1<KBoolSort, T>

class KFpIsZeroDecl<T : KFpSort> : KFuncDecl1<KBoolSort, T>

class KFpLessDecl<T : KFpSort> : KFuncDecl2<KBoolSort, T, T>

KFpLessOrEqualDecl

class KFpLessOrEqualDecl<T : KFpSort> : KFuncDecl2<KBoolSort, T, T>

class KFpMaxDecl<T : KFpSort> : KFuncDecl2<T, T, T>

class KFpMinDecl<T : KFpSort> : KFuncDecl2<T, T, T>

class KFpMulDecl<T : KFpSort> : KFuncDecl3<T, KFpRoundingModeSort, T, T>

KFpNegationDecl

class KFpNegationDecl<T : KFpSort> : KFuncDecl1<T, T>

class KFpRemDecl<T : KFpSort> : KFuncDecl2<T, T, T>

KFpRoundingModeDecl

class KFpRoundingModeDecl(ctx: KContext, val value: KFpRoundingMode) : KConstDecl<KFpRoundingModeSort>

KFpRoundToIntegralDecl

class KFpRoundToIntegralDecl<T : KFpSort> : KFuncDecl2<T, KFpRoundingModeSort, T>

class KFpSqrtDecl<T : KFpSort> : KFuncDecl2<T, KFpRoundingModeSort, T>

class KFpSubDecl<T : KFpSort> : KFuncDecl3<T, KFpRoundingModeSort, T, T>

class KFpToBvDecl<T : KFpSort> : KFuncDecl2<KBvSort, KFpRoundingModeSort, T>

class KFpToFpDecl<T : KFpSort> : KToFpDecl<T, KFpSort>

KFpToIEEEBvDecl

class KFpToIEEEBvDecl<T : KFpSort> : KFuncDecl1<KBvSort, T>

class KFpToRealDecl<T : KFpSort> : KFuncDecl1<KRealSort, T>

abstract class KFuncDecl<T : KSort>(ctx: KContext, name: String, resultSort: T, argSorts: List<KSort>) : KDecl<T>

abstract class KFuncDecl1<T : KSort, A : KSort>(ctx: KContext, name: String, resultSort: T, val argSort: A) : KFuncDecl<T>

abstract class KFuncDecl2<T : KSort, A0 : KSort, A1 : KSort>(ctx: KContext, name: String, resultSort: T, val arg0Sort: A0, val arg1Sort: A1) : KFuncDecl<T>

abstract class KFuncDecl3<T : KSort, A0 : KSort, A1 : KSort, A2 : KSort>(ctx: KContext, name: String, resultSort: T, val arg0Sort: A0, val arg1Sort: A1, val arg2Sort: A2) : KFuncDecl<T>

abstract class KFuncDecl4<T : KSort, A0 : KSort, A1 : KSort, A2 : KSort, A3 : KSort>(ctx: KContext, name: String, resultSort: T, val arg0Sort: A0, val arg1Sort: A1, val arg2Sort: A2, val arg3Sort: A3) : KFuncDecl<T>

abstract class KFuncDeclChain<T : KSort, A : KSort>(ctx: KContext, name: String, resultSort: T, val argSort: A) : KFuncDecl<T>

class KImpliesDecl : KFuncDecl2<KBoolSort, KBoolSort, KBoolSort>

class KIntModDecl : KFuncDecl2<KIntSort, KIntSort, KIntSort>

class KIntNumDecl : KConstDecl<KIntSort>

class KIntRemDecl : KFuncDecl2<KIntSort, KIntSort, KIntSort>

class KIntToRealDecl : KFuncDecl1<KRealSort, KIntSort>

class KIteDecl<T : KSort> : KFuncDecl3<T, KBoolSort, T, T>

class KNotDecl : KFuncDecl1<KBoolSort, KBoolSort>

class KOrDecl : KFuncDeclChain<KBoolSort, KBoolSort>

KParameterizedFuncDecl

interface KParameterizedFuncDecl

class KRealIsIntDecl : KFuncDecl1<KBoolSort, KRealSort>

class KRealNumDecl : KConstDecl<KRealSort>

class KRealToFpDecl<T : KFpSort> : KToFpDecl<T, KRealSort>

class KRealToIntDecl : KFuncDecl1<KIntSort, KRealSort>

class KSignExtDecl : KFuncDecl1<KBvSort, KBvSort> , KParameterizedFuncDecl

abstract class KToFpDecl<T : KFpSort, S : KSort> : KFuncDecl2<T, KFpRoundingModeSort, S>

class KTrueDecl : KConstDecl<KBoolSort>

KUninterpretedConstDecl

class KUninterpretedConstDecl<T : KSort> : KConstDecl<T> , KInternedObject

KUninterpretedFuncDecl

class KUninterpretedFuncDecl<T : KSort> : KFuncDecl<T> , KInternedObject

KUninterpretedSortValueDecl

class KUninterpretedSortValueDecl : KConstDecl<KUninterpretedSort>

class KXorDecl : KFuncDecl2<KBoolSort, KBoolSort, KBoolSort>

class KZeroExtDecl : KFuncDecl1<KBvSort, KBvSort> , KParameterizedFuncDecl