ksmt-core/io.ksmt.solver.util/KExprConverterBase

KExprConverterBase

abstract class KExprConverterBase<T : Any>

Constructors

Link copied to clipboard

Functions

Link copied to clipboard
inline fun <T : KSort> convert(op: () -> KExpr<T>): ExprConversionResult
inline fun <S : KSort, A0 : KSort> T.convert(args: Array<T>, op: (KExpr<A0>) -> KExpr<S>): ExprConversionResult
inline fun <S : KSort, A0 : KSort, A1 : KSort> T.convert(args: Array<T>, op: (KExpr<A0>, KExpr<A1>) -> KExpr<S>): ExprConversionResult
inline fun <S : KSort, A0 : KSort, A1 : KSort, A2 : KSort> T.convert(args: Array<T>, op: (KExpr<A0>, KExpr<A1>, KExpr<A2>) -> KExpr<S>): ExprConversionResult
inline fun <S : KSort, A0 : KSort, A1 : KSort, A2 : KSort, A3 : KSort> T.convert(args: Array<T>, op: (KExpr<A0>, KExpr<A1>, KExpr<A2>, KExpr<A3>) -> KExpr<S>): ExprConversionResult
Link copied to clipboard
Link copied to clipboard
inline fun <S : KSort, A : KSort> T.convertList(args: Array<T>, op: (List<KExpr<A>>) -> KExpr<S>): ExprConversionResult
Link copied to clipboard
Link copied to clipboard
inline fun <S : KSort> T.convertReduced(args: Array<T>, op: (KExpr<S>, KExpr<S>) -> KExpr<S>): ExprConversionResult
Link copied to clipboard
fun ensureArgsConvertedAndConvert(expr: T, args: Array<T>, expectedSize: Int): List<KExpr<*>>?

Ensure all expression arguments are already converted. Return converted arguments or null if not all arguments converted.

inline fun ensureArgsConvertedAndConvert(expr: T, args: Array<T>, expectedSize: Int, converter: (List<KExpr<*>>) -> KExpr<*>): ExprConversionResult

Ensure all expression arguments are already converted. If not so, argumentsConversionRequired is returned.

Link copied to clipboard
abstract fun findConvertedNative(expr: T): KExpr<*>?
Link copied to clipboard
abstract fun saveConvertedNative(native: T, converted: KExpr<*>)

Properties

Link copied to clipboard