Existing techniques for Craig interpolation for the quanti er-free fragment of the theory of arrays require a special solver. The solver needs to know in advance the partitioning (A; B) of the interpolation problem and needs to avoid creating AB-mixed terms to be suitable for interpolation. This limits the e ciency of these solvers especially when computing sequence and tree interpolants. We present a new approach using Proof Tree Preserving Interpolation and an array solver based on Weak Equivalence on Arrays. We give an interpolation algorithm for the lemmas produced by the array solver.
Equality interpolating theories [
The algorithm of Yorsh and Musuvathi [
Totla and Wies [
The last two techniques require to know the partitions at solving time. Thus, when
computing sequence interpolants or tree interpolants, they would require either an adapted
interpolation procedure or the solver has to run multiple times. In contrast, our method can be
easily extended to tree interpolation [
We assume standard rst order logic. A theory T is given by a signature and a set of axioms.
The theory of arrays TA is parameterized by an index theory and an element theory. The
signature A of TA contains the select (or read ) function [ ] and the store (or write) function
h i. In the following, a; b; s; t will denote array terms, i; j; k index terms and v; w element
terms. For an array a, index i and element v, a[i] returns the element stored in a at i, and
ahi vi returns a copy of a where the element at index i is replaced by the element v, leaving
a unchanged. The functions are de ned by the following 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)
We consider the variant of the extensional theory of arrays proposed by Bruttomesso et al. [
An interpolation problem (A; B) is a pair of formulas where A ^ B is unsatis able. A Craig interpolant for (A; B) is a formula I such that (i) A implies I, (ii) I and B are unsatis able and (iii) I contains only symbols shared between A and B. Given an interpolation problem (A; B), the symbols shared between A and B are called shared, symbols only occuring in A are called A-local and symbols only occuring in B, B-local. A literal, e.g. a = b, that contains A-local and B-local symbols is called mixed. 3 3.1
Proof Tree Preserving Interpolation
In this section we give a short overview of the proof tree preserving interpolation framework
presented by Christ et al. [
The core idea of proof tree preserving interpolation is a scheme to handle mixed equalities a = b where a is A-local and b is B-local. For these a fresh variable xab is introduced and the projections are de ned as follows.
(a = b) A : (a = xab)
(a = b) B : (xab = b)
Thus, a = b is equivalent to 9xab:(a = b) A ^ (a = b) B and xab is a new shared variable
that may occur in interpolants. For disequalities we follow [
EQ(xab; a) (a 6= b) B : : EQ(xab; b) : For an interpolation problem (A^(:C) A; B ^(:C) B) where :C contains a 6= b we require as additional symbol condition that the interpolant has the form I[EQ(xab; s1)] : : : [EQ(xab; sn)]1, where s1; : : : ; sn are shared terms and each EQ term occurs positively in I. For a resolution step on the pivot literal a = b the following interpolation rule combines the partial interpolants of the input clauses to a partial interpolant of the resolvent.
C1 _ a = b : I1[EQ(xab; s1)] : : : [EQ(xab; sn)]
C2 _ a 6= b : I2(xab)
C1 _ C2 : I1[I2(s1)] : : : [I2(sn)]
1One can show that such an interpolant exists for every equality interpolating theory in the sense of De
nition 4.1 in [
Weakly Equivalent Arrays
In this section, we revisit the de nitions and results about weakly equivalent arrays that are
used in the decision procedure for the theory of arrays presented by Christ and Hoenicke [
For a formula F , let V be the set of terms that contains the array terms in F and in addition the select terms a[i] and their indices i and for every store term ahi vi in F the terms i, v, a[i] and ahi vi[i]. Let be the equivalence relation on V representing equality. The weak equivalence graph GW is de ned by its vertices, the array-valued terms in V , and its undirected edges of the form (i) s1 $ s2 if s1 s2 and (ii) s1 $i s2 if s1 has the form s2hi i or vice versa. If two arrays a and b are connected in GW by a path P they are called weakly equivalent. We write a ,P b. Weakly equivalent arrays can di er only at nitely many positions given by Stores (P ) := fi j 9s1 s2: s1 $i s2 2 P g. Two arrays a and b are called weakly equivalent on i, denoted by a i b, if there exists a path P between them such that k 6 i holds for every k 2 Stores (P ). If a and b are weakly equivalent on i, they must store the same value at i. Two arrays a and b are called weakly congruent on i, a i b, if the equality a0[j] = b0[k] holds for j k i and a0 i a, b0 i b. Also in this case they must store the same value at i.
We use Cond(a ,P b); Cond(a i b); Cond(a i b) to denote the conjunction of the literals v = v0 (resp. v 6= v0), v; v0 2 V , such that v v0 (resp. v 6 v0) is necessary to show the corresponding property. Instances of array lemmas are generated according to the following rules: i j a
i b i 6= j _ : Cond(a a ,P b : Cond(a ,P b) _ 8i 2 Stores (P ) : a i b
_ : Cond(a i2Stores(P )
a; b 2 V i b) _ a = b (read-over-weakeq) (weakeq-ext) The rst rule, based on (read-over-write), propagates equalities between select terms and the second, based on extensionality, propagates equalities on array terms. In the following, we will describe how we can derive partial interpolants for these array lemmas. 4
Interpolants for Read-Over-Weakeq Lemmas In this section, we show how to interpolate lemmas generated by (read-over-weakeq). A lemma of this type (see Figure 1) explains a con ict of the form i = j ^ Cond(a i b) ^ a[i] 6= b[j] : The weak equivalence a i b ensures that a and b are equal at i = j which contradicts a[i] 6= b[j].
If the index equality i = j is mixed, the interpolation problem contains the shared auxiliary variable xij for i = j. If i (resp. j) is shared, we call i (resp. j) the shared term for i = j. We then identify four basic cases: (i) there exists a shared term for i = j and a[i] 6= b[j] is in B or mixed, (ii) there is a shared term for i = j and a[i] 6= b[j] is A-local, (iii) both i and j are B-local, and (iv) both i and j are A-local. 4.1
There is a Shared Term for i = j and a[i] 6= b[j] is in B or mixed If there exists a shared term x for the index equality i = j, the interpolant I can contain terms s[x] for shared array terms s occuring in the weak path between a and b. The basic idea is to summarize the weak A-paths by applying rule (read-over-weakeq) on their end terms. a[i] a k1 n i | k2 j = =
j where a, k2, v2, i are A-local, b, k1, v1, j are B-local, and s1, s2, s3 are shared. Projecting the mixed literals on A and B as described in Section 3.1 yields the interpolation problem A : i = xij ^ a = s1 ^ s2hk2
v2i = s3 ^ EQ(xik1 ; i) ^ i 6= k2 ^ EQ(xa[i]b[j]; a[i]) B : xij = j ^ s1hk1
v1i = s2 ^ s3 = b ^ : EQ(xik1 ; k1) ^ : EQ(xa[i]b[j]; b[j]) :
I
EQ(xa[i]b[j]; s1[xij]) ^ s2[xij] = s3[xij] ^ EQ(xik1 ; xij) : A implies I. As a = s1 holds, we get a[xij] = s1[xij]. With EQ(xa[i]b[j]; a[i]) and i = xij follows EQ(xa[i]b[j]; s1[xij]). The equality s2[xij] = s3[xij] follows by applying (read-over-weakeq) on s3 = s2hk2 v2i and using xij = i 6= k2. Finally, EQ(xik1 ; i) and i = xij yield EQ(xik1 ; xij). B contradicts I. By : EQ(xik1 ; k1) and EQ(xik1 ; xij) we get xij 6= k1. With s2 = s1hk1 v1i and (read-over-weakeq) we get s1[xij] = s2[xij]. From s3 = b we get s3[xij] = b[xij]. Transitivity, EQ(xa[i]b[j]; s1[xij]) and s2[xij] = s3[xij] and the above select equalities yield EQ(xa[i]b[j]; b[xij]). With xij = j, we get a contradiction to : EQ(xa[i]b[j]; b[j]).
Symbol condition for I. I contains only shared symbols and auxiliary variables. All auxiliary variables introduced for disequalities appear in positive EQ terms.
Algorithm. Assume that the weak path P : a i b is subdivided into A- and B-paths where shared paths are added to B-paths. Let x be the shared term for i = j, i.e. x stands for i if i is shared, for j if i is not shared but j is, and for the auxiliary variable xij if i = j is mixed. (i) An inner A-path of P starts and ends with a shared term: : s1 i s2 (these shared array terms can also be auxiliary variables introduced for a mixed array equality). The summary is s1[x] = s2[x]. For every B-local index disequality i 6= k on add the disjunct x = k and for every mixed index disequality add the disjunct EQ(xik; x). The interpolant of the subpath is s1[x] = s2[x] _ F A(x) where F A(x) :
_ x = k _ k2Stores( ) i6=k B-local
_ EQ(xik; x) : k2Stores( ) i6=k mixed (ii) If a[i] 6= b[j] is mixed and a[i] is A-local, the rst A-path on P starts with a or a is shared, i.e. : a i s1 (where s1 can be a). For the path , build the term EQ(xa[i]b[j]; s1[x]) and add F A(x) as in case (i).
I
EQ(xa[i]b[j]; s1[x]) _ F A(x) (iii) Similarly in the case where a[i] 6= b[j] is mixed and b[j] is A-local, the last A-path on P ends with b or b is shared, : sn i b. In this case the disjunct i 6= j needs to be added if i = j is B-local and i, j are both shared.
I
EQ(xa[i]b[j]; sn[x]) _ F A(x) [ _ i 6= j] (iv) For every B-path , add the conjunct x 6= k for each A-local index disequality i 6= k, and the conjunct EQ(xik; x) for each mixed index disequality i 6= k on . We de ne I
F B(x) where F B(x) :
^ x 6= k ^ k2Stores( ) i6=k A-local ^
EQ(xik; x) : k2Stores( ) i6=k mixed
The lemma interpolant is the conjunction of the above path interpolants. If i; j are shared and i = j is A-local, add the conjunct i = j.
I
^ I
There is a Shared Term for i = j and a[i] 6= b[j] is A-local If there exists a shared index for i = j and a[i] 6= b[j] is A-local, we build disequalities for the B-paths instead of equalities for the A-paths. This corresponds roughly to obtaining the interpolant of the inverse problem (B; A) by Section 4.1 and negating the resulting formula. Only the EQ terms are not negated because of the asymmetry of the projection.
Using the de nitions of F A and F B from the previous section, the lemma interpolant is I
_ When both i and j are B-local, we have no term x representing the weak path index i in the interpolant I. Hence, summarizing A- (resp. B-) paths by terms of the form s1[x] = s2[x] _ F A (resp. s1[x] 6= s2[x] ^ F B) as above is not possible. Instead we use the di function to make statements about the desired index. For instance, if a = bhi vihj wi for arrays a; b with b[j] 6= w, then a 2 b = b and di (a; b) = j or di (a 1 b; b) = j hold.
i = j ^ a = s1 ^ s1hk
vi = s2 ^ s2 = b ^ i 6= k ^ a[i] 6= b[j] where a, b, i, j are B-local, k, v are A-local, and s1, s2 are shared. Splitting the mixed disequality i 6= k as described in Section 3.1 results in the interpolation problem A : s1hk
vi = s2 ^ EQ(xik; k)
B : i = j ^ a = s1 ^ s2 = b ^ : EQ(xik; i) ^ a[i] 6= b[j] : An interpolant should re ect the information that s1 and s2 can di er at most at one index satisfying the EQ term. Using di , we can express the interpolant
I : (s1 = s2 _ EQ(xik; di (s1; s2))) ^ s1 1 s2 = s2 : A implies I. The rst literal in A implies that s1 and s2 di er at most at index k, yielding s1 1 s2 = s2. If s1 6= s2, then k = di (s1; s2) and EQ(xik; di (s1; s2)) follows from EQ(xik; k). B contradicts I. B implies that s1[i] 6= s2[i] holds. Thus, s1 = s2 cannot hold and I states that EQ(xik; di (s1; s2)) holds. With : EQ(xik; i) in B, this implies di (s1; s2) 6= i. Hence, s1 and s2 must di er at least at two indices. This contradicts s1 1 s2 = s2 in I. Symbol condition for I. I contains only shared symbols and the auxiliary variable for i 6= k appears in a positive EQ term only.
To generalize this idea, we de ne inductively for arrays a and b, a number m formula F ( ) with one free parameter: weq(a; b; 0; F ( )) :
a = b weq(a; b; m + 1; F ( )) :
(a = b _ F (di (a; b))) ^ weq(a 1 b; b; m; F ( )) : The term weq(a; b; m; F ( )) states that arrays a and b di er at most at m indices and that each index i on which they di er satis es the formula F (i).
Algorithm. For any A-path : s1 i s2, we count the number of stores j j := j Stores ( ) j. Each index i where s1 and s2 di er needs to satisfy F A(i) as de ned in Section 4.1. There is nothing to do for B-paths. The lemma interpolant is 0 and a (weq) ^ ( :s1 is2)2A-paths
weq(s1; s2; j j; F A( )) : 4.4
Both i and j are A-local In the case where both i and j are A-local, we summarize the B-paths, as all B-path ends are shared terms. Analogously to weq, we de ne for arrays a; b, a number m 0 and a formula F : nweq(a; b; 0; F ( )) : nweq(a; b; m + 1; F ( )) : a 6= b (a 6= b ^ F (di (a; b))) _ nweq(a 1 b; b; m; F ( )) : (nweq) The term nweq(a; b; m; F ( )) expresses that either one of the rst m indices i found by stepwise rewriting a to b satis es the formula F (i), or a and b di er at more than m indices.
Analogously to the last section, the lemma interpolant can be expressed as
_ Note that this is almost the negation of the interpolant of (B; A) computed as in Section 4.3. Only the EQ terms are not negated because of the asymmetry of the projection. 5
Interpolants for Weakeq-Ext Lemmas In this section, we describe how to compute interpolants for array lemmas of type (weakeq-ext). Figure 2 displays a visualization of the corresponding con ict
Cond(a ,P b) ^ ^ Cond(a
i b) ^ a 6= b : i2Stores(P ) i1 im a a a i1 k11 | km 1 i2 The main path P shows that a and b di er at most at the indices in Stores (P ) and a i b shows that a and b do not di er at index i.
A weak path labelled with i (short: i-path) represents weak congruence on i, i.e. it can contain select edges a0 j; k b0 where i j and i k and a0[j] b0[k]. We modify the methods in Section 4 to summarize the i-paths. In the B-local case 4.3, B-local select edges make no di erence, as the weq terms are built over A-paths, and analogously for the A-local case 4.4. However, if there are A-local select edges in the B-local case or vice versa, then k is shared or the index equality i = k is mixed and we can use k or the auxiliary variable xik to proceed as in the shared cases 4.1 and 4.2.
We have to adapt the interpolation procedures in Sections 4.1 and 4.2 by adding the index equalities that pertain to a select edge, analogously to the index disequality for a store edge before. More speci cally, we add to F A(x) a disjunct x 6= k for each B-local i = k on an A-path, and x 6= xik for each mixed i = k. Here, x is the shared term for the main index equality i = j as before. For B-paths we add to F B(x) the conjunct x = k for each A-local i = k and x = xik for each mixed i = k. Furthermore, if there is a mixed select equality a0[j] = b0[k] on the weak path, the auxiliary variable xa0[j]b0[k] is used in the summary for the A-path instead of s[x], i.e., we get a term of the form xa0[j]b0[k] = s2[x] in 4.1, and analogously for 4.2.
For (weakeq-ext) lemmas, we distinguish three cases: (i) a 6= b is in B, (ii) a 6= b is A-local, or (iii) a 6= b is mixed. 5.1
a 6= b is in B If the disequality a 6= b is in B, the A-paths both on the main store path and on the weak paths have only shared path ends. Hence, we summarize A-paths similarly to Sections 4.1 and 4.3. Algorithm. Divide the main path a ,P b into A-paths and B-paths. For each i 2 Stores (P ) on a B-path, summarize the corresponding i-path as in Sections 4.1 or 4.3. The resulting summary is denoted by Ii. For an A-path s1 , s2 use a weq term to state that each index where s1 and s2 di er satis es Ii( ) for some i 2 Stores ( ) where Ii is computed as in 4.1 with the shared term for i = j. The lemma interpolant is
I
^ Ii i2Stores( ) 2B-paths
^ ^
weq(s1; s2; j j; (s1,s2)2A-paths
_ Ii( )) : i2Stores( ) 5.2
a 6= b is A-local The case where a 6= b is A-local is similar with the roles of A and B swapped. For each i 2 Stores ( ) on an A-path on P , interpolate the corresponding weak path as in Sections 4.2 or 4.4 and obtain Ii. For each i 2 Stores ( ) on a B-path on P , interpolate the corresponding weak path as in Section 4.2 using as shared term and obtain Ii( ). The lemma interpolant is I
_ Ii i2Stores( ) 2A-paths
_ _
nweq(s1; s2; j j; (s1,s2)2B-paths
^ Ii( )) : i2Stores( ) 5.3
a 6= b is mixed If a 6= b is mixed, where w.l.o.g. a is A-local, the outer A- and B-paths end with A-local or B-local terms respectively. The auxiliary variable xab may not be used in store or select terms, thus we rst need to nd a shared term representing a before we can summarize A-paths. Example 3. Consider the following con ict: a = shi1
v1i ^ b = shi2 ^ a[i1] = s1[i1] ^ b = s1hk1 v2i ^ a 6= b w1i ^ i1 6= k1 ^ a = s2hk2 w2i ^ i2 6= k2 ^ b[i2] = s2[i2] (main path) (i1-path) (i2-path) where a, i1, v1, k2, w2 are A-local, b, i2, v2, k1, w1 are B-local and s, s1, s2 are shared. An interpolant for the con ict is I
EQ(xab; s) ^ weq(s; s2; 1; EQ(xi2k2 ; )) _ nweq s; s1; 2; EQ(xab; sh s1[ ]i) ^ weq(sh s1[ ]i; s2; 1; EQ(xi2k2 ; :)) ^ EQ(xi1k1 ; ) ; where in the second line the symbol refers to the di term of the outer nweq term and the symbol : to the di term of the inner weq term.
A implies I. Because of a = shi1 v1i, the arrays a and s can di er only at i1. If a = s, we get EQ(xab; s) by replacing a in the A-projection of a 6= b and we get weq(s; s2; 1; EQ(xi2k2 ; )) from the i2-path as in Section 4.3. Otherwise, s[i1] 6= s1[i1], as a[i1] = s1[i1] holds in A by the i1-path. By correcting s at i1 with s1[i1], we get a, and therefore EQ(xab; shi1 s1[i1]i) holds. Again, we get weq(shi1 s1[i1]i; s2; 1; EQ(xi2k2 ; :)) as in Section 4.3. Finally, for i1, we have the literal EQ(xi1k1 ; i1) by projection. We know that i1 is among the di terms between s and s1. Thus, the nweq term holds since i1 satis es the nested formula.
I contradicts B. Assume that the rst disjunct of I holds. By EQ(xab; s) in I and : EQ(xab; b) in B, we get s 6= b. The only potential di erence is at i2 because of B. Since B contains s2[i2] = b[i2] this implies that s and s2 also di er at i2. However, with the weq term in I and : EQ(xi2k2 ; i2) in B, we get a contradiction. Assume now that the second disjunct of I holds. Then either s and s1 must di er at some index which satis es the formula inside the nweq term, or at more than 2 positions. We know from B that s and s1 can only di er at i2 and k1. For k1, there is the term : EQ(xi1k1 ; k1) in B. Hence, can only be i2. Because of EQ(xab; sh s1[ ]i) in I and : EQ(xab; b) in B, we get sh s1[ ]i 6= b. Since s and b only di er at i2, the di erence can only be at i2 = and sh s1[ ]i[i2] 6= b[i2] = s2[i2]. By the inner weq term in I, i2 has to satisfy EQ(xi2k2 ; i2), which is a contradiction to B. Algorithm. Identify in the main path P the rst A-path a ,0 s1 and its store indices Stores ( 0) = fi1; : : : ij 0jg. To build an interpolant, we rewrite s1 by storing at each index im the value a[im]. We use s~ to denote the intermediate arrays. We build a formula Im(s~) inductively over m j 0j. This formula is an interpolant if s~ is a shared array that di ers from a only at the indices i1; : : : ; im.
For m = 0, i.e., a = s~, we modify the lemma by adding the strong edge s~ $ a in front of all paths and summarize it as if it was B-local using the algorithm in Section 5.1, but drop the weq term for the path s~ $ a ,0 s1. This yields I5:1(s~). We de ne
I0(s~)
EQ(xab; s~) ^ I5:1(s~) :
For the induction step to m + 1 we assume that s~ only di ers from a at i1; : : : ; im; im+1. Our goal is to nd a shared index term x for im+1 and a shared value v for a[x]. We use the im+1-path to conclude that s~hx vi is equal to a at im+1. Then we can include Im(s~hx vi) computed using the induction hypothesis.
(i) If there is a select edge on a B-subpath of the im+1-path or if im+1 is itself shared, we immediately get a shared term x for im+1. If the last B-path m+1 on the im+1-path starts with a mixed select equality, then the corresponding auxiliary variable is the shared value v. Otherwise, m+1 starts with a shared array sm+1 and v := sm+1[x]. We summarize the im+1-path from a to the start of m+1 as in Section 4.2 and get I4:2(x). Finally, we set Im+1(s~)
I4:2(x) _ (Im(s~hx vi) ^ F Bm+1 (x)) : (ii) Otherwise, we split the im+1-path into a im+1 sm+1 and sm+1 m,+1 b, where m+1 is the last B-subpath of the im+1-path. If s1 and a are equal on im+1 then also s~ and a are equal and the interpolant is simply Im(s~). If a and sm+1 di er on im+1, we build an interpolant from a im+1 sm+1 as in 4.4 and obtain I4:4. Otherwise, s1 and sm+1 di er on im+1. We build the store path s1 ,P0 sm+1 by concatenating P and m+1. Using nweq on the subpaths s , s0 of P 0 we nd the shared term x for im+1. If is in A we need to add the conjunct s j j s0 = s0 to obtain an interpolant. We get
Im+1(s~)
Im(s~) _ I4:4 [for a
im+1 sm+1] _
_ nweq s; s0; j j; Im(s~h s,s0 in P 0 sm+1[ ]i) ^ F Bm+1 ( ) [ ^ s j j s0 = s0] : The lemma interpolant for the mixed extensionality lemma is I Ij 0j(s1). 6
We presented an interpolation algorithm for the quanti er-free fragment of the theory of arrays. The algorithm uses an e cient array solver based on weak equivalence on arrays. In contrast to most existing interpolation algorithms for arrays, the solver does not depend on the partioning of the interpolation problem. Thus, our technique allows for e cient interpolation especially in the context of sequence interpolants and tree interpolants where interpolants for di erent partitions of the same unsatis able formula need to be computed.
Because we use the framework of proof tree preserving interpolation we only need to provide algorithms to interpolate the lemmas. These algorithms build the formulas by simply iterating over the weak equivalence and weak congruence paths found by the array solver.
Implementation of the algorithm in SMTInterpol [