Array theories are fragments of the first-order theory of arrays which restrict the use of first-order quantifiers. They were first used in deductive software verification to reason about properties of imperative programs. Since then, research has focused in identifying decidable fragments and applications.

In recent years, a family of decidable fragments of the theory of arrays have been used in the verification of so-called array-based systems. This abstraction is used to model sequential programs manipulating linear data structures such as arrays and lists, as well as parameterised concurrent systems with local and shared variables. These programs are essential in specialised computing scenarios such as data-base driven systems.

Lately, we have investigated the algebraic structure of these array theories. We have observed that they extend the quantifier-free fragment of the theory of arrays with relations that are defined homogeneously for every component of the arrays. We have also given an algebraic description of the decision procedures for the satisfiability problem of these theories. In particular, we have described how the satisfiability problem can be reduced in polynomial time to the satisfiability problem of the theory of a power structure. Our results are applicable to a variety of array theories from the literature to which we refer to as “parametric” array theories since they often allow to be instantiated with different index and element theories.

An interesting feature of parametric array theories is that the componentwise relations only need one universal quantifier to be expressed. This is in contrast to other fragments of the theory of arrays such as the array property fragment. While “array properties” allow several universal quantifiers, this comes at the cost of severe syntactic restrictions. In contrast, parametric array theories offer the possibility of using linear arithmetic constraints on the cardinalities of sets of indices as well as constraints on the sums of elements of array variables. These properties are inexpressible in the array property fragment.

This paper shows that constraints on the cardinalities of sets of indices and sums of elements can be combined with regular relations on the indices of arrays while preserving decidability. This extension is useful for specifying properties of arrays such as those appearing in array folds logic. While array folds logic only allows folding expressions over one array variable, this restriction does not appear in the fragment that we present.

Our extension is motivated by model theoretic considerations. In particular, Feferman and Vaught introduced the notion of generalised power of a structure and motivated by the question of decidability of the weak monadic second order theory of one succesor (WS1S), raised by Tarski, discuss this theory of indices in their paper. However, deciding WS1S is computationally intractable. Thus, we present the definable relations of the theory in the form of regular expressions. It was proved by Büchi that both formalisms are expressively equivalent.