0.5.23

AstManagementMode

SimplificationMode

CacheRemoveHandler

ConcurrentGcAstCache

ConcurrentGcAstInterner

ConcurrentNoGcAstCache

ConcurrentNoGcAstInterner

KInternedObject

mkAstInterner()

SingleThreadGcAstCache

SingleThreadGcAstInterner

SingleThreadNoGcAstCache

SingleThreadNoGcAstInterner

structurallyEqual()

io.ksmt.cache.weak

ConcurrentWeakCache

ConcurrentWeakHashMapCache

ConcurrentWeakInterner

WeakHashMapCache

KArithPowerDecl

KArithUnaryMinusDecl

KArray2SelectDecl

KArray2StoreDecl

KArray3SelectDecl

KArray3StoreDecl

KArrayConstDecl

KArrayNSelectDecl

KArrayNStoreDecl

KArraySelectDecl

KArraySelectDeclBase

KArrayStoreDecl

KArrayStoreDeclBase

KBitVec16ValueDecl

KBitVec1ValueDecl

KBitVec32ValueDecl

KBitVec64ValueDecl

KBitVec8ValueDecl

KBitVecCustomSizeValueDecl

KBitVecValueDecl

KBvAddNoOverflowDecl

KBvAddNoUnderflowDecl

KBvArithShiftRightDecl

KBvDivNoOverflowDecl

KBvLogicalShiftRightDecl

KBvMulNoOverflowDecl

KBvMulNoUnderflowDecl

KBvNegationDecl

KBvNegNoOverflowDecl

KBvReductionAndDecl

KBvReductionOrDecl

KBvRotateLeftDecl

KBvRotateLeftIndexedDecl

KBvRotateRightDecl

KBvRotateRightIndexedDecl

KBvShiftLeftDecl

KBvSignedDivDecl

KBvSignedGreaterDecl

KBvSignedGreaterOrEqualDecl

KBvSignedLessDecl

KBvSignedLessOrEqualDecl

KBvSignedModDecl

KBvSignedRemDecl

KBvSubNoOverflowDecl

KBvSubNoUnderflowDecl

KBvUnsignedDivDecl

KBvUnsignedGreaterDecl

KBvUnsignedGreaterOrEqualDecl

KBvUnsignedLessDecl

KBvUnsignedLessOrEqualDecl

KBvUnsignedRemDecl

KFpCustomSizeDecl

KFpFusedMulAddDecl

KFpGreaterOrEqualDecl

KFpIsInfiniteDecl

KFpIsNegativeDecl

KFpIsNormalDecl

KFpIsPositiveDecl

KFpIsSubnormalDecl

KFpLessOrEqualDecl

KFpNegationDecl

KFpRoundingModeDecl

KFpRoundToIntegralDecl

KFpToIEEEBvDecl

KParameterizedFuncDecl

KUninterpretedConstDecl

KUninterpretedFuncDecl

KUninterpretedSortValueDecl

KArrayLambdaBase

KArraySelectBase

KArrayStoreBase

KBitVecCustomValue

KBitVecNumberValue

KBvAddNoOverflowExpr

KBvAddNoUnderflowExpr

KBvArithShiftRightExpr

KBvDivNoOverflowExpr

KBvLogicalShiftRightExpr

KBvMulNoOverflowExpr

KBvMulNoUnderflowExpr

KBvNegationExpr

KBvNegNoOverflowExpr

KBvReductionAndExpr

KBvReductionOrExpr

KBvRotateLeftExpr

KBvRotateLeftIndexedExpr

KBvRotateRightExpr

KBvRotateRightIndexedExpr

KBvShiftLeftExpr

KBvSignedDivExpr

KBvSignedGreaterExpr

KBvSignedGreaterOrEqualExpr

KBvSignedLessExpr

KBvSignedLessOrEqualExpr

KBvSignedModExpr

KBvSignedRemExpr

KBvSignExtensionExpr

KBvSubNoOverflowExpr

KBvSubNoUnderflowExpr

KBvUnsignedDivExpr

KBvUnsignedGreaterExpr

KBvUnsignedGreaterOrEqualExpr

KBvUnsignedLessExpr

KBvUnsignedLessOrEqualExpr

KBvUnsignedRemExpr

KBvZeroExtensionExpr

KExistentialQuantifier

KFpCustomSizeValue

KFpFusedMulAddExpr

KFpGreaterOrEqualExpr

KFpIsInfiniteExpr

KFpIsNegativeExpr

KFpIsNormalExpr

KFpIsPositiveExpr

KFpIsSubnormalExpr

KFpLessOrEqualExpr

KFpNegationExpr

KFpRoundingMode

RoundNearestTiesToEven

RoundNearestTiesToAway

RoundTowardPositive

RoundTowardNegative

RoundTowardZero

KFpRoundingModeExpr

KFpRoundToIntegralExpr

KFpToIEEEBvExpr

KFunctionAsArray

KInterpretedValue

KPowerArithExpr

KUnaryMinusArithExpr

KUninterpretedSortValue

KUniversalQuantifier

io.ksmt.expr.printer

BvValuePrintMode

ExpressionPrinter

ExpressionPrinterWithLetBindings

io.ksmt.expr.rewrite

KExprSubstitutor

KExprUninterpretedDeclCollector

io.ksmt.expr.rewrite.simplify

areDefinitelyDistinct()

bvLessOrEqual()

castRealValue()

distributeExtractOverConcat()

distributeOperationOverConcat()

ensureExpressionsOrder()

evalBvOperation()

evalBvSignedMulNoOverflow()

evalFpPredicateOr()

executeIfValue()

ExpressionOrdering

flatBinaryBvExpr()

flatConcatArgs()

KArithExprSimplifier

KArrayExprSimplifier

KBoolExprSimplifier

KBvExprSimplifier

KExprSimplifier

KExprSimplifierBase

KFpExprSimplifier

rewriteArithGe()

rewriteArithGt()

rewriteArithSub()

rewriteBvAddNoOverflowExpr()

rewriteBvAddNoUnderflowExpr()

rewriteBvConcatEq()

rewriteBvDivNoOverflowExpr()

rewriteBvMulNoOverflowExpr()

rewriteBvMulNoUnderflowExpr()

rewriteBvNAndExpr()

rewriteBvNegNoOverflowExpr()

rewriteBvNorExpr()

rewriteBvRepeatExpr()

rewriteBvRotateLeftIndexedExpr()

rewriteBvRotateRightIndexedExpr()

rewriteBvSignedGreaterExpr()

rewriteBvSignedGreaterOrEqualExpr()

rewriteBvSignedLessExpr()

rewriteBvSubExpr()

rewriteBvSubNoOverflowExpr()

rewriteBvSubNoUnderflowExpr()

rewriteBvUnsignedGreaterExpr()

rewriteBvUnsignedGreaterOrEqualExpr()

rewriteBvUnsignedLessExpr()

rewriteBvUnsignedLessOrEqualExprLight()

rewriteBvXNorExpr()

rewriteBvZeroExtensionExpr()

rewriteFpGreaterExpr()

rewriteFpGreaterOrEqualExpr()

rewriteFpSubExpr()

rewriteImplies()

SIMPLIFIER_DEFAULT_BOUNDED_REWRITE_DEPTH

simplifyAndOr()

simplifyArithAdd()

simplifyArithAddLight()

simplifyArithDiv()

simplifyArithDivLight()

simplifyArithGe()

simplifyArithGt()

simplifyArithLe()

simplifyArithLeLight()

simplifyArithLt()

simplifyArithLtLight()

simplifyArithMul()

simplifyArithMulLight()

simplifyArithPower()

simplifyArithPowerLight()

simplifyArithSub()

simplifyArithUnaryMinus()

simplifyArithUnaryMinusLight()

simplifyArrayNSelect()

simplifyArrayNSelectFromArrayStore()

simplifyArrayNSelectLambda()

simplifyArrayNStore()

simplifyArrayNStoreLight()

simplifyArraySelect()

simplifyArraySelectLambda()

simplifyArrayStore()

simplifyArrayStoreLight()

simplifyBoolIteConstBranches()

simplifyBoolIteSameConditionBranch()

simplifyBv2IntExpr()

simplifyBv2IntExprLight()

simplifyBvAddExpr()

simplifyBvAddExprLight()

simplifyBvAddExprNestedAdd()

simplifyBvAddNoOverflowExpr()

simplifyBvAddNoUnderflowExpr()

simplifyBvAndExpr()

simplifyBvAndExprLight()

simplifyBvAndExprNestedAnd()

simplifyBvAndOr()

simplifyBvArithShiftRightExpr()

simplifyBvArithShiftRightExprLight()

simplifyBvConcatExpr()

simplifyBvConcatExprLight()

simplifyBvConcatExprNestedConcat()

simplifyBvDivNoOverflowExpr()

simplifyBvExtractExpr()

simplifyBvExtractExprLight()

simplifyBvExtractExprNestedExtract()

simplifyBvExtractExprTryRewrite()

simplifyBvLogicalShiftRightExpr()

simplifyBvLogicalShiftRightExprConstShift()

simplifyBvLogicalShiftRightExprLight()

simplifyBvMulExpr()

simplifyBvMulExprLight()

simplifyBvMulExprMinusOneConst()

simplifyBvMulExprNestedMul()

simplifyBvMulNoOverflowExpr()

simplifyBvMulNoUnderflowExpr()

simplifyBvNAndExpr()

simplifyBvNegationExpr()

simplifyBvNegationExprAdd()

simplifyBvNegationExprLight()

simplifyBvNegationNoOverflowExpr()

simplifyBvNorExpr()

simplifyBvNotExpr()

simplifyBvNotExprConcat()

simplifyBvNotExprIte()

simplifyBvNotExprLight()

simplifyBvOrExpr()

simplifyBvOrExprLight()

simplifyBvOrExprNestedOr()

simplifyBvReductionAndExpr()

simplifyBvReductionAndExprLight()

simplifyBvReductionOrExpr()

simplifyBvReductionOrExprLight()

simplifyBvRepeatExpr()

simplifyBvRepeatExprLight()

simplifyBvRotateLeftExpr()

simplifyBvRotateLeftExprConstRotation()

simplifyBvRotateLeftIndexedExpr()

simplifyBvRotateRightExpr()

simplifyBvRotateRightExprConstRotation()

simplifyBvRotateRightIndexedExpr()

simplifyBvShiftLeftExpr()

simplifyBvShiftLeftExprConstShift()

simplifyBvShiftLeftExprLight()

simplifyBvShiftLeftExprNestedShiftLeft()

simplifyBvSignedDivExpr()

simplifyBvSignedDivExprLight()

simplifyBvSignedGreaterExpr()

simplifyBvSignedGreaterOrEqualExpr()

simplifyBvSignedLessExpr()

simplifyBvSignedLessOrEqualExpr()

simplifyBvSignedLessOrEqualExprLight()

simplifyBvSignedModExpr()

simplifyBvSignedModExprLight()

simplifyBvSignedRemExpr()

simplifyBvSignedRemExprLight()

simplifyBvSignExtensionExpr()

simplifyBvSignExtensionExprLight()

simplifyBvSubExpr()

simplifyBvSubNoOverflowExpr()

simplifyBvSubNoUnderflowExpr()

simplifyBvToFpExpr()

simplifyBvToFpExprLight()

simplifyBvUnsignedDivExpr()

simplifyBvUnsignedDivExprLight()

simplifyBvUnsignedDivExprPowerOfTwoDivisor()

simplifyBvUnsignedGreaterExpr()

simplifyBvUnsignedGreaterOrEqualExpr()

simplifyBvUnsignedLessExpr()

simplifyBvUnsignedLessOrEqualExpr()

simplifyBvUnsignedRemExpr()

simplifyBvUnsignedRemExprLight()

simplifyBvUnsignedRemExprPowerOfTwoDivisor()

simplifyBvXNorExpr()

simplifyBvXorExpr()

simplifyBvXorExprLight()

simplifyBvXorExprMaxConst()

simplifyBvXorExprNestedXor()

simplifyBvZeroExtensionExpr()

simplifyBvZeroExtensionExprLight()

simplifyDistinct()

simplifyDistinctLight()

simplifyEqBool()

simplifyEqBoolLight()

simplifyEqBoolNot()

simplifyEqBvConcat()

simplifyEqBvLight()

simplifyEqFpLight()

simplifyEqIntLight()

simplifyEqLight()

simplifyEqRealLight()

simplifyExprBase()

simplifyFlatBvAddExpr()

simplifyFlatBvAndExpr()

simplifyFlatBvAndExprDistributeOverConcat()

simplifyFlatBvConcatExpr()

simplifyFlatBvMulExpr()

simplifyFlatBvOrExpr()

simplifyFlatBvOrExprDistributeOverConcat()

simplifyFlatBvXorExpr()

simplifyFlatBvXorExprDistributeOverConcat()

simplifyFpAbsExpr()

simplifyFpAbsExprLight()

simplifyFpAddExpr()

simplifyFpAddExprLight()

simplifyFpDivExpr()

simplifyFpDivExprLight()

simplifyFpEqualExpr()

simplifyFpEqualExprLight()

simplifyFpFromBvExpr()

simplifyFpFromBvExprLight()

simplifyFpFusedMulAddExpr()

simplifyFpFusedMulAddExprLight()

simplifyFpGreaterExpr()

simplifyFpGreaterOrEqualExpr()

simplifyFpIsInfiniteExpr()

simplifyFpIsInfiniteExprLight()

simplifyFpIsNaNExpr()

simplifyFpIsNaNExprLight()

simplifyFpIsNegativeExpr()

simplifyFpIsNegativeExprLight()

simplifyFpIsNormalExpr()

simplifyFpIsNormalExprLight()

simplifyFpIsPositiveExpr()

simplifyFpIsPositiveExprLight()

simplifyFpIsSubnormalExpr()

simplifyFpIsSubnormalExprLight()

simplifyFpIsZeroExpr()

simplifyFpIsZeroExprLight()

simplifyFpLessExpr()

simplifyFpLessExprLight()

simplifyFpLessOrEqualExpr()

simplifyFpLessOrEqualExprLight()

simplifyFpMaxExpr()

simplifyFpMaxExprLight()

simplifyFpMinExpr()

simplifyFpMinExprLight()

simplifyFpMulExpr()

simplifyFpMulExprLight()

simplifyFpNegationExpr()

simplifyFpNegationExprLight()

simplifyFpRemExpr()

simplifyFpRemExprLight()

simplifyFpRoundToIntegralExpr()

simplifyFpRoundToIntegralExprLight()

simplifyFpSqrtExpr()

simplifyFpSqrtExprLight()

simplifyFpSubExpr()

simplifyFpToBvExpr()

simplifyFpToBvExprLight()

simplifyFpToFpExpr()

simplifyFpToFpExprLight()

simplifyFpToIEEEBvExpr()

simplifyFpToIEEEBvExprLight()

simplifyFpToRealExpr()

simplifyFpToRealExprLight()

simplifyImplies()

simplifyIntMod()

simplifyIntModLight()

simplifyIntRem()

simplifyIntRemLight()

simplifyIntToReal()

simplifyIntToRealLight()

simplifyIteBool()

simplifyIteLight()

simplifyIteNotCondition()

simplifyIteSameBranches()

simplifyNotLight()

simplifyRealIsInt()

simplifyRealIsIntLight()

simplifyRealToFpExpr()

simplifyRealToFpExprLight()

simplifyRealToInt()

simplifyRealToIntLight()

simplifySelectFromArrayStore()

tryEvalArithPower()

tryMergeBvConcatExtract()

trySimplifyAndOrElement()

trySimplifyBvSignedMulNoOverflow()

trySimplifyBvUnsignedMulNoOverflow()

withExpressionsOrdered()

io.ksmt.expr.transformer

KExprVisitResult

KNonRecursiveTransformer

KNonRecursiveTransformerBase

KNonRecursiveVisitor

KNonRecursiveVisitorBase

KTransformerBase

KSMTLibParseException

KSolverConfiguration

KSolverException

KSolverUniversalConfigurationBuilder

KSolverUnsupportedFeatureException

KSolverUnsupportedParameterException

io.ksmt.solver.model

KFuncInterpEntry

KFuncInterpEntryNAry

KFuncInterpEntryOneAry

KFuncInterpEntryThreeAry

KFuncInterpEntryTwoAry

KFuncInterpEntryVarsFree

KFuncInterpEntryVarsFreeNAry

KFuncInterpEntryVarsFreeOneAry

KFuncInterpEntryVarsFreeThreeAry

KFuncInterpEntryVarsFreeTwoAry

KFuncInterpEntryWithVars

KFuncInterpEntryWithVarsNAry

KFuncInterpEntryWithVarsOneAry

KFuncInterpEntryWithVarsThreeAry

KFuncInterpEntryWithVarsTwoAry

KFuncInterpVarsFree

KFuncInterpWithVars

KModelEvaluator

KNativeSolverModel

io.ksmt.solver.util

conversionLoop()

ensureArgsConvertedAndConvert()

ExprConversionResult

internalizationLoop()

KExprConverterBase

KExprConverterUtils

KExprInternalizerBase

KExprIntInternalizerBase

KExprLongConverterBase

KExprLongInternalizerBase

transformList()

KBvCustomSizeSort

KFpCustomSizeSort

KFpRoundingModeSort

KUninterpretedSort

DefaultValueSampler

extendWithLeadingZeros()

extractExponent()

extractSignificand()

getHalfPrecisionExponent()

halfPrecisionSignificand

mkFreshConstDecl()

normalizeValue()

toUnsignedBigInteger()

uncheckedCast()

io.ksmt.utils.library

NativeLibraryLoader

NativeLibraryLoaderArm

NativeLibraryLoaderLinux

NativeLibraryLoaderMac

NativeLibraryLoaderUtils

NativeLibraryLoaderWindows

NativeLibraryLoaderX64

ksmt-core/io.ksmt/KContext/mkBvReductionOrDecl

mkBvReductionOrDecl

fun <T : KBvSort> mkBvReductionOrDecl(sort: T): KBvReductionOrDecl<T>

© 2024 CopyrightGenerated by dokka