ksmt-core/io.ksmt.expr

Package-level declarations

Types

KAddArithExpr

class KAddArithExpr<T : KArithSort> : KApp<T, T>

KAndBinaryExpr

class KAndBinaryExpr : KAndExpr

KAndExpr

abstract class KAndExpr(ctx: KContext) : KApp<KBoolSort, KBoolSort>

KAndNaryExpr

class KAndNaryExpr : KAndExpr

KApp

abstract class KApp<T : KSort, A : KSort> : KExpr<T>

KArray2Lambda

class KArray2Lambda<D0 : KSort, D1 : KSort, R : KSort> : KArrayLambdaBase<KArray2Sort<D0, D1, R>, R>

KArray2Select

class KArray2Select<D0 : KSort, D1 : KSort, R : KSort> : KArraySelectBase<KArray2Sort<D0, D1, R>, R>

KArray2Store

class KArray2Store<D0 : KSort, D1 : KSort, R : KSort> : KArrayStoreBase<KArray2Sort<D0, D1, R>, R>

KArray3Lambda

class KArray3Lambda<D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> : KArrayLambdaBase<KArray3Sort<D0, D1, D2, R>, R>

KArray3Select

class KArray3Select<D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> : KArraySelectBase<KArray3Sort<D0, D1, D2, R>, R>

KArray3Store

class KArray3Store<D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> : KArrayStoreBase<KArray3Sort<D0, D1, D2, R>, R>

KArrayConst

class KArrayConst<A : KArraySortBase<R>, R : KSort> : KApp<A, R>

KArrayLambda

class KArrayLambda<D : KSort, R : KSort> : KArrayLambdaBase<KArraySort<D, R>, R>

KArrayLambdaBase

sealed class KArrayLambdaBase<A : KArraySortBase<R>, R : KSort> : KExpr<A>

Array lambda binding.

KArrayNLambda

class KArrayNLambda<R : KSort> : KArrayLambdaBase<KArrayNSort<R>, R>

KArrayNSelect

class KArrayNSelect<R : KSort> : KArraySelectBase<KArrayNSort<R>, R>

KArrayNStore

class KArrayNStore<R : KSort> : KArrayStoreBase<KArrayNSort<R>, R>

KArraySelect

class KArraySelect<D : KSort, R : KSort> : KArraySelectBase<KArraySort<D, R>, R>

KArraySelectBase

sealed class KArraySelectBase<A : KArraySortBase<R>, R : KSort> : KApp<R, KSort>

KArrayStore

class KArrayStore<D : KSort, R : KSort> : KArrayStoreBase<KArraySort<D, R>, R>

KArrayStoreBase

sealed class KArrayStoreBase<A : KArraySortBase<R>, R : KSort> : KApp<A, KSort>

Base expression for various array store expressions with interpreted indices cache support.

KBitVec16Value

class KBitVec16Value : KBitVecNumberValue<KBv16Sort, Short>

KBitVec1Value

class KBitVec1Value : KBitVecValue<KBv1Sort>

KBitVec32Value

class KBitVec32Value : KBitVecNumberValue<KBv32Sort, Int>

KBitVec64Value

class KBitVec64Value : KBitVecNumberValue<KBv64Sort, Long>

KBitVec8Value

class KBitVec8Value : KBitVecNumberValue<KBv8Sort, Byte>

KBitVecCustomValue

class KBitVecCustomValue : KBitVecValue<KBvSort>

KBitVecNumberValue

abstract class KBitVecNumberValue<S : KBvSort, N : Number>(ctx: KContext) : KBitVecValue<S>

KBitVecValue

abstract class KBitVecValue<S : KBvSort>(ctx: KContext) : KInterpretedValue<S>

KBv2IntExpr

class KBv2IntExpr : KApp<KIntSort, KBvSort>

Creates an integer from the bit-vector argument value.

KBvAddExpr

class KBvAddExpr<S : KBvSort> : KApp<S, S>

Two's complement addition.

KBvAddNoOverflowExpr

class KBvAddNoOverflowExpr<S : KBvSort> : KApp<KBoolSort, S>

KBvAddNoUnderflowExpr

class KBvAddNoUnderflowExpr<S : KBvSort> : KApp<KBoolSort, S>

KBvAndExpr

class KBvAndExpr<S : KBvSort> : KApp<S, S>

Bitwise conjunction.

KBvArithShiftRightExpr

class KBvArithShiftRightExpr<S : KBvSort> : KApp<S, S>

Arithmetic shift right.

KBvConcatExpr

class KBvConcatExpr : KApp<KBvSort, KBvSort>

Bit-vector concatenation.

KBvDivNoOverflowExpr

class KBvDivNoOverflowExpr<S : KBvSort> : KApp<KBoolSort, S>

KBvExtractExpr

class KBvExtractExpr : KApp<KBvSort, KBvSort>

Bit-vector extraction.

KBvLogicalShiftRightExpr

class KBvLogicalShiftRightExpr<S : KBvSort> : KApp<S, S>

Logical shift right.

KBvMulExpr

class KBvMulExpr<S : KBvSort> : KApp<S, S>

Two's complement multiplication.

KBvMulNoOverflowExpr

class KBvMulNoOverflowExpr<S : KBvSort> : KApp<KBoolSort, S>

KBvMulNoUnderflowExpr

class KBvMulNoUnderflowExpr<S : KBvSort> : KApp<KBoolSort, S>

KBvNAndExpr

class KBvNAndExpr<S : KBvSort> : KApp<S, S>

Bitwise NAND.

KBvNegationExpr

class KBvNegationExpr<S : KBvSort> : KApp<S, S>

Standard two's complement unary minus.

KBvNegNoOverflowExpr

class KBvNegNoOverflowExpr<S : KBvSort> : KApp<KBoolSort, S>

KBvNorExpr

class KBvNorExpr<S : KBvSort> : KApp<S, S>

Bitwise NOR.

KBvNotExpr

class KBvNotExpr<S : KBvSort> : KApp<S, S>

Bitwise negation.

KBvOrExpr

class KBvOrExpr<S : KBvSort> : KApp<S, S>

Bitwise disjunction.

KBvReductionAndExpr

class KBvReductionAndExpr<S : KBvSort> : KApp<KBv1Sort, S>

Takes conjunction of bits in the value, return a vector of length 1.

KBvReductionOrExpr

class KBvReductionOrExpr<S : KBvSort> : KApp<KBv1Sort, S>

Take disjunction of bits in value, return a vector of length 1.

KBvRepeatExpr

class KBvRepeatExpr : KApp<KBvSort, KBvSort>

Bit-vector repetition.

KBvRotateLeftExpr

class KBvRotateLeftExpr<S : KBvSort> : KApp<S, S>

Rotate left.

KBvRotateLeftIndexedExpr

class KBvRotateLeftIndexedExpr<S : KBvSort> : KApp<S, S>

Rotate left.

KBvRotateRightExpr

class KBvRotateRightExpr<S : KBvSort> : KApp<S, S>

Rotate right.

KBvRotateRightIndexedExpr

class KBvRotateRightIndexedExpr<S : KBvSort> : KApp<S, S>

Rotate right.

KBvShiftLeftExpr

class KBvShiftLeftExpr<S : KBvSort> : KApp<S, S>

Shift left.

KBvSignedDivExpr

class KBvSignedDivExpr<S : KBvSort> : KApp<S, S>

Signed division.

KBvSignedGreaterExpr

class KBvSignedGreaterExpr<S : KBvSort> : KApp<KBoolSort, S>

Two's complement signed greater-than.

KBvSignedGreaterOrEqualExpr

class KBvSignedGreaterOrEqualExpr<S : KBvSort> : KApp<KBoolSort, S>

Two's complement signed greater than or equal to.

KBvSignedLessExpr

class KBvSignedLessExpr<S : KBvSort> : KApp<KBoolSort, S>

Two's complement signed less-than.

KBvSignedLessOrEqualExpr

class KBvSignedLessOrEqualExpr<S : KBvSort> : KApp<KBoolSort, S>

Two's complement signed less-than or equal to.

KBvSignedModExpr

class KBvSignedModExpr<S : KBvSort> : KApp<S, S>

Two's complement signed remainder (sign follows divisor). If arg1 is zero, then the result is undefined.

KBvSignedRemExpr

class KBvSignedRemExpr<S : KBvSort> : KApp<S, S>

Signed remainder.

KBvSignExtensionExpr

class KBvSignExtensionExpr : KApp<KBvSort, KBvSort>

Bit-vector sign extension.

KBvSubExpr

class KBvSubExpr<S : KBvSort> : KApp<S, S>

Two's complement subtraction.

KBvSubNoOverflowExpr

class KBvSubNoOverflowExpr<S : KBvSort> : KApp<KBoolSort, S>

KBvSubNoUnderflowExpr

class KBvSubNoUnderflowExpr<S : KBvSort> : KApp<KBoolSort, S>

KBvToFpExpr

class KBvToFpExpr<S : KFpSort> : KApp<S, KSort>

KBvUnsignedDivExpr

class KBvUnsignedDivExpr<S : KBvSort> : KApp<S, S>

Unsigned division.

KBvUnsignedGreaterExpr

class KBvUnsignedGreaterExpr<S : KBvSort> : KApp<KBoolSort, S>

Unsigned greater-than.

KBvUnsignedGreaterOrEqualExpr

class KBvUnsignedGreaterOrEqualExpr<S : KBvSort> : KApp<KBoolSort, S>

Unsigned greater than or equal to.

KBvUnsignedLessExpr

class KBvUnsignedLessExpr<S : KBvSort> : KApp<KBoolSort, S>

Unsigned less-than.

KBvUnsignedLessOrEqualExpr

class KBvUnsignedLessOrEqualExpr<S : KBvSort> : KApp<KBoolSort, S>

Unsigned less-than or equal to.

KBvUnsignedRemExpr

class KBvUnsignedRemExpr<S : KBvSort> : KApp<S, S>

Unsigned remainder.

KBvXNorExpr

class KBvXNorExpr<S : KBvSort> : KApp<S, S>

Bitwise XNOR.

KBvXorExpr

class KBvXorExpr<S : KBvSort> : KApp<S, S>

Bitwise XOR.

KBvZeroExtensionExpr

class KBvZeroExtensionExpr : KApp<KBvSort, KBvSort>

Bit-vector zero extension.

KConst

class KConst<T : KSort> : KFunctionApp<T>

KDistinctExpr

class KDistinctExpr<T : KSort> : KApp<KBoolSort, T>

KDivArithExpr

class KDivArithExpr<T : KArithSort> : KApp<T, T>

KEqExpr

class KEqExpr<T : KSort> : KApp<KBoolSort, T>

KExistentialQuantifier

class KExistentialQuantifier : KQuantifier

KExpr

abstract class KExpr<T : KSort>(val ctx: KContext) : KAst, KInternedObject

KFalse

class KFalse(ctx: KContext) : KInterpretedValue<KBoolSort>

KFp128Value

class KFp128Value : KFpValue<KFp128Sort>

KFp128 value.

KFp16Value

class KFp16Value : KFpValue<KFp16Sort>

Fp16 value. Note that value should has biased Fp32 exponent, but a constructed Fp16 will have an unbiased one.

KFp32Value

class KFp32Value : KFpValue<KFp32Sort>

KFp64Value

class KFp64Value : KFpValue<KFp64Sort>

KFpAbsExpr

class KFpAbsExpr<S : KFpSort> : KApp<S, S>

KFpAddExpr

class KFpAddExpr<S : KFpSort> : KApp<S, KSort>

KFpCustomSizeValue

class KFpCustomSizeValue : KFpValue<KFpSort>

KFp value of custom size.

KFpDivExpr

class KFpDivExpr<S : KFpSort> : KApp<S, KSort>

KFpEqualExpr

class KFpEqualExpr<S : KFpSort> : KApp<KBoolSort, S>

KFpFromBvExpr

class KFpFromBvExpr<S : KFpSort> : KApp<S, KBvSort>

KFpFusedMulAddExpr

class KFpFusedMulAddExpr<S : KFpSort> : KApp<S, KSort>

KFpGreaterExpr

class KFpGreaterExpr<S : KFpSort> : KApp<KBoolSort, S>

KFpGreaterOrEqualExpr

class KFpGreaterOrEqualExpr<S : KFpSort> : KApp<KBoolSort, S>

KFpIsInfiniteExpr

class KFpIsInfiniteExpr<S : KFpSort> : KApp<KBoolSort, S>

KFpIsNaNExpr

class KFpIsNaNExpr<S : KFpSort> : KApp<KBoolSort, S>

KFpIsNegativeExpr

class KFpIsNegativeExpr<S : KFpSort> : KApp<KBoolSort, S>

KFpIsNormalExpr

class KFpIsNormalExpr<S : KFpSort> : KApp<KBoolSort, S>

KFpIsPositiveExpr

class KFpIsPositiveExpr<S : KFpSort> : KApp<KBoolSort, S>

KFpIsSubnormalExpr

class KFpIsSubnormalExpr<S : KFpSort> : KApp<KBoolSort, S>

KFpIsZeroExpr

class KFpIsZeroExpr<S : KFpSort> : KApp<KBoolSort, S>

KFpLessExpr

class KFpLessExpr<S : KFpSort> : KApp<KBoolSort, S>

KFpLessOrEqualExpr

class KFpLessOrEqualExpr<S : KFpSort> : KApp<KBoolSort, S>

KFpMaxExpr

class KFpMaxExpr<S : KFpSort> : KApp<S, S>

KFpMinExpr

class KFpMinExpr<S : KFpSort> : KApp<S, S>

KFpMulExpr

class KFpMulExpr<S : KFpSort> : KApp<S, KSort>

KFpNegationExpr

class KFpNegationExpr<S : KFpSort> : KApp<S, S>

Inverts the sign bit.

KFpRemExpr

class KFpRemExpr<S : KFpSort> : KApp<S, S>

KFpRoundingMode

enum KFpRoundingMode : Enum<KFpRoundingMode>

KFpRoundingModeExpr

class KFpRoundingModeExpr(ctx: KContext, val value: KFpRoundingMode) : KInterpretedValue<KFpRoundingModeSort>

KFpRoundToIntegralExpr

class KFpRoundToIntegralExpr<S : KFpSort> : KApp<S, KSort>

KFpSqrtExpr

class KFpSqrtExpr<S : KFpSort> : KApp<S, KSort>

KFpSubExpr

class KFpSubExpr<S : KFpSort> : KApp<S, KSort>

KFpToBvExpr

class KFpToBvExpr<S : KFpSort> : KApp<KBvSort, KSort>

KFpToFpExpr

class KFpToFpExpr<S : KFpSort> : KApp<S, KSort>

KFpToIEEEBvExpr

class KFpToIEEEBvExpr<S : KFpSort> : KApp<KBvSort, S>

KFpToRealExpr

class KFpToRealExpr<S : KFpSort> : KApp<KRealSort, S>

KFpValue

abstract class KFpValue<T : KFpSort>(ctx: KContext) : KInterpretedValue<T>

KFunctionApp

open class KFunctionApp<T : KSort> : KApp<T, KSort>

KFunctionAsArray

class KFunctionAsArray<A : KArraySortBase<R>, R : KSort> : KExpr<A>

KGeArithExpr

class KGeArithExpr<T : KArithSort> : KApp<KBoolSort, T>

KGtArithExpr

class KGtArithExpr<T : KArithSort> : KApp<KBoolSort, T>

KImpliesExpr

class KImpliesExpr : KApp<KBoolSort, KBoolSort>

KInt32NumExpr

class KInt32NumExpr : KIntNumExpr

KInt64NumExpr

class KInt64NumExpr : KIntNumExpr

KIntBigNumExpr

class KIntBigNumExpr : KIntNumExpr

KInterpretedValue

abstract class KInterpretedValue<T : KSort>(ctx: KContext) : KApp<T, KSort>

Specify that the expression is an interpreted value in some theory.

KIntNumExpr

abstract class KIntNumExpr(ctx: KContext, value: Number) : KInterpretedValue<KIntSort>

KIsIntRealExpr

class KIsIntRealExpr : KApp<KBoolSort, KRealSort>

KIteExpr

class KIteExpr<T : KSort> : KApp<T, KSort>

KLeArithExpr

class KLeArithExpr<T : KArithSort> : KApp<KBoolSort, T>

KLtArithExpr

class KLtArithExpr<T : KArithSort> : KApp<KBoolSort, T>

KModIntExpr

class KModIntExpr : KApp<KIntSort, KIntSort>

KMulArithExpr

class KMulArithExpr<T : KArithSort> : KApp<T, T>

KNotExpr

class KNotExpr : KApp<KBoolSort, KBoolSort>

KOrBinaryExpr

class KOrBinaryExpr : KOrExpr

KOrExpr

abstract class KOrExpr(ctx: KContext) : KApp<KBoolSort, KBoolSort>

KOrNaryExpr

class KOrNaryExpr : KOrExpr

KPowerArithExpr

class KPowerArithExpr<T : KArithSort> : KApp<T, T>

KQuantifier

abstract class KQuantifier(ctx: KContext, val body: KExpr<KBoolSort>, val bounds: List<KDecl<*>>) : KExpr<KBoolSort>

KRealNumExpr

class KRealNumExpr : KInterpretedValue<KRealSort>

KRealToFpExpr

class KRealToFpExpr<S : KFpSort> : KApp<S, KSort>

KRemIntExpr

class KRemIntExpr : KApp<KIntSort, KIntSort>

KSubArithExpr

class KSubArithExpr<T : KArithSort> : KApp<T, T>

KToIntRealExpr

class KToIntRealExpr : KApp<KIntSort, KRealSort>

KToRealIntExpr

class KToRealIntExpr : KApp<KRealSort, KIntSort>

KTrue

class KTrue(ctx: KContext) : KInterpretedValue<KBoolSort>

KUnaryMinusArithExpr

class KUnaryMinusArithExpr<T : KArithSort> : KApp<T, T>

KUninterpretedSortValue

class KUninterpretedSortValue : KInterpretedValue<KUninterpretedSort>

KUniversalQuantifier

class KUniversalQuantifier : KQuantifier

KXorExpr

class KXorExpr : KApp<KBoolSort, KBoolSort>