mk
open fun <D : KSort, R : KSort> mkArrayStoreNoSimplifyNoAnalyze(array: KExpr<KArraySort<D, R>>, index: KExpr<D>, value: KExpr<R>): KArrayStore<D, R>
Create an array store expression (store array value) without cache. Cache is used to speed up mkArraySelect operation simplification but can result in a huge memory consumption.
See also
for the cache details.
open fun <D0 : KSort, D1 : KSort, R : KSort> mkArrayStoreNoSimplifyNoAnalyze(array: KExpr<KArray2Sort<D0, D1, R>>, index0: KExpr<D0>, index1: KExpr<D1>, value: KExpr<R>): KArray2Store<D0, D1, R>
Create an array store expression (store array index1) without cache. Cache is used to speed up mkArraySelect operation simplification but can result in a huge memory consumption.
See also
for the cache details.
open fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> mkArrayStoreNoSimplifyNoAnalyze(array: KExpr<KArray3Sort<D0, D1, D2, R>>, index0: KExpr<D0>, index1: KExpr<D1>, index2: KExpr<D2>, value: KExpr<R>): KArray3Store<D0, D1, D2, R>
Create an array store expression (store array index1 value) without cache. Cache is used to speed up mkArraySelect operation simplification but can result in a huge memory consumption.
See also
for the cache details.