simplify
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).
See simplifyExprBase for the details.
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.