Introduction

Many abstractions in computer science and mathematics are naturally modelled as collections of objects of certain type. When addressing the problem of automatically verifying properties of such abstractions it becomes crucial to choose an adequate language in which to express the properties of interest.

Our research is influenced by work in the area of deductive software verification [5,23]. Research in this area led to the development of specialised algorithms that determine the validity of formulas in restricted fragments of first-order logic. The resulting algorithms are today studied in the so-called satisfiability modulo theories (SMT) framework.

Starting with [21], first-order theories under the name of "array theories" have been studied and, along the years, new decidable fragments and applications have been found. Bradley [6] carried out a systematic exploration of a very expressive and decidable fragment known as the "array property fragment". Most notably, this fragment allowed to express the property of an array being ordered while having an efficiently decidable satisfiable problem under mild restrictions. Moreover, Bradley's work showed that minor variations to the fragment's syntax would led to undecidability, by reduction from Hilbert's tenth problem.

In spite of the above, and after Bradley's work, a family of decidable array theories has been used in the verification of so-called array-based systems [17,26,13,27,15]. This framework has been used to model sequential programs manipulating arrays and lists, as well as parameterised concurrent systems with local and shared variables [3,1,20]. These programs are essential in specialised computing scenarios such as data-base driven systems [4] or business processes [15].

In [30,29,31,32], we have investigated the structure of these array theories. We have observed that they extend classical array theories with point-wise relations, which are defined as in the element theory for every component of the arrays. The conclusion of our investigation is that these point-wise relations are the essential difficulty when designing decision procedures for these theories. In particular, we have described how the satisfiability problem of these theories can be reduced in polynomial time to the satisfiability problem of the theory of a power structure [28] and that the latter admits an efficient procedure for eliminating existential quantifiers [30].

Our results are applicable to a variety of array theories from the literature [10,16,14,1] 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 require one universal quantifier to be expressed. For instance, one may define the addition of two arrays 𝑎 and 𝑏 as:

𝑎 + 𝑏 = 𝑐 if and only if for every 𝑖 ∈ 𝐼 , 𝑎(𝑖) + 𝑏(𝑖) = 𝑐(𝑖)

This is in contrast to other array theories such as the array property fragment [5], which allow properties using several related universally quantified indices. For instance, one may define in this fragment the property of an array being ordered:

𝑎 is ordered if and only if for every 𝑖, 𝑗 ∈ 𝐼 , 𝑖 ≤ 𝑗 implies 𝑎[𝑖] ≤ 𝑎 [𝑗] While "array properties" in [5] allow several universal quantifiers, this comes at the cost of severe syntactic restrictions. In contrast, parametric array theories offer the possibility of using linear cardinality relations on sets of indices [16,14,1,30] 1 as well as constraints on the sums of elements of array variables. These properties are inexpressible in the array property fragment.

These results motivate us to push further our investigation. In this paper, rather than moving to the design of algorithms for first-order theories (which would be justified by the incipient quantifier elimination method of [30]), we choose to further explore the possibilities in the quantifier-free setting which is the one relevant to the satisfiability modulo theories framework.

We take inspiration from the work of Feferman and Vaught [12], who 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 generalised powers with this theory of indices in the later sections of their paper. However, deciding WS1S is computationally intractable [34]. Thus, we present the definable relations of the theory in the form of regular expressions. It was proved by Büchi [7] that both formalisms are expressively equivalent. We refer to the relations on sets of indices induced by regular expressions or WS1S formulas as regular relations. 2 There are several reasons that lead us to think that an extension of array theories with cardinality constraints and regular expressions is worthwhile investigating. First, this extends the work of Alberti, Ghilardi and Pagani [1] since it is well-known that WS1S is more expressive than Presburger arithmetic [35]. Second, this extension allows us to express properties of arrays such as those appearing in array folds logic [9]. While array folds logic only allows folding expressions over one array variable, this restriction does not appear in the fragment that we present. Third, a similar extension but without cardinality constraints has been considered concurrently to our work in [18].

Both in [18] and in our work, it seems that a non-trivial insight for the construction of the decision algorithm is needed. We point out to the reader that this insight is materialised in our paper in the partition variables introduced in Section 4.1. Indeed, since our specifications contain formulas whose interpretations, as sets of indices of the arrays, may overlap, it is essential to ensure that there exists a model adhering to the regular specification regardless of the overlaps in the semantic domain.

Unlike [18], we focus in the case of regular languages which should be more familiar to the readers. Nevertheless, we include a final section pointing out the main ingredients of the extension to regular tree languages. Also, for the sake of clarity, we have focused in cardinality constraints, but it should be clear that an extension to summation constraints is also possible.

Organisation of the paper. The rest of the paper is organised as follows. Section 2 describes generalised powers using specific theories of sets with cardinalities, theories describing their contents, and theories describing regular relations on the indices of these sets. Section 3 describes the satisfiability preserving encoding of arrays in generalised powers. Section 4 gives an algorithm that in polynomial time takes as input a generalised power structure specification and outputs an equivalent formula in 1 A similar notion appears in the model theory literature under the name of Härtig's quantifier [2]. 2 We had considered regular expressions in our PhD thesis [29]. Here we consider regular expressions over first-order formulas. This formalism has been popularised in recent times under the name of symbolic regular expression and it can also be seen as motivated by Feferman-Vaught's results. This is what we mean by "succinct" regular relations. We also sometimes speak of "ordering" instead of regular relations since regular relations are precisely those expressible in the monadic theory of order [7].

the combination of the quantifier-free theory of Boolean algebra of sets with Presburger arithmetic and the alphabet's theory. Section 5 discusses the applicability of the technique in the setting of theories of trees, connecting to recent work. Section 6 concludes the paper.

Generalised powers

Let us start with the definition of generalised power structure as it is given in [12].

Definition 2.1. The generalised power 𝒫 (ℳ, 𝐼 ) of a structure ℳ = ⟨𝑀, …⟩ is a structure whose carrier set is the set 𝑀 𝐼 of functions from the (possibly infinite) index set 𝐼 to the carrier set 𝑀 of the structure ℳ and whose relations are interpreted as sets of the form

{(𝑎 1 , … , 𝑎 𝑛 ) ∈ (𝑀 𝐼 ) 𝑛 | Φ(𝑆 1 , … , 𝑆 𝑘 )}

where 𝑛 is a natural number, Φ is a Boolean algebra expression over 𝒫 (𝐼 ) using the symbols ⊆, ∪, ∩ or ⋅ 𝑐 and each set variable 𝑆 is interpreted as

𝑆 = {𝑖 ∈ 𝐼 | 𝜃(𝑎 1 (𝑖), … , 𝑎 𝑛 (𝑖))}

where 𝜃 is a formula in the first-order theory of ℳ.

In the following, we will use the term "arrays" for the functional elements in the carrier from a generalised power 𝒫 (ℳ, 𝐼 ), the term "elements" for the members of the carrier set of the structure ℳ and the term "indices" for the members of the set 𝐼. We will use the notation 𝑎(𝑖) when we want to emphasize the algebraic perspective and the notation 𝑎[𝑖] when we want to emphasize the connection to array theories. In particular, we will use the latter notation when describing how to translate from parametric array theories to generalised powers.

Nothing prevents us from considering set interpretations of the form

𝑆 = {𝑖 ∈ 𝐼 | 𝜓 (𝑖)}

where 𝜓 is a formula that refers only to indices in the set 𝐼. In fact, this direction is pursued in [1] where a fragment of the theory of arrays is investigated that corresponds to a generalised power whose set interpretations conflate both the theory of indices and the theory of elements using the quantifier-free fragment of Presburger arithmetic to refer to both. We will use different set interpretations for indices and elements. We will use relations of the following form:

𝐹 (𝑆 1 , … , 𝑆 𝑘 ) ∧ 𝑅(𝑆 1 , … , 𝑆 𝑘 ) ∧ 𝐶(𝑎 1 , … , 𝑎 𝑘 )(1)

Here 𝐹 specifies linear cardinality constraints on the shared set variables 𝑆 1 , … , 𝑆 𝑘 . 𝑅 specifies the regular relations on the set of indices 𝑆 1 , … , 𝑆 𝑘 . Finally, 𝐶 specifies the componentwise relations on the arrays 𝑎 1 , … , 𝑎 𝑘 . The precise description of Formula (1) occupies the rest of the section.

Sets of indices

Formulas 𝐹 , 𝑅 and 𝐶 in (1) use variables 𝑆 1 , … , 𝑆 𝑘 representing subsets of an index set 𝐼. This is explicitly shown in (1) for 𝐹 and 𝑅. The variables 𝑆 1 , … , 𝑆 𝑘 are omitted from formula 𝐶 to emphasize the role of componentwise relations on array variables. Thus, the variables 𝑆 1 , … , 𝑆 𝑘 are used to combine the three theories. This approach to theory combination was pioneered in [37]. As we focus on arrays, 𝐼 = ℕ. Generalisations to trees are also possible and in that case 𝐼 = {0, 1} * .

Linear cardinality constraints on the sets of indices

𝐹 (𝑆 1 , … , 𝑆 𝑘 ) is a formula in the quantifier-free theory of Boolean algebra with Presburger arithmetic (QFBAPA) [25]. The syntax of QFBAPA is given in Figure 1. The top-level symbol 𝐹 presents the Boolean structure of the formula, 𝐴 stands for the atomic formulas which can be either Boolean algebra expressions on the sets denoted by the symbol 𝐵 or Presburger arithmetic restrictions on numbers denoted by the symbol 𝑇. The operator dvd stands for the divisibility relation, which is used to ensure that the quantifier-free fragment has the same expressive power as the full first-order theory of Boolean algebra with Presburger arithmetic (BAPA) [24]. 𝒰 represents the universal set 𝐼. Lowercase 𝑥 and 𝑘 represent Boolean and integer variables respectively. The remaining interpretations are standard in the respective theories (Boolean algebra of sets or Presburger arithmetic).

𝐹 ∶∶= 𝐴 | 𝐹 1 ∧ 𝐹 2 | 𝐹 1 ∨ 𝐹 2 | ¬𝐹 𝐴 ∶∶= 𝐵 1 = 𝐵 2 | 𝐵 1 ⊆ 𝐵 2 | 𝑇 1 = 𝑇 2 | 𝑇 1 ≤ 𝑇 2 | 𝐾 dvd 𝑇 𝐵 ∶∶= 𝑥 | ∅ | 𝒰 | 𝐵 1 ∪ 𝐵 2 | 𝐵 1 ∩ 𝐵 2 | 𝐵 𝑐 𝑇 ∶∶= 𝑘 | 𝐾 | 𝑇 1 + 𝑇 2 | 𝐾 ⋅ 𝑇 | |𝐵| 𝐾 ∶∶= … | − 2 | − 1 | 0 | 1 | 2 | … Figure 1: QFBAPA's syntax Example 2.1. An example of QFBAPA formula is |𝐴| > 1 ∧ 𝐴 ⊆ 𝐵 ∧ |𝐵 ∩ 𝐶| ≤ 2.

Componentwise relations on arrays

𝐶(𝑎 1 , … , 𝑎 𝑘 ) is a formula specifying componentwise relations. It does so with set interpretations of the form:

𝑆 𝑗 = {𝑖 ∈ 𝐼 | 𝜙 𝑗 (𝑎(𝑖), 𝑐)}

where 𝑎 denotes a tuple of array variables, 𝑐 denotes a tuple of constants from the element theory and 𝜙 𝑗 is a formula of the element theory. As in Definition 2.1, 𝑎(𝑖) denotes the 𝑖-th position of array 𝑎 and 𝑎(𝑖) = (𝑎 1 (𝑖), … , 𝑎 𝑘 (𝑖)).

Example 2.2. The equality between two arrays 𝑎 1 and 𝑎 2 can be written in the fragment of (1) as:

𝑆 = {𝑖 ∈ 𝐼 | 𝑎 1 (𝑖) = 𝑎 2 (𝑖)} ∧ |𝑆| = |𝒰|

where 𝒰 as explained above, represents the universal set 𝐼.

Regular relations on the set of indices

𝑅(𝑆 1 , … , 𝑆 𝑘 ) is a formula specifying regular relations in the set of indices. For instance, the array could be specified by the symbolic regular expression:3

𝜙 1 (𝑒, 𝑐)(𝜙 1 (𝑒, 𝑐) ∨ 𝜙 2 (𝑒, 𝑐)) * 𝜙 3 (𝑒, 𝑐)(2)

This specifies that the first element 𝑒 of the array satisfies the formula 𝜙 1 (𝑒, 𝑐), then there is a sequence of zero or more elements 𝑒 satisfying either 𝜙 1 (𝑒, 𝑐) or 𝜙 2 (𝑒, 𝑐) and the last element 𝑒 satisfies the formula 𝜙 3 (𝑒, 𝑐). Each instantiation of 𝑒 is different for each witness, while the value of the parameters in 𝑐 must be the same for the whole array. However, this approach conflates the specifications of the indices and the specifications of the elements of the arrays.

Let us instead write a symbolic version of the regular expression above

𝑆 1 (𝑆 1 ∨ 𝑆 2 ) * 𝑆 3(3)

To relate this symbolic expression and the theory of the elements, we let 𝑡 be a sequence of bit-strings 𝑡 ∈ ({0, 1} 3 ) * and define

𝑆 1 = {𝑖 ∈ 𝐼 | 𝑡 1 (𝑖) = 1} ∧ 𝑆 1 = {𝑖 ∈ 𝐼 | 𝜙 1 (𝑎(𝑖), 𝑐)} 𝑆 2 = {𝑖 ∈ 𝐼 | 𝑡 2 (𝑖) = 1} ∧ 𝑆 2 = {𝑖 ∈ 𝐼 | 𝜙 2 (𝑎(𝑖), 𝑐)} 𝑆 3 = {𝑖 ∈ 𝐼 | 𝑡 3 (𝑖) = 1} ∧ 𝑆 3 = {𝑖 ∈ 𝐼 | 𝜙 3 (𝑎(𝑖), 𝑐)} (4)

where 𝑡 1 , 𝑡 2 and 𝑡 3 denote, respectively, the first, second and third rows of the sequence and 𝑡 𝑗 (𝑖) denotes the 𝑖-th position in 𝑡 𝑗 .

Then, satisfiability of ( 2) is equivalent to satisfiability of

∃𝑡 ∈ ({0, 1} 3 ) * .𝑡 ⊧ 𝑆 1 (𝑆 1 ∨ 𝑆 2 ) * 𝑆 3 ∧ (4)(5)

where 𝑡 ⊧ 𝑅(𝑆 1 , … , 𝑆 𝑘 ) means that the bit-string sequence 𝑡 satisfies propositionally the regular expression 𝑅(𝑆 1 , … , 𝑆 𝑘 ), that is, there is a word 𝑤 of propositional formulas over the variables 𝑆 1 , 𝑆 2 and 𝑆 3 generated by 𝑅 such that for each 𝑖, 𝑡(𝑖) ⊧ 𝑤(𝑖) propositionally.

Example 2.3. A bit-string sequence 𝑡 belonging to the language of the symbolic regular expression 𝑆 1 (𝑆 1 ∨ 𝑆 2 ) * 𝑆 3 is the following

( 1 1 0 ) ( 1 0 0 ) ( 0 1 0 ) ( 0 1 1 ) ( 0 0 1 )

The values of its rows are respectively 𝑡 1 = 11000, 𝑡 2 = 10110 and 𝑡 3 = 00011.

It satisfies the word of propositional formulas

𝑆 1 (𝑆 1 ∨ 𝑆 2 )(𝑆 1 ∨ 𝑆 2 )(𝑆 1 ∨ 𝑆 2 )𝑆 3 which is generated by 𝑆 1 (𝑆 1 ∨ 𝑆 2 ) * 𝑆 3 .

We call the bit-string sequences 𝑡 regular tables or simply tables and write 𝑇 (𝑅) for the set of all tables satisfying the symbolic regular expression 𝑅.

Encoding of arrays

Let us briefly mention how would the terms of an array theory, most importantly, array "reads" and "writes", be written in the language of generalised powers, while preserving the satisfiability of formulas.

A componentwise specification is written as in Example 2.2. An array read is a functional term 𝑎[𝑗]. To encode this term in generalised powers, we introduce the set variable 𝐽 representing the singleton set {𝑗} and require that |𝐽 | = 1. We then introduce an element theory variable 𝑎 𝑗 and require that {𝑖 ∈ 𝐼 | 𝑎(𝑖) = 𝑎 𝑗 } ⊇ 𝐽.

An array write is a functional term 𝑠𝑡𝑜𝑟𝑒(𝑎, 𝑗, 𝑣). To encode this term in generalised powers, we introduce a new variable 𝑏 to stand for the term 𝑠𝑡𝑜𝑟𝑒(𝑎, 𝑗, 𝑣) and require that {𝑖 ∈ 𝐼 | 𝑏(𝑖) = 𝑣} ⊇ 𝐽 and {𝑖 ∈ 𝐼 | 𝑎(𝑖) = 𝑏(𝑖)} ⊇ 𝒰 ∖ 𝐽.

Example 3.1. Consider the array formula from [5].

𝑖 1 = 𝑗 ∧ 𝑖 1 ≠ 𝑖 2 ∧ 𝑎[𝑗] = 𝑣 1 ∧ 𝑠𝑡𝑜𝑟𝑒(𝑠𝑡𝑜𝑟𝑒(𝑎, 𝑖 1 , 𝑣 1 ), 𝑖 2 , 𝑣 2 )[𝑗] ≠ 𝑎[𝑗]

For each index variable 𝑗, 𝑖 1 , 𝑖 2 , we introduce set variables 𝐽 , 𝐼 1 , 𝐼 2 and impose that 𝐼 1 = 𝐽, 𝐼 1 ≠ 𝐼 2 and

|𝐼 1 | = |𝐼 2 | = |𝐽 |. The term 𝑎[𝑗] = 𝑣 1 is translated into {𝑖 ∈ 𝐼 | 𝑎(𝑖) = 𝑣 1 } ⊇ 𝐽.

We introduce the array variables 𝑏 for 𝑠𝑡𝑜𝑟𝑒(𝑎, 𝑖 1 , 𝑣 1 ) and 𝑐 for 𝑠𝑡𝑜𝑟𝑒(𝑏, 𝑖 2 , 𝑣 2 ). We can then encode the fourth conjunct as {𝑖 ∈ 𝐼 | 𝑐(𝑖) ≠ 𝑎(𝑖)} ⊇ 𝐽. The store operators are encoded as indicated above.

The resulting formula is in the theory of the generalised power and is equisatisfiable to the original.

Deciding generalised powers

Let us now give a method to decide satisfiability of formulas of the form (1). These are of the following form:

𝐹 (𝑆 1 , … , 𝑆 𝑘 ) ∧ ∃𝑡 ∈ 𝑇 (𝑅). 𝑘 ⋀ 𝑖=1 𝑆 𝑖 = { 𝑛 ∈ ℕ | 𝜙 𝑖 (𝑎(𝑛), 𝑐) } = { 𝑛 ∈ ℕ | 𝑡 𝑖 (𝑛) = 1 }(6)

The satisfiability problem requires showing that the following formula is true:

∃𝑎 ∈ 𝒟 * ,𝑡 ∈ 𝑇 (𝑅), 𝑐. 𝐹 (𝑆 1 , … , 𝑆 𝑘 ) ∧ 𝑘 ⋀ 𝑖=1 𝑆 𝑖 = { 𝑛 ∈ ℕ | 𝜙 𝑖 (𝑎(𝑛), 𝑐) } = { 𝑛 ∈ ℕ | 𝑡 𝑖 (𝑛) = 1 } (7)

where 𝒟 is the domain of the array elements.

We show how to compute in polynomial time a formula in the combination of QFBAPA and the existential fragment of the first-order theory of the domain 𝒟 such that Formula ( 7) is equivalent to the computed formula.

Theorem 4.1.

There is a polynomial time algorithm that given formula ( 7) computes an equivalent formula (8) in the combination of QFBAPA and the existential fragment of the first-order theory of 𝒟, 𝑇 ℎ ∃ * (𝒟 ).

Construction of the equivalent formula

The equivalent formula has three parts. The first is an existential prefix shared between both QFBAPA and 𝑇 ℎ

∃ * (𝒟 ) ∃𝑁 ≤ 𝑝(|𝐹 |), ∃𝑠 ∈ [𝑚], 𝜎 ∶ [𝑠] ↪ [𝑚], ∃𝛽 1 , … , 𝛽 𝑁 ∈ {0, 1} 𝑘 .

where where we use the notation that given the list 𝜙 1 , … , 𝜙 𝑘 of formulas specifying the elements in Formula 6 and given a bit-string 𝛽 ∈ {0, 1} 𝑘 , 𝜙 𝛽 ∶= ⋀ 𝑘 𝑖=1 𝜙

𝛽(𝑖)

𝑖 . The third part of the formula is in QFBAPA

𝐻 (𝑐 1 , … , 𝑐 𝑘 , …) ∶=𝜌(𝑐 1 , … , 𝑐 𝑚 ) ∧ 𝐹 (𝑆 1 , … , 𝑆 𝑘 ) ∧ 𝑠 ⋀ 𝑖=1 𝑃 𝑖 ⊆ 𝑝 𝐿 𝜎(𝑖) ∧ 𝑠 ⋀ 𝑖=1 |𝑃 𝑖 | = 𝑐 𝜎 (𝑖) ∧ ∪ 𝑘 𝑖=1 𝑆 𝑖 = ∪ 𝑚 𝑖=1 𝑝 𝐿 𝑖 = ∪ 𝑁 𝑖=1 𝑝 𝛽 𝑖 = ∪ 𝑠 𝑖=1 𝑃 𝑖

where 𝜌 is a formula in the existential fragment of Presburger arithmetic of size linear in the size of the regular expression 𝑅. 𝜌 describes the Parikh image of 𝑅. The description of the Parikh image in terms of linear-size existential Presburger arithmetic formulas is based on a result from [33].

Definition 4.1 (Parikh Image).

The Parikh image of a symbolic regular expression 𝑅 using propositional letters 𝐿 1 , … , 𝐿 𝑚 over the variables 𝑆 1 , … , 𝑆 𝑘 is the set

Parikh(𝑅) = {(|𝑠| 𝐿 1 , … , |𝑠| 𝐿 𝑚 ) | 𝑠 ∈ 𝑀 𝑆 (𝐿

This formula can be computed in polynomial time.

Intuitively, the partition variables 𝑃 𝑖 determine which propositional formula generated each value of the arrays accepted, so that, even if these formulas overlap, a model corresponding to a run of the automaton can be rebuilt. The reason why we need to check the existence of only one witness per elementary Venn region follows from the fact that we can "replicate" this witness in each of the indices that satisfied the corresponding formula 𝜙 𝛽 (see also [30,31]).

Proof of the theorem

We prove that Formula (6) and Formula (13) are equivalent.

⇒) If Formula ( 7) is true, then there are sets 𝑆 1 , … , 𝑆 𝑘 , a finite array 𝑎 and a table 𝑡 ∈ 𝑇 (𝑅) such that

𝐹 (𝑆 1 , … , 𝑆 𝑘 ) ∧ 𝑘 ⋀ 𝑖=1 𝑆 𝑖 = { 𝑛 ∈ ℕ | 𝜙 𝑖 (𝑎(𝑛), 𝑐) } = { 𝑛 ∈ ℕ | 𝑡 𝑖 (𝑛) = 1 }(9)

Let 𝑠 be the symbolic table corresponding to 𝑡, that is, the table made of the propositional formulas generated by 𝑅(𝑆 1 , … , 𝑆 𝑘 ) such that 𝑡 satisfies 𝑠.

𝜌(𝑐 1 , … , 𝑐 𝑚 ) ∧ 𝐹 (𝑆 1 , … , 𝑆 𝑘 ) ∧ 𝑠 ⋀ 𝑖=1 𝑃 𝑖 ⊆ 𝑝 𝐿 𝜎(𝑖) ∧ 𝑠 ⋀ 𝑖=1 |𝑃 𝑖 | = 𝑐 𝜎 (𝑖) ∧ ∪ 𝑘 𝑖=1 𝑆 𝑖 = ∪ 𝑚 𝑖=1 𝑝 𝐿 𝑖 = ∪ 𝑠 𝑖=1 𝑃 𝑖(10)

Formula ( 10) is in QFBAPA. Following the procedure from [25], we eliminate Boolean algebra expressions and the cardinality operator yielding a system of equations of the form

∃𝑘 1 , … , 𝑘 𝑝 .𝐺 ∧ 2 𝑘 −1 ∑ 𝑗=0 ( 𝑏 0 𝛽 𝑗 ⋮ 𝑏 𝑝 𝛽 𝑗 ) ⋅ 𝑙 𝛽 𝑗 = ( 𝑘 1 ⋮ 𝑘 𝑝 ) (11)

where 𝐺 is the existential Presburger arithmetic formula that results from (10) after the elimination and

𝑙 𝛽 𝑗 = |𝑝 𝛽 𝑗 |.

We remove from the sum those terms corresponding to elementary Venn regions 𝛽 such that 𝑙 𝛽 = 0. This includes regions whose associated formula in the interpreted Boolean algebra 𝜙 𝛽 (𝑎, 𝑐) is unsatisfiable, and regions corresponding to bit-strings not occurring in 𝑡. This transformation leaves a reduced set of indices ℛ participating in the sum:

∃𝑘 1 , … , 𝑘 𝑝 .𝐺 ∧ ∑ 𝛽∈{ 𝛽 1 ,…,𝛽 𝑁 }⊆ℛ ( 𝑏 0 𝛽 𝑗 ⋮ 𝑏 𝑝 𝛽 𝑗 ) ⋅ 𝑙 𝛽 𝑗 = ( 𝑘 1 ⋮ 𝑘 𝑝 )(12)

We now give the key auxiliary result from [25] proved in [11].

Definition 4.2. Given a subset 𝑆 ⊆ ℝ 𝑛 , the integer conic hull of 𝑆 is the set

𝑖𝑛𝑡 𝑐𝑜𝑛𝑒 (𝑆) = { 𝑡 ∑ 𝑖=1 𝜆 𝑖 𝑠 𝑖 |𝑡 ≥ 0,( 𝑏 0 𝛽 𝑗 ⋮ 𝑏 𝑝 𝛽 𝑗 ) ⋅ 𝑙 ′ 𝛽 𝑗 = ( 𝑘 1 ⋮ 𝑘 𝑝 )(13)

We can assume that each cardinality variable 𝑙 ′ 𝛽 is non-zero, since otherwise, we can remove it from the sum. With this assumption, 𝑙 ′ 𝛽 1 , … , 𝑙 ′ 𝛽 𝑁 lists the cardinalities of a model of (10) which defines the cardinality of the elementary Venn region 𝑆

′𝛽 1 1 ∩ … ∩ 𝑆 ′𝛽 𝑘

𝑘 to be equal to 𝑙 ′ 𝛽 if 𝛽 ∈ {𝛽 1 , … , 𝛽 𝑁 } and zero otherwise. In particular, we have that the following formula, corresponding to the subformula 𝐻 in (8), holds

𝜌(𝑐 1 , … , 𝑐 𝑚 ) ∧ 𝐹 (𝑆 ′ 1 , … , 𝑆 ′ 𝑘 ) ∧ 𝑘 ⋀ 𝑖=1 𝑃 ′ 𝑖 ⊆ 𝑝 ′ 𝐿 𝜎(𝑖) ∧ 𝑠 ⋀ 𝑖=1 |𝑃 ′ 𝑖 | = 𝑐 𝜎 (𝑖) ∧ ∪ 𝑘 𝑖=1 𝑆 ′ 𝑖 = ∪ 𝑚 𝑖=1 𝑝 ′ 𝐿 𝑖 = ∪ 𝑁 𝑖=1 𝑝 𝛽 𝑖 = ∪ 𝑠 𝑖=1 𝑃 ′ 𝑖(14)

For each 𝛽 ∈ {𝛽 1 , … , 𝛽 𝑁 }, the formula ∃𝑒.𝜙 𝛽 (𝑒, 𝑐) is true, since 𝑙 ′ 𝛽 > 0. Thus, the subformula 𝐶 in ( 8) is also true.

⇐) If Formula (8) is true, then there is a natural number 𝑁 ≤ 𝑝(|𝐹 |) where 𝑝 is a polynomial, 𝑠 ∈ [𝑚], 𝛽 1 , … , 𝛽 𝑁 ∈ {0, 1} 𝑘 , 𝑐 1 , … , 𝑐 𝑚 ∈ ℕ and sets 𝑆 1 , … , 𝑆 𝑘 , 𝑃 1 , … , 𝑃 𝑠 such that ∃𝑐. 𝑁 ⋀ 𝑗=1 ∃𝑒.𝜙 𝛽 𝑗 (𝑒, 𝑐) ∧ 𝜌(𝑐 1 , … , 𝑐 𝑚 ) ∧ 𝐹 (𝑆 1 , … , 𝑆 𝑘 ) ∧ 𝑠 ⋀ 𝑖=1 𝑃 𝑖 ⊆ 𝑝 𝐿 𝜎(𝑖) ∧ ∧ 𝑠 ⋀ 𝑖=1 |𝑃 𝑖 | = 𝑐 𝜎 (𝑖) ∧ ∪ 𝑘 𝑖=1 𝑆 𝑖 = ∪ 𝑚 𝑖=1 𝑝 𝐿 𝑖 = ∪ 𝑠 𝑖=1 𝑃 𝑖 = ∪ 𝑁 𝑖=1 𝑝 𝛽 𝑖(15)

From (15) and the definition of 𝜌, follows that there is a symbolic

𝑆 𝑗 = ∪ {𝑖|𝛽 𝑖 (𝑗)=1} 𝑝 𝛽 𝑖 = { 𝑛 ∈ ℕ | 𝑡 𝑗 (𝑛) = 1 } 𝑆 𝑗 = ∪ {𝑖|𝛽 𝑖 (𝑗)=1} 𝑝 𝛽 𝑖 = { 𝑛 ∈ ℕ | 𝜙 𝑗 (𝑎(𝑛), 𝑐) }

Thus, Formula ( 7) is true.

Computational complexity of the combination

Note that Theorem 4.1 also allows to assert at once the complexity of the underlying logical theory.

The case of trees

One can adapt the techniques of Section 4 to the case when the regular specification is given by a parametric tree automaton, thus extending the results of [18]. The main difference with the procedure of Section 4 is that in the case of parametric tree automata one needs to compute the Parikh image of a regular tree language. This is done in a completely analogous way as it is done in Definition 4.1 for parametric finite automata. Note that it is easy to convert from non-deterministic top-down to non-deterministic bottom-up tree automata [8, Theorem 1.6.1]. One can then use the observation of Klaedtke and Rueß [22,Lemma 17] which allows to reduce the problem to the computation of the Parikh image of a context-free grammar. Finally, [36] says that the Parikh image of a context-free grammar can be described by a linear-sized existential Presburger arithmetic formula.

Conclusion

We have shown how to extend decision procedures for satisfiability of parametric array fragments with regular constraints. In terms of quantifiers, this shows how to simultaneously support Härtig's quantifiers and WS1S second-order quantification. Our techniques extend previous results of Alberti, Ghilardi and Pagani [1] since the relations expressible in WS1S extend those expressible in Presburger arithmetic. They also extend recent results in the literature [18], which did not handle the cardinality operator.

Our work mixes ideas from decision algorithms for three different logical theories: quantifier-free BAPA [25], combinations of BAPA with WS1S and WS2S [37] and existential fragment of power structures [30]. However, a crucial technical difficulty has been overcome to make the combination work. This difficulty stems from the fact that while Büchi's automata are over finite alphabets, the corresponding automata (or equivalently, regular expressions) that appear in the Feferman-Vaught framework use first-order formulas in their transitions, since set variables are interpreted. We demonstrated, as our colleagues [18], that one can still use the Parikh image of this symbolic automata to combine theories. Since one is now counting formulas rather than symbols from a finite alphabet, and formulas can overlap in the semantic domain, it becomes necessary to indicate to the QFBAPA constraint which transition of the automaton produced each index. We achieved this by introducing a partition of the sets of indices of the array, where each part corresponds to the indices generated by a given transition.

The implementation of the algorithm could be achieved mixing the techniques of ARCA-SAT [1] with software computing the Parikh image of regular expressions and context-free grammars. For the latter, there exist several implementations, we mention for instance [19], where a fix to the construction original of Verma et alii [36], is also described.

Possible applications of the decision procedure include automatic verification of array manipulating programs in deductive verification systems and model checking of distributed protocols. Nevertheless, due to the number of ideas that are combined in this work, we would not be surprised if further applications are found in the future.