Mnacho Echenim
email: mnacho.echenim@univ-grenoble-alpes.fr

Radu Iosif
email: radu.iosif@univ-grenoble-alpes.fr

Nicolas Peltier
email: nicolas.peltier@univ-grenoble-alpes.fr

The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates

Keywords: Separation logic, Bernays-Schönfinkel-Ramsey class, decision procedures, complexity, PSPACE-completeness

This paper investigates the satisfiability problem for Separation Logic with k record fields, with unrestricted nesting of separating conjunctions and implications. It focuses on prenex formulae with a quantifier prefix in the language ∃ * ∀ * , that contain uninterpreted (heap-independent) predicate symbols. In analogy with first-order logic, we call this fragment Bernays-Schönfinkel-Ramsey Separation Logic [BSR(SL k )]. In contrast with existing work on Separation Logic, in which the universe of possible locations is assumed to be infinite, we consider both finite and infinite universes in the present paper. We show that, unlike in first-order logic, the (in)finite satisfiability problem is undecidable for BSR(SL k ). Then we define two non-trivial subsets thereof, for which the finite and infinite satisfiability problems are PSPACE-complete, respectively, assuming that the maximum arity of the uninterpreted predicate symbols does not depend on the input. These fragments are defined by controlling the polarity of the occurrences of separating implications, as well as the occurrences of universally quantified variables within their scope. These decidability results have natural applications in program verification, as they allow to automatically prove lemmas that occur in e.g. entailment checking between inductively defined predicates and validity checking of Hoare triples expressing partial correctness conditions.

INTRODUCTION

Separation Logic [START_REF] Samin | BI as an assertion language for mutable data structures[END_REF][START_REF] Reynolds | Separation Logic: A Logic for Shared Mutable Data Structures[END_REF] (SL) is a logical framework used in program verification to describe properties of the dynamically allocated memory, such as topologies of data structures (lists, trees), (un)reachability between pointers, etc. In a nutshell (formal definitions are given below), given an integer k ≥ 1, the logic SL k is obtained from the first-order theory of a finite partial function h : U ⇀ U k called a heap, by adding two non-classical connectives: 1. the separating conjunction ϕ 1 * ϕ 2 , that asserts the existence of a split of the heap into disjoint heaps satisfying ϕ 1 and ϕ 2 respectively, and 2. the separating implication, or magic wand ϕ 1 -- * ϕ 2 , stating that each extension of the heap by a disjoint heap satisfying ϕ 1 must satisfy ϕ 2 .

Intuitively, the set U denotes the universe of possible of memory locations (cells) and k is the number of record fields in each memory cell. The separating connectives * and -- * may be used to express dynamic transformations of the heap. As such, they allow for concise definitions of program semantics, via weakest precondition calculi [START_REF] Samin | BI as an assertion language for mutable data structures[END_REF] and easy-to-write specifications of recursive linked data structures (e.g. singly-and doubly-linked lists, trees with linked leaves and parent pointers, etc.), when inductive definitions are added [START_REF] Reynolds | Separation Logic: A Logic for Shared Mutable Data Structures[END_REF].

Investigating the decidability and complexity of the satisfiability problem for fragments of SL is thus of great theoretical and practical interest. In contrast to first-order logic for which the decision problem has been thoroughly investigated (see, e.g., [START_REF] Börger | The Classical Decision Problem[END_REF]), only a few results are known for SL. The earliest such results show undecidability of SL k and the PSPACE-completeness of its quantifier-free fragment, for any k ≥ 2 [START_REF] Calcagno | Computability and Complexity Results for a Spatial Assertion Language for Data Structures[END_REF]. These results have been subsequently refined, by showing undecidability of SL1 , even if only two quantified variables are allowed [START_REF] Demri | Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction[END_REF]. Decidability of SL 1 is shown for the fragment without the magic wand connective, but the complexity lower bound is not elementary recursive. This lower bound drops if at most one quantified variable is allowed, in which case SL 1 is PSPACE-complete. Extending SL 1 with higher-order inductive predicates, such as reachability, leads to undecidability in the presence of the magic wand and becomes PSPACE-complete if the magic wand is not allowed [START_REF] Demri | The Effects of Adding Reachability Predicates in Propositional Separation Logic[END_REF].

A salient feature of SL is the ability of describing recursive data structures by means of inductive definitions. The axioms defining such interpreted predicates use a very restricted fragment of SL, consisting of atoms (equalities, disequalities and single cell descriptions) joined with separating conjunctions, called the symbolic heap fragment. Since negation does not occur within symbolic heaps, one must consider the satisfiability and entailment problems separately. For instance, satisfiability of a symbolic heap is EXPTIME-complete, in general, and NP-complete if the maximum arity of the predicates is a constant, not part of the input [START_REF] Brotherston | A Decision Procedure for Satisfiability in Separation Logic with Inductive Predicates[END_REF]. On the other hand, entailment between symbolic heaps is undecidable in general, and becomes elementary recursive under certain conditions guaranteing that the treewidth of each model is bounded by the size of the inductive definition [START_REF] Iosif | The Tree Width of Separation Logic with Recursive Definitions[END_REF]. In particular, the problem is EXPTIME-hard [START_REF] Antonopoulos | Foundations for Decision Problems in Separation Logic with General Inductive Predicates[END_REF] and the more restricted problem of the validity of entailments of the form P (x 1 , . . . , x n ) |= Q (x 1 , . . . , x n ) has been recently shown to belong to 2EXPTIME [START_REF] Katelaan | Effective Entailment Checking for Separation Logic with Inductive Definitions[END_REF].

In this paper, we consider prenex SL formulae with a quantifier prefix in the language ∃ * ∀ * , possibly containing heap-independent uninterpreted 1 predicate symbols. In analogy with the Bernays-Schönfinkel-Ramsey fragment of first-order logic with ∃ * ∀ * quantifier prefix, equality and uninterpreted predicates and without function symbols of arity greater than 0 [BSR(FO)] [START_REF] Ramsey | On a Problem of Formal Logic[END_REF], we call this fragment Bernays-Schönfinkel-Ramsey SL [BSR(SL k )].

As far as we are aware, all existing work on SL assumes that the universe U is countably infinite. This assumption is not necessarily realistic in practice since the available memory is usually finite, although the bound depends on the hardware and is not known in advance. However, reasoning about pointer-manipulating programs under the finite memory assumption proves to be harder than under the assumption that memory is infinite, when the bound on the memory size is not known à priori. In particular, the frame rule of classical Separation Logic [? ], which is a crucial enabler of local reasoning, breaks, in general, for programs that allocate memory, because, intuitively, adding frames is not possible unless enough free memory is available. Nevertheless, restricted versions of the frame rule still hold, with additional side conditions on the structure of the programs and/or the context to which it is applied. A thorough investigation of the soundness of the frame rule for bounded memory domains is, however, out of the scope of this paper and considered as future work.

In this paper we consider the satisfiability problem for BSR(SL k ), with k ≥ 2, in both cases of finite and infinite universe, referred to as finite and infinite satisfiability, respectively. We show that both problems are undecidable (unlike in the BSR fragment of first-order logic) and that they become PSPACE-complete under some additional restrictions, related to the occurrences of the magic wand and universal variables, namely:

The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates • 3 I. The infinite satisfiability problem is PSPACE-complete if the positive occurrences of -- * (i.e., the occurrences of -- * that are in the scope of an even number of negations) contain no universal variables. II. The finite satisfiability problem is PSPACE-complete if there is no positive occurrence of -- * (i.e., -- * only occurs in the scope of an odd number of negations). This additional restriction stems from the fact that, actually, the finite satisfiability problem becomes undecidable even for only one positive occurrence of a -- * with no variable within its scope. These results establish sharp decidability frontiers within BSR(SL k ). In both cases, we assume that the arity of the uninterpreted predicate symbols is bounded by a constant (the satisfiability problem is already NEXPTIMEcomplete for BSR first-order formulae with unbounded predicate arity [START_REF] Papadimitriou | Computational Complexity[END_REF]). In contrast, the number k of record fields is not bounded and may be part of the input. Reasoning on finite domains is more difficult than on infinite ones, due to the possibility of asserting cardinality constraints on unallocated cells, which explains that the latter condition is more restrictive than the former one. However, the finite universe hypothesis is especially useful when dealing with bounded memory issues, for instance checking that the execution of a program satisfies its postcondition, provided that there are sufficiently many available memory cells.

Theory-parameterized versions of BSR(SL k ) have been shown to be undecidable in [START_REF] Reynolds | Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic[END_REF], e.g. when integer linear arithmetic is used to reason about locations, and claimed to be PSPACE-complete for countably infinite and finite unbounded location sorts, with no relation other than equality. In the present paper, we show that this claim is wrong, and draw a precise chart of decidability for both infinite and finite satisfiability of BSR(SL k ), for k ≥ 2. To complete the picture, the entire prenex fragment of SL 1 has been recently shown decidable but not elementary recursive, whereas the fragment BSR(SL 1 ) is PSPACE-complete [START_REF] Echenim | Prenex Separation Logic with One Selector Field[END_REF].

Undecidability is shown by reduction from BSR first-order formulae with two monadic function symbols, for which satisfiability is known to be undecidable [START_REF] Börger | The Classical Decision Problem[END_REF]. To establish the decidability results, we first show that every quantifier-free SL formula can be transformed into an equivalent boolean combination of formulae of some specific patterns, called test formulae. This result is interesting in itself, since it provides a precise and intuitive characterization of the expressive power of SL: it shows that separating connectives can be confined to a small set of test formulae. Such expressive completeness results were already known for infinite universes (see, e.g., [START_REF] Lozes | Separation Logic preserves the Expressive Power of Classical Logic[END_REF]), but our transformation algorithm also provides insights on the form of the obtained formulae, especially on the polarity of occurrences of some test formulae, which turns out to be useful latter on in the remainder of the paper. Further, we extend the expressive completeness result to finite universes, with additional test formulae asserting cardinality constraints on unallocated cells.

One advantage of the translation to test formulae is that the latter can be straightforwardly translated into firstorder formulae, by encoding the heap as a (k + 1)-ary predicate. Note that another translation of quantifier-free SL k into first-order logic with equality has been described in [START_REF] Calcagno | From Separation Logic to First-Order Logic[END_REF]. There, the small model property of quantifier-free SL k [START_REF] Calcagno | Computability and Complexity Results for a Spatial Assertion Language for Data Structures[END_REF] is used to bound the number of first-order variables to be considered and the separating connectives are interpreted as first-order quantifiers. The result is an equisatisfiable first-order formula. This translation scheme cannot be, however, directly applied to BSR(SL k ), which does not have a small model property, being moreover undecidable.

We focus first on the infinite satisfiability problem and show that, if the above condition (I) is satisfied, then the obtained first-order formulae are in the BSR(FO) class. The infinite satisfiability problem for BSR(SL) is thus reduced to the satisfiability problem for BSR(FO), with some additional constraints on the cardinality of the interpretation: the universe must be infinite, and the heap must be finite. We show that these constraints may be handled by relying on an existing characterization of the models of BSR(FO) formulae with infinitely countable universe [START_REF] Fontaine | Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class[END_REF].

For the finite satisfiability class, the decidability proof is more involved, as the obtained first-order formulae are not in BSR(FO), even if the above condition (II) is satisfied. However, this problem can be overcome by focusing on some class of structures satisfying additional properties ensuring that a reduction to BSR(FO) is feasible. Note that in this case, the cardinality constraints on the universe and heap are straightforward to handle, as the BSR(FO) class is finitely controllable (i.e., every satisfiable BSR(FO) formula has a finite model).

The above transformation algorithm does not by itself provide an efficient decision procedure, as the size of the obtained boolean combination of test formulae is exponential w.r.t. that of the initial (BSR) formula. The PSPACE upper bound thus relies on a careful analysis of the maximal size of the test formulae. The analysis reveals that, although the boolean combination of test formulae is of exponential size, its so-called minterms (i.e., the conjunctions in its disjunctive normal form) are of polynomial size and can be enumerated in polynomial space. The above algorithms can thus be refined to run in polynomial space.

This paper is an extended and thoroughly revised version of the conference paper [START_REF] Echenim | The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains[END_REF]. The latter paper only handles SL formulae with no uninterpreted predicate symbols. The addition of uninterpreted predicate symbols has a limited impact on the transformation of SL formulae into boolean combinations of test formulae. Indeed, since these predicates do not depend on the heap the corresponding atoms can be easily shifted outside of the separated connectives. However, non trivial adaptations are required in the satisfiability tests, since the presence of uninterpreted predicates makes it much more difficult to ensure that the considered formula has a model of the expected cardinality (finite or infinite).

The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates • 5

The bottom inference rule introduces one of the two cases produced by unfolding the inductive definitions on both sides of the sequent2 . Note that the quantifications ∃z, e on the left-hand side have been omitted because they can be eliminated by using the standard ∃-left rule of the sequent calculus (if z and e are fresh variables). The second inference rule is a reduction of the sequent obtained by unfolding, to a sequent matching the initial one (by renaming z to x and e to d), and allows to close this branch of the proof by an inductive argument, based on the principle of infinite descent [START_REF] Brotherston | Automated Cyclic Entailment Proofs in Separation Logic[END_REF]. The simplification applied by the second inference above relies on the validity of the entailment d ≺ e ∧ x → (d, z) |= ∃u∃f . x → ( f , u), which reduces to the (un)satisfiability of the formula d ≺ e ∧ x → (d, z) ∧ ∀u∀f . ¬x → ( f , u). The latter falls into the BSR(SL 2 ) fragment. A consequence of the results in this paper is that, if the inductive rules contain no occurrence of -- * and ∀, then there exist algorithms for solving the above entailment problem in both finite and infinite universes, in the presence of uninterpreted predicates. The only requirement is that the axiomatization of these predicates can be done using BSR(FO), i.e., that the interpretation of these predicates does not depend on the heap. Checking Inductive Invariants with Universal Quantifiers. Purely universal SL formulae are also useful to express pre-or post-conditions asserting "local" constraints on the shape of the data structures manipulated by a program. For instance, the atomic proposition x → (p, n, d ) states that the value of the heap at x is the triple (p, n, d ), where n (resp. p) is the location of the next (resp. previous) cell in the list and d is a data value. Moreover, x → (p, n, d ) holds if and only if there is no location, other than x, in the domain of the heap. With this in mind, the following formula describes a well-formed doubly-linked sorted list:

∀x 1 , x 2 , x 3 , x 4 , x 5 , y 1 , y 2 . x 1 → (x 2 , x 3 , y 1 ) * x 2 → (x 4 , x 5 , y 2 ) * ⊤ → x 5 ≈ x 1 ∧ y 1 ≺ y 2 (1)
Such constraints cannot be expressed by using inductively defined predicates for which the entailment problem is known to be decidable 3 , which shows the practical relevance of the considered fragment. The separating implication (magic wand) seldom occurs in such shape constraints. However, it is useful to describe the dynamic transformations of the data structures, as in the following Hoare-style axiom, giving the weakest precondition of a universal formula ∀u . ψ with respect to redirecting the i-th record field of x to z [START_REF] Samin | BI as an assertion language for mutable data structures[END_REF]:

{x → (y 1 , . . . , y k ) * [x → (y 1 , . . . , y i-1 , z, . . . , y k ) - - * ∀u . ψ ]} x.i := z {∀u . ψ }
For example, the Hoare-style axiom for the weakest precondition of the universal formula ∀u . ψ when redirecting the 'next' field in a doubly-linked list is

{x → (p, n, d ) * [x → (p, z, d ) - - * ∀u . ψ ]} x.next := z {∀u . ψ }.
Intuitively, the formula x → (p, n, d ) * [x → (p, z, d ) -- * ∀u . ψ ] holds when the heap can be separated into disjoint parts, one in which cell x is allocated, and one that, when extended with a heap in which the 'next' field of x is mapped to z, satisfies ∀u . ψ . The universal formula ∀u . ψ could be the doubly-linked list invariant (1) for instance.

In the general case, the precondition for the redirection of the i-th record field of x to z is equivalent to ∀u . x → (y 1 , . . . , y k ) * [x → (y 1 , . . . , y i-1 , z, . . . , y k ) -- * ψ ] because, although hoisting universal quantifiers outside of the separating conjunction is unsound in general, this is possible here due to the special form of the left-hand side x → (y 1 , . . . , y i-1 , z, . . . , y k ) which unambiguously defines a single heap cell.

Checking entailment between two universal formulae boils down to checking the satisfiability of a BSR(SL k ) formula, which can be done thanks to the decidability results in our paper. In particular, checking that ∀u . ψ is an invariant of the program statement x.i := z amounts to checking that the formula ∀u . ψ ∧ ∃u . ¬[x → (y 1 , . . . , y k ) * (x → (y 1 , . . . , y i-1 , z, . . . , y k ) -- * ψ )] is unsatisfiable. Because the magic wand occurs negated, this formula falls into a decidable class defined in the present paper, for both finite and infinite satisfiability.

Roadmap

The remainder of the paper is structured as follows. In Section 2, usual notions and results are briefly reviewed and the definition of the logic SL k is provided. In Section 4 a set of formula patterns, called test formulae, is introduced, and it is shown that these patterns can be expressed in first-order logic. In Section 5, an algorithm is described to transform every SL k formula into an equivalent boolean combination of test formulae. The output formula is of exponential size, however, we show that the conjunctions of literals occurring in its disjunctive normal form are of polynomial size and may be enumerated in polynomial space. In Section 6, the BSR(SL k ) class is investigated and (un)decidability and complexity results are established based on the previous transformation algorithms. Section 7 briefly concludes the paper.

PRELIMINARIES 2.1 First Order Logic

Syntax. We denote by Z and N the sets of integer and natural numbers, respectively. Let Z ∞ = Z ∪ {∞} and N ∞ = N ∪ {∞}, where for each n ∈ Z we have n + ∞ = ∞ and n < ∞. For any countable set S, we denote by ||S || ∈ N ∞ the cardinality of S.

Let U be a sort symbol denoting a universe sort and let B be the usual boolean sort. We consider a countably infinite set Var of variables of sort U, ranged over by x, y, z, and a countably infinite set F of function symbols.

Each function symbol f ∈ F has a sort σ ( f ) ∈ {U, B}. A function symbol f takes #( f ) ≥ 0 arguments of sort U. If #( f ) = 0 we call f a constant and if #( f ) = 1 we say that f is monadic. If σ ( f ) = B, f is called a predicate.
First-order (FO) terms t and formulae φ are defined by the following grammar:

t := x | f (t 1 , . . . , t #(f ) ) φ := ⊥ | ⊤ | t 1 ≈ t 2 | q(t 1 , . . . , t #(q) ) | φ ∧ φ | ¬φ | ∃x . φ
where x ∈ Var, f , q ∈ F , σ ( f ) = U and σ (q) = B. The logical symbols ⊥ and ⊤ denote the boolean constants false and true, respectively. As usual, f (t 1 , . . . , t n ) is simply written f if n = 0. We write φ 1 ∨ φ 2 for ¬(¬φ 1 ∧ ¬φ 2 ), φ 1 → φ 2 for ¬φ 1 ∨ φ 2 , φ 1 ↔ φ 2 for φ 1 → φ 2 ∧ φ 2 → φ 1 and ∀x . φ for ¬∃x . ¬φ. The size of a formula φ, denoted as size(φ), is the number of occurrences of symbols in it. We denote by Var(φ) the set of variables that occur free in φ, i.e. not in the scope of a quantifier, by F (ϕ) the set of function symbols occurring in ϕ, by P (ϕ) the set of predicate symbols in F (ϕ) and by Const(ϕ) the set of constants of sort U in ϕ.

A vector of variables will often be denoted by x, y . . . , and x i will denote the i-th component of x. An equation x ≈ y with x = (x 1 , . . . , x n ) and y = (y 1 , . . . , y n ) denotes the formula n i=1 x i ≈ y i . Semantics. First-order formulae are interpreted over FO-structures4 S = (U, s, I), where U is a nonempty countable set, called a universe, the elements of which are called locations; s : Var ⇀ U is a partial mapping of variables to elements of U, called a store and I interprets each function symbol f by a function

f I : U #(f ) → U if σ ( f ) = U or by a relation f I ⊆ U #(f ) if σ ( f ) = B. A structure (U, s, I) is finite when ||U|| ∈ N and infinite otherwise.
By writing S |= φ, for a structure S = (U, s, I), we mean that Var(φ) ⊆ dom(s) and φ is true when interpreted in S. This relation is defined recursively on the structure of φ, as usual. When S |= φ, we say that S is a model of φ. A formula is [finitely] satisfiable when it has a [finite] model. Given two formulae φ 1 and φ 2 , we say that φ 1 entails φ 2 (written φ 1 |= φ 2 ) when every model of φ 1 is a model of φ 2 , and that φ 1 and φ 2 are equivalent (written φ 1 ≡ φ 2 ) when (U, s, I) |= φ 1 ⇔ (U, s, I) |= φ 2 , for every structure (U, s, I). For any store s on U, variables x 1 , . . . , x n and

The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates • 7 elements ℓ 1 , . . . , ℓ n ∈ U, we denote by s[x 1 ← ℓ 1 , . . . , x n ← ℓ n ] the store that coincides with s on every variable not in {x 1 , . . . , x n } and maps x i to ℓ i , for all i = 1, . . . , n. We also call s[x 1 ← ℓ 1 , . . . , x n ← ℓ n ] an extension of s. If y = (y 1 , . . . , y n ) is a vector of variables, and s is a store, then s(y) denotes the vector (s(y 1 ), . . . , s(y n )). BSR(FO) Formulae. The Bernays-Schönfinkel-Ramsey fragment of FO [BSR(FO)] is the set of formulae of the form ∃x 1 . . . ∃x n ∀y 1 . . . ∀y m . φ, where φ is a quantifier-free formula and all function symbols f ∈ F (φ) of arity #( f ) > 0 have sort σ ( f ) = B. For simplicity we often restrict ourselves to BSR(FO) formulae containing no existential quantification. This is without any loss of generality, since ∃x 1 . . . ∃x n ∀y 1 . . . ∀y m . φ is satisfiable if and only if ∀y 1 . . . ∀y m . φ is satisfiable.

S ′ def = (U ′ , s ′ , I ′ ). The structure S ′ is called a restriction of S to U ′ if U ′ ⊆ U, s ′ (x ) = s(x )
for every x ∈ dom(s), q I ′ = q I ∩ U ′#(q) for every predicate symbol q and f I ′ = f I for every function symbol f .

The following proposition states a well-known property of BSR(FO):

Proposition 2.2. Let φ be a formula in BSR(FO) with no existential quantifier and let S = (U, s, I) be a model of φ.

If U ′ is a nonempty subset of U such that {s(x ) | x ∈ Var(φ)} ∪ {c I | c ∈ Const(φ)} ⊆ U ′ and S ′ def = (U ′ , s ′ , I ′ ) is a restriction of S to U ′ , then S ′ is a model of φ. As a consequence, if φ is satisfiable, then it admits a model (U, s, I) such that ||U|| ≤ max(1, ||Var(φ)|| + ||Const(φ)||).
Proof. See for instance [START_REF] Fontaine | Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class[END_REF]Theorem 3]. □

The decidability of BSR(FO) is a consequence of the above small model property. It is known that the satisfiability problem for this class is NEXPTIME-complete [? ]. The condition requiring the absence of function symbols of sort U in BSR(FO) is justified by the fact that undecidability occurs as soon as two monadic function symbols are allowed. Let BSR 2 (FO) be the extension of BSR(FO) consisting of the formulae ∃x 1 . . . ∃x n ∀y 1 . . . ∀y m . φ, where φ is a quantifier-free formula in which at most two monadic function symbols occur. Proposition 2.3. The satisfiability problem is undecidable for BSR 2 (FO), even if only one universal quantifier and no predicates are allowed.

Proof. See [START_REF] Börger | The Classical Decision Problem[END_REF]Theorem 4.1.8]. □

Separation Logic

Syntax Let k be a strictly positive integer. The logic SL k is the set of formulae generated by the grammar:

φ := ⊥ | ⊤ | emp | x ≈ y | x → (y 1 , . . . , y k ) | q(x 1 , . . . , x #(q) ) | φ ∧ φ | ¬φ | φ * φ | φ - - * φ | ∃x . φ
where x, y, y 1 , . . . , y k , x 1 , . . . , x #(q) ∈ Var, q ∈ F and σ (q) = B. The connectives * and -- * are respectively called the separating conjunction and separating implication (or magic wand). The size size(φ) and set of free variables Var(φ) of an SL k formula φ are defined as for first-order formulae, as well as the formulae φ 1 ∨ φ 2 , φ 1 → φ 2 , φ 1 ↔ φ 2 and ∀x . φ. Moreover, we write φ 1 ⊸ φ 2 for ¬(φ 1 -- * ¬φ 2 ) and call the symbol ⊸ septraction in the following. Throughout the paper, we assume that the arity of the predicate symbols occurring in the SL k formulae is bounded by a constant, whereas k is not necessarily bounded. Definition 2.4. Given a SL k formula ϕ and a subformula ψ of ϕ, we say that ψ occurs at polarity p ∈ {-1, 0, 1} iff one of the following holds:

(1) ϕ = ψ and p = 1, (2) ϕ = ¬ϕ 1 and ψ occurs at polarity -p in ϕ 1 , (3) ϕ = ϕ 1 ∧ ϕ 2 or ϕ = ϕ 1 * ϕ 2 , and ψ occurs at polarity p in ϕ i , for some i = 1, 2, (4) ϕ = ϕ 1 -- * ϕ 2 and either ψ is a subformula of ϕ 1 and p = 0, or ψ occurs at polarity p in ϕ 2 , or

(5) ϕ = ∃x . ϕ 1 and ψ occurs at polarity p in ϕ 1 . A polarity of 1, 0 or -1 is also referred to as positive, neutral or negative, respectively. Note that our notion of polarity is slightly different than the usual one, because the antecedent of a separating implication is of neutral polarity while the antecedent of an implication is usually of negative polarity. This is meant to strengthen upcoming decidability results (see Remark 3.4). Semantics SL k formulae are interpreted over SL-structures S = (U, s, I, h), where U, s and I are defined as for FO and h : U ⇀ fin U k is a finite partial mapping of U to k-tuples of elements of U, called a heap. As for FO, a structure (U, s, I, h) is finite when ||U|| ∈ N and infinite otherwise. We denote by dom(h) the domain of the heap h and by ||h|| ∈ N the cardinality of dom(h). A location ℓ ∈ U (resp. a variable x) is allocated in S if ℓ ∈ dom(h) (resp. if s(x ) ∈ dom(h)). Two heaps h 1 and h 2 are disjoint iff dom(h 1 ) ∩ dom(h 2 ) = ∅, in which case h 1 ⊎ h 2 denotes their union. h ′ is an extension of h iff h ′ = h ⊎ h ′′ , for some heap h ′′ . The relation (U, s, I, h) |= φ is defined recursively on the structure of φ, as follows:

(U, s, I, h) |= ⊤ ⇔ always (U, s, I, h) |= ⊥ ⇔ never (U, s, I, h) |= x ≈ y ⇔ s(x ) = s(y) (U, s, I, h) |= q(x 1 , . . . , x #(q) ) ⇔ (s(x 1 ), . . . , s(x #(q) )) ∈ q I (U, s, I, h) |= emp ⇔ h = ∅ (U, s, I, h) |= x → (y 1 , . . . , y k ) ⇔ h = s(x ), (s(y 1 ), . . . , s(y k )) (U, s, I, h) |= φ 1 ∧ φ 2 ⇔ (U, s, I, h) |= φ i , for all i = 1, 2 (U, s, I, h) |= ¬φ ⇔ (U, s, I, h) ̸ |= φ (U, s, I, h) |= ∃x . φ 1 ⇔ there exists u ∈ U such that(U, s[x ← u], I, h) |= φ 1 (U, s, I, h) |= φ 1 * φ 2 ⇔ there exist disjoint heaps h 1 , h 2 such that h = h 1 ⊎ h 2 and (U, s, I, h i ) |= φ i , for i = 1, 2 (U, s, I, h) |= φ 1 - - * φ 2 ⇔ for all heaps h ′ disjoint from h such that (U, s, I, h ′ ) |= φ 1 , we have (U, s, I, h ⊎ h ′ ) |= φ 2
Satisfiability, entailment and equivalence are defined for SL k as for FO formulae. We write ϕ ≡ fin ψ (resp. ϕ ≡ inf ψ ) if ϕ has the same truth value as ψ in all finite (resp. infinite) structures.

Remark 2.5. The cardinality of the universe has a deep impact on the semantics of SL formulae. For instance, the formula ϕ = ¬emp -- * ⊥ states that no nonempty heap disjoint from the current heap exists, which is always false in an infinite universe (since every heap is finite) but is true in a finite universe where all elements are allocated. ■

THE BSR(SL k ) CLASS

In this section, we give the definition of the Bernays-Schönfinkel-Ramsey fragment of SL k and provide a brief summary of the results proved in this paper. Definition 3.1. The Bernays-Schönfinkel-Ramsey fragment of SL k , denoted by BSR(SL k ), is the set of formulae of the form ∃x 1 . . . ∃x n ∀y 1 . . . ∀y m . ϕ, where ϕ is a quantifier-free SL k formula. Note that, since there is no function symbol of sort U in SL k , there is no restriction, other than the form of the quantifier prefix, defining BSR(SL k ). As for FO, we will often restrict ourselves to BSR(SL k ) formulae containing no existential quantifier. As satisfiability is not decidable for BSR(SL k ) (see Theorem 3.3 below), we define two fragments of BSR(SL k ) for which finite and infinite satisfiability are respectively decidable. The definition is based on the polarity (see Definition 2.4) of the occurrences of the symbol -- * and on the universal variables occurring within their scope.

The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates • 9 Definition 3.2. Given an integer k ≥ 1, we define: (1) BSR inf (SL k ) as the set of formulae ∀y 1 . . . ∀y m . ϕ such that for all i ∈ [1, m] and all formulae ψ 1 -- * ψ 2 occurring at polarity 1 in ϕ, we have y i Var(ψ 1 ) ∪ Var(ψ 2 ), (2) BSR fin (SL k ) as the set of formulae ∀y 1 . . . ∀y m . ϕ such that no formula ψ 1 -- * ψ 2 occurs at polarity 1 in ϕ.

Note that BSR fin (SL k ) ⊊ BSR inf (SL k ) ⊊ BSR(SL k ), for any k ≥ 1. We know state the main results of the paper.

Theorem 3.3. The satisfiability problem is undecidable for BSR(SL k ). The infinite satisfiability problem for BSR inf (SL k ) and the finite satisfiability problem for BSR fin (SL k ) are both PSPACE-complete.

The remainder of the paper is devoted the proof of Theorem 3.

x → y def = x → (y 1 , . . . , y k ) * ⊤ |U | ≥ n def = ⊤ ⊸ |h| ≥ n alloc(x ) def = x → (x, . . . , x ) k times - - * ⊥ |h| ≥ |U | -n def = |h| ≥ n + 1 - - * ⊥ x ≈ y q(x 1 , . . . , x #(q) ) |h| ≥ m def =        |h| ≥ m -1 * ¬emp, if 0 < m < ∞ ⊤, if m = 0 ⊥, if m = ∞
where x, y ∈ Var, q ∈ F , σ (q) = B, x 1 , . . . , x #(q) , y 1 , . . . ,

y k ∈ Var, n ∈ N and m ∈ N ∞ .
If ϕ is a test formula of the form t ≥ s then the formula ¬ϕ will often be denoted by t < s. For a set of variables X ⊆ Var, let alloc(X ) def = x ∈X alloc(x ) and nalloc(X ) def = x ∈X ¬alloc(x ). The trivial test formulae |h| ≥ 0 and |h| ≥ ∞ are introduced for reasons that will become clear in Section 5. The semantics of test formulae is very natural: x → y means that x points to vector y, alloc(x ) means that x is allocated, and the arithmetic expressions are interpreted as usual, where |h| and |U | respectively denote the number of allocated cells and the number of locations (possibly ∞). Formally: Proposition 4.2. Given an SL-structure (U, s, I, h), the following equivalences hold, for all variables x, y 1 , . . . , y k ∈ Var and integers n ∈ N:

(U, s, I, h) |= x → y ⇔ h(s(x )) = s(y) (U, s, I, h) |= |h| ≥ |U | -n ⇔ ||h|| ≥ ||U|| -n (U, s, I, h) |= |U | ≥ n ⇔ ||U|| ≥ n (U, s, I, h) |= |h| ≥ n ⇔ ||h|| ≥ n (U, s, I, h) |= alloc(x ) ⇔ s(x ) ∈ dom(h)
Proof. Let S = (U, s, I, h) be an SL-structure. We establish each statement separately.

• S |= x → y ⇔ h(s(x )) = (s(y 1 ), . . . , s(y k )). Assume that S |= x → y. Then by definition, there exist disjoint heaps h 1 , h 2 such that (U, s, I, h 1 ) |= x → y, (U, s, I, h 2 ) |= ⊤ and h = h 1 ⊎h 2 . Thus s(x ) ∈ dom(h 1 ) ⊆ dom(h) and h(s(x

)) = h 1 (s(x )) = (s(y 1 ), . . . , s(y k )). Conversely, assume h(s(x )) = (s(y 1 ), . . . , s(y k )). Then h is of the form h 1 ⊎ h 2 , where h 1 is the restriction of h to {s(x )} and h 2 is the restriction of h to U \ {s(x )}. By definition, h 1 = s(x ), (s(y 1 ), . . . , s(y k )) , hence h 1 |= x → y. Furthermore, h 2 |= ⊤. Thus S |= x → y.
• S |= alloc(x ) ⇔ s(x ) ∈ dom(h). Assume that S |= alloc(x ). This means that there is no heap h ′ disjoint from h such that (U, s, I, h ′ ) |= x → (x, . . . , x ). If s(x ) dom(h), then the heap h ′ defined as h ′ = ⟨s(x ), (s(x ), . . . , s(x ))⟩ is disjoint from h and we have (U, s, I, h ′ ) |= x → (x, . . . , x ). Thus s(x ) ∈ dom(h). Conversely, assume s(x ) ∈ dom(h). By definition, for any heap h ′ such that (U, s,

I, h ′ ) |= x → (x, . . . , x ) we have s(x ) ∈ dom(h ′ ), hence h ′ ∩ h ∅. Thus S |= alloc(x ). • S |= |h| ≥ n ⇔ ||h|| ≥ n. Assume that S |= |h| ≥ n.
I, h ⊎ h ′ ) |= |h| ≥ n, which proves that S |= |U | ≥ n. • S |= |h| ≥ |U | -n ⇔ ||h|| ≥ ||U|| -n.. Assume that S |= |h| ≥ |U | -n.
By definition, this entails that there is no heap disjoint from h with a domain of cardinality at least n + 1. In particular, if

L = U \ dom(h), and h ′ is any heap of domain L, then dom(h) ∩ dom(h ′ ) = ∅, hence ||h ′ || ≤ n. Since ||U|| = ||h|| + ||h ′ ||, we deduce that ||h|| ≥ ||U|| -n. Conversely, if ||h|| ≥ ||U|| -n then ||U \ dom(h)|| ≤ n,

A Generalization of Test Formulae

For technical convenience, we extend the previous patterns to express more general cardinality constraints. For every n ∈ N, we denote by

|U | ≃ n (resp., |h| ≃ n) the formula |U | ≥ n ∧ |U | < n + 1 (resp., |h| ≥ n ∧ |h| < n + 1). Similarly, |h| ≃ |U | -n denotes either |h| ≥ |U | -n ∧ |h| < |U | -(n -1) (if n > 0) or |h| ≥ |U | -0 (if n = 0).
We then extend the notation |h| ≥ t to the case where t is a linear function of |U |, with coefficients in Z.

Definition 4.3. Given integers α, β ∈ Z, where α {0, 1}, let

|h| ≥ α • |U | + β def =                ⊥ if α > 1, β > 0 ⊤ if α, β < 0 |U | < 1-β α -1 ∧ 1≤n≤ -β α -1 (|U | ≃ n → |h| ≥ α • n + β ) if α > 1, β ≤ 0 1≤n < -β α (|U | ≃ n → |h| ≥ α • n + β ) if α < 0, β ≥ 0 If α = 0 and β < 0 then |h| ≥ α .|U | + β def = ⊤. If α = 1 and β > 0 then |h| ≥ α .|U | + β def = ⊥.
Note that the cases α = 0, β ≥ 0 and α = 1, β ≤ 0 are already covered by Definition 4.1. The following proposition states that the semantics of these formulae is as expected.

The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates • 11 Proposition 4.4. Given an SL-structure (U, s, I, h), we have (U, s,

I, h) |= |h| ≥ α • |U | + β iff ||h|| ≥ α • ||U|| + β, for all α, β ∈ Z, α {0, 1}.
Proof. We distinguish the four cases below:

• If α > 1 and β > 0 then ||U|| ≥ ||h|| ≥ α • ||U|| + β never holds. • If α < 0 and β < 0 then ||h|| ≥ 0 ≥ α • ||U|| + β, always holds. • If α > 1 and β ≤ 0, assume first that (U, s, I, h) |= |h| ≥ α • |U | + β. Then (U, s, I, h) |= |U | < 1-β α -1 , thus 1 ≤ ||U|| < 1-β α -1 by Proposition 4.2. If ||U|| > -β α -1 then ||U|| ≥ -β α -1 + 1 = 1-β α -1 , which contradicts (U, s, I, h) |= |U | < 1-β α -1 , by Proposition 4.2. Otherwise, we have ||U|| = n, with 1 ≤ n ≤ -β α -1 . In this case (U, s, I, h) |= |h| ≥ α • n + β, which implies ||h|| ≥ α • ||U|| + β, by Proposition 4.2. Conversely, assume that ||h|| ≥ α • ||U|| + β. Since necessarily ||U|| ≥ ||h||, we obtain ||U|| ≥ α • ||U|| + β, i.e., ||U|| > α • ||U|| + β -1 and thus ||U|| < 1-β α -1 , so that (U, s, I, h) |= |U | < 1-β α -1 . Moreover, if n = ||U || then (U, s, I, h) |= |h| ≥ α • n + β by Proposition 4.2. • If α < 0 and β ≥ 0, assume first that (U, s, I, h) |= |h| ≥ α • |U | + β. If, moreover, ||U|| ≥ -β α , then α • ||U|| + β ≤ 0, thus ||h|| ≥ 0 ≥ α • ||U|| + β holds. Otherwise, 1 ≤ ||U|| < -β α and if (U, s, I, h) |= |U | ≃ n, for some 1 ≤ n < -β α , then we have (U, s, I, h) |= |h| ≥ α • n + β, thus ||h|| ≥ α • ||U|| + β, by Proposition 4.2. Conversely, assume that ||h|| ≥ α • ||U|| + β and (U, s, I, h) |= |U | ≃ n, for some integer 1 ≤ n < -β α . By Proposition 4.2, we have ||U|| = n and ||h|| ≥ α • n + β, thus (U, s, I, h) |= |h| ≥ α • |U | + β. □

From Test formulae to FO

The introduction of test formulae (Definition 4.1) is motivated by the reduction of the (in)finite satisfiability problem for quantified boolean combinations thereof to the same problem for FO. The reduction is based on a straightforward encoding of the heap as a (k + 1)-ary predicate symbol, however it is devised below in such a way that the obtained formula is in the BSR class, if possible. To this purpose, we also use a monadic predicate symbol encoding the domain of the heap and boolean constants encoding cardinality constraints. We thus introduce several special (pairwise distinct) function symbols: a (k + 1)-ary predicate p, a monadic predicate d, boolean constants a n , b n and c n , and the following constants of sort U: u n , u i n , v n , w n and ξ i x , for n ≥ 0, i ∈ [1, k] and x ∈ Var. The symbol p will encode the heap, d will encode the domain of the heap, the constants a n , b n and c n encode the constraints over the number of (allocated or unallocated) locations, and u n , u i n , v n , w n and ξ i x are interpreted as pairwise distinct elements of the universe, used to express such constraints in FO.

Given a quantified boolean combination of test formulae ϕ not containing the above symbols, the FO formula τ (ϕ) is defined by induction on the structure of ϕ:

τ (|h| ≥ n) def = a n τ (|U | ≥ n) def = b n τ (|h| ≥ |U | -n) def = ¬c n+1 τ (¬ϕ 1 ) def = ¬τ (ϕ 1 ) τ (x → y) def = p(x, y 1 , . . . , y k ) τ (alloc(x )) def = d(x ) τ (ϕ 1 ∧ ϕ 2 ) def = τ (ϕ 1 ) ∧ τ (ϕ 2 ) τ (∃x . ϕ 1 ) def = ∃x . τ (ϕ 1 ) τ (q(x 1 , . . . , x #(q) )) def = q(x 1 , . . . , x #(q) ) τ (x ≈ y) def = x ≈ y
The special symbols are related by the following axioms:

(Heap) ∀x∀y∀y ′ . p(x, y) ∧ p(x, y ′ ) → y ≈ y ′ (Dom x ) d(x ) → p(x, ξ 1 x , . . . , ξ k x ) for each x ∈ Var(ϕ) (A 0 ) a 0 (A n ) a n → (a n-1 ∧ p(u n , u 1 n , . . . , u k n ) ∧ n-1 i=1 ¬u i ≈ u n ) ∧ ∀x∀y . ¬a n ∧ p(x, y) → n-1 i=1 x ≈ u i (B 0 ) b 0 (B n ) b n → (b n-1 ∧ n-1 i=1 ¬v i ≈ v n ) ∧ ∀x . ¬b n → n-1 i=1 x ≈ v i (C 0 ) c 0 (C n ) ∀y . c n → (c n-1 ∧ ¬p(w n , y) ∧ n-1 i=1 ¬w n ≈ w i )
Intuitively, p encodes the heap in the following sense. If (U, s, I) |= Heap then there exists a heap h on U such that y = h(x ) ⇔ (x, y) ∈ p I . The constant a n (resp. b n ) is true if there are at least n cells in the domain of the heap (resp. in the universe), namely u 1 , . . . , u n (resp. v 1 , . . . , v n ). If c n is true, then there are at least n locations w 1 , . . . , w n outside of the domain of the heap (i.e., n unallocated locations), but the converse does not hold. Indeed, the axioms C n do not state the equivalence of c n with the existence of at least n free locations, because such an equivalence cannot be expressed in BSR(FO) 5 . Similarly, the axiom Dom states that if x is allocated then d(x ) holds, but the converse is true only for x ∈ Var(ϕ) (as stated by the axiom Dom x ). Again, adding the implication ∀x . d(x ) → ∃y 1 , . . . , y k . p(x, y 1 , . . . , y k ) would result in a formula that is not in BSR(FO). Instead, we only assert finitely many (skolemized) instances of the latter formula, for every free variable x, which is sufficient for our purpose. As a consequence, the transformation preserves sat-equivalence only if the formulae |h| ≥ |U | -n or alloc(x ) with x Var(ϕ) occur only at negative polarity (see Lemma 4.9, Point 2). ∀x, y, z . p(x, y)

, if x = h(y) ⇔ (x, y) ∈ p I , then we say that h is associated with (U, s, I). An element x ∈ U is allocated in (U, s, I) (resp. points to y in (U, s, I)) if there exists y ∈ U k such that (x, y) ∈ p I (resp. if (x, y) ∈ p I ).
def = Heap ∧ N (ϕ ) i=0 A i ∧ N (ϕ ) i=0 B i ∧ N (ϕ )+1 i=0 C i ∧ Dom ∧ x
∧ p(x, z) → y ≈ z a 0 ∧ (a 1 → a 0 ∧ p(u 1 , u 1 1 )) ∧ (a 2 → a 1 ∧ p(u 2 , u 1 2 ) ∧ ¬u 1 ≈ u 2 ) c 0 ∧ (∀y . c 1 → c 0 ∧ ¬p(w 1 , y))
The formula τ (ϕ) ∧ A(ϕ) states that p(x, y) holds, that p is a partial function and that there exist at least two distinct allocated elements (namely u 1 and u 2 ) and one unallocated element (w 1 ).

Let ϕ ′ be the SL 2 formula alloc(u) ∧ ∀y . ¬u ≈ y → ¬alloc(y). Then τ (ϕ ′ ) = d(u) ∧ (∀y . ¬u ≈ y → ¬d(y)), where the relevant axioms in A(ϕ ′ ) are:

∀x, y 1 , y 2 , z 1 , z 2 . p(x, y 1 , y 2 ) ∧ p(x, z 1 , z 2 ) → y 1 ≈ z 1 ∧ y 2 ≈ z 2 ∀x, y 1 , y 2 . p(x, y 1 , y 2 ) → d(x ) d(u) → p(u, ξ 1 u , ξ 2 u ) ■
The relationship between ϕ and τ (ϕ) is stated below.

The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates • 13 Definition 4.8. A formula ϕ is BSR-compatible if: (i) each test formula |h| ≥ |U | -n in ϕ occurs at a negative polarity (ii) if a formula alloc(x ) occurs at positive polarity in ϕ, then x ∈ Var(ϕ). Lemma 4.9. Let ϕ be a quantified boolean combination of test formulae. The following hold, for any universe U and any store s:

(1) if (U, s, I, h) |= ϕ, for a heap h, then (U, s, J ) |= τ (ϕ) ∧ A (ϕ) for an interpretation J coinciding with I on every symbol not occurring in A(ϕ) and such that h is associated with (U, s, J ); (2) if ϕ is BSR-compatible and (U, s, I) |= τ (ϕ) ∧ A(ϕ) for an interpretation I such that ||p I || ∈ N, then (U, s, I, h) |= ϕ, where h denotes the heap associated with (U, s, I).

Proof. ( 1) Let (U, s, I, h) be a model of ϕ. Let J be an interpretation coinciding with I on every symbol occurring in ϕ, and extended to the symbols p, a i , b i , c j , u i , v i , w i , for i ∈ [0, N (ϕ)] and j ∈ [0, N (ϕ) +1], as follows: for all ℓ 0 , . . . , ℓ k ∈ U we set (ℓ 0 , . . . , ℓ k ) ∈ p J iff h(ℓ 0 ) = (ℓ 1 , . . . , ℓ k ) and d I = dom(h). The interpretation of the boolean constants is defined below:

a J i def = ⊤ if 0 ≤ i ≤ min(||h||, N (ϕ)) ⊥ if i > min(||h||, N (ϕ)) b J i def = ⊤ if 0 ≤ i ≤ min(||U||, N (ϕ)) ⊥ if i > min(||U||, N (ϕ)) c J i def = ⊤ if 0 ≤ i ≤ min(||U|| -||h||, N (ϕ) + 1) ⊥ if i > min(||U|| -||h||, N (ϕ) + 1)
The constants of sort U are interpreted as locations, as follows:

• u J 1 , . . . , u J min( | |h | |, N (ϕ ))
are pairwise distinct locations in dom(h) and u i n is the i-th component of the vector referred to by u n .

• v J 1 , . . . , v J min( | |U | |, N (ϕ )) are pairwise distinct locations in U. • w J 1 , . . . , w J min( | |U | |-| |h | |, N (ϕ )+1
) are pairwise distinct locations in U \ dom(h). The other symbols are interpreted arbitrarily. It is straightforward to check that (U, s, J ) |= A (ϕ). We prove that (U, s, I, h) |= ψ iff (U, s, J ) |= τ (ψ ) for every subformula ψ of ϕ by induction on the structure of ϕ:

• ψ = x ≈ y: We have τ (ψ ) = ψ . Further, (U, s, I, h) |= ψ ⇔ s(x ) = s(y) ⇔ (U, s, J ) |= ψ .

• ψ = q(x 1 , . . . , x #(q) ): We have τ (ψ ) = ψ . Moreover, (U, s, I, h) |= ψ ⇔ (s(x 1 ), . . . , s(x #(q) )) ∈ q I and (U, s, J ) |= ψ ⇔ (s(x 1 ), . . . , s(x #(q) )) ∈ q J . Because I and J coincide on every symbol occurring in ψ , q I = q J . Thus (U, s,

I, h) |= ψ ⇔ (U, s, J ) |= ψ . • ψ = |h| ≥ n: (U, s, I, h) |= ψ iff ||h|| ≥ n by Proposition 4.2. Since n ≤ N (ψ ), we have ||h|| ≥ n ⇔ n ≤ min(||h||, N (ψ )) ⇔ a J n = ⊤ ⇔ (U, s, J ) |= τ (ψ ). • ψ = |U | ≥ n: (U, s, I, h) |= ψ iff ||U|| ≥ n, by Proposition 4.2. Since n ≤ N (ψ ), we have ||U|| ≥ n ⇔ n ≤ min(||U||, N (ψ )) ⇔ b I n = ⊤ ⇔ (U, s, J ) |= τ (ψ ). • ψ = |h| ≥ |U | -n: (U, s, I, h) |= ψ iff ||h|| ≥ ||U|| -n, by Proposition 4.2, i.e., iff n + 1 > ||U|| -||h||. Since n ≤ N (ψ ), we have (U, s, I, h) |= ψ ⇔ n + 1 > min(||U|| -||h||, N (ψ ) + 1) ⇔ c I n+1 = ⊥ ⇔ (U, s, J ) |= ¬c n+1 ⇔ (U, s, J ) |= τ (ψ ). • ψ = x → (y 1 , . . . , y k ): (U, s, I, h) |= ψ iff h(s(x )) = (s(y 1 ), . . . , s(y k )) iff (s(x ), s(y 1 ), . . . , s(y k )) ∈ p J iff (U, s, J ) |= p(x, y 1 , . . . , y k ). • ψ = alloc(x ): (U, s, I, h) |= ψ iff s(x ) ∈ dom(h) iff s(x ) ∈ d I iff (U, s, J ) |= d(x ). • The cases ψ = ψ 1 ∧ ψ 2 , ψ = ¬ψ 1 and ψ = ∃x . ψ 1 are by the inductive hypothesis, since (U, s, I, h) |= ψ i ⇔ (U, s, J ) |= τ (ψ i ), for all i = 1, 2. (2) Let (U, s, I) be a model of τ (ϕ) ∧ A(ϕ), such that ||p I || ∈ N.
We define a heap h as follows: for each (k + 1)tuple of locations ℓ 0 , . . . , ℓ k ∈ U such that (ℓ 0 , . . . , ℓ k ) ∈ p I , we set h(ℓ 0 ) def = (ℓ 1 , . . . , ℓ k ). Since (U, s, I) |= Heap and ||p I || ∈ N, h is a finite partial function. Let ϕ nnf be the negation normal form of ϕ. It is easy to check that τ (ϕ nnf ) ≡ τ (ϕ). We prove that (U, s, I) |= τ (ψ ) ⇒ (U, s, I, h) |= ψ for every subformula ψ in ϕ nnf : Proof. The proof is by a straightforward inspection of τ (φ) and of the axioms in A (φ). There are k

• ψ = |h| ≥ n: τ (ψ ) = a
•n constants ξ j x i , N (φ) + 1 constants a i , b i and w i , N (φ) constants u i , v i , N (φ) + 2 constants c i , and k • N (φ) constants u j i . □ 5 FROM QUANTIFIER-FREE SL k TO TEST FORMULAE
This section establishes the expressive completeness result of the paper, namely that any quantifier-free SL k formula is equivalent, on both finite and infinite models, to a boolean combination of test formulae. Starting from a quantifier-free SL k formula φ, we define a set µ (φ) of conjunctions of test formulae and their negations, called minterms, such that φ ≡ M ∈µ (φ ) M. The definition of µ (φ) depends on the cardinality of the universe (finite or infinite). The number of minterms in µ (φ) is exponential in the size of φ, however, the size of every M ∈ µ (φ) is bounded by a polynomial in the size of φ and, as we show, checking the membership of a given minterm M in µ (φ) can be done in PSPACE.

The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates • 15

Minterms

We introduce some definitions and notations, and establish basic properties.

Definition 5.1. A literal is a test formula or its negation. A minterm M is a set of literals, interpreted as the conjunction of its elements, that contains:

• at most one literal of the form |U | ≥ n;

• at most one literal of the form |U | < n;

• exactly one literal |h| ≥ min M , where min

M ∈ N ∪ {|U | -n | n ∈ N}; • exactly one literal |h| < max M , where max M ∈ N ∞ ∪ {|U | -n | n ∈ N}.
Definition 5.2. Given a minterm M, we define the sets:

M e def = M ∩ x ≈ y, ¬x ≈ y | x, y ∈ Var M a def = M ∩ {alloc(x ), ¬alloc(x ) | x ∈ Var} M u def = M ∩ {|U | ≥ n, |U | < n | n ∈ N} M p def = M ∩ {x → y, ¬x → y | x, y ∈ Var k +1 } M f def = M ∩ {q(x), ¬q(x) | q ∈ F , σ (q) = B, x ∈ Var #(q) } Thus, M = M e ∪ M u ∪ M a ∪ M p ∪ M f ∪ {|h| ≥ min M , |h| < max M }, for each minterm M.
Proposition 5.3. Given a minterm M, for all structures S = (U, s, I, h) and

S ′ = (U, s, I, h ′ ) we have S |= M e ∧ M u ∧ M f ⇔ S ′ |= M e ∧ M u ∧ M f .
Proof. This is immediate, since the semantics of the test formulae in M e ∪ M u ∪ M f does not depend on the heap. □ Definition 5.4. Given a set of variables X ⊆ Var, a minterm M is (1) E-complete for X iff for all x, y ∈ X , exactly one of x ≈ y ∈ M, ¬x ≈ y ∈ M holds, and (2) A-complete for X iff for each x ∈ X exactly one of alloc(x ) ∈ M, ¬alloc(x ) ∈ M holds. Proof. This is an immediate consequence of the fact that if x, x ′ ∈ X , then s(x ) = s(x ′ ) if and only if M |= x ≈ x ′ . □ Definition 5.6. For a set T of literals, let:

av(T ) def = x ∈ Var | ∃x ′ ∈ Var . x ≈ T x ′ , T ∩ {alloc(x ′ ), x ′ → y | y ∈ Var k } ∅ nv(T ) def = {x ∈ Var | ∃x ′ ∈ Var . x ≈ T x ′ , ¬alloc(x ′ ) ∈ T } fp X (T ) def = T ∩ {alloc(x ), ¬alloc(x ), x → y, ¬x → y | x ∈ X , y ∈ Var k } # a (T ) def = |av(T )| T # n (X ,T ) def = |X ∩ nv(T )| T
For notational convenience, we also let fp a (T ) def = fp av(T ) (T ).

Intuitively, av(T ) (resp. nv(T )) is the set of variables that must be (resp. are never) allocated in every (resp. any) model of T . The symbol # a (T ) represents the number of equivalence classes of ≈ T containing variables allocated in every model of T ; # n (X ,T ) represents the number of equivalence classes of ≈ T containing variables from X that are not allocated in any model of T and fp X (T ) is the footprint of T relative to the set X ⊆ Var, i.e. the set of formulae describing allocation and points-to relations over variables from X . For example, if T = {x ≈ z, alloc(x ), ¬alloc(y), ¬z → y}, then av(T ) = {x, z}; nv(T ) = y ; # a (T ) = 1; # n ( y ,T ) = 1; fp a (T ) = alloc(x ), ¬z → y and fp nv(T ) (T ) = ¬alloc(y) .

Proposition 5.7. Given a set T of test formulae and a structure (U, s, I, h), if (U, s, I, h) |= fp a (T ), then (U, s, I, h ′ ) |= fp a (T ) for every extension h ′ of h.

Proof. Assume that (U, s, I, h) |= fp a (T ) and let ϕ ∈ fp a (T ). If ϕ is of the form ¬alloc(x ), then since x ∈ av(T ), necessarily, T contains an atom of the form alloc(x ′ ) or x ′ → y, where x ′ is a variable such that x ′ ≈ T x. In both cases, fp a (T ) must be unsatisfiable, contradicting the assumption that (U, s, I, h) |= fp a (T ). If ϕ is of the form x → y, then, since (U, s, I, h) |= ϕ, we have h(s(x )) = s(y), thus h ′ (s(x )) = s(y) (since h ′ is an extension of h) so that (U, s, I, h ′ ) |= ϕ. The proof is similar if ϕ = alloc(x ). If ϕ = ¬x → y and T contains an atom of the form alloc(x ′ ) for some variable x ′ such that x ≈ T x ′ , then s(x ) ∈ dom(h) and h(s(x )) s(y). This entails that h ′ (s(x )) s(y) (since h ′ is an extension of h) and (U, s, I, h ′ ) |= ϕ. Otherwise, because x ∈ av(T ), T must contain an atom of the form x ′ → y ′ for some variable x ′ such that x ≈ T x ′ . Thus, h(s(x )) = s(y ′ ) s(y), and we deduce that h ′ (s(x )) s(y).

□ Definition 5.8. Given the minterms M 1 , M 2 , let npto(M 1 , M 2 ) def = (M 1 ∩ M 2 ) ∩ {¬x → y | x av(M 1 ∪ M 2 )
, y ∈ Var k } be the set of negative points-to literals common to M 1 and M 2 , involving left-hand side variables not allocated in either M 1 or M 2 .

For example, if

M 1 = {x → y, ¬y → z, ¬y → u, ¬z → u, |h| ≥ 1, |h| < ∞} and M 2 = {x → y, ¬y → z, ¬z → u, alloc(z), |h| ≥ 1, |h| < ∞}. Then npto(M 1 , M 2 ) = {¬y → z}. Observe that M 1 * M 2 necessarily entails npto(M 1 , M 2 )
, since the assertion y → z cannot hold in any part of the heap.

We now introduce some conditions that are necessary for a minterm to be satisfiable. The first condition is that the same element cannot point to distinct vectors. Definition 5.9. Given a minterm M, its points-to closure is pc(M ) def = ⊥ if there exist literals x → y, x ′ → y ′ ∈ M such that x ≈ M x ′ and y, y ′ are M-distinct; and pc(M

) def = M, otherwise. Intuitively, pc(M ) is ⊥ iff M contradicts the fact that the heap is a partial function. For instance, let M = {x → (y 1 , y 2 ), x ′ → (y ′ 1 , y ′ 2 ), x ≈ x ′ , ¬y 1 ≈ y ′ 1 , |h| ≥ 1, |h| < ∞}.
We have pc(M ) = ⊥, and it is clear that M is unsatisfiable as the same location cannot point to both (y 1 , y 2 ) and (y ′ 1 , y ′ 2 ). Note that we do not assert the equality y ≈ y ′ , instead we only check that it is not falsified. This is sufficient for our purpose because in the following we always assume that the considered minterms are E-complete.

The second condition is that the alloc and point-to literals should be consistent:

Definition 5.10. A minterm M is footprint-consistent if for all x, x ′ ∈ Var and y, y ′ ∈ Var k , such that x ≈ M x ′ and y i ≈ M y ′ i for all i ∈ [1, k], we have (1) if alloc(x ) ∈ M then ¬alloc(x ′ ) M, and (2) if x → y ∈ M then ¬alloc(x ′ ), ¬x ′ → y ′ ∩ M = ∅. Proposition 5.11. If M is a footprint-consistent minterm, then nv(M ) ∩ av(M ) = ∅. If, moreover, M is E-complete for Var(M ), then s(X ) ∩ s(av(M )) = ∅ for each set X disjoint from av(M ) and each model (U, s, I, h) of M.
Proof. Suppose first that x ∈ nv(M ) ∩ av(M ). Then there exist literals ¬alloc(x ′ ) and alloc(x ′′ ) in M such that x ≈ M x ′ and x ≈ M x ′′ , which contradicts the footprint consistency of M. For the second point, suppose

The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates • 17 that ℓ ∈ s(X ) ∩ s(av(M )). Then there exist variables x ∈ X and x ′ ∈ av(M ) such that s(x

) = s(x ′ ) = ℓ. If M is E-complete, either x ≈ x ′ ∈ M or ¬x ≈ x ′ ∈ M.
The first case contradicts x av(M ) and the second case contradicts (U, s, I, h) |= M. □ Footprint-consistency is not sufficient for satisfiability. For example, x → y, x ′ → y ′ , ¬y ≈ y ′ , |h| < 2 is at the same time footprint-consistent and unsatisfiable, because x and x ′ point to distinct elements but there is at most one allocated location. We thus introduce additional conditions related to the cardinality of the heap or of the universe. Intuitively, for any minterm M, we define a formula dc(M ) that asserts that min M < max M and that the domain contains enough elements to allocate all cells. Essentially, given a structure (U, s, I, h), if h(x ) is known to be defined and distinct from n pairwise distinct vectors of locations v 1 , . . . , v n , then necessarily at least n + 1 vectors must exist. Since there are ||U|| k vectors of length k, we must have

||U|| k ≥ n + 1, hence ||U|| ≥ k √ n + 1. For instance, if M = {¬x → y i | i ∈ [1, n]} ∪ {alloc(x )} ∪ {y i ̸ ≈ y j | i, j ∈ [1, n], i j}
then it is clear that M is unsatisfiable if there are less than n locations, since x cannot be allocated in this case.

Definition 5.12. Given a minterm M, the domain closure of M is dc(M

) def = ⊥ if either min M = n 1 and max M = n 2 for some n 1 , n 2 ∈ Z such that n 1 ≥ n 2 , or min M = |U | -n 1 and max M = |U | -n 2 ,
where n 2 ≥ n 1 ; and otherwise: Proof. Let S = (U, s, I, h) and n 1 , n 2 ∈ N ∞ . We distinguish the following cases:

dc(M ) def = M ∪ |U | ≥ k max x ∈av(M ) (δ x (M ) + 1) ∪ {|U | ≥ n 1 + n 2 + 1 | min M = n 1 , max M = |U | -n 2 , n 1 , n 2 ∈ N} ∪ {|U | < n 1 + n 2 | min M = |U | -n 1 , max M = n 2 , n 1 , n 2 ∈
• If min M = n 1 and max M = n 2 then n 1 < n 2 must be the case, or else dc(M ) ≡ ⊥, in contradiction with We have h(s(x )) = (s(y 1 ), . . . , s(y k )), h(s(x ′ )) = (s(y 1 ), . . . , s(y k )) and h(s(x )) = h(s(x ′ )), thus s(y i ) = s(z i ), for all i ∈ [1, k], a contradiction. Thus S |= pc(M ). For a variable x ∈ av(M ), let ¬x 1 → y 1 , . . . , ¬x n → y n ∈ M be all literals such that x 1 ≈ M . . . ≈ M x n ≈ M x and y i ̸ ≈ M y j for all i j. Then h(s(x )) ∈ U k \ s(y 1 ), . . . , s(y n ) , thus

S |= dc(M ) u . • If min M = n 1 and max M = |U | -n 2 then |U | ≥ n 1 + n 2 + 1 ∈ dc(M ) and since S |= dc(M ) u , we obtain n 1 < ||U|| -n 2 . • If min M = |U | -n 1 and max M = n 2 then |U | < n 1 + n 2 ∈ dc(M ) and since S |= dc(M u ), we obtain ||U|| -n 1 < n 2 . • If min M = |U | -n 1 and max M = |U | -n 2 then n 2 < n 1 must
||U|| k ≥ n + 1 = δ x (M ) + 1. Since this holds for each x ∈ av(M ), we have S |= |U | ≥ k max x ∈av(M ) (δ x (M ) + 1) . Furthermore, if |h| ≥ n 1 , |h| < |U | -n 2 ∈ M then, since S |= M, ||U|| -n 2 > ||h|| ≥ n 1 , thus ||U || ≥ n 1 + n 2 + 1 and S |= |U | ≥ n 1 +n 2 + 1. Analogously, we obtain S |= |U | < n 1 +n 2 in the case |h| < n 1 , |h| ≥ |U | -n 2 ∈ M. □

Eliminating Spatial Connectives

We now show how to eliminate the connectives * and -- * , i.e., to transform a formula of the form ϕ 1 * ϕ 2 or ϕ 1 -- * ϕ 2 into an equivalent boolean combination of test formulae, assuming ϕ 1 and ϕ 2 have already been transformed. We solve this problem by restricting ourselves to the case where ϕ 1 and ϕ 2 are minterms satisfying some additional properties. We first consider the separating conjunction. Lemma 5.16. Let M 1 , M 2 be two minterms that are footprint-consistent and E-complete for Var(M 1 ∪ M 2 ), with atoms(M

p 1 ) = atoms(M p 2 ). Then M 1 * M 2 ≡ elim * (M 1 , M 2 ), where elim * (M 1 , M 2 ) def = M e 1 ∧ M e 2 ∧ M f 1 ∧ M f 2 ∧ dc(M 1 ) u ∧ dc(M 2 ) u ∧ (2)
x ∈av(M 1 ), y ∈av(M 2 )

¬x ≈ y ∧ fp a (M 1 ) ∧ fp a (M 2 ) ∧ (3) nalloc(nv(M 1 ) ∩ nv(M 2 )) ∧ npto(M 1 , M 2 ) ∧ (4) |h| ≥ min M 1 + min M 2 ∧ |h| < max M 1 + max M 2 -1 (5) ∧ η 12 ∧ η 21 (6)
and

η i j def = Y ⊆nv(M j )\av(M i ) alloc(Y ) → (|h| ≥ # a (M i ) + |Y | M i + min M j ∧ # a (M i ) + |Y | M i < max M i ) .
Intuitively, if M 1 and M 2 hold separately, then all heap-independent literals from M 1 ∪ M 2 must be satisfied (2), the variables allocated in M 1 and M 2 must be pairwise distinct and their footprints, relative to the allocated variables, jointly asserted (3). Moreover, unallocated variables on both sides must not be allocated and common negative points-to literals must be asserted [START_REF] Brotherston | Automated Cyclic Entailment Proofs in Separation Logic[END_REF]. Since the heap satisfying elim * (M 1 , M 2 ) is the disjoint union of the heaps for M 1 and M 2 , its bounds are the sum of the bounds on both sides (5) and the variables that M 2 never allocates (the set nv(M 2 )) may occur allocated in the heap of M 1 and vice versa, thus the constraints η 12 and η 21 , respectively [START_REF] Calcagno | From Separation Logic to First-Order Logic[END_REF].

The proof of Lemma 5.16 requires the following result: Proposition 5.17. Let M 1 , M 2 be two minterms that are footprint-consistent and E-complete for Var(M 1 ∪ M 2 ) and let S = (U, s, I, h) be a model of elim * (M 1 , M 2 ). Let L i , Y i , A i be the following sets, for i = 1, 2:

L i = {s(x ) ∈ dom(h) | x ∈ nv(M 3-i ) \ av(M i )} Y i = {x ∈ Var | s(x ) ∈ L i } A i = {s(x ) | x ∈ av(M i )} Then L 1 ∩ L 2 = ∅, L i ∩ (A 1 ∪ A 2 ) = ∅ (for i = 1, 2) and S |= alloc(Y 1 ) ∧ alloc(Y 2 ).
Proof. We have the following results:

• L 1 ∩ L 2 = ∅. By contradiction, suppose that there exists ℓ ∈ L 1 ∩ L 2 . Then ℓ = s(y 1 ) = s(y 2 ) for some y 1 ∈ nv(M 1 ) and y 2 ∈ nv(M 2 ). Because M 1 is E-complete for Var(M 1 ∪ M 2 ), exactly one of y 1 ≈ y 2 , ¬y 1 ≈ y 2 belongs to M 1 . But ¬y 1 ≈ y 2 ∈ M 1 contradicts s(y 1 ) = s(y 2 ) and y 1 ≈ y 2 ∈ M 1 leads to

The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates • 19

y 2 ∈ nv(M 1 ). Symmetrically, y 1 ∈ nv(M 2 ), thus y 1 , y 2 ∈ nalloc(nv(M 1 ) ∩ nv(M 2 )). Since (U, s, I, h) |= nalloc(nv(M 1 ) ∩ nv(M 2 )
) by ( 4), we have ℓ dom(h), which contradicts with the fact that L 1 ∪ L 2 ⊆ dom(h), according to the definition of L 1 and L 2 . 3), ( 4), ( 5) and ( 6).

• L i ∩ (A 1 ∪ A 2 ) = ∅. First, L i ∩ A i = ∅ because M i is E-complete for Var(M 1 ∪ M 2 ),
(2) Since (U, s, I,

h i ) |= M e i ∧ M u i ∧ M f i , by Proposition 5.3, we also have (U, s, I, h) |= M e i ∧ M u i ∧ M f i , for i = 1, 2
. By Proposition 5.15, we obtain further that (U, s, I, h) |= dc(M i ) u , for i = 1, 2.

(3) Since dom(h 1 ) ∩ dom(h 2 ) = ∅, for every x ∈ av(M 1 ) and y ∈ av(M 2 ), we must have s(x ) s(y), hence S |= ¬x ≈ y. Further, we have (U, s, I, h i ) |= M i , thus (U, s, I, h i ) |= fp a (M i ) and, by Proposition 5.7, (U, s, I, h) |= fp a (M i ), for i = 1, 2. (4) Consider a variable x ∈ nv(M 1 ) ∩ nv(M 2 ). Then there exist variables x 1 and x 2 such that ¬alloc(x 1 ) ∈ M 1 , x ≈ M 1 x 1 , ¬alloc(x 2 ) ∈ M 2 and x ≈ M 2 x 2 . Hence s(x ) = s(x 1 ) dom(h 1 ) and s(x ) = s(x 2 ) dom(h 2 ), thus s(x ) dom(h) and (U, s, I, h) |= ¬alloc(x ). Since x was chosen arbitrarily, we have (U, s, I, h) |= nalloc(nv(M 1 ) ∩ nv(M 2 )). Secondly, let ¬x → y ∈ M 1 ∩ M 2 , for some x av(M 1 ∪ M 2 ). Since dom(h 1 ) ∩ dom(h 2 ) = ∅, only the following are possible: i. s(x ) ∈ dom(h 1 ). Since (U, s, I, h 1 ) |= M 1 , we must have h 1 (s(x )) s(y). Then h(s(x )) s(y) thus (U, s, I, h) |= ¬x → y. ii. s(x ) ∈ dom(h 2 ) and h 2 (x ) s(y) is symmetrical. iii. s(x ) dom(h 1 ) ∪ dom(h 2 ), then s(x ) dom(h) and (U, s, I, h) |= ¬x → y. Since ¬x → y ∈ npto(M 1 , M 2 ) was chosen arbitrarily, (U, s,

I, h) |= npto(M 1 , M 2 ). (5) Since h = h 1 ⊎ h 2 ,
) ∈ dom(h). Moreover, s(Y ) ∩ s(av(M 1 )) = ∅ because Y ∩ av(M 1 ) = ∅ and M 1 is E-complete for Var(M 1 ∪ M 2 ), by Proposition 5.11. Thus # a (M 1 ) + |Y | M 1 ≤ ||h 1 || < max S M 1 and ||h|| = ||h 1 || + ||h 2 || ≥ # a (M 1 ) + |Y | M 1 + min S M 2 , as required. • elim * (M 1 , M 2 ) |= M 1 * M 2 .
Let S = (U, s, I, h) be a model of elim * (M 1 , M 2 ). We will find h 1 and h 2 such that h = h 1 ⊎h 2 and (U, s, I, 5), we have, by Proposition 4.2:

h i ) |= M i , for i = 1, 2. Since S |= min M 1 +min M 2 ≤ |h|∧|h| < max M 1 +max M 2 -1 by (
min S M 1 + min S M 2 ≤ ||h|| < max S M 1 + max S M 2 -1 (7)
Let us now define the following sets, for i = 1, 2:

L i = {s(x ) ∈ dom(h) | x ∈ nv(M 3-i ) \ av(M i )} Y i = {x ∈ Var | s(x ) ∈ L i } A i = {s(x ) | x ∈ av(M i )}
By Proposition 5.17, we have

L 1 ∩ L 2 = ∅, L i ∩ (A 1 ∪ A 2 ) = ∅, for i = 1,
max I M 1 max I M 2 | |A 1 | | + | |L 1 | | | |A 2 | | + | |L 2 | | (b) max(||A 1 || + ||L 1 ||, min I M 1 ) max(||A 2 || + ||L 2 ||, min I M 2 ) max I M 1 max I M 2 | |A 1 | | + | |L 1 | | | |A 2 | | + | |L 2 | | n 1 n 2 (a) n 1 n 2 |h |
Fig. 1 Furthermore, we have ||h|| < max S M 1 + max S M 2 -1 by [START_REF] Calcagno | Computability and Complexity Results for a Spatial Assertion Language for Data Structures[END_REF] and one of the following cases holds (see Fig. 1): 1 (a)). We have that n 1 ≥ 0 by [START_REF] Demri | The Effects of Adding Reachability Predicates in Propositional Separation Logic[END_REF] and n 2 ≥ 0 by the hypothesis max

(1) If max S M 1 -1 ≤ ||h|| -max(||A 2 || + ||L 2 ||, min S M 2 ) then let n 1 def = max S M 1 -||A 1 || -||L 1 || -1 and n 2 def = ||h|| -max S M 1 -||A 2 || -||L 2 || + 1 (Fig.
S M 1 -1 ≤ ||h|| -max(||A 2 || + ||L 2 ||, min S M 2 ). (2) Otherwise, let n 1 def = ||h|| -||A 1 || -||L 1 || -max S (||A 2 || + ||L 2 ||, min S M 2 ) and n 2 def = max S (||A 2 || + ||L 2 ||, min S M 2 ) -||A 2 || -||L 2 || (Fig. 1 (b)
). We have n 1 ≥ 0 by [START_REF] Echenim | Prenex Separation Logic with One Selector Field[END_REF] and n 2 ≥ 0 is immediate. In both cases, the following holds, for i = 1, 2:

min S M i ≤ ||A i || + ||L i || + n i < max S M i (11)
We have used the fact that min S M i < max S M i , for i = 1, 2, which is a consequence of the fact that S |= dc(M i ) u , by (2) and Proposition 5.14.

The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates • 21

Further, we have that ||h|| = i=1,2 ||A i || + ||L i || + n i . Moreover, there are exactly n 1 + n 2 locations in dom(h) \ (A 1 ∪ L 1 ∪ A 2 ∪ L 2 ), thus we can partition this set into N 1 and N 2 such that ||N i || = n i and define h i to be the restriction of h to A i ∪ L i ∪ N i , for i = 1, 2. It remains to be shown that (U, s, I, h i ) |= M i , for i = 1, 2. Below we do the proof for i = 1, the case i = 2 being similar.

Clearly, (U, s, I, 3). Since h and h 1 agree on A 1 , we also have (U, s, I, h 1 ) |= x → y. Dually, let ¬x → y ∈ M p 1 . If x ∈ av(M 1 ) then ¬x → y ∈ fp a (M 1 ), thus (U, s, I, h 1 ) |= ¬x → y, since h and h 1 agree on A 1 . Otherwise, if x av(M 1 ), we distinguish the cases:

h 1 ) |= M e 1 ∧ M f 1 ∧ M u 1 , because (U, s, I, h) |= M e 1 ∧ M f 1 ∧ dc(M 1 ) u ,
-if x ∈ av(M 2 ) then s(x ) ∈ A 2 ,
M 1 = E ∪ {|h| ≥ 2, |h| < 4, x → y, alloc(y), ¬y → x, ¬z → z} M 2 = E ∪ {|h| ≥ 1, |h| < 2} with E = {¬x ≈ y, ¬y ≈ z, ¬x ≈ z}. Then M 1 * M 2 ≡ E ∪ {|h| ≥ 3, |h| < 5, x → y, alloc(y), ¬y → x }. Let M ′ 1 = {|h| ≥ 0, |h| < 1, ¬x ≈ y} and M ′ 2 = {|h| ≥ 0, |h| < ∞, ¬x ≈ y, ¬alloc(x )}. Then M ′ 1 * M ′ 2 ≡ {|h| ≥ 0, |h| < ∞, alloc(x ) → 1 < 1} ≡ {|h| ≥ 0, |h| < ∞, ¬alloc(x )}. Indeed, no model of M ′
1 * M ′ 2 may allocate x since the part of the heap that corresponds to M ′ 1 is empty and M ′ 2 |= ¬alloc(x ). ■ Remark 5.19. Note that elim * (M 1 , M 2 ) contains negative occurrences of test formulae alloc(x ) that do not occur in M 1 ∪ M 2 . Such occurrences are introduced at Lines 4 and 6, due to the fact that we consider the closure of ¬alloc(x ) formulae w.r.t. all the equalities in M 1 , M 2 . For example, if M 1 = ¬alloc(x ), x ≈ y, |h| ≥ 0, |h| < ∞ and M 2 = {|h| ≥ 0, |h| < ∞}, then y ∈ nv(M 1 ) and alloc(y) occurs at negative polarity in elim * (M 1 , M 2 ). This is problematic because upcoming results depend on the fact that the polarity of alloc(x ) formulae is preserved (Lemma 5.29). However, if alloc(x ) occurs at a negative polarity in elim * (M 1 , M 2 ), then there exists a literal ¬alloc(

x ′ ) ∈ M 1 ∪ M 2 , such that elim * (M 1 , M 2 ) |= x ≈ x ′ ,
making the negative occurrence of alloc(x ) actually redundant. Consequently, equivalence is preserved when only the test formulae alloc(x ) such that ¬alloc(x ) ∈ M 1 ∪ M 2 occur at negative polarity in elim * (M 1 , M 2 ). This refined version of elim * (M 1 , M 2 ) is used in the proof of Lemma 5.29. However, taking this observation into account at this point would clutter the definition of elim * (M 1 , M 2 ). ■

Next, we show a similar result for the separating implication. For technical convenience, we translate the septraction M 1 ⊸ M 2 , instead of M 1 -- * M 2 , as an equivalent boolean combination of test formulae. This is without loss of generality, because M 1 -- * M 2 ≡ ¬(M 1 ⊸ ¬M 2 ). Unlike with the case of the separating conjuction (Lemma 5.16), here the definition of the boolean combination of test formulae depends on whether the universe is finite or infinite.

If the complement of some literal ℓ ∈ fp a (M 1 ) belongs to M 2 then no extension by a heap that satisfies ℓ may satisfy ℓ. Therefore, as an additional simplifying assumption, we suppose that fp a (M 1 ) ∩ M 2 = ∅, so that M 1 ⊸ M 2 is not trivially unsatisfiable. Lemma 5.20. Let M 1 and M 2 be footprint-consistent minterms that are E-complete for Var(M 1 ∪ M 2 ), such that:

(a) M 1 is A-complete for Var(M 1 ∪ M 2 ), (b) atoms(M a 2 ∪ M p 2 ) ⊆ atoms(M a 1 ∪ M p 1 ), and (c) fp a (M 1 ) ∩ M 2 = ∅. Then, M 1 ⊸ M 2 ≡ fin elim fin ⊸ (M 1 , M 2 ) and M 1 ⊸ M 2 ≡ inf elim inf ⊸ (M 1 , M 2 ), where: elim † ⊸ (M 1 , M 2 ) def = pc(M 1 ) e ∧ M e 2 ∧ M f 1 ∧ M f 2 ∧ dc(M 1 ) u ∧ dc(M 2 ) u ∧ (12) nalloc(av(M 1 )) ∧ fp nv(M 1 ) (M 2 ) ∧ (13) |h| ≥ min M 2 -max M 1 + 1 ∧ |h| < max M 2 -min M 1 (14) ∧ λ † ( 15
)
with λ fin def = Y ⊆Var(M 1 ∪M 2 ) nalloc(Y ) → |h| < |U | -min M 1 -# n (Y , M 1 ) + 1 ∧ |U | ≥ min M 2 + # n (Y , M 1 )
, and

λ inf def = ⊤.
Intuitively, a heap satisfies M 1 ⊸ M 2 iff it has an extension, by a disjoint heap satisfying M 1 , that satisfies M 2 . Thus, elim † ⊸ (M 1 , M 2 ) must entail the heap-independent literals of both M 1 and M 2 [START_REF] Fontaine | Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class[END_REF]. Next, no variable allocated by M 1 must be allocated by elim † ⊸ (M 1 , M 2 ), otherwise no extension by a heap satisfying M 1 is possible and, moreover, the footprint of M 2 relative to the unallocated variables of M 1 must be asserted [START_REF] Iosif | The Tree Width of Separation Logic with Recursive Definitions[END_REF]. The heap's cardinality constraints depend on the bounds of M 1 and M 2 [START_REF] Samin | BI as an assertion language for mutable data structures[END_REF] and, if Y is a set of variables not allocated in the heap, these variables can be allocated in the extension [START_REF] Katelaan | Effective Entailment Checking for Separation Logic with Inductive Definitions[END_REF]. Actually, this is where the finite universe assumption first comes into play. If the universe is infinite, then there are enough locations outside the heap to be assigned to Y . However, if the universe is finite, then it is necessary to ensure that there are at least # n (Y , M 1 ) free locations to be assigned to Y [START_REF] Katelaan | Effective Entailment Checking for Separation Logic with Inductive Definitions[END_REF]. We now give the proof of Lemma 5.20.

Proof. If pc(M

1 ) = ⊥ then M 1 ⊸ M 2 ≡ elim ⊸ (M 1 , M 2 ) ≡ ⊥. Also, since M 1 and M 2 are E-complete for Var(M 1 ∪ M 2 ), if we suppose that M e 1 M e 2 then M 1 ⊸ M 2 ≡ elim ⊸ (M 1 , M 2 ) ≡ ⊥.
From now on, we will assume that pc(M 1 ) = M 1 and

M e 1 = M e 2 . • M 1 ⊸ M 2 |= elim ⊸ (M 1 , M 2 ). Let S = (U, s, I, h) be a structure such that S |= M 1 ⊸ M 2 . Then there exists a heap h ′ disjoint from h such that (U, s, I, h ′ ) |= M 1 and (U, s, I, h ⊎ h ′ ) |= M 2 .
Below we prove that S is also a model of the formulae ( 12), ( 13), ( 14) and ( 15), respectively.

(

) We have (U, s, I, h ′ ) |= M e 1 ∧ M u 1 ∧ M f 1 , thus (U, s, I, h) |= M e 1 ∧ M u 1 ∧ M f 1 by 12
M 2 ≤ ||h||+||h ′ || < max S M 2 . Since (U, s, I, h ′ ) |= M 1 we also have min S M 1 ≤ ||h ′ || < max S M 1 , thus min S M 1 ≤ ||h ′ || ≤ max S M 1 -1, i.e., -max S M 1 + 1 ≤ -||h ′ || ≤ -min S M 1 so that min S M 2 -max S M 1 + 1 ≤ ||h|| < max S M 2 -min S M 1 . (15) Assume that (U, s, I, h) |= nalloc(Y ) for a set Y ⊆ Var(M 1 ∪ M 2 ), which implies that dom(h) ∩ s(Y ) = ∅. Since (U, s, I, h ′ ) |= M 1 , we also have dom(h ′ ) ∩ s(nv(M 1 )) = ∅. Thus ||U|| ≥ ||h|| + ||h ′ || + ||s(Y ∩ nv(M 1 ))|| ≥ ||h||+min S M 1 +# n (Y , M 1 ), because ||h ′ || ≥ min S M 1 and ||s(Y ∩ nv(M 1 ))|| = |Y ∩ nv(M 1 )| M 1 = # n (Y , M 1 ), by Proposition 5.5, since M 1 is E-complete. Therefore, ||h|| ≤ ||U|| -min S M 1 -# n (Y , M 1 ). Moreover, since (U, s, I, h ⊎ h ′ ) |= M 2 , we obtain |U | ≥ ||h ⊎ h ′ || + # n (Y , M 1 ) ≥ min S M 2 + # n (Y , M 1 ). • elim ⊸ (M 1 , M 2 ) |= M 1 ⊸ M 2 . Let S = (U, s, I, h) be a structure such that S |= elim ⊸ (M 1 , M 2 ). We build a heap h ′ such that dom(h) ∩ dom(h ′ ) = ∅, (U, s, I, h ′ ) |= M 1 and (U, s, I, h ⊎ h ′ ) |= M 2 . First, for each variable x ∈ av(M 1 ) such that x ′ → y ∈ M p 1 for some variable x ′ with x ≈ M 1 x ′ , we add the tuple (s(x ), s(y)) to h ′ . Since (U, s, I, h) |= pc(M 1 ) e , for any pair of variables x ≈ M 1 x ′ if x → y, x ′ → y ′ ∈ M 1 then y i ≈ M 1 y ′ i
, and the result is a functional relation. We define:

A = {x ∈ av(M 1 ) | ∀x ′ ∀y . x ≈ M 1 x ′ → x ′ → y M p 1 } V x = {(s(y 1 ), . . . , s(y k )) ∈ U k | x ≈ M 1 x ′ , ¬x ′ → y ∈ M p 1 }, for x ∈ av(M 1 ) N = {x ∈ Var(M 1 ∪ M 2 ) | s(x ) dom(h)}
Intuitively, A denotes the set of variables that must be allocated but with no constraint on their image; this set is independent of the interpretation under consideration. The set V x denotes the set of images the allocated variable x cannot point to, and N denotes the set of variables that are not allocated in h. For each x ∈ A we choose a tuple (ℓ 1 , . . . , ℓ k ) ∈ U k \ V x and let h ′ (s(x )) = (ℓ 1 , . . . , ℓ k ). Since M 1 is E-complete, we have ||V x || ≤ δ x (M 1 ) for each x ∈ A, and such a choice is possible because (U, s, [START_REF] Samin | BI as an assertion language for mutable data structures[END_REF] it must be the case that:

I, h) |= dc(M 1 ) u , thus ||U k || ≥ δ x (M 1 ) + 1. Since (U, s, I, h) |= nalloc(N ), if U is finite, by
||h|| < ||U|| -min S M 1 -# n (N , M 1 ) + 1 (16) ||U|| ≥ min S M 2 + # n (N , M 1 ) (17)
Finally, let

L ⊆ U \ (dom(h) ∪ s(av(M 1 )) ∪ s(nv(M 1 ))) be a finite set of locations of cardinality ||L|| = max(min S M 1 , min S M 2 -||h||) -# a (M 1
). Choosing such a set L is possible, because either U is infinite, or U is finite, in which case:

||U|| ≥ max(min S M 1 + ||h||, min S M 2 ) + # n (N , M 1 )
, by ( 16) and ( 17)

≥ max(min S M 1 , min S M 2 -||h||) -# a (M 1 ) + ||h|| + # a (M 1 ) + # n (N , M 1 ) = ||L|| + ||h|| + # a (M 1 ) + # n (N , M 1 ) ≥ ||L|| + ||dom(h) ∪ s(av(M 1 )) ∪ s(nv(M 1 ))||
where the last inequality is a consequence of Proposition 5.5. We choose an arbitrary tuple (ℓ 1 , . . . , ℓ k ) ∈ U k and let h ′ (ℓ) = (ℓ 1 , . . . , ℓ k ) for all ℓ ∈ L. Because U is non-empty, such a tuple exists. Consequently, we have dom(h ′ ) = s(av(M 1 )) ∪ L and dom(h ′ ) ∩ dom(h) = ∅ because s(av(M 1 )) ∩ dom(h) = ∅ by ( 13) and L ∩ dom(h) = ∅ by construction. We now prove: [START_REF] Fontaine | Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class[END_REF] and Proposition 5.15. To show (U, s, I, h ′ ) |= M a 1 , observe that s(x ) ∈ dom(h ′ ) for each x ∈ av(M 1 ), hence for each literal alloc(x ) ∈ M 1 we have (U, s, I, h ′ ) |= alloc(x ). Moreover, we have dom(h ′ ) ∩ s(nv(M 1 )) = (s(av(M 1 )) ∪ L) ∩ s(nv(M 1 )) = ∅, because M 1 is footprint consistent and E-complete for Var(M 1 ∪ M 2 ), by Proposition 5.11. Thus (U, s,

-(U, s, I, h ′ ) |= M 1 . Clearly (U, s, I, h) |= M e 1 ∧M u 1 ∧M f 1 by
I, h ′ ) |= ¬alloc(x ) for each literal ¬alloc(x ) ∈ M a 1 . For each literal x → y ∈ M p 1 we have h ′ (s(x )) = (s(y 1 ), . . . , s(y k )) by construction, thus (U, s, I, h ′ ) |= x → y. For each literal ¬x → y ∈ M p 1 , we distinguish two cases. * If x ∈ av(M 1 ), then (s(y 1 ), . . . , s(y k )) ∈ V x hence h(s(x )) (s(y 1 ), . . . , s(y k )) by construction. * If x av(M 1 ), then since M 1 is A-complete for Var(M 1 ∪ M 2 ), we have x ∈ nv(M 1 ), thus s(x ) dom(h ′ ) = s(av(M 1 )) ∪ L. We finally prove that (U, s, I, h ′ ) |= |h| ≥ min M 1 ∧ |h| < max M 1 . Since dom(h ′ ) = s(av(M 1 )) ∪ L and s(av(M 1 ))∩L = ∅, we have ||h ′ || = ||s(av(M 1 ))||+||L|| = max(min S M 1 , min S M 2 -||h||). If ||h ′ || = min I M 1 then ||h ′ || < max I M 1 because S |= dc(M 1 ) u , which implies that min S M 1 < max S M 1 ,
) ||h|| ≥ min I M 2 -max I M 1 +1, thus ||h|| > min I M 2 -max I M 1 , and therefore ||h ′ || < max I M 1 . -(U, s, I, h ′ ⊎ h) |= M 2 . We have (U, s, I, h ′ ⊎h) |= M e 2 ∧M f 2 ∧M u 2 because (U, s, I, h) |= M e 2 ∧M
f 2 ∧M u 2 and these formulae do not depend on the heap. Next, for a given variable x, let [START_REF] Iosif | The Tree Width of Separation Logic with Recursive Definitions[END_REF]. Moreover, because h and h ⊎ h ′ agree on s(nv(M 1 )),

α x ∈ {alloc(x ), ¬alloc(x ), x → y, ¬x → y | y ∈ Var k } ∩ M 2 be a literal and let α x denote its complement. If x ∈ nv(M 1 ) then α x ∈ fp nv(M 1 ) (M 2 ) and (U, s, I, h) |= α x by
we obtain (U, s, I, h ⊎ h ′ ) |= α x . Otherwise x nv(M 1 ) hence x ∈ av(M 1 ) because M 1 is A-complete for Var(M 1 ∪ M 2 ), and since α x ∈ M a 2 ∪ M p 2 and atoms(M a 2 ∪ M a 2 ) ⊆ atoms(M a 1 ∪ M p 1
), we have α x ∈ fp a (M 1 ), because the case α x ∈ fp a (M 1 ) is in contradiction with fp a (M 1 ) ∩ M 2 = ∅ (condition (c) of the Lemma). But then (U, s, I, h ′ ) |= α x and (U, s, I, h ⊎ h ′ ) |= α x follows, by Proposition 5.7. We have thus proved that (U, s, I, h⊎h ′ ) |= M a 2 ∪M p 2 . We are left with proving that min S M 2 ≤ ||h||+||h ′ || = max(min [START_REF] Samin | BI as an assertion language for mutable data structures[END_REF].

I M 1 + ||h||, min S M 2 ) < max S M 2 . If min S M 1 + ||h|| ≤ min S M 2 the
□ Example 5.21. Let M 1 = {alloc(x ), ¬alloc(y), ¬x ≈ y, |h| ≥ 1, |h| < 2}, M 2 = {¬x ≈ y, |h| ≥ 3, |h| < ∞, ¬x → x, ¬y → y}. Then M 1 ⊸ M 2 ≡ inf {|h| ≥ 2, |h| < ∞, ¬alloc(x ), ¬y → y}. ■

Translating Quantifier-free SL k into Minterms

We prove next that each quantifier-free SL k formula is equivalent to a finite disjunction of minterms. Intuitively, these disjunctions are defined by induction on the structure of the formula. The base cases and classical connectives are easy to handle. For formulae ψ 1 * ψ 2 or ψ 1 ⊸ ψ 2 , the transformation is first applied on ψ 1 and ψ 2 , then the following equivalences are used to shift * and ⊸ innermost in the formula:

(ϕ 1 ∨ ϕ 2 ) * ϕ ≡ (ϕ 1 * ϕ) ∨ (ϕ 2 * ϕ) (ϕ 1 ∨ ϕ 2 ) ⊸ ϕ ≡ (ϕ 1 ⊸ ϕ) ∨ (ϕ 2 ⊸ ϕ) ϕ * (ϕ 1 ∨ ϕ 2 ) ≡ (ϕ * ϕ 1 ) ∨ (ϕ * ϕ 2 ) ϕ ⊸ (ϕ 1 ∨ ϕ 2 ) ≡ (ϕ ⊸ ϕ 1 ) ∨ (ϕ ⊸ ϕ 2 )
The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates • 25

Afterwards, the operands of * and ⊸ are minterms, and the result is obtained using the equivalences from Lemmas 5.16 and 5.20, respectively (up to a transformation into disjunctive normal form). The only difficulty is that these lemmas impose some additional conditions on the minterms (e.g., being E-complete, or A-complete). However, the conditions are easy to enforce by case splitting, as illustrated by Example 5.22.

Example 5.22. Consider the formula x → x ⊸ y → y. It is easy to check that x → x ≡ M 1 , where

M 1 = x → x ∧ |h| ≥ 1 ∧ |h| < 2 and y → y ≡ M 2 , where M 2 = y → y ∧ |h| ≥ 1 ∧ |h| < 2.
To apply Lemma 5.20, we need to ensure that M 1 and M 2 are E-complete, which may be done by adding either x ≈ y or x ̸ ≈ y to each minterm. We also have to ensure that M 1 is A-complete, thus for z ∈ x, y , we add either alloc(z) or ¬alloc(z) to M 1 . Finally, we must have

atoms(M a 2 ∪ M p 2 ) ⊆ atoms(M a 1 ∪ M p 1
), thus we add either y → y or ¬y → y to M 1 . After removing redundancies, we get (among others) the minterms:

M ′ 1 = x → x ∧ |h| ≥ 1 ∧ |h| < 2 ∧ x ≈ y and M ′ 2 = y → y ∧ |h| ≥ 1 ∧ |h| < 2 ∧ x ≈ y. Afterwards we compute elim fin ⊸ (M ′ 1 , M ′ 2 ) = x ≈ y ∧ ¬alloc(x ) ∧ |h| ≥ 0 ∧ |h| < 1. ■
To describe the transformation in a more formal way, we first need to show that the conjunction of two minterms can be written as a disjunction of minterms. To this aim, given minterms M 1 and M 2 , we define the sets of constraints minh(M 1 , M 2 ) and maxh(M 1 , M 2 ) by taking the conjunction of the lower and upper bounds on the cardinality of the heap and keeping the most restrictive bounds. Definition 5.23.

minh(M 1 , M 2 ) def =                            |h| ≥ max(min M 1 , min M 2 ) if min M 1 , min M 2 ∈ N |h| ≥ min M i ∧ |U | < min M i + m + 1, |h| ≥ min M 3-i ∧ |U | ≥ min M i + m + 1 if min M i ∈ N, min M 3-i = |U | -m, i = 1, 2 {|h| ≥ |U | -min(m 1 , m 2 )} if min M i = |U | -m i , i = 1, 2 maxh(M 1 , M 2 ) def =                                      |h| < min(max M 1 , max M 2 ) if max M 1 , max M 2 ∈ N ∞ |h| < max M i if max M 3-i = ∞, max M i = |U | -m, i = 1, 2 |h| < max M i ∧ |U | ≥ max M i + m, |h| < |U | -m ∧ |U | < max M i + m if max M i ∈ N, max M 3-i = |U | -m, i = 1, 2 {|h| < |U | -max(m 1 , m 2 )} if max M i = |U | -m i , i = 1, 2 For instance, if M 1 = {|h| ≥ 2, |h| < |U | -1} and M 2 = {|h| ≥ 3, |h| < |U | -2}, then minh(M 1 , M 2 ) = {|h| ≥ 3} and maxh(M 1 , M 2 ) = {|h| < |U | -2}.
Heterogeneous constraints are merged by performing a case split on the value of |U |. For example, if

M 1 = {|h| ≥ |U | -4} and M 2 = {|h| ≥ 1}, then the first condition prevails if |U | ≥ 5 yielding: minh(M 1 , M 2 ) = {|h| ≥ 1 ∧ |U | < 5, |h| ≥ |U | -4 ∧ |U | ≥ 5}.
The disjunction of minterms equivalent to a conjunction of two minterms is then defined as follows:

Definition 5.24. For any minterms M 1 , M 2 , let [M 1 , M 2 ] def = i=1,2 M e i ∧ M f i ∧ M a i ∧ M p i ∧ M u i ∧ µ ∧ ν | µ ∈ minh(M 1 , M 2 ), ν ∈ maxh(M 1 , M 2 )
. We extend this notation recursively to any set of minterms of size n > 2:

[M 1 , M 2 , . . . , M n ] def = M ∈[M 1 , ..., M n-1 ] [M, M n ]. Proposition 5.25. Given minterms M 1 , . . . , M n , we have n i=1 M i ≡ M ∈[M 1 , ..., M n ] M.
Proof. We prove the result for n = 2, the general result follows by induction. For n = 2, this is a consequence of the fact that |h| ≥ min

M 1 ∧ |h| ≥ min M 2 ≡ µ ∈minh(M 1 , M 2 ) µ, and |h| < max M 1 ∧ |h| < max M 2 ≡ ν ∈maxh(M 1 , M 2 ) ν .
We prove the first fact in the case where min

• if m 1 ≥ ||U || -m 2 , then necessarily ||U|| < m 1 + m 2 + 1, so that S |= |h| ≥ m 1 ∧ |U | < m 1 + m 2 + 1. • otherwise, we have ||U || ≥ m 1 + m 2 + 1, so that S |= |h| ≥ |U | -m 2 ∧ |U | ≥ m 1 + m 2 + 1. Conversely, if S is a structure such that either S |= |h| ≥ m 1 ∧ |U | < m 1 + m 2 + 1 or S |= |h| ≥ |U | -m 2 ∧ |U | ≥ m 1 + m 2 + 1, then it is straightforward to verify that S |= |h| ≥ m 1 ∧ |h| ≥ |U | -m 2 .
□

The following proposition states some properties of the literals occurring in [M 1 , . . . , M n ].

Proposition 5.26.

Given minterms M 1 , . . . , M n and M ∈ [M 1 , . . . , M n ], if ℓ ∈ M is a literal then either ℓ ∈ M i , for some i = 1, . . . , n, or ℓ ∈ {|U | ≥ m 1 + m 2 , |U | < m 1 + m 2 , |U | ≥ m 1 + m 2 + 1, |U | < m 1 + m 2 + 1}, where M 1 ∪ • • • ∪ M n contains two literals ℓ i ∈ {|h| ≥ m i , |h| < m i , |h| ≥ |U | -m i , |h| < |U | -m i }, for i = 1, 2. Proof. Assume that n = 2. If ℓ M 1 ∪M 2 then by definition of [M 1 , M 2 ], necessarily ℓ occurs in minh(M 1 , M 2 )∪ maxh(M 1 , M 2
) and the proof is immediate, by definition of these sets. The proof for n > 2 goes by induction on n. □ For two sets K, L of literals, a completion of K w.r.t. L is a set of literals K ′ that is minimal with respect to inclusion of sets, such that K ⊆ K ′ and atoms(L) ⊆ atoms(K ) (i.e., K ⊆ K ′ and for every ℓ ∈ L, K ′ contains either ℓ or ℓ). We denote by (K ) L the set of completions of K w.r.t. L. Proposition 5.27. If K and L are sets of literals, then K ≡ ψ ∈(K ) L ψ . If further K is a minterm and L contains no literals of the form |h| ≥ t or |h| < t, then every set P ∈ (K ) L is a minterm such that Var(P ) = Var(K ) ∪ Var(L), min P = min K and max P = max K .

Proof. Immediate, by the definition of (K ) L . □

For a literal ℓ, let [ℓ] mt be an equivalent minterm obtained from ℓ by adding the missing lower/upper bounds on the cardinality of the heap, namely

|h| ≥ 0 if ℓ {|h| ≥ n, |h| ≥ |U | -n | n ∈ Z}} and |h| < ∞ if ℓ {|h| < n, |h| < |U |-n | n ∈ Z}.
We extend this notation to sets (i.e., conjunctions) of literals as [ℓ 1 , . . . , ℓ n ] mt def = [[ℓ 1 ] mt , . . . , [ℓ n ] mt ]. We have ℓ ≡ [ℓ] mt for any literal ℓ and L ≡ M ∈[L] mt M, for any set L of literals. For a boolean combination of literals ϕ, we denote by (ϕ) dnf its disjunctive normal form. We assume from now on that the disjunctive normal form of a formula is canonical and all the conjunctions are incomparable with respect to logical entailment.

Given a formula ϕ in disjunctive normal form ϕ = n i=1 C i , where C 1 , . . . , C n are conjunctions (represented by sets) of literals, we define

ϕ mt def = n i=1 [C i ] mt . We have ϕ mt ≡ M ∈[ϕ] mt M. Further, let E(L) def = x ≈ y | x, y ∈ Var(L) and A(L) def = {alloc(x ) | x ∈ Var(L)}
, for a set L of literals. For each † ∈ fin, inf , we define the set of minterms µ † (ϕ) recursively on the structure of ϕ: The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates • 27

µ † (emp) def = {|h| ≃ 0} µ † (x → y) def = x → y ∧ |h| ≃ 1 µ † (x ≈ y) def = x ≈ y ∧ |h| ≥ 0 ∧ |h| < ∞ µ † (q(x 1 , . . . , x #(q) ) def = q(x 1 , . . . , x #(q) ) ∧ |h| ≥ 0 ∧ |h|
µ † (ϕ 1 ∧ ϕ 2 ) def = M i ∈µ † (ϕ i ) i=1,2 [M 1 , M 2 ] µ † (¬ϕ 1 ) def = ℓ 1 , . . . , ℓ n mt ℓ i ∈ M i , i ∈ [1, n] , where µ † (ϕ 1 ) = {M 1 , . . . , M n } µ † (ϕ 1 * ϕ 2 ) def = M i ∈µ † (ϕ i ) i=1,2
(elim * (P 1 , P 2 )) dnf mt N j ∈ (M j ) E(M 1 ∪M 2 ) , P j ∈ (N j ) N p 3-j , j = 1, 2

µ † (ϕ 1 ⊸ ϕ 2 ) def = M i ∈µ † (ϕ i ) i=1,2 elim † ⊸ (Q 1 , N 2 ) dnf mt N j ∈ (M j ) E(M 1 ∪M 2 ) , P 1 ∈ (N 1 ) A(M 1 ∪M 2 ) , Q 1 ∈ (P 1 ) M a 2 ∪M p 2 , j = 1, 2
Intuitively, µ † (ϕ 1 * ϕ 2 ) and µ † (ϕ 1 ⊸ ϕ 2 ) are obtained by first recursively computing µ † (ϕ 1 ) and µ † (ϕ 2 ), then extending the obtained minterms in such a way that the hypotheses of Lemmas 5.16 or 5.20 are satisfied, and finally applying elim † * and elim † ⊸ , respectively.

Lemma 5.28. Given a quantifier-free SL k formula ϕ, the following equivalences hold: (1) ϕ ≡ fin M ∈µ fin (ϕ ) M, and (2) ϕ ≡ inf M ∈µ inf (ϕ ) M.

Proof. We show that ϕ ≡ fin M ∈µ fin (ϕ ) M by induction on the structure of ϕ. The fact that ϕ ≡ inf M ∈µ inf (ϕ ) M is proved in the same way. The base cases are immediate and the inductive cases are dealt with below:

• If ϕ = ϕ 1 ∧ ϕ 2 and ϕ i ≡ fin M i ∈µ fin (ϕ i ) M i for i = 1, 2 by the inductive hypothesis and Proposition 5.25, we have:

ϕ ≡ fin M 1 ∈µ fin (ϕ 1 ) M 1 ∧ M 2 ∈µ fin (ϕ 2 ) M 2 ≡ fin M i ∈µ fin (ϕ i ), i=1,2 M 1 ∧ M 2 ≡ fin M i ∈µ fin (ϕ i ), i=1,2 M ∈[M 1 , M 2 ] M • If ϕ = ¬ϕ 1 , µ fin (ϕ 1 ) = {M 1 , . . . , M n }, M i = ℓ i1 , . . . , ℓ in i for all i ∈ [1, n], then since ϕ 1 ≡ fin n i=1 n i
j=1 ℓ i j by the inductive hypothesis, we have:

¬ϕ 1 ≡ fin n i=1 n i j=1 ℓ i j ≡ fin n i=1 n i j=1 ℓ i j mt ≡ fin ℓ 1 mt ∧ . . . ∧ ℓ n mt ℓ i ∈ M i , i ∈ [1, n] ≡ fin ℓ 1 , . . . , ℓ n mt ℓ i ∈ M i , i ∈ [1, n]
• If ϕ = ϕ 1 * ϕ 2 and ϕ i ≡ fin M ∈µ fin (ϕ i ) M for i = 1, 2 by the induction hypothesis, we compute successively7 :

(ϕ 1 * ϕ 2 ) [distributivity of * with ∨] ≡ fin M i ∈µ fin (ϕ i ), i=1,2 M 1 * M 2 because M i ≡ N i ∈(M i ) E(M 1 ∪M 2 ) N i ≡ fin M i ∈µ fin (ϕ i ), i=1,2 N i ∈(M i ) E(M 1 ∪M 2 ) N 1 * N 2 because N i ≡ P i ∈(N i ) N p 3-i P i ≡ fin M i ∈µ fin (ϕ i ), i=1,2 N i ∈(M i ) E(M 1 ∪M 2 ) P i ∈(N i ) N p 3-i P 1 * P 2
At this point, observe that N i , and thus P i , are E-complete for Var(M 1 ∪ M 2 ), for i = 1, 2. Moreover, atoms(P p 1 ) = atoms(P p 2 ), because P i ∈ (N i ) N p 3-i , for i = 1, 2. We can thus apply Lemma 5.16 and infer that:

P 1 * P 2 ≡ elim * (P 1 , P 2 ) ≡ (elim * (P 1 , P 2 )) dnf ≡ M ∈ (elim * (P 1 , P 2 )) dnf mt M • If ϕ = ϕ 1 ⊸ ϕ 2 and ϕ i ≡ fin M ∈µ fin (ϕ i ) M, i = 1, 2
, by the induction hypothesis, we compute, successively:

(ϕ 1 ⊸ ϕ 2 ) [distributivity of ⊸ with ∨] ≡ fin M i ∈µ fin (ϕ i ), i=1,2 M 1 ⊸ M 2 because M i ≡ N i ∈(M i ) E(M 1 ∪M 2 ) N i ≡ fin M i ∈µ fin (ϕ i ), i=1,2 N i ∈(M i ) E(M 1 ∪M 2 ) N 1 ⊸ N 2 because N 1 ≡ P 1 ∈(N 1 ) A(M 1 ∪M 2 ) P 1 ≡ fin M i ∈µ fin (ϕ i ), i=1,2 N i ∈(M i ) E(M 1 ∪M 2 ) P 1 ∈(N 1 ) A(M 1 ∪M 2 ) P 1 ⊸ N 2 because P 1 ≡ Q 1 ∈(P 1 ) N a 2 ∪N p 2 Q 1 ≡ fin M i ∈µ fin (ϕ i ), i=1,2 N i ∈(M i ) E(M 1 ∪M 2 ) P 1 ∈(N 1 ) A(M 1 ∪M 2 ) Q 1 ∈(P 1 ) N a 2 ∪N p 2 Q 1 ⊸ N 2
Observe that N i and thus

P i are E-complete for Var(M 1 ∪ M 2 ), for i = 1, 2. Moreover, P 1 is A-complete for Var(M 1 ∪ M 2 ), because P 1 ∈ (N 1 ) A(M 1 ∪M 2 ) and atoms(N a 2 ∪ N p 2 ) ⊆ atoms(Q a 1 ∪ Q p 1 ), because Q 1 ∈ (P 1 ) N a 2 ∪N p 2 .
Then we can apply Lemma 5.20 and infer that:

Q 1 ⊸ N 2 ≡ fin elim fin ⊸ (Q 1 , N 2 ) ≡ elim fin ⊸ (Q 1 , N 2 ) dnf ≡ M ∈ elim fin ⊸ (Q 1 , N 2 ) dnf mt M □
As explained in Section 4.3, boolean combinations of minterms can only be transformed into sat-equivalent BSR(FO) formulae if there is no positive occurrence of test formulae |h| ≥ |U | -n or alloc(x ) (see Definition 4.8 and the second item of Lemma 4.9). Consequently, we relate the polarity of these formulae in some minterm M ∈ µ fin (ϕ) ∪ µ inf (ϕ) with that of a separating implication within ϕ. The analysis depends on whether the universe is finite or infinite. Lemma 5.29. For any quantifier-free SL k formula ϕ, the following properties hold:

(1) For all M ∈ µ inf (ϕ), we have

M ∩ {|h| ≥ |U | -n, |h| < |U | -n | n ∈ N} = ∅. (2) If |h| ≥ |U | -n ∈ M (resp. |h| < |U | -n ∈ M)
for some minterm M ∈ µ fin (ϕ), then a formula ψ 1 -- * ψ 2 occurs at a positive (resp. negative) polarity in ϕ.

(3) If alloc(x ) ∈ M (resp. ¬alloc(x ) ∈ M) for some minterm M ∈ µ inf (ϕ), then a formula ψ 1 -- * ψ 2 , such that x ∈ Var(ψ 1 ) ∪ Var(ψ 2 ), occurs at a positive (resp. negative) polarity in ϕ. (4) If M ∩ {alloc(x ), ¬alloc(x ) | x ∈ Var} ∅ for some minterm M ∈ µ fin (ϕ), then a formula ψ 1 -- * ψ 2 , such that x ∈ Var(ψ 1 ) ∪Var(ψ 2 ), occurs in ϕ at some polarity p ∈ {-1, 1}. Moreover, alloc(x ) occurs at a polarity -p, only if alloc(x ) is in the scope of a λ fin subformula8 of a formula elim fin ⊸ (M 1 , M 2 ) used to compute M ∈µ fin (ϕ ) M.

• ϕ = ϕ 1 ⊸ ϕ 2 = ¬(ϕ 1 - - * ¬ϕ 2 ): there exist minterms M i ∈ µ inf (ϕ i ), N i ∈ (M i ) E(M 1 ∪M 2 ) , for i = 1, 2, P 1 ∈ (N 1 ) A(M 1 ∪M 2 ) and Q 1 ∈ (P 1 ) M a 2 ∪M p 2 , such that M ∈ elim inf ⊸ (Q 1 , N 2 ) dnf mt
. By inspection of elim inf ⊸ (Q 1 , N 2 ), the only possible case is ℓ = ¬alloc(x ) with x ∈ av(M 1 ) (Equation ( 13) in Lemma 5.20), thus x ∈ Var(ϕ 1 ) ∪ Var(ϕ 2 ) and (ϕ 1 -- * ¬ϕ 2 ) occurs at polarity -1 in ϕ, which completes the proof. (4) The proof is similar to point (3). The only difference is that alloc(x ) may occur in the λ fin subformula (Equation [START_REF] Katelaan | Effective Entailment Checking for Separation Logic with Inductive Definitions[END_REF] in Lemma 5.20) of the elim fin ⊸ (Q 1 , N 2 ), in which case its polarity may be different from that of ϕ 1 -- * ϕ 2 . □ Note that Property 3 in Lemma 5.29 does not hold for µ fin (ϕ):

Example 5.30. Consider a fixed number n ≥ 1, as well as the following formulae:

ϕ def = |h| ≃ U -n ψ 1 def = (¬alloc(x ) ∧ |h| ≃ n) - - * ⊥ ψ 2 def = alloc(x )
We verify that ψ 2 ∧ ϕ ≡ fin ¬ψ 1 ∧ ϕ:

• If (U, s, I, h) |= ψ 2 ∧ ϕ, then s(x )
is allocated in h and there are exactly n unallocated cells. Then the heap h ′ whose domain is the set of unallocated cells in h is disjoint from h and satisfies ¬alloc(x ) ∧ |h| ≃ n, which proves that (U, s, I, h) |= ¬ψ 1 . • If (U, s, I, h) |= ¬ψ 1 ∧ ϕ, then there are exactly n unallocated cells in U, and there exists a heap h ′ disjoint from h with n elements in its domain, non of which is s(x ). Thus, s(x ) must occur in the domain of h, and (U, s, I, h) |= ψ 2 .

However, the polarity of alloc(x ) is positive in ψ 2 , whereas x only occurs in the scope of neutral occurrences of -- * in ¬ψ 1 . ■

We provide another example illustrating Property 4.

Example 5.31.

Let M 1 = {|h| ≥ 0, |h| < 2, ¬alloc(x )} and M 2 = {|h| ≥ 0, |h| < ∞, ¬x → x }. We have M 1 ⊸ M 2 ≡ fin ¬x ≈ y ∧ |h| ≥ 0 ∧ |h| < |U | ∧ ¬alloc(x ) → (|U | ≥ 2 ∧ |h| < |U | -1)
. The last two formulae are parts of λ fin in Lemma 5.20: |h| < |U | ensures that there exists at least one free location (so that there exists a disjoint heap satisfying M 1 ), and if x is not allocated, then there must actually exist 2 free locations, since x cannot be allocated in the extension. Observe that alloc(x ) occurs positively in the latter formula (since it is in scope of 2 negations), whereas x only occurs in the scope of negative (or neutral) occurrences of -- * in M 1 * M 2 (i.e., positive occurrences of ⊸). This happens because alloc(x ) occurs in λ fin . ■

Testing Membership in µ † (ϕ) in PSPACE

Given a quantifier-free SL k formula ϕ, the number of minterms occurring in µ fin (ϕ) (resp. µ inf (ϕ)) is exponential in the size of ϕ, in the worst case. Therefore, an optimal decision procedure cannot generate and store these sets explicitly, but rather must enumerate minterms lazily. We show that (i) the size of the minterms in µ fin (ϕ) ∪ µ inf (ϕ) is bounded by a polynomial in the size of ϕ, and that (ii) the problem "given a minterm M, does M occur in µ fin (ϕ) (resp. in µ inf (ϕ))?" is in PSPACE. To this aim, we define a measure on a quantifier-free formula ϕ, which bounds

The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates • 31 the size of the minterms in the sets µ fin (ϕ) and µ inf (ϕ), inductively on the structure of the formulae:

M (⊤) def = 0 M (⊥) def = 0 M (x ≈ y) def = 0 M (q(x)) def = 0 M (emp) def = 1 M (x → y) def = 2 M (¬ϕ 1 ) def = M (ϕ 1 ) M (ϕ 1 ∧ ϕ 2 ) def = max(M (ϕ 1 ), M (ϕ 2 )) M (ϕ 1 * ϕ 2 ) def = 2 i=1 (M (ϕ i ) + ||Var(ϕ i )||) M (ϕ 1 - - * ϕ 2 ) def = 2 i=1 (M (ϕ i ) + ||Var(ϕ i )||)
The intuition is that M (ϕ) is an upper bound on natural number occurring in the test formulae in µ fin (ϕ) ∪ µ inf (ϕ), when viewed as linear inequalities on |U | and |h|. For instance, M (emp) is 1, because emp ≡ |h| < 1, whereas

M (x → y) is 2, because M (x → y) ≡ x → y ∧ |h| ≥ 1 ∧ |h| < 2.
The extension to the standard connectives is straightforward, but the handling of the separating connectives is more involved: first, the combination of two inequalities may increase the bound (for instance, |h| ≥ 1 * |h| ≥ 2 ≡ |h| ≥ 3) and second, the elimination of these connectives yields additional inequalities (see Lemma 5.16 and Lemma 5.20).

Proposition 5.32. For any n ∈ N, we have: Proof. This is an immediate corollary of Proposition 5.26. □

M (|h| ≥ n) = M (|U | ≥ n) = n M (|h| ≥ |U | -n) = n + 1 Proof. By induction on n ≥ 0. □ Note that, because |h| < ∞ is a shorthand for ⊤, we have M (|h| < ∞) = 0. Definition 5.33. A minterm M is M-bounded by a formula ϕ, if for each literal ℓ ∈ M, the following hold: (i) M (ℓ) ≤ M (ϕ) if ℓ ∈ |h| ≥ min M i , |h| < max M i ; (ii) M (ℓ) ≤ 2M (ϕ) + 1, if ℓ ∈ {|U | ≥ n, |U | < n | n ∈ N}.
The following lemma provides the required result: Lemma 5.35. Given a quantifier-free SL k formula ϕ, each minterm M ∈ µ fin (ϕ) ∪ µ inf (ϕ) is M-bounded by ϕ.

Proof. We prove that each M ∈ µ fin (ϕ) is M-bounded by ϕ. The proof for M ∈ µ inf (ϕ) follows from the observation that, because of the definition of elim inf ⊸ , for each M ∈ µ inf (ϕ) there exists M ′ ∈ µ fin (ϕ) such that M (M ) ≤ M (M ′ ). By induction on the structure of ϕ:

• If ϕ = emp then µ fin (ϕ) = {|h| ≥ 0 ∧ |h| < 1}, M (|h| ≥ 0) = 0, M (|h| < 1) = M (|h| ≥ 1) = 1 and M (emp) = 1, by definition. • If ϕ = x → y then µ fin (ϕ) = x → y ∧ |h| ≥ 1 ∧ |h| < 2 , M (|h| ≥ 1) = 1, M (|h| < 2) = 2 and M (x → y) = 2, by definition. • If ϕ = q(y) with q ∈ F then µ fin (ϕ) = q(y) ∧ |h| ≥ 0 ∧ |h| < ∞ , M (|h| ≥ 0) = 0, M (|h| < ∞) = 0 and M (q(y)) = 0, by definition. • If ϕ = x ≈ y then µ fin (ϕ) = x ≈ y ∧ |h| ≥ 0 ∧ |h| < ∞ and M (|h| ≥ 0) = M (|h| < ∞) = 0, by definition. • If ϕ = ϕ 1 ∧ ϕ 2 , let ℓ ∈ M be a literal, where M ∈ µ fin (ϕ 1 ∧ ϕ 2 ) is a minterm. Then M ∈ [M 1 , M 2 ],
for some minterms M i ∈ µ fin (ϕ i ), i = 1, 2 and the proof follows from Proposition 5.34, because M i is M-bounded by ϕ i and M (ϕ i ) ≤ M (ϕ), so that M i is M-bounded by ϕ, for i = 1, 2.

The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates • 37 where9 α fin def = |h| ≥ |U | -0, α inf def = ∀x∀y∀z . x → (y, z) → alloc(y) ∧ alloc(z) and ϕ sl is obtained from ϕ flat by replacing each occurrence of c by x c , each term f (c) (resp. д(c)) by y c (resp. z c ) and each term f (x i ) (resp. д(x i )) by y i (resp. z i ). Next, we show that the following statements are equivalent:

(1) φ flat has a finite model (U, s, I),

′ , h) |= α fin ∧ x c → (y c , z c ), because dom(h) = U and h(c I ) = ( f I (c I ), д I (c I )). Consider a store s ′′ def = s ′ [x i ← ℓ i , y i ← ℓ ′ i , z i ← ℓ ′′ i | i = 1, . . . , n], for an arbitrary set {ℓ i , ℓ ′ i , ℓ ′′ i | i ∈ [1, n]} ⊆ U and assume that (U, s ′′ , h) |= n i=1 x i → (y i , z i ). Then by definition of h, for all i ∈ [1, n], we have ℓ ′ i = f I (ℓ i ) and ℓ ′′ i = д I (ℓ i ); hence, (U, s ′′ , h) |= ϕ sl . Since ℓ i , ℓ ′ i and ℓ ′′ i are arbitrary, for i ∈ [1, n], this proves that (U, s ′ , h) is a finite model of φ fin sl . "(2) ⇒ (3)" We define U ∞ def = U ⊎ L, where L is an infinite set of locations not in U. Clearly (U ∞ , s ′ , h) |= α inf , because x → (y, z) is false for any extension of s ′ with a pair of the form [x ← ℓ], [y ← ℓ] or [z ← ℓ], where ℓ ∈ L. Furthermore, the valuation of x c → (y c , z c ) is unchanged between (U, s ′ , h) and (U ∞ , s ′ , h). Consider a store s ′′ def = s ′ [x i ← ℓ i , y i ← ℓ ′ i , z i ← ℓ ′′ i | i = 1, . . . , n], for an arbitrary set {ℓ i , ℓ ′ i , ℓ ′′ i | i ∈ [1, n]} ⊆ U and assume that (U, s ′′ , h) |= n i=1 x i → (y i , z i ). Then necessarily, ℓ i , ℓ ′ i , ℓ ′′ i | i ∈ [1, n] ∩ L = ∅. Next, we show that (U, s ′′ , h) |= ϕ sl ⇔ (U ∞ , s ′′ , h) |= ϕ sl , by induction on the structure of ϕ sl . Since (U, s ′′ , h) |= ϕ sl by the hypothesis, we have (U ∞ , s ′′ , h) |= ϕ sl , thus (U ∞ , s, h) |= φ inf sl . "(3) ⇒ (1)" Let U def = dom(h) ∪ {ℓ 1 , ℓ 2 | ∃ℓ ∈ U ∞ . h(ℓ) = (ℓ 1 , ℓ 2 )}.
Since h is finite, so is U. Let s be an arbitrary10 store on U and define I such that:

• c I = s ′ (x c ), and,

• for each ℓ ∈ U, such that h(ℓ) = (ℓ ′ , ℓ ′′ ), we have f I (ℓ) = ℓ ′ and д I (ℓ) = ℓ ′′ . Note that c I ∈ U, because by hypothesis (U ∞ , s ′ , h) |= x c → (y c , z c ), hence s ′ (x c ) ∈ dom(h). Similarly, f I (ℓ), д I (ℓ) ∈ U, for each ℓ ∈ U, by the definition of U. Moreover, since (U ∞ , s ′ , h) |= α inf we obtain that f I and д I are well-defined total functions. For each set {ℓ

i | i = 1, . . . , n} ⊆ U, the function s ′′ = s[x i ← ℓ i , y i ← f I (ℓ i ), z i ← д I (ℓ i ) | i = 1, . . . , n] is a store on U ∞ such that (U ∞ , s ′′ , h) |= x i → (y i , z i ) for every i ∈ [1, n], hence (U ∞ , s ′′ , h) |= ϕ sl . By induction on the structure of ϕ flat , one shows that (U ∞ , s ′′ , h) |= ϕ sl ⇔ (U, s ′′ , I) |= ϕ flat . Since (U ∞ , s ′′ , h) |= ϕ sl , we have (U, s, I) |= ϕ flat . □
Note that, by the previous proof, the undecidability result still holds for finite satisfiability if a single occurrence of -- * is allowed, in a ground formula (indeed, we may take α fin = (|h| ≥ |U | -0) = (¬emp -- * ⊥)). For infinite satisfiability one occurrence of -- * is still sufficient, however there must be a universally quantified variable within the scope of -- * . The reductions [START_REF] Ramsey | On a Problem of Formal Logic[END_REF] use positive occurrences of test formulae |h| ≥ |U | -n and alloc(x ), where x is universally quantified. We obtain decidable subsets of BSR(SL k ) by devising conditions that are sufficient to discard positive occurrences of such formulae from µ † (ϕ), where † ∈ fin, inf and ∀y 1 . . . ∀y m . ϕ is a BSR(SL k ) formula. Note that µ inf (ϕ) contains no formulae of the form |h| ≥ |U | -n (as such test formulae are trivially false in all infinite structures) which explains why slightly less restrictive conditions are needed for infinite structures. As we shall see (Proposition 6.5), these conditions are sufficient to ensure that the formula ∀y 1 , . . . , ∀y m . M ∈µ inf (ϕ ) M is BSR-compatible (but not that ∀y 1 , . . . , ∀y m . M ∈µ fin (ϕ ) M is BSR-compatible, see Section 6.2.3 for details). definition, U ′k +1 ∩p I = A k +1 ∩p I . Conversely, let S = (U, s, I) be an infinite model of φ ∧ φ p . Then by definition of φ p for every (ℓ 1 , . . . , ℓ k +1 ) such that (ℓ 1 , . . . , ℓ k +1 ) ∈ p I , and for every i ∈ [1, k + 1], either ℓ i = c I for some c ∈ F (φ), or ℓ i = s(x ) for some x ∈ Var(φ). Since F (φ) and Var(φ) are both finite, p I is also finite. □ Putting all results together, we obtain the first decidability result of this paper: Theorem 6.11. The infinite satisfiability problem for BSR inf (SL k ) is PSPACE-complete.

Proof. PSPACE-hardness is an immediate consequence of the fact that the quantifier-free fragment of SL k , without the separating implication, but with the separating conjunction and negation, is PSPACE-hard [7, Proposition 5].

To The algorithm is then defined as follows. We guess an FO-structure (U, s, I) such that ||U|| = O(k • size(φ) 2 ) and (U, s, I) |= Heap (where Heap is the formula in Definition 4.6). Note that since k may depend on the input, U k is of exponential size, hence in principle the interpretation of p may be exponential. However, since we assume that (U, s, I) |= Heap, for every element x ∈ U, there is at most one vector y ∈ U k such that (x, y) ∈ p I , hence ||p I || ≤ ||U||. To ensure that Heap holds, it suffices to guess a subset of U (the set of allocated locations), and choose for every element x in this subset one vector y ∈ U k such that (x, y) ∈ p I . Moreover, the arity of each predicate symbol in φ that are different from p is bounded by a constant, thus their interpretation is polynomial w.r.t. U. Then we check that (U, s, I) is m-repetitive and that (U, s, I) |= τ (φ ′ ) ∧ A (φ ′ ) ∧ ψ p . This test is feasible in PSPACE:

• the problem of testing whether (U, s, I) is m-repetitive is in PSPACE by Proposition 6.8.

• the problem (U, s, I) |= τ (φ ′ ) is in PSPACE by Lemma 6.3,

• the problems (U, s, I) |= A (φ ′ ) and (U, s, I) |= ψ p are both in PSPACE, by Proposition 6.2. □ Remark 6.12. The algorithm given in the proof of Theorem 6.11 is based on guessing some structure of size s, with s = O(k • size(φ) 2 ). To apply the algorithm one needs of course to know an upper bound of s. Because our aim in the present paper is only to prove the existence of such an algorithm, we do not bother to give this bound explicitly, as this would only hinder readability, and we only state that it exists. However, the bound can easily be extracted from the above proofs, if needed. Similarly, an explicit bound on the size of the minterms in µ inf (ϕ) could be extracted from the proof of Lemma 5.42. ■ 6.2.3 Finite Satisfiability (BSR fin (SL k )). We now prove that finite satisfiability is PSPACE-complete for the class BSR fin (SL k ), defined as the set of formulae with no positive occurrence of separating implications. Even with this stronger restriction, the previous proof based on a translation to first-order logic cannot be carried over without any additional argument, because Proposition 6.5 does not hold for BSR fin (SL k ). The problem is that, in the case of a finite universe, alloc(x ) test formulae may occur at a positive polarity, even if every ϕ 1 -- * ϕ 2 subformula occurs at a negative polarity, due to the positive occurrences of alloc(x ) within the subformula λ fin in The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates • 41 the definition of elim fin ⊸ (M 1 , M 2 ) (Equation ( 15) in Lemma 5.20), see also Example 5.30. As previously discussed, positive occurrences of alloc(x ) hinder the translation into BSR(FO), because of the existential quantifiers that may occur in the scope of a universal quantifier.

The solution is to distinguish a class of finite structures (U, s, I, h). Given α ∈ N, we consider the so-called αcontrolled structures, for which there exists a set of locations ℓ 1 , . . . , ℓ α , such that every location ℓ ∈ U \{ℓ 1 , . . . , ℓ α } points to a tuple from the set {ℓ 1 , . . . , ℓ α , ℓ}. An example of a 3-controlled structure is given in Figure 2. Any α-controlled SL-structure is finite, since U = dom(h) ∪ {s(x 1 ), . . . , s(x α )}, but its cardinality is not bounded. Furthermore, if ||U|| ≤ α, then (U, s, I, h) is necessarily α-controlled. Overview of the Proof for Finite Satisfiability. For a formula φ = ∀y 1 . . . ∀y m . ϕ in BSR fin (SL k ), we distinguish the following cases:

(1) If φ has an α-controlled model S, the formula obtained by replacing each occurrence of an alloc(x ) with α i=1 (x ≈ x i → alloc(x i )) in ∀y 1 . . . ∀y m M ∈µ fin (ϕ ) M is satisfied by S (as stated by Proposition 6.15). (2) Otherwise, each finite model of φ is non-α-controlled and we can build a model S, with a sufficiently large universe, such that each test formula θ ∈ {|U | ≥ n, |h| < |U | -n | n ∈ N} becomes true in S. Assume alloc(x ) occurs positively in a λ fin subformula of some formula elim fin ⊸ (M 1 , M 2 ). The latter must have been generated by the elimination of a separating implication from ϕ, hence alloc(x ) occurs in a disjunction with a formula of the form |h| < |U | -n 1 ∧ |U | ≥ n 2 ; its truth value in S can thus be ignored and the entire subformula deleted. In both cases, we obtain an equisatisfiable universally quantified boolean combination of test formulae with no positive occurrence of alloc(y i ) formulae. We translate this into an equisatisfiable BSR(FO) formula, for which finite satisfiability is decidable and apply a similar argument to that for the infinite case, to obtain the PSPACE upper bound. The Case of Controlled Structures. We first consider the case where the considered models are α-controlled. Proof. The result is trivial if n = 0, since S is a restriction of itself and trivially contains at least 0 unallocated elements. Thus we assume that n > 0. Let S = (U, s, I) be a non α-controlled model of φ ∪ Heap . Let A = s(Var(φ)) ∪ {c I | c ∈ Const(φ)}. Note that by definition, ||A|| ≤ m. We construct a sequence of pairwise distinct elements x 1 , . . . , x n ∈ U and a sequence of sets of elements Y 0 ⊆ Y 1 ⊆ • • • ⊆ Y n ⊆ U \A such that ||Y i || ≤ i, x 1 , . . . , x i Y i and for every j ∈ [1, i], either x j is unallocated or points to a vector containing an element of Y i . The sequence is constructed inductively as follows. Let Y 0 def = ∅. Assume that x 1 , . . . , x i , Y 1 , . . . , Y i have been constructed, for some i ∈ [0, n-1]. Let X = {x 1 , . . . , x i }, E = {z 1 , . . . , z k | (x j , z 1 , . . . , z k ) ∈ p I , 1 ≤ j ≤ i}. Because S |= Heap, for every j ∈ [1, i] there is at most one vector (z 1 , . . . , z k ) such that (x j , z 1 , . . . , z k ) ∈ p I , hence

||E|| ≤ k • i ≤ k • n. Further, ||X || = i ≤ n and ||Y i || ≤ i ≤ n. Thus ||E ∪ A ∪ X ∪ Y i || ≤ ||E|| + ||A|| + ||X || + ||Y i || ≤ k •n+m+2•n ≤ α.
Thus, since φ is not α-controlled, by Proposition 6.17, there exists an element x i+1 E ∪A∪X ∪Y i such that either x i+1 is not allocated, or there exists a (unique) vector z i such that (x i+1 , z i ) ∈ p I and z has a component y i+1 with y i+1 E ∪ X ∪ Y i ∪ A ∪ {x i+1 }. In the former case, we take Y i+1 Proof. By Lemma 4.9 (1), there exists J such that (U, s, J ) |= τ (φ) ∧ A (φ), where h is associated with J . If (U, s, J ) is α-controlled, then there exists an extension s ′ of s such that (U, s ′ , J ) |= τ (C(α )). This entails that for all extensions s ′′ of s ′ to x, (U, s ′′ , J ) |= α i=1 x ≈ x i ∨ y∈vect k (x 1 , ...,x α ,x ) p(x, y). By definition, (U, s ′′ , J ) |= x ≈ x i iff (U, s ′′ , I, h) |= x ≈ x i . Furthermore, since h is associated with J , we have by definition (U, s ′′ , J ) |= p(x, y) iff (U, s ′′ , I, h) |= x → y. Therefore (U, s ′′ , I, h) |= α i=1 x ≈ x i ∨ y∈vect k (x 1 , ...,x α ,x ) x → y. As s ′′ is arbitrary, this entails that (U, s, I, h) is α-controlled, contradicting our hypothesis. □

We are now in the position to state the second decidability result of the paper, concerning the decidability of the finite satisfiability for BSR fin (SL k ): Theorem 6.20. The finite satisfiability problem for BSR fin (SL k ) is PSPACE-complete.

Proof. PSPACE-hardness is proved using the same argument as in the proof of Theorem 6.11, which does not rely on the infiniteness of the universe.

Let φ def = ∀y 1 , . . . , y m . ϕ be a formula in BSR fin (SL k ), where ϕ is quantifier-free and Var(φ) = {x 1 , . . . , x n }. ). In this case, φ has a finite model, and otherwise φ has a finite model iff it has a non-α-controlled finite model. We now assume that φ does not have any α-controlled model.

Let φ ′ def = ∀y 1 , . . . , y m . χ ′ , where χ ′ is obtained from χ by replacing all positive occurrences of a formula alloc(x ), where x ∈ {x 1 , . . . , x n , y 1 , . . . , y m }, by ⊥. We prove that φ ′ has a finite model iff φ has a finite model.

The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates • 45 quantifier-free formula ϕ is sat-equivalent to a formula ϕ ⊸ ⊤ that is both in BSR fin (SL k ) and BSR inf (SL k ), since the left-hand side of -- * has neutral polarity. Future work includes the implementation of an effective procedure for testing satisfiability of BSR(SL) formulae in the above fragments. Since a non deterministic algorithm based on a guess-and-check approach is not practical, such a procedure could rely either on an encoding in QBF based on the finite model property derived in the present paper, or on some compact computational representations of boolean combinations of test formulae. The bottleneck of the approach is certainly the computation of equivalent boolean combinations of test formulae. To make the transformation more efficient, refined versions of Lemmas 5.16 and 5.20 could be derived, getting rid of some hypotheses such as E-completeness or A-completeness (as enforcing these hypotheses yield an exponential blow-up). Instead, the needed test formulae could be added on demand, only if needed.

An extension of the presented results to formulae containing inductively defined predicates (such as singlylinked lists) or interpreted predicates or functions (such as arithmetic symbols) will also be considered. This would allow us to extend existing approaches to test satisfiability of such formulae [5? ] to formulae containing negation.

Definition 2 . 1 .

 21 Consider the structures S def = (U, s, I) and

  hence there is no heap disjoint from h with a domain of cardinality at least n + 1, so that S |= |h| ≥ |U | -n. □ Not all atoms of SL k are test formulae, for instance x → y and emp are not test formulae. However, by Proposition 4.2, we have the equivalences x → y ≡ x → y ∧ ¬|h| ≥ 2 and emp ≡ ¬|h| ≥ 1. Note that, for any n ∈ N, the test formulae |U | ≥ n and |h| ≥ |U | -n are trivially true and false respectively, if the universe is infinite.

Definition 4 . 5 .

 45 Given a structure (U, s, I) such that (U, s, I) |= Heap and a heap h on U

Definition 4 . 6 .

 46 For a quantified boolean combination of test formulae ϕ, we let N (ϕ) be the maximum integer n occurring in a test formula θ of the form |h| ≥ n, |U | ≥ n, or |h| ≥ |U | -n from ϕ and define A (ϕ)

Example 4 . 7 .

 47 ∈Var(ϕ ) Dom x as the conjunction of axioms related to ϕ. Let ϕ be the SL 1 formula: x → y ∧ |h| ≥ 2 ∧ |h| < |U |. Then τ (ϕ) = p(x, y) ∧ a 2 ∧ c 1 , and A (ϕ) contains, among others, the following formulae 6 :

  n and (U, s, I) |= a n ⇒ a I n = ⊤. Since n ≤ N (ψ ) and (U, s, I) |= N (ψ ) i=0 A j , we have a I j = ⊤ and u I j ∈ dom(h), for all j ∈ [1, n]. Because u I j are pairwise distinct, for j ∈ [1, n], we obtain that ||h|| ≥ n, and (U, s, I, h) |= ψ follows, by Proposition 4.2. • ψ = |h| < n: τ (ψ ) = ¬a n and (U, s, I) |= ¬a n ⇒ a I n = ⊥. Since n ≤ N (ψ ) and (U, s, I) |= N (ψ ) i=0 A j , each location ℓ ∈ dom(h) must be one of u I 1 , . . . , u I n-1 , thus ||dom(h)|| ≤ n -1 and (U, s, I, h) |= |h| < n follows, by Proposition 4.2. • ψ = |U | ≥ n: τ (ψ ) = b n and (U, s, I) |= b n ⇒ b I n = ⊤. Since n ≤ N (ψ ) and (U, s, I) |= N (ψ ) i=0 B j , we have b I j = ⊤, for all j ∈ [1, n]. Because v I j are pairwise distinct, for all j ∈ [1, n], we obtain that ||U|| ≥ n, and (U, s, I, h) |= ψ follows, by Proposition 4.2. • ψ = |U | < n: τ (ψ ) = ¬b n and (U, s, I) |= ¬b n ⇒ b I n = ⊥. Since n ≤ N (ψ ) and (U, s, I) |= N (ψ ) i=0 B j , we have that each location ℓ ∈ U must be one of v I 1 , . . . , v I n-1 , thus ||U|| ≤ n -1 and (U, s, I, h) |= ψ follows, by Proposition 4.2. • ψ = |h| ≥ |U | -n: this case is impossible because |h| ≥ |U | -n must occur at a negative polarity in ψ . • ψ = |h| < |U | -n: τ (ψ ) = c n+1 and (U, s, I) |= c n+1 ⇒ c n+1 = ⊤. Since n ≤ N (ψ ) and (U, s, I) |= N (ψ )+1 i=0 C j , we obtain that w I j ∈ U \ dom(h), for all j ∈ [1, n + 1]. Since w I j are pairwise disjoint, we obtain ||U || -||h|| ≥ n + 1 thus (U, s, h) |= ψ follows, by Proposition 4.2. • ψ = alloc(x ). Since ψ occurs at positive polarity and ϕ is BSR-compatible, necessarily x ∈ Var(ϕ). Since (U, s, I) |= d(x ) and (U, s, I) |= Dom x , we must have (U, s, I) |= p(x, ξ 1 x , . . . , ξ k x ), and therefore s(x ) ∈ dom(h). Thus (U, s, I, h) |= ψ . • ψ = ¬alloc(x ). Since (U, s, I) |= d(x ) and (U, s, I) |= Dom, we have (U, s, I) |= ∀y 1 , . . . , y k . ¬p(x, y 1 , . . . , y k ), thus s(x ) dom(h). Hence (U, s, I, h) |= ψ . • ψ ∈ x ≈ y, ¬x ≈ y, q(x), ¬q(x), x → y, ¬x → y : The equivalence statement (U, s, I, h) |= ψ ⇔ (U, s, J ) |= ψ is proven in the same way as for point (1). • The cases ψ = ψ 1 ∧ ψ 2 , ψ = ψ 1 ∨ ψ 2 , ∃x . ψ 1 are by inductive hypothesis. □ The following proposition states essential syntactic properties of τ (φ) ∧ A (φ). Proposition 4.10. Let φ = ∀y . ϕ, where ϕ is a boolean combination of test formulae, with Var(φ) = {x 1 , . . . , x n }. The formula τ (φ) ∧ A(φ) is a BSR(FO) formula with no existential quantifier such that ||Const(τ (φ) ∧ A (φ))|| = k • n + (k + 6) • N (φ) + 5 (where k denotes the number of record fields) and Var(τ (φ) ∧ A (φ)) = Var(φ).

  For a literal ℓ, we denote by ℓ its complement, i.e., θ def = ¬θ and ¬θ def = θ , where θ is a test formula. If T is a set of literals, then we denote by atoms(T ) the set of all test formulae ϕ such that either ϕ or ¬ϕ occurs in T . The equivalence relation x ≈ T y is defined as T |= x ≈ y and we write x ̸ ≈ T y for T |= ¬x ≈ y. Observe that x ̸ ≈ T y is not the complement of x ≈ T y. For a set X of variables, |X | T is the number of equivalence classes of ≈ T in X . Two tuples y, y ′ ∈ Var k are T -distinct if y i ̸ ≈ T y ′ i , for some i ∈ [1, k]. Proposition 5.5. If M is E-complete for Var(M ), (U, s, I, h) |= M and X ⊆ Var(M ), then |X | M = ||s(X )||.

  N} , where δ x (M ) is the number of pairwise M-distinct tuples y for which there exists ¬x ′ → y ∈ M such that x ≈ M x ′ . For any SL-structure S = (U, s, I, h), we denote by min S M , max S M ∈ N ∞ the values obtained by replacing |U | with ||U|| in min M and max M , respectively. Example 5.13. Let M = {|h| ≥ 0, |h| < ∞, alloc(y 0 )} ∪ {¬y i ≈ y j | i, j ∈ [0, n], i j} ∪ {y 0 → y i | i ∈ [1, n]}. Then y 0 ∈ av(M ), δ x (M ) = n and dc(M ) = M ∪ {|U | ≥ n + 1}. This states that all models of M contain at least n + 1 locations: y 1 , . . . , y n and the image of y 0 by the heap. Let M ′ = {|h| ≥ 1, |h| < |U | -1}. Then dc(M ′ ) = M ′ ∪ {|U | ≥ 3}. All models of M ′ contain at least 3 locations (one allocated and two non allocated). ■ Proposition 5.14. Given a minterm M, min S M < max S M for every model S of dc(M ) u .

Proposition 5 . 15 .

 515 be the case, or else dc(M ) ≡ ⊥, in contradiction with S |= dc(M ) u . □ For any minterm M, we have M ≡ pc(M ) ≡ dc(M ). Proof. It is clear that pc(M ) |= M and dc(M ) |= M. Let S = (U, s, I, h) be a model of M. If S ̸ |= pc(M ) then necessarily pc(M ) = ⊥ and there exist variables x, x ′ ∈ Var(M ) such that x → (y 1 , . . . , y k ), x ′ → (z 1 , . . . , z k ) ∈ M, x ≈ M x ′ and (y 1 , . . . , y k ) and (z 1 , . . . , z k ) are M-distinct, i.e., there exists i ∈ [1, k] such that M |= ¬y i ≈ z i .

1 )

 1 and since dom(h 1 ) ∩ A 2 = ∅, we have s(x ) dom(h 1 ), thus (U, s, I, h 1 ) |= ¬x → y.otherwise, x av(M 2 ), and since atoms(Mp = atoms(M p 2 ), we have x → y, ¬x → y ∩ M 2 ∅. Since x av(M 2 ), the only possibility is ¬x → y ∈ M 2 , thus ¬x → y ∈ npto(M 1 , M 2 ) and (U, s, I, h) |= ¬x → y, by (4). Since h is an extension of h 1 , we obtain that (U, s, I, h 1 ) |= ¬x → y as well.□We provide simple examples of application.Example 5.18. Consider the following minterms:

1 . 2 x-

 12 Proposition 5.3, and by Proposition 5.15, we deduce that (U, s, I, h) |= pc(M 1 ) e ∧ dc(M 1 ) u ∧ M f Analogously, (U, s, I, h) |= M e 2 ∧ dc(M 2 ) u ∧ M f follows from (U, s, I, h ⊎ h ′ ) |= M 2 by Propositions 5.3 and 5.15. (13) Since (U, s, I, h ′ ) |= M 1 , also (U, s, I, h ′ ) |= alloc(av(M 1 )) and since dom(h ′ ) ∩ dom(h) = ∅, we have (U, s, I, h) |= nalloc(av(M 1 )). To prove that (U, s, I, h) |= fp nv(M 1 ) (M 2 ), we consider four cases, depending on the form of the literal: ACM Trans. Comput. Logic, Vol. 1, No. 1, Article . Publication date: December 2019. The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates • 23 If alloc(x ) ∈ M 2 and x ∈ nv(M 1 ), then s(x ) ∈ dom(h) ∪ dom(h ′ ) and s(x ) dom(h ′ ), thus s(x ) ∈ dom(h) and (U, s, I, h) |= alloc(x ), by Proposition 4.2. -The cases x → y ∈ M 2 and x ∈ nv(M 1 ) use a similar argument. -If ¬alloc(x ) ∈ M 2 and x ∈ nv(M 1 ), then s(x ) dom(h ∪ h ′ ), hence s(x ) dom(h) and (U, s, I, h) |= ¬alloc(x ), by Proposition 4.2. -If ¬x → y ∈ M 2 and x ∈ nv(M 1 ) then s(x ) dom(h ′ ) and either: * s(x ) dom(h) and (U, s, I, h) |= ¬x → y, by Proposition 4.2, or * s(x ) ∈ dom(h) in which case h ′ ⊎ h and h agree on s(x ) and (U, s, I, h) |= ¬x → y. (14) We have ||h ⊎ h ′ || = ||h||+||h ′ || and since (U, s, I, h⊎h ′ ) |= M 2 , we obtain min S

M 1 =

 1 m 1 and min M 2 = |U | -m 2 , the other cases are similar. Consider a structure S = (U, s, I, h) such that S |= |h| ≥ m 1 ∧ |h| ≥ |U | -m 2 . Then ||h|| ≥ m 1 and ||h|| ≥ ||U|| -m 2 , and we distinguish two cases.

  < ∞ ACM Trans. Comput. Logic, Vol. 1, No. 1, Article . Publication date: December 2019.

Proposition 5 .

 5 34. Given minterms M 1 , . . . , M n all M-bounded by ϕ, each minterm M ∈ [M 1 , . . . , M n ] is also M-bounded by ϕ.

fin

  sl has a finite model (U, s ′ , I, h), and (3) φ inf sl has an infinite model (U ∞ , s ′ , I, h). "(1) ⇒ (2)" We define the store s ′ def = s[x c ← c I , y c ← f I (c I ), z c ← д I (c I )] and the heap h such that dom(h) = U and h(ℓ) def = ( f I (ℓ), д I (ℓ)), for all ℓ ∈ U. By construction, we have (U, s

x 1 x 2 x 3 Fig. 2 .

 32 Fig. 2. A finite 3-controlled SL 2 structure. Definition 6.13. An SL-structure S is α-controlled if S |= ∃x 1 , . . . , x α . C(α ), with

Proposition 6 . 14 .Lemma 6 . 18 .

 614618 Let S = (U, s, I) be an FO-structure. The problem of testing whether S |= τ (C(α )) is in P.Proof. Note that the size of C(α ) is exponential w.r.t. k. However, to test that S |= τ (C(α )), it suffices to check that for every u ∈ U \ s({x 1 , . . . ,x α }), there exist v 1 , . . . , v k such that (u, v 1 , . . . , v k ) ∈ p I and v 1 , . . . , v k ⊆ {u} ∪ s({x 1 , . . . , x α }),which can be done in time polynomial in size(S). □ The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates • 43 Let n ∈ N. Consider a BSR(FO) formula φ, let m def = ||Var(φ)||+||Const(ϕ)|| and let α ≥ (k +2) •n+m. If φ ∪ Heap has a non-α-controlled model S then there is a restriction of S that also validates φ ∪ Heap and has at least n unallocated elements.

Proposition 6 . 19 .

 619 def= Y i and in the latter case,Y i+1 def = Y i ∪ {y i+1 }. Note that in both cases Y i+1 ⊇ Y i and ||Y i+1 || ≤ ||Y i || + 1 ≤ i + 1. Further, since x i+1 Y i and y i+1 X ∪ {x i+1 }, necessarily x 1 , . . . , x i+1 Y i+1, thus the sequences fulfill the required properties.Then, we consider the restrictionS ′ of S to U ′ def = U \ Y n . As x 1 , . . . , x n Y n , U \ Y n is not empty and contains x 1 , . . . , x n . By Proposition 2.2, since Y n ∩ A = ∅, S ′ |= φ ∪ Heap . If x i is allocated in S ′, then there exists z ∈ U ′k such that (x i , z) ∈ p I . But by the construction above, z contains an element in Y i ⊆ Y n , which contradicts the fact that z ∈ U ′k . Thus necessarily x i is unallocated in S ′ . Since the elements x 1 , . . . , x n are pairwise distinct, the proof is completed.□ Let φ be an SL formula. If φ has a non-α-controlled SL-model (U, s, I, h) then τ (φ) ∧ A(φ) has a non-α-controlled FO-model where the interpretation of p is finite.

Let χ def =

 def M ∈µ fin (ϕ ) M and α def = (k + 2) • (N (χ ) + 1) + (k + 1) • n + (k + 6) • N (χ ) + 5.We first test whether φ admits an α-controlled model, which can be done in PSPACE, by Lemma 6.16 since, by Proposition 5.36,N (χ ) = O(size(ϕ) 2 ), thus α = O(k • size(φ) 2

  3 (see Theorems 6.1, 6.11 and 6.20).We define a small set of SL k patterns of formulae, possibly parameterized by a positive integer, called test formulae. These patterns capture properties related to allocation, points-to relations in the heap and cardinality constraints.

	Remark 3.4. Because the polarity of the antecedent of a separating implication is neutral, Definition 3.2 imposes
	no constraint on the occurrences of separating implications at the left of an occurrence of -- * .	■
	4 TEST FORMULAE FOR SL k
	4.1 Definition and Basic Properties
	Definition 4.1. The following patterns are called test formulae:

  Then since h has a finite domain, it is clear that ||h|| ≥ n if n = 0 and that no such structure exists if n = ∞. When n ≥ 1, we prove the result by induction on n. By definition, S |= |h| ≥ n -1 * ¬emp, hence there exist disjoint heaps h 1 , h 2 such that (U, s, I, h 1 ) |= |h| ≥ n -1, (U, s, I, h 2 ) |= ¬emp and h = h 1 ⊎ h 2 . By the induction hypothesis ||h 1 || ≥ n -1 and by definition, ||h 2 || ≥ 1, so that ||h 1 ⊎ h 2 || ≥ n. Conversely, assume that ||h|| ≥ n. Since h is finite, this entails that n ∞. If n = 0 then S |= |h| ≥ n always holds. Otherwise, we prove the result by induction on n. Consider ℓ ∈ dom(h) and let h 1 and h 2 respectively denote the restrictions of h to U \ {ℓ} and to {ℓ}, so that h = h 1 ⊎ h 2 . Since ||h 1 || ≥ n -1, by the induction hypothesis (U, s, I, h 1 ) |= |h| ≥ n -1, and since dom(h 2 ) ∅, (U, s, I, h 2 ) |= ¬emp. Thus S |= |h| ≥ n.

• S |= |U | ≥ n ⇔ ||U|| ≥ n. Assume that S |= |U | ≥ n. Then there exists a heap h 1 disjoint from h such that (U, s, I, h ⊎ h 1 ) |= |h| ≥ n. This entails that ||h ⊎ h 1 || ≥ n and since dom(h ⊎ h 1 ) ⊆ U, necessarily, ||U|| ≥ n. Conversely, if ||U|| ≥ n, then there exists a set L ⊆ U such that dom(h) ∩ L = ∅ and ||L|| = n -||h||. Let h ′ be any heap of domain L. Then h and h ′ are disjoint and (U, s,

  and by Proposition 5.11. Second,L i ∩ A 3-i = ∅ because M i is E-complete for Var(M 1 ∪ M 2 ) and nv(M 3-i ) ∩ av(M 3-i ) = ∅,by Proposition 5.11. • S |= alloc(Y 1 ) ∧ alloc(Y 2 ). this follows immediately from the fact that L 1 ∪ L 2 ⊆ dom(h) by definition of L 1 , L 2 . Since M 1 and M 2 are E-complete for Var(M 1 ∪ M 2 ), there must exist a literal x ≈ y ∈ M e 1 such that ¬x ≈ y ∈ M e 2 , or vice versa. In both cases however M 1 * M 2 ≡ elim * (M 1 , M 2 ) ≡ ⊥. Thus we consider from now on that M e 1 = M e 2 . • M 1 * M 2 |= elim * (M 1 , M 2 ). Let S = (U, s, I, h) be a model of M 1 * M 2 . Then there exist disjoint heaps h 1

		□
	We are now in the position to prove Lemma 5.16:
	Proof. Suppose first that M e 1	M e 2 .

and h 2 such that h = h 1 ⊎ h 2 and (U, s, I, h i ) |= M i , for all i = 1, 2. Below we show that S is a model of the formulae (2), (

  we have ||h|| = ||h 1 || + ||h 2 ||, thus the first two constraints are obtained by summing up the constraints min S M i ≤ ||h i || < max S M i , for i = 1, 2. (6) We prove S |= η 12 , the proof for S |= η 21 being symmetrical. Consider a set Y ⊆ nv(M 2 ) \ av(M 1 ) and suppose that (U, s, I, h) |= alloc(Y ). For each y ∈ Y we must have s(y) ∈ dom(h 1 ), because s(y) dom(h 2 ) and s(y

  2 and S |= alloc(Y 1 ) ∧ alloc(Y 2 ). Moreover, because (U, s, I, h) |= η 12 ∧ η 21 , the following hold, for i = 1, 2:||h|| ≥ ||A i || + ||L i || + min S ||A 1 || + ||L 1 ||) + max(min S M 2 , ||A 2 || + ||L 2 ||) ≤ ||h||(10)(1) if min S M 1 ≥ ||A 1 || + ||L 1 || then we have min S M 1 + max(min S M 2 , ||A 2 || + ||L 2 ||) ≤ ||h|| by (5) and (8). The case min S M 2 ≥ ||A 2 || + ||L 2 || is symmetric, and (2) otherwise, if min S M 1 < ||A 1 || + ||L 1 || and min S M 2 < ||A 2 || + ||L 2 ||, because S |= x ∈av(M 1 ), y ∈av(M 2 ) ¬x ≈ y, the sets of locations L 1 , L 2 , A 1 and A 2 are pairwise disjoint and, since L 1 ∪ L 2 ∪ A 1 ∪ A 2 ⊆ dom(h), it must be the case that ||h|| ≥ ||A 1 || + ||L 1 || + ||A 2 || + ||L 2 ||.

	M 3-i	(8)	||A i || + ||L i || < max I i	(9)
	We prove the following relation by distinguishing the cases below:
	max(min S M 1 ,

|h | max(||A 1 || + ||L 1 ||, min I M 1 ) max(||A 2 || + ||L 2 ||, min I M 2 )

  by Proposition 5.3. Further, by[START_REF] Echenim | The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains[END_REF] and Proposition 4.2, we have (U, s, I, h 1 ) |= |h| ≥ min M 1 ∧ |h| < max M 1 . There remains to show that (U, s, I, h 1 ) |= M a 1 ∧ M Then x ∈ av(M 1 ), thus s(x ) ∈ A 1 and (U, s, I, h 1 ) |= alloc(x ) follows, by the definition of h 1 . Dually, let ¬alloc(x ) ∈ M a 1 be a literal. Then, we have x ∈ nv(M 1 ). We distinguish the following cases:-If x ∈ av(M 2 ) then s(x ) ∈ A 2 and since dom(h 1 ) ∩ A 2 = ∅, we have s(x ) dom(h 1 ), thus (U, s, I, h 1 ) |= ¬alloc(x ). -Otherwise, x ∈ nv(M 1 ) \ av(M 2 ). Again, we distinguish the cases: otherwise, x Y 2 , thus s(x ) L 2 . But since x ∈ nv(M 1 ) \ av(M 2 ), by the definition of L 2 , it must be the Then x ∈ av(M 1 ) and s(x ) ∈ A 1 . Moreover, we have x → y ∈ fp a (M 1 ), thus (U, s, I, h) |= x → y, by (

	p 1 . 1 be a literal. 1 ) Let alloc(x ) ∈ M a (M a

* if x ∈ Y 2 then s(x ) ∈ L 2 and because dom(h 1 ) ∩ L 2 = ∅, we obtain s(x ) dom(h 1 ), thus (U, s, I, h 1 ) |= ¬alloc(x ). * case that s(x ) dom(h), thus (U, s, I, h) |= ¬alloc(x ) and (U, s, I, h 1 ) |= ¬alloc(x ) follows. (M p 1 ) Let x → y ∈ M p 1 be a literal.

  by Proposition 5.14. Otherwise ||h ′ || = min S M 2 -||h|| ≥ min I M 1 and we have by (14

  result follows from the fact that S |= dc(M 2 ) u , which implies min S M 2 < max S M 2 , by Proposition 5.14. Otherwise, ||h|| + ||h ′ || = min S M 1 + ||h|| > min S M 2 and ||h|| + ||h ′ || < max S M 2 follows from

  show membership in PSPACE, let φ = ∀y 1 . . . ∀y m . ϕ be a formula in BSR inf (SL k ), where ϕ is quantifier-free and Var(φ) = {x 1 , . . . , x n }. Let φ ′ def = ∀y 1 . . . ∀y m . χ , with χ ′ ) ∧A (φ ′ ). By Lemma 5.28, φ ≡ inf φ ′ . By Proposition 6.5, χ is BSR-compatible and we deduce by Lemma 4.9 that φ ′ (and hence φ) has an infinite model iff ψ has an infinite model where the interpretation of p is finite. We now show how to solve the latter problem. By Proposition 4.10, ψ is a BSR(FO) formula with no existential variable and contains k • n + (k + 6) • N (χ ) + 5 constants. By Proposition 5.36, N (χ ) = O(size(ϕ) 2 ), thus we deduce that ψ is a BSR(FO) formula, with O(k • size(φ) 2 ) constants and free variables. By Proposition 6.10, ψ has an infinite model where the interpretation of p is finite iff ψ ∧ ψ p has an infinite model. By Theorem 6.7, ψ ∧ ψ p has an infinite model iff it has an m-repetitive model (U, s, I) of cardinality ||U|| = O(k • size(φ) 2 ), because ψ p is a BSR(FO) formula with no existential variable and contains no constant or free variable other than those in ψ .

def = M ∈µ inf (ϕ ) M and let ψ def = τ (φ

ACM Trans. Comput. Logic, Vol. 1, No. 1, Article . Publication date: December 2019.

By "uninterpreted" we mean that the interpretation of such predicate symbols is not fixed by a theory or by inductive definitions. ACM Trans. Comput. Logic, Vol. 1, No. 1, Article . Publication date: December

The second case emp ∧ x ≈ y ⊢ ∃u ∃f . x → (f , u ) * ls(u, y ) ∨ emp ∧ x ≈ y is trivial and omitted for clarity.

This is due to the fact that some of the edges, for instance those pointing to list values, may be "dangling". In other words, this structure does not fulfill the so called establishment condition of[START_REF] Iosif | The Tree Width of Separation Logic with Recursive Definitions[END_REF].ACM Trans. Comput. Logic, Vol. 1, No. 1, Article . Publication date: December 2019.

These will simply be called structures, when no confusion arises. ACM Trans. Comput. Logic, Vol. 1, No. 1, Article . Publication date: December 2019.

The converse of C n : ∀x . (¬c n ∧ ∀y . ¬p(x, y)) → n-1 i =1 x ≈ w i is not in BSR(FO).

For simplicity, only the relevant axioms are given. ACM Trans. Comput. Logic, Vol. 1, No. 1, Article . Publication date: December 2019.

See Definition 5.2 for the definition of N p . ACM Trans. Comput. Logic, Vol. 1, No. 1, Article . Publication date: December 2019.

See equation (15) in Lemma 5.20. ACM Trans. Comput. Logic, Vol. 1, No. 1, Article . Publication date: December 2019.

Note that an equivalent definition of α fin is α fin def = ∀x . alloc(x ).

The store is arbitrary because φ contains no free variables. ACM Trans. Comput. Logic, Vol. 1, No. 1, Article . Publication date: December 2019.

ACKNOWLEDGMENTS

The authors wish to acknowledge the contributions of Stéphane Demri and Étienne Lozes to the insightful discussions during the early stages of this work.

The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates • 29 Proof.

(1) By induction on the structure of ϕ, one shows that no literal from {|h| ≥ |U | -n, |h| < |U | -n | n ∈ N} is introduced during the construction of µ inf (ϕ).

(2) Let ℓ ∈ M ∩ {|h| ≥ |U | -n, |h| < |U | -n | n ∈ N} be a literal. The proof is by induction on the structure of ϕ:

• The cases ϕ = emp, ϕ = x → y, ϕ = q(x) and ϕ = x ≈ y are trivial, because ℓ µ fin (ϕ).

• ϕ = ϕ 1 ∧ ϕ 2 : we have M ∈ [M 1 , M 2 ], for some minterms M i ∈ µ fin (ϕ i ), for i = 1, 2. By Proposition 5.26, since ℓ {|U | ≥ n, |U | < n | n ∈ N}, we deduce that ℓ ∈ M 1 ∪ M 2 and the proof follows from the induction hypothesis, since any formula occurring in ϕ i , i = 1, 2, occurs at the same polarity in ϕ. • ϕ = ¬ϕ 1 : assuming µ fin (ϕ 1 ) = {M 1 , . . . , M m }, we have M ∈ ℓ 1 , . . . , ℓ m mt , for some literals ℓ i ∈ M i , i ∈ [1, m]. By Proposition 5.26, we deduce that ℓ = ℓ i for some i = 1, . . . , n, because ℓ {|U | ≥ n, |U | < n | n ∈ N}. By the induction hypothesis, there exists a formula ψ 1 -- * ψ 2 occurring at polarity p ∈ {1, -1} in ϕ 1 , where

Then ℓ occurs at polarity -p in M and ψ 1 -- * ψ 2 occurs at polarity -p in ϕ.

• ϕ = ϕ 1 * ϕ 2 : for i = 1, 2, there exist minterms M i ∈ µ fin (ϕ i ), N i ∈ (M i ) E(M 1 ∪M 2 ) and P i ∈ (N i ) N p 3-i , such that M ∈ (elim * (P 1 , P 2 )) dnf mt . Since by hypothesis ℓ ∈ {|h| ≥ |U | -n, |h| < |U | -n | n ∈ N}, by Proposition 5.26, this literal is necessarily introduced by elim * (P 1 , P 2 ) and, by inspection of elim * (P 1 , P 2 ), one of the following must hold: -ℓ = |h| ≥ min M 1 + min M 2 , where min M 1 and/or min M 2 is of the form |U | -n. By the induction hypothesis ϕ i contains a formula ψ 1 -- * ψ 2 at polarity 1, for some i = 1, 2, and the proof is completed.

, where max M 1 and/or max M 2 is of the form |U | -n. The proof is similar, with polarity -1.

where min M j is of the form |U | -n. The proof is similar.

. By inspection of elim fin ⊸ (Q 1 , N 2 ), one of the following cases must occur: -ℓ = |h| ≥ min M 2 -max M 1 -1, where min M 2 is of the form |U |-n 2 . By the induction hypothesis, ϕ 2 contains a formula ψ 1 -- * ψ 2 at polarity 1, and this formula also occurs at polarity 1 in ϕ, thus the proof is completed. Note that if max ℓ = |h| < |U |min M 1 -# n (Y , M 1 ) + 1. In this case since (ϕ 1 -- * ¬ϕ 2 ) occurs at polarity -1 in ϕ, the proof is completed.

(3) Let ℓ ∈ M ∩ {alloc(x ), ¬alloc(x ) | x ∈ Var} be a literal occurring in some minterm M ∈ µ inf (ϕ). The proof is by induction on the structure of ϕ:

• The cases ϕ = emp, ϕ = x → y, ϕ = x ≈ y and ϕ = q(x) are trivial, because ℓ µ inf (ϕ).

• The cases ϕ = ϕ 1 ∧ ϕ 2 and ϕ = ¬ϕ 1 are similar to point (2) of the Lemma.

, for all i = 1, 2. By inspection of elim * (P 1 , P 2 ), one of the following cases must occur:

Assuming that the definition of elim * (P 1 , P 2 ) is changed according to Remark 5.19, it must be the case that ¬alloc(x ) occurs at a positive polarity in M 1 or M 2 . Then, by the induction hypothesis ϕ i contains a subformula ψ 1 -- * ψ 2 at polarity -1 with x ∈ Var(ψ 1 ) ∪ Var(ψ 2 ). But then ψ 1 -- * ψ 2 also occurs at polarity -1 in ϕ and the proof is completed. -ℓ = ¬alloc(x ) with x ∈ Y ⊆ nv(M j ). Similar to the previous case.

. By the induction hypothesis, ℓ i is M-bounded by ϕ, for every i ∈ 1, . . . , n, thus the same holds for

we deduce that ℓ i mt is M-bounded by ϕ, and the proof follows from Proposition 5.34.

First assume that ℓ is of the form |h| ≥ t or |h| < t. We only consider the case where ℓ occurs in elim * (P 1 , P 2 ), the rest of the cases follow from Proposition 5.34. We distinguish the following:

by Proposition 5.27. By the inductive hypothesis we have

we have:

If min

and we obtain:

Otherwise, min

-The proof in the case where ℓ is a subformula of |h|

Then one of the following holds: -ℓ ∈ dc(P i ) u , for some i = 1, 2, and we have two cases:

, where min P i = min M i = n 1 and max

By the induction hypothesis, we have 2 ) , for i = 1, 2, and minterms The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates • 33

. We only consider the case where ℓ occurs in elim fin ⊸ (Q 1 , N 2 ), in the remaining cases, the result follows directly from Proposition 5.34. If ℓ is of the form |h| ≥ t or |h| < t then either:

Otherwise, min M 2 = n 2 and max

is polynomially bounded by size(ϕ), this entails that it is possible to check whether M ∈ µ fin (ϕ) (resp. µ inf (ϕ)) using space bounded also by a polynomial in size(ϕ).

Proposition 5.36. Given a quantifier-free SL k formula ϕ and a minterm

Proof. We give the proof for M ∈ µ fin (ϕ), the case M ∈ µ inf (ϕ) being similar. Let ℓ ∈ M be a literal. We distinguish the following cases, based on the form of ℓ:

• ℓ ∈ {alloc(x ), ¬alloc(x ) | x ∈ Var}: ℓ must occur in ϕ or has been introduced by µ fin (.), in which case, at most 2 • ||Var(ϕ)|| such literals are introduced.

introduce literals of this form.

• ℓ ∈ {x ≈ y, ¬x ≈ y | x, y ∈ Var}: ℓ occurs in ϕ or has been introduced by µ fin (.), in which case at most 2 • ||Var(ϕ)|| 2 such literals are introduced.

for each such literal. Furthermore, M contains at most two literals of this form (up to redundancy). • ℓ ∈ {|h| ≥ min M , |h| < max M }: by Lemma 5.35, M (ℓ) ≤ M (ϕ) and consequently, size(ℓ) = O(size(ϕ) 2 ) for each such literal. Furthermore, M contains exactly two literals of this form by definition of minterms. Summing up, we obtain that size(M ) = O(size(ϕ) 2 ). This second result follows immediately. □ Proposition 5.37. Let L be a set of literals and ϕ be a boolean combination of literals. The problem of deciding whether L ∈ (ϕ) dnf is in NSPACE(size(L) + size(ϕ)).

Proof. W.l.o.g., we may assume that ϕ is in negation normal form. The algorithm is nondeterministic and proceeds recursively on the structure of ϕ:

• ϕ = ℓ is a literal: then (ϕ) dnf = {ℓ} hence it suffices to verify whether L = {ℓ}, using O(size(L) + size(ϕ)) space.

) dnf and we check that one of L ∈ (ϕ 1 ) dnf and L ∈ (ϕ 2 ) dnf holds. By the induction hypothesis, checking L ∈ (ϕ i ) dnf can be done using O(size(L) + size(ϕ i )) space. Since the working space used for L ∈ (ϕ 1 ) dnf can be reused for L ∈ (ϕ 2 ) dnf , the entire check takes O(size(L) + size(ϕ)) space.

Since we must store L 2 during the check L 1 ∈ (ϕ 1 ) dnf and the working space can be reused for L 2 ∈ (ϕ 2 ) dnf , the entire check takes O(size(L) + size(ϕ)) space. □ Proposition 5.38. Let L be a set of literals and let M 1 , M 2 be minterms. Checking whether L ∈ ((elim

Proof. The algorithm proceeds by induction on the structure of (elim * (M 1 , M 2 )) dnf as in the proof of Proposition 5.37. The only difference concerns the subformulae η i j (Line 6 in Lemma 5.16) which cannot be constructed explicitly since they are of exponential size. However, η i j is of positive polarity, and to check that L ∈ η i j dnf , it suffices to guess a set of variables Y ⊆ nv(M j ) \ av(M i ) and check whether:

The size of the above formula is of the order of O(size(M 1 ) + size(M 2 )), thus L ∈ ((elim * (M 1 , M 2 )) dnf can be checked in NSPACE(size(L) + size(M 1 ) + size(M 2 )), by Proposition 5.37. □ Proposition 5.39. Let L be a set of literals and let M 1 , M 2 be minterms. The problems whether L ∈ (elim fin

Proof. The proof is similar to that of Proposition 5.38 (again, the formula λ † is exponential, but does not have to be constructed explicitly). The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates • 35

Proof. The proof is by induction on

i=1 size(M i ). The nondeterministic algorithm guesses and stores a minterm M ′ 1 of size at most n-1 i=1 size(M i ) and checks that

space, and the second check takes space O(size(M ′ 1 ) Proof. We show the existence of a nondeterministic algorithm that decides M ∈ µ fin (ϕ) in space O(size(M ) + size(ϕ) 8 ). The PSPACE upper bound is by an application of Savitch's Theorem [START_REF] Walter | Relationships between nondeterministic and deterministic tape complexities[END_REF]. We only give the proof for M ∈ µ fin (ϕ), the proof for M ∈ µ inf (ϕ) is similar and omitted. By induction on the structure of ϕ, we distinguish the following cases:

• ϕ = emp: we check M = |h| ≃ 0 in space O(size(M ) + size(ϕ)).

• ϕ = x → y: we check M = x → y ∧ |h| ≃ 1 in space O(size(M ) + size(ϕ)).

• ϕ = q(x 1 , . . . , x #(q) ): we check M = q(x 1 , . . . , ). Since we only need to store M 1 and M 2 between the checks, the entire procedure takes space O(size(M ) + size(ϕ) 8 ).

, where µ fin (ϕ) = {M 1 , . . . , M m }. For any i ∈ [1, m], we distinguish the following cases: ) 2 ) = O(size(M ) + size(ϕ 1 ) 8 ), by Proposition 5.40. Observe that this case is the most complex one, and it leads to the exponent 8 in the above inductive invariant. To ensure that the set {ℓ 1 , . . . , ℓ m } contains no literal other than ℓ ′ 1 , . . . , ℓ ′ n , we also have to check that every minterm M j , for j ∈ [1, m] contains a literal ℓ ′ i , for some i ∈ [1, n]. To this aim, we use a nondeterministic algorithm for the complement: we guess a minterm M ′ M-bounded by ϕ 1 , check that M ′ ∈ µ (ϕ 1 ) and that it contains no literal ℓ i , for i ∈ [1, n]. By the inductive hypothesis, this is possible in space O(size(M ′ ) + size(ϕ 1 ) 8 ) = O(size(ϕ 1 ) 2 + size(ϕ 1 ) 8 ) = O(ϕ 8 1 ). Then, checking that every minterm M j , for j ∈ [1, m] contains a literal ℓ ′ i , for some i ∈ [1, n] can be done in the same amount of space, using a nondeterministic algorithm, see e.g. [START_REF] Arora | Computational Complexity -A Modern Approach[END_REF]Corollary 4.21].

, for i = 1, 2. We first guess minterms M 1 , M 2 of size O(size(ϕ 1 ) 2 ) and O(size(ϕ 2 ) 2 ), respectively, check that M i ∈ µ fin (ϕ i ), then guess N i ∈ (M i ) E(M 1 ∪M 2 ) and P i ∈ (N i ) N p 3-i , for i = 1, 2. This is feasible since by definition each minterm in these sets is of size O(size(M 1 ) + size(M 2 )). Next, we guess minterms M ′ , M ′′ , of size O(size(M 1 ) + size(M 2 )) as well, and check that M ′ ∈ (elim * (P 1 , P 2 )) dnf in space O(size(M ′ ) + size(P 1 ) + size(P 2 )), by Proposition 5.40 and M ′′ ∈ [M ′ ] mt in space O(size(M ′′ ) + size(M ′ ) 2 ), by Proposition 5.41.

• ϕ 1 ⊸ ϕ 2 : the proof is similar to the previous case. □

BERNAYS-SCHÖNFINKEL-RAMSEY SL k

This section contains the results concerning decidability of the (in)finite satisfiability problems within the BSR(SL k ) fragment. First, we show that, contrary to BSR(FO), the satisfiability of BSR(SL k ) is undecidable for k ≥ 2. Second, we carve two nontrivial fragments of BSR(SL k ), for which the infinite and finite satisfiability problems are both PSPACE-complete. defined based on restrictions of (i) polarities of the occurrences of the separating implication, and (ii) occurrences of universally quantified variables in the scope of separating implications. These results draw a rather precise chart of decidability within the BSR(SL k ) fragment.

Undecidability of BSR(SL k )

Theorem 6.1. The finite and infinite satisfiability problems are both undecidable for formulae in BSR(SL k ) even if the formulae contain no uninterpreted predicates.

Proof. Let φ = ∀x . ϕ be a formula in BSR 2 (FO), where ϕ is quantifier-free, contains no predicate symbol, one variable x, one constant symbol c and two monadic function symbols f and д of sort U. It is known that the finite satisfiability problem is undecidable for such formulae, by Proposition 2.3. We reduce this problem to the infinite and finite satisfiability problems for BSR(SL k ) formulae. We proceed by first flattening each term in ϕ consisting of nested applications of f and д. The result is an equivalent sentence φ flat = ∀x 1 . . . ∀x n . ϕ flat , in which the only terms are x i , c, f

The formal construction is standard and thus omitted. We define the following BSR(SL 2 ) formulae, for † ∈ fin, inf :

6.2 Decidability Proofs To check that S ̸ |= τ (∀y 1 . . . ∀y m . M ∈µ † (ϕ ) M ), we may thus guess locations ℓ 1 , . . . , ℓ m ∈ U and check that

There remains to prove that the latter test in is PSPACE.

To this aim, we consider again the complement problem (U, s[y

We guess a minterm M that is M-bounded by ϕ, then check that M ∈ µ † (ϕ) and that (U, s[y

The first check is in PSPACE, by Lemma 5.42. The second check is also in PSPACE, by Proposition 6.2. □ Remark 6.4. Note that the size of an FO-structure S = (U, s, I) is exponential w.r.t. the arity of the symbols in F . In our context, the arity of all symbols is bounded by a constant, except that of the special symbol p that encodes the heap. Further, in the following (see for instance the proof of Theorem 6.11), we will only consider structures that satisfy the formula Heap in Definition 4.6 , so that p I is a partial function and ||p I || ≤ ||U||. Hence we may assume that the size of S is polynomial in ||U|| + k + dom(s). ■ 6.2.2 Infinite Satisfiability (BSR inf (SL k )). We start by showing decidability, in PSPACE, of the infinite satisfiability problem for the BSR inf (SL k ) fragment. We first establish the following result: Proposition 6.5. Let φ = ∀y 1 . . . ∀y m . ϕ be a formula in BSR inf (SL k ), where ϕ is quantifier-free. The formula

Proof. By Lemma 5.29 [START_REF] Antonopoulos | Foundations for Decision Problems in Separation Logic with General Inductive Predicates[END_REF], no formula of the form |h| ≥ |U | -i occurs positively in χ . Furthermore, if alloc(x ) positively occurs in χ , then it must occur in a minterm in µ inf (ϕ), and by Lemma 5.29 (3), x necessarily occurs in the scope of a positive occurrence of -- * , which entails by definition of BSR inf (SL k ) that x {y 1 , . . . , y n }. Consequently, χ is BSR-compatible. □ Proposition 6.5, together with Lemma 5.28, ensures that a reduction from BSR inf (SL k ) to BSR(FO) is feasible. However, we also have to ensure that the cardinality of the universe is infinite and that the cardinality of the heap is finite, which cannot be expressed in FO. To this aim, we rely on existing results about the cardinality of models of BSR(FO) formulae. The definition and theorem below are from [START_REF] Fontaine | Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class[END_REF] (they have been slightly adapted to handle formulae containing free variables).

The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates • 39 Definition 6.6. Let S = (U, s, I) be an FO-structure.

and there exists a total order ≺ on U such that for every n ≤ m and strictly increasing sequences e 1 ≺ • • • ≺ e n and e ′ 1 ≺ • • • ≺ e ′ n of elements in B, for every predicate symbol q ∈ F and every d 1 , . . . , d #(q) ∈ A ∪ {e 1 , . . . , e n } the following holds:

The following theorem, proved in [START_REF] Fontaine | Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class[END_REF], characterizes the existence of an infinite model of a BSR(FO) formula. The intuition is that, due to the above condition, the interpretation of the predicate symbols in an m-repetitive model fulfills some symmetry properties that make it possible to extend this model into an infinite one by adding infinitely many copies of existing elements. Conversely, it is possible to show that every infinite model (actually, every model of sufficiently large cardinality) admits a restriction that is m-repetitive (the proof is based on Ramsey's theorem for hypergraphs [? ]). Theorem 6.7. Consider a BSR(FO) formula φ containing n free variables and constants, no existential quantifier and m distinct universally quantified formulae. The formula φ has an infinite model if and only if it has an m-repetitive model (U, s, I) such that ||U|| ≤ n + m.

Proof. See [START_REF] Fontaine | Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class[END_REF]Theorems 4 and 5]. The addition of free variables is not problematic as they can be handled as constants. □ Proposition 6.8. Testing whether a first-order structure S = (U, s, I) is m-repetitive for a given m ∈ N is in PSPACE.

Proof. The algorithm is straightforward: it is clear that A and B can be computed in polynomial time, then it suffices to guess some total order < on U, to iterate over the increasing sequences (e 1 , . . . , e n ), (e ′ 1 , . . . , e ′ n ) ∈ B n , with n ≤ m, over the predicate symbols q ∈ F and elements d 1 , . . . , d #(q) ∈ A ∪ {e 1 , . . . , e n }, to compute in each case the elements d ′ 1 , . . . , d ′ #(q) according to Definition 6.6 and to check that the equivalence (d 1 , . . . , d #(q) ) ∈ q I ⇔ (d ′ 1 , . . . , d ′ #(q) ) ∈ q I holds. □ Theorem 6.7 and Proposition 6.8 provide an effective method to decide whether a formula ϕ in BSR(FO) has an infinite model. To ensure that the domain of the predicate p encoding the heap is finite we rely on the following definition and result: Definition 6.9. Let φ be a BSR(FO) formula. We denote by φ p the formula:

where x 1 , . . . , x k +1 are pairwise distinct variables not occurring in φ. Proposition 6.10. Let φ be a BSR(FO) formula. The two following assertions are equivalent.

• φ has an infinite model (U, s, I) such that p I is finite.

• φ ∧ φ p has an infinite model.

Proof. This is immediate, since C(α ) entails that every element distinct from x 1 , . . . , x α is allocated. □ Lemma 6.16. Given a formula φ ∈ BSR fin (SL k ) and a number α ∈ N encoded in unary, the problem of checking whether φ has an α-controlled model is in PSPACE.

Proof. We assume that the formula φ is of the form ∀y 1 , . . . , y m . ϕ, with Var(φ) = {x 1 , . . . , x n }. Let x 1 , . . . , x α be pairwise distinct variables not occurring in {x 1 , . . . , x n , y 1 , . . . , y m }. It is clear that φ admits an α-controlled model iff it admits a model that also validates C(α ). Let χ

The algorithm is defined as follows (see the proof of Theorem 6.11 for details). We first guess a structure (U, s, I) such that ||U|| = O(k • size(φ) 2 + k • α ) and (U, s, I) |= Heap. Then we check that (U, s, I) |= τ (φ ′ ) (as done in the proof of Lemma 6.3, except that all formulae alloc(x ) are replaced by α i=1 (x ≈ x i → alloc(x i ))), that (U, s, I) |= τ (C(α )) (using Proposition 6.14) and that (U, s, I) |= A(φ ′ ∧ C(α )) (using Proposition 6.2). □

The General Case. To handle the case where no α-controlled model exists, the following results are used. Proposition 6.17. Let (U, s, I) be a non-α-controlled FO-structure satisfying the (Heap) axiom, defined on page 11. Let E ⊆ U, with ||E|| ≤ α. There exists an element u ∈ U \ E such that either u is not allocated, or there exist v 1 , . . . , v k ∈ U and j ∈ [1, k] such that (u, v 1 , . . . , v k ) ∈ p I and v j E ∪ {u}.

Proof. Because (U, s, I) is not α-controlled, we have

Let s ′ be any extension of s to x 1 , . . . , x α such that s ′ ({x 1 , . . . , x α }) = E (such as store necessarily exists since ||E|| ≤ α). We have 4), every literal alloc(x ) occurs within a subformula λ fin of some formula elim fin ⊸ (M 1 , M 2 ), hence inside a formula of the form alloc(x ) ∨ (|h| < |U | -q ∧ |U | ≥ r ). Thus C (hence C ′ ) contains either |h| < |U | -q or |U | ≥ r , and necessarily, q, r ≤ N (χ 2 ) ≤ N (χ ). But S has more than N (χ ) unallocated elements, hence S |= (|h| < |U | -q ∧ |U | ≥ r ). Therefore, (U, s ′ , I, h) |= C ′ , which contradicts our previous assumption.

Consequently, the initial problem boils down to testing whether φ ′ has a finite model. It is clear that φ ′ is BSR-compatible (since by definition all positive occurrences of alloc(x ) have been removed), hence by Lemma 5.28, it is sufficient to test whether τ (φ ′ ) ∧ A(φ ′ ) has a finite model. By Proposition 4.10, the formula τ (φ ′ ) ∧ A(φ ′ ) is equivalent to a formula in BSR(FO). We have N (φ ′ ) ≤ N (∀y 1 , . . . , y m . χ ), hence, using Propositions 2.2, 4.10 and 5.36 we deduce as it is done in the proof of Theorem 6.11, that τ (φ ′ ) ∧ A(φ ′ ) has a finite model iff it has a model (U, s, I), with ||U|| = O(k • size(φ) 2 ).

The algorithm is then defined as follows (see the proof of Theorem 6.11 for details). We guess an FO-structure (U, s, I) satisfying Heap such that ||U|| = O(k • size(φ) 2 ) and check in polynomial space that (U, s, I) |= τ (φ ′ ) (this is done as in Lemma 6.3, except that the test formulae alloc(x ) are replaced by ⊤) and that (U, s, I) |= A (φ ′ ) (using Proposition 6.2) . □

CONCLUSION

We have studied the decidability problem for SL formulae with quantifier prefix in the language ∃ * ∀ * , denoted as BSR(SL k ), for finite and infinite universes, in the presence of uninterpreted predicate symbols. Although both problems were found to be undecidable, we identified two non-trivial subfragments for which the infinite and finite satisfiability are PSPACE-complete. These fragments are defined by restricting the polarity of occurrences of separating implications as well as the occurrence of universally quantified variables within the scope of separating implications. In both cases, the number of record fields k may be part of the input, but we assume that the arity of the uninterpreted predicates is bounded by a constant. If the latter condition does not hold, then the provided algorithms run in exponential space, and the problem is NEXPTIME-complete. Note that the PSPACE-completeness results for BSR fin (SL k ) and BSR inf (SL k ) allow us to (re-)establish the PSPACE-membership of the satisfiability problem for quantifier-free formulae of SL k , both in finite and infinite domains. Indeed, every