ksmt-core/io.ksmt.expr.rewrite.simplify/KExprSimplifierBase

KExprSimplifierBase

interface KExprSimplifierBase : KTransformer

Functions

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

abstract fun <T : KSort> areDefinitelyDistinct(lhs: KExpr<T>, rhs: KExpr<T>): Boolean

Checks if the provided expressions can never be equal. For example, two unequal theory interpreted constants cannot be equal.

boundedRewrite

abstract fun <T : KSort> boundedRewrite(allowedDepth: Int, expr: KExpr<T>): KExpr<T>

Ask simplifier to rewrite an expression with bound check. Typically used for expressions which produce expressions of the same type during simplification process.

canPerformBoundedRewrite

abstract fun canPerformBoundedRewrite(): Boolean

Returns true if simplifier has enough depth to perform bounded rewrite.

rewrite

abstract fun <T : KSort> rewrite(expr: KExpr<T>): KExpr<T>

Force simplifier to rewrite an expression. Typically used for a new expression created by simplifying another expression.

transform

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>

transformApp

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>

transformExpr

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>

transformValue

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

Properties

ctx

abstract val ctx: KContext

Inheritors

Extensions

areDefinitelyDistinct

fun KExprSimplifierBase.areDefinitelyDistinct(left: List<KExpr<*>>, right: List<KExpr<*>>): Boolean

left and right are definitely distinct if there is at least one distinct pair of expressions.

internalizationLoop

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

simplifyExpr

inline fun <T : KSort, P : KExpr<T>, A : KSort> KExprSimplifierBase.simplifyExpr(expr: P, args: List<KExpr<A>>, preprocess: KContext.(P) -> KExpr<T> = { expr }, crossinline simplifier: KContext.(List<KExpr<A>>) -> KExpr<T>): KExpr<T>

Simplify an expression. preprocess Rewrite an expression before simplification of an args (top-down). simplifier Rewrite an expression after args simplification (bottom-up).

inline fun <T : KSort, P : KExpr<T>> KExprSimplifierBase.simplifyExpr(expr: P, preprocess: KContext.(P) -> KExpr<T>): KExpr<T>

Specialized version of simplifyExpr for expressions which are always rewritten with another expression on the preprocess stage.

inline fun <T : KSort, P : KExpr<T>, A0 : KSort> KExprSimplifierBase.simplifyExpr(expr: P, a0: KExpr<A0>, preprocess: KContext.(P) -> KExpr<T> = { expr }, crossinline simplifier: KContext.(KExpr<A0>) -> KExpr<T>): KExpr<T>

Specialized version of simplifyExpr for expressions with a single argument.

inline fun <T : KSort, P : KExpr<T>, A0 : KSort, A1 : KSort> KExprSimplifierBase.simplifyExpr(expr: P, a0: KExpr<A0>, a1: KExpr<A1>, preprocess: KContext.(P) -> KExpr<T> = { expr }, crossinline simplifier: KContext.(KExpr<A0>, KExpr<A1>) -> KExpr<T>): KExpr<T>

Specialized version of simplifyExpr for expressions with two arguments.

inline fun <T : KSort, P : KExpr<T>, A0 : KSort, A1 : KSort, A2 : KSort> KExprSimplifierBase.simplifyExpr(expr: P, a0: KExpr<A0>, a1: KExpr<A1>, a2: KExpr<A2>, preprocess: KContext.(P) -> KExpr<T> = { expr }, crossinline simplifier: KContext.(KExpr<A0>, KExpr<A1>, KExpr<A2>) -> KExpr<T>): KExpr<T>

Specialized version of simplifyExpr for expressions with three arguments.

inline fun <T : KSort, P : KExpr<T>, A0 : KSort, A1 : KSort, A2 : KSort, A3 : KSort> KExprSimplifierBase.simplifyExpr(expr: P, a0: KExpr<A0>, a1: KExpr<A1>, a2: KExpr<A2>, a3: KExpr<A3>, preprocess: KContext.(P) -> KExpr<T> = { expr }, crossinline simplifier: KContext.(KExpr<A0>, KExpr<A1>, KExpr<A2>, KExpr<A3>) -> KExpr<T>): KExpr<T>

Specialized version of simplifyExpr for expressions with four arguments.

inline fun <T : KSort, P : KExpr<T>, A0 : KSort, A1 : KSort, A2 : KSort, A3 : KSort, A4 : KSort> KExprSimplifierBase.simplifyExpr(expr: P, a0: KExpr<A0>, a1: KExpr<A1>, a2: KExpr<A2>, a3: KExpr<A3>, a4: KExpr<A4>, preprocess: KContext.(P) -> KExpr<T> = { expr }, crossinline simplifier: KContext.(KExpr<A0>, KExpr<A1>, KExpr<A2>, KExpr<A3>, KExpr<A4>) -> KExpr<T>): KExpr<T>

Specialized version of simplifyExpr for expressions with five arguments.

simplifyExprBase

inline fun <T : KSort> KExprSimplifierBase.simplifyExprBase(expr: KExpr<T>, preprocess: KExprSimplifier.() -> KExpr<T>, simplify: KExprSimplifier.() -> KExpr<T>): KExpr<T>

Simplify an expression.