ksmt-core/io.ksmt.decl/KFuncDecl1

KFuncDecl1

abstract class KFuncDecl1<T : KSort, A : KSort>(ctx: KContext, name: String, resultSort: T, val argSort: A) : KFuncDecl<T>

Constructors

fun <T : KSort, A : KSort> KFuncDecl1(ctx: KContext, name: String, resultSort: T, argSort: A)

Functions

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

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

abstract fun KContext.apply(arg: KExpr<A>): KApp<T, A>

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 argSorts: List<KSort>

val ctx: KContext

val name: String

val sort: T

Inheritors

KArithUnaryMinusDecl

KArrayConstDecl

KBvReductionAndDecl

KBvReductionOrDecl

KBvNegationDecl

KBvRotateLeftIndexedDecl

KBvRotateRightIndexedDecl

KBvNegNoOverflowDecl

KFpNegationDecl

KFpIsNormalDecl

KFpIsSubnormalDecl

KFpIsInfiniteDecl

KFpIsNegativeDecl

KFpIsPositiveDecl

KFpToIEEEBvDecl