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

KExprSimplifier

open class KExprSimplifier(val ctx: KContext) : KNonRecursiveTransformerBase, KExprSimplifierBase, KBoolExprSimplifier, KArithExprSimplifier, KBvExprSimplifier, KFpExprSimplifier, KArrayExprSimplifier

Constructors

KExprSimplifier

fun KExprSimplifier(ctx: KContext)

Types

Companion

object Companion

Functions

apply

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

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

areDefinitelyDistinct

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

areDefinitelyDistinctBool

open fun areDefinitelyDistinctBool(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>): Boolean

areDefinitelyDistinctBv

open fun <T : KBvSort> areDefinitelyDistinctBv(lhs: KExpr<T>, rhs: KExpr<T>): Boolean

areDefinitelyDistinctFp

open fun <T : KFpSort> areDefinitelyDistinctFp(lhs: KExpr<T>, rhs: KExpr<T>): Boolean

areDefinitelyDistinctInt

open fun areDefinitelyDistinctInt(lhs: KExpr<KIntSort>, rhs: KExpr<KIntSort>): Boolean

areDefinitelyDistinctReal

open fun areDefinitelyDistinctReal(lhs: KExpr<KRealSort>, rhs: KExpr<KRealSort>): Boolean

areDefinitelyDistinctUninterpreted

open fun areDefinitelyDistinctUninterpreted(lhs: KExpr<KUninterpretedSort>, rhs: KExpr<KUninterpretedSort>): Boolean

boundedRewrite

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

open override fun canPerformBoundedRewrite(): Boolean

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

disablePostRewrite

fun disablePostRewrite()

enablePostRewrite

fun enablePostRewrite()

eraseTransformationResult

fun eraseTransformationResult(expr: KExpr<*>)

Erase expr transformation result. Useful for transformer auxiliary expressions.

exprTransformationRequired

open override fun <T : KSort> exprTransformationRequired(expr: KExpr<T>): Boolean

Allows to skip expression transformation and stop deepening.

markExpressionAsNotTransformed

fun markExpressionAsNotTransformed()

Inform KNonRecursiveTransformer that transformation was not applied to expression

postRewrite

fun postRewrite(original: KExpr<*>, rewritten: KExpr<*>)

postRewriteAnd

open fun KContext.postRewriteAnd(args: List<KExpr<KBoolSort>>): KExpr<KBoolSort>

postRewriteArithAdd

open fun <T : KArithSort> KContext.postRewriteArithAdd(args: List<KExpr<T>>): KExpr<T>

postRewriteArithDiv

open fun <T : KArithSort> KContext.postRewriteArithDiv(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

postRewriteArithGe

open fun <T : KArithSort> KContext.postRewriteArithGe(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

postRewriteArithGt

open fun <T : KArithSort> KContext.postRewriteArithGt(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

postRewriteArithLe

open fun <T : KArithSort> KContext.postRewriteArithLe(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

postRewriteArithLt

open fun <T : KArithSort> KContext.postRewriteArithLt(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

postRewriteArithMul

open fun <T : KArithSort> KContext.postRewriteArithMul(args: List<KExpr<T>>): KExpr<T>

postRewriteArithPower

open fun <T : KArithSort> KContext.postRewriteArithPower(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

postRewriteArithSub

open fun <T : KArithSort> KContext.postRewriteArithSub(args: List<KExpr<T>>): KExpr<T>

postRewriteArithUnaryMinus

open fun <T : KArithSort> KContext.postRewriteArithUnaryMinus(arg: KExpr<T>): KExpr<T>

postRewriteArrayLambda

fun <D : KSort, R : KSort> KContext.postRewriteArrayLambda(bound: KDecl<D>, simplifiedBody: KExpr<R>): KExpr<KArraySort<D, R>>

fun <R : KSort> KContext.postRewriteArrayLambda(bounds: List<KDecl<*>>, simplifiedBody: KExpr<R>): KExpr<KArrayNSort<R>>

fun <D0 : KSort, D1 : KSort, R : KSort> KContext.postRewriteArrayLambda(bound0: KDecl<D0>, bound1: KDecl<D1>, simplifiedBody: KExpr<R>): KExpr<KArray2Sort<D0, D1, R>>

fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> KContext.postRewriteArrayLambda(bound0: KDecl<D0>, bound1: KDecl<D1>, bound2: KDecl<D2>, simplifiedBody: KExpr<R>): KExpr<KArray3Sort<D0, D1, D2, R>>

postRewriteArrayNSelect

open fun <R : KSort> KContext.postRewriteArrayNSelect(array: KExpr<KArrayNSort<R>>, indices: List<KExpr<KSort>>): KExpr<R>

postRewriteArrayNStore

open fun <R : KSort> KContext.postRewriteArrayNStore(array: KExpr<KArrayNSort<R>>, indices: List<KExpr<KSort>>, value: KExpr<R>): KExpr<KArrayNSort<R>>

postRewriteArraySelect

open fun <D : KSort, R : KSort> KContext.postRewriteArraySelect(array: KExpr<KArraySort<D, R>>, index: KExpr<D>): KExpr<R>

open fun <D0 : KSort, D1 : KSort, R : KSort> KContext.postRewriteArraySelect(array: KExpr<KArray2Sort<D0, D1, R>>, index0: KExpr<D0>, index1: KExpr<D1>): KExpr<R>

open fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> KContext.postRewriteArraySelect(array: KExpr<KArray3Sort<D0, D1, D2, R>>, index0: KExpr<D0>, index1: KExpr<D1>, index2: KExpr<D2>): KExpr<R>

postRewriteArrayStore

open fun <D : KSort, R : KSort> KContext.postRewriteArrayStore(array: KExpr<KArraySort<D, R>>, index: KExpr<D>, value: KExpr<R>): KExpr<KArraySort<D, R>>

open fun <D0 : KSort, D1 : KSort, R : KSort> KContext.postRewriteArrayStore(array: KExpr<KArray2Sort<D0, D1, R>>, index0: KExpr<D0>, index1: KExpr<D1>, value: KExpr<R>): KExpr<KArray2Sort<D0, D1, R>>

open fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> KContext.postRewriteArrayStore(array: KExpr<KArray3Sort<D0, D1, D2, R>>, index0: KExpr<D0>, index1: KExpr<D1>, index2: KExpr<D2>, value: KExpr<R>): KExpr<KArray3Sort<D0, D1, D2, R>>

postRewriteBv2IntExpr

open fun <T : KBvSort> KContext.postRewriteBv2IntExpr(value: KExpr<T>, isSigned: Boolean): KExpr<KIntSort>

postRewriteBvAddExpr

open fun <T : KBvSort> KContext.postRewriteBvAddExpr(args: List<KExpr<T>>): KExpr<T>

postRewriteBvAddNoOverflowExpr

open fun <T : KBvSort> KContext.postRewriteBvAddNoOverflowExpr(lhs: KExpr<T>, rhs: KExpr<T>, isSigned: Boolean): KExpr<KBoolSort>

postRewriteBvAddNoUnderflowExpr

open fun <T : KBvSort> KContext.postRewriteBvAddNoUnderflowExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

postRewriteBvAndExpr

open fun <T : KBvSort> KContext.postRewriteBvAndExpr(args: List<KExpr<T>>): KExpr<T>

postRewriteBvArithShiftRightExpr

open fun <T : KBvSort> KContext.postRewriteBvArithShiftRightExpr(arg: KExpr<T>, shift: KExpr<T>): KExpr<T>

postRewriteBvConcatExpr

open fun KContext.postRewriteBvConcatExpr(args: List<KExpr<KBvSort>>): KExpr<KBvSort>

postRewriteBvDivNoOverflowExpr

open fun <T : KBvSort> KContext.postRewriteBvDivNoOverflowExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

postRewriteBvExtractExpr

open fun KContext.postRewriteBvExtractExpr(high: Int, low: Int, value: KExpr<KBvSort>): KExpr<KBvSort>

postRewriteBvLogicalShiftRightExpr

open fun <T : KBvSort> KContext.postRewriteBvLogicalShiftRightExpr(arg: KExpr<T>, shift: KExpr<T>): KExpr<T>

postRewriteBvMulExpr

open fun <T : KBvSort> KContext.postRewriteBvMulExpr(args: List<KExpr<T>>): KExpr<T>

postRewriteBvMulNoOverflowExpr

open fun <T : KBvSort> KContext.postRewriteBvMulNoOverflowExpr(lhs: KExpr<T>, rhs: KExpr<T>, isSigned: Boolean): KExpr<KBoolSort>

postRewriteBvMulNoUnderflowExpr

open fun <T : KBvSort> KContext.postRewriteBvMulNoUnderflowExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

postRewriteBvNAndExpr

open fun <T : KBvSort> KContext.postRewriteBvNAndExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

postRewriteBvNegationExpr

open fun <T : KBvSort> KContext.postRewriteBvNegationExpr(arg: KExpr<T>): KExpr<T>

postRewriteBvNegNoOverflowExpr

open fun <T : KBvSort> KContext.postRewriteBvNegNoOverflowExpr(arg: KExpr<T>): KExpr<KBoolSort>

postRewriteBvNorExpr

open fun <T : KBvSort> KContext.postRewriteBvNorExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

postRewriteBvNotExpr

open fun <T : KBvSort> KContext.postRewriteBvNotExpr(arg: KExpr<T>): KExpr<T>

postRewriteBvOrExpr

open fun <T : KBvSort> KContext.postRewriteBvOrExpr(args: List<KExpr<T>>): KExpr<T>

postRewriteBvReductionAndExpr

open fun <T : KBvSort> KContext.postRewriteBvReductionAndExpr(arg: KExpr<T>): KExpr<KBv1Sort>

postRewriteBvReductionOrExpr

open fun <T : KBvSort> KContext.postRewriteBvReductionOrExpr(arg: KExpr<T>): KExpr<KBv1Sort>

postRewriteBvRepeatExpr

open fun <T : KBvSort> KContext.postRewriteBvRepeatExpr(repeatNumber: Int, arg: KExpr<T>): KExpr<KBvSort>

postRewriteBvRotateLeftExpr

open fun <T : KBvSort> KContext.postRewriteBvRotateLeftExpr(value: KExpr<T>, rotation: KExpr<T>): KExpr<T>

postRewriteBvRotateLeftIndexedExpr

open fun <T : KBvSort> KContext.postRewriteBvRotateLeftIndexedExpr(rotation: Int, value: KExpr<T>): KExpr<T>

postRewriteBvRotateRightExpr

open fun <T : KBvSort> KContext.postRewriteBvRotateRightExpr(value: KExpr<T>, rotation: KExpr<T>): KExpr<T>

postRewriteBvRotateRightIndexedExpr

open fun <T : KBvSort> KContext.postRewriteBvRotateRightIndexedExpr(rotation: Int, value: KExpr<T>): KExpr<T>

postRewriteBvShiftLeftExpr

open fun <T : KBvSort> KContext.postRewriteBvShiftLeftExpr(arg: KExpr<T>, shift: KExpr<T>): KExpr<T>

postRewriteBvSignedDivExpr

open fun <T : KBvSort> KContext.postRewriteBvSignedDivExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

postRewriteBvSignedGreaterExpr

open fun <T : KBvSort> KContext.postRewriteBvSignedGreaterExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

postRewriteBvSignedGreaterOrEqualExpr

open fun <T : KBvSort> KContext.postRewriteBvSignedGreaterOrEqualExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

postRewriteBvSignedLessExpr

open fun <T : KBvSort> KContext.postRewriteBvSignedLessExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

postRewriteBvSignedLessOrEqualExpr

open fun <T : KBvSort> KContext.postRewriteBvSignedLessOrEqualExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

postRewriteBvSignedModExpr

open fun <T : KBvSort> KContext.postRewriteBvSignedModExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

postRewriteBvSignedRemExpr

open fun <T : KBvSort> KContext.postRewriteBvSignedRemExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

postRewriteBvSignExtensionExpr

open fun <T : KBvSort> KContext.postRewriteBvSignExtensionExpr(extensionSize: Int, value: KExpr<T>): KExpr<KBvSort>

postRewriteBvSubExpr

open fun <T : KBvSort> KContext.postRewriteBvSubExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

postRewriteBvSubNoOverflowExpr

open fun <T : KBvSort> KContext.postRewriteBvSubNoOverflowExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

postRewriteBvSubNoUnderflowExpr

open fun <T : KBvSort> KContext.postRewriteBvSubNoUnderflowExpr(lhs: KExpr<T>, rhs: KExpr<T>, isSigned: Boolean): KExpr<KBoolSort>

postRewriteBvToFpExpr

open fun <T : KFpSort> KContext.postRewriteBvToFpExpr(sort: T, roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<KBvSort>, signed: Boolean): KExpr<T>

postRewriteBvUnsignedDivExpr

open fun <T : KBvSort> KContext.postRewriteBvUnsignedDivExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

postRewriteBvUnsignedGreaterExpr

open fun <T : KBvSort> KContext.postRewriteBvUnsignedGreaterExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

postRewriteBvUnsignedGreaterOrEqualExpr

open fun <T : KBvSort> KContext.postRewriteBvUnsignedGreaterOrEqualExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

postRewriteBvUnsignedLessExpr

open fun <T : KBvSort> KContext.postRewriteBvUnsignedLessExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

postRewriteBvUnsignedLessOrEqualExpr

open fun <T : KBvSort> KContext.postRewriteBvUnsignedLessOrEqualExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

postRewriteBvUnsignedRemExpr

open fun <T : KBvSort> KContext.postRewriteBvUnsignedRemExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

postRewriteBvXNorExpr

open fun <T : KBvSort> KContext.postRewriteBvXNorExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

postRewriteBvXorExpr

open fun <T : KBvSort> KContext.postRewriteBvXorExpr(args: List<KExpr<T>>): KExpr<T>

postRewriteBvZeroExtensionExpr

open fun <T : KBvSort> KContext.postRewriteBvZeroExtensionExpr(extensionSize: Int, value: KExpr<T>): KExpr<KBvSort>

postRewriteDistinct

fun <T : KSort> KContext.postRewriteDistinct(args: List<KExpr<T>>): KExpr<KBoolSort>

postRewriteEnabled

fun postRewriteEnabled(): Boolean

postRewriteEq

fun <T : KSort> KContext.postRewriteEq(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

postRewriteExistentialQuantifier

fun KContext.postRewriteExistentialQuantifier(bounds: List<KDecl<*>>, simplifiedBody: KExpr<KBoolSort>): KExpr<KBoolSort>

postRewriteFpAbsExpr

open fun <T : KFpSort> KContext.postRewriteFpAbsExpr(value: KExpr<T>): KExpr<T>

postRewriteFpAddExpr

open fun <T : KFpSort> KContext.postRewriteFpAddExpr(roundingMode: KExpr<KFpRoundingModeSort>, lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

postRewriteFpDivExpr

open fun <T : KFpSort> KContext.postRewriteFpDivExpr(roundingMode: KExpr<KFpRoundingModeSort>, lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

postRewriteFpEqualExpr

open fun <T : KFpSort> KContext.postRewriteFpEqualExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

postRewriteFpFromBvExpr

open fun <T : KFpSort> KContext.postRewriteFpFromBvExpr(sign: KExpr<KBv1Sort>, biasedExponent: KExpr<out KBvSort>, significand: KExpr<out KBvSort>): KExpr<T>

postRewriteFpFusedMulAddExpr

open fun <T : KFpSort> KContext.postRewriteFpFusedMulAddExpr(roundingMode: KExpr<KFpRoundingModeSort>, arg0: KExpr<T>, arg1: KExpr<T>, arg2: KExpr<T>): KExpr<T>

postRewriteFpGreaterExpr

open fun <T : KFpSort> KContext.postRewriteFpGreaterExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

postRewriteFpGreaterOrEqualExpr

open fun <T : KFpSort> KContext.postRewriteFpGreaterOrEqualExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

postRewriteFpIsInfiniteExpr

open fun <T : KFpSort> KContext.postRewriteFpIsInfiniteExpr(arg: KExpr<T>): KExpr<KBoolSort>

postRewriteFpIsNaNExpr

open fun <T : KFpSort> KContext.postRewriteFpIsNaNExpr(arg: KExpr<T>): KExpr<KBoolSort>

postRewriteFpIsNegativeExpr

open fun <T : KFpSort> KContext.postRewriteFpIsNegativeExpr(arg: KExpr<T>): KExpr<KBoolSort>

postRewriteFpIsNormalExpr

open fun <T : KFpSort> KContext.postRewriteFpIsNormalExpr(arg: KExpr<T>): KExpr<KBoolSort>

postRewriteFpIsPositiveExpr

open fun <T : KFpSort> KContext.postRewriteFpIsPositiveExpr(arg: KExpr<T>): KExpr<KBoolSort>

postRewriteFpIsSubnormalExpr

open fun <T : KFpSort> KContext.postRewriteFpIsSubnormalExpr(arg: KExpr<T>): KExpr<KBoolSort>

postRewriteFpIsZeroExpr

open fun <T : KFpSort> KContext.postRewriteFpIsZeroExpr(arg: KExpr<T>): KExpr<KBoolSort>

postRewriteFpLessExpr

open fun <T : KFpSort> KContext.postRewriteFpLessExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

postRewriteFpLessOrEqualExpr

open fun <T : KFpSort> KContext.postRewriteFpLessOrEqualExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

postRewriteFpMaxExpr

open fun <T : KFpSort> KContext.postRewriteFpMaxExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

postRewriteFpMinExpr

open fun <T : KFpSort> KContext.postRewriteFpMinExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

postRewriteFpMulExpr

open fun <T : KFpSort> KContext.postRewriteFpMulExpr(roundingMode: KExpr<KFpRoundingModeSort>, lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

postRewriteFpNegationExpr

open fun <T : KFpSort> KContext.postRewriteFpNegationExpr(value: KExpr<T>): KExpr<T>

postRewriteFpRemExpr

open fun <T : KFpSort> KContext.postRewriteFpRemExpr(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

postRewriteFpRoundToIntegralExpr

open fun <T : KFpSort> KContext.postRewriteFpRoundToIntegralExpr(roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<T>): KExpr<T>

postRewriteFpSqrtExpr

open fun <T : KFpSort> KContext.postRewriteFpSqrtExpr(roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<T>): KExpr<T>

postRewriteFpSubExpr

open fun <T : KFpSort> KContext.postRewriteFpSubExpr(roundingMode: KExpr<KFpRoundingModeSort>, lhs: KExpr<T>, rhs: KExpr<T>): KExpr<T>

postRewriteFpToBvExpr

open fun <T : KFpSort> KContext.postRewriteFpToBvExpr(roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<T>, bvSize: Int, isSigned: Boolean): KExpr<KBvSort>

postRewriteFpToFpExpr

open fun <T : KFpSort> KContext.postRewriteFpToFpExpr(sort: T, roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<out KFpSort>): KExpr<T>

postRewriteFpToIEEEBvExpr

open fun <T : KFpSort> KContext.postRewriteFpToIEEEBvExpr(arg: KExpr<T>): KExpr<KBvSort>

postRewriteFpToRealExpr

open fun <T : KFpSort> KContext.postRewriteFpToRealExpr(arg: KExpr<T>): KExpr<KRealSort>

postRewriteImplies

open fun KContext.postRewriteImplies(p: KExpr<KBoolSort>, q: KExpr<KBoolSort>): KExpr<KBoolSort>

postRewriteIntMod

open fun KContext.postRewriteIntMod(lhs: KExpr<KIntSort>, rhs: KExpr<KIntSort>): KExpr<KIntSort>

postRewriteIntRem

open fun KContext.postRewriteIntRem(lhs: KExpr<KIntSort>, rhs: KExpr<KIntSort>): KExpr<KIntSort>

postRewriteIntToReal

open fun KContext.postRewriteIntToReal(arg: KExpr<KIntSort>): KExpr<KRealSort>

postRewriteIte

open fun <T : KSort> KContext.postRewriteIte(condition: KExpr<KBoolSort>, trueBranch: KExpr<T>, falseBranch: KExpr<T>): KExpr<T>

postRewriteNot

open fun KContext.postRewriteNot(arg: KExpr<KBoolSort>): KExpr<KBoolSort>

postRewriteOr

open fun KContext.postRewriteOr(args: List<KExpr<KBoolSort>>): KExpr<KBoolSort>

postRewriteRealIsInt

open fun KContext.postRewriteRealIsInt(arg: KExpr<KRealSort>): KExpr<KBoolSort>

postRewriteRealToFpExpr

open fun <T : KFpSort> KContext.postRewriteRealToFpExpr(sort: T, roundingMode: KExpr<KFpRoundingModeSort>, value: KExpr<KRealSort>): KExpr<T>

postRewriteRealToInt

open fun KContext.postRewriteRealToInt(arg: KExpr<KRealSort>): KExpr<KIntSort>

postRewriteUniversalQuantifier

fun KContext.postRewriteUniversalQuantifier(bounds: List<KDecl<*>>, simplifiedBody: KExpr<KBoolSort>): KExpr<KBoolSort>

postRewriteXor

open fun KContext.postRewriteXor(a: KExpr<KBoolSort>, b: KExpr<KBoolSort>): KExpr<KBoolSort>

preprocess

open fun <T : KArithSort> KContext.preprocess(expr: KAddArithExpr<T>): KExpr<T>

open fun <T : KArithSort> KContext.preprocess(expr: KDivArithExpr<T>): KExpr<T>

open fun <T : KArithSort> KContext.preprocess(expr: KGeArithExpr<T>): KExpr<KBoolSort>

open fun <T : KArithSort> KContext.preprocess(expr: KGtArithExpr<T>): KExpr<KBoolSort>

open fun KContext.preprocess(expr: KIsIntRealExpr): KExpr<KBoolSort>

open fun <T : KArithSort> KContext.preprocess(expr: KLeArithExpr<T>): KExpr<KBoolSort>

open fun <T : KArithSort> KContext.preprocess(expr: KLtArithExpr<T>): KExpr<KBoolSort>

open fun KContext.preprocess(expr: KModIntExpr): KExpr<KIntSort>

open fun <T : KArithSort> KContext.preprocess(expr: KMulArithExpr<T>): KExpr<T>

open fun <T : KArithSort> KContext.preprocess(expr: KPowerArithExpr<T>): KExpr<T>

open fun KContext.preprocess(expr: KRemIntExpr): KExpr<KIntSort>

open fun <T : KArithSort> KContext.preprocess(expr: KSubArithExpr<T>): KExpr<T>

open fun KContext.preprocess(expr: KToIntRealExpr): KExpr<KIntSort>

open fun KContext.preprocess(expr: KToRealIntExpr): KExpr<KRealSort>

open fun <T : KArithSort> KContext.preprocess(expr: KUnaryMinusArithExpr<T>): KExpr<T>

open fun <D0 : KSort, D1 : KSort, R : KSort> KContext.preprocess(expr: KArray2Select<D0, D1, R>): KExpr<R>

open fun <D0 : KSort, D1 : KSort, R : KSort> KContext.preprocess(expr: KArray2Store<D0, D1, R>): KExpr<KArray2Sort<D0, D1, R>>

open fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> KContext.preprocess(expr: KArray3Select<D0, D1, D2, R>): KExpr<R>

open fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> KContext.preprocess(expr: KArray3Store<D0, D1, D2, R>): KExpr<KArray3Sort<D0, D1, D2, R>>

open fun <R : KSort> KContext.preprocess(expr: KArrayNSelect<R>): KExpr<R>

open fun <R : KSort> KContext.preprocess(expr: KArrayNStore<R>): KExpr<KArrayNSort<R>>

open fun <D : KSort, R : KSort> KContext.preprocess(expr: KArraySelect<D, R>): KExpr<R>

open fun <D : KSort, R : KSort> KContext.preprocess(expr: KArrayStore<D, R>): KExpr<KArraySort<D, R>>

open fun KContext.preprocess(expr: KAndExpr): KExpr<KBoolSort>

open fun KContext.preprocess(expr: KImpliesExpr): KExpr<KBoolSort>

open fun <T : KSort> KContext.preprocess(expr: KIteExpr<T>): KExpr<T>

open fun KContext.preprocess(expr: KNotExpr): KExpr<KBoolSort>

open fun KContext.preprocess(expr: KOrExpr): KExpr<KBoolSort>

open fun KContext.preprocess(expr: KXorExpr): KExpr<KBoolSort>

open fun KContext.preprocess(expr: KBv2IntExpr): KExpr<KIntSort>

open fun <T : KBvSort> KContext.preprocess(expr: KBvAddExpr<T>): KExpr<T>

open fun <T : KBvSort> KContext.preprocess(expr: KBvAddNoOverflowExpr<T>): KExpr<KBoolSort>

open fun <T : KBvSort> KContext.preprocess(expr: KBvAddNoUnderflowExpr<T>): KExpr<KBoolSort>

open fun <T : KBvSort> KContext.preprocess(expr: KBvAndExpr<T>): KExpr<T>

open fun <T : KBvSort> KContext.preprocess(expr: KBvArithShiftRightExpr<T>): KExpr<T>

open fun KContext.preprocess(expr: KBvConcatExpr): KExpr<KBvSort>

open fun <T : KBvSort> KContext.preprocess(expr: KBvDivNoOverflowExpr<T>): KExpr<KBoolSort>

open fun KContext.preprocess(expr: KBvExtractExpr): KExpr<KBvSort>

open fun <T : KBvSort> KContext.preprocess(expr: KBvLogicalShiftRightExpr<T>): KExpr<T>

open fun <T : KBvSort> KContext.preprocess(expr: KBvMulExpr<T>): KExpr<T>

open fun <T : KBvSort> KContext.preprocess(expr: KBvMulNoOverflowExpr<T>): KExpr<KBoolSort>

open fun <T : KBvSort> KContext.preprocess(expr: KBvMulNoUnderflowExpr<T>): KExpr<KBoolSort>

open fun <T : KBvSort> KContext.preprocess(expr: KBvNAndExpr<T>): KExpr<T>

open fun <T : KBvSort> KContext.preprocess(expr: KBvNegNoOverflowExpr<T>): KExpr<KBoolSort>

open fun <T : KBvSort> KContext.preprocess(expr: KBvNegationExpr<T>): KExpr<T>

open fun <T : KBvSort> KContext.preprocess(expr: KBvNorExpr<T>): KExpr<T>

open fun <T : KBvSort> KContext.preprocess(expr: KBvNotExpr<T>): KExpr<T>

open fun <T : KBvSort> KContext.preprocess(expr: KBvOrExpr<T>): KExpr<T>

open fun <T : KBvSort> KContext.preprocess(expr: KBvReductionAndExpr<T>): KExpr<KBv1Sort>

open fun <T : KBvSort> KContext.preprocess(expr: KBvReductionOrExpr<T>): KExpr<KBv1Sort>

open fun KContext.preprocess(expr: KBvRepeatExpr): KExpr<KBvSort>

open fun <T : KBvSort> KContext.preprocess(expr: KBvRotateLeftExpr<T>): KExpr<T>

open fun <T : KBvSort> KContext.preprocess(expr: KBvRotateLeftIndexedExpr<T>): KExpr<T>

open fun <T : KBvSort> KContext.preprocess(expr: KBvRotateRightExpr<T>): KExpr<T>

open fun <T : KBvSort> KContext.preprocess(expr: KBvRotateRightIndexedExpr<T>): KExpr<T>

open fun <T : KBvSort> KContext.preprocess(expr: KBvShiftLeftExpr<T>): KExpr<T>

open fun KContext.preprocess(expr: KBvSignExtensionExpr): KExpr<KBvSort>

open fun <T : KBvSort> KContext.preprocess(expr: KBvSignedDivExpr<T>): KExpr<T>

open fun <T : KBvSort> KContext.preprocess(expr: KBvSignedGreaterExpr<T>): KExpr<KBoolSort>

open fun <T : KBvSort> KContext.preprocess(expr: KBvSignedGreaterOrEqualExpr<T>): KExpr<KBoolSort>

open fun <T : KBvSort> KContext.preprocess(expr: KBvSignedLessExpr<T>): KExpr<KBoolSort>

open fun <T : KBvSort> KContext.preprocess(expr: KBvSignedLessOrEqualExpr<T>): KExpr<KBoolSort>

open fun <T : KBvSort> KContext.preprocess(expr: KBvSignedModExpr<T>): KExpr<T>

open fun <T : KBvSort> KContext.preprocess(expr: KBvSignedRemExpr<T>): KExpr<T>

open fun <T : KBvSort> KContext.preprocess(expr: KBvSubExpr<T>): KExpr<T>

open fun <T : KBvSort> KContext.preprocess(expr: KBvSubNoOverflowExpr<T>): KExpr<KBoolSort>

open fun <T : KBvSort> KContext.preprocess(expr: KBvSubNoUnderflowExpr<T>): KExpr<KBoolSort>

open fun <T : KBvSort> KContext.preprocess(expr: KBvUnsignedDivExpr<T>): KExpr<T>

open fun <T : KBvSort> KContext.preprocess(expr: KBvUnsignedGreaterExpr<T>): KExpr<KBoolSort>

open fun <T : KBvSort> KContext.preprocess(expr: KBvUnsignedGreaterOrEqualExpr<T>): KExpr<KBoolSort>

open fun <T : KBvSort> KContext.preprocess(expr: KBvUnsignedLessExpr<T>): KExpr<KBoolSort>

open fun <T : KBvSort> KContext.preprocess(expr: KBvUnsignedLessOrEqualExpr<T>): KExpr<KBoolSort>

open fun <T : KBvSort> KContext.preprocess(expr: KBvUnsignedRemExpr<T>): KExpr<T>

open fun <T : KBvSort> KContext.preprocess(expr: KBvXNorExpr<T>): KExpr<T>

open fun <T : KBvSort> KContext.preprocess(expr: KBvXorExpr<T>): KExpr<T>

open fun KContext.preprocess(expr: KBvZeroExtensionExpr): KExpr<KBvSort>

fun <D0 : KSort, D1 : KSort, R : KSort> KContext.preprocess(expr: KArray2Lambda<D0, D1, R>): KExpr<KArray2Sort<D0, D1, R>>

fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> KContext.preprocess(expr: KArray3Lambda<D0, D1, D2, R>): KExpr<KArray3Sort<D0, D1, D2, R>>

fun <D : KSort, R : KSort> KContext.preprocess(expr: KArrayLambda<D, R>): KExpr<KArraySort<D, R>>

fun <R : KSort> KContext.preprocess(expr: KArrayNLambda<R>): KExpr<KArrayNSort<R>>

fun <T : KSort> KContext.preprocess(expr: KDistinctExpr<T>): KExpr<KBoolSort>

fun <T : KSort> KContext.preprocess(expr: KEqExpr<T>): KExpr<KBoolSort>

fun KContext.preprocess(expr: KExistentialQuantifier): KExpr<KBoolSort>

fun KContext.preprocess(expr: KUniversalQuantifier): KExpr<KBoolSort>

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>

resetCache

fun resetCache()

Reset transformer expression cache.

retryExprTransformation

fun retryExprTransformation(expr: KExpr<*>)

rewrite

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

rewrittenOrNull

fun <T : KSort> rewrittenOrNull(expr: KExpr<T>): KExpr<T>?

simplifyEqArray

open fun <A : KArraySortBase<R>, R : KSort> simplifyEqArray(lhs: KExpr<A>, rhs: KExpr<A>): KExpr<KBoolSort>

simplifyEqBool

open fun simplifyEqBool(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>): KExpr<KBoolSort>

simplifyEqBv

open fun <T : KBvSort> simplifyEqBv(lhs: KExpr<T>, rhs: KExpr<T>): KExpr<KBoolSort>

simplifyEqFp

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.

simplifyEqInt

open fun simplifyEqInt(lhs: KExpr<KIntSort>, rhs: KExpr<KIntSort>): KExpr<KBoolSort>

simplifyEqReal

open fun simplifyEqReal(lhs: KExpr<KRealSort>, rhs: KExpr<KRealSort>): KExpr<KBoolSort>

simplifyEqUninterpreted

open fun simplifyEqUninterpreted(lhs: KExpr<KUninterpretedSort>, rhs: KExpr<KUninterpretedSort>): KExpr<KBoolSort>

simplifyQuantifier

inline fun <B : KSort, Q : KSort> simplifyQuantifier(bounds: List<KDecl<*>>, simplifiedBody: KExpr<B>, eliminateQuantifier: (KExpr<B>) -> KExpr<Q>, buildQuantifier: (List<KDecl<*>>, KExpr<B>) -> KExpr<Q>): KExpr<Q>

transform

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 <T : KSort> transform(expr: KDistinctExpr<T>): KExpr<KBoolSort>

open override fun <T : KSort> transform(expr: KEqExpr<T>): KExpr<KBoolSort>

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 : KArithSort> transform(expr: KDivArithExpr<T>): KExpr<T>

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>

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

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

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

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

transformAfter

fun KExpr<*>.transformAfter(dependency: KExpr<*>)

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

Transform this expression after dependencies expressions

transformApp

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.

transformAppAfterArgsTransformed

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

KApp non-recursive transformation helper.

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>

transformedExpr

fun <T : KSort> transformedExpr(expr: KExpr<T>): KExpr<T>?

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

transformExpr

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

transformExprAfterTransformed

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.

transformExprDependencyIfNeeded

fun transformExprDependencyIfNeeded(dependency: KExpr<*>, transformedDependency: KExpr<*>?)

transformFpValue

open fun <T : KFpSort> transformFpValue(expr: KFpValue<T>): KExpr<T>

transformIntNum

open fun transformIntNum(expr: KIntNumExpr): KExpr<KIntSort>

transformSelect

open fun <R : KSort> transformSelect(array: KExpr<KArrayNSort<R>>, indices: List<KExpr<KSort>>): KExpr<R>

open fun <D : KSort, R : KSort> transformSelect(array: KExpr<KArraySort<D, R>>, index: KExpr<D>): KExpr<R>

open fun <D0 : KSort, D1 : KSort, R : KSort> transformSelect(array: KExpr<KArray2Sort<D0, D1, R>>, index0: KExpr<D0>, index1: KExpr<D1>): KExpr<R>

open fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transformSelect(array: KExpr<KArray3Sort<D0, D1, D2, R>>, index0: KExpr<D0>, index1: KExpr<D1>, index2: KExpr<D2>): KExpr<R>

transformValue

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

Properties

ctx

open override val ctx: KContext

Inheritors

KModelEvaluator

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.