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

transform

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