ksmt-core/io.ksmt.solver.util/KExprIntInternalizerBase

KExprIntInternalizerBase

abstract class KExprIntInternalizerBase : KTransformerBase

Specialized version of KExprInternalizerBase for Int native expressions.

Constructors

Link copied to clipboard

Types

Link copied to clipboard
object Companion

Functions

Link copied to clipboard
open fun <T : KSort> apply(expr: KExpr<T>): KExpr<T>
Link copied to clipboard
abstract fun findInternalizedExpr(expr: KExpr<*>): Int

Return internalized expression or NOT_INTERNALIZED if expression was not internalized yet.

Link copied to clipboard
Link copied to clipboard
abstract fun saveInternalizedExpr(expr: KExpr<*>, internalized: Int)
Link copied to clipboard
abstract fun <T : KArithSort> transform(expr: KAddArithExpr<T>): KExpr<T>
abstract fun transform(expr: KAndBinaryExpr): KExpr<KBoolSort>
abstract fun transform(expr: KAndExpr): KExpr<KBoolSort>
abstract fun <D0 : KSort, D1 : KSort, R : KSort> transform(expr: KArray2Lambda<D0, D1, R>): KExpr<KArray2Sort<D0, D1, R>>
abstract fun <D0 : KSort, D1 : KSort, R : KSort> transform(expr: KArray2Select<D0, D1, R>): KExpr<R>
abstract fun <D0 : KSort, D1 : KSort, R : KSort> transform(expr: KArray2Store<D0, D1, R>): KExpr<KArray2Sort<D0, D1, R>>
abstract fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(expr: KArray3Lambda<D0, D1, D2, R>): KExpr<KArray3Sort<D0, D1, D2, R>>
abstract fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(expr: KArray3Select<D0, D1, D2, R>): KExpr<R>
abstract fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(expr: KArray3Store<D0, D1, D2, R>): KExpr<KArray3Sort<D0, D1, D2, R>>
abstract fun <A : KArraySortBase<R>, R : KSort> transform(expr: KArrayConst<A, R>): KExpr<A>
abstract fun <D : KSort, R : KSort> transform(expr: KArrayLambda<D, R>): KExpr<KArraySort<D, R>>
abstract fun <R : KSort> transform(expr: KArrayNLambda<R>): KExpr<KArrayNSort<R>>
abstract fun <R : KSort> transform(expr: KArrayNSelect<R>): KExpr<R>
abstract fun <R : KSort> transform(expr: KArrayNStore<R>): KExpr<KArrayNSort<R>>
abstract fun <D : KSort, R : KSort> transform(expr: KArraySelect<D, R>): KExpr<R>
abstract fun <D : KSort, R : KSort> transform(expr: KArrayStore<D, R>): KExpr<KArraySort<D, R>>
abstract fun transform(expr: KBitVec16Value): KExpr<KBv16Sort>
abstract fun transform(expr: KBitVec1Value): KExpr<KBv1Sort>
abstract fun transform(expr: KBitVec32Value): KExpr<KBv32Sort>
abstract fun transform(expr: KBitVec64Value): KExpr<KBv64Sort>
abstract fun transform(expr: KBitVec8Value): KExpr<KBv8Sort>
abstract fun transform(expr: KBitVecCustomValue): KExpr<KBvSort>
abstract fun transform(expr: KBv2IntExpr): KExpr<KIntSort>
abstract fun <T : KBvSort> transform(expr: KBvAddExpr<T>): KExpr<T>
abstract fun <T : KBvSort> transform(expr: KBvAddNoOverflowExpr<T>): KExpr<KBoolSort>
abstract fun <T : KBvSort> transform(expr: KBvAddNoUnderflowExpr<T>): KExpr<KBoolSort>
abstract fun <T : KBvSort> transform(expr: KBvAndExpr<T>): KExpr<T>
abstract fun <T : KBvSort> transform(expr: KBvArithShiftRightExpr<T>): KExpr<T>
abstract fun transform(expr: KBvConcatExpr): KExpr<KBvSort>
abstract fun <T : KBvSort> transform(expr: KBvDivNoOverflowExpr<T>): KExpr<KBoolSort>
abstract fun transform(expr: KBvExtractExpr): KExpr<KBvSort>
abstract fun <T : KBvSort> transform(expr: KBvLogicalShiftRightExpr<T>): KExpr<T>
abstract fun <T : KBvSort> transform(expr: KBvMulExpr<T>): KExpr<T>
abstract fun <T : KBvSort> transform(expr: KBvMulNoOverflowExpr<T>): KExpr<KBoolSort>
abstract fun <T : KBvSort> transform(expr: KBvMulNoUnderflowExpr<T>): KExpr<KBoolSort>
abstract fun <T : KBvSort> transform(expr: KBvNAndExpr<T>): KExpr<T>
abstract fun <T : KBvSort> transform(expr: KBvNegNoOverflowExpr<T>): KExpr<KBoolSort>
abstract fun <T : KBvSort> transform(expr: KBvNegationExpr<T>): KExpr<T>
abstract fun <T : KBvSort> transform(expr: KBvNorExpr<T>): KExpr<T>
abstract fun <T : KBvSort> transform(expr: KBvNotExpr<T>): KExpr<T>
abstract fun <T : KBvSort> transform(expr: KBvOrExpr<T>): KExpr<T>
abstract fun <T : KBvSort> transform(expr: KBvReductionAndExpr<T>): KExpr<KBv1Sort>
abstract fun <T : KBvSort> transform(expr: KBvReductionOrExpr<T>): KExpr<KBv1Sort>
abstract fun transform(expr: KBvRepeatExpr): KExpr<KBvSort>
abstract fun <T : KBvSort> transform(expr: KBvRotateLeftExpr<T>): KExpr<T>
abstract fun <T : KBvSort> transform(expr: KBvRotateLeftIndexedExpr<T>): KExpr<T>
abstract fun <T : KBvSort> transform(expr: KBvRotateRightExpr<T>): KExpr<T>
abstract fun <T : KBvSort> transform(expr: KBvRotateRightIndexedExpr<T>): KExpr<T>
abstract fun <T : KBvSort> transform(expr: KBvShiftLeftExpr<T>): KExpr<T>
abstract fun transform(expr: KBvSignExtensionExpr): KExpr<KBvSort>
abstract fun <T : KBvSort> transform(expr: KBvSignedDivExpr<T>): KExpr<T>
abstract fun <T : KBvSort> transform(expr: KBvSignedGreaterExpr<T>): KExpr<KBoolSort>
abstract fun <T : KBvSort> transform(expr: KBvSignedGreaterOrEqualExpr<T>): KExpr<KBoolSort>
abstract fun <T : KBvSort> transform(expr: KBvSignedLessExpr<T>): KExpr<KBoolSort>
abstract fun <T : KBvSort> transform(expr: KBvSignedLessOrEqualExpr<T>): KExpr<KBoolSort>
abstract fun <T : KBvSort> transform(expr: KBvSignedModExpr<T>): KExpr<T>
abstract fun <T : KBvSort> transform(expr: KBvSignedRemExpr<T>): KExpr<T>
abstract fun <T : KBvSort> transform(expr: KBvSubExpr<T>): KExpr<T>
abstract fun <T : KBvSort> transform(expr: KBvSubNoOverflowExpr<T>): KExpr<KBoolSort>
abstract fun <T : KBvSort> transform(expr: KBvSubNoUnderflowExpr<T>): KExpr<KBoolSort>
abstract fun <T : KFpSort> transform(expr: KBvToFpExpr<T>): KExpr<T>
abstract fun <T : KBvSort> transform(expr: KBvUnsignedDivExpr<T>): KExpr<T>
abstract fun <T : KBvSort> transform(expr: KBvUnsignedGreaterExpr<T>): KExpr<KBoolSort>
abstract fun <T : KBvSort> transform(expr: KBvUnsignedGreaterOrEqualExpr<T>): KExpr<KBoolSort>
abstract fun <T : KBvSort> transform(expr: KBvUnsignedLessExpr<T>): KExpr<KBoolSort>
abstract fun <T : KBvSort> transform(expr: KBvUnsignedLessOrEqualExpr<T>): KExpr<KBoolSort>
abstract fun <T : KBvSort> transform(expr: KBvUnsignedRemExpr<T>): KExpr<T>
abstract fun <T : KBvSort> transform(expr: KBvXNorExpr<T>): KExpr<T>
abstract fun <T : KBvSort> transform(expr: KBvXorExpr<T>): KExpr<T>
abstract fun transform(expr: KBvZeroExtensionExpr): KExpr<KBvSort>
abstract fun <T : KSort> transform(expr: KConst<T>): KExpr<T>
abstract fun <T : KSort> transform(expr: KDistinctExpr<T>): KExpr<KBoolSort>
abstract fun <T : KArithSort> transform(expr: KDivArithExpr<T>): KExpr<T>
abstract fun <T : KSort> transform(expr: KEqExpr<T>): KExpr<KBoolSort>
abstract fun transform(expr: KExistentialQuantifier): KExpr<KBoolSort>
open fun transform(expr: KExpr<*>): Any
abstract fun transform(expr: KFalse): KExpr<KBoolSort>
abstract fun transform(expr: KFp128Value): KExpr<KFp128Sort>
abstract fun transform(expr: KFp16Value): KExpr<KFp16Sort>
abstract fun transform(expr: KFp32Value): KExpr<KFp32Sort>
abstract fun transform(expr: KFp64Value): KExpr<KFp64Sort>
abstract fun <T : KFpSort> transform(expr: KFpAbsExpr<T>): KExpr<T>
abstract fun <T : KFpSort> transform(expr: KFpAddExpr<T>): KExpr<T>
abstract fun transform(expr: KFpCustomSizeValue): KExpr<KFpSort>
abstract fun <T : KFpSort> transform(expr: KFpDivExpr<T>): KExpr<T>
abstract fun <T : KFpSort> transform(expr: KFpEqualExpr<T>): KExpr<KBoolSort>
abstract fun <T : KFpSort> transform(expr: KFpFromBvExpr<T>): KExpr<T>
abstract fun <T : KFpSort> transform(expr: KFpFusedMulAddExpr<T>): KExpr<T>
abstract fun <T : KFpSort> transform(expr: KFpGreaterExpr<T>): KExpr<KBoolSort>
abstract fun <T : KFpSort> transform(expr: KFpGreaterOrEqualExpr<T>): KExpr<KBoolSort>
abstract fun <T : KFpSort> transform(expr: KFpIsInfiniteExpr<T>): KExpr<KBoolSort>
abstract fun <T : KFpSort> transform(expr: KFpIsNaNExpr<T>): KExpr<KBoolSort>
abstract fun <T : KFpSort> transform(expr: KFpIsNegativeExpr<T>): KExpr<KBoolSort>
abstract fun <T : KFpSort> transform(expr: KFpIsNormalExpr<T>): KExpr<KBoolSort>
abstract fun <T : KFpSort> transform(expr: KFpIsPositiveExpr<T>): KExpr<KBoolSort>
abstract fun <T : KFpSort> transform(expr: KFpIsSubnormalExpr<T>): KExpr<KBoolSort>
abstract fun <T : KFpSort> transform(expr: KFpIsZeroExpr<T>): KExpr<KBoolSort>
abstract fun <T : KFpSort> transform(expr: KFpLessExpr<T>): KExpr<KBoolSort>
abstract fun <T : KFpSort> transform(expr: KFpLessOrEqualExpr<T>): KExpr<KBoolSort>
abstract fun <T : KFpSort> transform(expr: KFpMaxExpr<T>): KExpr<T>
abstract fun <T : KFpSort> transform(expr: KFpMinExpr<T>): KExpr<T>
abstract fun <T : KFpSort> transform(expr: KFpMulExpr<T>): KExpr<T>
abstract fun <T : KFpSort> transform(expr: KFpNegationExpr<T>): KExpr<T>
abstract fun <T : KFpSort> transform(expr: KFpRemExpr<T>): KExpr<T>
abstract fun <T : KFpSort> transform(expr: KFpRoundToIntegralExpr<T>): KExpr<T>
abstract fun transform(expr: KFpRoundingModeExpr): KExpr<KFpRoundingModeSort>
abstract fun <T : KFpSort> transform(expr: KFpSqrtExpr<T>): KExpr<T>
abstract fun <T : KFpSort> transform(expr: KFpSubExpr<T>): KExpr<T>
abstract fun <T : KFpSort> transform(expr: KFpToBvExpr<T>): KExpr<KBvSort>
abstract fun <T : KFpSort> transform(expr: KFpToFpExpr<T>): KExpr<T>
abstract fun <T : KFpSort> transform(expr: KFpToIEEEBvExpr<T>): KExpr<KBvSort>
abstract fun <T : KFpSort> transform(expr: KFpToRealExpr<T>): KExpr<KRealSort>
abstract fun <T : KSort> transform(expr: KFunctionApp<T>): KExpr<T>
abstract fun <A : KArraySortBase<R>, R : KSort> transform(expr: KFunctionAsArray<A, R>): KExpr<A>
abstract fun <T : KArithSort> transform(expr: KGeArithExpr<T>): KExpr<KBoolSort>
abstract fun <T : KArithSort> transform(expr: KGtArithExpr<T>): KExpr<KBoolSort>
abstract fun transform(expr: KImpliesExpr): KExpr<KBoolSort>
abstract fun transform(expr: KInt32NumExpr): KExpr<KIntSort>
abstract fun transform(expr: KInt64NumExpr): KExpr<KIntSort>
abstract fun transform(expr: KIntBigNumExpr): KExpr<KIntSort>
abstract fun transform(expr: KIsIntRealExpr): KExpr<KBoolSort>
abstract fun <T : KSort> transform(expr: KIteExpr<T>): KExpr<T>
abstract fun <T : KArithSort> transform(expr: KLeArithExpr<T>): KExpr<KBoolSort>
abstract fun <T : KArithSort> transform(expr: KLtArithExpr<T>): KExpr<KBoolSort>
abstract fun transform(expr: KModIntExpr): KExpr<KIntSort>
abstract fun <T : KArithSort> transform(expr: KMulArithExpr<T>): KExpr<T>
abstract fun transform(expr: KNotExpr): KExpr<KBoolSort>
abstract fun transform(expr: KOrBinaryExpr): KExpr<KBoolSort>
abstract fun transform(expr: KOrExpr): KExpr<KBoolSort>
abstract fun <T : KArithSort> transform(expr: KPowerArithExpr<T>): KExpr<T>
abstract fun transform(expr: KRealNumExpr): KExpr<KRealSort>
abstract fun <T : KFpSort> transform(expr: KRealToFpExpr<T>): KExpr<T>
abstract fun transform(expr: KRemIntExpr): KExpr<KIntSort>
abstract fun <T : KArithSort> transform(expr: KSubArithExpr<T>): KExpr<T>
abstract fun transform(expr: KToIntRealExpr): KExpr<KIntSort>
abstract fun transform(expr: KToRealIntExpr): KExpr<KRealSort>
abstract fun transform(expr: KTrue): KExpr<KBoolSort>
abstract fun <T : KArithSort> transform(expr: KUnaryMinusArithExpr<T>): KExpr<T>
abstract fun transform(expr: KUninterpretedSortValue): KExpr<KUninterpretedSort>
abstract fun transform(expr: KUniversalQuantifier): KExpr<KBoolSort>
abstract fun transform(expr: KXorExpr): KExpr<KBoolSort>
inline fun <S : KExpr<*>> S.transform(operation: () -> Int): S
inline fun <S : KExpr<*>> S.transform(arg: KExpr<*>, operation: (Int) -> Int): S
inline fun <S : KExpr<*>> S.transform(arg0: KExpr<*>, arg1: KExpr<*>, operation: (Int, Int) -> Int): S
inline fun <S : KExpr<*>> S.transform(arg0: KExpr<*>, arg1: KExpr<*>, arg2: KExpr<*>, operation: (Int, Int, Int) -> Int): S
inline fun <S : KExpr<*>> S.transform(arg0: KExpr<*>, arg1: KExpr<*>, arg2: KExpr<*>, arg3: KExpr<*>, operation: (Int, Int, Int, Int) -> Int): S
Link copied to clipboard
inline fun <S : KExpr<*>> S.transformList(args: List<KExpr<*>>, operation: (IntArray) -> Int): S

Properties

Link copied to clipboard

Extensions

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