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

KNonRecursiveTransformerBase

abstract class KNonRecursiveTransformerBase : KTransformer

Non-recursive expression transformer.

Standard use-case: perform bottom-up expression transformation. In this scenario, we need to transform expression arguments first, and then perform transformation of the expression using the transformed arguments. For this scenario, non-recursive transformer provides a transformExprAfterTransformed method.

Constructors

Link copied to clipboard

Functions

Link copied to clipboard
open override fun <T : KSort> apply(expr: KExpr<T>): KExpr<T>

Transform expr and all it sub-expressions non-recursively.

Link copied to clipboard
fun eraseTransformationResult(expr: KExpr<*>)

Erase expr transformation result. Useful for transformer auxiliary expressions.

Link copied to clipboard
open fun <T : KSort> exprTransformationRequired(expr: KExpr<T>): Boolean

Allows to skip expression transformation and stop deepening.

Link copied to clipboard
fun markExpressionAsNotTransformed()

Inform KNonRecursiveTransformer that transformation was not applied to expression

Link copied to clipboard
fun resetCache()

Reset transformer expression cache.

Link copied to clipboard
Link copied to clipboard
abstract override fun <D0 : KSort, D1 : KSort, R : KSort> transform(expr: KArray2Lambda<D0, D1, R>): KExpr<KArray2Sort<D0, D1, R>>

Disable KTransformer transform KArray2Lambda implementation since it is incorrect for non-recursive usage.

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

Disable KTransformer transform KArray3Lambda implementation since it is incorrect for non-recursive usage.

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

Disable KTransformer transform KArrayLambda implementation since it is incorrect for non-recursive usage.

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

Disable KTransformer transform KArrayNLambda implementation since it is incorrect for non-recursive usage.

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

Disable KTransformer transform KExistentialQuantifier implementation since it is incorrect for non-recursive usage.

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

Disable KTransformer transform KUniversalQuantifier implementation since it is incorrect for non-recursive usage.

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: 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: 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 <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: 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: KXorExpr): KExpr<KBoolSort>
Link copied to clipboard
fun KExpr<*>.transformAfter(dependency: KExpr<*>)

fun KExpr<*>.transformAfter(dependencies: List<KExpr<*>>)

Transform this expression after dependencies expressions

Link copied to clipboard
abstract override fun <T : KSort, A : KSort> transformApp(expr: KApp<T, A>): KExpr<T>

Disable KTransformer transformApp implementation since it is incorrect for non-recursive usage.

Link copied to clipboard
inline fun <T : KSort, A : KSort> transformAppAfterArgsTransformed(expr: KApp<T, A>, transformer: (List<KExpr<A>>) -> KExpr<T>): KExpr<T>

KApp non-recursive transformation helper.

Link copied to clipboard
Link copied to clipboard
Link copied to clipboard
Link copied to clipboard
Link copied to clipboard
fun <T : KSort> transformedExpr(expr: KExpr<T>): KExpr<T>?

Get expr transformation result or null if expression was not transformed yet

Link copied to clipboard
open fun <T : KSort> transformExpr(expr: KExpr<T>): KExpr<T>
Link copied to clipboard
inline fun <T : KSort, A : KSort> transformExprAfterTransformed(expr: KExpr<T>, dependency: KExpr<A>, transformer: (KExpr<A>) -> KExpr<T>): KExpr<T>

Specialized version of transformExprAfterTransformed for expression with single argument.

inline fun <T : KSort, A : KSort> transformExprAfterTransformed(expr: KExpr<T>, dependencies: List<KExpr<A>>, transformer: (List<KExpr<A>>) -> KExpr<T>): KExpr<T>

Transform expr only if all it sub-expressions dependencies were already transformed. Otherwise, register expr for transformation after dependencies and keep expr unchanged.

inline fun <T : KSort, A0 : KSort, A1 : KSort> transformExprAfterTransformed(expr: KExpr<T>, dependency0: KExpr<A0>, dependency1: KExpr<A1>, transformer: (KExpr<A0>, KExpr<A1>) -> KExpr<T>): KExpr<T>

Specialized version of transformExprAfterTransformed for expression with two arguments.

inline fun <T : KSort, A0 : KSort, A1 : KSort, A2 : KSort> transformExprAfterTransformed(expr: KExpr<T>, dependency0: KExpr<A0>, dependency1: KExpr<A1>, dependency2: KExpr<A2>, transformer: (KExpr<A0>, KExpr<A1>, KExpr<A2>) -> KExpr<T>): KExpr<T>

Specialized version of transformExprAfterTransformed for expression with three arguments.

inline fun <T : KSort, A0 : KSort, A1 : KSort, A2 : KSort, A3 : KSort> transformExprAfterTransformed(expr: KExpr<T>, dependency0: KExpr<A0>, dependency1: KExpr<A1>, dependency2: KExpr<A2>, dependency3: KExpr<A3>, transformer: (KExpr<A0>, KExpr<A1>, KExpr<A2>, KExpr<A3>) -> KExpr<T>): KExpr<T>

Specialized version of transformExprAfterTransformed for expression with four arguments.

inline fun <T : KSort, A0 : KSort, A1 : KSort, A2 : KSort, A3 : KSort, A4 : KSort> transformExprAfterTransformed(expr: KExpr<T>, dependency0: KExpr<A0>, dependency1: KExpr<A1>, dependency2: KExpr<A2>, dependency3: KExpr<A3>, dependency4: KExpr<A4>, transformer: (KExpr<A0>, KExpr<A1>, KExpr<A2>, KExpr<A3>, KExpr<A4>) -> KExpr<T>): KExpr<T>

Specialized version of transformExprAfterTransformed for expression with five arguments.

Link copied to clipboard
fun transformExprDependencyIfNeeded(dependency: KExpr<*>, transformedDependency: KExpr<*>?)
Link copied to clipboard
open fun <T : KFpSort> transformFpValue(expr: KFpValue<T>): KExpr<T>
Link copied to clipboard
Link copied to clipboard
open fun <T : KSort> transformValue(expr: KInterpretedValue<T>): KExpr<T>

Properties

Link copied to clipboard
abstract val ctx: KContext

Inheritors

Link copied to clipboard
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