simplifySelectFromArrayStore

inline fun <A : KArraySortBase<R>, R : KSort, S : KArrayStoreBase<A, R>> KContext.simplifySelectFromArrayStore(initialArray: KExpr<A>, storeIndicesMatch: (S) -> Boolean, storeIndicesDistinct: (S) -> Boolean, findArrayToSelectFrom: (S) -> KExpr<A>, default: (KExpr<A>) -> KExpr<R>): KExpr<R>

Simplify select from a chain of array store expressions.

If array stores are not analyzed (see KArrayStoreBase.analyzeStore) this operation will traverse whole array store chain. Otherwise, we speed up the traversal with KArrayStoreBase.findArrayToSelectFrom. In the case of a one-dimensional arrays, this operation is guaranteed to perform only one iteration of the loop (constant). For the multi-dimensional arrays, usually only a few iterations will be performed, but in the worst case we may traverse the entire stores chain.


inline fun <D : KSort, R : KSort> KContext.simplifySelectFromArrayStore(array: KExpr<KArraySort<D, R>>, index: KExpr<D>, storeIndexMatch: KContext.(KArrayStore<D, R>, KExpr<D>) -> Boolean, storeIndexDistinct: KContext.(KArrayStore<D, R>, KExpr<D>) -> Boolean, cont: (KExpr<KArraySort<D, R>>, KExpr<D>) -> KExpr<R>): KExpr<R>
inline fun <D0 : KSort, D1 : KSort, R : KSort> KContext.simplifySelectFromArrayStore(array: KExpr<KArray2Sort<D0, D1, R>>, index0: KExpr<D0>, index1: KExpr<D1>, storeIndexMatch: KContext.(KArray2Store<D0, D1, R>, KExpr<D0>, KExpr<D1>) -> Boolean, storeIndexDistinct: KContext.(KArray2Store<D0, D1, R>, KExpr<D0>, KExpr<D1>) -> Boolean, cont: (KExpr<KArray2Sort<D0, D1, R>>, KExpr<D0>, KExpr<D1>) -> KExpr<R>): KExpr<R>
inline fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> KContext.simplifySelectFromArrayStore(array: KExpr<KArray3Sort<D0, D1, D2, R>>, index0: KExpr<D0>, index1: KExpr<D1>, index2: KExpr<D2>, storeIndexMatch: KContext.(KArray3Store<D0, D1, D2, R>, KExpr<D0>, KExpr<D1>, KExpr<D2>) -> Boolean, storeIndexDistinct: KContext.(KArray3Store<D0, D1, D2, R>, KExpr<D0>, KExpr<D1>, KExpr<D2>) -> Boolean, cont: (KExpr<KArray3Sort<D0, D1, D2, R>>, KExpr<D0>, KExpr<D1>, KExpr<D2>) -> KExpr<R>): KExpr<R>