We prove an NP upper bound on a theory of integer-indexed integer-valued arrays that extends combinatory array logic with an ordering relation on the index set and the ability to express sums of elements. We compare our fragment with seven other fragments in the literature in terms of their expressiveness and computational complexity.

翻译：我们证明了在索引集上具有序关系并能表达元素求和的整数索引整数值数组理论具有NP上界。我们从表达能力和计算复杂度两方面，将我们的片段与文献中的其他七个片段进行了比较。