ksmt-core/io.ksmt.expr/KArrayLambdaBase

KArrayLambdaBase

sealed class KArrayLambdaBase<A : KArraySortBase<R>, R : KSort> : KExpr<A>

Array lambda binding.

Defined as in the Z3 solver

Functions

abstract fun accept(transformer: KTransformerBase): KExpr<A>

open operator override fun equals(other: Any?): Boolean

open override fun hashCode(): Int

abstract fun internEquals(other: Any): Boolean

Any.equals analogue for interning purposes.

abstract fun internHashCode(): Int

Any.hashCode analogue for interning purposes.

open override fun print(printer: ExpressionPrinter)

open override fun print(builder: StringBuilder)

open override fun toString(): String

Properties

val body: KExpr<R>

val ctx: KContext

indexVarDeclarations

abstract val indexVarDeclarations: List<KDecl<*>>

open override val sort: A

Inheritors

Extensions

fun <T : KSort> KExpr<*>.asExpr(sort: T): KExpr<T>

fun KExpr<KBoolSort>.isComplement(other: KExpr<KBoolSort>): Boolean

fun <T : KArithSort> KExpr<T>.toRealValue(): ArithUtils.RealValue?