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

KFpExprSimplifier

interface KFpExprSimplifier : KExprSimplifierBase

Functions

Link copied to clipboard
open fun <T : KSort> apply(expr: KExpr<T>): KExpr<T>
Link copied to clipboard
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.

Link copied to clipboard
open fun <T : KFpSort> areDefinitelyDistinctFp(lhs: KExpr<T>, rhs: KExpr<T>): Boolean
Link copied to clipboard
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.

Link copied to clipboard
abstract fun canPerformBoundedRewrite(): Boolean

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

Link copied to clipboard
open fun <T : KFpSort> KContext.postRewriteBvToFpExpr(sort: T, roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<KBvSort>, signed: Boolean): KExpr<T>
Link copied to clipboard
open fun <T : KFpSort> KContext.postRewriteFpAbsExpr(value: KExpr<T>): KExpr<T>
Link copied to clipboard
open fun <T : KFpSort> KContext.postRewriteFpAddExpr(roundingMode: KExpr<KFpRoundingModeSort>, lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>
Link copied to clipboard
open fun <T : KFpSort> KContext.postRewriteFpDivExpr(roundingMode: KExpr<KFpRoundingModeSort>, lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>
Link copied to clipboard
Link copied to clipboard
open fun <T : KFpSort> KContext.postRewriteFpFromBvExpr(sign: KExpr<KBv1Sort>, biasedExponent: KExpr<out KBvSort>, significand: KExpr<out KBvSort>): KExpr<T>
Link copied to clipboard
open fun <T : KFpSort> KContext.postRewriteFpFusedMulAddExpr(roundingMode: KExpr<KFpRoundingModeSort>, arg0: KExpr<T>, arg1: KExpr<T>, arg2: KExpr<T>): KExpr<T>
Link copied to clipboard
Link copied to clipboard
Link copied to clipboard
Link copied to clipboard
Link copied to clipboard
Link copied to clipboard
Link copied to clipboard
Link copied to clipboard
Link copied to clipboard
Link copied to clipboard
Link copied to clipboard
Link copied to clipboard
open fun <T : KFpSort> KContext.postRewriteFpMaxExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>
Link copied to clipboard
open fun <T : KFpSort> KContext.postRewriteFpMinExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>
Link copied to clipboard
open fun <T : KFpSort> KContext.postRewriteFpMulExpr(roundingMode: KExpr<KFpRoundingModeSort>, lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>
Link copied to clipboard
Link copied to clipboard
open fun <T : KFpSort> KContext.postRewriteFpRemExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>
Link copied to clipboard
Link copied to clipboard
open fun <T : KFpSort> KContext.postRewriteFpSqrtExpr(roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<T>): KExpr<T>
Link copied to clipboard
open fun <T : KFpSort> KContext.postRewriteFpSubExpr(roundingMode: KExpr<KFpRoundingModeSort>, lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>
Link copied to clipboard
open fun <T : KFpSort> KContext.postRewriteFpToBvExpr(roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<T>, bvSize: Int, isSigned: Boolean): KExpr<KBvSort>
Link copied to clipboard
open fun <T : KFpSort> KContext.postRewriteFpToFpExpr(sort: T, roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<out KFpSort>): KExpr<T>
Link copied to clipboard
Link copied to clipboard
Link copied to clipboard
open fun <T : KFpSort> KContext.postRewriteRealToFpExpr(sort: T, roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<KRealSort>): KExpr<T>
Link copied to clipboard
open fun <T : KFpSort> KContext.preprocess(expr: KBvToFpExpr<T>): KExpr<T>
open fun <T : KFpSort> KContext.preprocess(expr: KFpAbsExpr<T>): KExpr<T>
open fun <T : KFpSort> KContext.preprocess(expr: KFpAddExpr<T>): KExpr<T>
open fun <T : KFpSort> KContext.preprocess(expr: KFpDivExpr<T>): KExpr<T>
open fun <T : KFpSort> KContext.preprocess(expr: KFpEqualExpr<T>): KExpr<KBoolSort>
open fun <T : KFpSort> KContext.preprocess(expr: KFpFromBvExpr<T>): KExpr<T>
open fun <T : KFpSort> KContext.preprocess(expr: KFpFusedMulAddExpr<T>): KExpr<T>
open fun <T : KFpSort> KContext.preprocess(expr: KFpGreaterExpr<T>): KExpr<KBoolSort>
open fun <T : KFpSort> KContext.preprocess(expr: KFpGreaterOrEqualExpr<T>): KExpr<KBoolSort>
open fun <T : KFpSort> KContext.preprocess(expr: KFpIsInfiniteExpr<T>): KExpr<KBoolSort>
open fun <T : KFpSort> KContext.preprocess(expr: KFpIsNaNExpr<T>): KExpr<KBoolSort>
open fun <T : KFpSort> KContext.preprocess(expr: KFpIsNegativeExpr<T>): KExpr<KBoolSort>
open fun <T : KFpSort> KContext.preprocess(expr: KFpIsNormalExpr<T>): KExpr<KBoolSort>
open fun <T : KFpSort> KContext.preprocess(expr: KFpIsPositiveExpr<T>): KExpr<KBoolSort>
open fun <T : KFpSort> KContext.preprocess(expr: KFpIsSubnormalExpr<T>): KExpr<KBoolSort>
open fun <T : KFpSort> KContext.preprocess(expr: KFpIsZeroExpr<T>): KExpr<KBoolSort>
open fun <T : KFpSort> KContext.preprocess(expr: KFpLessExpr<T>): KExpr<KBoolSort>
open fun <T : KFpSort> KContext.preprocess(expr: KFpLessOrEqualExpr<T>): KExpr<KBoolSort>
open fun <T : KFpSort> KContext.preprocess(expr: KFpMaxExpr<T>): KExpr<T>
open fun <T : KFpSort> KContext.preprocess(expr: KFpMinExpr<T>): KExpr<T>
open fun <T : KFpSort> KContext.preprocess(expr: KFpMulExpr<T>): KExpr<T>
open fun <T : KFpSort> KContext.preprocess(expr: KFpNegationExpr<T>): KExpr<T>
open fun <T : KFpSort> KContext.preprocess(expr: KFpRemExpr<T>): KExpr<T>
open fun <T : KFpSort> KContext.preprocess(expr: KFpRoundToIntegralExpr<T>): KExpr<T>
open fun <T : KFpSort> KContext.preprocess(expr: KFpSqrtExpr<T>): KExpr<T>
open fun <T : KFpSort> KContext.preprocess(expr: KFpSubExpr<T>): KExpr<T>
open fun <T : KFpSort> KContext.preprocess(expr: KFpToBvExpr<T>): KExpr<KBvSort>
open fun <T : KFpSort> KContext.preprocess(expr: KFpToFpExpr<T>): KExpr<T>
open fun <T : KFpSort> KContext.preprocess(expr: KFpToIEEEBvExpr<T>): KExpr<KBvSort>
open fun <T : KFpSort> KContext.preprocess(expr: KFpToRealExpr<T>): KExpr<KRealSort>
open fun <T : KFpSort> KContext.preprocess(expr: KRealToFpExpr<T>): KExpr<T>
Link copied to clipboard
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.

Link copied to clipboard
open fun <T : KFpSort> simplifyEqFp(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

Simplify an expression of the form (= a b). For the simplification of (fp.eq a b) see KFpEqualExpr.

Link copied to clipboard
open override fun <T : KFpSort> transform(expr: KBvToFpExpr<T>): KExpr<T>
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 : KFpSort> transform(expr: KRealToFpExpr<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 : 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 transform(expr: KFpCustomSizeValue): KExpr<KFpSort>
open override fun transform(expr: KFpRoundingModeExpr): KExpr<KFpRoundingModeSort>
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 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>
Link copied to clipboard
open fun <T : KSort, A : KSort> transformApp(expr: KApp<T, A>): KExpr<T>
Link copied to clipboard
Link copied to clipboard
Link copied to clipboard
Link copied to clipboard
Link copied to clipboard
open fun <T : KSort> transformExpr(expr: KExpr<T>): KExpr<T>
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

Extensions

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

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

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

Simplify an expression.