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上界，该理论扩展了组合数组逻辑，增加了索引集上的序关系以及表达元素求和的能力。我们从表达能力和计算复杂度两个方面，将我们的片段与文献中其他七个片段进行了比较。