Parametric array theories are extensions of the quantifier-free theory of arrays with relations that hold componentwise. Unlike more expressive theories of arrays they allow specifying linear cardinality constraints on interpreted sets of indices, a notion close to the Härtig quantifier from model theory. We apply the notion of generalised power of a structure to study the satisfiability problem of parametric array theories. We show that reasoning about component-wise relations, linear cardinality constraints and succinct regular relations can be done eficiently by reduction to propositional satisfiability. We indicate how our techniques can be adapted to theories of trees.
CEUR
ceur-ws.org 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 ofer 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
2We 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.
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 diferent set interpretations for indices
and elements. We will use relations of the following form:
( 1, … , ) ∧ ( 1, … , ) ∧ ( 1, … , )
(
Formulas , and in (
( 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 | … Example 2.1. An example of QFBAPA formula is || > 1 ∧ ⊆ ∧ | ∩ | ≤ 2 2.3. 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 (
be specified by the symbolic regular expression: 3
( 1, … , )is a formula specifying regular relations in the set of indices. For instance, the array could
1(, )( 1(, ) ∨ 2(, ))∗ 3(, )
(
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 diferent 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.
To relate this symbolic expression and the theory of the elements, we let be a sequence of bit-strings
∈ ({0, 1}3)∗ and define
(
∃ ∈ ({0, 1}3)∗. ⊧ 1( 1 ∨ 2) 3 ∧ (
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 0 0
(
0 0 0 1 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 .
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.
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 { ∈ ∣ () = ()} ⊇ ∖ .
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.
Let us now give a method to decide satisfiability of formulas of the form (
⋀ = { ∈ ℕ | ((), ) } = { ∈ ℕ | () = 1 } The satisfiability problem requires showing that the following formula is true: ∃ ∈ ∗, ∈ (), .
( 1, … , ) ∧⋀ = { ∈ ℕ ∣ ((), ) } = { ∈ ℕ ∣ () = 1 }
(
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 (
Theorem 4.1. There is a polynomial time algorithm that given formula (
QFBAPA ∃ ≤ (| |), ∃ ∈ [], ∶ [] ↪ [], ∃ 1, … , ∈ {0, 1} . where is a natural number, is a polynomial, | | is the number of symbols used to write , [] ∶= { 1, … , } abbreviates the set of the first natural numbers, is the number of propositional formulas used in , is an injection from [] to []
and is the number of set variables used in .
The second part of the formula is an expression in the theory ℎ ∃∗( ) ( 1, … , ) ∶= ∃.
⋀ ∃ ∈ .
(, ) and given a bit-string ∈ {0, 1} , ∶= ⋀=1
The third part of the formula is in QFBAPA
() . where we use the notation that given the list 1, … , of formulas specifying the elements in Formula 6 ( 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). variables 1, … , is the set The Parikh image of a symbolic regular expression using propositional letters 1, … , over the
Parikh() = {(|| 1, … , || ) ∣ ∈ ( 1, … , )}
table .
where is a word of propositional formulas and || is the number of occurrences of in the symbolic
∗
Example 4.1. Continuing Example 2.3, we had a symbolic regular expression 1( 1 ∨ 2) 3 and a word
of propositional formulas 1( 1 ∨ 2)(1 ∨ 2)(1 ∨ 2) 3. Thus, one vector in the Parikh image is (
Continuing with the description of the third part of the formula, is the QFBAPA term in Formula 6, ∶= ∩=1 ()
where ∈ {0, 1} , ∶= ∪⊧ where ⊧ is the propositional satisfaction relation and ∈ {0, 1} , | ⋅ | denotes the cardinality of the argument set expression, ∪̇∈ is the set ∪∈ where we emphasize that each pair of sets , are disjoint.
∃ ≤ (| |), ∃ ∈ [], ∶ [] ↪ [], ∃ ∈ {0, 1} .( ) ∧ ∃ , . ( , , )
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]).
(
We prove that Formula (
⇒)If Formula (
Define ∶= || for ∈ {1, … , }
as the number of occurrences of in the symbolic table , = | { | ≠ 0 }|, mapping the indices in [] to the indices of the terms for which is non-zero and }. From the equalities = { ∈ ℕ | () = 1 } = { ∈ ℕ | ((), ) } in (9), ( 1, … , ) ∧ ( 1, … , ) ∧⋀ ⊆ () ∧ =1
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 2 −1 J 0K ∑ (
⋮ =0
J K 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,
Definition 4.2.
Given a subset ⊆ ℝ , the integer conic hull of is the set =1
() = { ∑ | ≥ 0, ∈ , ∈ ℕ} Theorem 4.2. Let ⊆ ℤ be a finite set of integer vectors, ∈ ( ) and = maxx∈ ‖x‖∞ = maxx∈ max{| 1|, … , | |} where || denotes the absolute value of the number . There exists a subset ⊆ such that ∈ ( ′)and | ′| ≤ 2 log2(4 ) where | ′| denotes the cardinality of the set cardinalities 1, … , ′
′ such that: Using Theorem 4.2, there is a polynomial family of Venn regions 1, … , and corresponding We can assume that each cardinality variable ′ is non-zero, since otherwise, we can remove it from the sum. With this assumption, 1, … , ′
′
cardinality of the elementary Venn region 1
lists the cardinalities of a model of (10) which defines the
′ 1
∩ … ∩
′ to be equal to ′ if ∈ { 1, … , } and zero
otherwise. In particular, we have that the following formula, corresponding to the subformula in (
From (15) and the definition of , follows that there is a symbolic table generated by the symbolic regular expression such that || = for each ∈ { 1, … , } occurring in . Moreover, from ′
′ ( 1, … , ) ∧ ( 1, … , ) ∧⋀ ⊆ () ∧ ′
′ =1
′ (, ) ∧ ( 1, … , ) ∧ ( 1, … , ) ∧⋀ ⊆ () ∧ ∧ ⋀ | | = ()
∧ ∪=1 = ∪=1 = ∪̇=1 = ∪=1 also true.
⇐)If Formula (
For each ∈ { 1, … , }, the formula ∃.
(, ) is true, since ′ > 0. Thus, the subformula in (
where is a polynomial, ∈ [] , =1 =1 ⋀ ⊆ ()
∧ ∪=1 = ∪̇=1
From the subformula
we have that all the sets are empty except (
∪=1 = ∪̇=1 ∧ ⋀ ⊆ () ∧ ⋀ | | = () =1 =1 follows that we may define to consist of the indices of labelled with the formula () for each ∈ {1, … , } . This is because the values in are guaranteed to satisfy the formula () . Note that the values in could satisfy other formulas () . However, the role of the variables is to determine which formula of the regular expression generated the values satisfying () regardless of whether the witnesses satisfied other formulas too.
From the subformula ∃.
Observe that ( 1, … , )holds by assumption. Moreover, all the elements in belong to a single set . it follows that there exist values 1, … , satisfying the formulas 1(, ), … , (, ) and moreover, we build an array by substituting in the indices in by the values such that ⊆ .
We define a table by substituting in the indices in by the values such that ⊆ . Similarly, = ∪{∣ ()=1} = { ∈ ℕ ∣ () = 1 } = ∪{∣ ()=1} = { ∈ ℕ ∣ ((), ) }
Note that Theorem 4.1 also allows to assert at once the complexity of the underlying logical theory. If =
P then the satisfiability problem of formulas of the form (
satisfiability problem of formulas of the form (
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 diference 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.
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.
BAPA [25], combinations of BAPA with WS1S and WS2S [37] and existential fragment of power structures [30]. However, a crucial technical dificulty has been overcome to make the combination work.
ing automata (or equivalently, regular expressions) that appear in the Feferman-Vaught framework use ifrst-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.
The author wishes to express his gratitude to Viktor Kunčak for suggesting us the application of the methods of our thesis to symbolic automata. Anthony Lin and Oliver Markgraf provided useful remarks on the final presentation of the results in this paper. Research supported by the Swiss NSF Project P500PT_222338 [9] Przemysław Daca, Thomas A. Henzinger, and Andrey Kupriyanov. Array Folds Logic. In Computer
International Publishing. doi:10.1007/978-3-319-41540-6_13. [10] Leonardo de Moura and Nikolaj Bjorner. Generalized, eficient array decision procedures. In 2009 Formal Methods in Computer-Aided Design, pages 45–52, Austin, TX, November 2009. IEEE. doi:10.1109/FMCAD.2009.5351142. [11] Friedrich Eisenbrand and Gennady Shmonin. Carathéodory bounds for integer cones. Operations
Research Letters, 34(
Mathematicae, 47(
1609/aaai.v35i7.16785. [14] Klaus Freiherr von Gleissenthall. Cardinalities in Software Verification . PhD thesis, Technische
Universität München, Fakultät für Informatik, 2016. [15] Alessandro Gianola. Verification of Data-Aware Processes via Satisfiability Modulo Theories , volume 470 of Lecture Notes in Business Information Processing. Springer Nature Switzerland, Cham, 2023. doi:10.1007/978-3-031-42746-6. [16] Klaus v. Gleissenthall, Nikolaj Bjørner, and Andrey Rybalchenko. Cardinalities and universal quantifiers for verifying parameterized systems. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’16, pages 599–613, New York, NY,
[17] Arie Gurfinkel, Sharon Shoham, and Yuri Meshman. SMT-based verification of parameterized systems. In Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering , FSE 2016, pages 338–348, New York, NY, USA, November 2016. Association for Computing Machinery. URL: https://dl.acm.org/doi/10.1145/2950290.2950330, doi:10.1145/ 2950290.2950330. [18] Matthew Hague, Artur Jeż, and Anthony W. Lin. Parikh’s Theorem Made Symbolic. Proceedings of the ACM on Programming Languages, 8(POPL):65:1945–65:1977, January 2024. URL: https: //dl.acm.org/doi/10.1145/3632907, doi:10.1145/3632907. [19] Matthew Hague and Anthony Widjaja Lin. Synchronisation- and Reversal-Bounded Analysis of
Springer. doi:10.1007/978-3-642-31424-7_22. [20] Chih-Duo Hong and Anthony W. Lin. Regular Abstractions for Array Systems. Proceedings of the
1145/3632864, doi:10.1145/3632864. [21] James Cornelius King. A program verifier . PhD thesis, Carnegie-Mellon University, Pittsburgh
citations/AD0699248. [22] Felix Klaedtke and Harald Rueß. Parikh Automata and Monadic Second-Order Logics with Linear
2002. [23] Daniel Kroening and Ofer Strichman. Decision Procedures. Texts in Theoretical Computer Science.
An EATCS Series. Springer Berlin Heidelberg, Berlin, Heidelberg, 2 edition, 2016. doi:10.1007/
978-3-662-50497-0.
[24] Viktor Kunčak, Huu Hai Nguyen, and Martin Rinard. Deciding Boolean Algebra with
Presburger Arithmetic. Journal of Automated Reasoning, 36(