Giuseppe Iurato
email: giuseppe.iurato@community.unipa.it

Mathematical thought in the light of Matte Blanco's work

Taking into account some basic epistemological considerations on psychoanalysis by Ignacio Matte Blanco, it is possible to deduce some first simple remarks on certain logical aspects of schizophrenic reasoning. Further remarks on mathematical thought are also made in the light of what has been established, taking into account the comparison with schizophrenia pattern.

Ignacio Matte Blanco has been a notable psychiatrist and psychoanalyst who has devoted many years of his work in studying the mathematical thought, starting from his many-years experience with schizophrenic patients. His definitive results were published in the celebrated work entitled Unconscious as Infinite Sets: An Essay on Bilogic (1975), which has seen various editions.

In this paper, we mainly follow the synthetic work [START_REF] Figà-Talamanca | La logica dell'inconscio[END_REF] which explain the main psychoanalytic considerations, also from an epistemological viewpoint, on the logic of unconscious deduced by Matte Blanco from his already mentioned fundamental psychiatric experience on schizophrenic patients.

First, the preface by Professor Adriano Ossicini to [START_REF] Figà-Talamanca | La logica dell'inconscio[END_REF] argues on the general epistemological aspects of the psychological sciences, since the work of Matte Blanco is just directed toward these last, that is to say, he tries to establish fundamental relationships between the psychoanalysis and the exact sciences, in particular the mathematics. The work of Matte Blanco1 is an original, interpretative afterthought of the Freudian theory through the methods of elementary logic. He starts from certain Freudian postulates which characterize the dynamical structure of unconscious, namely 1) displacement, 2) condensation, 3) absence of time, 4) substitution of the external reality with the psychic one (literal interpretation of the metaphor) and 5) absence of mutual contradiction among the presentation of the various instincts (or drives).

In particular, according to Freud2 , the usual ordinary logic rules of conscious thought are no valid for the unconscious since it operates according to another logic system. The former is ruled by a classical, assertoric (i.e., not modal) logic founded on the material implication and having, as fundamental laws, the identity principle, the non-contradiction principle, the bivalent principle, the principle of sufficient reason and the principle of the excluded third (tertium non datur). Instead, according to the studies on schizophrenia made by Matte Blanco, the fundamental principles of the unconscious are the generalization principle 3 and the symmetric principle 4 (see [1, Chap. I, Section 2]), through which it carries out the primary process (whereas the secondary process concerns the modus operandi of conscious thought). Subsequently, through them, Matte Blanco tries to explain the previous Freudian characteristic principles of unconscious (see [START_REF] Figà-Talamanca | La logica dell'inconscio[END_REF]Chap. II]). In particular, he re-examines (see [1, Chap. II, Section 2]) the classical Freudian agencies in the light of his principles. According to Matte Blanco, the conscious and unconscious are two different modes of being respect to the psychophysics unity of the human individual, asymmetric and in becoming the first one, symmetric and static the second one: this terminology is due to the fact that the latter is regulated by the above mentioned symmetric principle, contrarily to the first one.

Following [1, Chap. III], the symmetry and staticity, characterizing the unconscious, do not allow any finite-dimensional space-time idea as well as any sequential logic reasoning (which relies on asymmetry, as we will see later), so that the asymmetric conscious thought seems to be the result of a sort of 'symmetry breaking' of the infinite symmetric unconscious world (recalling, besides, that the symmetry breaking mechanisms, according to the modern physics, are at the basis of any fundamental physical phenomenology from the dynamical viewpoint). Nevertheless, according to Matte Blanco, the conscious becoming cannot do without the being unconscious, so that it may seem to be, in a certain sense, solved the secular vexata quaestio concerning the known Parmenides-Heraclitean dialectic between the logic of being and the logic of becoming (see also [START_REF] Carruccio | Mondi della Logica[END_REF]Chap. 6, Section 6.2]). Indeed, according to this Author, the pair unconscious-conscious is inseparable. The symmetric thought is unthinkable without the asymmetric one, and the limit between normality and abnormality is given by the degree of reciprocal compenetration of these two modes of being.

In [1, Chap. IV], it is discussed the Matte Blanco's notion of unconscious as infinite set, resuming the distinction between set and class, as typical of formal set theory. The unconscious does not distinguish between partial and total object and, moreover, each element of any set is conceived as having only human qualities (anthropomorphization attempts). This last property is a fundamental epistemological assumption common to many theory of the history of human thought, even if Matte Blanco deduced it from psychoanalytic considerations.

In [1, Chap. IV], it is also discussed the notion of infinite set in Mathematics, analogically compared with the symmetric mode of being of the unconscious, precisely with its property of indistinguishability between the part and the whole, in the sense that they both have the same cardinality, this just being the first notion of infinite set according to R. Dedekind (that, inter alia, has considered the notion of infinite set as a tool to explain the world of the human thought -see [1, Chap. IV, pp. 47-48, footnote 3]). Again according to Matte Blanco, many other mathematical concepts (like that of limit process) have their origins by the attempts to asymmetrically explain the properties of the symmetric one.

In [1, Chap. V], it is explained some useful concepts about consciousness according to Matte Blanco. Exactly, it cannot do without the asymmetric thought, in the sense that a conscious act consists in a continuous setting-up of asymmetric relations around the cathexis object (that is to say, the not-well defined thing invested by the human desire). The main consciousness' activity is essentially analytic because it fundamentally subdivides every analyzed object into its constitutive components or parts (partial objects), unlike by an emotion, or an affection, which is a globally conceived symmetric sentiment 5 .

Nevertheless, the symmetric and asymmetric modes are inseparable amongst them, because an entirely symmetric mode is typical of any state of loss of consciousness whereas a complete asymmetric mode is also impossible since it would imply a total absence of any cathexis object, which is impossible for each human being. Every normal psychic state varies within an interval (or range) including a right mixing of both these modes, but whose ratio is continuously changing. Moreover, if we consider, for instance, a mathematical argument -hence a full asymmetric thought, at least in the involved theoretical principles and at the end of his formulation -then there is always an unavoidable emotional involvement which may be described as an involvement of asymmetrical type 6 . Therefore, albeit a certain human result -like a mathematical proof -may seem to be the result of a completely asymmetrical work, indeed its production is never separated from an emotive-affective component of symmetric nature. This last remark is a fundamental one for understanding the nature of a creative thought. Here, we simply observe that this fact gives a line of overall consistency to the whole present paper: indeed, a creative thought is just of this last type, that is to say, it is the result of a dialectical (inseparable) interaction of the two modes of being, symmetric and asymmetric 7 . Further, according to Matte Blanco, the consciousness may think only in a three-dimensionally way, plus eventually a fourth temporal dimension, so that the threedimensional space seems to be the dimension of consciousness and imagination. The human thought thinks mainly by three-dimensional images, also in abstraction (confirming a suggestion by J. Hadamard -see [START_REF] Hadamard | The Psychology of Invention in the Mathematical Field[END_REF]). On the other hand, some consciousness contents are available only by means of introspection, which is an asymmetric phenomenon. According to Matte Blanco, it has a precise characteristic: namely, it never concerns the instant in which takes place the introspection, but it concerns the immediately previous moments (hence, the past). The human thought exists only if it is reflected on itself, or else, the most peculiar character of the human thought is just this reflectivity. The elusive character of the conscious thought is due to the fact that the real nature of the consciousness is temporally located between these two modes of being, the symmetric and the asymmetric one, so that each time we try to think a conscious content, then we diachronically restrict ourselves to the asymmetric mode, so completely excluding the (synchronically inevitable) symmetric components. Only historically thinking, it is possible to avoid (or minimize) the latter. In [1, Chap. VI], it is discussed the concept of emotion (see previous footnotes 5 and 6 ) which plays a fundamental role for all the psychic life, above all in the formation of the thought. It is also describable by means of introspection. Nevertheless, it is mainly (but not completely) a symmetric phenomenon (see [1, Chap. VI, p. 68]).

Finally, in [1, Chap. VII], it is delineated one of most important Matte Blanco' notions, precisely that of Bilogic. According to this Author, the unconscious logic (or symmetric logic) is, as already said, mainly based on the principle of symmetry and on the principle of generalization, which regulate the so-called mode of being symmetric. The latter is inseparable from the mode of being asymmetric, regulated by the bivalent logic (as already said, the usual 'definitions' are possible only with the asymmetric thought), and vice versa, that is to say, any human psychic manifestations is the result of the interaction and/or the cooperation between these two modes of being. And this implies that any human reasoning is the result of the combination of the rules of two main logics, that symmetric and the bivalent (or asymmetric) one, which, in turn, are interpreted as components of a unique bilogic. Therefore, every human psychic phenomenon turns out to be a bilogic process which is a mixed chain of symmetric and asymmetric subprocesses whose combination modes are, a priori, various and infinities, giving rise to the rich variety of the human thoughts. The emergence, at the threshold of consciousness, of a bilogic process is related with the concept of triad by Matte Blanco. This last concept should be meant as a fundamental structure of the Mathematical Logic, according to which it is the entity formed by two theoretical objects related with each other by a third object called relation. Matte Blanco thinks that the logic-mathematical structures are the results of the application of his theory of human psyche structure based on the notion of bilogic process. The bilogic process has been analyzed in many therapeutic cases treated by Matte Blanco, in both normal and pathological (schizophrenic) cases. At the end, he has formulation, on given philosophical ideas, hence with a certain sentimental (hence emotive, according to Damasio) participation (see also next footnote 9 ) if one considers the arising process of philosophical systems. 7 This point of view is also supported by the theses of one of the foremost scholars of schizophrenia, Silvano Arieti (1914Arieti ( -1981)). In fact, in his remarkable studies on this disorder, exposed in [START_REF] Arieti | Interpretazione della schizofrenia[END_REF], he subsequently distinguishes (in [START_REF] Arieti | Creatività. La sintesi magica[END_REF]) three main processes with which the human being thinks: a primary process which is prelogic with a paleosymbolic function, primitive, not abstract and with individual referents; a secondary process which regulates the logic-formal models of the vigil thought; and a tertiary process which is the result of the interaction of the first two, and culminating into the creative intuition. The first two of these three Arieti's mental processes are substantially those corresponding to the Freudian ones. concluded that the normal thought takes place in a context of (logic) causality, whereas the schizophrenic one (which, as an emblematic paradigm, permits us to shed a look within the unconscious realm) seems to follow an acausal context.

Finally, in [1, Chap. VII, Section 2], it is summarized other very interesting analyses of the bilogic structure in schizophrenic patients according to the studies conducted by Matte Blanco. For our purposes, it is simply enough to observe that the chronic schizophrenic thought continuously uses the symmetric and generalized principles in her or his reasoning. On the other hand, these last, from a formal (or mathematical) viewpoint, imply an impossibility to establish the so-called axiom of specification (or of separation) of the Formal Set Theory, according to which (see [5, Chap. 1, Section 1]), if A is a set and p(x) is a statement for each x of A, then there exists a set B such that y∈B if and only if y∈A and p(y) is true 8 ; in such a case, we will write B≐{y; y∈A, p(y)}. The chronic schizophrenic patient, according to Matte Blanco, is unable to use such a fundamental axiom, hence he or she is also unable to (mentally) construct the Boolean algebra P(A) given by all the subsets of an arbitrary set A (to which every complete and completely distributive Boolean algebra is isomorphic, by means of the theorems of A. Tarski -see [6, Chap. V, Section 2] -and other representation theorems like those of M.H. Stone). This is due to the almost total use of symmetry and generalization principles in her or his reasoning. On the other hand, according to the just mentioned Stone's representation theorems (see [6, Chap. V, Section 2], [7, Chap. I] and [17, Proposition 1.4.4]), the two-element Boolean algebra 2 (following Halmos' notations) with support set {0,1}, is isomorphic to a Boolean algebra of the type P(A) for some set A (like, for instance, the set of all maximal ideals of 2, that is to say, its maximal spectrum). On the other hand, since 2 is the mathematical structure which formalizes the propositional calculus (that is to say, it is its propositional algebrasee [START_REF] Pini | Primo Corso di Algebra[END_REF]Chap. 6] and [START_REF] Carruccio | Mondi della Logica[END_REF]Chap. 4]), it follows that a chronic schizophrenic patient is basically unable to construct such an algebra, that is to say, he or she is unable to perform a rigorous syllogistic inference (which is the general element of 2). This might explain, amongst other things, the great difficulties to perform a makes sense reasoning by a chronic schizophrenic patient. Furthermore, and this is a crucial point of our discussion, the two-element Boolean Algebra 2 is also the truth's value algebra of the semantics (meant as the study of the various, possible interpretations of the propositional calculussee [14, Chap. 5]), whence it follows too that a chronic schizophrenic patient is unable to integrate syntax-semantics and semantics-pragmatics, as also witnessed by recent neuropsycholinguistic researches (see [START_REF] Iurato | On Jacques Lacan Psychosis Theory and ERPs Analysis[END_REF]). Moreover, from an historical viewpoint, we remember that the original motivations to the same George Boole's work entitled An investigation of the laws of thought (1854), in which he introduced this algebra structure (see [8, Chap. 2, Section 2.1.2]), were just due to the attempts to formally analyze the laws of Logic considered as a result of human thought.

Moreover, in [8, Chap. 7, Section 7.3], it is confirmed that many people reason according to an incorrect inference that, in the light of what has been said above, may be explained (following Matte Blanco) through the unavoidable presence of the symmetric thought together the asymmetric one, that is to say, by means of a bilogic process. In [8, Chap. 7, Section 7.3.1], it is discussed the structure of a syllogistic inference of the type A⇒C considered as the main elementary and basic logic tool of reasoning, the primary epitome of consciousness: it is, according to the Mental Models Theory (see [START_REF] Johnson-Laird | Syllogistic Inference[END_REF]), the result of the action of three inseparable phases, the construction, the integration and the verification. The construction consists in the interpretation of the premises (relatives to A), namely, in the individual construction, for each premise, of a mental model representing the state of things that every premises describes. The integration consists in the coherent integration of these various models into a unique integrated model (for instance, individuating one or more so-called intermediate terms B between the extreme terms A and C) for the syllogistic conclusion (relatives to C). Finally, the verification consists in the epistemological analysis of the validity of the reached conclusion (for instance, by means of the K.R. Popper falsification method, constructing suitable counterexamples). Often, the integration phase includes the institution of possible effect-cause links between the two extreme terms. Moreover, the establishing of these last relations is mainly a creative activity, since it is not based on preconstituted laws. On the other hand, following [START_REF] Lolli | QED -Fenomenologia della dimostrazione[END_REF], a conditional enunciate is a (rational) enunciate of the type «if A then C» where A are the initial assumptions (like, for example, a single enunciate or a conjunction or a set of enunciates) considered as axioms of a certain theory, whereas C is the conclusion. Usually, in the conditional enunciates of the type A⇒C, A are the hypotheses while C is the thesis. Not every conditional enunciate is a theorem, since as theorem we mean a conditional enunciate in which C is a logical consequence of A, that is to say, if, in every interpretation of the formal language in which are formulated A and C, C is true whenever A is true, and, in such a case, we write more specifically ⊨A⇒C. Hence, in each theorem, the conditional enunciate A⇒C means that this syllogistic inference is valid, namely it is true for every interpretation. This leads us towards the syntax, independently by the semantics (which studies all the possible interpretations). From here, we are naturally led towards the general notion of proof of a theorem of the type ⊨A⇒C which is the search for the chain (called derivation) of the formal passages each constituted by an elementary conditional enunciation through which it is overall possible to deduce C from A. Hence, it is formally explainable as the search for a series of intermediate terms B 1 , ..., B n such that the proof is formed by the chain A⇒B 1 ⇒ ... ⇒B n-1 ⇒B n ⇒C explicable by means of the correct application of the rational logic rules. The quest for a proof is therefore a fundamental creative process considered as a transcendental mental function in searching for the structure of being. The existence of almost one derivation of C from A for a given theorem ⊨A⇒C, is guaranteed by the well-known Gödel's completeness theorem (1930): this theorem has mainly a psychological function because it does not suggest any operative or methodological indication about the search or individuation of the proof strategy as well as one of its possible derivations, this confirming the nature prevalently creative of it 9 . On the other hand, considering, for example, an arbitrary insight process, it is therefore plausible to think that the long unconscious work in finding a proof (mentioned, amongst others, by J. Hadamard and H.J. Poincaré 10 ) is owned to the (indivisible and homogeneous unity or) syncretic character of unconscious which has mainly an immediate unifying and multiple logic character 11 , impossible to the asymmetric (or conscious) thought. Indeed, following what is mentioned in [28, Chap. 1, Section 10], according to Poincaré the most insights spring out of an unexpected inner decisive inspiration often taking place in a moment in which the mind is very far from the solution to the problem under examination which has yet been, for a long time, inconclusively discussed and unconsciously incubated. It is as if, all the elements of this searched solution, put in movement from the previous conscious study (of the problem under examination), continue to mechanically (and unconsciously) roam within a sort of 'cerebral maze' until up when, suddenly, they finally find a road along which link themselves, in a continuous chain (that is, a derivation), from the hypotheses towards the thesis. Afterwards, Hadamard says as, amongst the infinite possible choices (namely, the above road), that is to say, amongst the infinite possible (unconscious) association of ideas (which pursue the solution), just our own unconscious seems to choose the one satisfying a kind of 'beauty criterion' (d'après P.A.M. Dirac) which is ruled by a certain instinctive sense of scientificartistic elegance. In turn, the latter is influenced by our scientific education (as said in [START_REF] Ageno | Le radiazioni e i loro effetti[END_REF]Chap. 1]), that is to say, it is just the method that will become an instinct, in a manner that it is impossible to explain in words. Maybe, this might be related with the continuous content exchange between explicit and implicit memories. On the other hand, following [START_REF] Bara | Scienza Cognitiva[END_REF], a syllogism is nothing but an explicitation process of the valid or interesting conclusions of what implicitly contained into the premises. Furthermore, taking into account what has been just said by Poincaré and Hadamard,Mario Ageno (in [28,Chap. 1]) adds that however only the (scientific) method cannot open the way to the finding of the solution to a problem if one does not learn to discovery as well new problems and to correctly formulate them.

Then, when one conducts a logic derivation of a mathematical proof, we essentially follow a bilogic process made by symmetric steps (which have a unifying and creative character in finding the various, not a priori given, intermediate terms B i i=1, ... ,n) and asymmetric steps (in applying the necessary logic tools and rules for the various partial elementary syllogistic inferences B i ⇒ B i+1 for each i); in these two inseparable types of thought, it is then important to consider their degree of more or less contemporaneity. Hence, the Matte Blanco bilogic process may be considered as one of the most suitable candidate in trying to explain the primary bases of a creative process, whence it follows the unescapable role (or influence) played by unconscious (or symmetric) thought in finding a new mathematical proof (which is not otherwise rationally deducible -for instance, by means of generalization, analogy, extension, reductio ad absurdum, etc 12 ), specially as concerns the affective-emotive aspects involved in it. The unavoidable presence of symmetric thought aspects also explains why, in certain cases, the new proof of a theorem is almost never perfect in its first initial form 13 , but it shall reach its perfect and correct (in a certain sense, definitive) form after the subsequent correction made upon the possible initial imperfections, that is, by elimination of any symmetric thought interference.

unconscious that assures, amongst other, the existence of opposite pairs of dialectic type and not of polar type, inasmuch the former reach a (Hegelian dialectic) synthesis' conclusion from the initial dual elements of the opposite pair, whereas the latter keep, into a dynamical tensional state, such opposite elements without reaching any their synthesis (see also [18]). Thus, it would also be possible trying to explain the above syncretic character by means of the well-known Pseudo Scoto Law (see [START_REF] Carruccio | Mondi della Logica[END_REF]) according to which, if a proposition and its negation (like in an opposite pair) contemporaneously subsist as true, then it is deductible every other possible proposition, so reaching to touch clear syncretic characters. 12 In this regards, it is fundamental taking into account the distinction between logic and mathematical processes according to Hermann Weyl (see [22, Chap. XII, Section 1]), the second ones corresponding to the creative processes here considered. From the various, reciprocal interaction between these two basic generative principles of an arbitrary mathematical construction, it follows a remarkable thought's line of the modern Mathematical Philosophy. 13 See the further, recent example given by the creative proof of the last Fermat's theorem by Andrew J. Wiles, with the collaboration of Richard Taylor, whose first form (given in the celebrated 1993 Cambridge lectures) had needed for some corrections (worked out upon the previous Cambridge version, just with the aid of his former PhD student Richard Taylor) in order that it were correct (last 1995 proof). Nevertheless, this detracts nothing to the exceptional initial creative work of Wiles and to the subsequent as many creative error corrections by Wiles and Taylor. In this regards, see the interesting survey paper [START_REF] Singh | La dimostrazione dell'ultimo teorema di Fermat[END_REF] and references therein.

In [START_REF] Hadamard | The Psychology of Invention in the Mathematical Field[END_REF], Hadamard has hence pointed out that the major part of the mathematical insights take place through images 14 and not through verbal processes. His conjecture is now also confirmed by the double codex theory due to W. Bucci (see [START_REF] Bucci | The dual code model and the interpretation of dreams[END_REF], [START_REF] Bucci | Dual coding: a cognitive model for psychoanalytic research[END_REF] and [13, Vol. 1, Chap. 5, Section 5.4]) and according to which, starting from the ideas of A. Paivio (see [13, Vol. 2, Chap. 5, Section 5.1]), there exist two equal rank codices, that verbal and the non-verbal one. The mature thought may be placed in both these codices. In particular, the non-verbal codex is that appointed to the emotional functions and to other holistic type of thoughts. It works by synchronous information through parallel multiple channels (hence following a synchronous logic). Therefore, we would be tempted to suggest that the asymmetric thought is ruled by an asynchronous logic, whereas the symmetric thought is mainly ruled by a synchronous logic. The brain perceives and works out the reality simultaneously by means of both codices, and they are continuously in reciprocal communication through bidirectional connections and continuous referential links. The thought by images is the primary (but not the unique one) and specific expression of complex emotions like desires, beliefs, expectations and other holistic sensory-motor experienced, representational and mathematical contents and others, which cannot be verbally expressed. It is evident that the Bucci's double codex theory may be closely correlated with the Matte Blanco's bilogic process and vice versa, at least from a historiographical and epistemological perspective.

Of such a theoretical system, herein we give only a few hints, possibly reserving us to study in-depth the thought of this Author, in its relationships with the mathematics, in further papers.

We recall that the above mentioned primary unconscious logic mechanisms were deduced by Freud mainly by two his clinical cases, precisely the case of the Rat Man (of 1909) and that of the Wolf Man(of 1914-1915), thanks to which Freud reached the discovery of the neurotic-obsessive disorders (see[START_REF]collection EDMA par Charles-Henri Favrod[END_REF]). Besides, from the Rat Man paper, Freud established some analogies between the neurosis mechanisms and the primitive mind (see[START_REF]collection EDMA par Charles-Henri Favrod[END_REF]).

According to this principle, the unconscious treats a single thing (individual, object, concept, etc) as it were a member, or an element, of a class which contains other members or elements; in turn, this class is considered as a subclass of another more general class, and so forth.

According to which, in the realm of unconscious, every relation is symmetric (just in the mathematical sense of this term).

It will also be interesting to discuss the essential difference among emotions, sentiments and affects -as, for instance, made by the notable recent work of the neuroscientist Antonio R. Damasio -and their possible role in Mathematics (see also next footnote), and this also taking into account other remarkable works of Matte-Blanco himself on the same subject.

This phenomenon can be identified in many historical cases of fundamental creative innovation: for instance, the celebrated Einstein's (as well as the main Riemannian) ideas on space-time, have been mainly based, at least in their initial theoretical

p(x) true[false] means that x has [does not have] the property expressed by the statement p, supposing that every element of A has, or does not have, such a property p.

In this regards, one of the most paradigmatic examples is given by the recent proof of Poincaré conjecture by Grigorij J. Perel'man, who has outlined it in three papers only without many formal details, between 2002 and 2003, but the experts, called to explicitate all the formal passages of the proof, later found that these papers already contained all the ideas need for constructing a complete proof of this geometrisation conjecture. For the relative validation, it has been necessary to explicitly deduce any elementary passage B i ⇒B i+1 involved in it, reaching to a complete proof of several hundred pages (more than six hundredsee[START_REF] Morgan | Ricci Flow and the Poincaré Conjecture[END_REF]), whilst the Author achieved it with few ones in an utter and inexplicable (if not at the intuitive level) creative manner. This is an epitome of the mathematical creative work.

On the other hand, Poincaré himself, in[START_REF] Poincaré | The Value of Science[END_REF], stated that ''in Mathematics, it is the intuition that discovers, whilst it is the logic that proves'', coherently with what we have here established. The philosophical thought of this Author is indeed very close to the ideas here exposed and based on Matte Blanco's work. Thereafter, I. Lakatos said (in [26, Vol. II]) that the mathematics grows up and develops just thanks to a main dialectic relationship between rigour (formal proofs) and intuition (preformal and postformal proofs). Furthermore, following[21, pp. 285-286], in an emblematic and explicit way, Federigo Enriques affirms as «such an extralogic dimension, called ''unconscious'', is powerfully present within the same mental processes. The knowledge acquisition does not wholly fall into the lucid consciousness and volition domain, but extends itself through unconscious and instinctive associations and links. At the same sources of the rational processes, it is present an ''original impulse'' which strongly acts in the infancy of the individual and in that of the humankind; in short, the development of pure science embeds its roots into an affective disposition». Finally, Giulio Vivanti, in [27, Preface, p. VII], in regards to the creative Weiesrtarss' approach to analytic functions, states that «[with this method] one replaces to the calculus -which proves, but doesn't illuminate -the reasoning». Finally, it would also be interesting to see what Krzysztof Maurin states in[START_REF] Maurin | The Riemann Legacy[END_REF] Foreword] about the role played by unconscious (see above all [29, Foreword, pp. xxi-xxii]) in the creative thought, taking, as main model, the work achieved by Riemann, so confirming most of what has been said in this paper.

In[START_REF] Iurato | On Jung and Lévi-Strauss Unconscious: A Brief Comparison[END_REF], we have taken into account some similar structural aspects of the yet distinct notions of unconscious according to C. Lévi-Strauss and C.G. Jung. The first Author considers a notion of unconscious meant as the place from which originates every form of possible thought, that is to say, it is considered as the 'place of every science', whereas the second Author considers a collective


Andrew Reynolds

Radu Iosif

Cristina Serban

Tim King

A Decision Procedure for Separation Logic in SMT

come

Introduction

Separation Logic (SL) [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF] is a logical framework for describing dynamically allocated mutable data structures generated by programs that use pointers and low-level memory allocation primitives. The logics in this framework are used by a number of academic (Space Invader [START_REF] Berdine | Shape analysis for composite data structures[END_REF]), and industrial (Infer [START_REF] Calcagno | Infer: An automatic program verifier for memory safety of c programs[END_REF]) tools for program verification. The main reason for choosing to work within the SL framework is its ability to provide compositional proofs of programs, based on the principle of local reasoning: analyzing different parts of the program (e.g. functions, threads), that work on disjoint parts of the heap, and combining the analysis results a posteriori.

The main ingredients of SL are: (i) the separating conjunction φ * ψ, which asserts that φ and ψ hold for separate portions of the memory (heap), and (ii) the magic wand ϕ -- * ψ, which asserts that any extension of the heap by a disjoint heap that satisfies ϕ must satisfy ψ. Consider, for instance, a memory configuration (heap), in which two cells are allocated, and pointed to by the program variables x and y, respectively, where the x cell has an outgoing selector field to the y cell, and vice versa. The heap can be split into two disjoint parts, each containing exactly one cell, and described by an atomic proposition x → y and y → x, respectively. Then the entire heap is described by the formula x → y * y → x, which reads "x points to y and, separately, y points to x".

The expressive power of SL comes with the inherent difficulty of automatically reasoning about the satisfiability of its formulae, as required by push-button program analysis tools. Indeed, SL becomes undecidable in the presence of first-order quantification, even when the fragment uses only points-to predicates, without the separating conjunction or the magic wand [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF]. Moreover, the quantifier-free fragment with no data constraints, using only points-to predicates x → (y, z), where x, y and z are interpreted as memory addresses, is PSPACE-complete, due to the implicit quantification over memory partitions, induced by the semantics of the separation logic connectives [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF]. This paper presents a decision procedure for quantifier-free SL which is entirely parameterized by a base theory T of heap locations and data, i.e. the sorts of memory addresses and their contents can be chosen from a large variety of available theories handled by Satisfiability Modulo Theories (SMT) solvers, such as linear integer (real) arithmetic, strings, sets, uninterpreted functions, etc. Given a base theory T , we call SL(T ) the set of separation logic formulae built on top of T , by considering points-to predicates and the separation logic connectives.

Contributions First, we show that the satisfiability problem for the quantifier-free fragment of SL(T ) is PSPACE-complete, provided that the satisfiability of the quantifierfree fragment of the base theory T is in PSPACE. Our method is based on a semanticspreserving translation of SL(T ) into second-order T formulae with quantifiers over a domain of sets and uninterpreted functions, whose cardinality is polynomially bound by the size of the input formula. For the fragment of T formulae produced by the translation from SL(T ), we developed a lazy quantifier instantiation method, based on counterexample-driven refinement. We show that the quantifier instantiation algorithm is sound, complete and terminates on the fragment under consideration. We present our algorithm for the satisfiability of quantifier-free SL(T ) logics as a component of a DPLL(T ) architecture, which is widely used by modern SMT solvers. We have implemented the technique as a subsolver of the CVC4 SMT solver [START_REF] Barrett | CAV'11[END_REF] and carried out experiments that handle non-trivial examples quite effectively. Applications of our procedure include:

1. Integration within theorem provers for SL with inductive predicates. Most inductive provers for SL use a high-level proof search strategy relying on a separate decision procedure for entailments in the non-inductive fragment, used to simplify the proof obligations, by discharging the non-inductive parts of both left-and right-hand sides, and attain an inductive hypothesis [START_REF] Brotherston | A generic cyclic theorem prover[END_REF]. Due to the hard problem of proving entailments in the non-inductive fragment of SL, these predicates use very simple non-inductive formulae (a list of points-to propositions connected with separating conjunction), for which entailments are proved by syntactic substitutions and matching. Our work aims at extending the language of inductive SL solvers, by outsourcing entailments in a generic non-inductive fragment to a specialized procedure. To this end, we conducted experiments on several entailments corresponding to finite unfoldings of inductive predicates used in practice (Section 6). 2. Use as back-end of a bounded model checker for programs with pointer and data manipulations, based on a complete weakest precondition calculus that involves the magic wand connective [START_REF] Ishtiaq | BI as an assertion language for mutable data structures[END_REF]. To corroborate this hypothesis, we tested our procedure on verification conditions automatically generated by applying the weakest precondition calculus described in [START_REF] Ishtiaq | BI as an assertion language for mutable data structures[END_REF] to several program fragments (Section 6).

Related Work

The study of the algorithmic properties of Separation Logic [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF] has produced an extensive body of literature over time. We need to distinguish between SL with inductive predicates and restrictive non-inductive fragments, and SL without inductive predicates, which is the focus of this paper.

Regarding SL with fixed inductive predicates, Perez and Rybalchenko [START_REF] Navarro Pérez | Separation logic + superposition calculus = heap theorem prover[END_REF] define a theorem proving framework relying on a combination of SL inference rules dealing with singly-linked lists only, and a superposition calculus dealing with equalities and aliasing between variables. Concerning SL with generic user-provided inductive predicates, the theorem prover Cyclist [START_REF] Brotherston | A generic cyclic theorem prover[END_REF] builds entailment proofs using a sequent calculus. More recently, the tool Slide [START_REF] Iosif | Slide: Separation logic with inductive definitions[END_REF] reduces the entailment between inductive predicates to an inclusion between tree automata. The great majority of these inductive provers focus on applying induction strategies efficiently, and consider a very simple fragment of noninductive SL formulae, typically conjunctions of equalities and disequalities between location variables and separated points-to predicates, without negations or the magic wand. On a more general note, the tool Spen [START_REF] Enea | On automated lemma generation for separation logic with inductive definitions[END_REF] considers also arithmetic constraints between the data elements in the memory cells, but fixes the shape of the user-defined predicates.

The idea of applying SMT techniques to decide satisfiability of SL formulae is not new. In their work, Piskac, Wies and Zufferey translate from SL with singly-linked list segments [START_REF] Piskac | Automating separation logic using SMT[END_REF] and trees [START_REF] Piskac | Automating separation logic with trees and data[END_REF], respectively, into first-order logics (Grass and Grit) that are decidable in NP. The fragment handled in this paper is incomparable to the logics Grass [START_REF] Piskac | Automating separation logic using SMT[END_REF] and Grit [START_REF] Piskac | Automating separation logic with trees and data[END_REF]. On one hand, we do not consider predicates defining recursive data structures, such as singly-linked lists. On the other hand, we deal with the entire quantifier-free fragment of SL, including arbitrary nesting of the magic wand, separating conjunction and classical boolean connectives. As a result, the decision problem we consider is PSPACE-complete, due to the possibility of arbitrary nesting of the boolean and SL connectives. To the best of our knowledge, our implementation is also the first to enable theory combination involving SL, in a fine-grained fashion, directly within the DPLL(T ) loop.

The first theoretical results on decidability and complexity of SL without inductive predicates were given by Calcagno, Yang and O'Hearn [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF]. They show that the quantifier-free fragment of SL without data constraints is PSPACE-complete by an argument that enumerates a finite (yet large) set of heap models. Their argument shows also the difficulty of the problem, however it cannot be directly turned into an effective decision procedure, because of the ineffectiveness of model enumeration. Building up on this small model property for the quantifier-free fragment of SL, a translation to first-order logic over uninterpreted sorts with empty signature is described in [START_REF] Calcagno | From separation logic to first-order logic[END_REF]. This translation is very similar to our translation to multi-sorted second-order logic, the main difference being using bounded tuples instead of sets of bounded cardinality. It also provides a decision procedure, though no implementation is available for comparison. A more elaborate tableau-based decision procedure is described by Méry and Galmiche [START_REF] Galmiche | Tableaux and resource graphs for separation logic[END_REF]. This procedure generates verification conditions on-demand, but here no data constraints are considered, either.

Our procedure relies on a decision procedure for quantifier-free parametric theory of sets and on-demand techniques for quantifier instantiation. Decision procedures for the theory of sets in SMT are given in [START_REF] Suter | Sets with cardinality constraints in satisfiability modulo theories[END_REF][START_REF] Bansal | Decision Procedures for Finite Sets with Cardinality and Local Theory Extensions[END_REF]. Techniques for model-driven quantifier instantiation were introduced in the context of SMT in [START_REF] Ge | Complete instantiation for quantified formulas in satisfiability modulo theories[END_REF], and have been developed recently in [START_REF] Reynolds | Counterexample guided quantifier instantiation for synthesis in CVC4[END_REF][START_REF] Bjørner | Playing with quantified satisfaction[END_REF].

Preliminaries

We consider formulae in multi-sorted first-order logic, over a signature Σ consisting of a countable set of sort symbols and a set of function symbols. We assume that signatures always include a boolean sort Bool with constants and ⊥ denoting true and false respectively, and that each sort σ is implicitly equipped with an equality predicate ≈ over σ × σ. Moreover, we may assume without loss of generality that equality is the only predicate belonging to Σ, since we can model other predicate symbols as function symbols with return sort Bool4 .

We consider a set Var of first-order variables, with associated sorts, and denote by ϕ(x) the fact that the free variables of the formula ϕ belong to x ⊆ Var. Given a signature Σ, well-sorted terms, atoms, literals, and formulae are defined as usual, and referred to respectively as Σ-terms. We denote by φ[ϕ] the fact that ϕ is a subformula (subterm) of φ and by φ[ψ/ϕ] the result of replacing ϕ with ψ in φ. We write ∀x.ϕ to denote universal quantification over variable x, where x occurs as a free variable in ϕ. If x = x 1 , . . . , x n is a tuple of variables, we write ∀x ϕ as an abbreviation of ∀x 1 • • • ∀x n ϕ. We say that a Σ-term is ground if it contains no free variables. We assume that Σ contains an if-thenelse operator ite(b, t, u), of sort Bool × σ × σ → σ, for each sort σ, that evaluates to t if b is true, and to u, otherwise.

A Σ-interpretation I maps: (i) each set sort symbol σ ∈ Σ to a non-empty set σ I , the domain of σ in I, (ii

) each function symbol f ∈ Σ of sort σ 1 × . . . × σ n → σ to a total function f I of sort σ I 1 × . . . × σ I n → σ I if n > 0,
and to an element of σ I if n = 0, and (iii) each variable x ∈ x to an element of σ I

x , where σ x is the sort symbol associated with x. We denote by t I the interpretation of a term t induced by the mapping I. The satisfiability relation between Σ-interpretations and Σ-formulae, written I | = ϕ, is defined inductively, as usual. We say that I is a model of ϕ if I | = ϕ.

A first-order theory is a pair T = (Σ, I) where Σ is a signature and I is a nonempty set of Σ-interpretations, the models of T . For a formula ϕ, we denote by

[[ϕ]] T = {I ∈ I | I | = ϕ} its set of T -models. A Σ-formula ϕ is T -satisfiable if [[ϕ]] T ∅, and T - unsatisfiable otherwise. A Σ-formula ϕ is T -valid if [[ϕ]] T = I, i.e. if ¬ϕ is T -unsatisfiable. A formula ϕ T -entails a Σ-formula ψ, written ϕ | = T ψ, if every model of T that satisfies ϕ also satisfies ψ. The formulae ϕ and ψ are T -equivalent if ϕ | = T ψ and ψ | = T ϕ, and equisatisfiable (in T ) if ψ is T -satisfiable if and only if ϕ is T -satisfiable.
Furthermore, formulas ϕ and ψ are equivalent (up to k) if they are satisfied by the same set of models (when restricted to the interpretation of variables k). The T -satisfiability problem asks, given a Σ-formula ϕ, whether [[ϕ]] T ∅, i.e. whether ϕ has a T -model.

Separation Logic

In the remainder of the paper we fix a theory T = (Σ, I), such that the T -satisfiability for the language of quantifier-free boolean combinations of equalities and disequalties between Σ-terms is decidable. We fix two sorts Loc and Data from Σ, with no restriction other than the fact that Loc is always interpreted as a countably infinite set. We refer to Separation Logic for T , written SL (T ), as the set of formulae generated by the syntax:

φ := t ≈ u | t → u | emp | φ 1 * φ 2 | φ 1 - - * φ 2 | φ 1 ∧ φ 2 | ¬φ 1
where t and u are well-sorted Σ-terms and that for any atomic proposition t → u, t is of sort Loc and u is of sort Data. Also, we consider that Σ has a constant nil of sort Loc, with the meaning that t → u never holds when t ≈ nil. In the following, we write φ ∨ ψ for ¬(¬φ ∧ ¬ψ) and φ ⇒ ψ for ¬φ ∨ ψ.

Given an interpretation I, a heap is a finite partial mapping h : Loc I fin Data I . For a heap h, we denote by dom(h) its domain. For two heaps h 1 and h 2 , we write

h 1 #h 2 for dom(h 1 ) ∩ dom(h 2 ) = ∅ and h = h 1 h 2 for h 1 #h 2 and h = h 1 ∪ h 2 .
For an interpretation I, a heap h : Loc I fin Data I and a SL(T ) formula φ, we define the satisfaction relation I, h | = SL φ inductively, as follows:

I, h | = SL emp ⇐⇒ h = ∅ I, h | = SL t → u ⇐⇒ h = {(t I , u I )} and t I ≈ nil I I, h | = SL φ 1 * φ 2 ⇐⇒ ∃h 1 , h 2 . h = h 1 h 2 and I, h i | = SL φ i , for all i = 1, 2 I, h | = SL φ 1 - - * φ 2 ⇐⇒ ∀h if h #h and I, h | = SL φ 1 then I, h h | = SL φ 2
The satisfaction relation for the equality atoms t ≈ u and the Boolean connectives ∧, ¬ are the classical ones from first-order logic. In particular t ≈ t is always true, denoted by , for any given heap. The (SL, T )-satisfiability problem asks, given an SL formula ϕ, if there is a T -model I such that (I, h) | = SL ϕ for some heap h.

In this paper we tackle the (SL, T )-satisfiability problem, under the assumption that the quantifier-free data theory T = (Σ, I) has a decidable satisfiability problem for constraints involving Σ-terms. It has been proved [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF] that the satisfiability problem is PSPACE-complete for the fragment of separation logic in which Data is interpreted as the set of pairs of sort Loc. We generalize this result to any theory whose satisfiability problem, for the quantifier-free fragment, is in PSPACE. This is, in general, the case of most SMT theories, which are typically in NP, such as the linear arithmetic of integers and reals, possibly with sets and uninterpreted functions, etc.

Reducing SL (T ) to Multisorted Second-Order Logic

It is well-known [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF] that separation logic cannot be formalized as a classical (unsorted) first-order theory, for instance, due to the behavior of the * connective, that does not comply with the standard rules of contraction φ ⇒ φ * φ and weakening φ * ϕ ⇒ φ5 . The basic reason is that φ * ϕ requires that φ and ϕ hold on disjoint heaps. Analogously, φ -- * ϕ holds on a heap whose extensions, by disjoint heaps satisfying φ, must satisfy ϕ. In the following, we leverage from the expressivity of multi-sorted first-order theories and translate SL(T ) formulae into quantified formulae in the language of T , assuming that T subsumes a theory of sets and uninterpreted functions.

The integration of separation logic within the DPLL(T) framework [START_REF] Ganzinger | Dpll(t): Fast decision procedures[END_REF] requires the input logic to be presented as a multi-sorted logic. To this end, we assume, without loss of generality, the existence of a fixed theory T = (Σ, I) that subsumes a theory of sets Set(σ) [START_REF] Bansal | Decision Procedures for Finite Sets with Cardinality and Local Theory Extensions[END_REF], for any sort σ of set elements, whose functions are the union ∪, intersection ∩ of sort Set(σ) × Set(σ) → Set(σ), singleton {.} of sort σ → Set(σ) and emptyset ∅ of sort Set(σ). We write ⊆ as a shorthand for ∪ ≈ and t ∈ for {t} ⊆ , for any terms and of sort Set(σ) and t of sort σ. The interpretation of the functions in the set theory is the classical (boolean) one.

Also, we assume that Σ contains infinitely many function symbols pt, pt , . . . ∈ Σ of sort Loc → Data, where Loc and Data are two fixed sorts of T , such that for any interpretation I ∈ I, Loc I is an infinite countable set.

The main idea is to express the atoms and connectives of separation logic in multisorted second-order logic by means of a transformation, called labeling, which introduces (i) constraints over variables of sort Set(Loc) and (ii) terms over uninterpreted points-to functions of sort Loc → Data. We describe the labeling transformation using judgements of the form φ [ , pt], where φ is a SL(T ) formula, = 1 , . . . , n is a tuple of variables of sort Set(Loc) and pt = pt 1 , . . . , pt n is a tuple of uninterpreted function symbols occurring under the scopes of universal quantifiers. To ease the notation, we write and pt instead of the singleton tuples and pt . In the following, we also write for

1 ∪ . . . ∪ n , ∩ for ∩ 1 , . . . , ∩ n , • for , 1 , . . . , n and ite(t ∈ , pt(t) = u) for ite(t ∈ 1 , pt 1 (t) = u, ite(t ∈ 2 , pt 2 (t) = u, . . . , ite(t ∈ n , pt n (t) = u, ) . . .)).
Intuitively, a labeled formula φ [ , pt] says that it is possible to build, from any of its satisfying interpretations I, a heap h such that

I, h | = SL φ, where dom(h) = I 1 ∪ . . . ∪ I n and h = pt I 1 ↓ I 1 ∪ . . . ∪ pt I n ↓ I n 6
. More precisely, a variable i defines a slice of the domain of the heap, whereas the restriction of pt i to (the interpretation of) i describes the heap relation on that slice. Observe that each interpretation of and pt, such that I i ∩ I j = ∅, for all i j, defines a unique heap.

First, we translate an input SL(T ) formula φ into a labeled second-order formula, with quantifiers over sets and uninterpreted functions, defined by the rewriting rules in Figure 1. A labeling step φ[ϕ] =⇒ φ[ψ/ϕ] applies if ϕ and ψ match the antecedent and consequent of one of the rules in Figure 1, respectively. It is not hard to show that this rewriting system is confluent, and we denote by φ⇓ the normal form of φ with respect to the application of labeling steps. Example 1. Consider the SL(T ) formula (x → a -- * y → b) ∧ emp. The reduction to second-order logic is given below:

(φ * ψ) [ , pt] ¬∀ 1 ∀ 2 . ¬( 1 ∩ 2 ≈ ∅ ∧ 1 ∪ 2 ≈ ∧ φ [ 1 ∩ , pt] ∧ ψ [ 2 ∩ , pt]) (φ ∧ ψ) [ , pt] φ [ , pt] ∧ ψ [ , pt] (φ - - * ψ) [ , pt] ∀ ∀pt . ( ∩ ( ) ≈ ∅ ∧ φ [ , pt ]) ⇒ ψ [ • , pt • pt] (¬φ) [ , pt] ¬(φ [ , pt]) t → u [ , pt] ≈ {t} ∧ ite(t ∈ , pt(t) ≈ u) ∧ t ≈ nil emp [ , pt] ≈ ∅ ϕ [ , pt] ϕ ϕ is pure
((x → a - - * y → b) ∧ emp) [ , pt] =⇒ * ≈ ∅ ∧ ∀ ∀pt . ∩ ≈ ∅ ∧ ≈ {x} ∧ ite(x ∈ , pt (x) ≈ a, ) ∧ x ≈ nil ⇒ ∪ ≈ {y} ∧ ite(y ∈ , pt (y) ≈ b, ite(y ∈ , pt(y) ≈ b, )) ∧ y ≈ nil
The following lemma reduces the (SL, T )-satisfiability problem to the satisfiability of a quantified fragment of the multi-sorted second-order theory T , that contains sets and uninterpreted functions. For an interpretation I, a variable x and a value s ∈ σ I

x , we denote by I[x ← s] the extension of I which maps x into s and behaves like I for all other symbols. We extend this notation to tuples x = x 1 , . . . , x n and s = s 1 , . . . , s n and write

I[x ← s] for I[x 1 ← s 1 ] . . . [x n ← s n ].
For a tuple of heaps h = h 1 , . . . , h n we write dom(h) for dom(h 1 ), . . . , dom(h n ) .

Lemma 1. Given a SL(T ) formula ϕ and tuples = 1 , . . . , n and pt = pt 1 , . . . , pt n for n > 0, for any interpretation I of T and any heap h: I, h | = SL ϕ if and only if

1. for all heaps h = h 1 , . . . , h n such that h = h 1 . . . h n , 2. for all heaps h = h 1 , . . . ,

h n such that h 1 ⊆ h 1 , . . . , h n ⊆ h n , we have I[ ← dom(h)][pt ← h ] | = T ϕ [ , pt]⇓ .
Although, in principle, satisfiability is undecidable in the presence of quantifiers and uninterpreted functions, the result of the next section strengthens this reduction, by adapting the labeling rules for * and -- * (Figure 1) to use bounded quantification over finite (set) domains.

A Reduction of SL (T ) to Quantifiers Over Bounded Sets

In the previous section, we have reduced any instance of the (SL, T )-satisfiability problem to an instance of the T -satisfiability problem in the second-order multi-sorted theory T which subsumes the theory Set(Loc) and contains several quantified uninterpreted function symbols of sort Loc → Data. A crucial point in the translation is that the only quantifiers occurring in T are of the forms ∀ and ∀pt, where is a variable of sort Set(Loc) and pt is a function symbol of sort Loc → Data. Leveraging from a small model property for SL over the data domain Data = Loc × Loc [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF], we show that it is sufficient to consider only the case when the quantified variables range over a bounded domain of sets. In principle, this allows us to eliminate the universal quantifiers by replacing them with finite conjunctions and obtain a decidability result based on the fact that the quantifier-free theory T with sets and uninterpreted functions is decidable. Since the cost of a-priori quantifier elimination is, in general, prohibitive, in the next section we develop an efficient lazy quantifier instantiation procedure, based on counterexample-driven refinement.

For reasons of self-containment, we quote the following lemma [START_REF] Yang | Local Reasoning for Stateful Programs[END_REF] and stress the fact that its proof is oblivious of the assumption Data = Loc × Loc on the range of heaps. Given a formula φ in the language SL(T ), we first define the following measure:

|φ * ψ| = |φ| + |ψ| |φ - - * ψ| = |ψ| |φ ∧ ψ| = max(|φ|, |ψ|) |¬φ| = |φ| |t → u| = 1 |emp| = 1 |φ| = 0 if φ is a Σ-formula
Intuitively, |φ| gives the maximum number of invisible locations in the domain of a heap h, that are not in the range of I and which can be distinguished by φ. For instance, if Then, for any heap h, we have

I, h | = SL
I, h | = SL φ iff I, h | = SL φ, for any heap h such that: -dom(h ) ⊆ L ∪ Pt(φ) I , -for all ∈ dom(h ), h ( ) ∈ Pt(φ) I ∪ {v}
Based on the fact that the proof of Lemma 2 [START_REF] Yang | Local Reasoning for Stateful Programs[END_REF] does not involve reasoning about data values, other than equality checking, we refine our reduction from the previous section, by bounding the quantifiers to finite sets of constants of known size. To this end, we assume the existence of a total order on the (countable) set of constants in Σ of sort Loc, disjoint from any Σ-terms that occur in a given formula φ, and define Bnd(φ,C) = {c m+1 , . . . , c m+|φ| }, where m = max{i | c i ∈ C}, and m = 0 if C = ∅. Clearly, we have Pt(φ) ∩ Bnd(φ,C) = ∅ and also C ∩ Bnd(φ,C) = ∅, for any C and any φ.

We now consider labeling judgements of the form ϕ [ , pt,C], where C is a finite set of constants of sort Loc, and modify all the rules in Figure 1 Observe that the result of the labeling process is a formula in which all quantifiers are of the form ∀ 1 . . .

∀ n ∀pt 1 . . . ∀pt n . n i=1 i ⊆ L i ∧ n i=1 pt i ⊆ L i × D i ⇒ ψ( , pt)
, where L i 's and D i 's are finite sets of terms, none of which involves quantified variables, and ψ is a formula in the theory T with sets and uninterpreted functions. Moreover, the labeling rule for φ -- * ψ [ , pt,C] uses a fresh constant d that does not occur in φ or ψ. Example 2. We revisit below the labeling of the formula (x → a -- * y → b) ∧ emp:

φ * ψ [ , pt,C] ¬∀ 1 ∀ 2 . 1 ∪ 2 ⊆ C ∪ Pt(φ * ψ) ⇒ ¬( 1 ∩ 2 ≈ ∅ ∧ 1 ∪ 2 ≈ ∧ φ [ 1 ∩ , pt,C] ∧ ψ [ 2 ∩ , pt,C]) φ - - * ψ [ , pt,C] ∀ ∀pt . ⊆ C ∪ Pt(φ - - * ψ) ∧ pt ⊆ (C ∪ Pt(φ - - * ψ)) × (Pt(φ - - * ψ) ∪ {d}) ⇒ ( ∩ ( ) ≈ ∅ ∧ φ [ , pt ,C ]) ⇒ ψ [ • , pt • pt,C] C = Bnd(φ ∧ ψ,C) d Pt(φ - - * ψ)
((x → a - - * y → b) ∧ emp) [ , pt,C] =⇒ * ≈ ∅ ∧ ∀ ⊆ {x, y, a, b, c} ∀pt ⊆ {x, y, a, b, c} × {x, y, a, b, d}) . ∩ ≈ ∅ ∧ ≈ {x} ∧ ite(x ∈ , pt (x) ≈ a, ) ∧ x ≈ nil ⇒ ∪ ≈ {y} ∧ ite(y ∈ , pt (y) ≈ b, ite(y ∈ , pt(y) ≈ b, )) ∧ y ≈ nil .
where Pt((x → a -- * y → b) ∧ emp) = {x, y, a, b}. Observe that the constant c was introduced by the bounded quantifier labeling of the term x → a -- * y → b.

The next lemma states the soundness of the translation of SL(T ) formulae in a fragment of T that contains only bounded quantifiers, by means of the rules in Figure 2.

Lemma 3. Given a formula ϕ in the language SL(T ), for any interpretation I of T , let L ⊆ Loc I \ Pt(ϕ) I be a set of locations such that | |L| | = |ϕ| and v ∈ Data I \ Pt(ϕ) I be a data value. Then there exists a heap h such that I, h | = SL ϕ iff there exist heaps h = h 1 , . . . , h n and h = h 1 , . . . , h n such that:

1. for all 1 ≤ i < j ≤ n, we have h i #h j , 2. for all 1 ≤ i ≤ n, we have h i ⊆ h i and 3.

I[ ← dom(h )][pt ← h ][C ← L][d ← v] | = T ϕ [ , pt,C]⇓ .

A Counterexample-Guided Approach for Solving SL (T ) Inputs

This section presents a novel decision procedure for the (SL, T )-satisfiability of the set of quantifier-free SL (T ) formulae ϕ. To this end, we present an efficient decision procedure for the T -satisfiability of (ϕ [ , pt,C])⇓, obtained as the result of the transformation described in Section 4. The main challenge in doing so is treating the universal quantification occurring in (ϕ [ , pt,C])⇓. As mentioned, the key to decidability is that all quantified formulae in (ϕ [ , pt,C])⇓ are equivalent to formulas of the form ∀x.( x ⊆ s) ⇒ ϕ, where each term in the tuple s is a finite set (or product of sets) of ground Σ-terms. For brevity, we write ∀x ⊆ s.ϕ to denote a quantified formula of this form. While such formulae are clearly equivalent to a finite conjunction of instances, the cost of constructing these instances is in practice prohibitively expensive. Following recent approaches for handling universal quantification [START_REF] Ge | Complete instantiation for quantified formulas in satisfiability modulo theories[END_REF][START_REF] Reynolds | Counterexample guided quantifier instantiation for synthesis in CVC4[END_REF][START_REF] Bjørner | Playing with quantified satisfaction[END_REF][START_REF] Reynolds | An instantiation-based approach for solving quantified linear arithmetic[END_REF], we use a counterexample-guided approach for choosing instances of quantified formulae that are relevant to the satisfiability of our input. The approach is based on an iterative procedure maintaining an evolving set of quantifier-free Σ-formulae Γ, which is initially a set of formulae obtained from ϕ by a purification step, described next. We associate with each closed quantified formula a boolean variable A, called the guard of ∀x.ϕ, and a (unique) set of Skolem symbols k of the same sort as x. We write (A, k) ∀x.ϕ to denote that A and k are associated with ∀x.ϕ. For a set of formulae Γ, we write Q(Γ) to denote the set of quantified formulae whose guard occurs within a formula in Γ. We write ψ for the result of replacing in ψ all closed quantified formulae (not occurring beneath other quantifiers in ψ) with their corresponding guards. Conversely, we write Γ to denote the result of replacing all guards in Γ by the quantified formulae they are associated with. Then ψ * denotes the smallest set of Σ-formulae: solve T (Γ):

1. If Γ is T -unsatisfiable, return "unsat", else let I be a T -model of Γ. 2. If Γ, A | = T ψ[k/x] for all ∀x.ψ ∈ Q(Γ), where (A, k) ∀x.ψ and A I = , return "sat", else let J be a T -model of Γ ∪ {A, ¬ ψ[k/x] } for some ≺ Γ,I -minimal ∀x ⊆ s.ψ,
where (A, k) ∀x ⊆ s.ψ. 3. Let t be a vector of terms, such that t ⊆ s, and

t J = k J . Return solve T ( Γ ∪ A ⇒ ψ[t/x] * ).
ψ ∈ ψ * (¬A ⇒ ¬ϕ[k/x] ) ∈ ψ * if ∀x.ϕ ∈ Q( ψ * ) where (A, k) ∀x.ϕ.
In other words, ψ * contains clauses that witness the negation of each universally quantified formula occurring in ψ. It is easy to see that if ψ is a Σ-formula possibly containing quantifiers, then ψ * is a set of quantifier-free Σ-formulae, and if all quantified formulas in ψ are of the form ∀x ⊆ s.ϕ mentioned above, then all quantified formulas in Q( ψ * ) are also of this form.

Example 3. If ψ is the formula ∀x.(P(x) ⇒ ¬∀y.R(x, y)), then ψ * is the set:

{A 1 , ¬A 1 ⇒ ¬(P(k 1 ) ⇒ A 2 ), ¬A 2 ⇒ ¬R(k 1 , k 2 )}
where (A 1 , k 1 ) ∀x.(P(x) ⇒ ¬∀y.R(x, y)) and (A 2 , k 2 ) ∀y.R(k 1 , y).

Our algorithm solve SL(T) for determining the (SL, T )-satisfiability of input ϕ is given in Figure 3. It first constructs the set C based on the value of |ϕ|, which it computes by traversing the structure of ϕ. It then invokes the subprocedure solve T on the set (ϕ [ , pt,C])⇓ * where and pt are fresh free symbols.

At a high level, the recursive procedure solve T takes as input a (quantifier-free) set of T -formulae Γ, where Γ is T -unsatisfiable if and only if (ϕ [ , pt,C])⇓ is. On each invocation, solve T will either (i) terminate with "unsat", in which case ϕ is Tunsatisfiable, (ii) terminate with "sat", in which case ϕ is T -satisfiable, or (iii) add the set corresponding to the purification of the instance A ⇒ ψ[t/x] * to Γ and repeats.

In more detail, in Step 1 of the procedure, we determine the T -satisfiability of Γ using a combination of a satisfiability solver and a decision procedure for T 7 . If Γ is T -unsatisfiable, since Γ is T -entailed by Γ , we may terminate with "unsat". Otherwise, there is a T -model I for Γ and T . In Step 2 of the procedure, for each A that is interpreted to be true by I, we check whether Γ ∪ {A} T -entails ψ[k/x] for fresh free constants k, which can be accomplished by determining whether Γ ∪ {A, ¬ ψ[k/x] } is T -unsatisfiable. If this check succeeds for a quantified formula ∀x.ψ, the algorithm has established that ∀x.ψ is entailed by Γ. If this check succeeds for all such quantified formulae, then Γ is equivalent to Γ , and we may terminate with "sat". Otherwise, let Q + I (Γ) be the subset of Q(Γ) for which this check did not succeed. We call this the set of active quantified formulae for (I, Γ). We consider an active quantified formula that is minimal with respect to the relation ≺ Γ,I over Q(Γ), where:

ϕ ≺ Γ,I ψ if and only if ϕ ∈ Q( ψ * ) ∩ Q + I (Γ)
By this ordering, our approach considers innermost active quantified formulae first. Let ∀x.ψ be minimal with respect to ≺ Γ,I , where (A, k) ∀x.ψ. Since Γ, A does not T -entail ψ[k/x] , there must exist a model J for Γ ∪ { ¬ψ[k/x] } where A J = . In Step 3 of the procedure, we choose a tuple of terms t = (t 1 , . . . , t n ) based on the model J, and add to Γ the set of formulae obtained by purifying A ⇒ ψ[t/x], where A is the guard of ∀x ⊆ s.ψ. Assume that s = (s 1 , . . . , s n ) and recall that each s i is a finite union of ground Σ-terms. We choose each t such that t i is a subset of s i for each i = 1, . . . n, and t J = k J . These two criteria are the key to the termination of the algorithm: the former ensures that only a finite number of possible instances can ever be added to Γ, and the latter ensures that we never add the same instance more than once.

Theorem 1. For all SL (T ) formulae ϕ, solve SL(T) (ϕ):

1. Answers "unsat" only if ϕ is (SL, T )-unsatisfiable. 2. Answers "sat" only if ϕ is (SL, T )-satisfiable.

Terminates.

By Theorem 1, solve SL(T) is a decision procedure for the (SL, T )-satisfiability of the language of quantifier-free SL (T ) formulae. The following corollary gives a tight complexity bound for the (SL, T )-satisfiability problem.

Corollary 1. The (SL, T )-satisfiability problem is PSPACE-complete for any theory T whose satisfiability (for the quantifier-free fragment) is in PSPACE.

In addition to being sound and complete, in practice, the approach solve SL(T) terminates in much less time that its theoretical worst-case complexity, given by the above corollary. This fact is corroborated by our evaluation of our prototype implementation of the algorithm, described in Section 6, and in the following example. and pt of sorts Set(Loc) and Loc → Data respectively. The formula (ϕ [ , pt,C])⇓ is ≈ ∅ ∧ ∀ 4 ∀pt .ψ ∧ y ≈ nil, where after simplification ψ is:

ψ 4 ≡ ( 4 ⊆ {y, 0, 1, c} ∧ pt ⊆ {y, 0, 1, c} × {y, 0, 1, d}) ⇒ ( 4 ∩ ≈ ∅ ∧ 4 ≈ {y} ∧ pt (y) ≈ 0 ∧ y ≈ nil) ⇒ ( 4 ∪ ≈ {y} ∧ ite(y ∈ 4 , pt (y) ≈ 1, pt(y) ≈ 1) ∧ y ≈ nil) Let (A 4 , (k 1 , k 2 )) ∀ 4 ∀pt .ψ 4 .
We call the subprocedure solve T on Γ 0 , where:

Γ 0 ≡ (ϕ [ , pt,C])⇓ * ≡ { ≈ ∅ ∧ A 4 ∧ y ≈ nil, ¬A 4 ⇒ ¬ψ 4 [k 1 , k 2 / 4 , pt ]}.
The set Γ 0 is T -satisfiable with a model I 0 where A

I 0 4 = .
Step 2 of the procedure determines a model J for

Γ 0 ∪ {A 4 , ¬ψ 4 [k 1 , k 2 / 4 , pt ]}.
Let t 1 be {y}, where we know t J 1 = k J 1 since J must satisfy k 1 ≈ {y} as a consequence of ¬ψ 4 [k 1 , k 2 / 4 , pt ]. Let t 2 be a well-sorted subset of {y, 0, 1, c} × {y, 0, 1, d} such that t J 2 = k J 2 . Such a subset exists since J satisfies k 2 ⊆ {y, 0, 1, c} × {y, 0, 1, d}. Notice that t 2 (y) J = 0 J since J must satisfy k 2 (y) ≈ 0. Step 3 of the procedure recursively invokes solve T on Γ 1 , where:

Γ 1 ≡ Γ 0 ∪ A 4 ⇒ ψ 4 [t 1 , t 2 / 4 , pt ] * ≡ Γ 0 ∪ {A 4 ⇒ y ≈ nil ⇒ ({y} ≈ {y} ∧ ite(y ∈ {y}, 0 ≈ 1, pt(y) ≈ 1) ∧ y ≈ nil)} ≡ Γ 0 ∪ {A 4 ⇒ y ≈ nil ⇒ ⊥}
The set Γ 1 is T -unsatisfiable, since the added constraint contradicts A 4 ∧ y ≈ nil.

Integration in DPLL(T )

We have implemented the algorithm described in this section within the SMT solver CVC4 [START_REF] Barrett | CAV'11[END_REF]. Our implementation accepts an extended syntax of SMT-LIB version 2 format [START_REF] Barrett | The SMT-LIB 2.5 standard[END_REF] for specifying SL (T ) formulae. In contrast to the presentation so far, our implementation does not explicitly introduce quantifiers, and instead treats SL atoms natively using an integrated subsolver that expands the semantics of these atoms in lazy fashion.

In more detail, given a SL (T ) input ϕ, our implementation lazily computes the expansion of (ϕ [ , pt,C])⇓ based on the translation rules in Figures 1 and2 and the counterexample-guided instantiation procedure in Figure 3. This is accomplished by a module, which we refer to as the SL solver, that behaves analogously to a DPLL(T )style theory solver, that is, a dedicated solver specialized for the T -satisfiability of a conjunction of T -constraints.

The DPLL(T ) solving architecture [START_REF] Ganzinger | Dpll(t): Fast decision procedures[END_REF] used by most modern SMT solvers, given as input a set of quantifier-free T -formulae Γ, incrementally constructs of set of literals over the atoms of Γ until either it finds a set M that entail Γ at the propositional level, or determines that such a set cannot be found. In the former case, we refer to M as a satisfying assignment for Γ. If T is a combination of theories T 1 ∪ . . . ∪ T n , then M is partitioned into M 1 ∪ . . . ∪ M n where the atoms of M i are either T i -constraints or (dis)equalities shared over multiple theories. We use a theory solver (for T i ) to determine the T i -satisfiability of the set M i , interpreted as a conjunction. Given M i , the solver will either add additional formulae to Γ, or otherwise report that M i is T i -satisfiable.

For SL (T ) inputs, we extend our input syntax with a set of functions:

→: Loc × Data → Bool * n : Bool n → Bool emp : Bool - - * : Bool × Bool → Bool lbl : Bool × Set(Loc) → Bool
which we call spatial functions 8 . We refer to lbl as the labeling predicate, which can be understood as a placeholder for the transformation in Figures 1 and2. We refer to p(t) as an unlabeled spatial atom if p is one of {emp, →, * n ,-- * } and t is a vector of terms not containing lbl. If a is an unlabeled spatial atom, We refer to lbl(a, ) as a labeled spatial atom, and extend these terminologies to literals. We assume that all occurrences of spatial functions in our input ϕ occur only in unlabeled spatial atoms. Moreover, during execution, our implementation transforms all spatial atoms into a normal form, by applying associativity to flatten nested applications of * , and distributing Σ-formulae over spatial connectives, e.g.

((x → y ∧ t ≈ u) * z → w) ⇐⇒ t ≈ u ∧ (x → y * z → w).
When constructing satisfying assignments for ϕ, we relegate the set of all spatial literals M k to the SL solver. For all unlabeled spatial literals (¬)a, we add to Γ the formula (a ⇔ lbl(a, 0 )), where 0 is a distinguished free constant of sort Set(Loc). Henceforth, it suffices for the SL solver to only consider the labeled spatial literals in M k . To do so, firstly, it adds to Γ formulae based on the following criteria, which model one step of the reduction from Figure 1:

lbl(emp, ) ⇔ ≈ ∅ if (¬)lbl(emp, ) ∈ M k lbl(t → u, ) ⇔ ≈ {t} ∧ pt(t) ≈ u ∧ t ≈ nil if (¬)lbl(t → u, ) ∈ M k lbl((ϕ 1 * . . . * ϕ n ), ) ⇒ (ϕ 1 [ 1 ] ∧ . . . ∧ ϕ n [ n ]) if lbl((ϕ 1 * . . . * ϕ n ), ) ∈ M k ¬lbl((ϕ 1 - - * ϕ 2 ), ) ⇒ (ϕ 1 [ 1 ] ∧ ¬ϕ 2 [ 2 ]) if ¬lbl((ϕ 1 - - * ϕ 2 ), ) ∈ M k
where each i is a fresh free constant, and ϕ i [ i ] denotes the result of replacing each top-level spatial atom a in ϕ i with lbl(a, i ). These formulae are added eagerly when such literals are added to M k . To handle negated * -atoms and positive -- * -atoms, the SL solver adds to Γ formulae based on the criteria:

¬lbl((ϕ 1 * . . . * ϕ n ), ) ⇒ (¬ϕ 1 [t 1 ] ∨ . . . ∨ ¬ϕ n [t n ]) if ¬lbl((ϕ 1 * . . . * ϕ n ), ) ∈ M k lbl((ϕ 1 - - * ϕ 2 ), ) ⇒ (¬ϕ 1 [t 1 , f 1 ] ∨ ϕ 2 [t 2 , f 2 ]) if lbl((ϕ 1 - - * ϕ 2 ), ) ∈ M k
where each t i and f i is chosen based on the same criterion as described in Figure 3. For wand, we write ϕ i [t i , f i ] to denote ϕ i [t i ], where ϕ i is the result of replacing all atoms of the form t → u where t ∈ t 1 in ϕ i by f i (t) ≈ u. CVC4 uses a scheme for incrementally checking the T -entailments required by solve T , as well as constructing models J satisfying the negated form of the literals in literals in M k before choosing such terms [START_REF] Reynolds | An instantiation-based approach for solving quantified linear arithmetic[END_REF]. The formula of the above form are added to Γ lazily, that is, after all other solvers (for theories T i ) have determined their corresponding sets of literals M i are T i -satisfiable. Partial Support for Quantifiers In many practical cases it is useful to check the validity of entailments between existentially quantified SL(T ) formulae such as ∃x . φ(x) and ∃y . ψ(y). Typically, this problem translates into a satisfiability query for an SL(T ) formula ∃x∀y . φ(x) ∧ ¬ψ(y), with one quantifier alternation. A partial solution to this problem is to first check the satisfiability of φ. If φ is not satisfiable, the entailment holds trivially, so let us assume that φ has a model. Second, we check satisfiability of φ ∧ ψ. Again, if this is unsatisfiable, then the entailment cannot hold, because there exists a model of φ which is not a model of ψ. Else, if φ ∧ ψ has a model, we add an equality x = y for each pair of variables (x, y) ∈ x × y that are mapped to the same term in this model, the result being a conjunction E(x, y) of equalities. Finally, we check the satisfiability of the formula φ ∧ ¬ψ ∧ E. If this formula is unsatisfiable, the entailment is valid, otherwise, the test is inconclusive. In section 6, we applied this method manually, to test entailments between existentially quantified variables -general procedure for quantifier instantiation for SL(T ) is envisaged in the near future.

Evaluation

We tested our implementation of the (SL, T )-satisfiability procedure in CVC4 (version 1.5 prerelease) 9 on two kinds of benchmarks: (i) finite unfoldings of inductive predicates with data constraints, mostly inspired by existing benchmarks, such as SL-COMP'14 [START_REF] Sighireanu | Report on SL-COMP 2014[END_REF], and (ii) verification conditions automatically generated by applying the weakest precondition calculus of [START_REF] Ishtiaq | BI as an assertion language for mutable data structures[END_REF] to the program loops in Figure 4 several times. All experiments were run on a 2.80GHz Intel(R) Core(TM) i7 CPU machine with with 8MB of cache 10 . For a majority of benchmarks, the runtime of CVC4 is quite low, with the exception of the n = 4, 8 cases of the entailments between tree n 1 and tree n 2 formulae, which resulted in a timeout after 300 seconds. For benchmarks where CVC4 times out, the performance bottleneck resides in its ground decision procedure for finite sets, indicating efficient support for this theory is important for our approach to separation logic. The first set of experiments is reported in Table 1. We have considered inductive predicates commonly used as verification benchmarks [START_REF] Sighireanu | Report on SL-COMP 2014[END_REF]. Here we check the validity x →a * neg 5 (a,y) 0.02s 0.05s 0.14s 0.32s 3.69s of the entailment between lhs and rhs, where both predicates are unfolded n = 1, 2, 3, 4, 8 times. The second set of experiments, reported in Table 1, considers the verification conditions of the forms ϕ ⇒ wp(l, φ) and ϕ ⇒ wp n (l, φ), where wp(l, φ) denotes the weakest precondition of the SL formula φ with respect to the sequence of statements l, and wp n (l, φ) = wp(l, . . . wp(l, wp(l, φ)) . . .) denotes the iterative application of the weakest precondition n times in a row. We consider the loops depicted in Figure 4, where, for each loop l we consider the variant zl as well, which tests that the data values contained within the memory cells are 0, by the assertions on line 2. The postconditions are specified by finite unfoldings of the inductive predicates ls and zls (Figure 4).

Conclusions

We have presented a decision procedure for quantifier-free SL (T ) formulas that relies on a efficient, counterexample-guided approach for establishing the T -satisfiability of formulas having quantification over bounded sets. We have described an implementation of the approach as an integrated subsolver in the DPLL(T )-based SMT solver CVC4, showing the potential of the procedure as a backend for tools reasoning about low-level pointer and data manipulations.

Fig. 1 .

 1 Fig. 1. Labeling Rules 6 We denote by F↓ D the restriction of the function F to the domain D ⊆ dom(F).

  ¬emp * ¬emp and the domain of h contains more than two locations, then it is possible to restrict dom(h) to |¬emp * ¬emp| = 2 locations only, to satisfy this formula.Let Pt(φ) be the set of terms (of sort Loc ∪ Data) that occur on the left-or righthand side of a points-to atomic proposition in φ. Formally, we have Pt(t → u) = {t, u}, Pt(φ * ψ) = Pt(φ -- * ψ) = Pt(φ) ∪ Pt(ψ), Pt(¬φ) = Pt(φ) and Pt(emp) = Pt(φ) = ∅, for a Σ-formula φ. The small model property is given by the next lemma: Lemma 2. [24, Proposition 96] Given a formula φ ∈ SL(T ), for any interpretation I of T , let L ⊆ Loc I \ Pt(φ) I be a set of locations, such that | |L| | = |φ| and v ∈ Data I \ Pt(φ) I .

  , besides the ones with premises (φ * ψ) [ , pt] and (φ -- * ψ) [ , pt], by replacing any judgement ϕ [ , pt] with ϕ [ , pt,C]. The two rules in Figure 2 are the bounded-quantifier equivalents of the (φ * ψ) [ , pt] and (φ -- * ψ) [ , pt] rules in Figure 1. As usual, we denote by (ϕ [ , pt,C])⇓ the formula obtained by exhaustively applying the new labeling rules to ϕ [ , pt,C].

Fig. 2 .

 2 Fig. 2. Bounded Quantifier Labeling Rules

  solve SL(T) (ϕ): Let C be a set of fresh constants of sort Loc such that | |C| | = |ϕ|. Let and pt be a fresh symbols of sort Set(Loc) and Loc ⇒ Data respectively. Return solve T ( (ϕ [ , pt,C])⇓ * ).

Fig. 3 .

 3 Fig. 3. Procedure solve SL(T) for deciding (SL, T )-satisfiability of SL (T ) formula ϕ.

Example 4 .

 4 Consider the SL(T ) formula ϕ ≡ emp ∧ (y → 0 -- * y → 1) ∧ y ≈ nil. When running solve SL(T) (ϕ), we first compute the set C = {c}, and introduce fresh symbols the domain of k may be restricted to the set {c I | c ∈ S 1 } in models I found in Steps 1 and 2 of the procedure. This restriction comes with no loss of generality since, by construction of (ϕ [ , pt,C])⇓, k is applied only to terms occurring in S 1 .

1 :Fig. 4 .

 14 Fig. 4. Program Loops

lhs rhs n = 1 n

 1 = 2 n = 3 n = 4 n = 8 Unfoldings of inductive predicates lseg 1 (x,y,a) emp∧x=y∨∃z∃b . lseg 2 (x,y,a) emp∧x=y∨∃z∃b . unsat unsat unsat unsat unsat x →(a,z) * lseg 1 (z,y,b)∧b=a+10 x →(a,z) * lseg 2 (z,y,b)∧a≤b < 0.01s < 0.01s < 0.01s 0.01s 0.01s tree 1 (x,a) emp∧x=nil∨∃y∃z∃b∃c . tree 2 (x,a) emp∧x=nil∨∃y∃z∃b∃c . unsat unsat unsat timeout timeout x →(a,y,z) * tree 1 (y,b) * tree 1 (z,c)∧ x →(a,y,z) * tree 2 (y,b) * tree 2 (z,c)∧ < 0.01s 0.06s 1.89s > 300s > 300s b=a-10∧c=a+10 b≤a∧a≤c pos 1 (x,a) x →a∨∃y∃b . neg 1 (x,a) ¬x →a∨∃y∃b . unsat unsat unsat unsat unsat x →a * pos 1 (y,b) x →a * neg 1 (y,b) 0.02s 0.04s 0.11s 0.25 s 3.01s pos 1 (x,a) x →a∨∃y∃b . neg 2 (x,a) x →a∨∃y∃b . unsat unsat unsat unsat unsat x →a * pos 1 (y,b) ¬x →a * neg 2 (y,b) 0.01s 0.05s 0.11s 0.23s 2.10s pos 1 (x,a) x →a∨∃y∃b . neg 3 (x,a) x →a∨∃y∃b . unsat unsat unsat unsat unsat x →a * pos 1 (y,b) x →a * ¬neg 3 (y,b) 0.02s 0.07s 0.24s 0.46s 4.05s pos 1 (x,a) x →a∨∃y∃b . neg 4 (x,a) x →a∨∃y∃b . unsat sat unsat sat sat x →a * pos 1 (y,b) ¬x →a * ¬neg 4 (y,b) 0.05s 0.24s 0.33s 2.77s 24.72s pos 2 (x,a) x →a∨∃y . neg 5 (x,a) ¬x →a∨∃y . unsat unsat unsat unsat unsat x →a * pos 2 (a,y)

Table 1 .

 1 pos 2 (x,a) x →a∨∃y . neg 6 (x,a) x →a∨∃y . sat unsat unsat unsat unsat x →a * pos 2 (a,y) ¬x →a * neg 6 (a,y) 0.02s 0.04s 0.13s 0.27s 2.22s (u) * ls 0 (v) wp(rev,ls n-1 (u) * ls 1 (v)) 0.06s 0.08s 0.14s 0.30s 2.83s ls n (u) * ls 0 (v) wp n (rev,u=nil∧ls n (v)) 0.06s 0.12s 0.56s 1.75s 27.82s zls n (u) * zls 0 (v) wp(zrev,zls n-1 (u) * zls 1 (v)) 0.22s 0.04s 0.12s 0.25s 2.16s zls n (u) * zls 0 (v) wp n (zrev,u=nil∧zls n (v)) 0.04s 0.10s 0.41s 1.27s 20.26s Experimental results

		Verification conditions
	ls n (w)	wp(disp,ls n-1 (w))	< 0.01s 0.02s 0.05s 0.12s 1.97s
	ls n (w)	wp n (disp,emp∧w=nil)	< 0.01s 0.02s 0.12s 0.41s 22.97s
	zls n (w)	wp(zdisp,zls n-1 (w))	0.01s 0.02s 0.05s 0.11s 1.34s
	zls n (w)	wp n (zdisp,emp∧w=nil)	0.01s 0.02s 0.11s 0.43s 24.13s
	ls n

For brevity, we may write p(t) as shorthand for p(t) ≈ , where p is a function into Bool.

Take for instance φ as x → 1 and ϕ as y → 2.

Non-constant Skolem symbols k introduced by the procedure may be treated as uninterpreted functions. Constraints of the form k ⊆ S 1 × S 2 are translated to c∈S 1 k(c) ∈ S 2 . Furthermore,

These functions are over the Bool sort. We refer to these functions as taking formulae as input, where formulae may be cast to terms of sort Bool through use of an if-then-else construct.

Available at http://cvc4.cs.nyu.edu/web/.

The CVC4 binary and examples used in these experiments are available at http://cvc4.cs. nyu.edu/papers/ATVA2016-seplog/.