The (extensional) theory of arrays is widely used to model systems. Hence, e cient decision procedures are needed to model check such systems. Current decision procedures for the theory of arrays saturate the read-over-write and extensionality axioms originally proposed by McCarthy. Various lters are used to limit the number of axiom instantiations while preserving completeness. We present an algorithm that lazily instantiates lemmas based on weak equivalence classes. These lemmas are easier to interpolate as they only contain existing terms. We formally de ne weak equivalence and show correctness of the resulting decision procedure.
This work is supported by the German Research Council (DFG) as part of the Transregional Collaborative
Research Center \Automatic Veri cation and Analysis of Complex Systems" (SFB/TR14 AVACS)
Related Work Since the proposal of the theory of arrays by McCarthy [
Armando et al. [
Bruttomesso et al. [
A decision procedure for the theory of arrays based on instantiating McCarthy's axioms is
given by de Moura et al. [
Closest to our work is the decision procedure published by Brummayer et al. [
A rst order theory consists of a signature and a set of models M. We assume the equality symbol = with its usual interpretation is part of any signature. Every model contains for every sort interpreted by this model a non-empty domain and a mapping from constant or function symbol into the corresponding domain. A theory T is stably in nite if and only if every satis able quanti er-free formula is satis ed in a model of T with an in nite universe.
The theory of arrays TA is parameterised by an index theory TI and an element theory TE .
The signature of TA consists of the two functions [ ] and h i. Every model of the theory of
arrays satis es the select-over-store-axioms proposed by McCarthy [
8a i v: ahi 8a i j v: i 6= j =) ahi vi[i] = v vi[j] = a[j]
(idx) (read-over-write) Additionally we consider the extensional variant of the theory of arrays. Then, every model has to satisfy the extensionality axiom: (ext)
We use a; b to denote array-valued variables, i; j; k to denote index variables, and v; w to denote element variables. Additionally we use subscripts to distinguish di erent variables. We use P to denote a path in a graph. A path in a graph is interpreted as a sequence of edges.
In the remainder of this paper, we consider quanti er-free TA-formulae. Furthermore we x the index TI to a stably in nite theory and the element theory TE to a theory that contains at least two di erent values1. 3
Multiple theories are usually combined with a variant of the Nelson{Oppen combination
procedure [
The procedure rst transforms the input such that every literal is pure with respect to the theories. Let f (t) be a term in the input. If f is interpreted by theory T1 and t is interpreted by theory T2, then f (t) is not pure. The rst step of the Nelson{Oppen procedure then generates a fresh variable v, rewrites f (t) into f (v), and adds the de nition v = t as a new conjunct to the formula. The fresh variable is shared between theories T1 and T2. This step is repeated until all terms are pure. By abuse of notation, we name the shared variable after its de ning term t, e. g., we use a[i] to denote the shared variable that is de ned as a[i].
Let V be the set of fresh variables introduced in the rst step of the combination procedure. The second step of the procedure tries to nd an arrangement of V , i. e., an equivalence relation between variables in V such that T1 and T2 produce partial models that agree with this equivalence relation. Finding such an arrangement is typically done by propagating equalities or providing case split lemmas. In the following, we call this arrangement strong equivalence to distinguish it from weak equivalence de ned in the next section. We write a b to denote that a and b are strongly equivalent, i.e., that in the current arrangement the shared variables a and b are equal.
For the theory of arrays, we consider every term of the form h i or [ ] as being interpreted by the array theory. We consider all array terms, store, and select terms to be shared and thus they have to occur in the arrangement. Furthermore, every index term that appears in a store or select is considered shared between the array theory and the index theory. Then the goal is to nd a suitable arrangement to these shared terms such that all theories agree on this arrangement.
For an array solver to be used in Nelson{Oppen combination we have to propagate equalities between shared array terms and shared select terms. Furthermore, the other theories have to propagate equalities between terms used as index in a select or store. In the remainder of this paper we will rst show how to propagate equalities between select terms and afterwards deal with extensionality to propagate equalities between array-valued terms. 4
The theory of arrays has two constructors for arrays: array variables, and store terms h i. Assuming quanti er-free input, we can only constrain the values of a nite number of indices.
1Note that TA is stably in nite under these conditions.
These constraints can either be explicity like a[i] = v, or implicit like ahi vi where axiom (idx) produces the corresponding ahi vi[i] = v. Hence, for quanti er-free input, arrays that are connected via a sequence of h i can only di er in nitely many positions. We call such arrays weakly equivalent. In this section we formally de ne weak equality and show how to exploit this to produce a decision procedure for the (extensional) theory of arrays.
Let S be the set of all terms of the form h i in the input formula and A be the set of all array-valued terms that are not in S. Since ahi vi modi es a only at index i, these two arrays are guaranteed to be equal on all indices except on index i. We generalise this observation to chains of the form : : : hj wihi vi to extract a set of indices for which two arrays might store di erent values.
De nition 1 (weak equivalence). A weak equivalence graph GW contains vertices S [ A and undirected edges de ned as follows: 1. a $ b if a
b, and 2. a $i b if a has form bhi
(P ) We write a , b if there exists a path P between nodes a and b in GW . In this case, we call a and b weakly equal. The weak equivalence class containing all elements that are weakly equal (P ) to a is de ned as WeakEQ(a) := fb j 9P: a , bg.
For a path P we de ne Stores (P ) as the set of all indices corresponding to edges of the form $, i. e., Stores (P ) := fi j 9a b: a $i b 2 P g.
Example 1. Consider the formula a = bhj vi ^ b = chi wi ^ d = e ^ c[i] = w. The weak equivalence graph for this example is shown in Figure 1. Note that the last conjunct is not important for the construction of the weak equivalence graph.
a bhj vi j b d chi
wi e
i c
We get two di erent weak equivalence classes. The rst one contains the nodes a, bhj vi, b, chi wi, and c. The second contains d and e. Note that d and e are actually strongly equivalent. Thus, they store the same value at every position. Let P denote the path from a to c in the weak equivalence graph. Then, Stores (P ) = fi; jg. Thus, arrays a and c can only di er in at most the values stored at the indices i and j. (P )
If we want to know if a[i] and b[i] should be equal, we check if a , b for a path P such that i 62 Stores (P ). If this is the case, P witnesses the equivalence between the select terms. De nition 2 (weak equivalence modulo i). Two arrays a and b are weakly equivalent modulo i if and only if they are weakly equivalent and connected by a path that does not contain an edge of the form $j where j i. We denote weak equivalence modulo i by a i b and de ne it as a i b := 9P: a (,P) b ^ 8j 2 Stores (P ) : j 6 i.
Using this de nition we can propagate equalities between shared selects if the arrays are weakly equivalent modulo the index of the select.
and b[j] be two selects such that i
be an arrangement satisfying the array axioms. Let a[i] j and a i b. Then, a[i] b[j] holds.
Proof. We induct over the length of the path P witnessing a i b.
Base case. In this case, a and b are the same term. Hence a[i] b[j] holds by congruence.
Step case. Let the step from c to b be the last step of path P . By induction hypothesis we know that a[i] c[j] holds.
If the edge between c and b is due to a strong equivalence (i. e., c b), then c[j] b[j] follows from congruence.
If the edge between c and b is of the form c $k b, then either c is bhk i or b is chk both cases, we get the lemma j = k _ c[j] = b[j] from axiom (read-over-write). Since j i 6 k, we get j 6 k and thus c[j] b[j]. We conclude a[i] b[j] by transitivity. i. In i and
This lemma allows us to propagate equalities between shared selects. Note that it depends upon disequalities between index terms needed to ensure a i b.
If two arrays are weak equivalent modulo i they store the same value at the index i. The reverse is not necessarily true. Therefore, we de ne a weaker relation weak congruence modulo i. De nition 3 (weak congruence modulo i). Arrays a and b are weak congruent modulo i if and only if they are guaranteed to store the same value at index i. We denote weak congruence modulo i by i and de ne a i b := a i b_9a0 b0 j k: a i a0^i j^a0[j] b0[k]^k i^b0 i b.
We use weak congruences to decide extensionality. Intuitively, if for all indices i the weak congruence modulo i a i b holds, then a = b should be propagated. But this nave approach requires checking every index occurring in the formula. To minimise the number of indices we need to consider, we exploit the weak equivalence graph.
Lemma 2 (weakeq-ext). Let
(P ) two arrays such that a , b holds. If for all indices i 2 Stores (P ) we have a holds.
be an arrangement satisfying the array axioms. Let a and b be i b, then a b
5
Our decision procedure is based on weak equivalences and the Nelson{Oppen combination scheme. It propagates equalities between terms shared by multiple theories. We limit the propagation to shared array terms and array select terms.
The TA-formulae are preprocessed as follows. For every ahi vi contained in the input, we (1) instantiate the axiom (idx) and (2) add a[i] to the set of terms contained in the input2. Thus, the preprocessing step adds at most two select operations for every store.
We propagate new equalities from weak equivalence relations and weak congruence relations based on lemmas 1 and 2. These relations depend on the arrangement , which represents logical equality (=). We now de ne a function Cond( ) that computes a condition (a conjunction of equalities and inequalities) under which a weak equivalence or weak congruence holds. To 2This can be achieved by adding the equality a[i] = a[i]. denote the condition for a path that does not contain an edge labelled with index i we use Condi( ). For an edge in the weak equivalence graph that represents an equality, the condition re ects this equality. For an edge that comes from a hj i, no condition is needed. However, Condi( ) should ensure that i does not occur on the path, so i 6= j needs to hold.
Cond(a $ b) := a = b Cond(a $j b) := true
Condi(a $ b) := a = b Condi(a $j b) := i 6= j We can extend these de nitions to paths by conjoining the conditions for all edges on that path. Then, we can compute Cond(a i b) using the path that witnesses a i b.
Cond(a i b) := Condi(P ) where a (,P) b ^ 8j 2 Stores (P ) : i 6 j Finally, to de ne Cond(a i b), we use the de nition of i.
8Cond(a i b) > Cond(a i b) := < Cond(a i a0) ^ i = j ^ a0[j] = b0[k] > : ^ k = i ^ Cond(b0 i b) if a i b if a i a0 ^ i
j ^ a0[j] ^ k i ^ b0 i b b0[k] Example 2. Consider again the formula a = bhj vi ^ b = chi wi ^ d = e ^ c[i] = w from Example 1 whose weak equivalence graph is shown in Figure 1. Assume i 6 j. Then we have a i chi wi since no edge contains a label that is equivalent to i. We get Cond(a i chi wi) a = bhj vi ^ i 6= j ^ b = chi wi.
From Axiom (idx) we get chi wi[i] = w. With c[i] = w we conclude a i c since a i chi wi and chi wi[i] = c[i]. We have Cond(a i c) Cond(a i chi wi) ^ chi wi[i] = c[i].
To decide the theory of arrays we de ne two rules to generate instances of array lemmas. We present the rules as inference rules. The rule is applicable if the current arrangement on the shared variables V satis es the conditions above the line. The rule then generates a new (valid) lemma that can propagate an equality under the current arrangement.
The rst rule is based on Lemma 1. Two select terms are equivalent if the indices of the selects are congruent and the arrays are weakly equivalent modulo that index. We only create this lemma if the select terms existed in the formula. Note that we create for select terms in the formula a shared variable with the same name in V .
a i b i j
a[i]; b[j] 2 V i 6= j _ : Cond(a i b) _ a[i] = b[j] (read-over-weakeq)
The next rule is based on Lemma 2 and used to propagate an equality between two extensionally equal array terms. Two arrays a and b have to be equal if there is a path P such that a (,P) b and for all i 2 Stores (P ), a i b holds.
a (,P) b : Cond(P ) _ 8i 2 Stores (P ) : a i b _
a; b 2 V : Cond(a i b) _ a = b i2Stores(P ) (weakeq-ext)
The resulting decision procedure is sound and complete for the existential theory of arrays
assuming sound and complete decision procedures for the index and element theories.
Lemma 3 (soundness). Rules (read-over-weakeq) and (weakeq-ext) are sound.
Proof. Soundness of the rules follows directly from the lemma with the corresponding name.
Lemma 4 (completeness). The rules (read-over-weakeq) and (weakeq-ext) are complete.
The proof of this lemma can be found in the extended version of this paper [
The preprocessor is the only component of our decision procedure that produces new select terms and thus might trigger new lemmas. These lemmas only generate new (dis-)equality literals between existing terms. Thus, reducing the number of select terms might reduce the number of lemmas generated by our decision procedure and speed up the procedure.
If the element theory is stably in nite we can omit the preprocessor step that adds for every ahi vi the select a[i]. Instead, we simply assume a[i] to be di erent than any other b[i] unless a b. This method preserves soundness and completeness.
Lemma 5. (soundness of modi ed procedure) The modi ed procedure is sound. Proof. Follows directly from Lemma 3 since it does not rely on the addition of a[i] for every ahi i.
For the completeness lemma we take into account the fact that the element theory is stably
in nite. Thus, if a[i] is not present we use a fresh element in the value domain.
Lemma 6 (completeness of modi ed procedure). The modi ed procedure is complete.
The proof of this lemma can be found in the extended version of this paper [
This optimisation enables us to limit the number of additional terms in the input. Since
we only need to generate (read-over-weakeq) lemmas if the select terms in the conclusion are
present after preprocessing, this optimisation also reduces the number of lemmas. Furthermore,
it is widely applicable. In fact, the non-bitvector logics de ned in the SMTLIB [
We implemented the decision procedure described in this paper in our SMT solver
SMTInterpol [
We represent the weak equivalence relation and the weak equivalence modulo i relations in a
forest structure, similarly to the representation of equivalence graph in congruence solvers [
We have to distinguish between strong equivalence, weak equivalence, and weak equivalence modulo i. The strong equivalence classes are already handled by the equality solver. In our implementation of the array solver we treat them as indivisible and create a single node for every strong equivalence class. To represent the weak equivalence relations the nodes have up to two outgoing edges, a primary p and a secondary s, see Figure 2. The edges come from a store operation and correspond to the edges $i in the weak equivalence graph. The index of the primary edge is stored in the pi eld. The primary edge points towards the representative struct node p : node pi : index s : node get-rep(n : node) if n:p = nil then n else get-rep(n:p) make-rep(n : node) if n:p 6= nil then make-rep(n:p) nnn:::ppp::pp:=i:=:n=inln:pi=;9 iendvgeert primary make-repi(n) get-repi(n : node; i : index) if n:p = nil then n elseif n:pi 6= i then get-repi(n:p; i) elseif n:s = nil then n else get-repi(n:s; i) make-repi(n : node) if n:s 6= nil then if n:s:pi 6= n:pi then n:s := n:s:p rmeopvreesetnotwaatirvdes make-repi(n) else make-repi(n:s) n:s:s := n:s invert n:s := nil secondary edge of the weak equivalence class. Every primary edge p connects the node representing (the strong equivalence class of) a store ahj vi with the node representing a and the corresponding index in the pi eld is j. Note, however, that the direction of the edge can be arbitrary, as we invert the edges during the execution of the algorithm. If the primary edge is missing the node is the representative of its weak equivalence class and of all its weak equivalence modulo i classes.
While the primary edge is enough to represent the weak equivalence relation we need another edge to represent weak equivalence modulo i. The representative of weak equivalence modulo i is also found by following the primary edges. However, if the store of the primary edge is on the index i, the secondary edge is followed instead. If the secondary edge is missing the node is the representative of its weak equivalence modulo i class.
The equivalence classes are represented as follows. Two arrays a and b are weakly equivalent i get-rep(a) = get-rep(b) and a i b i get-repi(a; i) = get-repi(b; i).
The algorithm proceeds by inserting the store edges one by one, similarly to the algorithm
presented in [
return if a:pi 2= S ^ get-repi(a; a:pi) 6= b then make-repi(a) a:s := b add-secondary(S [ fa:pig; a:p; b) else make-rep(b) if get-rep(a) = b then add-secondary(fig; a; b) b:p := a b:pi := i can be inserted as a new primary edge.
If the nodes are already weakly equivalent the procedure add-secondary is called. This procedure follows the path from the other array a to the array b that was made the representative. For every node on this path it checks if a secondary edge needs to be added. If the primary edge of the node is labelled with a store on i, the algorithm rst checks if the node is weakly equivalent modulo i with b due to the new store edge. This is the case if no store on i occurred on the path so far and the new store is also on an index di erent from i. We use the set S to collect these forbidden indices. Then if b is not already the representative of the weak equivalence modulo i class, the outgoing secondary edges are reversed and a new secondary edge is added.
The complexity of the procedure add-store is worst case quadratic in the size of the weak equivalence class. This stems from make-repi being linear in the size and being called a linear number of times. The overall complexity is cubic in the number of stores in the input formula. The space requirement, however, is only linear. In our current implementation in SMTInterpol this procedure was not a bottleneck so far. In SMTInterpol we also keep the stores that created the primary and secondary edge in the data-structure. This allows for computing the paths needed for lemma generation in linear time.
Example 3. Figure 4 shows an example of the data structure where the primary edges are labelled by the index of the corresponding store. This data structure represents only one weak equivalence class with the representative node 0. The resulting data structure after adding a store with index k between nodes 0 and 4 is shown on the right. Since nodes 0 and 4 were already in the same weak equivalence class, secondary edges were added.
These secondary edges are needed to connect the weak equivalence modulo i and modulo j classes. Figure 5(a) shows how the rst secondary edge connects the two weak equivalence modulo i classes rooted at nodes 0 resp. 3. This is necessary since there is now a new path using the edge from 4 to 0. Note that no secondary edge is added to node 1, since nodes 1, 2, and 5 are still not weakly equivalent modulo i to the other nodes. Figure 5(b) shows the connection between the two weak equivalence modulo j classes rooted at nodes 0 resp. 2. The weak equivalence modulo j class rooted at node 6 is not a ected by a new edge between nodes 0 and 4 since these nodes are on a di erent path.
We implemented this decision procedure in our SMT solver SMTInterpol [
We presented a new decision procedure for the extensional theory of arrays. This procedure
exploits weak equalities to limit the number of axiom instantiations. The instantiations produced
by the decision procedure presented in this paper can be restricted to terms already present
in the input formula. Furthermore we discussed an implementation based on a graph
structure similar to congruence closure graphs. This decision procedure is implemented in our SMT
solver SMTInterpol [