ksmt-core/io.ksmt.expr.transformer/KNonRecursiveTransformer/transform

transform

open override fun <T : KSort> transform(expr: KFunctionApp<T>): KExpr<T>
open override fun <T : KSort> transform(expr: KConst<T>): KExpr<T>
open override fun transform(expr: KAndExpr): KExpr<KBoolSort>
open override fun transform(expr: KAndBinaryExpr): KExpr<KBoolSort>
open override fun transform(expr: KOrExpr): KExpr<KBoolSort>
open override fun transform(expr: KOrBinaryExpr): KExpr<KBoolSort>
open override fun transform(expr: KNotExpr): KExpr<KBoolSort>
open override fun transform(expr: KImpliesExpr): KExpr<KBoolSort>
open override fun transform(expr: KXorExpr): KExpr<KBoolSort>
open override fun <T : KSort> transform(expr: KEqExpr<T>): KExpr<KBoolSort>
open override fun <T : KSort> transform(expr: KDistinctExpr<T>): KExpr<KBoolSort>
open override fun <T : KSort> transform(expr: KIteExpr<T>): KExpr<T>
open override fun <T : KBvSort> transform(expr: KBvNotExpr<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 <T : KBvSort> transform(expr: KBvAndExpr<T>): KExpr<T>
open override fun <T : KBvSort> transform(expr: KBvOrExpr<T>): KExpr<T>
open override fun <T : KBvSort> transform(expr: KBvXorExpr<T>): KExpr<T>
open override fun <T : KBvSort> transform(expr: KBvNAndExpr<T>): KExpr<T>
open override fun <T : KBvSort> transform(expr: KBvNorExpr<T>): KExpr<T>
open override fun <T : KBvSort> transform(expr: KBvXNorExpr<T>): KExpr<T>
open override fun <T : KBvSort> transform(expr: KBvNegationExpr<T>): KExpr<T>
open override fun <T : KBvSort> transform(expr: KBvAddExpr<T>): KExpr<T>
open override fun <T : KBvSort> transform(expr: KBvSubExpr<T>): KExpr<T>
open override fun <T : KBvSort> transform(expr: KBvMulExpr<T>): KExpr<T>
open override fun <T : KBvSort> transform(expr: KBvUnsignedDivExpr<T>): KExpr<T>
open override fun <T : KBvSort> transform(expr: KBvSignedDivExpr<T>): KExpr<T>
open override fun <T : KBvSort> transform(expr: KBvUnsignedRemExpr<T>): KExpr<T>
open override fun <T : KBvSort> transform(expr: KBvSignedRemExpr<T>): KExpr<T>
open override fun <T : KBvSort> transform(expr: KBvSignedModExpr<T>): KExpr<T>
open override fun <T : KBvSort> transform(expr: KBvUnsignedLessExpr<T>): KExpr<KBoolSort>
open override fun <T : KBvSort> transform(expr: KBvSignedLessExpr<T>): KExpr<KBoolSort>
open override fun <T : KBvSort> transform(expr: KBvUnsignedLessOrEqualExpr<T>): KExpr<KBoolSort>
open override fun <T : KBvSort> transform(expr: KBvSignedLessOrEqualExpr<T>): KExpr<KBoolSort>
open override fun <T : KBvSort> transform(expr: KBvUnsignedGreaterOrEqualExpr<T>): KExpr<KBoolSort>
open override fun <T : KBvSort> transform(expr: KBvSignedGreaterOrEqualExpr<T>): KExpr<KBoolSort>
open override fun <T : KBvSort> transform(expr: KBvUnsignedGreaterExpr<T>): KExpr<KBoolSort>
open override fun <T : KBvSort> transform(expr: KBvSignedGreaterExpr<T>): KExpr<KBoolSort>
open override fun transform(expr: KBvConcatExpr): KExpr<KBvSort>
open override fun transform(expr: KBvExtractExpr): KExpr<KBvSort>
open override fun transform(expr: KBvSignExtensionExpr): KExpr<KBvSort>
open override fun transform(expr: KBvZeroExtensionExpr): KExpr<KBvSort>
open override fun transform(expr: KBvRepeatExpr): KExpr<KBvSort>
open override fun <T : KBvSort> transform(expr: KBvShiftLeftExpr<T>): KExpr<T>
open override fun <T : KBvSort> transform(expr: KBvLogicalShiftRightExpr<T>): KExpr<T>
open override fun <T : KBvSort> transform(expr: KBvArithShiftRightExpr<T>): KExpr<T>
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 transform(expr: KBv2IntExpr): KExpr<KIntSort>
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: KBvSubNoOverflowExpr<T>): KExpr<KBoolSort>
open override fun <T : KBvSort> transform(expr: KBvSubNoUnderflowExpr<T>): KExpr<KBoolSort>
open override fun <T : KBvSort> transform(expr: KBvDivNoOverflowExpr<T>): KExpr<KBoolSort>
open override fun <T : KBvSort> transform(expr: KBvNegNoOverflowExpr<T>): KExpr<KBoolSort>
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 : KFpSort> transform(expr: KFpAbsExpr<T>): KExpr<T>
open override fun <T : KFpSort> transform(expr: KFpNegationExpr<T>): KExpr<T>
open override fun <T : KFpSort> transform(expr: KFpAddExpr<T>): KExpr<T>
open override fun <T : KFpSort> transform(expr: KFpSubExpr<T>): KExpr<T>
open override fun <T : KFpSort> transform(expr: KFpMulExpr<T>): KExpr<T>
open override fun <T : KFpSort> transform(expr: KFpDivExpr<T>): KExpr<T>
open override fun <T : KFpSort> transform(expr: KFpFusedMulAddExpr<T>): KExpr<T>
open override fun <T : KFpSort> transform(expr: KFpSqrtExpr<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: KFpMinExpr<T>): KExpr<T>
open override fun <T : KFpSort> transform(expr: KFpMaxExpr<T>): KExpr<T>
open override fun <T : KFpSort> transform(expr: KFpLessOrEqualExpr<T>): KExpr<KBoolSort>
open override fun <T : KFpSort> transform(expr: KFpLessExpr<T>): KExpr<KBoolSort>
open override fun <T : KFpSort> transform(expr: KFpGreaterOrEqualExpr<T>): KExpr<KBoolSort>
open override fun <T : KFpSort> transform(expr: KFpGreaterExpr<T>): KExpr<KBoolSort>
open override fun <T : KFpSort> transform(expr: KFpEqualExpr<T>): KExpr<KBoolSort>
open override fun <T : KFpSort> transform(expr: KFpIsNormalExpr<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: 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: KFpIsPositiveExpr<T>): KExpr<KBoolSort>
open override fun <T : KFpSort> transform(expr: KFpToBvExpr<T>): KExpr<KBvSort>
open override fun <T : KFpSort> transform(expr: KFpToRealExpr<T>): KExpr<KRealSort>
open override fun <T : KFpSort> transform(expr: KFpToIEEEBvExpr<T>): KExpr<KBvSort>
open override fun <T : KFpSort> transform(expr: KFpFromBvExpr<T>): KExpr<T>
open override fun <T : KFpSort> transform(expr: KFpToFpExpr<T>): KExpr<T>
open override fun <T : KFpSort> transform(expr: KRealToFpExpr<T>): KExpr<T>
open override fun <T : KFpSort> transform(expr: KBvToFpExpr<T>): KExpr<T>
open override fun <D : KSort, R : KSort> transform(expr: KArrayStore<D, R>): KExpr<KArraySort<D, 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: KArray3Store<D0, D1, D2, R>): KExpr<KArray3Sort<D0, D1, D2, 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 <D0 : KSort, D1 : KSort, R : KSort> transform(expr: KArray2Select<D0, D1, R>): KExpr<R>
open override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(expr: KArray3Select<D0, D1, D2, R>): KExpr<R>
open override fun <R : KSort> transform(expr: KArrayNSelect<R>): KExpr<R>
open override fun <A : KArraySortBase<R>, R : KSort> transform(expr: KArrayConst<A, R>): KExpr<A>
open override fun <T : KArithSort> transform(expr: KAddArithExpr<T>): KExpr<T>
open override fun <T : KArithSort> transform(expr: KMulArithExpr<T>): KExpr<T>
open override fun <T : KArithSort> transform(expr: KSubArithExpr<T>): KExpr<T>
open override fun <T : KArithSort> transform(expr: KUnaryMinusArithExpr<T>): KExpr<T>
open override fun <T : KArithSort> transform(expr: KDivArithExpr<T>): KExpr<T>
open override fun <T : KArithSort> transform(expr: KPowerArithExpr<T>): KExpr<T>
open override fun <T : KArithSort> transform(expr: KLtArithExpr<T>): KExpr<KBoolSort>
open override fun <T : KArithSort> transform(expr: KLeArithExpr<T>): KExpr<KBoolSort>
open override fun <T : KArithSort> transform(expr: KGtArithExpr<T>): KExpr<KBoolSort>
open override fun <T : KArithSort> transform(expr: KGeArithExpr<T>): KExpr<KBoolSort>
open override fun transform(expr: KModIntExpr): KExpr<KIntSort>
open override fun transform(expr: KRemIntExpr): KExpr<KIntSort>
open override fun transform(expr: KToRealIntExpr): KExpr<KRealSort>
open override fun transform(expr: KToIntRealExpr): KExpr<KIntSort>
open override fun transform(expr: KIsIntRealExpr): KExpr<KBoolSort>

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 <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 <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 transform(expr: KUniversalQuantifier): KExpr<KBoolSort>

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