ksmt-core/io.ksmt.expr.transformer/KTransformer

KTransformer

interface KTransformer : KTransformerBase

Functions

open fun <T : KSort> apply(expr: KExpr<T>): KExpr<T>

open override fun <T : KArithSort> transform(expr: KAddArithExpr<T>): KExpr<T>

open override fun transform(expr: KAndBinaryExpr): KExpr<KBoolSort>

open override fun transform(expr: KAndExpr): KExpr<KBoolSort>

open override fun <D0 : KSort, D1 : KSort, R : KSort> transform(expr: KArray2Lambda<D0, D1, R>): KExpr<KArray2Sort<D0, D1, R>>

open override fun <D0 : KSort, D1 : KSort, R : KSort> transform(expr: KArray2Select<D0, D1, R>): KExpr<R>

open override fun <D0 : KSort, D1 : KSort, R : KSort> transform(expr: KArray2Store<D0, D1, R>): KExpr<KArray2Sort<D0, D1, R>>

open override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(expr: KArray3Lambda<D0, D1, D2, R>): KExpr<KArray3Sort<D0, D1, D2, R>>

open override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(expr: KArray3Select<D0, D1, D2, R>): KExpr<R>

open override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(expr: KArray3Store<D0, D1, D2, R>): KExpr<KArray3Sort<D0, D1, D2, R>>

open override fun <A : KArraySortBase<R>, R : KSort> transform(expr: KArrayConst<A, R>): KExpr<A>

open override fun <D : KSort, R : KSort> transform(expr: KArrayLambda<D, R>): KExpr<KArraySort<D, R>>

open override fun <R : KSort> transform(expr: KArrayNLambda<R>): KExpr<KArrayNSort<R>>

open override fun <R : KSort> transform(expr: KArrayNSelect<R>): KExpr<R>

open override fun <R : KSort> transform(expr: KArrayNStore<R>): KExpr<KArrayNSort<R>>

open override fun <D : KSort, R : KSort> transform(expr: KArraySelect<D, R>): KExpr<R>

open override fun <D : KSort, R : KSort> transform(expr: KArrayStore<D, R>): KExpr<KArraySort<D, R>>

open override fun transform(expr: KBitVec16Value): KExpr<KBv16Sort>

open override fun transform(expr: KBitVec1Value): KExpr<KBv1Sort>

open override fun transform(expr: KBitVec32Value): KExpr<KBv32Sort>

open override fun transform(expr: KBitVec64Value): KExpr<KBv64Sort>

open override fun transform(expr: KBitVec8Value): KExpr<KBv8Sort>

open override fun transform(expr: KBitVecCustomValue): KExpr<KBvSort>

open override fun transform(expr: KBv2IntExpr): KExpr<KIntSort>

open override fun <T : KBvSort> transform(expr: KBvAddExpr<T>): KExpr<T>

open override fun <T : KBvSort> transform(expr: KBvAddNoOverflowExpr<T>): KExpr<KBoolSort>

open override fun <T : KBvSort> transform(expr: KBvAddNoUnderflowExpr<T>): KExpr<KBoolSort>

open override fun <T : KBvSort> transform(expr: KBvAndExpr<T>): KExpr<T>

open override fun <T : KBvSort> transform(expr: KBvArithShiftRightExpr<T>): KExpr<T>

open override fun transform(expr: KBvConcatExpr): KExpr<KBvSort>

open override fun <T : KBvSort> transform(expr: KBvDivNoOverflowExpr<T>): KExpr<KBoolSort>

open override fun transform(expr: KBvExtractExpr): KExpr<KBvSort>

open override fun <T : KBvSort> transform(expr: KBvLogicalShiftRightExpr<T>): KExpr<T>

open override fun <T : KBvSort> transform(expr: KBvMulExpr<T>): KExpr<T>

open override fun <T : KBvSort> transform(expr: KBvMulNoOverflowExpr<T>): KExpr<KBoolSort>

open override fun <T : KBvSort> transform(expr: KBvMulNoUnderflowExpr<T>): KExpr<KBoolSort>

open override fun <T : KBvSort> transform(expr: KBvNAndExpr<T>): KExpr<T>

open override fun <T : KBvSort> transform(expr: KBvNegNoOverflowExpr<T>): KExpr<KBoolSort>

open override fun <T : KBvSort> transform(expr: KBvNegationExpr<T>): KExpr<T>

open override fun <T : KBvSort> transform(expr: KBvNorExpr<T>): KExpr<T>

open override fun <T : KBvSort> transform(expr: KBvNotExpr<T>): KExpr<T>

open override fun <T : KBvSort> transform(expr: KBvOrExpr<T>): KExpr<T>

open override fun <T : KBvSort> transform(expr: KBvReductionAndExpr<T>): KExpr<KBv1Sort>

open override fun <T : KBvSort> transform(expr: KBvReductionOrExpr<T>): KExpr<KBv1Sort>

open override fun transform(expr: KBvRepeatExpr): KExpr<KBvSort>

open override fun <T : KBvSort> transform(expr: KBvRotateLeftExpr<T>): KExpr<T>

open override fun <T : KBvSort> transform(expr: KBvRotateLeftIndexedExpr<T>): KExpr<T>

open override fun <T : KBvSort> transform(expr: KBvRotateRightExpr<T>): KExpr<T>

open override fun <T : KBvSort> transform(expr: KBvRotateRightIndexedExpr<T>): KExpr<T>

open override fun <T : KBvSort> transform(expr: KBvShiftLeftExpr<T>): KExpr<T>

open override fun transform(expr: KBvSignExtensionExpr): KExpr<KBvSort>

open override fun <T : KBvSort> transform(expr: KBvSignedDivExpr<T>): KExpr<T>

open override fun <T : KBvSort> transform(expr: KBvSignedGreaterExpr<T>): KExpr<KBoolSort>

open override fun <T : KBvSort> transform(expr: KBvSignedGreaterOrEqualExpr<T>): KExpr<KBoolSort>

open override fun <T : KBvSort> transform(expr: KBvSignedLessExpr<T>): KExpr<KBoolSort>

open override fun <T : KBvSort> transform(expr: KBvSignedLessOrEqualExpr<T>): KExpr<KBoolSort>

open override fun <T : KBvSort> transform(expr: KBvSignedModExpr<T>): KExpr<T>

open override fun <T : KBvSort> transform(expr: KBvSignedRemExpr<T>): KExpr<T>

open override fun <T : KBvSort> transform(expr: KBvSubExpr<T>): KExpr<T>

open override fun <T : KBvSort> transform(expr: KBvSubNoOverflowExpr<T>): KExpr<KBoolSort>

open override fun <T : KBvSort> transform(expr: KBvSubNoUnderflowExpr<T>): KExpr<KBoolSort>

open override fun <T : KFpSort> transform(expr: KBvToFpExpr<T>): KExpr<T>

open override fun <T : KBvSort> transform(expr: KBvUnsignedDivExpr<T>): KExpr<T>

open override fun <T : KBvSort> transform(expr: KBvUnsignedGreaterExpr<T>): KExpr<KBoolSort>

open override fun <T : KBvSort> transform(expr: KBvUnsignedGreaterOrEqualExpr<T>): KExpr<KBoolSort>

open override fun <T : KBvSort> transform(expr: KBvUnsignedLessExpr<T>): KExpr<KBoolSort>

open override fun <T : KBvSort> transform(expr: KBvUnsignedLessOrEqualExpr<T>): KExpr<KBoolSort>

open override fun <T : KBvSort> transform(expr: KBvUnsignedRemExpr<T>): KExpr<T>

open override fun <T : KBvSort> transform(expr: KBvXNorExpr<T>): KExpr<T>

open override fun <T : KBvSort> transform(expr: KBvXorExpr<T>): KExpr<T>

open override fun transform(expr: KBvZeroExtensionExpr): KExpr<KBvSort>

open override fun <T : KSort> transform(expr: KConst<T>): KExpr<T>

open override fun <T : KSort> transform(expr: KDistinctExpr<T>): KExpr<KBoolSort>

open override fun <T : KArithSort> transform(expr: KDivArithExpr<T>): KExpr<T>

open override fun <T : KSort> transform(expr: KEqExpr<T>): KExpr<KBoolSort>

open override fun transform(expr: KExistentialQuantifier): KExpr<KBoolSort>

open override fun transform(expr: KExpr<*>): Any

open override fun transform(expr: KFalse): KExpr<KBoolSort>

open override fun transform(expr: KFp128Value): KExpr<KFp128Sort>

open override fun transform(expr: KFp16Value): KExpr<KFp16Sort>

open override fun transform(expr: KFp32Value): KExpr<KFp32Sort>

open override fun transform(expr: KFp64Value): KExpr<KFp64Sort>

open override fun <T : KFpSort> transform(expr: KFpAbsExpr<T>): KExpr<T>

open override fun <T : KFpSort> transform(expr: KFpAddExpr<T>): KExpr<T>

open override fun transform(expr: KFpCustomSizeValue): KExpr<KFpSort>

open override fun <T : KFpSort> transform(expr: KFpDivExpr<T>): KExpr<T>

open override fun <T : KFpSort> transform(expr: KFpEqualExpr<T>): KExpr<KBoolSort>

open override fun <T : KFpSort> transform(expr: KFpFromBvExpr<T>): KExpr<T>

open override fun <T : KFpSort> transform(expr: KFpFusedMulAddExpr<T>): KExpr<T>

open override fun <T : KFpSort> transform(expr: KFpGreaterExpr<T>): KExpr<KBoolSort>

open override fun <T : KFpSort> transform(expr: KFpGreaterOrEqualExpr<T>): KExpr<KBoolSort>

open override fun <T : KFpSort> transform(expr: KFpIsInfiniteExpr<T>): KExpr<KBoolSort>

open override fun <T : KFpSort> transform(expr: KFpIsNaNExpr<T>): KExpr<KBoolSort>

open override fun <T : KFpSort> transform(expr: KFpIsNegativeExpr<T>): KExpr<KBoolSort>

open override fun <T : KFpSort> transform(expr: KFpIsNormalExpr<T>): KExpr<KBoolSort>

open override fun <T : KFpSort> transform(expr: KFpIsPositiveExpr<T>): KExpr<KBoolSort>

open override fun <T : KFpSort> transform(expr: KFpIsSubnormalExpr<T>): KExpr<KBoolSort>

open override fun <T : KFpSort> transform(expr: KFpIsZeroExpr<T>): KExpr<KBoolSort>

open override fun <T : KFpSort> transform(expr: KFpLessExpr<T>): KExpr<KBoolSort>

open override fun <T : KFpSort> transform(expr: KFpLessOrEqualExpr<T>): KExpr<KBoolSort>

open override fun <T : KFpSort> transform(expr: KFpMaxExpr<T>): KExpr<T>

open override fun <T : KFpSort> transform(expr: KFpMinExpr<T>): KExpr<T>

open override fun <T : KFpSort> transform(expr: KFpMulExpr<T>): KExpr<T>

open override fun <T : KFpSort> transform(expr: KFpNegationExpr<T>): KExpr<T>

open override fun <T : KFpSort> transform(expr: KFpRemExpr<T>): KExpr<T>

open override fun <T : KFpSort> transform(expr: KFpRoundToIntegralExpr<T>): KExpr<T>

open override fun transform(expr: KFpRoundingModeExpr): KExpr<KFpRoundingModeSort>

open override fun <T : KFpSort> transform(expr: KFpSqrtExpr<T>): KExpr<T>

open override fun <T : KFpSort> transform(expr: KFpSubExpr<T>): KExpr<T>

open override fun <T : KFpSort> transform(expr: KFpToBvExpr<T>): KExpr<KBvSort>

open override fun <T : KFpSort> transform(expr: KFpToFpExpr<T>): KExpr<T>

open override fun <T : KFpSort> transform(expr: KFpToIEEEBvExpr<T>): KExpr<KBvSort>

open override fun <T : KFpSort> transform(expr: KFpToRealExpr<T>): KExpr<KRealSort>

open override fun <T : KSort> transform(expr: KFunctionApp<T>): KExpr<T>

open override fun <A : KArraySortBase<R>, R : KSort> transform(expr: KFunctionAsArray<A, R>): KExpr<A>

open override fun <T : KArithSort> transform(expr: KGeArithExpr<T>): KExpr<KBoolSort>

open override fun <T : KArithSort> transform(expr: KGtArithExpr<T>): KExpr<KBoolSort>

open override fun transform(expr: KImpliesExpr): KExpr<KBoolSort>

open override fun transform(expr: KInt32NumExpr): KExpr<KIntSort>

open override fun transform(expr: KInt64NumExpr): KExpr<KIntSort>

open override fun transform(expr: KIntBigNumExpr): KExpr<KIntSort>

open override fun transform(expr: KIsIntRealExpr): KExpr<KBoolSort>

open override fun <T : KSort> transform(expr: KIteExpr<T>): KExpr<T>

open override fun <T : KArithSort> transform(expr: KLeArithExpr<T>): KExpr<KBoolSort>

open override fun <T : KArithSort> transform(expr: KLtArithExpr<T>): KExpr<KBoolSort>

open override fun transform(expr: KModIntExpr): KExpr<KIntSort>

open override fun <T : KArithSort> transform(expr: KMulArithExpr<T>): KExpr<T>

open override fun transform(expr: KNotExpr): KExpr<KBoolSort>

open override fun transform(expr: KOrBinaryExpr): KExpr<KBoolSort>

open override fun transform(expr: KOrExpr): KExpr<KBoolSort>

open override fun <T : KArithSort> transform(expr: KPowerArithExpr<T>): KExpr<T>

open override fun transform(expr: KRealNumExpr): KExpr<KRealSort>

open override fun <T : KFpSort> transform(expr: KRealToFpExpr<T>): KExpr<T>

open override fun transform(expr: KRemIntExpr): KExpr<KIntSort>

open override fun <T : KArithSort> transform(expr: KSubArithExpr<T>): KExpr<T>

open override fun transform(expr: KToIntRealExpr): KExpr<KIntSort>

open override fun transform(expr: KToRealIntExpr): KExpr<KRealSort>

open override fun transform(expr: KTrue): KExpr<KBoolSort>

open override fun <T : KArithSort> transform(expr: KUnaryMinusArithExpr<T>): KExpr<T>

open override fun transform(expr: KUninterpretedSortValue): KExpr<KUninterpretedSort>

open override fun transform(expr: KUniversalQuantifier): KExpr<KBoolSort>

open override fun transform(expr: KXorExpr): KExpr<KBoolSort>

open fun <T : KSort, A : KSort> transformApp(expr: KApp<T, A>): KExpr<T>

transformArrayLambda

open fun <A : KArraySortBase<R>, R : KSort> transformArrayLambda(expr: KArrayLambdaBase<A, R>): KExpr<A>

transformArraySelect

open fun <A : KArraySortBase<R>, R : KSort> transformArraySelect(expr: KArraySelectBase<A, R>): KExpr<R>

transformArrayStore

open fun <A : KArraySortBase<R>, R : KSort> transformArrayStore(expr: KArrayStoreBase<A, R>): KExpr<A>

transformBitVecValue

open fun <T : KBvSort> transformBitVecValue(expr: KBitVecValue<T>): KExpr<T>

open fun <T : KSort> transformExpr(expr: KExpr<T>): KExpr<T>

transformFpValue

open fun <T : KFpSort> transformFpValue(expr: KFpValue<T>): KExpr<T>

transformIntNum

open fun transformIntNum(expr: KIntNumExpr): KExpr<KIntSort>

open fun <T : KSort> transformValue(expr: KInterpretedValue<T>): KExpr<T>

Properties

abstract val ctx: KContext

Inheritors

KExprSimplifierBase

KNonRecursiveTransformer

KNonRecursiveTransformerBase

Extensions

internalizationLoop

inline fun <T> KTransformerBase.internalizationLoop(exprStack: MutableList<KExpr<*>>, initialExpr: KExpr<*>, notInternalized: T, findInternalized: (KExpr<*>) -> T): T