ksmt-core/io.ksmt.expr.rewrite/KExprSubstitutor

KExprSubstitutor

open class KExprSubstitutor(val ctx: KContext) : KNonRecursiveTransformer

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
fun <T : KSort> substitute(from: KDecl<T>, to: KDecl<T>)

Substitute every occurrence of declaration from in expression expr with to.

fun <T : KSort> substitute(from: KExpr<T>, to: KExpr<T>)

Substitute every occurrence of from in expression expr with to.

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

open 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.

open 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.

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

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

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

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

open override fun <A : KArraySortBase<R>, R : KSort> transform(expr: KFunctionAsArray<A, R>): KExpr<A>
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: 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 <T : KFpSort> transform(expr: KFpAbsExpr<T>): KExpr<T>
open override fun <T : KFpSort> transform(expr: KFpAddExpr<T>): KExpr<T>
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 <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 <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: 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 <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 <T : KArithSort> transform(expr: KUnaryMinusArithExpr<T>): KExpr<T>
open override fun transform(expr: KXorExpr): KExpr<KBoolSort>
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: 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 transform(expr: KFpCustomSizeValue): KExpr<KFpSort>
open override fun transform(expr: KFpRoundingModeExpr): KExpr<KFpRoundingModeSort>
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: KRealNumExpr): KExpr<KRealSort>
open override fun transform(expr: KTrue): KExpr<KBoolSort>
open override fun transform(expr: KUninterpretedSortValue): KExpr<KUninterpretedSort>

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

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

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
open 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 override 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
inline fun <In : KExpr<T>, Out : KExpr<T>, T : KSort, A : KSort> transformExprAfterTransformedDefault(expr: In, dependency: KExpr<A>, ifNotTransformed: (In) -> KExpr<T>, transformer: KContext.(KExpr<A>) -> Out): KExpr<T>

Specialized version of transformExprAfterTransformedDefault for expression with single argument.

inline fun <In : KExpr<T>, Out : KExpr<T>, T : KSort, A : KSort> transformExprAfterTransformedDefault(expr: In, dependencies: List<KExpr<A>>, ifNotTransformed: (In) -> KExpr<T>, transformer: KContext.(List<KExpr<A>>) -> Out): KExpr<T>

Transform expressions dependencies before expression transformation. If all dependencies remain unchanged after transformation invoke ifNotTransformed on the original expression and return it result. Otherwise, apply transformer to the modified dependencies.

inline fun <In : KExpr<T>, Out : KExpr<T>, T : KSort, A0 : KSort, A1 : KSort> transformExprAfterTransformedDefault(expr: In, dependency0: KExpr<A0>, dependency1: KExpr<A1>, ifNotTransformed: (In) -> KExpr<T>, transformer: KContext.(KExpr<A0>, KExpr<A1>) -> Out): KExpr<T>

Specialized version of transformExprAfterTransformedDefault for expression with two arguments.

inline fun <In : KExpr<T>, Out : KExpr<T>, T : KSort, A0 : KSort, A1 : KSort, A2 : KSort> transformExprAfterTransformedDefault(expr: In, dependency0: KExpr<A0>, dependency1: KExpr<A1>, dependency2: KExpr<A2>, ifNotTransformed: (In) -> KExpr<T>, transformer: KContext.(KExpr<A0>, KExpr<A1>, KExpr<A2>) -> Out): KExpr<T>

Specialized version of transformExprAfterTransformedDefault for expression with three arguments.

inline fun <In : KExpr<T>, Out : KExpr<T>, T : KSort, A0 : KSort, A1 : KSort, A2 : KSort, A3 : KSort> transformExprAfterTransformedDefault(expr: In, dependency0: KExpr<A0>, dependency1: KExpr<A1>, dependency2: KExpr<A2>, dependency3: KExpr<A3>, ifNotTransformed: (In) -> KExpr<T>, transformer: KContext.(KExpr<A0>, KExpr<A1>, KExpr<A2>, KExpr<A3>) -> Out): KExpr<T>

Specialized version of transformExprAfterTransformedDefault for expression with four arguments.

inline fun <In : KExpr<T>, Out : KExpr<T>, T : KSort, A0 : KSort, A1 : KSort, A2 : KSort, A3 : KSort, A4 : KSort> transformExprAfterTransformedDefault(expr: In, d0: KExpr<A0>, d1: KExpr<A1>, d2: KExpr<A2>, d3: KExpr<A3>, d4: KExpr<A4>, ifNotTransformed: (In) -> KExpr<T>, transformer: KContext.(KExpr<A0>, KExpr<A1>, KExpr<A2>, KExpr<A3>, KExpr<A4>) -> Out): KExpr<T>

Specialized version of transformExprAfterTransformedDefault for expression with five arguments.

Link copied to clipboard
fun <T : KSort> transformExprDefault(expr: KExpr<T>): KExpr<T>
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
open override val ctx: KContext

Extensions

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