Mnacho Echenim

Instantiation Schemes for Nested Theories

Keywords: I.2.3 [Artificial Intelligence]: Deduction and Theorem Proving General Terms: Theory, Verification Instantiation-based Proof Procedures, Satisfiability Modulo Theories, Combination of Theories

This paper investigates under which conditions instantiation-based proof procedures can be combined in a nested way, in order to mechanically construct new instantiation procedures for richer theories. Interesting applications in the field of verification are emphasized, particularly for handling extensions of the theory of arrays.

INTRODUCTION

Proving the satisfiability or unsatisfiability of a first-order formula (possibly modulo some background theory) is an essential problem in computer science -in particular for the automatic verification of complex systems, and instantiation schemes can be used for this purpose. Such schemes can be viewed as functions Θ that map a set of formulae (or clauses) S to a set of ground (i.e. without variable) instances Θ(S) of S. An instantiation scheme Θ is refutationally complete if for all sets of clauses S, Θ(S) is satisfiable exactly when S is. Examples of refutationally complete instantiation schemes include [START_REF] Lee | Eliminating duplication with the hyper-linking strategy[END_REF][START_REF] Plaisted | Ordered semantic hyperlinking[END_REF][START_REF] Ganzinger | New directions in instantiation-based theorem proving[END_REF][START_REF] Baumgartner | The Model Evolution Calculus[END_REF]. It is clear that an instantiation scheme that is refutationally complete does not always terminate, as Θ(S) may be infinite, but schemes that are both complete and terminating can be defined for specific classes of clause sets, that are thus decidable. A trivial and well-known example is the Bernays-Schönfinkel class (i.e. the class of purely universal formulae without function symbols of arity distinct from 0, see, e.g., [START_REF] Dreben | The Decision Problem, Solvable Classes of Quantificational Formulas[END_REF]), since in this case the set of ground instances is finite. Other examples include the class of stratified clause sets [START_REF] Abadi | Decidable fragments of many-sorted logic[END_REF]] and many classes of clause sets of the form G ∪ A, where G is a set of ground formulae and A is the set of axioms of a specific theory 1 , such as the theory of arrays (see for example [START_REF] Bradley | The Calculus of Computation: Decision Procedures with Applications to Verification[END_REF]), the theory of pointer structures such as lists [START_REF] Mcpeak | Data structure specifications via local equality axioms[END_REF], of sets with cardinalities [START_REF] Ohlbach | Modal logics, description logics and arithmetic reasoning[END_REF], a local theory [START_REF] Givan | New results on local inference relations[END_REF] etc. For instance, [Mc-peak and Necula 2005] provides an instantiation scheme for a language that describes properties of scalar fields and pointers. As long as no disequalities between pointers are allowed, their instantiation scheme is complete.

Instantiation schemes can also be defined for specific theories for which decision procedures exist. Then, the theory is not axiomatized, but directly handled by an external prover -used as a "black box". In this case, the instantiation procedure should preserve the validity of the formula modulo the considered theory. Such procedures are appealing, because it is usually much easier to check the validity of a ground set than that of a non-ground set (see for instance [START_REF] Bradley | What's decidable about arrays?[END_REF]).

Frequently, one has to handle heterogeneous problems, defined on complex theories for which no instantiation procedure exists. Such theories are frequently obtained by combining simpler theories. For instance the theory describing a data-structure (arrays, list, etc.) may be combined with the theory modeling the elements it contains (e.g., integers). Most systems rely on the Nelson-Oppen method and its numerous refinements to reason on combination of theories. This scheme allows one -under certain conditions -to combine independent decision procedures (see, e.g., [START_REF] Tinelli | A new correctness proof of the Nelson-Oppen combination procedure[END_REF][START_REF] Echenim | Modular instantiation schemes[END_REF]), but it is of no use for reasoning on theories that include axioms containing function or predicate symbols from both theories. As an example, consider the following formula: ∀i, j : nat, i ≤ j ⇒ select(t, i) ≤ select(t, j), that states that an array t is sorted. This formula uses symbols from the theory of integers (the predicate ≤) and from the theory of arrays (the function select, which returns the value stored in a certain array at a certain index).

In this paper, we show how to construct automatically instantiation schemes for such axioms, by combining existing instantiation schemes. More precisely, from two complete instantiation procedures Θ N and Θ A for the theory of integers and for the theory of arrays respectively, we construct a new procedure Θ which is able to handle a particular class of "mixed" axioms, containing function symbols from both theories (including for instance the axioms for sorted arrays and many others). Θ will be complete and terminating if both Θ N and Θ A are (as proven in Section 4). This approach is not restricted to specific theories such as Θ N and Θ A ; on the contrary it is generic and applies to a wide range of theories and some examples are provided in Section 5. The conditions that must be satisfied by the considered theories and by their instantiation procedures are identified in Section 3.2. They can be roughly summarized as follows. Firstly, the combination of theories must be hierarchic, in the sense that the domains of the function symbols of the first theory (called the base theory) must be distinct from the ranges of the function symbols of the second theory (called the nesting theory). Second, the instantiation procedure for the base theory must instantiate variables by ground terms in a uniform way; and this set of ground terms must be invariant under some operations on the considered clause sets, such as disjunction and replacement of variables by variables. Finally, the instantiation procedure for the nesting theory must be monotonic and the instances cannot depend on the names of the base terms occurring in the clauses.

Comparison with Related Work

There is an extensive amount of work on the combination of (usually disjoint) theories, using mainly refinements or extensions of the Nelson-Oppen method (see, e.g., [START_REF] Nelson | Simplification by cooperating decision procedures[END_REF][START_REF] Tinelli | A new correctness proof of the Nelson-Oppen combination procedure[END_REF][START_REF] Bruttomesso | Delayed theory combination vs. nelson-oppen for satisfiability modulo theories: a comparative analysis[END_REF]). For instance, [START_REF] Fontaine | Combinations of theories for decidable fragments of first-order logic[END_REF] shows that many decidable fragments of first-order logic can be combined with any disjoint theory, even if these fragments do not fulfill the stable infiniteness condition in general. A related result is presented in [START_REF] Fontaine | Combining lists with non-stably infinite theories[END_REF] for the theory of lists (with a length function). However, these results do not apply to non-disjoint theories such as those we consider in this paper, and they cannot handle nested combinations of arbitrary theories.

Reasoning on the combination of theories with mixed axioms has been recognized as an important problem and numerous solutions have been proposed in many specific cases. Most existing work focuses on testing the satisfiability problem of ground formulae in combinations or extensions of existing theories. In contrast, our method aims at reducing non-ground satisfiability to ground satisfiability tests, via instantiation.

For instance, [START_REF] Bradley | What's decidable about arrays?[END_REF][START_REF] Bradley | The Calculus of Computation: Decision Procedures with Applications to Verification[END_REF] define a decision procedure for extensions of the theory of arrays with integer elements, which is able to handle axioms such as the one above for sorted arrays. As we shall see in Section 5, our approach, when applied to these particular theories, permits to handle a strictly more expressive class of quantified formulae.

[ Ghilardi et al. 2007a] focuses on arrays with integer indices and devises a method to combine existing decision procedures (for Presburger arithmetic and for the theory of arrays). This method is able to handle some important specific features of arrays such as sortedness or array dimension. Similarly to our approach, theirs is based on an instantiation of the axioms. As we shall see, some of its features can be tackled with our method and others (such as Injectivity) are out of its scope. However, our method is generic in the sense that it applies to a wide class of theories and axioms (in particular, it applies to axioms that are not considered in [Ghilardi et al. 2007a]). It is essentially syntactic, whereas that of [Ghilardi et al. 2007a] is more of a semantic nature.

A logic devoted to reasoning with arrays of integers is presented in [START_REF] Habermehl | What else is decidable about integer arrays?[END_REF]] and the decidability of the satisfiability problem is established by reduction to the emptiness problem for counter automata. In Section 5 we shall show that the expressive power of this logic is again incomparable with the one we obtain with our approach.

Most approaches for handling quantified formulae rely on the original work of [START_REF] Detlefs | Simplify: a theorem prover for program checking[END_REF]] on the Simplify prover, in which heuristics for quantifier instantiation are devised (based on E-matching). Of course, these heuristics are not complete in general, and the class for which completeness is ensured is not precisely characterized. State-of-the-art techniques include [Ge et al. 2009;[START_REF] De Moura | Efficient E-Matching for SMT Solvers[END_REF]. [START_REF] Ge | Complete instantiation for quantified formulas in satisfiabiliby modulo theories[END_REF] proposes an instantiation scheme for sets of clauses possibly containing arithmetic literals, which can handle some of the axioms we consider. However termination is not guaranteed for this scheme, in contrast to ours.

Reduction functions are widely used tools allowing to reduce complex theories to simple ones. The instantiation procedures considered in the present work can be viewed as reduction procedures from quantified formulae to ground sets. [START_REF] Kapur | A reduction approach to decision procedures[END_REF] identifies various reduction methods that are widely used in efficient SMT-solvers [START_REF] Barrett | The Satisfiability Modulo Theories Library (SMT-LIB)[END_REF]] (e.g. from arrays to equality theory) and provides a general method for combining existing reduction procedures. Unlike the present paper, arbitrary combinations are allowed, but only ground formulae are considered.

Slightly closer to our approach is the work described in [START_REF] Sofronie-Stokkermans | Hierarchic reasoning in local theory extensions[END_REF][START_REF] Sofronie-Stokkermans | Hierarchical reasoning for the verification of parametric systems[END_REF], which defines the notion of the (stably) local extension of a theory and shows that the satisfiability problem in a (stably) local extension of a theory A can be reduced to a simple satisfiability test in A. The notion of a local extension is a generalization of the notion of a local theory, originally defined for Horn clauses in [START_REF] Givan | New results on local inference relations[END_REF][START_REF] Givan | Polynomial-time computation via local inference relations[END_REF]] and then generalized by allowing arbitrary term orderings and full clauses in [START_REF] Basin | Automated complexity analysis based on ordered resolution[END_REF] (semantic criteria based on saturation are proposed in [START_REF] Ganzinger | Relating semantic and proof-theoretic concepts for polynomial time decidability of uniform word problems[END_REF]] for proving locality of a theory). The idea is that, for testing the satisfiability of a ground formula G in the local extension of a theory, it is sufficient to instantiate the variables occurring in the new axioms by ground terms occurring either in G or in the axioms (in [START_REF] Ihlemann | On local reasoning in verification[END_REF], the notion of locality is further generalized by considering a closure operator Ψ which returns the set of terms that must instantiate the variables). The previous condition holds for numerous useful extensions of base theories, including for instance extensions with free functions, with selector functions for an injective constructor, with monotone functions over integers or reals etc. Our approach departs from these results because our goal is not to extend basic theories, but rather to combine existing instantiation procedures. Locality (or Ψ-locality) is a property of a set of axioms: there exists local and non-local presentation of a given theory. However, it is essentially a semantic notion, in the sense that testing whether a given presentation is local or whether there exists an equivalent local presentation, is an undecidable problem. Thus, this property must be established separately for every considered extension, although there exist decidable criteria and automated methods for extending a non-local presentation into a local one [START_REF] Ganzinger | Relating semantic and proof-theoretic concepts for polynomial time decidability of uniform word problems[END_REF][START_REF] Basin | Automated complexity analysis based on ordered resolution[END_REF]. Actually, our results can be viewed as a general method for proving that a given theory extension is local (relatively to some closure operator): if the theories B and N satisfy the conditions of Section 3.2 then any hierarchic expansion N [B] (see Definition 3) is Ψ-local (in the sense of [START_REF] Ihlemann | On local reasoning in verification[END_REF]), where Ψ is the closure operator obtained by considering the whole set of ground terms obtained by applying the instantiation procedure Θ N [Θ B ] defined in Definition 13.

In our approach we define conditions on the theories ensuring that they can be safely combined. These conditions can be tested once and for all for each theory, and then any combination is allowed. An important restriction of our approach compared to [START_REF] Sofronie-Stokkermans | Hierarchic reasoning in local theory extensions[END_REF][START_REF] Sofronie-Stokkermans | Hierarchical reasoning for the verification of parametric systems[END_REF] is that the theories must be combined in a hierarchic way: intuitively there can be function symbols mapping elements of the first theory B (the "base" theory) to elements of the second one N (the "nesting" theory), but no function symbols are allowed from N to B.

Other methods based on the superposition calculus [Bachmair and Ganzinger 1994] have also been proposed. [START_REF] Bonacina | On deciding satisfiability by theorem proving with speculative inferences[END_REF] investigates how to test the satisfiability of formulae involving quantifiers and decidable subtheories by tightly coupling a general-purpose theorem prover based on the superposition calculus with SMT solvers for the subtheories. Other extensions of the superposition calculus have also been proposed to handle first-order extensions of a base theory (see for example [Bachmair et al. 1994;[START_REF] Althaus | Superposition modulo linear arithmetic sup(la)[END_REF]). The superposition calculus is used to reason on the generic part of the formulae whereas the theory-specific part is handled by an external prover. These proof procedures can be used to reason on some of the formulae we consider in the present paper. However, we are not aware of any termination result for these approaches (even completeness requires additional restrictions that are not always satisfied in practice). [START_REF] Ganzinger | Modular proof systems for partial functions with evans equality[END_REF]] devises a superposition calculus for combinations of first-order theories involving total and partial functions. Some termination and completeness results are presented. Our approach uses an instantiationbased approach instead of superposition, and ensures that termination is preserved by the combination, at the cost of much stronger syntactic restrictions on the considered formulae.

Organization of the Paper

The rest of the paper is structured as follows. Section 2 contains general definitions and notations used throughout the present work. Most of them are standard, but some are more particular, such as the notions of ω-clauses or specifications. Section 3 describes our procedure for the nested combination of instantiation schemes, and introduces conditions to ensure that completeness is preserved. Section 5 shows some interesting applications of these results for theories that are particularly useful in the field of verification (especially for extensions of the theory of arrays). Section 6 concludes the paper and gives some lines of future work.

PRELIMINARIES

In this section, we first briefly review usual notions and notations about first-order clausal logic. Then we introduce the rather nonstandard notion of an ω-clause (a clause with infinitely many literals). We define the notion of specifications and provide some examples showing how usual theories such as those for integers or arrays can be encoded. Finally we introduce the notion of instantiation methods.

Syntax

Let S be a set of sort symbols and F be a set of function symbols together with a ranking function rnk : F → S * × S. For every f ∈ F, we write f :

s 1 × • • • × s n → s if rnk(f ) = s 1 , . . . , s n , s. If n = 0 then f is a constant symbol of sort s.
We assume that F contains at least one constant symbol of each sort. To every sort s ∈ S is associated a countably infinite set X s of variables of sort s, such that these sets are pairwise disjoint. X = s∈S X s denotes the entire set of variables. For every s ∈ S, the set of terms of sort s is denoted by T s (X ) and built inductively as usual on X and F:

-X s def ⊆ T s (X ). -If f : s 1 × . . . × s n → s and for all i ∈ [1, n], t i ∈ T si (X ) then f (t 1 , . . . , t n ) def ∈ T s (X ).
The set of terms is defined by T(X )

def = s∈S T s (X ).
An atom is an equality t ≃ s between terms of the same sort. A literal is either an atom or the negation of an atom (written t ≃ s). If L is a literal, then L c denotes its complementary:

(t ≃ s) c def = (t ≃ s) and (t ≃ s) c def = (t ≃ s).
A clause is a finite set (written as a disjunction) of literals. We assume that S contains a sort bool and that F contains a constant symbol true of sort bool. For readability, atoms of the form p ≃ true will be simply denoted by p (thus we write, e.g., a ≤ 2 instead of (a ≤ 2) ≃ true).

The set of variables occurring in an expression (term, atom, literal or clause) E is denoted by Var(E), and E is ground iff Var(E) = ∅. The set of ground terms of sort s is denoted by T s and the set of ground terms by T def = s∈S T s . A substitution is a function that maps every variable to a term of the same sort. The image of a variable x by a substitution σ is denoted by xσ. The domain of a substitution σ is the set2 dom(σ) def = {x ∈ X | xσ = x}, and its co-domain is the set of elements the variables in the domain are mapped to. Substitutions are extended to terms, atoms, literals and clauses as usual:

f (t 1 , . . . , t n )σ def = f (t 1 σ, . . . , t n σ), (t ≃ s)σ def = (tσ ≃ sσ), (¬L)σ def = ¬(Lσ) and ( n i=1 L i )σ def = n i=1 L i σ. A substitution σ is ground if ∀x ∈ dom(σ), Var(xσ) = ∅.
A ground instance of an expression E is an expression of the form Eσ, where σ is a ground substitution of domain Var(E). Definition 1. A substitution σ is pure iff for all x ∈ X , xσ ∈ X . In this case, for any term t, tσ is a pure instance of t. A substitution σ is a renaming if it is pure and injective.

✸

A substitution σ is a unifier of a set of pairs {(t i , s i ) | i ∈ [1, n]} iff ∀i ∈ [1, n], t i σ = s i σ.
It is well-known that all unifiable sets have a most general unifier (mgu), which is unique up to a renaming.

Semantics

An interpretation I is a function mapping:

-All sort symbols s ∈ S to nonempty disjoint sets s I . -Every function symbol f : s 1 × . . . × s n → s ∈ F to a function f I : s I 1 × . . . × s I n → s I . D I denotes the domain of I, i.e., the set s∈S s I . As usual, the valuation function E → [E] I maps every ground expression E to a value defined as follows:

- In the sequel, we restrict ourselves, w.l.o.g., to interpretations such that, for every s ∈ S, s I = {[t] I | t ∈ T s }.

[f (t 1 , . . . , t n )] I def = f I ([t 1 ] I , . . . , [t n ] I ), -[t ≃ s] I = true iff [t] I = [s] I , -[t ≃ s] I = true iff [t ≃ s] I = true, -[ n i=1 L i ] I def = true iff ∃i ∈ [1, n], [L i ] I = true.

ω-Clauses

For technical convenience, we extend the usual notion of a clause by allowing infinite disjunctions of literals: Of course, most of the usual properties of first-order logic such as semi-decidability or compactness fail if ω-clauses are considered. For instance, if C stands for the ω-

clause {b ≃ f i (a) | i ∈ N} and D j def = {b ≃ f j (a)} for j ∈ N, then S def = {D j | j ∈ N} ∪ {C}
is unsatisfiable, although every finite subset of S is satisfiable.

Specifications

Usually, theories are defined by sets of axioms and are closed under logical consequence. In our setting, we will restrict either the class of interpretations (e.g., by fixing the interpretation of a sort int to the natural numbers) or the class of clause sets (e.g., by considering only clause sets belonging to some decidable fragments or containing certain axioms). This is why we introduce the (slightly unusual) notion of specifications, of which we provide examples in the following section: Definition 4. A specification A is a pair (I, C), where I is a set of interpretations and C is a class of clause sets. A clause set S ∈ C is A-satisfiable if there exists an I ∈ I such that I |= S (I is an A-model of S). S and S ′ are A-equisatisfiable if they are both A-satisfiable or both A-unsatisfiable. We write S |= A S ′ iff every A-model of S is also an A-model of S ′ . ✸

For the sake of readability, if A is clear from the context, we will say that a set of clauses is satisfiable, instead of A-satisfiable. We write (I, C) ⊆ (I ′ , C ′ ) iff I = I ′ and C ⊆ C ′ . By a slight abuse of language, we say that C occurs in A if there exists a set S ∈ C such that C ∈ S.

In many cases, I will simply be the set of all interpretations, which we denote by I fol . But our results also apply to domain-specific instantiation schemes such as those for Presburger arithmetic. Of course, restricting the form of the clause sets in C is necessary in many cases for defining instantiation schemes that are both terminating and refutationally complete. This is why we do not assume that C contains every clause set. We shall simply assume that C is closed under inclusion and ground instantiations, i.e., for all S ∈ C if S ′ ⊆ S and S ′′ only contains ground instances of clauses in S, then S ′ , S ′′ ∈ C. All the classes of clause sets considered in this paper satisfy these requirements.

We shall restrict ourselves to a particular class of specifications: those with a set of interpretations that can be defined by a set of ω-clauses. ✸ Assumption 6. From now on, we assume that all the considered specifications are ωdefinable.

In most cases, the axioms of the considered specifications will be standard clauses. Infinite axioms are useful mainly to encode the domain of the specification, for instance for the natural numbers: ∀x, i∈N x ≃ s i (0). Of course, it could be possible to avoid having to consider such infinite disjunctions by adding further restrictions on the considered interpretations (e.g. by explicitly restricting their domains). However, it would then be necessary to add additional conditions on the interpretations in order to ensure that the combination is feasible; in our setting, the condition is straightforward: it suffices to assume that these axioms are defined over disjoint signatures.

Examples

Example 7. The specification of first-order logic is defined by A fol def = (I fol , C fol ) where:

-I fol is the set of all interpretations (i.e. Ax(I fol

) def = ∅).
-C fol is the set of all clause sets on the considered signature.

Example 8. The specification of Presburger arithmetic is defined as follows:

A Z def = (I Z , C Z ) where:
-Ax(I Z ) contains the domain axiom: k∈N (x ≃ s k (0) ∨ x ≃ -s k (0)) and the usual axioms for the function symbols 0 : int, -: int → int, s : int → int, p : int → int, + : int × int → int, and for the predicate symbols

≃ k : int × int → bool (for every k ∈ N) ≤: int × int → bool and <: int × int → bool: 0 + x ≃ x s(x) + y ≃ s(x + y) p(x) + y ≃ p(x + y) p(s(x)) ≃ x s(p(x)) ≃ x s k (0) ≃ k 0 -0 ≃ 0 -s(x) ≃ p(-x) -p(x) ≃ s(-x) x ≃ k y ∨ s k (x) ≃ k y x ≃ k y ∨ p k (x) ≃ k y x < y ⇔ s(x) < s(y) x < y ∨ x < s(y) x ≤ y ⇔ (x < y ∨ x ≃ y) x < s(x)
≃ k denotes equality modulo k (which will be used in Section 5.1.1); x, y denote variables of sort int and k is any natural number. Note that the domain axiom is an infinite ω-clause, while the other axioms can be viewed as standard clauses.

-C Z is the class of clause sets built on the previous set of function and predicate symbols.

In the sequel, the terms s k (0) and p k (0) will be written k and -k respectively.

Example 9. The specification of arrays is

A A def = (I A , C A ) where: -Ax(I A ) def = {select(store(x, z, v), z) ≃ v, z ′ ≃ z ∨ select(store(x, z, v), z ′ ) ≃ select(x, z ′ )}
, where select and store are respectively of profile: array × ind → elem and array × ind × elem → array (x is a variable of sort array, z, z ′ are variables of sort ind and v is a variable of sort elem).

-C A is the class of ground clause sets built on select, store and a set of constant symbols.

It should be noted that reals can be also handled by using any axiomatization of real closed fields, which are elementarily equivalent to the real numbers (in this case the axioms are standard clauses: there is no need for an infinite domain axiom).

Instantiation Procedures

An instantiation procedure is a function that reduces the A-satisfiability problem for any set of A-clauses to that of a (possibly infinite) set of ground A-clauses.

Definition 10. Let A = (I, C) be a specification. An instantiation procedure for A is a function Θ from C to C such that for every S ∈ C, Θ(S) is a set of ground instances of clauses in S. Θ is complete for A if for every finite clause set S ∈ C, S and Θ(S) are A-equisatisfiable. It is terminating if Θ(S) is finite for every finite clause set S ∈ C. ✸ If Θ is complete and terminating, and if there exists a decision procedure for checking whether a ground (finite) clause set is satisfiable in I, then the A-satisfiability problem is clearly decidable. Several examples of complete instantiation procedures are available in the literature. Some of them are general (hence non-terminating) methods handling full first-order logic [START_REF] Plaisted | Ordered semantic hyperlinking[END_REF][START_REF] Ganzinger | New directions in instantiation-based theorem proving[END_REF][START_REF] Baumgartner | The Model Evolution Calculus[END_REF][START_REF] Bonacina | On deciding satisfiability by theorem proving with speculative inferences[END_REF], other focus on or some decidable subclasses [START_REF] Abadi | Decidable fragments of many-sorted logic[END_REF][START_REF] Echenim | Instantiation of SMT problems modulo Integers[END_REF]. Several techniques have been devised for handling specific theories, by providing ways of instantiating axioms in such a way that satisfiability is preserved [START_REF] Loos | Applying linear quantifier elimination[END_REF][START_REF] Bradley | What's decidable about arrays?[END_REF][START_REF] Echenim | An instantiation scheme for satisfiability modulo theories[END_REF][START_REF] Sofronie-Stokkermans | Hierarchical reasoning for the verification of parametric systems[END_REF][START_REF] Goel | Deciding array formulas with frugal axiom instantiation[END_REF]. Our goal in this paper is to provide a general mechanism for constructing new complete instantiation procedures by combining existing ones.

Instantiation schemes for nested theories 0:9

NESTED COMBINATION OF SPECIFICATIONS

Definition

Theories are usually combined by considering their (in general disjoint) union. Decision procedures for disjoint theories can be combined (under certain conditions) by different methods, including the Nelson-Oppen method [START_REF] Tinelli | A new correctness proof of the Nelson-Oppen combination procedure[END_REF] or its refinements. In this section we consider a different way of combining specifications. The idea is to combine them in a "hierarchic" way, i.e., by considering the formulae of the first specification as constraints on the formulae of the second one.

For instance, if A Z is the specification of Presburger arithmetic and A A is the specification of arrays, then:

-0 ≤ x ≤ n is a formula of A Z (x denotes a variable and n denotes a constant symbol of sort int). -select(t, x) ≃ a is a formula of A A (stating that t is a constant array). -0 ≤ x ≤ n ⇒ select(t, x) ≃ a (stating that t is a constant on the interval [0, n]) is a formula obtained by combining A Z and A A hierarchically.
Such a combination cannot be viewed as a union of disjoint specifications, since the axioms contain function symbols from both specifications.

More formally, we assume that the set of sorts S is divided into two disjoint sets S B and S N such that for every function f :

s 1 ×. . .×s n → s, if s ∈ S B , then s 1 , . . . , s n ∈ S B . A term is a base term if it is of a sort s ∈ S B
and a nesting term if it is of a sort s ∈ S N and contains no non-variable base term. Any clause will be divided into two disjoint parts, a base part, containing only base terms, and a nesting part, containing only nesting terms. By definition, no nesting term can occur in a base term and the only base terms occurring in nesting terms are variables. This last condition is not by itself a serious restriction, because every non-variable base term t can be replaced by a variable x by adding the inequation x ≃ t in the base part of the clause. The essential point (that also justifies the distinction between the base specification and the nesting specification) is that function symbols from S N to S B are not allowed, while there can be functions from S B to S N . Note that since S B and S N are disjoint, the boolean sort cannot occur both in S B and S N . However, this problem can easily be overcome by considering two copies of this sort (bool and bool ′ ).

In the sequel we let

X B def = s∈S B X s (resp. X N def = s∈S N X s )
be the set of base variables (resp. nesting variables) and let F B (resp. F N ) be the set of function symbols whose codomain is in S B (resp. S N ). An S B -ground instance of an expression E is an expression of the form Eσ where σ is a ground substitution of domain Var(E) ∩ X B . Intuitively, an S B -ground instance of E is obtained from E by replacing every variable of a sort s ∈ S B (and only these variables) by a ground term of the same sort.

Definition 1. Ω B denotes the set of ω-clauses C such that every term occurring in C is a base term. Ω N denotes the set of ω-clauses C such that:

(1) Every non-variable term occurring in C is a nesting term.

(2) For every atom t ≃ s occurring in C, t and s are nesting terms. ✸

Notice that it follows from the definition that

Ω B ∩ Ω N = ∅, since S B and S N are disjoint. Definition 2. A specification (I, C) is a base specification if Ax(I) ⊆ Ω B and for every S ∈ C, S is a finite subset of Ω B . It is a nesting specification if Ax(I) ⊆ Ω N and for every S ∈ C, S ⊆ Ω N . ✸
In the example at the beginning of the section, A Z is the base specification and A A is the nesting specification.

Throughout this section, B = (I B , C B ) will denote a base specification and N = (I N , C N ) a nesting specification. Notice that the clause sets in C B are finite, but that those in C N can be finite or infinite. Base and nesting specifications are combined as follows:

Definition 3. The hierarchic expansion of N over B is the specification N [B] = (I, C) defined as follows:

(1) Ax(I)

def = Ax(I B ) ∪ Ax(I N ). (2) Every clause set in C is of the form {C B i ∨ C N i | i ∈ N} where {C B i | i ∈ N} ∈ C B and {C N i | i ∈ N} ∈ C N . If C is a clause in C, then C B is
c1 {x ≥ a ∨ select(t, x) ≃ b} (t is constant on [a, ∞[) c2 {x ≥ a ∨ x ≤ b ∨ select(t, x) ≃ select(t ′ , x)} (t and t ′ coincide on [a, b]) c3 {select(t, i) ≃ select(t ′ , i + 1)} (t and t ′ coincide up to a shift) c4 {x ≤ y ∨ select(t, x) ≤ select(t, y)} (t is sorted) c5 {select(t, x) ≤ x} (t is lower than the identity)
Clauses c 1 and c 2 occur in A A [A Z ], and for instance,

c N 1 = (select(t, x) ≃ b) and c B 1 = (x ≥ a). Clause c 3 does not occur in A A [A Z ]
because the atom select(t ′ , i + 1) of the nesting specification contains the non-variable term i + 1 of the base specification. However, c 3 can be equivalently written as follows:

c ′ 3 {j ≃ i + 1 ∨ select(t, i) ≃ select(t ′ , j)} and c ′ 3 is in A A [A Z ] 3 . Clause c 4 does not occur in A A [A Z ],
because select(t, x) ≤ select(t ′ , x) contains symbols from both A Z (namely ≤) and A A (select) which contradicts Condition 2 of Definition 3. However, c 4 can be handled in this setting by considering a copy A ′ Z of A Z (with disjoint sorts and function symbols). In this case, c 4 belongs to

(A A ∪ A ′ Z )[A Z ], where A A ∪ A ′ Z denotes the union of the specifications A A and A ′ Z . Of course A ′
Z can be replaced by any other specification containing an ordering predicate symbol. The same transformation cannot be used on the clause c 5 , since (because of the literal select(t, x) ≤ x) the sort of the indices cannot be separated from that of the elements. Again, this is not surprising because, as shown in [START_REF] Bradley | The Calculus of Computation: Decision Procedures with Applications to Verification[END_REF], such axioms (in which index variables occur out of the scope of a select) easily make the theory undecidable. A natural and potentially interesting line of research would be to identify classes of formulae that can be automatically transformed into clause sets in A A [A Z ] by duplicating some elements of the signature, as done previously for the clause c 4 .

Nested Combination of Instantiation Schemes

The goal of this section is to investigate how instantiation schemes for B and N can be combined in order to obtain an instantiation scheme for N [B]. For instance, given two instantiation schemes for integers and arrays respectively, we want to automatically derive an instantiation scheme handling mixed axioms such as those in Example 4. We begin by imposing conditions on the schemes under consideration.

3.2.1. Conditions on the Nesting Specification. First, we investigate what conditions can be imposed on the instantiation procedure for the nesting specification N . Note that having a complete instantiation procedure for N is not sufficient; indeed, since by definition every term of a sort in S B occurring in C N is a variable, such an instantiation would normally replace every such variable by an arbitrary ground term (a constant, for example). This is not satisfactory because in the current setting, the value of these variables can be constrained by the base part of the clause. Thus we need to impose a stronger condition. We shall assume that the considered procedure is complete for every clause set that is obtained from clauses in C N by grounding the variables in X B , no matter the grounding instantiation. Definition 5. An S B -mapping is a function α mapping ground base terms to ground base terms. Such a mapping is extended straightforwardly into a function from expressions to expressions: for every expression (term, atom, literal, clause or set of clauses) E, α(E) denotes the expression obtained from E by replacing every base term t occurring in E by α(t).

An instantiation procedure Θ is S B -invariant iff for every S B -mapping α, and every clause C in a set S, C ∈ Θ(S) ⇒ α(C) ∈ Θ(α(S)). ✸

We may now define nesting-complete instantiation procedures. Intuitively, such a procedure must be complete on those sets in which the only terms of a sort in S B that occur are ground, the instances cannot depend on the names of the base terms and the addition of information cannot make the procedure generate less instances for a given clause set. Definition 6. An instantiation procedure Θ is nesting-complete if the following conditions hold:

(1) For all sets S ∈ C N and all set of clauses S ′ such that every clause in S ′ is an S B -ground instance of a clause in S, S ′ and Θ(S

′ ) are N -equisatisfiable. (2) Θ is S B -invariant. (3) Θ is monotonic: S ′ ⊆ S ⇒ Θ(S ′ ) ⊆ Θ(S).
✸

Notice that a nesting-complete instantiation procedure is necessarily complete (for the nesting specification).

3.2.2. Conditions on the Base Specification. Second, we impose conditions on the instantiation procedure for the base specification B. We need the following definitions: Definition 7. Let S be a set of clauses and let G be a set of terms. We denote by S ↓G the set of clauses of the form Cσ, where C ∈ S and σ maps every variable in C to a term of the same sort in G. ✸ Example 8. Let S = {p(x, n), f (x, y) ≃ c}, where x, y are variables of sort s and n is a variable of sort nat.

Let G = {a, b : s, 0 : nat}. Then S ↓G = {p(a, 0), p(b, 0), f (a, a) ≃ c, f (a, b) ≃ c, f (b, a) ≃ c, f (b, b) ≃ c}.
Definition 9. If S is a set of clauses, we denote by S ⋆ ∨ the set of clauses of the form i=1,...,n C i σ i such that for every i ∈ [1, n], C i ∈ S and σ i is a pure substitution. ✸

Example 10. Let S = {p(x, y)}. Then S ⋆ ∨ contains among others the clauses p(x, x), p(x, y), p(x, y) ∨ p(z, u), p(x, y) ∨ p(y, x), p(x, y) ∨ p(y, z) ∨ p(z, u), etc. Definition 11. An instantiation procedure Θ for B is base-complete if for every finite clause set S there exists a finite set of terms G S such that Θ(S) = S ↓G S and the following conditions hold:

(1) For every S ∈ C B , S ↓G S and S are B-equisatisfiable.

(2

) If S ′ ⊆ S then G S ′ ⊆ G S . (3) For every clause set S ∈ C, G S ⋆ ∨ ⊆ G S (thus by 2, we have G S ⋆ ∨ = G S ). ✸
Obviously these conditions are much stronger than those of Definition 6. Informally, Definition 11 states that all variables must be instantiated in a uniform4 way by ground terms, and that:

(1) Satisfiability must be preserved.

(2) The instantiation procedure is monotonic.

(3) The considered set of ground terms does not change when new clauses are added to S, provided that these clauses are obtained from clauses already occurring in S by disjunction and pure instantiation only.

These conditions are somewhat similar to those on closure operators in [START_REF] Ihlemann | On local reasoning in verification[END_REF]]. Actually, the function mapping the set of terms in S to G S could be viewed as a closure operator. The difference is that G S is defined on a set of clauses S whereas closure operators are defined on the sets of ground terms occurring in S. Since G S depends on the clause set and not on the terms it contains, Condition 3 is not necessarily fulfilled. Consider for instance an instantiation procedure based on hyper-linking5 [START_REF] Lee | Eliminating duplication with the hyper-linking strategy[END_REF]. Let S = {p(a), ¬p(x), q(f (x)), ¬q(x)}. The only hyper-links are p(a), ¬p(x) and q(f (x)), ¬q(x), which yields the following set of ground terms: {a, f (⊥)}.

On the other hand, if the clause ¬p(x) ∨ q(f (x)) is considered, then the term f (a) must be added.

3.2.3. Definition of the Combined Instantiation Scheme. We now define an instantiation procedure for N [B]. Intuitively this procedure is defined as follows.

(1) First, the nesting part of each clause in S is extracted and all base variables are instantiated by arbitrary constant symbols • (one for each base sort).

(2) The instantiation procedure for N is applied on the resulting clause set. This instantiates all nesting variables (but not the base variables, since they have already been instantiated at Step 1). The role of this step is essentially to compute the nesting part of the instantiating substitutions. Notice that the instantiation procedure is not applied to the clause set obtained after instantiating base variables because this set may be very large. The formal definition of the procedure is given below. Let γ • be a substitution mapping every variable of a sort s ∈ S B to an arbitrary constant symbol • s of sort s.

Definition 13. Let Θ B be a base-complete instantiation procedure and Θ N be a nesting-complete instantiation procedure. Θ N [Θ B ](S) is defined as the set of clauses of the form (C B ∨ C N )θ ′ σ where:

-C ∈ S. -C N γ • θ ∈ Θ N (S N γ • ).
θ ′ is obtained from θ by replacing every occurrence of a constant symbol • s in the co-domain of θ by a fresh variable of the same sort. -σ maps every variable in Cθ ′ to a term of the same sort in G S B . ✸

The following proposition is straightforward to prove and states the soundness of this procedure: Proposition 14. Let Θ B be a base-complete instantiation procedure and let Θ N be a nesting-complete instantiation procedure. For every set of clauses

S ∈ C, Θ N [Θ B ](S) is a set of ground instances of clauses in S. Thus if Θ N [Θ B ](S) is N [B]-unsatisfiable, then so is S.
Several examples of concrete instantiation procedures satisfying the conditions of Definitions 6 and 11 are provided in Section 5.

In order to be applicable in practice, the described procedure has to be refined and adapted so that the instances can be generated efficiently. Obviously, the set of instances Θ N [Θ B ](S) can be generated with only a minimal modification of the base and nesting instantiation procedures Θ B and Θ N : we only have to make them return the instantiating substitutions, rather than the corresponding clauses. Apart from this, the procedures are used as black boxes. Thus our technique could be integrated into existing systems without too drastic a change in the code. The applications of the procedures Θ B and Θ N are completely independent and thus can be run in parallel. Existing heuristics for guiding the choice of the most relevant instances for the base and nesting theories (as for instance those described in [START_REF] Detlefs | Simplify: a theorem prover for program checking[END_REF]Ge et al. 2009;[START_REF] De Moura | Efficient E-Matching for SMT Solvers[END_REF]) can also be applied to the combined procedure. It is clear that the instances can be generated in an incremental way: rather than generating the whole set of clauses Θ N (S N γ • ), and then -for each clause C N γ • θ occurring in this set -computing the corresponding set of clauses (C B ∨ C N )θ ′ σ, it is obviously possible to generate these instances on the fly and send them to a ground SMT-solver in a dynamic way: in case a contradiction is found then the search can be stopped, otherwise one has to iterate the process to generate new instances. This is particularly important if the set Θ N (S N γ • ) is infinite, or very large.

COMPLETENESS

This section is devoted to the proof of the main result of this paper, namely that the procedure

Θ N [Θ B ] is complete for N [B]:
Theorem 1. Let Θ B be a base-complete instantiation procedure (for B) and let Θ N be a nesting-complete instantiation procedure (for N ). Then Θ N [Θ B ] is complete for N [B]; furthermore, this procedure is monotonic and S B -invariant.

The rest of the section (up to Page 21) can be skipped entirely by readers not interested in the more theoretical aspects of the work. The proof of this theorem relies on a few intermediate results that are developed in what follows.

Overview of the Proof

We start by providing a general overview of the proof. Although it hides some technicalities, this overview should help the reader understand the following subsections. In all examples in this section a literal belongs to the nested specification iff it is nonequational.

We consider an unsatisfiable clause set S and we prove that Θ N [Θ B ](S) is unsatisfiable.

(1) From S to S| I : For each interpretation I in the base specification, we define (in Section 4.3) a clause set S| I , obtained by instantiating the base variables of the clauses in S in all possible ways and by evaluating the base part of each instantiated clause using the interpretation I. For instance, if S = {x ≃ 0 ∨ a ≃ x + 1 ∨ p(x, y)}, then S| I will either be ∅ (if I |= a ≃ 1) or p(0, y) (if I |= a ≃ 1). The goal of this transformation is to make possible the application of the instantiation procedure for the nesting specification. To accomplish this, we first need to prove that any ground substitution can be decomposed into two parts: a nesting substitution and a base substitution, which is done in Section 4.2. This ensures that every clause in S| I is obtained by instantiating a nesting clause by a base substitution, which makes the procedure Θ N applicable on S| I . (2) S| I is unsatisfiable: We then remark in Lemma 7 that S| I is unsatisfiable (for every interpretation I). Indeed, we prove that if S| I has a model J then it can be transformed into a model of S by combining it with I in a rather natural way, which yields a contradiction since S is unsatisfiable by hypothesis. Since Θ N is complete, this entails that Θ N (S| I ) is also unsatisfiable. Since Θ N (S| I ) is infinite in general, this disjunction is not necessarily a clause: it is an ω-clause, denoted by E I , and by construction E I is false in I. By considering the set of all ω-clauses E I for every interpretation I in the base specification, we thus obtain an unsatisfiable set U of ω-clauses. We then apply the instantiation procedure Θ B on U , after proving that the former is complete for sets of ω-clauses (not only for standard clauses), which is done in Section 4.5. This shows that

Θ B (U ) is unsatisfiable. (4) If Θ B (U ) is unsatisfiable then Θ N [Θ B ](S)
[Θ B ](S) |= Θ B (U ), hence that Θ N [Θ B ](S) is unsatisfiable.
We wish to emphasize the important role played by the notion of ω-clauses in this proof. It allows us to handle non-compact specifications in a rather natural way. Indeed, since we do not assume that the considered specifications are compact, the "unsatisfiable core" of the set of instances that is generated by Θ N on the clause sets S| I can be infinite. To propagate the information to the base procedure Θ B , it is necessary to consider an infinite disjunction of base clauses and to establish completeness results of the instantiation procedure Θ B for these infinite disjunctions (see Section 4.5). Without this notion, the scope of the results would have to be restricted, either by assuming that N is compact or that Θ N is terminating.

Substitution Decomposition

Definition 2. A substitution σ is a base substitution iff dom(σ) ⊆ X B . It is a nesting substitution iff dom(σ) ⊆ X N and for every x ∈ dom(σ), xσ contains no non-variable base term. ✸

We show that every ground substitution can be decomposed into two parts: a nesting substitution and a base substitution. We begin by an example:

Example 3. Assume that B = A Z , N = A fol and that F contains the following symbols: f : s × int → s, c : s. Consider the ground substitution σ = {x → f (c, s(0)), y → f (f (c, 0), 0), n → s(0)}. We can extract from σ a nesting substitution by replacing all base terms by variables8 , thus obtaining

σ N = {x → f (c, n), y → f (f (c, m), m)}, and then construct the base substitution σ B = {n → s(0), m → 0} such that σ = σ N σ B .
Note that σ N is not ground and that dom(σ B ) ⊆ dom(σ).

The following result generalizes this construction: Proposition 4. Every ground substitution σ can be decomposed into a product σ = (σ N σ B )| dom(σ) where σ N is a nesting substitution, σ B is a base substitution, and for all x ∈ dom(σ B ) \ dom(σ):

-∀y ∈ dom(σ B ) ∩ dom(σ), xσ B = yσ B , -∀y ∈ dom(σ B ) \ dom(σ), yσ = xσ ⇒ x = y.
PROOF. Let E be the set of base terms occurring in an element of the co-domain of σ (in the previous example, we get: E = {s(0), 0}). Let ν be a partial function mapping every term t ∈ E to an arbitrarily chosen variable ν(t) such that ν(t)σ = t (e.g. ν : {s(0) → n}). This function ν is extended into a total function on E by mapping all terms t for which ν(t) is undefined to pairwise distinct new variables, not occurring in dom(σ) (continuing the previous example we can take: ν : {s(0) → n, 0 → m}). Note that ν is injective by construction. The substitutions σ B and σ N are defined as follows:

-dom(σ N ) def = dom(σ)∩X N and xσ N is the term obtained by replacing every occurrence of a term t ∈ E in xσ by ν(t);

-dom(σ B ) def = [dom(σ) ∩ X B ] ∪ ν(E); if x = ν(t) for some term t ∈ E, then xσ B def = t; otherwise, xσ B def = xσ. Note that σ B is well-defined, since by definition if ν(t) = ν(s) then t = s.
In the previous example, the reader can check that we obtain the substitutions

σ N = {x → f (c, n), y → f (f (c, m, m))} and σ B = {n → s(0), m → 0}. By construction, σ N is a nesting substitution and σ B is a base substitution. Furthermore, since ν(t)σ B = t, xσ N σ B = xσ for every x ∈ dom(σ) ∩ X N . Similarly, for every x ∈ dom(σ) ∩ X B , xσ N σ B = xσ B = xσ and therefore σ = (σ N σ B )| dom(σ) . Let x ∈ dom(σ B ) \ dom(σ).
By definition of σ B , x is of the form ν(t) for some t ∈ E, and there is no variable y ∈ dom(σ) such that yσ = t, since otherwise ν(t) would have been defined as y. Thus ∀y ∈ dom(σ B ) ∩ dom(σ), xσ B = yσ = yσ B . Now if y ∈ dom(σ B ) \ dom(σ) and xσ B = yσ B , then y is also of the form ν(s) for some s ∈ E and we have xσ B = t and yσ B = s, hence t = s and x = y.

Partial Evaluations

Given a set of clauses S in N [B] and an interpretation I of B, we consider a set of clauses S ′ of N by selecting those ground instances of clauses in S whose base part evaluates to false in I and adding their nesting part to S ′ . This will allow us to apply the procedure Θ N on S ′ . More formally: Definition 5. For every clause C B ∈ C B and for every interpretation I ∈ I B , we denote by Φ I (C B ) the set of ground substitutions η of domain Var(C B ) such that I |= C B η. Then, for every S ∈ C we define:

S| I def = {C N η | C ∈ S, η ∈ Φ I (C B )}. Example 6. Let S = {x ≃ a ∨ P (x), y < 2 ∨ Q(y, z)} be a set of clauses in A fol [A Z ],
where x, y, a are of sort int and z is a variable of a sort distinct from int. Let I be the interpretation of natural numbers such that a I = 1.

Then Φ I (x ≃ a) = {x → 1} and Φ I (y < 2) = {y → k | k ∈ N, k ≥ 2}. Therefore S| I = {P (1)} ∪ {Q(k, z) | k ∈ N, k ≥ 2}.
The following lemma shows that S| I is N -unsatisfiable when S is N [B]-unsatisfiable.

Lemma 7. For every N [B]-unsatisfiable set of clauses S ∈ C and for every

I ∈ I B , S| I is N -unsatisfiable.

PROOF. Let N [B] = (I, C).

Assume that S| I is N -satisfiable, i.e. that there exists an interpretation J ∈ I N validating S| I . W.l.o.g. we assume that the domain of J is disjoint from that of I. We construct an interpretation K ∈ I satisfying S, which will yield a contradiction since S is N [B]-unsatisfiable by hypothesis.

For all sort symbols s ∈ S B and for all e ∈ s I , we denote by γ(e) an arbitrarily chosen ground base term such that [γ(e)] I = e9 . If E is a ground expression, we denote by E ↓ γ the expression obtained from E by replacing every term t by γ([t] I ); by construction [E] I = [E ↓ γ ] I . Let ψ : D I ⊎ D J → D J be the function defined for every element e ∈ D I ∪ D J as follows:

-if e ∈ s I then ψ(e) We define the interpretation K by combining I and J as follows:

-K coincides with I on S B and on every function symbol whose co-domain is in S B .

-K coincides with J on S N .

-For all function symbols f ∈ F N of arity n, f K (e 1 , . . . , e n ) def = f J (ψ(e 1 ), . . . , ψ(e n )). Note that f K is well-defined since by definition of ψ, if e ∈ s K then ψ(e) ∈ s J .

Let E be a ground expression (term, atom, literal, clause or ω-clause) such that E↓ γ = E. Assume that E is a ground instance of an expression occurring in a clause in Ω N . We prove by structural induction on

E that [E] J = ψ([E] K ).
-If E is a term of a sort in S B then since I and K coincide on S B ∪ F B , we have

[E] K = [E] I . By hypothesis E↓ γ = E, thus γ([E] I ) = E and by definition of ψ, ψ([E] K ) = ψ([E] I ) = [γ(E)] J = [E] J . -If E is of the form f (t 1 , . . . , t n ) where f ∈ F N , then by definition [E] J = f J ([t 1 ] J , . . . , [t n ] J )
and by the induction hypothesis,

[t i ] J = ψ([t i ] K ) for i ∈ [1, n]. Again by definition, [E] K = f J (ψ([t 1 ] K ), . . . , ψ([t n ] K )) = f J ([t 1 ] J , . . . , [t n ] J ) = [E] J .
Thus, since the domains of I and J are disjoint,

[E] J ∈ S I B , hence ψ([E] J ) = [E] J .
-If E is an atom of the form t 1 ≃ t 2 then t 1 , t 2 ∈ S B . Indeed E occurs in a ground instance of a clause C occurring in Ω N and by Definition 1, such clauses cannot contain equalities between base terms. Thus we have ψ(

[t i ] K ) = [t i ] K (for i = 1, 2)
and the proof is straightforward. -The proof is immediate if E is a literal or a (possibly infinite) disjunction of literals.

Since J |= S| I and all specifications are assumed to be ω-definable (see Definition 5), we deduce that K |= S| I ∪ Ax(I N ). Indeed, for the sake of contradiction, assume that there exists an ω-clause C ∈ S| I ∪ Ax(I N ) and a ground substitution θ of domain Var

(C) such that K |= Cθ. Since K |= t ≃ t ↓ γ for every term t, necessarily K |= Cθ ′ where xθ ′ def = xθ ↓ γ . But then Cθ ′ ↓ γ = Cθ ′ and since [E] J = ψ([E] K ), we conclude that J |= Cθ ′ which is impossible since by hypothesis J is an N -model of S| I .
We now prove that K |= S. Let C ∈ S and η be a ground substitution of domain Var(C). W.l.o.g. we assume that ∀x ∈ Var(C), xη ↓ γ = xη. Let η B (resp. η N ) be the restriction of η to the variables of a sort in S B (resp. in

S N ). If I |= C B η B then K |= C B η B because K and I coincide on S B ∪ F B , and consequently K |= Cη (since Cη ⊇ C B η B ). If I |= C B η B then η B ∈ Φ I (C), hence C N η B ∈ S| I . Again K |= Cη B hence K |= Cη; therefore K |= S.
Finally, since K coincides with I on S B ∪ F B we have K |= Ax(I B ). This proves that K is an N [B]-model of S, which is impossible.

Abstraction of Base Terms

Lemma 7 relates the N [B]-unsatisfiability of a set of clauses S to the N -unsatisfiability of sets of the form S| I . By definition, S| I is of the form S ′ σ, for some clause set S ′ ∈ C N and for some ground base substitution σ. However, since neither Ax(I N ) nor C N contains symbols of a sort in S B , the interpretation of the ground base terms of S ′ in an interpretation of I N is arbitrary: changing the values of these terms does not affect the N -satisfiability of the formula. Thus the actual concrete values of the ground base terms does not matter: what is important is only how these terms compare to each other.

Example 8. Assume that N = A fol , p : int × s → bool, a : s, and let S = {p(x, z), ¬p(y, a)}. Consider σ : {x → 0, y → 0}, clearly, Sσ |= N ✷. But also S{x → s(0), y → s(0)} |= N ✷ and more generally S{x → t, y → t} |= N ✷. On the other hand,

S{x → 0, y → s(0)} |= N ✷ and more generally S{x → t, y → t ′ } |= N ✷ if t, t ′ are distinct integers.
Therefore, if Sσ |= N Cσ for some base substitution σ then actually Sθ |= N Cθ, for every substitution θ such that xθ = yθ ⇔ xσ = yσ. This will be formalized in the following definitions and lemma. We first introduce an unusual notion of semantic entailment. The intuition is that variables in S B are considered as "rigid" variables that must be instantiated by arbitrary ground terms: Definition 9. Let S ∈ C N . We write S |= r C iff for every ground substitution of domain X B , Sσ |= N Cσ. ✸

Example 10. Assume that N = A fol . Let a : s, p : int × s → bool and q : int → bool, where int ∈ S B , s ∈ S N . Let S = {p(x, y), ¬p(u, a) ∨ q(u)}, where x, y, u are variables.

Then S |= r q(x), but S |= r q(0). Note that x denotes the same variable in S and q(x) (the variables are not renamed).

Definition 11. For every substitution σ we denote by σ an arbitrarily chosen pure substitution such that xσ = yσ ⇒ x σ = y σ , for every x, y ∈ X . ✸

Note that such a substitution always exists10 . The next lemma can be viewed as a generalization lemma: it shows that the values of the ground base terms can be abstracted into variables.

Lemma 12. Let S ∈ C N and σ be a base substitution. If Sσ |= N Cσ then S σ |= r C σ .

PROOF. Let θ be a substitution of domain X B . We assume that there exists an I ∈ I N such that I |= S σ θ and I |= C σ θ, and we show that a contradiction can be derived.

For every ground term t, we denote by Γ(t) the ground term obtained from t by replacing every ground subterm of the form xσ by x σ θ. Γ is well-defined: indeed, if xσ = yσ, then by definition of σ , x σ = y σ thus x σ θ = y σ θ. Let J be the interpretation defined as follows11 :

-If s ∈ S B then s J def = T s . -If f is a symbol of rank s 1 × . . . × s n → s where s 1 , . . . , s n , s ∈ S B then f J (t 1 , . . . , t n ) def = f (t 1 , . . . , t n ). -If f is a symbol of rank s 1 × . . . × s n → s where s ∈ S B then f J (t 1 , . . . , t n ) def = f I (t ′ 1 , . . . , t ′ n ) where for every i ∈ [1, n], s i ∈ S N ⇒ t ′ i = [t i ] J and s i ∈ S B ⇒ t ′ i = [Γ(t i )] I .
By construction, [s] J = s for every ground base term s; we prove that for every ground nesting term t, [t] J = [Γ(t)] I , by induction on t.

If t = f (t 1 , . . . , t n ), then [t] J = f I (t ′ 1 , . . . , t ′ n ) where for every i ∈ [1, n], s i ∈ S N ⇒ t ′ i = [t i ] J and s i ∈ S B ⇒ t ′ i = [Γ(t i )] I . By the induction hypothesis, s i ∈ S N ⇒ t ′ i = [Γ(t i )] I . Thus [t] J = f I ([Γ(t 1 )] I , . . . , [Γ(t n )] I ) = [Γ(t)] I .
Now let σ ′ be a ground substitution with a domain in X N , and let θ ′ def = Γ • σ ′ . We prove that for every expression E occurring in S ∪{C} that is not a base term,

[Eσσ ′ ] J = [E σ θθ ′ ] I . -Assume that E is a variable x in X N . Then [Eσσ ′ ] J = [xσ ′ ] J ,

and by the previous relation we get [Eσσ

′ ] J = [Γ(xσ ′ )] I = [xθ ′ ] I = [E σ θθ ′ ] I .
-Assume that E is a nesting term of the form f (t 1 , . . . , t n ). Then by the result above,

[Eσσ ′ ] J = [Γ(Eσσ ′ )] I . By definition of Γ we have Γ(Eσσ ′ ) = f (Γ(t 1 σσ ′ ), . . . , Γ(t n σσ ′ )), therefore, [Eσσ ′ ] J = f I ([Γ(t 1 σσ ′ )] I , . . . , [Γ(t n σσ ′ )] I ). For i ∈ [1, n], if t i is a nesting term then by the result above [Γ(t i σσ ′ )] I = [t i σσ ′ ] J and by the induction hypothesis, [Γ(t i σσ ′ )] I = [t i σ θθ ′ ] I .
Otherwise, t i is a base term, and must necessarily be a variable, thus

Γ(t i σ) = t i σ θ. Therefore Γ(t i σσ ′ ) = Γ(t i σ) = t i σ θ = t i σ θθ ′ . Therefore [Eσσ ′ ] J = f I ([t 1 σ θθ ′ ] I , . . . , [t n σ θθ ′ ] I ) = [E σ θθ ′ ] I . -The proof is similar if E is of the form t ≃ s, t ≃ s of n i=1 l i . We thus conclude that for every clause D ∈ S ∪{C}∪Ax(I), J |= Dσσ ′ iff I |= D σ θθ ′ . Since I |= S σ θ ∪ Ax(I N ), we deduce that J |= Sσ ∪ Ax(I N ), which proves that J ∈ I N . Since I |= C σ θ we have J |= Cσ, which is impossible because J ∈ I N and Sσ |= N Cσ.

Completeness of ΘB for ω-Clauses

In this section, we prove that any procedure that is base-complete is also complete for some classes of sets of possibly infinite ω-clauses -this is of course not the case in general. We first notice that the notation S ⋆ ∨ of Definition 9 can be extended to ωclauses, by allowing infinite disjunctions: Definition 13. Given a set of clauses, S, we denote by S ω ∨ the set of ω-clauses12 of the form

{C i σ i | i ∈ N, C i ∈ S, σ i is a pure substitution}. ✸
The notation S ↓G also extends to ω-clauses: S ↓G is the set of ω-clauses Cσ such that C ∈ S and σ maps every variable in C to a term in G. Proposition 14. Let S be a finite set of clauses and G be a finite set of terms. Then S ω ∨ ↓G is a finite set of clauses.

PROOF. By definition, any literal occurring in S ω

∨ is of the form Lσ where L is a literal occurring in a clause C ∈ S and σ is a pure substitution. Thus any literal occurring in S ω ∨ ↓G is of the form Lσθ where L is literal occurring in a clause in S, σ is pure and θ maps every variable to a term in G. Obviously, since G and S are finite, there are finitely many literals of this form. Hence all the ω-clauses in S ω ∨ ↓G are actually finite, and there are only finitely many possible clauses.

Lemma 15. Let S be a finite set of clauses and S ′ a set of ω-clauses with S ′ ⊆ S ω ∨ . If G is a finite set of terms, then there exists a finite set of clauses S ′′ S ′ such that S ′′ ↓G = S ′ ↓G .

PROOF. Let C be a clause in S ′ ↓G ; by Proposition 14, C is finite. By definition there exists an ω-clause C ′ ∈ S ′ such that C = C ′ θ, where θ is a substitution mapping all the variables in Var(C ′ ) to a term in G. Every literal in C ′ is of the form Lγ, where literal L occurs in S and γ is a pure substitution of Var(L). Since S and G are finite, there is a finite number of possible pairs (L, γθ). Thus there exists a finite subset D C ⊆ C ′ such that for every literal Lγ occurring in C ′ , there exists a literal Lγ ′ ∈ D C with γθ = γ ′ θ.

Every variable occurring in a literal Lγ of C ′ is of the form xγ, where x ∈ Var(L). Let η C be the substitution mapping every variable

xγ ∈ Var(C ′ \ D C ) to xγ ′ . Then for every literal Lγ ∈ C ′ , we have Lγη C = Lγ ′ ∈ D C . Thus C ′ η C = D C ; furthermore, η C is pure and D C η C = D C .
We define

S ′′ = {D C | C ∈ S ′ ↓G }; obviously S ′′ S ′
and by definition S ′′ ↓G ⊇ S ′ ↓G . Conversely, let E be a clause in S ′′ ↓G , E is necessarily of the form D C θ where C ∈ S ′ ↓G and θ maps every to a term in G. But then E is of the form C ′ η C θ, where C ′ ∈ S ′ , and η C θ is a substitution mapping every variable in C ′ to a term in G; thus E must occur in S ′ ↓G .

The next lemma proves the completeness result for ω-clauses: Lemma 16. Let Θ be a base-complete instantiation procedure (with Θ(S) = S ↓G S ) and S be a finite set of clauses. If S ′ ⊆ S ω ∨ then S ′ and S ′ ↓G S are B-equisatisfiable. Note that the clauses in S are finite, but those in S ′ may be infinite. PROOF. S ′ ↓G S is a logical consequence of S ′ , thus if S ′ is satisfiable then so is S ′ ↓G S ; we now prove the converse. Let I be an interpretation validating S ′ ↓G S . By Lemma 15, there exists a set of clauses S ′′ such that S ′′ S ′ and S ′ ↓G S = S ′′ ↓G S . Since I |= S ′ ↓G S , we deduce that S ′′ ↓G S is satisfiable, hence (since by Condition 1 in Definition 11, Θ is complete13 ) so is S ′′ . But S ′′ S ′ therefore by Proposition 3, S ′ is satisfiable.

Example 17. Assume for instance that C B is the specification of Bernays-Schönfinkel clause sets (interpreted in the usual way). Then the procedure replacing all variables by every constant symbol 14 is base-complete. Lemma 16 proves that this procedure is also complete for sets of infinite clauses constructed over C B . For instance, the satisfiability of the set S = {¬p(x i , y) | i ∈ N} ∪ {p(a, b)} can be decided by instantiating all variables x i , y by a and b. Although S contains an infinite clause, the instantiated clauses are finite, since the number of constants is finite.

Main Proof

We are now in the position to give the proof of the main theorem. For the reader's convenience, this theorem is stated again below: Theorem 1. Let Θ B be a base-complete instantiation procedure (for B) and let Θ N be a nesting-complete instantiation procedure (for

N ). Then Θ N [Θ B ] is complete for N [B];
furthermore, this procedure is monotonic and S B -invariant.

PROOF. Let Θ def = Θ N [Θ B ]
and let S be an unsatisfiable clause set in C. We prove that Θ(S) is also unsatisfiable.

Let I ∈ I B , by Lemma 7, the set

S| I = {C N η | C ∈ S, η ∈ Φ I (C)} is N -unsatisfiable,
and by completeness of Θ N , so is Θ N (S| I ). We define

A I = Cηθ | C ∈ S, C N ηθ ∈ Θ N (S| I ) .
This set may be infinite, since no assumption was made on the decidability of N (for instance, if N is first-order logic, then obviously no complete instantiation procedure can be terminating, thus Θ N (S| I ) -and therefore also A I -can be infinite). Every clause in A I is of the form Cηθ where I |= C B η,15 and by Proposition 4, Cηθ = Cσσ ′ , where σ is a nesting substitution and σ ′ is a base substitution. In particular, since dom

(σ) ⊆ X N , C B σσ ′ = C B σ ′ and I |= C B σ ′ .
By construction, the set

{C N σσ ′ | (C N ∨ C B )σσ ′ ∈ A I } is N -unsatisfiable. Thus for every model J of A I , there exists a clause (C N ∨ C B )σσ ′ ∈ A I such that J |= C N σσ ′ , hence J |= C B σσ ′ (since J |= A I we have J |= (C N ∨ C B )σσ ′ ). Since the C B cannot contain nesting variables, we have C B σσ ′ = C B σ ′ . Hence A I |= N Cσσ ′ ∈A I C B σ ′ .
We let T = S B and define:

B I = Cσ σ ′ | Cσσ ′ ∈ A I and E I = Cσσ ′ ∈A I C B σ ′ .
Note that since A I may be infinite, E I is an ω-clause that belongs to T ω ∨ . Lemma 12 guarantees that B I |= r E I ; thus by definition, for all sets of ground base terms G, B I ↓G |= N E I ↓G . This is in particular the case for G = G T .

Let U = {E I | I ∈ I B }; by construction, for all I ∈ I B , I |= U ; hence U is Bunsatisfiable and since U ⊆ T ω ∨ , by Lemma 16, U ↓G T is also B-unsatisfiable (notice that T is finite, since the base theory only contains finite sets of clauses). We have shown that B I ↓G |= N E I ↓G . This, together with the fact that

U ↓G T = I∈I B E I ↓G T per- mits to deduce that I∈I B B I ↓G T |= N U ↓G T . Since U ↓G T is B-unsatisfiable (hence also N [B]-unsatisfiable), I∈I B B I ↓G T is N [B]-unsatisfiable.
There remains to prove that I∈I B B I ↓G T ⊆ Θ(S) to obtain the result. Consider the function α that maps every term of a sort s ∈ S B to • s ; it is clear that α(S| I ) ⊆ S N γ • . In particular, if C N σσ ′ ∈ Θ N (S| I ), then by the S B -invariance and monotonicity of Θ N ,

C N σ σ ′ γ • = α(C B σσ ′ ) ∈ Θ N (α(S| I )) ⊆ Θ N (S N γ • ).
Therefore, (Cσ σ ′ ) ↓G T ⊆ Θ(S), hence the result.

The fact that Θ N [Θ B ] is S B -invariant and monotonic follows immediately from the definition and from the fact that Θ N is S B -invariant and that Θ B and Θ N are monotonic.

APPLICATIONS

In this section, we show some examples of applications of Theorem 1 that are particularly relevant in the context of program verification.

Examples of Base-Complete Specifications

5.1.1. Presburger Arithmetic. No base-complete instantiation procedure can be defined for the specification A Z as defined in Section 2.5, as evidenced by the following example.

Example 1. Assume that a base-complete procedure Θ exists, and consider the clause set S = {x ≃ y + 1, y ≃ 0}. Since Θ is base-complete by hypothesis, by Definition 11, Θ(S) = S ↓G S for some finite set of ground terms G S , and by Condition 3, G S contains G S ⋆ ∨ . But S ⋆ ∨ contains in particular the clause:

C n : n i=1 x i ≃ x i-1 + 1 ∨ x 0 ≃ 0. C n is obviously A Z -unsatisfiable (since the x i 's denote universally quantified variables), but the only instance of C n that is A Z -unsatisfiable is: C n {x i → i | i ∈ [0, n]}. Consequently {i | i ∈ [0, n]} ⊆ G S hence G S cannot
be finite, thus contradicting Definition 11.

It is however possible to define base-complete procedures for less general specifications, that are still of a practical value.

Definition 2. Let χ be a special constant symbol of sort int, let m be a natural number distinct from 0 and let T B be a set of ground terms of sort int not containing χ. We denote by B Z the specification

(I ′ Z , C ′ Z ) defined as follows. Ax(I ′ Z ) def = Ax(I Z ) ∪ {χ > t + m | t ∈ T B },
where Ax(I Z ) is defined in Example 8 (Section 2.5). C ′ Z contains every clause set S such that every non-ground literal occurring in a clause in S is of one of the following forms:

x ≤ t or t ≤ x for some variable x and for some ground term t ∈ T B ; -x ≤ y for some variables x, y; -x ≃ k t for some k ∈ N \ {0} that divides m, some ground term t ∈ T B and some variable x. ✸

Intuitively, the constant χ occurring in Ax(I ′ Z ) is meant to translate the fact that the terms appearing in S admit an upper bound (namely χ). It is clear that if S is an arbitrary set of arithmetic clauses (not containing the special constant χ), then the set T B and the integer m can be computed so that S indeed belongs to C ′ Z . Definition 3. For every set of clauses S ∈ C ′ Z , let B S be the set of ground terms t such that either t = χ or S contains an atom of the form x ≤ t. We define the instantiation procedure Θ Z by: Θ Z (S)

def = S ↓G Z S , where G Z S is defined by: G Z S def = {t -l | t ∈ B S , 0 ≤ l < m}. ✸
The two following propositions are straightforward consequences of the definition:

Proposition 4. If S ⊆ S ′ then G Z S ⊆ G Z S ′ . Proposition 5. G Z S = G Z S ⋆
∨ . PROOF. This is immediate because the set of ground terms occurring in S ⋆ ∨ is the same as that of S, since the atoms in S ⋆ ∨ are pure instances of atoms in S.

Thus B S ⋆ ∨ = B S . Theorem 6. Θ Z is base-complete if B = B Z .
PROOF. We adopt the following notations for the proof: given a set of terms W , we write x ≤ W for t∈W x ≤ t and x ≥ W for t∈W x ≥ t. Additionally, if K is a set of pairs (k, t) ∈ N × T int then we denote by ¬K(x) the disjunction (k,t)∈K x ≃ k t.

Let S ∈ C ′ Z and assume that S is B Z -unsatisfiable, we prove that Θ Z (S) is also B Zunsatisfiable. Let I ∈ I ′ Z , then in particular,

I |= {χ > t + m | t is a ground term in S}. Let C be a clause in S such that I |= C. By definition of C ′ Z , C can be written as C = D ∨ n i=1 (x i ≤ U i ∨ x i ≥ L i ∨ ¬K i (x i ))
, where D is ground and where the x i 's (1 ≤ i ≤ n) denotes distinct variables 16 . Since I |= C, there exists a ground substitution θ such that I |= Cθ, i.e., for all i ∈ [1, n]:

-∀u ∈ U i , [x i θ] I ≤ [u] I ; -∀l ∈ L i , [l] I ≤ [x i θ] I ; -∀(k, t) ∈ K i , [x i θ] I ≃ k [t] I . If [x i θ] I is such that [x i θ] I > [χ] I ,
then it is straightforward to verify that [x i θ] Im satisfies the same conditions, since for all terms t in U i ∪ L i , [χ] Im > [t] I , and since m is a common multiple of every k occurring in K i . We may therefore assume that

[x i θ] I ≤ [χ] I .
We denote by u i an element in

U i ∪ {χ} such that [u i ] I is minimal in {[u] I | u ∈ U i ∪ {χ}},
and by m i the greatest integer such that m i ≤ [u i ] I and for every (k, t) ∈ K i , m i ≃ k t holds; the existence of m i is guaranteed by what precedes and [x i θ] I ≤ m i . We cannot have m i + m ≤ u i , because otherwise m i would not be the greatest integer satisfying the conditions above. Thus, necessarily, m i > [u i ] Im, and there must exist

a term v i ∈ G Z S such that [v i ] I = m i . Let σ def = {x i → v i | i ∈ [1, n]}, we deduce that I |= Cσ. Since Cσ ∈ S ↓G Z
S , we conclude that S ↓G Z S is B Z -unsatisfiable, hence the result. We have shown that Condition 1 of Definition 11 is satisfied. By construction, G Z S is finite. By Propositions 4 and 5, Conditions 2 and 3 are satisfied, respectively, which concludes the proof.

5.1.2. Term Algebra with Membership Constraints. We give a second example of a specification for which a base-complete instantiation procedure can be defined. We consider formulae built over a signature containing:

-a set of free function symbols Σ; -a set of constant symbols interpreted as ground terms built on Σ; -a set of monadic predicate symbols P, each predicate p in P is interpreted as a (fixed) set p of ground terms built on Σ. We assume that the emptiness problem is decidable for any finite intersection of these sets (for instance p can be the set of terms accepted by a regular tree automaton, see [START_REF] Comon | Tree automata techniques and applications[END_REF]] for details).

From a more formal point of view:

Definition 7. Let Σ ⊆ F B .
We denote by T(Σ) s the set of ground terms of sort s built on Σ. Let P be a finite set of unary predicate symbols, together with a function p → p mapping every symbol p : s → bool ∈ P to a subset of T(Σ) s .

We denote by A ∈ the specification (I ∈ , C ∈ ) where:

-Ax(I ∈ ) contains the following axioms:

t∈T(Σ)s x ≃ t for s ∈ S B , x ∈ X B , x i ≃ y i ∨ f (x 1 , . . . , x n ) ≃ f (y 1 , . . . , y n ) if f ∈ Σ, i ∈ [1, n] p(t) if p ∈ P, t ∈ p. ¬p(t) if p ∈ P, t ∈ p.
-Every non-ground atom in C ∈ is of the form ¬p(x), or of the form x ≃ t for some ground term t. ✸

The axioms of Ax(I ∈ ) entail the following property which is proved by a straightforward induction on the depth of the terms: Proposition 8. For all interpretations I ∈ I ∈ and all terms t, t ′ occurring in a clause in

C ∈ , if [t] I = [t ′ ] I then t = t ′ .
If the sets in {p | p ∈ P} are regular then A ∈ is well-known to be decidable, see, e.g., [START_REF] Comon | Equational formulae with membership constraints[END_REF]. We define the following instantiation procedure for A ∈ : Definition 9. For every clause set S, Θ ∈ (S) def = S ↓G ∈ S , where G ∈ S is the set of ground terms containing:

-Every ground term t such that S contains an atom of the form x ≃ t.

-An arbitrarily chosen ground term s P ∈ p∈P p, for each P ⊆ P such that p∈P p = ∅ (recall that the emptiness problem is assumed to be decidable).

✸ Theorem 10. Θ ∈ is base-complete if B = A ∈ . PROOF. Let C be a clause in C ∈ , C is of the form n i=1 x i ≃ t i ∨ m i=1 ¬p i (y i ) ∨ D where D is ground, x i and y j (i ∈ [1, n], j ∈ [1, m]) are variables, t i is a ground term for i ∈ [1, n] and p j ∈ P for j ∈ [1, m]. Let X = {x 1 , . . . ,
x n } and Y = {y 1 , . . . , y m }; note that these sets are not necessarily disjoint. For every variable y ∈ Y we denote by P y the set of predicates p j (1 ≤ j ≤ m) such that y j = y and we let s y def = s Py . Consider the substitution σ of domain X ∪ Y such that:

-x i σ def = t i for every i ∈ [1, n]; -if y ∈ Y \ X then yσ
∈ S = G ∈ S ⋆ ∨ and G ∈ S ⊆ G ∈ S ′ if S ⊆ S ′ .
Hence all the conditions of Definition 11 are satisfied.

Combination of Specifications

Building on the results of the previous section, we now provide some concrete applications of Theorem 1.

5.2.1. Combining First-order Logic without Equality and Presburger Arithmetic. We begin with a simple example to illustrate how the method works, by showing how to enrich the language of first-order predicate logic with some arithmetic constraints. We assume that F contains no function symbol of co-domain int other than the usual symbols 0, s, +,introduced in Section 2.5.

Let N fol be the restriction of the specification A fol defined in Example 7 to nonequational clause sets (i.e. to clause sets in which all atoms are of the form t ≃ true). We consider the combination N fol [B Z ] of the specification B Z introduced in Section 5.1.1 with N fol . According to Theorem 6, Θ Z is base-complete for B Z ; thus, in order to apply Theorem 1, we only need to find a nesting-complete instantiation procedure for N fol . We will use an instantiation procedure based on hyper-linking [START_REF] Lee | Eliminating duplication with the hyper-linking strategy[END_REF]. It is defined by the following inference rule:

n i=1 l i , m 1 ∨ C 1 , . . . , m n ∨ C n n i=1 l i σ if σ is an mgu. of the (l i , m c i )'s.
If S is a set of clauses, we denote by Θ ′ fol (S) the set of clauses that can be obtained from S by applying the rule above (in any number of steps) and by Θ fol (S) the set of clauses obtained from Θ ′ fol (S) by replacing all remaining variables of sort s by a constant symbol ⊥ s of the same sort.

Proposition 11. Θ fol is nesting-complete for N fol .

PROOF. In [START_REF] Lee | Eliminating duplication with the hyper-linking strategy[END_REF], it is proven that S and Θ fol (S) are equisatisfiable, thus Condition 1 of Definition 6 holds; furthermore, by definition, Θ fol is monotonic. To verify that Θ fol is S B -invariant, it suffices to remark that if a clause D is deducible from a set of clauses S by the instantiation rule above, then for every S Bmapping α, α(D) must be deducible from Θ fol (α(S)), since the unifiers are not affected by the replacement of ground terms: if an mgu maps a variable x to a term t in S, then the corresponding mgu will map x to α(t) in α(S).

Theorem 1 guarantees that Θ fol [Θ Z ] is complete for N fol [B Z ]. Note that in general, Θ fol [Θ Z ]
(and Θ fol ) are not terminating. However, Θ fol [Θ Z ] is terminating if the set of ground terms containing no subterm of sort int (and distinct from • int ) is finite (for instance if F contains no function symbol of arity greater than 0 and of a sort distinct from int).

Example 12. Consider the following set of clauses S, where i, j denote variables of sort int, x, y denote variables of sort s, and F contains the following symbols: a, b : int, c, d : s, p : int × s → bool and q : int × s × s → bool.

(1) ¬p(i, x) ∨ ¬q(i, y) ∨ r(i, x, y) (2) p(a, c) (3) j < b ∨ q(j, d) (4) i ≃ 2 0 ∨ ¬r(i, x, y)
Clauses ( 2) and (3) are not in N fol [B Z ]. Indeed, the non-arithmetic atom p(a, c) contains a non-variable arithmetic subterm a and (3) contains a literal j < b that is not allowed in B Z (see Definition 2). Thus these clauses must be reformulated as follows:

(

2)' i ≤ a ∨ a ≤ i ∨ p(i, c) (3)' j ≤ b -1 ∨ q(j, d)
To apply the procedure Θ fol [Θ Z ], we compute the set S N and replace every arithmetic variable occurring in it by a special constant • of sort int:

S N =      ¬p(•, x) ∨ ¬q(•, y) ∨ r(•, x, y) p(•, c) q(•, d) ¬r(•, x, y)
We apply the procedure Θ fol . The reader can verify that we obtain the following clause set:

Θ fol (S N ) =              ¬p(•, ⊥) ∨ ¬q(•, ⊥) ∨ r(•, ⊥, ⊥) p(•, c) q(•, d) ¬r(•, ⊥, ⊥) ¬p(•, c) ∨ ¬q(•, d) ∨ r(•, c, d) ¬r(•, c, d) Next we consider the clauses in S B : {i ≤ a ∨ a ≤ i, j ≤ b -1, i ≃ 2 0}
¬p(a, ⊥) ∨ ¬q(a, ⊥) ∨ r(a, ⊥, ⊥) p(a, c) ¬p(b -1, ⊥) ∨ ¬q(b -1, ⊥) ∨ r(b -1, ⊥, ⊥) p(b -1, c) ¬p(a -1, ⊥) ∨ ¬q(a -1, ⊥) ∨ r(a -1, ⊥, ⊥) p(a -1, c) ¬p(b -2, ⊥) ∨ ¬q(b -2, ⊥) ∨ r(b -2, ⊥, ⊥) p(a -2, c) ¬r(a, ⊥, ⊥) ¬r(a, c, d) ¬r(b -1, ⊥, ⊥) ¬r(b -1, c, d) ¬r(a -1, ⊥, ⊥) ¬r(a -1, c, d) ¬r(b -2, ⊥, ⊥) ¬r(b -2, c, d) ¬p(a, c) ∨ ¬q(a, d) ∨ r(a, c, d) q(a, d) ¬p(b -1, c) ∨ ¬q(b -1, d) ∨ r(b -1, c, d) q(b -1, d) ¬p(a -1, c) ∨ ¬q(a -1, d) ∨ r(a -1, c, d) q(a -1, d) ¬p(b -2, c) ∨ ¬q(b -2, d) ∨ r(b -2, c, d) q(b -2, d)
The resulting set of clauses is N fol [B Z ]-unsatisfiable, hence, so is S.

5.2.2. Arrays with Integer Indices and Uninterpreted Elements. The specification of arrays with integer indices and uninterpreted elements can be defined as a hierarchic expansion of the base specification B Z defined in Section 5.1.1 with a simple specification N A = (I fol , C A ), where the clauses in C A are built on a set of variables of sort int, on a signature containing only constant symbols of sort array or elem and a function symbol select : array × int → elem. We have assumed that C A contains no occurrence of the function symbol store for convenience. There is no loss of generality: indeed, every definition of the form s = store(t, i, a) where s, t, i, a are ground terms can be written as the conjunction of the following clauses:

select(s, i) = v i + 1 ≤ z ∨ select(s, z) ≃ select(t, z) z ≤ i -1 ∨ select(s, z) ≃ select(t, z)
It is simple to verify that these three clauses are in C A . Obviously, the last two clauses are equivalent to z ≃ i ∨ select(s, z) ≃ select(t, z).

There exists a straightforward nesting-complete instantiation procedure for N A : namely the identity function id(S) def = S. This is indeed an instantiation procedure since all the variables occurring in C A are of type int; these variables will already be instantiated by the instantiation procedure for B Z and the remaining clause set will be ground. The following result is a direct consequence of Theorem 1:

Proposition 13. id[Θ Z ] is complete for N A [B Z ].
We provide some examples of properties that have been considered in [START_REF] Bradley | The Calculus of Computation: Decision Procedures with Applications to Verification[END_REF][START_REF] Habermehl | What else is decidable about integer arrays?[END_REF]Ghilardi et al. 2007b], and can be expressed in N A [B Z ] (t,t ′ denotes constant symbols of sort array).

(I ′

Z , C Z ) where Ax(I ′ Z ) is the image of Ax(I Z ) by the previous transformation and where the clause sets in C Z A are built on a set of variables of sort int and on a signature containing all function symbols 0 ′ , s ′ , ≤ ′ ,. . . in Ax(I ′ Z ), constant symbols of sort array or int ′ and a function symbol select : array × int → int ′ . Then N Z A [B Z ] is a specification of arrays with integer indices and integer elements, and by Theorem 1, id[Θ Z ] is complete for N Z A [B Z ]. Note however that, due to the fact that the sort symbols are renamed, equations between integer elements and integer indices are not permitted: indices cannot be stored into arrays and terms of the form select(t, select(t, i)) are forbidden. However, the sharing of a constant symbol c between the two sorts int and int ′ (as in the equation: select(t, c) ≃ c) is possible, by adding ground axioms of the form: k ≃ c ⇒ k ′ ≃ c ′ , where c ′ denotes the copy of c, k is any integer in int and k ′ denotes its copy in int ′ . Let A denote this set of axioms; it is obvious that A is countably infinite. It is clear that id[Θ Z ](S ∪ A) = id[Θ Z ](S) ∪ A, so that the instantiation procedure is not affected by this addition. Thus these axioms can be simply removed afterward by "merging" int and int ′ and by replacing c ′ by c (it is straightforward to verify that this transformation preserves satisfiability).

We provide some examples. ≤ ′ and + ′ are renaming of the symbols ≤ and + respectively. Notice that the indices of the arrays are of sort int, whereas the elements are of sort int ′ . The following properties can be expressed in N Z A [B Z ]: (1) ∀i, j, i ≤ j ∨ select(t, i) ≤ ′ select(t, j) Array t is sorted.

(2) ∀i, j, a

≤ i ∨ i ≤ b ∨ c ≤ j ∨ j ≤ c ∨ select(t, i) ≤ ′ select(t ′ , j)
The values of t at [a, b] are lower than those of t ′ at [c, d].

(3) ∀i, i ≃ 2 0 ∨ i ≤ n ∨ select(t, i) ≃ ′ select(t ′ , i) + ′ select(t ′′ , i) For every even index lower than n, t is the sum of t ′ and t ′′ .

Here are some examples of properties that cannot be handled:

(4) ∀i, select(t, i) ≃ i Array t is the identity.

(5) ∀i, select(t, i)select(t, i + 1) ≤ 2 The distance between the values at two consecutive index is at most 2.

Property (4) is not in N Z

A [B Z ] because there is an equation relating an element of sort int (i.e. an index) to an element of sort int ′ = int (an element). Property (5) could be expressed in our setting as ∀i, j, j ≃ i + 1 ∨ select(t, i)select(t, j) ≤ 2 but the atom j ≃ i + 1 is not in B Z . Property (5) can be expressed in the logic LIA (see [START_REF] Habermehl | What else is decidable about integer arrays?[END_REF]). This shows that the expressive power of this logic is not comparable to ours.

These results extend straightforwardly to multidimensional arrays.

5.2.4. Arrays with Translations on Arrays Indices. In some cases, properties relating the value of an array at an index i to the value at index i + k for some natural number k can be expressed by reformulations.

Definition 15. Let S be a clause set, containing clauses that are pairwise variabledisjoint. Let λ be a function mapping every array constant to a ground term of sort int. S is shiftable relatively to λ iff the following conditions hold:

(1) Every clause in S is of the form C ∨ D, where D is a clause in N Z A and every literal in C is of one of the following form: i ≤ j + s, i ≤ s, s ≤ i, i ≃ k s, where i, j are variables of sort int, s is a ground term of sort int and k is a natural number. At this point, ≤ ′ may be simply replaced by ≤ (this operation obviously preserves equisatisfiability) and the resulting clause set can be refuted by any SMT-solver handling ground equality and integer arithmetic.

Such nested array reads are outside the scope of the Array property fragment of [START_REF] Bradley | The Calculus of Computation: Decision Procedures with Applications to Verification[END_REF] and of the Logic LIA of [START_REF] Habermehl | What else is decidable about integer arrays?[END_REF]. They are not subsumed either by the extensions of the theory of arrays considered in [Ghilardi et al. 2007b]. Note that, due to the fact that we use distinct renamings of the specification of integers, equations such as select(t ′ , select(t, a)) ≃ select(t ′ , a) are forbidden (if arrays are viewed as heaps, this means that there can be no equation between pointers and referenced values).

DISCUSSION

In this paper we have introduced a new combination method of instantiation schemes and presented sufficient conditions that guarantee the completeness of the resulting procedure. As evidenced by the examples provided in Section 5, this combination method permits to obtain instantiation procedures for several theories that are quite expressive, at almost no cost. One direct consequence of these results is that it should be possible for developers of SMT solvers to focus on the design of efficient decision procedures for a few basic theories, such as, e.g., the theory of equality with uninterpreted function symbols (EUF) or Presburger arithmetic, and obtain efficient SMT solvers for a large panel of theories.

This combination method may seem inefficient, since exponentially many ground clauses may be generated, except for the trivial cases. An interesting line of research is to investigate how incremental techniques can be implemented and the instantiations controlled so that the (un)satisfiability of the clause set under consideration can be detected before all clauses are instantiated in all possible ways. For instance, we believe it is possible -but this will probably depend on B and N -to devise more subtle strategies that first replace base variables with the constants • s and apply the instantiation procedure for N , and then derive additional information from the resulting set of ground clauses to avoid having to instantiate all base variables in all possible ways. Further investigations into this line of work could lead to the design of more powerful instantiation procedures that could enlarge the scope of modern SMT solvers by making them able to handle efficiently more expressive classes of quantified formulae. The idea is to use the models constructed by the SMT-solvers to guide the generation of new instances. Techniques such as those described in [START_REF] Plaisted | Ordered semantic hyperlinking[END_REF][START_REF] Ganzinger | New directions in instantiation-based theorem proving[END_REF] (for first-order logic with equality) and [START_REF] Jacobs | Incremental instance generation in local reasoning[END_REF][START_REF] Sofronie-Stokkermans | Hierarchic reasoning in local theory extensions[END_REF] (for local reasoning) could be used to that end, and we believe this to be a fruitful line of research.

Definition 2 .

 2 An ω-clause is a possibly infinite set of literals. ✸ The notion of instance extends straightforwardly to ω-clauses: if C is an ω-clause then Cσ denotes the ω-clause {Lσ | L ∈ C} (recall that the domain of σ may be infinite). Similarly, the semantics of ω-clauses is identical to that of standard clauses: if C is a ground ω-clause, then [C] I def = true iff there exists an L ∈ C such that [L] I = true. If C is a non-ground ω-clause, then I |= C iff for every ground substitution of domain Var(C), [Cσ] I = true. The notions of satisfiability, models etc. are extended accordingly. If S, S ′ are two sets of ω-clauses, we write S S ′ if for every ω-clause C ′ ∈ S ′ there exists an ω-clause C ∈ S such that C ⊆ C ′ . Proposition 3. If S S ′ then S ′ is a logical consequence of S.

Definition 5 .

 5 A specification A = (I, C) is ω-definable iff there exists a (possibly infinite) set of ω-clauses Ax(I) such that I = {I | I |= Ax(I)}.

  the base part of the clause and C N is its nesting part. If S is a set of clauses in C, then S B and S N respectively denote the sets {C B | C ∈ S} and {C N | C ∈ S}, and are respectively called the base part and nesting part of S. ✸ It is easy to check that for every clause C occurring in a clause set in C, there exist two unique clauses C B and C N such that C = C B ∨ C N . Example 4. Consider the following clauses:

  (3) All the substitutions on nesting variables from Step 2 are applied to the initial set of clauses. Notice that base variables are not instantiated. Furthermore, the constant • can appear in the obtained clause set (it will the eliminated during the next step). (4) Assuming the instantiation procedure for B is base-complete, if this procedure was applied to the base part of the clauses, then by Definition 11, the base variables in the base part of the clauses would be uniformly instantiated by some set of terms G. All base variables and all occurrences of constants • (occurring in the co-domainInstantiation schemes for nested theories 0:13 of a substitution generated during the previous step) are replaced by all possible terms in G. All occurrences of every variable are mapped to the same term, which ensures that all the generated clauses are instances of the original ones.Example 12. Assume that B = A Z , N = A fol and that F contains the following symbols: a : int, b : int, c : s and p : int×s → bool. Consider the set S = {x ≤ a∨p(x, y), u ≤ b ∨ ¬p(u, c)}. The instantiation procedures for B and N are assumed to be given (formal definitions and proofs will be given later).(1) We compute the set S N = {p(x, y), ¬p(u, c)} and replace every base variable by •. This yields the set: {p(•, y), ¬p(•, c)}. (2) We apply an instantiation procedure for A fol 6 . Obviously, this procedure should instantiate the variable y by c, yielding {p(•, c), ¬p(•, c)}. (3) We apply the (unique in our case) substitution y → c to the initial clauses: {x ≤ a ∨ p(x, c), u ≤ b ∨ ¬p(u, c)}. Note that at this point all the remaining variables are in X B . (4) We compute the set of clauses S B = {x ≤ a, u ≤ b} and the set of terms G S B . It should be intuitively clear 7 that x must be instantiated by a and u by b, yielding G S B = {a, b}. (5) We thus replace all base variables by every term in {a, b} yielding the set {a ≤ a ∨ p(a, c), b ≤ a ∨ p(b, c), a ≤ b ∨ ¬p(a, c), b ≤ b ∨ ¬p(b, c)}, i.e., after simplification, {p(a, c), b ≤ a ∨ p(b, c), a ≤ b ∨ ¬p(a, c), ¬p(b, c)}. It is straightforward to check that this set of clauses is unsatisfiable. Any SMT-solver capable of handling arithmetic and propositional logic can be employed to test the satisfiability of this set.

( 3 )

 3 If S| I is unsatisfiable for every I then Θ B (U ) is unsatisfiable: By construction, for every clause C N η ∈ Θ N (S| I ), the set of ground instances of S will contain a clause of the form (C B ∨C N )η, where I |= C B η. Thus, since Θ N (S| I ) is contradictory, it follows that the disjunction of the clauses C B η, where C N η ranges over the whole set Θ N (S| I ), is a logical consequence of S, and more precisely of the instances of S that are obtained by applying the grounding substitutions generated by Θ N . For instance, if S = {0+1 ≃ 1∨p(x), 0 ≃ 1∨¬p(a)∨p(y), ¬p(b)}, then S| I = {p(x), ¬p(a)∨ p(y), ¬p(b)}, Θ N (S| I ) = {p(a), ¬p(a)∨p(b), ¬p(b)}, and we have {0+1 ≃ 1∨p(a), 0 ≃ 1 ∨ ¬p(a) ∨ p(b), ¬p(b)} |= 0 + 1 ≃ 1 ∨ 0 ≃ 1.

  We get: {¬p(a, a), ¬p(a, a) ∨ ¬p(b, a), ¬p(b, a), ¬p(a, b), ¬p(a, b) ∨ ¬p(b, b), ¬p(b, b), p(a, b)}.

  def = s y (notice that s y must be defined since y ∈ Y ) We prove that Cσ |= A∈ C. Let I be an interpretation such that I |= Cσ and I |= C. Then there exists a substitution θ such that I |= Cθ, which implies that for all i ∈ [1, n], [x i θ] I = [t i ] I , and for all j ∈ [1, m], [y j θ] I ∈ [ pj ] I . Proposition 8 entails that x i θ = t i for all i ∈ [1, n], and y j θ ∈ pj for all j ∈ [1, m]. Thus, in particular, for all x ∈ X, xσ = xθ, and for all y ∈ Y \ X, p∈Py p = ∅. Since I |= Cσ and x i σ = t i for all i ∈ [1, n], there must exist a j ∈ [1, m] such that [y j σ] I ∈ [ pj ] I ; and, again by Proposition 8, this is equivalent to y j σ / ∈ pj . If y j ∈ X, then y j θ = y j σ / ∈ pj and I |= Cθ, which is impossible. Thus y j ∈ Y \ X, and since p∈Py j p = ∅, by construction, y j σ = s yj ∈ pj ; this contradicts the assumption that y j σ / ∈ pj . Since Cσ |= A∈ C, we deduce that for every clause C ∈ S, there exists a D ∈ S ↓G ∈ S such that D |= A∈ C, and therefore, S ≡ A∈ S ↓G ∈ S . By construction, G ∈ S is finite, G

  and compute the set G Z S B Z , according to Definition 3. The terms occurring as the right operands of a symbol ≤ are {a, b -1}. The least common multiple of all the natural numbers k such that S B contains a comparison modulo k is 2. Thus G Z S B Z = {a, b -1, a -1, b -2}. To get the clause set Θ[Θ Z ](S), the substitutions generated by Θ are combined with all instantiations of integer variables by elements of G Z S B Z . This yields:

a

  ≤ b ∨ select(t, a) ≤ select(t, b) b ≤ a ∨ select(t, b) ≤ select(t, a) select(t, a) ≤ select(t, a) ∨ select ′ (t ′ , select(t, a)) ≤ ′ select ′ (t ′ , select(t, a)) select(t, a) ≤ select(t, b) ∨ select ′ (t ′ , select(t, a)) ≤ ′ select ′ (t ′ , select(t, b)) select(t, b) ≤ select(t, b) ∨ select ′ (t ′ , select(t, b)) ≤ ′ select ′ (t ′ , select(t, b)) select(t, b) ≤ select(t, a) ∨ select ′ (t ′ , select(t, a)) ≤ ′ select ′ (t ′ , select(t, a)) a ≤ b select ′ (t ′ , select(t, a)) > select ′ (t ′ , select(t, b))

  An interpretation I satisfies a clause C if for every ground instance Cσ of C we have [Cσ] I = true. A set of clauses S is satisfied by I if I satisfies every clause in S. If this is the case, then I is a model of S and we write I |= S. A set of clauses S is satisfiable if it has a model; two sets of clauses are equisatisfiable if they are both satisfiable or both unsatisfiable.

  is unsatisfiable: In order to obtain the desired result, we finally show that Θ N [Θ B ](S) |= Θ B (U ). To this purpose, we remark that the entailment S |= U only depends on the nesting part of the clauses, hence holds for all possible values of the base terms, provided the relations between these terms are preserved. To formalize this property, we introduce a new notion of logical entailment, denoted by |= r , in which the base variables are handled in a "rigid" way. This is done in Section 4.4. This relation, together with the definition of Θ N [Θ B ], enables us to prove that Θ N

ACM Transactions on Computational Logic, Vol. 0, No. 0, Article 0, Publication date: 201?.

for technical convenience we do not assume that dom(σ) is finite.ACM Transactions on Computational Logic, Vol. 0, No. 0, Article 0, Publication date: 201?.

However as we shall see in Section 5, our method cannot handle such axioms, except in some very particular cases. In fact, adding axioms relating two consecutive elements of an array easily yields undecidable specifications (as shown in[START_REF] Bradley | The Calculus of Computation: Decision Procedures with Applications to Verification[END_REF]).ACM Transactions on Computational Logic, Vol. 0, No. 0, Article 0, Publication date: 201?.

Of course sort constraints must be taken into account.

See Section 5.2.1. We assume that the variables are instantiated in a uniform way, so that the conditions of Definition 11 hold.

There exist several instantiation procedures for A fol , one such example is given in Section 5.2.1.

A formal definition of an instantiation procedure for this fragment of Presburger arithmetic will be given in Section 5.1.1.ACM Transactions on Computational Logic, Vol. 0, No. 0, Article 0, Publication date: 201?.

Equal subterms may be replaced by the same variable.ACM Transactions on Computational Logic, Vol. 0, No. 0, Article 0, Publication date: 201?.

γ(e) always exists since we restricted ourselves to interpretations such that, for every s ∈ S, sI = {[t] I | t ∈ Ts} (see Section 2.2).ACM Transactions on Computational Logic, Vol. 0, No. 0, Article 0, Publication date: 201?.

It suffices, e.g., to fix a total order among variables and to map every variable x to the least variable y such that xσ = yσ.

Intuitively, J interprets every base term as itself and coincides with I on nesting terms.

By definition, any clause is an ω-clause, thus S ω ∨ is a set of ω-clauses.ACM Transactions on Computational Logic, Vol. 0, No. 0, Article 0, Publication date: 201?.

Recall that S ′′ is a set of finite clauses.

Recall that C B η = C B ηθ, since η is a ground base substitution ACM Transactions on Computational Logic, Vol. 0, No. 0, Article 0, Publication date: 201?.

Note that the sets U i , L i and K i could be empty.ACM Transactions on Computational Logic, Vol. 0, No. 0, Article 0, Publication date: 201?.

Acknowledgments

The authors wish to thank the anonymous referees for their thorough reviews and pertinent comments.

The restriction of t and t ′ to [a, b] and [c, d] respectively are disjoint. (4) ∀i, j, i ≃2 0 ∨ j ≃2 1 ∨ select(t, i) ≃ select(t, j) The values of t at even indices are disjoint from those at odd ones. (5) ∀i, i ≃2 0 ∨ select(t, i) ≃ select(t ′ , i) ∨ select(t, i) ≃ select(t ′′ , i) For every even index, the value of t is equal to the value of t ′ or t ′′ . (6) ∀i, i ≥ 0

Array map(f, t) is obtained from t by iterating function f . Arrays play a fundamental role in verification, and numerous techniques have been considered for reasoning about them. For instance, Properties (1-3) can be expressed in the Array property fragment (see [START_REF] Bradley | The Calculus of Computation: Decision Procedures with Applications to Verification[END_REF]), but not Property (4), because of condition i ≃ 2 0. Property (4) is expressible in the Logic for Integer Arrays (LIA) introduced in [START_REF] Habermehl | What else is decidable about integer arrays?[END_REF], but not Property (5), because there is a disjunction in the value formula. The combinatory array logic of [START_REF] De Moura | Generalized, efficient array decision procedures[END_REF] allows one to reason on arrays built over a combination of theories, enriched by new combinators that can express properties such as ( 1) and ( 7), but does not consider quantified formulae. [Ghilardi and Ranise 2010] contains a decidability result for a very general class of formulae with quantification on the indices, provided the theory of indices satisfies some additional properties (which do not hold for integers).

On the other hand, Properties such as Injectivity cannot be expressed in our setting:

Indeed, the literal i ≃ j is not allowed in C ′ Z . 5.2.3. Arrays with Integer Indices and Interpreted Elements. Instead of using the mere specification N A , one can combine the specification B Z with a richer specification, with function and predicate symbols operating on the elements of the arrays. For instance, consider the specification N R A = (I R , C R A ), where Ax(I R ) is some axiomatization of real closed fields over a signature F R and the clauses occurring in C R A are built on a set of variables of sort int and on a signature containing all function symbols in F R , constant symbols of sort array or real and a function symbol select :

is the specification of arrays with integer indices and real elements, and an immediate application of Theorem 1 yields:

To model arrays with integer indices and integer elements, it is necessary to use a combination of the specification B Z with a specification containing the symbols in B Z : 0 : int, s : int → int, ≤: int × int → bool, etc. However, this is not permitted in our approach since the clause sets of the nesting specification would then contain function symbols with co-domains of a sort of the base specification (namely int), thus contradicting the conditions on S B and S N (see Section 3.1). A solution is to use a copy of the sort int and of every symbol of co-domain int. We denote by N Z A the specification

(2) For every clause C ∈ S and for every literal i ≤ j + s occurring in C, where i, j are variables and s is a term of sort int, C contains two terms of the form select(t, i) and select(t ′ , j) where λ(t ′ )λ(t) is equivalent to s.

(3) If C contains two terms of the form select(t, i) and select(t

✸

The existence of such a function λ is easy to determine: conditions (2-4) above can immediately be translated into arithmetic constraints on the λ(t)'s, and the satisfiability of this set of constraints can be tested by using any decision procedure for Presburger arithmetic.

We define the following transformation of clause sets:

Definition 16. Let t → t ′ be an arbitrarily chosen function mapping all the constants t of sort array to pairwise distinct fresh constants t ′ of sort array. We denote by shift(S) the clause set obtained from S by applying the following rules:

-every clause C containing a term of the form select(t, i) (where i is a variable) is replaced by C{i → iλ(t)}; -then, every term of the form select(t, s) is replaced by select(t ′ , s + λ(t)). ✸ Lemma 17. Let S be a shiftable clause set. Then:

shift(S) and S are equisatisfiable.

-

It is clear that for every clause C in S, C ≡ C{i → i -k}: since i ranges over all integers, i and ik range over the same set. The replacement of select(t, s) by select(t ′ , s + λ(t)) obviously preserves sat-equivalence: it suffices to interpret t ′ as the array defined by the relation: select(t ′ , i) def = select(t, iλ(t)). Thus shift(S) and S are equisatisfiable.

We prove that shift(S) is in

. By Condition 3 of Definition 15, if a clause C{i → iλ(t)} contains a term of the form select(s, iλ(t)) then we must have λ(s) = λ(t), thus this term is replaced by select(s ′ , i) when the second rule above is applied. Consequently, the non-arithmetic part of the resulting clause cannot contain any non-variable term of sort int. Now assume that C contains an arithmetic literal of the form i ≤ j + s. Then by Condition 2, C also contains terms of the form select(t, i) and select(t ′ , j), where λ(t ′ )λ(t) is equivalent to s. Hence, the clause in shift(S) corresponding to C contains the literal i-λ(t) ≤ j -λ(t ′ )+s ≡ i ≤ j -(λ(t ′ )-λ(t))+s ≡ i ≤ j.

Lemma 17 shows that the satisfiability test for shiftable clause set can be reduced to a satisfiability test for a clause set in N Z A [B Z ]. This does not imply that the instantiation procedure id[Θ Z ] is complete for shiftable clause set. We provide an example in which this result applies.

Example 18. Consider for instance the following clause set:

It is simple to check that S is shiftable relatively to the mapping: λ(u) = a + a, λ(s) = a and λ(t) = 0. According to Definition 17, S is reformulated as follows:

shift(S) and S are equisatisfiable, and shift(S) belongs to

The unsatisfiability of shift(S) can be proven by applying the procedure id[Θ Z ].

5.2.5. Nested Arrays. An interesting feature of this approach is that it can be applied recursively, using nesting specifications some nested combination of other specifications: Theorem 1 ensures that the obtained instantiation procedure satisfies the required properties. This idea is similar to the chains of (local) theory extensions used in, e.g., [START_REF] Ihlemann | On local reasoning in verification[END_REF] to extend the array property fragment. Note that it would not be possible to use a nested combination of specifications as the base specification, because a nested combination of instantiation procedures is not necessarily base-complete.

We denote by B ′ Z a copy of the specification B Z in which the symbols int, 0, s, ≤, . . . are renamed into int ′ , 0 ′ , s ′ , ≤ ′ , . . . We denote by Θ ′ Z the corresponding instantiation procedure, as defined by Definition 3. Let N Z A ′ be a copy of the specification

In A Z3 , the (integer) indices of an array t can themselves be stored into arrays of integers, but of a different type than t.

Example 20. The following clause set is A Z3 -unsatisfiable (for the sake of readability we use t ≃ s as a shorthand for t ≤ s ∨ t ≤ s):

(

We describe the way the procedure works on this very simple but illustrative example. According to the definition of id[Θ ′ Z ][Θ Z ], the variables i, j, x and y are replaced by a special symbol • and the instantiation procedure id[Θ ′ Z ] is applied. The variables i ′ , j ′ , x ′ , y ′ are replaced by a constant symbol • ′ and the procedure id is applied on the resulting clause set (in a trivial way, since this set is ground). Next, we apply the procedure Θ ′ Z . According to Definition 3, Θ ′ Z instantiates the variables i ′ , j ′ , x ′ , y ′ by select(t, •). This substitution is applied to the original clause set and the procedure Θ Z is invoked. The variables i, j, x and y, and the constant symbol • are replaced by {a, b}. After obvious simplifications, we obtain the following set of instances: