ksmt-core/io.ksmt.expr/KApp

KApp

abstract class KApp<T : KSort, A : KSort> : KExpr<T>

Functions

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

fun ~~decl~~(): KDecl<T>

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

open override fun hashCode(): Int

open override fun internEquals(other: Any): Boolean

Any.equals analogue for interning purposes.

open override 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

abstract val args: List<KExpr<A>>

val ctx: KContext

abstract val decl: KDecl<T>

abstract val sort: T

Inheritors

KUnaryMinusArithExpr

KPowerArithExpr

KArrayStoreBase

KArraySelectBase

KBvReductionAndExpr

KBvReductionOrExpr

KBvNegationExpr

KBvUnsignedDivExpr

KBvSignedDivExpr

KBvUnsignedRemExpr

KBvSignedRemExpr

KBvSignedModExpr

KBvUnsignedLessExpr

KBvSignedLessExpr

KBvUnsignedLessOrEqualExpr

KBvSignedLessOrEqualExpr

KBvUnsignedGreaterOrEqualExpr

KBvSignedGreaterOrEqualExpr

KBvUnsignedGreaterExpr

KBvSignedGreaterExpr

KBvSignExtensionExpr

KBvZeroExtensionExpr

KBvShiftLeftExpr

KBvLogicalShiftRightExpr

KBvArithShiftRightExpr

KBvRotateLeftExpr

KBvRotateLeftIndexedExpr

KBvRotateRightExpr

KBvRotateRightIndexedExpr

KBvAddNoOverflowExpr

KBvAddNoUnderflowExpr

KBvSubNoOverflowExpr

KBvSubNoUnderflowExpr

KBvDivNoOverflowExpr

KBvNegNoOverflowExpr

KBvMulNoOverflowExpr

KBvMulNoUnderflowExpr

KFpNegationExpr

KFpFusedMulAddExpr

KFpRoundToIntegralExpr

KFpLessOrEqualExpr

KFpGreaterOrEqualExpr

KFpIsNormalExpr

KFpIsSubnormalExpr

KFpIsInfiniteExpr

KFpIsNegativeExpr

KFpIsPositiveExpr

KFpToIEEEBvExpr

KInterpretedValue

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?