ksmt-core/io.ksmt.solver.util

Package-level declarations

Types

Link copied to clipboard
@JvmInline
value class ExprConversionResult(expr: KExpr<*>?)
Link copied to clipboard
abstract class KExprConverterBase<T : Any>
Link copied to clipboard
Link copied to clipboard
Link copied to clipboard
abstract class KExprIntInternalizerBase : KTransformerBase

Specialized version of KExprInternalizerBase for Int native expressions.

Link copied to clipboard
abstract class KExprLongConverterBase

Specialized version of KExprConverterBase for Long native expressions.

Link copied to clipboard
abstract class KExprLongInternalizerBase : KTransformerBase

Specialized version of KExprInternalizerBase for Long native expressions.

Functions

Link copied to clipboard
inline fun <S : KSort, T, Stack> conversionLoop(stack: Stack, native: T, stackPush: (Stack, T) -> Unit, stackPop: (Stack) -> T, stackIsNotEmpty: (Stack) -> Boolean, convertNative: (T) -> ExprConversionResult, findConverted: (T) -> KExpr<*>?, saveConverted: (T, KExpr<*>) -> Unit): KExpr<S>
Link copied to clipboard
inline fun <T, TArray, Stack> ensureArgsConvertedAndConvert(stack: Stack, expr: T, args: TArray, expectedSize: Int, stackPush: (Stack, T) -> Unit, arraySize: (TArray) -> Int, arrayGet: (TArray, Int) -> T, findConverted: (T) -> KExpr<*>?): List<KExpr<*>>?

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

Link copied to clipboard
inline fun <T> KTransformerBase.internalizationLoop(exprStack: MutableList<KExpr<*>>, initialExpr: KExpr<*>, notInternalized: T, findInternalized: (KExpr<*>) -> T): T
Link copied to clipboard
inline fun <S : KExpr<*>, T> S.transform(operation: () -> T, saveInternalized: (KExpr<*>, T) -> Unit): S
inline fun <S : KExpr<*>, T> S.transform(exprStack: MutableList<KExpr<*>>, arg: KExpr<*>, operation: (T) -> T, notInternalized: T, findInternalized: (KExpr<*>) -> T, saveInternalized: (KExpr<*>, T) -> Unit): S
inline fun <S : KExpr<*>, T> S.transform(exprStack: MutableList<KExpr<*>>, arg0: KExpr<*>, arg1: KExpr<*>, operation: (T, T) -> T, notInternalized: T, findInternalized: (KExpr<*>) -> T, saveInternalized: (KExpr<*>, T) -> Unit): S
inline fun <S : KExpr<*>, T> S.transform(exprStack: MutableList<KExpr<*>>, arg0: KExpr<*>, arg1: KExpr<*>, arg2: KExpr<*>, operation: (T, T, T) -> T, notInternalized: T, findInternalized: (KExpr<*>) -> T, saveInternalized: (KExpr<*>, T) -> Unit): S
inline fun <S : KExpr<*>, T> S.transform(exprStack: MutableList<KExpr<*>>, arg0: KExpr<*>, arg1: KExpr<*>, arg2: KExpr<*>, arg3: KExpr<*>, operation: (T, T, T, T) -> T, notInternalized: T, findInternalized: (KExpr<*>) -> T, saveInternalized: (KExpr<*>, T) -> Unit): S
Link copied to clipboard
inline fun <S : KExpr<*>, T, A> S.transformList(exprStack: MutableList<KExpr<*>>, args: List<KExpr<*>>, operation: (A) -> T, mkArray: (Int) -> A, setArray: (A, Int, T) -> Unit, notInternalized: T, findInternalized: (KExpr<*>) -> T, saveInternalized: (KExpr<*>, T) -> Unit): S