ksmt-core/io.ksmt.decl/KFuncDecl2

KFuncDecl2

abstract class KFuncDecl2<T : KSort, A0 : KSort, A1 : KSort>(ctx: KContext, name: String, resultSort: T, val arg0Sort: A0, val arg1Sort: A1) : KFuncDecl<T>

Constructors

fun <T : KSort, A0 : KSort, A1 : KSort> KFuncDecl2(ctx: KContext, name: String, resultSort: T, arg0Sort: A0, arg1Sort: A1)

Functions

open override fun <R> accept(visitor: KDeclVisitor<R>): R

open override fun apply(args: List<KExpr<*>>): KApp<T, *>

abstract fun KContext.apply(arg0: KExpr<A0>, arg1: KExpr<A1>): KApp<T, *>

fun checkArgSorts(args: List<KExpr<*>>)

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

open override fun hashCode(): Int

open override fun print(builder: StringBuilder)

open override fun toString(): String

Properties

val arg0Sort: A0

val arg1Sort: A1

val argSorts: List<KSort>

val ctx: KContext

val name: String

val sort: T

Inheritors

KArithPowerDecl

KBvUnsignedDivDecl

KBvSignedDivDecl

KBvUnsignedRemDecl

KBvSignedRemDecl

KBvSignedModDecl

KBvUnsignedLessDecl

KBvSignedLessDecl

KBvSignedLessOrEqualDecl

KBvUnsignedLessOrEqualDecl

KBvUnsignedGreaterOrEqualDecl

KBvSignedGreaterOrEqualDecl

KBvUnsignedGreaterDecl

KBvSignedGreaterDecl

KBvShiftLeftDecl

KBvLogicalShiftRightDecl

KBvArithShiftRightDecl

KBvRotateLeftDecl

KBvRotateRightDecl

KBvAddNoOverflowDecl

KBvAddNoUnderflowDecl

KBvSubNoOverflowDecl

KBvSubNoUnderflowDecl

KBvDivNoOverflowDecl

KBvMulNoOverflowDecl

KBvMulNoUnderflowDecl

KFpRoundToIntegralDecl

KFpLessOrEqualDecl

KFpGreaterOrEqualDecl