François Bobot

Stéphane Graham-Lengrand

Bruno Marre

Guillaume Bury

Centralizing equality reasoning in MCSAT

come   L'archive ouverte pluridisciplinaire

Introduction

Model-constructing satisfiability (MCSAT) [START_REF] Jovanović | Solving Nonlinear Integer Arithmetic with MCSAT[END_REF][START_REF] De Moura | A Model-Constructing Satisfiability Calculus[END_REF] is an approach to SMT-solving that applies the principles of Conflict-Driven Clause Learning (CDCL) not only to propositional reasoning but also to theory reasoning. For instance, the main procedure is a loop that alternates model building phases with conflict analysis phases.

MCSAT is specifically tuned to theories that have a standard model, in the sense that a (quantifier-free) formula is satisfiable in the theory if and only if it evaluates to true in this particular model for some interpretation of its free variables. The MCSAT transition system, when given an input formula to satisfy, organises the search for such an interpretation similarly to CDCL. It gradually builds a candidate interpretation by aggregating on a trail explicit assignments of truth values to Boolean variables, e.g., (l←true), but in contrast to CDCL it also aggregates explicit assignments of model values to first-order variables, e.g., (x← 3 4). It relies on a theory plugin to provide an evaluation function and to generate theory lemmas whenever the candidate interpretation fails to satisfy the input formula, a situation known as a conflict. MCSAT thus combines with Boolean reasoning any theory for which an MCSAT theory plugin can be defined, including for instance linear and non-linear versions of arithmetic [START_REF] Jovanović | Solving Nonlinear Integer Arithmetic with MCSAT[END_REF][START_REF] Jovanović | Solving non-linear arithmetic[END_REF][START_REF] De Moura | A Model-Constructing Satisfiability Calculus[END_REF], and the theory of bitvectors [START_REF] Graham-Lengrand | An MCSAT treatment of Bit-Vectors[END_REF][START_REF] Zeljic | Deciding Bit-Vector Formulas with mcSAT[END_REF]. In [START_REF] Jovanović | The Design and Implementation of the Model Constructing Satisfiability Calculus[END_REF], Equality with Uninterpreted Functions (EUF) is added to the combination of Linear Real Arithmetic (LRA) and Boolean reasoning, hinting at a rather systematic approach to theory combination. The full development of this approach, proving soundness, completeness and termination properties for the combination of theories with disjoint signatures, was conducted in a more general framework called CDSAT for Conflict-Driven Satisfiability [START_REF] Bonacina | Proofs in Conflict-Driven Theory Combination[END_REF][START_REF] Bonacina | Satisfiability Modulo Theories and Assignments[END_REF]. CDSAT generically combines a collection of abstract theory modules where theory reasoning is specified in terms of inference rules rather than evaluation and theory lemmas, and therefore CDSAT does not require theories to have a standard model in the sense described above. Indeed the interpretation of sorts as sets, and of symbols as functions and predicates, may vary according to theory models, while being more specified than in theory EUF (imagine for instance a theory T inj whose unique function symbol f from sort s 1 to sort s 2 is injective). MCSAT is an instance of CDSAT, and the more traditional Nelson-Oppen scheme [START_REF] Nelson | Simplification by cooperating decision procedures[END_REF] for theory combination is another, where each theory T comes with a black box procedure that decides T -satisfiability. CDSAT can also combine MCSAT theory plugins with black box decision procedures. In all cases, the critical information exchanged between theory modules, whether explicitly or by assigning first-order values, is about equalities, i.e., which variables or terms are equal to which.

Indeed, theory combination in MCSAT raises for instance the question: if a theory module for, e.g., LRA communicates assignment x← 3 4, what should another theory module in the combination understand from it? From value 3 4 itself it should only understand that it is different from other values, say 2 3. Thus, if the LRA module communicates another assignment y← 2 3 (resp. y← 3 4), other theory modules only have to understand that x and y are different (resp. equal). Each theory module is therefore required to understand equality and reason about it taking into account reflexivity, symmetry and transitivity. In practice though, it is desirable to avoid duplicating computation for equality reasoning across different theory modules.

In this paper, we sketch the design of an architecture based on MCSAT where equality reasoning is centralized. A unique component implementing an equality graph (Egraph) lies at the centre of the architecture, and can be queried by the different theory modules.

On the one hand, this departs from the traditional SMT-solving architecture based on DPLL(T), where the SAT-solver, rather than the Egraph, has the central role. Instead, we follow the idea of MCSAT and CDSAT that Boolean reasoning can be considered as one of the theories to be combined, and we argue that it is more important for theory modules to be directly interfaced with the Egraph, delegating equality reasoning to it, rather than to be interfaced with the module handling Boolean connectives.

On the other hand, the literature on MCSAT and CDSAT hardly investigates whether and how the mechanisms controlling the assignments of values to terms can be usefully enhanced by centralizing equality reasoning: For instance, assume that terms t 0 , . . . , t n are equal, i.e., assume the connectivity of the graph whose vertices are those terms and whose edges are the explicitly known equalities t i = t j between them. There is a risk in MCSAT and CDSAT that deciding the assignment of a value to t 0 triggers n further assignments of the same value to t 1 , . . . , t n , via the equality constraints between the terms which, one after the other, all become unit constraints. On the contrary, not performing those n propagations may be problematic, say if the value of t 42 is needed for the evaluation of a bigger term where t 42 occurs.

In this paper we sketch how to leverage an Egraph in order to avoid such dilemmas and provide other benefits such as recording the domains of feasible values for equivalence classes of terms rather than for individual terms. The use of the Egraph during the model building phases, described in Section 2, then impacts how conflict analysis is also performed, as described in Section 3. A prototype is available at https://github.com/witan-org/witan.

Purpose and general principles of the equality reasoner

The equality reasoner has several purposes:

The first one is to make available, on demand, the information of whether two terms are equal, different, or whether this is unknown, given the knowledge that has been passed to the reasoner so far. This takes into account reflexivity, symmetry, and transitivity, but also (this is specific to MCSAT/CDSAT) the assignment of values to variables and more generally to terms: If x← 3 4, y← 3 4, z← 2 3 have been communicated to the equality reasoner, then the reasoner can tell (without understanding the semantics of 3 4 and 2 3) that x is equal to y and different from z. This inference power is formally identified in [START_REF] Bonacina | Proofs in Conflict-Driven Theory Combination[END_REF][START_REF] Bonacina | Satisfiability Modulo Theories and Assignments[END_REF], in the form of equality inferences.

The second purpose is to make available, on demand, the information of whether a term has a determined value (and if so, which one), either because a value has been assigned to it explicitly, or because a value has been explicitly assigned to another term that is equal to the first one according to equality inferences.

The third one is to record theory-specific information about terms that is meant to be invariant across classes of terms that are known to be equal. For instance, imagine the LRA theory module records that the range of feasible values for a variable x is in the interval [ 2 3, 3 4] (e.g., any other value would violate a constraint that must be satisfied), and wonders about the range of feasible values for variable y. If y can be inferred to be equal to x according to equality inferences, then the feasible values for y should also be in [ 2 3, 3 4]. This is particularly useful in MCSAT, where theory plugins often maintain, for each variable whose value is to be determined, a domain of feasible values to pick from. Maintaining one domain for each equivalence class of terms, rather than for each term or variable, is likely to be more efficient, and can be provided by the equality reasoner.

For obvious reasons of efficiency, an equality reasoner that makes all of this information available should avoid eager computations. For reflexivity, symmetry and transitivity, an Egraph based on union-find is the obvious and well-known structure to use, materialising equivalence classes of terms. Making the equality reasoner handle value assignments, so as to capture all equality inferences, only requires a minor adaptation: both terms and values can form nodes of the Egraph, and when x← 3 4 is communicated to the reasoner, the equivalence classes of x and 3 4 should be merged. The Egraph can record, for each equivalence class, the value (if any) that has been assigned to some term in the class, and otherwise the domain of feasible values. This allows the Egraph to fulfil the second and third purpose, and detect when merges lead to basic inconsistencies: for instance if in the example above some term in the same class as x has already been assigned a different value, say 2 3, the merge fails and a conflict is raised.

Finally, making all of this information available on demand means that the Egraph can be queried for a direct answer, but also that whichever component sends the query can also ask to be notified when the answer to the query changes in the future: typically, if two terms cannot be determined to be equal or different according to equality inferences, being notified when their equality becomes determined may be useful for a theory module. The Egraph therefore allows components to subscribe to a daemon monitoring the query.

In the next section we further detail the implementation and use of the Egraph, describing the objects that are manipulated, how theories could propagate information or be warned that some information have been propagated, and finally how the engine orders these request.

Implementation and use of the Egraph

Nodes A node of the Egraph is an inhabitant of an OCaml sum type, being either a term, of type ThTerms, or a value, of type Values. Both are hashconsed in our implementation. 1Since each theory module can use its own notion of value, the inhabitants of Values can be heterogeneous, implementing the Booleans (⊺, ), the rationals (for LRA), the algebraic reals (for NRA), etc. Type Values is actually an extensible type, so that it can be defined at runtime according to which theory modules participate to the theory combination. The requirement to hashcons the Values just means that an equality function (already needed) and a hash function (for limiting the use of the equality) must be provided, so even with complicated values such as the algebraic reals, there is no need for a costly canonical representation (equality using Thom encoding is NC [START_REF] Mishra | Arithmetic with real algebraic numbers is in NC[END_REF], the hash could use some fixed precision approximation of the real). Perhaps less expectedly, type ThTerms is also made of heterogeneous inhabitants: Besides syntactic terms, which directly implement the first-order term grammar and are obtained for instance as a result of parsing the input, each theory can use its own notion of term so that, for instance, if the syntactic term ((x + 7) + (xy))) is parsed, the LRA theory immediately creates a theory term appropriate for LRA, i.e., an implementation of the polynomial recording the map from variables to coefficients {x ↦ 2, y ↦ -1} and the constant 7. Variables x and y can more generally be nodes of the Egraph, e.g., composite terms whose head symbol is in the signature of another theory and which LRA treats as variables. Similarly, the Boolean theory can use theory terms of the form ± (±n 1 ∨ ⋅ ⋅ ⋅ ∨ ±n j ) where n 1 , . . . , n j are nodes (± marks the presence or absence of a negation). Such theory terms can be seen as the semantical values of [START_REF] Conchon | CC(X): Semantic Combination of Congruence Closure with Solvable Theories[END_REF]. Type ThTerms is an extensible one for the same reason as type Values, and syntactic terms are a particular instance of theory terms that is present in every combination. When a theory term is computed as a more appropriate representation of a syntactic term, their respective equivalence classes are immediately merged.

In this paper, our notations do not distinguish values and value nodes, e.g., ⊺, 3/ 4 are both values and nodes. On the other hand for clarity our notations distinguish theory terms and nodes, and we use a definitional notation such as n ≜ ± (±n 1 ∨ ⋅ ⋅ ⋅ ∨ ±n j ) to indicate that n is the view of the Boolean theory term ± (±n 1 ∨ ⋅ ⋅ ⋅ ∨ ±n j ) as a node.

Node

Figure 1: Relations between the object in the Egraph

Equivalence class information Information about each equivalence class can be recorded by an Egraph (e.g., at the root of the tree implementing the class in the unionfind structure). It can be useful to record: a value v if the equivalence class contains v as a node; if not, a domain of feasible values that can be assigned to the theory terms in the class; a syntactic term in the equivalence class, if there is one (it can be useful if a representative of the class is needed that is expressed in the vanilla first-order term grammar); if not, a theory term that can be picked as the class representative.

In fact, we may record for the class different values for different theory modules. Indeed, several modules may want to assign values to the theory terms in an equivalence class, if they share the sort of these terms but are using different kinds of values for that sort [START_REF] Bonacina | Satisfiability Modulo Theories and Assignments[END_REF], e.g., theory T 1 assigning t← 3 4 and theory T 2 assigning u←red, with t and u in the same class. Having both assignments is not necessarily unsatisfiable: 3 4 and red will only have to denote the same element in a (T 1 ∪T 2 )-model. For instance, T 1 could be LRA, with t and u being of sort Q (the rationals), and T 2 could be a theory whose signature involves this sort while the semantics of its inhabitants is irrelevant (e.g., the sort of values in the theory of arrays): T 2 is still allowed to use an arbitrary range of values such as red for its own reasoning mechanics, and store them in the Egraph. The Egraph does maintain the invariant that one theory module can only have at most one of its values in an equivalence class; and if there is one, it makes it readily available in the class information structure.

Likewise, the Egraph allows each theory module to maintain its own domain for the feasible values of a class. In fact, this domain can even be implemented as a composite domain: for instance the theory of bitvectors may maintain, as in [START_REF] Zeljic | Deciding Bit-Vector Formulas with mcSAT[END_REF], a bitvector interval domain, e.g., [1010, 1110], together with a bitvector mask domain, e.g., 1??0. Values to be picked must be in the intersection of the domains; in this example 1010, 1100, and 1110 are feasible. Disequality information is also recorded as a domain for the class (indicating which other equivalence classes should not be merged with this one).

Egraph operations

We now describe the operations that transform the Egraph during the model building phase; they each correspond to an exported primitive in the Egraph API. Any node participating to one of the Egraph operations must be registered. Until then the node is dormant; separating node creation and registration avoids reasoning on a part of formula that is not needed: e.g., with ite(c, t, e) the nodes t (resp. e) could be dormant until we know that c has value ⊺ (resp. )). Four kinds of Egraph operations can be applied to an Egraph E:

Merge: Two registered nodes n 1 and n 2 have their equivalence classes merged, the resulting Egraph being denoted merge n 1 n 2 in E.

ThTerms: The classes of a registered node and a theory term are merged.

Value: The value of a registered node is set, merging the classes of the node and the value. Domain: The domain of a registered node is set or modified. Operation Value (resp. ThTerms) is not subsumed by Merge, because the value (resp. the theory term) does not have to be registered. Because of this, none of the four operations above increase the number of equivalence classes, even temporarily.

Daemon Constraint Programming as known in the CP community, uses domains extensively with the help of daemons also called suspension [1, p. 185]. Daemons specify on which events they are waiting (e.g., the domain of specific node is modified, two equivalence classes are merged). They also provide a call-back function, to be run when the daemon is woken. In our design, daemons can wait on the following events: Domains: wake up when the specific kind of domain for a specific node is modified.

We write (t ◁ E D) when, in Egraph E, the theory term t has domain D in its class; Values: wake up when the specified node gets a value of the specified kind in its class. We write (t← E v) when, in Egraph E, the theory term t has value v in its class.

If on the contrary the class of t has no values of the specified kind we write (t ← E ). Node Registered: wake up when the specified node is registered; Theory Terms Registered: wake up when a theory term of the specified kind is registered; Value Registered: wake up when a value of the specified kind is registered;

Repr: wake up when this node is no longer the representative of its equivalence class. The events Domains and Values could be used for example for Boolean or arithmetic propagation. The events Node Registered can be used when delaying the registration of a sub-term, to know that it has been registered from somewhere else. The events Theory Terms Registered and Value Registered are used for initializing other daemons, for example to perfom domain or value propagations. The events Repr is used for congruence closure, as indeed for n ≜ f (x) we should merge the theory term f (y) with n when x is not the representative anymore.

Ordering The daemons are not woken immediately when an Egraph operation is performed. Otherwise a wake-up chain could be triggered, leading to potential loops or stack overflows. More importantly, this would make reasoning a lot harder. So most of the wake-ups are delayed. Also a merge between two classes cannot be done before the domains of the two classes are merged and therefore identical. Some daemon must be run with a higher priority than merging, for example because they ensure some invariant of a domain (for example for keeping a normalized linear polynomial as a domain), we call these daemons impatient. In order to satisfy these constraints the Egraph processes the actions using different queues in the following order of preference:

1. The registration of a node is done immediately, the woken deamons are queued. 2. Modification of domain is done immediately, the woken deamons are queued.

3. Setting of a value is done immediately if it is not registered and the woken daemons are queued, otherwise the merging of the nodes is queued. 4. Setting of a theory term is done immediately if it is not registered and the woken daemons are queued, otherwise the merging of the nodes is queued. 5. Running of impatient daemons. 6. Merging domains of the nodes that are going to be merged 7. Finish the merging of the nodes and the woken daemons are queued. This queue has always at most one element. 8. Start the merge of a pair of nodes, marked as merging n 1 n 2 in E by expl. It is done in two steps: first, queuing their domains, if different, for merging (priority 6); second, queuing the finishing of the merge (priority 7). 9. Run the other daemons. 10. Run the decisions.

The last two queues could be handled by an external scheduler that also handles the backtrack points and the alternation between the model building phase and conflict analysis phase.

Explanation Triggering most of the Egraph-transforming operations requires providing a piece of data called explanation. That data is later used during conflict analysis so as to remember why the operation was performed. The format of that data is specific to the module having triggered the operation, since the data will be passed back to the module if and when conflict analysis asks why this operation was performed. Explanations are similar to the theory proofs of [START_REF] Bonacina | Proofs in Conflict-Driven Theory Combination[END_REF]. Here, a particular case of explanation is the dummy one that marks the operation as having been performed "for no reason", i.e., as a decision. Such unjustified operations will be potential points of backtrack during search, as discussed in the next paragraph. An explanation is required for the Merge, Value and ThTerms operations, but not for the Domain one. It is required for the former because the equality is a central notion that any theory could use. On the other hand, the latter is specific to the theory that maintains this domain. Nonetheless at any time an explanation can be stored on the trail; we will see an example of this in Section 4.2.

Decisions During the model building phases, theory modules can declare their interest in some decisions being made (e.g., "I need the value of that variable to be decided"). The format of such declarations is again theory-specific, but it contains at least a declared Egraph node of interest. Such declarations are recorded centrally in a decision queue, which is a priority queue that uses the usual VSIDS heuristics [START_REF] Moskewicz | Chaff: Engineering an Efficient SAT Solver[END_REF], based here on the activity of nodes. When a clause is learnt, a set of useful nodes is identified in order to update their activity. When no more propagations are to be done, the scheduler selects one possible decision out of the decision queue, and asks the theory module that created it whether the decision is still needed. Indeed, since the proposed decision was placed into the queue, events might have happened (e.g., propagations) that make it obsolete. If the decision is not needed after all (e.g., the value of a variable has been already determined by propagation), the scheduler moves on without creating a backtrack point. If the decision is needed, the scheduler creates a backtrack point and applies the Egraph operation specified by the decision.

Conflict When a conflict is found by a daemon during propagation, the Egraph is notified and an explanation is given, this time justifying the conflict rather than a propagation. The Egraph could detect a conflict by itself when attempting an operation merge n 1 n 2 in E, e.g., if n 1 ← E v 1 and n 2 ← E v 2 for two values v 1 and v 2 of some theory T that are different. In that case the merge is not performed (as we prefer to keep the Egraph in a sound state) and, accordingly, the explanation expl given for the failed operation merge n 1 n 2 in E is not added to the trail. Instead, it contributes to the explanation Diff value(expl, n 1 , v 1 , n 2 , v 2 ) (c.f. Section 4.1) that the Egraph gives to justify the conflict that it detected. When the Egraph detects or is notified of a conflict, it in turn notifies the scheduler, which starts the conflict analysis phase. Conflict analysis computes the backtrack point that the scheduler should go back to, restoring the Egraph datastructure that existed then. The only information kept from this branch exploration is the constraint learnt during conflict analysis (and the VSIDS heuristic score updates). This ensures the Egraph does not grow indefinitely with the arbitrary values used during search.

Conflict Analysis

The conflict analysis phase should produce a new constraint that forbids at least the last decision that was made. In order to do that, explanations for Egraph operations are recorded in a trail, a stack that is similar to that used in CDCL, MCSAT and CDSAT. The number of elements in the trail is the current age. Backtrack points corresponds to particular ages of the stack.

Node history An additional structure, called the node history or nodehist, is used to answer the question: "are two nodes n 1 and n 2 in the same equivalence class, and if so, at which age did they first appear in the same class?". This is useful information because the trail has recorded, at this age, the explanation given for the merge. The node history, given a node n, indicates (i) at which age a n this node stopped being the representative of its class and (ii) what its new representative newrep(n) was. Recording that information during the model building phase is done in constant time. To answer the above question during conflict analysis, assume without loss of generality that a n1 < a n2 ; then if newrep(n 1 ) is n 2 the answer to the question is a n1 , and otherwise the answer is recursively computed for newrep(n 1 ) and n 2 .

Hypotheses and split function The conflict analysis is similar to that in other frameworks such as CDCL, MCSAT or CDSAT. It starts when a conflict is notified to the Egraph. The analysis maintains a conflict, i.e., a list H 1 , . . . , H n of conflict elements or hypotheses such that H 1 , . . . , H n ⊧ T∞ , where T ∞ is the union of the combined theories, as in [START_REF] Bonacina | Satisfiability Modulo Theories and Assignments[END_REF]. Hypotheses are theory-specific and called T -hypotheses; each T -hypothesis H should hold in the partial model described by the Egraph E, i.e., E ⊧ T H (in [START_REF] Bonacina | Satisfiability Modulo Theories and Assignments[END_REF] the conflict elements had to be explicitly present in the trail; here it can hold in a less direct way). The theory module for T must provide a means to retrieve, from H, the reasons why it holds according to the current Egraph E. Technically, this is given as a set ages(H) of ages, identifying the Egraph operations that contribute to making H hold. For instance an LRA-hypothesis H could be (0 ≤ x + y); assuming that H holds according to the Egraph E because x← E 2 and y← E 3, we would have ages(H) = {a x , a y }, where a x (resp. a y ) is the age when x and 2 (resp. y and 3) first appeared in the same class.

The analysis starts with H 0 ⊧ T∞ and H 0 = . Then each step consists of replacing one hypothesis H by a set of hypotheses such that H 1 , . . . , H n ⊧ T∞ H, as in [START_REF] Bonacina | Satisfiability Modulo Theories and Assignments[END_REF] We now look at how the new hypotheses H 1 , . . . , H n are recovered. If H is a T 1 -hypothesis, the theory module for T 1 can provide age max (H). Typically, the explanation expl found in the trail at age age max (H) is the explanation of a merge (merge n 1 n 2 in E), which was triggered by the theory module for a theory T 2 . From a logical point of view, we have E ∧ (n 1 =n 2 ) ⊧ T1 H and therefore E ⊧ T1 (n 1 =n 2 ) ⇒ H. We then rely on the T 1 theory module to provide new T 1hypotheses H 1 , . . . , H k , denoted split T1 (H, n 1 , n 2 ), that form an interpolant between E and (n 1 =n 2 ) ⇒ H, in the sense that E ⊧ T1 H 1 ∧ ⋅ ⋅ ⋅ ∧ H k and H 1 , . . . , H k ⊧ T1 (n 1 =n 2 ) ⇒ H.

For example, assume that T 1 is the theory of pure equality, T 1 -hypotheses are just equalities, H is x=y, and H holds in E because there is in E a chain of equalities, a.k.a. equality path, from x to y. If the equality that was last added to the chain is a = b, then age max (H) is the age of the merge between the classes of a and b, and split T1 (H, a, b) is the set of T 1 -hypotheses {(x=a), (b=y)}. More interestingly, if T 1 is LRA and 0 ≤ x + y holds in the partial model E because x← E 2 and y← E 3, split LRA (0 ≤ x + y, a, b) is the set of hypotheses {(0 ≤ b + y), (x=a)} if a = b is on the equality path from x to 2, and {(0 ≤ x + b), (y=a)} if it is on the equality path from y to 3. This is reminiscent of the substitution mechanism of [START_REF] Jovanović | Solving Nonlinear Integer Arithmetic with MCSAT[END_REF], used during conflict analysis when the last operation that contributed to the conflict was a propagated assignment.

Then the theory module for T 2 can use split T1 (H, n 1 , n 2 ) to produce H 1 , . . . , H n such that H 1 , . . . , H n ⊧ T∞ H. Typically, it will add to split T1 (H, n 1 , n 2 ) = {H 1 , . . . , H k } some T 2hypotheses H k+1 , . . . , H n that entail n 1 =n 2 and that can be recovered from the explanation expl recorded for the merge (merge n 1 n 2 in E). Unless that merge was a decision, n 1 =n 2 is a consequence of E, and H k+1 , . . . , H n will capture "what it is about E that justifies the merge". If the merge was a decision, {H k+1 , . . . , H n } can simply be {n 1 =n 2 } itself, but in that case the hypothesis n 1 =n 2 is marked so that it is never picked for replacement in the next steps of the conflict analysis (if the set {H 1 , . . . , H n } replacing H contained H, conflict analysis would loop).

More generally, the production of H 1 , . . . , H n according to each form expl can take is described by conflict analysis rules, as illustrated in the next section with different examples of theories T 2 . Finally, the conflict analysis step replaces H by H 1 , . . . , H n in the conflict. Value contradiction The conflict explanation given when merge n 1 n 2 in E fails because of a clash of values between v 1 and v 2 is Diff value(expl, n 1 , v 1 , n 2 , v 2 ). Its conflict analysis inference rule replaces by analyze(expl, v 1 = v 2 ). The analysis of expl will usually split the equality into v 1 = n 1 and n 2 = v 2 and add the hypothesis used for propagating n 1 = n 2 .

Examples

Boolean

As in MCSAT and CDSAT, the Boolean theory does not use a CNF transform, and conjunctions and disjunctions could be arbitrarily nested. But the implementation still uses a two-watched literals mechanism to implement Boolean Constraint Propagation (BCP). Theory terms are of the form n ≜ ± (±n 1 ∨ ⋅ ⋅ ⋅ ∨ ±n j ), as described previously. This format can represent conjunctions and disjunctions, and importantly it reduces the need to create nodes that are just negations of each other. The values are ⊺, and there are no domains used for that theory.

Figure 2 shows the propagation rules: the premises of each rule are events that the theory's daemons are notified about, and the conclusion is the Egraph operation that is triggered. The name of the rule and its parameter form the explanation given to the Egraph, i.e., the information kept for the conflict analysis phase. For readability, only the cases when ± is + are

Figure 2 :Figure 3 :

 23 Figure 2: Boolean Theory rules for the model building phase (simplified version only the + case of ± is shown). The name of the rules (Down, Decide, Not, Up, BCP -for Boolean Constraint Propagation, as in SAT) are the name of the explanations. The argument of the names are the information kept for the analysis phase.

  again. We use the ages of hypotheses in the same way a SAT solver uses the levels of literals in a conflict clause: the maximum age max (H) of the set ages(H) is greater than or equal to the age of the last decision, if and only if hypothesis H belongs to the level of the conflict; then If only one hypothesis in the conflict belongs to the level of the conflict, it forms a UIP and we can stop conflict analysis; Otherwise the hypothesis H with greatest age max (H) is chosen for replacement. The replacement is done by looking up, in the trail, the explanation that was given for the Egraph operation performed at age age max (H), and use that to recover new hypotheses H 1 , . . . , H n such that H 1 , . . . , H n ⊧ T∞ H.

As in CDCL, MCSAT, and CDSAT, the model building phase consists in making decisions about the model to be built, and propagating the consequences of these decisions to further complete the construction of the model. This section describes how the equality reasoner is used during that phase.

Two identical values (resp. theory terms) are necessarily at the same memory address.

* Work partially funded by ANR-14-CE28-0020 grant.

shown; the other cases can be obtained by switching ⊺ and according to whether ± is + or -. The rules of figure 3 are the conflict analysis inference rules as described in Section 3: there is one rule for each kind of explanation, which is indicated again in the rule name. The premise of the rule is the hypothesis H (from another theory T ) that needs replacing, and the conclusion of the rule is the set of new hypotheses that H is replaced with. As mentioned in Section 3, the rules rely on the function split T1 provided by T 1 , abbreviated as split in the figure.

We are illustrating the boolean propagation and learning with an example wich is not in CNF (n 1 ∧ n 4 is used as a shorthand for -(-n 1 ∨ -n 4 )), n 7 and n 8 are set to ⊺ at level 0. A sequence of decision and propagation gives the trail: Decide(n 3 ), BCP(n 4 ≜ +(+n 2 ∨ -n 3 ), n 3 ), Decide(n 1 ), BCP(n 1 ≜ n 1 ∧ n 4 , n 1 ) and leads to the contradiction Diff value(BCP(n 8 ≜ +(-n 2 ∨ -n 1 ), n 1 ), n 1 , ⊺, n 8 , ). The conflict analysis start with

Equalities

The theory of equality is responsible for the equality symbol but also of the n-ary function distinct. So theory terms are of the form m ≜ {n 1 ; . . . ; n j }, which intuitively stands for ⋁ i ⋁ k,k =i n i = n k . When this theory term is false we directly have the semantics of distinct. The implementation efficiently implements the distinct symbol by (i) tagging all arguments of distinct (when it has the ⊺ value) with the same tag (the node m), and (ii) checking that no merging is done between nodes sharing the same tags. For each node we store the set of tags

UpFalse(n1,D1,. . . ,nj,Dj) H . . , m l as a domain: {m 1 ↦ age 1 ; . . . ; m l ↦ age l }. The age 1 , . . . , age l are the age of the trail when the corresponding tag was added. The propagation rules are shown in Fig. 4, where n◁ E D means that n has domain D in the Egraph E. Even if DownFalse is not a merge we require the explanation to be added to the trail (at age next age). Merge is not added to the trail because it does not add any information. Fig. 5 shows the conflict analysis rules. Hypotheses H are of the form n 1 = n 2 [age], which is interpreted as a disequality and where ages(H) = {age}. The function originals(n 1 , D 1 , n 2 , D 2 ) computes the origin of a disequality, i.e. the two nodes and the age at which the nodes have been made disequal. Formally, originals(n 1 , D

Conclusion

The concepts and the prototype described in this paper can be further developed and extended to other theories, but we hope the initial development illustrates how an Egraph and domains could form useful features of an MCSAT implementation. We would like to thanks Simon Cruanes for his participation to fruitful discussions.


Marcos Di Iorio

Mireille Bossy

Cyril Mokrani

Antoine Rousseau

Particle tracking methodology for Lagrangian numerical simulations

come

• Reproduce the fluid particle trajectories in order to describe the physical processes involved in the flow.

• Provide a trajectory visualization tool useful for SDM-OceaPos developers and users.

• Create a plug-in version that can be implemented independently from the existing code.

• Automate the methodology customizable to different study cases.

• It was possible to extract and reproduce particle trajectories from the SDM-Ocepos simulation results.

• The tool allows the interpretation of the particle's behavior and helps to understand how it is affected by the Lagrangian algorithm.

• Intuitive parameters, such as trajectory length and particle velocity at the region of interest, can be implemented to customize the image generation.

  image and animation automated generation; 2. Exportable .vtk files for other visualization software (Paraview, Blender, etc.); 3. Eulerian velocity distribution with streamlines; 4. Particle field colored with instant velocity; 5. Select particle tracking starting points, seed-cells and particle trajectory detection region, "net-region"; 6. Particle trajectory visualization and post-treatment (fluctuation reduction, resolution, etc.)


Guillermo Gallardo

Nathalie T H Gayraud

Rachid Deriche

Maureen Clerc

Samuel Deslauriers-Gauthier

Demian Wassermann

Solving the Cross-Subject Parcel Matching Problem using Optimal Transport

Matching structural parcels across different subjects is an open problem in neuroscience. Even when produced by the same technique, parcellations tend to differ in the number, shape, and spatial localization of parcels across subjects. In this work, we propose a parcel matching method based on Optimal Transport. We test its performance by matching parcels of the Desikan atlas, parcels based on a functional criteria and structural parcels. We compare our technique against three other ways to match parcels which are based on the Euclidean distance, the cosine similarity, and the Kullback-Leibler divergence. Our results show that our method achieves the highest number of correct matches.

Introduction

Brain organization displays high variability across individuals and species. Studying brain connectivity therefore faces the challenge of locating homogeneous regions while accounting for this variability. Different techniques have been proposed to parcellate the brain based on its structural connectivity. However, matching the resulting parcels across different subjects is still an open problem in neuroscience. Even when produced by the same technique, parcellations tend to differ in the number, shape, and spatial localization of parcels across subjects [START_REF] Jbabdi | Long-range connectomics[END_REF]. Current theories hold that long-range structural connectivity, namely, extrinsic connectivity, is strongly related to brain function [START_REF] Passingham | The anatomical basis of functional localization in the cortex[END_REF]. Therefore, being able to match parcels with similar connectivity across subjects can help to understand brain function while also enabling the comparisons of cortical areas across different species [START_REF] Mars | Whole brain comparative anatomy using connectivity blueprints[END_REF].

Most of the current methods to match parcels across subjects are strongly linked to the technique used to create them. For example, Moreno-Dominguez et al. [START_REF] Moreno-Dominguez | A hierarchical method for whole-brain connectivity-based parcellation[END_REF] seek correspondences between dendrograms created by means of Hierarchical Clustering. Parisot et al. [START_REF] Parisot | Tractography-Driven Groupwise Multi-scale Parcellation of the Cortex[END_REF] impose the consistence of parcels across subjects while creating the parcellation. In recent works Mars et al. propose to use the Manhattan distance, cosine similarity [START_REF] Mars | Comparing brains by matching connectivity profiles[END_REF] or the Kullback-Leibler (KL) divergence [START_REF] Mars | Whole brain comparative anatomy using connectivity blueprints[END_REF] to compare and match connectivity fingerprints, successfully identifying common areas across humans and primates. Fig. 1: From the cortico-cortical structural connectivity matrix of a subject, we can estimate the connectivity fingerprints of each parcel in three different types of parcellations. For each parcellation we compute the amount of correct matches (green lines) that each matching technique produces.

In this work, we propose to match parcels based on their extrinsic connectivity fingerprint using Optimal Transportation theory. Optimal Transport (OT) is a technique that seeks the optimal way to transport mass between probability distributions. While KL divergence computes the difference between two distributions, OT computes a matching between them. In particular, our method adopts a discrete regularized version of Optimal Transport (OT), which has been presented in Gayraud et al. [START_REF] Gayraud | Optimal transport applied to transfer learning for p300 detection[END_REF] and Courty et al. [START_REF] Courty | Optimal transport for domain adaptation[END_REF] as a solution to the domain adaptation problem.

We validate our method with four different experiments. In the first experiment, we test the feasibility of our method by generating parcels with synthetic connectivity fingerprints and matching them. In the second one, we show that our technique is able to match parcels of the same atlas across subjects. We use the anatomical atlas of Desikan [START_REF] Desikan | An automated labeling system for subdividing the human cerebral cortex on MRI scans into gyral based regions of interest[END_REF] as its parcels have high spatial coherence and consistent connectivity profiles across subjects [START_REF] De Reus | The parcellation-based connectome: Limitations and extensions[END_REF]. Finally, we show the capacity of our method to match parcels generated with the same criteria but have some spatial cross-subject variability. We assess this for two different situations. In the first one, we derive the parcels from functional activations [START_REF] Barch | Function in the human connectome: Task-fMRI and individual differences in behavior[END_REF]. We use responses to motor and visual stimuli since they have been shown to be strongly related to structural connectivity [START_REF] Osher | Structural Connectivity Fingerprints Predict Cortical Selectivity for Multiple Visual Categories across Cortex[END_REF][START_REF] Penfield | Epilepsy and the Functional Anatomy of the Human Brain[END_REF]. In the second one, we divide the Lateral Occipital Gyrus in 3 parcels using a structurally-based parcellation technique [START_REF] Gallardo | Groupwise structural parcellation of the whole cortex: A logistic random effects model based approach[END_REF]. We use the Lateral Occipital Gyrus since it has been shown to have a consistent parcellation across subjects [START_REF] Thiebaut De Schotten | Rostro-caudal Architecture of the Frontal Lobes in Humans[END_REF][START_REF] Gallardo | Groupwise structural parcellation of the whole cortex: A logistic random effects model based approach[END_REF]. The outline of the last three experiments can be seen in Figure 1.

In each experiment, we compare our technique against three other ways to match parcels based on the Euclidean distance; the cosine similarity; and the Kullback-Leibler divergence. Our results on real data show that our method based on OT always achieves the highest number of correct matches.

Given two subjects with their respective parcellations, we compute their parcel matching by considering one as the origin and the other one as target. More formally, let X a = {x a i } Na i=1 , x a i ∈ Ω a ⊂ R n be an origin dataset where N a denotes the number of parcels; x a i is the extrinsic connectivity fingerprint of parcel i; and n denotes its dimension. We wish to recover a matching between X a and a target dataset

X b = {x b i } N b i=1 , x b i ∈ Ω b ⊂ R n .
In this section, we start by formulating our regularized discrete OT-based method and proceed by presenting three ways of computing this matching that are based on the Euclidean distance; the cosine similarity; and the KL-divergence.

Discrete Regularized Optimal Transport

Optimal Transport (OT) theory boils down to finding the optimal way to transport or redistribute mass from one probability distribution to another with respect to some cost function. In this work, since the datasets X a and X b are discrete datasets, we use their empirical probability distributions and apply the discrete formulation of OT [START_REF] Gayraud | Optimal transport applied to transfer learning for p300 detection[END_REF][START_REF] Courty | Optimal transport for domain adaptation[END_REF] to solve the parcel matching problem. A simplified example of how our method proceeds is presented in Figure 2.

Assume that X a and X b follow probability distributions p a (x a ) and p b (x b ), respectively. We suppose that X a has undergone a transformation T :

Ω a → Ω b , such that p b (T(x a )) = p b (x b
). We wish to recover T and use it to match the parcels of X a and X b . Using discrete regularized OT we compute a transport plan γ 0 between these two probability distributions. This transport plan is a doubly stochastic matrix which minimizes a certain transportation cost C over the vectors of X a and X b . In other words, it defines the optimal exchange of mass between the two probability distributions. We use γ 0 to compute an estimation T by selecting the pairs of vectors, i.e., parcels that exchange the most mass.

Since p a (x a ) and p b (x b ) are not known, we use the corresponding empirical

distributions µ a = N a i=1 p a i δ x a i and µ b = N b j=1 p b j δ x b j instead
, where p a i and p b j are the probability masses associated to each sample. However, given that the dimension of our data depends on the number of vertices in the cortical mesh, the curse of dimensionality makes the estimation of µ a and µ b intrinsically difficult. We therefore simply assume a uniform probability distribution over all vectors,

p a i = 1 N a and p b j = 1 N b .
We compute the transport plan γ 0 such that, if

B = γ ∈ (R + ) Na×N b | γ1 N b = 1 N a 1 Na , γ T 1 Na = 1 N b 1 N b (1)
denotes the set of all doubly stochastic matrices whose marginals are the probability measures µ a and µ b , where 1 N is an N -dimensional vector of ones, then γ 0 ∈ B is the output of the following minimization problem. The matrix C, where

γ 0 = arg min γ∈B γ, C F + λ i,j γ(i, j) log γ(i, j) (2)
C(i, j) = x a i -x b j 2 2
, represents the cost of moving probability mass from location x a j to location x b i , in terms of their squared Euclidean distance. The rightmost term is a regularization term based on the negative entropy of γ allows us to solve this optimization problem using the Sinkhorn-Knopp algorithm [START_REF] Cuturi | Sinkhorn distances: Lightspeed computation of optimal transport[END_REF] which improves the computation time.

Matrix γ 0 contains information about the exchange of probability mass between the vectors of X a and X b . By construction, this exchange depends on the selected cost function. The choice of the squared euclidean distance is motivated both by the fact that it renders the optimization problem convex and because it will allow the parcels to be matched according to the vicinity of their feature vectors. Hence, the origin feature vectors will distribute their corresponding probability mass to the target feature vectors that are closest to them. Consequently, we define T : Ω a → Ω b as T(x a i ) = x b ĵ where ĵ = arg max j γ 0 (i, j). Therefore, i will be matched to the parcel ĵ that it sent the most mass to.

Matching Parcels Based on Dissimilarity Between Features

Let d(x a i , x b j ) be some dissimilarity measure between the elements of X a and X b . Then, we say that parcel i matches parcel j if arg min k d(x a i , x b k ) = j. We compare three dissimilarity measures against our method. First, we use the Euclidean distance, which can be interpreted as matching the parcel i to the parcel j whose feature vector x b j is the closest to x a i . Then, we use the cosine similarity, which is minimized when two feature vectors are colinear. Lastly, we use the Kullback-Leibler divergence, which measures the difference between two probability distributions in terms of their relative entropy. Note that we need to convert our vectors into probability vectors in order to evaluate d KL .

Experiments and Results

Data and Preprocessing

For this work we randomly selected 20 subjects from the S500 group of the Human Connectome Project (HCP), all preprocessed with the HCP minimum pipeline [START_REF] Glasser | The minimal preprocessing pipelines for the Human Connectome Project[END_REF]. Fiber orientation distributions functions where computed using spherical constrained deconvolution with a spherical harmonic order of 8. Probabilistic tractography was then performed using 1000 seeds per vertex of the cortical mesh provided with the HCP data. For each subject, we computed a connectivity matrix by counting the number of streamlines that connect each pair of vertices of the cortical mesh. Each row in the matrix is a vertex connectivity vector, representing the probability that a connection exists between a surface vertex and the rest of the surface's vertices.

Given a whole brain cortical parcellation, we compute the connectivity fingerprint of each parcel by averaging the connectivity fingerprint of its vertices. Because the mesh's vertices are coregistered across subjects [START_REF] Glasser | The minimal preprocessing pipelines for the Human Connectome Project[END_REF], we are able to compare the connectivity fingerprints across subjects. The criterion to compute the parcel matching between two subjects is the similarity between connectivity fingerprints. That is, we match two parcels if they are connected to the rest of the brain in a similar manner. Due to the distance bias that occurs in tractography, a parcel tends to be highly connected to the vertices that compose it. To prevent the matching to be influenced by this bias, we disconnect each parcel from its own vertices.

Matching Parcels

In this section we evaluate the performance of our method by comparing it to the methods presented in Section 2.2. For each experiment we compute parcel matchings between all possible pairs of connectivity matrices. To quantify the result of each technique, we compute the accuracy in terms of percentage of correctly matched parcels per pairwise matching.

Matching parcels with synthetic fingerprints. In this first experiment, we test the feasibility of our method by generating parcels with synthetic connectivity fingerprints and matching them. We start by generating a connectivity matrix M using probabilistic Constrained Spherical Deconvolution based tractography to use as ground truth. Our ground truth matrix is a square matrix that represents the connectivity between the 64 parcels of the Desikan atlas in one subject of the HCP dataset. Each coefficient M (i, j) = θ ij is the parameter of a random variable that follows a Bernoulli distribution X ij B(θ ij ). This variable X ij represents the probability of a connection existing between the parcels i and j. Using M , we generate 20 synthetic matrices in such a way that the coefficients of each synthetic connectivity matrix are random variables that follow a binomial distribution X(i, j) ∼ B(p = M (i, j), n). By doing this we simulate doing tractography for various values of the number n of particles. Figure 3a shows the performance of each method as a function of n. Matching parcels of the Desikan Atlas. For each subject, we compute the connectivity fingerprint of each parcel in their Desikan atlas as explained in Section 3.1. When matching parcels across subjects, Figure 3b shows that on average OT achieves an accuracy of 98%±2%, followed by cosine similarity (94%±3%), KL divergence (87%±4%), and finally Euclidean distance (77%±11%).

Matching parcels created using functional criteria. Each subject in the HCP dataset possesses z-score maps representing responses to different stimuli obtained with functional MRI (fMRI) [START_REF] Barch | Function in the human connectome: Task-fMRI and individual differences in behavior[END_REF]. We derive parcels for each subject from the responses to motor (hand, foot and tongue movement) and visual stimuli (faces vs shape recognition). We do so by keeping only the vertices whose z-score is in the top 35%. Figure 3b shows that OT performs best with an average of 98%±6%. The cosine similarity, KL divergence, and Euclidean distance achieve average accuracies of 97%±6%, 92%±10%, and 90%±13% respectively.

Matching parcels created using structural criteria. For each subject, we first mask their Lateral Occipital Gyrus using the Desikan atlas. Then, we divide it into 3 parcels using the structural based parcellation technique of Gallardo et al. [START_REF] Gallardo | Groupwise structural parcellation of the whole cortex: A logistic random effects model based approach[END_REF]. Once more, we can see on Figure 3b that optimal transport has the highest average accuracy, equal to 92%±16%. It is followed by the cosine similarity, the KL divergence, and the Euclidean distance, whose average accuracies equal 85%±17%, 84%±17%, and 75%±17%

Discussion

In this work we proposed a method to match parcels across subjects based on the connectivity fingerprint of a parcel.

We tested our method with four different experiments. In the first experiment our technique correctly matched connectivity fingerprints created in a synthetic way. Specifically, each entry in a fingerprint was sampled from a Binomial distribution, whose parameter was chosen as the corresponding value of a ground truth connectivity matrix. This can be thought as a simulation of the process of tracking in tractography with different number of streamlines.

Our second experiment shows that we can correctly match parcels of the Desikan atlas across subjects with a 98% of correct matches. The parcels of the Desikan atlas are known to have high spatial coherence and consistent connectivity profiles across subjects [START_REF] De Reus | The parcellation-based connectome: Limitations and extensions[END_REF]. We therefore use this experiment as a reference point to benchmark our technique. The last two experiments show that our technique can match parcels generated with a same criteria, even when they have some spatial variability across-subjects. The first experiment uses parcels created from the functional response to specific motor and visual stimuli, known to be strongly linked to functional connectivity [START_REF] Osher | Structural Connectivity Fingerprints Predict Cortical Selectivity for Multiple Visual Categories across Cortex[END_REF][START_REF] Penfield | Epilepsy and the Functional Anatomy of the Human Brain[END_REF]. The second one, parcels created from the structural parcellation of the Lateral Occipital Gyrus, a structure documented to have a consistent structural division [START_REF] Thiebaut De Schotten | Rostro-caudal Architecture of the Frontal Lobes in Humans[END_REF][START_REF] Gallardo | Groupwise structural parcellation of the whole cortex: A logistic random effects model based approach[END_REF].

It's important to notice that our technique achieved more than a 90% of correct matches in every experiment with real data. Given that we used 20 subjects, this represents a total of 20x19=380 cross-subject matches. In the case of the Desikan atlas, which possesses 64 parcels, this translates into a total of 24320 matches, from which 98% where correctly matched. Furthermore, when tested with a paired t-test to compare the number of correct matches, our method always performs significantly better than the other three (p < 10 -256 ).

Conclusion

Matching structural parcels across different subjects is an open problem in neuroscience. In this work, we proposed a novel parcel matching method based on Optimal Transport. We tested its performance with four different experiments, always obtaining the highest number of correctly matched parcels, which is an improvement over the results of the currently used techniques. Our technique could have major implications in the study of brain connectivity and its relationship with brain function, allowing for the location of parcels with similar connectivity but not high spatial coherence. Also, it could help to understand the link between different brain atlases, and improve the comparisons of cortical areas between higher primates.

  Fig.2: A 2-d example of using OT to compute the matching between two different datasets. On the left we show the original and target datasets. The real matchings are displayed as green dashed edges. In the middle, the edge densities represent the values of the computed coupling γ0, which denote the amount of mass that is exchanged between vectors x a i and x b j . On the right, we see the recovered matching. The blue edges represent the correct matchings, while the red dotted edges represent the incorrect ones.

Fig. 3 :

 3 Fig.3: Proportion of parcels correctly matched by each method (see section 2.2) when matching: (a) synthetic connectivity fingerprints and (b) connectivity fingerprints of a cortical parcellation, for three different parcellations (as described in section 3.2). OT always performs significantly better.

Acknowledgements

This work has received funding from the European Research Council (ERC) under the Horizon 2020 research and innovation program (ERC Advanced Grant agreement No 694665 : CoBCoM), and from the ANR NeuroRef


Dr Marine Riou
email: marine.riou@curtin.edu.au

Stephen Ball

Teresa A Williams

Austin Whiteside

Peter Cameron

Daniel M Fatovich

Gavin D Perkins

Karen Smith

Madoka Janet Bray

Madoka Inoue

Kay L O'halloran

Paul Bailey

Deon Brink

Judith Finn

Keywords: Out-of-hospital cardiac arrest, recognition, agonal breathing, emergency medical services, dispatch, emergency calls, communication, conversation analysis

published or not. The documents may come

Introduction

During emergency medical calls, after determining whether the patient is conscious, calltakers ask callers whether the patient is breathing, and/or whether the patient is breathing normally. Breathing assessment is a challenging task for callers [START_REF] Møller | Debriefing bystanders of out-of-hospital cardiac arrest is valuable[END_REF] as well as for call-takers, [START_REF] Bohm | Tuition of emergency medical dispatchers in the recognition of agonal respiration increases the use of telephone assisted CPR[END_REF] but it is commonly used to help identify time-sensitive emergencies such as out-of-hospital cardiac arrest (OHCA). A reflexive breathing pattern referred to as 'agonal breathing' [START_REF] Fukushima | Abnormal breathing of sudden cardiac arrest victims described by laypersons and its association with emergency medical service dispatcher-assisted cardiopulmonary resuscitation instruction[END_REF][START_REF] Vaillancourt | In out-of-hospital cardiac arrest patients, does the description of any specific symptoms to the emergency medical dispatcher improve the accuracy of the diagnosis of cardiac arrest: a systematic review of the literature[END_REF] can sometimes be observed in the first few minutes after cardiac arrest. [START_REF] Haouzi | Breathing patterns during cardiac arrest[END_REF][START_REF] Zuercher | Continued breathing followed by gasping or apnea in a swine model of ventricular fibrillation cardiac arrest[END_REF] Agonal breathing presents a window of opportunity as it indicates that OHCA has recently occurred and therefore there is a higher likelihood of survival [START_REF] Bobrow | Gasping During Cardiac Arrest in Humans Is Frequent and Associated With Improved Survival[END_REF][START_REF] Clark | Incidence of agonal respirations in sudden cardiac arrest[END_REF] if cardio-pulmonary resuscitation (CPR) is started immediately. The paradox [START_REF] Rea | Agonal respirations during cardiac arrest[END_REF] is that lay rescuers often mistake agonal breathing for effective breathing and thus OHCA patients can be incorrectly assessed as breathing [START_REF] Alfsen | Barriers to recognition of out-of-hospital cardiac arrest during emergency medical calls: a qualitative inductive thematic analysis[END_REF][START_REF] Hauff | Factors impeding dispatcher-assisted telephone cardiopulmonary resuscitation[END_REF], thereby delaying any resuscitation attempt.

The question of whether the patient is breathing is binary and seeks to elicit a "yes" or "no" answer. However, callers often volunteer additional information about the patient's breathing ("yes but barely"). Previous research has identified common descriptors [START_REF] Fukushima | Abnormal breathing of sudden cardiac arrest victims described by laypersons and its association with emergency medical service dispatcher-assisted cardiopulmonary resuscitation instruction[END_REF][START_REF] Clark | Incidence of agonal respirations in sudden cardiac arrest[END_REF][START_REF] Bång | Interaction between emergency medical dispatcher and caller in suspected out-of-hospital cardiac arrest calls with focus on agonal breathing. A review of 100 tape recordings of true cardiac arrest cases[END_REF] These are typically integrated into the dispatch protocols used by Emergency Medical Services. For example, the Medical Priority Dispatch System (MPDS) [14] lists the following terms as indicators of ineffective/agonal breathing: "barely breathing", "can't breathe at all", "fighting for air", "gasping for air", "just a little", "making funny noises", "not breathing", and "turning blue/purple".

However, even with such descriptors in place, agonal breathing remains a major barrier to the recognition of OHCA at dispatch and thus delays initiation of bystander-CPR [START_REF] Hauff | Factors impeding dispatcher-assisted telephone cardiopulmonary resuscitation[END_REF][START_REF] Hardeland | Factors impacting upon timely and adequate allocation of prehospital medical assistance and resources to cardiac arrest patients[END_REF][START_REF] Dami | Time to identify cardiac arrest and provide dispatch-assisted cardio-pulmonary resuscitation in a criteria-based dispatch system[END_REF][START_REF] Travers | Out-of-hospital cardiac arrest phone detection: Those who most need chest compressions are the most difficult to recognize[END_REF] Interpreting what callers say is not just a matter of which keywords are said, but also of the overall context of their answers. This study aimed to determine whether the type of sentence used by callers in response to the question "Is s/he breathing?" had an impact on call-taker recognition of agonal breathing and thus, identification of OHCA.

Methods

Data collection

We retrospectively analysed a random selection of emergency medical calls received by St John Ambulance Western Australia (SJA-WA) between 1 January 2014 and 31 December 2015 for paramedic-confirmed OHCA that occurred in Perth. A flowchart for the data collection is presented in Fig. 1. As detailed in the over-arching study protocol, [START_REF] Riou | The linguistic and interactional factors impacting recognition and dispatch in emergency calls for out-of-hospital cardiac arrest. A linguistic analysis study protocol[END_REF] there were 3513 OHCA cases attended by SJA-WA paramedics during the study period. Of those, 1382 cases met the following initial criteria: non-traumatic OHCA in adults (≥14 years old) where the paramedics attempted resuscitation, no impediment to paramedic attendance, incidents with a single OHCA patient, OHCA not witnessed by paramedics, and cases for which the dispatch data were available. Due to the detailed analysis involved, we were unable to examine every call, thus a randomly selected subset was used. The cases meeting the initial criteria were listed in a randomised order (using Microsoft Excel 2013). We worked through this list sequentially until reaching the target of 200 cases: 100 calls in which cardiac arrest was recognised by the call-taker and 100 calls in which cardiac arrest was not recognised by the call-taker. This stratification by OHCA recognition was necessary because non-recognition is rarer (estimated <15% for the study period), and yet, these cases provide invaluable insight as to what linguistic factors can negatively impact dispatch. We excluded the following: cases in which the patient was unequivocally conscious, the caller was not a lay bystander, the caller was not on scene, the caller and/or call-taker was not a native speaker of English, and calls with very poor sound quality.

After listening to the 200 randomly selected calls, we excluded a further 12 calls: 7 calls because the call-takers did not ask the question "is s/he breathing?"; 3 calls because the calltakers asked two protocol questions at the same time ("and he's not awake and not breathing is that right?"); and 2 calls because the call-takers asked the question in a negative format ("and he's not breathing at all?"). Closer inspection of the electronic Patient Care Records led to the exclusion of 12 cases because OHCA was paramedic-witnessed. Consequently, this study was conducted on 176 calls.

Dispatch protocol

During the study period, SJA-WA used the MPDS (version 12.1.3), implemented with the ProQA software. [20] Calls start with a case entry sequence, with the following steps: after confirming (1) the address and (2) telephone number of the emergency, the call-taker (3) delivers the prompt "okay, tell me exactly what happened", and asks the questions (4) "Are you with the patient now?", (5) "How old is s/he?", (6) "Is s/he awake?", and (7) "Is s/he breathing?". Based on the caller's answers, the call-taker assigns the call to one of 32 Chief Complaints, representing the primary nature of the patient's emergency. Depending on the MPDS protocols for specific Chief Complaints, further questions about breathing may be asked after case entry, e.g. "is s/he breathing normally?" in the case of chest pain. This study focuses on initial breathing assessment during case entry, i.e. how callers responded to item (7) "is s/he breathing?" Fig. 2 summarises the overall structure of calls using the MPDS.

Analysis of dispatch data

We retrieved the following data from ProQA for each of the 176 calls: 1. Breathing status entered by call-takers, chosen from four possible options (breathing, not breathing, ineffective, unknown). 2. OHCA recognition: we considered that OHCA was recognised at dispatch in the presence of at least one of the following elements: (a) The dispatch code indicated cardiac arrest, (b) MPDS protocol steps for CPR were taken, (c) Two Priority 1 ("lights and siren") paramedic-staffed ambulances were dispatched, as SJA-WA automatically allocate dual responses to suspected cardiac arrest cases. Initial breathing assessment is the first opportunity to recognise OHCA. However, OHCA can also be recognised later in the call [START_REF] Hardeland | Factors impacting upon timely and adequate allocation of prehospital medical assistance and resources to cardiac arrest patients[END_REF] for patients initially coded as breathing.

Additionally, we investigated the timing of the breathing sequence. The breathing sequence is defined as the pair formed by the call-taker's question ("is s/he breathing?") and the caller's response (e.g., "no"). It can include a third turn, [START_REF] Stivers | Sequence Organization[END_REF][START_REF] Schegloff | Sequence organization in interaction. Volume 1, a primer in conversation analysis[END_REF] i.e., an additional utterance expanding or closing the sequence after the caller's response (e.g., "okay so not breathing"). Two measures of timing were taken:

1. Time to breathing sequence (from call start to call-taker's question), 2. Duration of breathing sequence (from call-taker's question to caller's response, or to third turn if present).

Linguistic analysis

The calls were transcribed following the methodology of Conversation Analysis. [START_REF] Sidnell | The Handbook of Conversation Analysis[END_REF] We coded caller response to the question "is s/he breathing?" using a coding scheme [START_REF] Stivers | A coding scheme for question-response sequences in conversation[END_REF] developed for a cross-linguistic study of question-answer pairs. [START_REF] Enfield | Question-response sequences in conversation across ten languages: An introduction[END_REF] Caller response was classified into two categories (response type):

1. Answers directly addressed the terms of the question. Answers could be a confirmation ("she is") or a disconfirmation ("no"). We refer to confirming answers globally as yes-answers, and to disconfirming answers as no-answers. 2. Non-answer responses did not directly address the terms of the question ("I don't know"). Additionally, we coded caller answers as qualified answers if they contained any words modifying them ("but gasping", "sort of"), and as plain answers otherwise.

Statistical analysis

We used logistic regression to analyse the relationship between response type and OHCA recognition. Time measures were summarised as medians and interquartile ranges (IQR). The Mann-Whitney U test was used to compare the differences in medians by group (OHCA recognised vs. not recognised) for continuous variables (time). A p-value <0.05 was considered statistically significant.

OHCA was subsequently recognised in 22% (14/63) of calls with a plain yes-answer and in 36% (18/50) of calls with a qualified yes-answer. The odds of OHCA recognition were not significantly higher following a qualified yes-answer rather than a plain yes-answer (Odds Ratio 1.96; 95% Confidence Interval 0.86-4.57; p=0.11).

Overall, the median time to the breathing sequence was 56 seconds (IQR 44-72) from call start, and the median duration of the breathing sequence was 5 seconds (IQR 3-10). The median duration of the breathing sequence was significantly shorter (p<0.001) in calls where OHCA was not recognised (median 4 seconds, IQR 3-7) than in calls where OHCA was recognised (median 7 seconds, .

Discussion

This study identified an important area for improvement in emergency medical call-taking. In a dispatch system using the MPDS with known descriptors of agonal breathing, we found a substantial number of missed opportunities to recognise agonal breathing. When callers gave a plain yes-answer ("she is"), there was little reason to suspect cardiac arrest from this response alone. However, there is considerable room for improvement for calls in which callers gave a qualified yes-answers ("yes gasping"). These answers, found in 37% (32/87) of non-recognised OHCA cases, were suggestive of agonal breathing. Yet, in 94% of cases they were interpreted by call-takers as confirmations that the patient was breathing, and their use did not significantly increase the odds of OHCA recognition. As the calls were stratified for OHCA recognition, our results are not representative of the whole population of OHCA cases. However, our study design enabled us to identify qualified yes-answers as a problem category requiring further attention.

We argue that, on top of the challenge of recognising agonal breathing, call-takers also faced a linguistic difficulty. The descriptors of agonal breathing typically appeared in sentences confirming breathing, often right next to the word "yes". This linguistic environment was inherently ambiguous, as qualified yes-answers confirmed that the patient was breathing while undermining this confirmation at the same time. It is unreasonable to expect lay callers to know that agonal breathing is not effective breathing. However, a lay caller will typically realise that the patient's breathing is not normal. It is thus logical that they would describe it as a type of breathing [START_REF] Clark | Incidence of agonal respirations in sudden cardiac arrest[END_REF]. Therefore, we should expect callers to describe agonal breathing as a confirmation ("yes but he's gasping") rather than a disconfirmation ("no he's gasping", invented example).

A linguistic perspective can explain in part the mismatch that we identified between what callers said and how it was treated by call-takers. Research on spontaneous conversation has identified a social preference for confirming answers to questions: it is much more common for speakers to answer "yes" after polar questions ("yes-no questions") than to answer "no". A study conducted on 10 languages [START_REF] Enfield | Question-response sequences in conversation across ten languages: An introduction[END_REF] found that between 72% (in English [START_REF] Stivers | An overview of the question-response system in American English conversation[END_REF]) and 88% (in Korean [START_REF] Yoon | Questions and responses in Korean conversation[END_REF]) of polar questions were answered with a confirmation. This is explained as a preference for agreement between two speakers interacting, [START_REF] Pomerantz | Agreeing and disagreeing with assessments: some features of preferred/dispreferred turn-shapes[END_REF][START_REF] Sacks | On the preferences for agreement and contiguity in sequences in conversation[END_REF] in an effort to promote social solidarity. In the context of cardiac arrest, our findings suggest that lay callers only report the patient as not breathing when they are sure of their assessment (rightly or wrongly). If they have doubts, they tend to report the patient as breathing, but qualify this confirmation. Our results suggest that this is typically where descriptions of agonal breathing fall, which seems to negatively impact on recognition.

Our results on timing suggest a mismatch between the linguistic complexity of caller answers and their interpretation at dispatch. In our data, the breathing sequence was completed in mere seconds (median 5 seconds). This is positive news from the point of view of dispatch efficiency, but raises questions regarding dispatch accuracy. A previous study on the MPDS [START_REF] Clegg | Dispatch-assisted CPR: Where are the hold-ups during calls to emergency dispatchers? A preliminary analysis of caller-dispatcher interactions during out-of-hospital cardiac arrest using a novel call transcription technique[END_REF] found that the median time to establish the patient's age was 5.5 seconds (IQR 3-9). Given how important breathing assessment is for OHCA recognition, it is troubling that, during case entry, the same amount of time is devoted to the patient's age and their breathing status. Our result that the median duration of the breathing sequence was 3 seconds shorter in calls where OHCA was not recognised suggests the importance of taking enough time to listen to caller responses, and especially to what may follow the words "yes" or "s/he is".

Outside of their professional role, call-takers would be less likely to be misled into thinking in terms of absolute "yes" and "no" answers. If they proposed marriage to their partner who responded "yes, sort of", they would probably assign meaning to the qualification and not consider the answer as a clear and resounding "yes". But because dispatch protocols are necessarily structured as decision trees, call-takers are on the lookout for "yes-or-no" answers, and thereby tempted to indiscriminately interpret any "yes" answer as indeed a "yes". This is illustrated in Extracts 7 and 8 in Appendix A: in both instances, the call-taker did not treat the caller's response as satisfying, and pursued a "yes-or-no" answer. [START_REF] Raymond | Grammar and social organization: Yes/no interrogatives and the structure of responding[END_REF] Call-taker training targeted at agonal breathing has been shown to increase OHCA recognition and the frequency of telephone-CPR. [START_REF] Bohm | Tuition of emergency medical dispatchers in the recognition of agonal respiration increases the use of telephone assisted CPR[END_REF][START_REF] Hardeland | Targeted simulation and education to improve cardiac arrest recognition and telephone assisted CPR in an emergency medical communication centre[END_REF] We recommend, based on our retrospective analysis of initial breathing assessment in OHCA calls, that call-takers be trained to be attentive to any qualifications following a breathing confirmation, whether callers say or imply "yes". Future research is needed to prospectively test the effects on dispatch accuracy of implementing this recommendation. It would also be valuable to compare how lay callers describe the patient's breathing in OHCA calls to other calls.

As previously recommended in the literature, [START_REF] Travers | Out-of-hospital cardiac arrest phone detection: Those who most need chest compressions are the most difficult to recognize[END_REF] our results emphasise the importance of listening to the details of what callers say. In their commentary [START_REF] Clawson | Can't breathe' or 'can't breathe at all'' Substance or Semantics?[END_REF] about recent changes to the MPDS (version 13.0), Clawson & Patterson discussed how a second-party caller (a bystander) may say the words "can't breathe" to describe ineffective breathing, but the same words coming from a first-party caller (the patient) who is able to utter them are more appropriately described as breathing with difficulty, rather than breathing ineffectively. Our study provides further support to the notion that linguistic context matters.

Emergency ambulance telephone calls represent something of a black box in terms of research on prehospital care for OHCA. While the literature has identified the need to focus on communication difficulties during calls, [START_REF] Alfsen | Barriers to recognition of out-of-hospital cardiac arrest during emergency medical calls: a qualitative inductive thematic analysis[END_REF][START_REF] Clegg | Dispatch-assisted CPR: Where are the hold-ups during calls to emergency dispatchers? A preliminary analysis of caller-dispatcher interactions during out-of-hospital cardiac arrest using a novel call transcription technique[END_REF][START_REF] Higgins | Communication difficulties during 999 ambulance calls: observational study[END_REF] relatively little is known about what specific aspects of the dialogue between callers and call-takers impact dispatch accuracy and timeliness. Data-driven, observational studies can contribute to the identification of "hurdles", [START_REF] Stokoe | The Conversation Analytic Role-play Method (CARM): A Method for Training Communication Skills as an Alternative to Simulated Role-play[END_REF] i.e., common communication difficulties experienced at certain points during the calls. Rather than defining a priori what the difficulties are, a linguistic analysis of what is said during the calls, and how it is said, can provide valuable insight into the difficulties that are actually encountered, and how to resolve them. Following this preliminary step, the hypotheses generated can then be tested prospectively. Our observational study contributes to the first part of this process, in generating the hypothesis that a certain aspect of the language used by callers is challenging for call-takers during initial breathing assessment, which seems to negatively impact dispatch performance.

A caveat of our study is the assumption that the patients had already arrested before the start of the call. By definition of our cohort, all patients were confirmed by paramedics as having arrested at the time of their arrival at the scene, however, some patients may have arrested in the interval between the start of the call and when paramedics arrived. We sought to minimise this possibility by excluding cases in which there were unequivocal signs that the patient was still conscious (as evidenced through their voice being heard during the call). [START_REF] Riou | The linguistic and interactional factors impacting recognition and dispatch in emergency calls for out-of-hospital cardiac arrest. A linguistic analysis study protocol[END_REF] Another caveat of this study is that it was conducted on a sample of calls stratified by OHCA recognition. Though our sample size of 176 calls stands in the upper range of previous studies analysing the dialogue between caller and call-taker in OHCA calls (e.g., 21 calls, [START_REF] Alfsen | Barriers to recognition of out-of-hospital cardiac arrest during emergency medical calls: a qualitative inductive thematic analysis[END_REF] 47 calls, [START_REF] Clegg | Dispatch-assisted CPR: Where are the hold-ups during calls to emergency dispatchers? A preliminary analysis of caller-dispatcher interactions during out-of-hospital cardiac arrest using a novel call transcription technique[END_REF] 82 calls, [START_REF] Travers | Out-of-hospital cardiac arrest phone detection: Those who most need chest compressions are the most difficult to recognize[END_REF] 100 calls, [START_REF] Bång | Interaction between emergency medical dispatcher and caller in suspected out-of-hospital cardiac arrest calls with focus on agonal breathing. A review of 100 tape recordings of true cardiac arrest cases[END_REF] 267 calls [START_REF] Culley | Dispatcher-assisted telephone CPR: Common delays and time standards for delivery[END_REF]), it does not preclude potential issues of representativeness.

Conclusion

Analysing a sample of emergency ambulance calls stratified by recognition of OHCA, this study identified a problem with call-taker interpretation of breathing status, resulting in potential delays in cardiac arrest response time. When asked whether the patient was breathing, lay callers often responded with words typically associated with agonal breathing, such as "gasping". Yet, call-takers overwhelmingly considered these answers as confirmations that the patient was breathing. We argue that the linguistic format of these qualified breathing confirmations ("yes but gasping") was challenging for call-takers because of their inherent ambiguity. We propose that dispatch performance could be improved if call-takers spent more time assessing breathing status and were trained to listen closely for any qualification that callers express when they report the patient as breathing. This is irrespective of whether "yes" is said or implied, as this is how lay callers typically describe agonal breathing.

Fig. 1 .

 1 Fig. 1. Data collection flowchart.

Fig. 2 .

 2 Fig. 2. Overall structure of calls with the Medical Priority Dispatch System.

This work has been supported by an NHMRC Partnership Project between Curtin University and St John Ambulance Western Australia (APP1076949 'Improving ambulance dispatch to time-critical emergencies').

Ethics

Approval for the study was granted by the Human Research Ethics Committee of Curtin University (HR128/2013) and the SJA-WA Research Advisory Group.

Results

Among all cases (recognised and non-recognised), the breathing question received an answer in 89% (157/176) of calls and a non-answer response in 11% (19/176) of calls (see Appendix A for examples). Among the 157 calls where the response was categorised as an 'answer', more callers gave a yes-answer (113 calls) than a no-answer (44 calls). Thus, 64% (113/176) of the patients were initially reported by callers as breathing (Table 1). OHCA was recognised in 28% (32/113) of calls with a yes-answer, 95% (42/44) of calls with a noanswer, and 79% (15/19) of calls with a non-answer response.

Callers often volunteered additional details: 32% (51/157) of answers to the breathing question were qualified (Table 1). Qualification was found in 44% (50/113) of yes-answers. Most of these qualified yes-answers (32/50) were composed of two parts: a response particle (yes/yeah/yep) and/or partial repeat (s/he is), as well as a qualification of this confirmation of breathing ("but gasping"). Some qualified yes-answers (18/50) solely expressed the qualification ("only just"), yet logically implying a confirmation of breathing. In these qualifications, callers described problematic aspects of the patients' breathing: questioning its very presence ("yep just"), difficulty ("yes but she's battling"), irregularity ("uh intermittently"), abnormal depth ("very-faint noises"), unusual sounds ("yes he's snoring"), or mentioning another symptom causing them concern ("breathing he's a bit grey"). Only 2% (1/44) of no-answers were qualified ("no he's not really he's got a little breath here and there but that's-").

Despite the fact that qualified yes-answers were suggestive of agonal breathing, they were treated similarly to plain yes-answers. Call-takers entered in ProQA that the patient was breathing after 94% (47/50) of qualified yes-answers and 94% (59/63) of plain yes-answers.