ksmt-core/io.ksmt.expr/KArrayNStore

KArrayNStore

class KArrayNStore<R : KSort> : KArrayStoreBase<KArrayNSort<R>, R>

Functions

open override fun accept(transformer: KTransformerBase): KExpr<KArrayNSort<R>>

analyzeStore

fun analyzeStore()

Analyze store to provide faster index lookups when store indices are interpreted values.

decl

fun ~~decl~~(): KDecl<KArrayNSort<R>>

equals

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

findArrayToSelectFrom

open override fun findArrayToSelectFrom(indices: List<KExpr<*>>): KExpr<KArrayNSort<R>>

Find an array expression containing the value for the provided indices.

getIndex

open override fun getIndex(idx: Int): KExpr<*>

getNumIndices

open override fun getNumIndices(): Int

hashCode

open override fun hashCode(): Int

internEquals

open override fun internEquals(other: Any): Boolean

Any.equals analogue for interning purposes.

internHashCode

open override fun internHashCode(): Int

Any.hashCode analogue for interning purposes.

open override fun print(printer: ExpressionPrinter)

open override fun print(builder: StringBuilder)

searchForIndex

fun searchForIndex(index: KExpr<*>, indexKind: Int): KExpr<KArrayNSort<R>>

toString

open override fun toString(): String

Properties

args

open override val args: List<KExpr<KSort>>

array

val array: KExpr<KArrayNSort<R>>

ctx

val ctx: KContext

decl

open override val decl: KDecl<KArrayNSort<R>>

indices

open override val indices: List<KExpr<KSort>>

sort

open override val sort: KArrayNSort<R>

value

val value: KExpr<R>

Extensions

asExpr

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

isComplement

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

toRealValue

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