Andreas Fellner
email: andreas.fellner@ait.ac.at

Pascal Fontaine
email: pascal.fontaine@inria.fr

Bruno Woltzenlogel Paleo
email: bruno.wp@gmail.com

David Déharbe

Yoann Guyot
email: yoann.guyot@cetic.be

Laurent Voisin
email: laurent.voisin@systerel.fr

Stephan Merz
email: stephan.merz@inria.fr

Thomas Bouton
email: thomas.bouton@loria.fr

Diego Caminha
email: diego.caminha@loria.fr

B De Oliveira

NP-completeness of small conflict set generation for congruence closure

Keywords: Satisfiability Modulo Theories, Decision procedures, Congruence closure, Complexity Formal methods, Event-B, SMT solving

About this

1 Introduction: on the importance of SMT Propositional Satisfiability (SAT) and Satisfiability Modulo Theories (SMT) have many industrial applications that should suffice to convince anyone of the interest to study this field. My involvement was mainly around verification; I contributed to the integration of SMT within verification platforms (Rodin, Atelier B) and interactive theorem provers with some success. However, if this serves well to justify my salary, the very reason for my interest for SMT does not rely on industrial applications. My previous life as a physics student gave me the very uncomfortable feeling that scientific reasoning is sometimes extremely imprecise, even when the right conclusions are drawn. I have found myself many times guilty of having completely false intuitions, and sometimes even writing very wrong proofs. I believe now that most hand written proofs are wrong or miss details, and a good hand written proof is not a correct one, but one that can easily be corrected. Rigor and precision are not easy to achieve. When the meanders of life brought me by pure chance to logic and to the right people to study it with, it was clear that I wanted to contribute to it. I was impressed by computer scientists who spend considerable time and energy to model, completely formally, large fragments of mathematics inside interactive theorem provers. In my very naive understanding of the world as a post teenager, I was even believing that some day, we would do the same with physics, chemistry, economy, law and politics. Part of this dream still lives on.

It was clear at that time that interactive theorem provers, although already awesome, were not yet perfect. In particular, automation was lacking. My bottom-up attitude to everything -after all, I studied physics to understand the world, and logic at first because I was unsatisfied with my sloppy understanding of the reasoning rules underlying physics -led me directly to propositional satisfiability checking. It was though also already clear to me that arithmetic, first-order logic, and quantifiers were to be added to the game for expressivity. In another environment or with a slightly different little influence, my core interest might have been superposition theorem proving [10,[START_REF] Nieuwenhuis | Paramodulation-based theorem proving[END_REF], but I discovered STeP (The Stanford Temporal Prover [23,[START_REF] Manna | STeP: The stanford temporal prover[END_REF]) and SVC (The Stanford Validity Checker [18], the ancestor of CVC4 [14]). Basically, my main research topic was settled on SMT. I can proudly assert that I never thought SMT would solve all problems easily. Indeed this has occupied me for nearly twenty years now.

In the first chapters, I will provide an informal and personal introduction to SAT and SMT. The next chapters are dedicated to some of my research directions, where I will present my contributions and objectives. The last chapter is a digression with a plan for educating young computer scientists to the basics of computer science alongside my research interests.

A gentle introduction to SAT and SMT

It is not easy to understand the true reasons for the success of classical propositional logic, propositional logic for short in the following. It is arguably not the historical foundation of logic, Artistotle's syllogistic logic [6] being closer to first-order predicate logic than to propositional logic. Without a clear definition of simplicity, propositional logic can also not be said to be the simplest logic: intuitionistic propositional logic actually does not impose the law of the excluded middle, and in that sense, is simpler. But considering intuition, classical propositional logic is unchallenged: it is very easy to make children and students believe a proposition is either true or false, and quickly understand in this context the basic notions of logic, e.g., satisfiability, equivalence or what is a decision procedure. While the expressivity of propositional logic is quite limited, many relevant problems can be encoded within classical propositional logic. Last, but not least for our part, propositional logic is the basis of a series of logic with increasing expressivity. The methodology used in SMT solving values this, eventually reducing expressive languages into propositional logic.

The SAT problem, i.e., checking the satisfiability of propositional formulas, is an NP-complete problem. It is in NP, since it is possible to check in polynomial time if a formula is true under a given valuation of the propositions, assigning to each of them either the value true or false. It is NP-hard since any problem in NP can be encoded polynomially into SAT [START_REF] Cook | The complexity of theorem-proving procedures[END_REF]. The SMT problem includes the SAT problem, that is, a SAT formula can be seen as an SMT formula, for the usual theories of interest. Thus SMT is NP-hard. Depending on the background theory and the restriction of the input language, the SMT problem may also be in NP. This is indeed the case whenever the satisfiability problem for conjunctive sets of literals in the SMT logic is itself in NP, e.g., for quantifier-free first-order logic with uninterpreted functions and predicates (see e.g., [START_REF] Nelson | Fast decision procedures based on congruence closure[END_REF]), and linear arithmetic on rationals and integers (see e.g., [START_REF] Papadimitriou | On the complexity of integer programming[END_REF]). In this context, solving the SMT problem with the help of a background SAT solver can just be seen as an on-the-fly encoding of an NP-complete problem into another. In the solving techniques, just like for the above complexity considerations, propositional SAT solving is central.

Solving the SAT problem

The paradigm at the core of most modern SAT solvers is Conflict-Driven Clause Learning (CDCL, see Chapter 4 of the Handbook of Satisfiability [22]). It is often claimed to be a refinement of the DPLL algorithm, by Davis, Puttnam, Logemann and Loveland [START_REF] Davis | A computing procedure for quantification theory[END_REF][START_REF] Davis | A machine program for theorem-proving[END_REF]. There is no doubt that the ideas in DPLL were of primal importance to the design of modern SAT solvers. But ignoring the history of the design of CDCL and understanding CDCL starting from truth tables might just be easier.

Checking if a propositional logic formula can be true or not can be as simple as checking the truth value for each possible assignment, i.e., building a truth table. Each line in the truth table states one assignment, and since there are only 2 n possible valuations assigning true or false to n propositional variables, a truth table for a formula with n variables contains 2 n lines. Creating the whole truth table is exponential in space, but keeping track of every assignment is of course not required. An algorithm using linear space would simply iterate over the assignments; when a satisfying assignment is found, the algorithm stops and declares the formula to be satisfiable. Let us however assume that the algorithm records the "failed" assignments, i.e., the ones that have been tried but do not satisfy the formula. The algorithm now picks successive assignments in no particular order, and uses exponential space to record them. Surprisingly, this makes the naive and inefficient algorithm of truth tables quite close to the state-of-the-art and efficient CDCL framework: iterating over assignments is also at the core of CDCL. Although CDCL does not record failing assignments, it learns conflict clauses, standing for all the assignments making this clause false, i.e., a set of failing assignments.

Consider now a formula (b 1 ∨ b 2 ) ∧ G(b 3 , . . . b n ) over n Boolean variables b 1 , . . . b n . Obviously, if b 1 and b 2 are false, it is not necessary to complete the assignment with valuations for b 3 , . . . b n and check every of the 2 n-2 possible completions. Provided the algorithm can detect some cases of unsatisfiability with partial assignments, this can lead to a dramatic improvement over checking all 2 n full assignments. If the formula is a set of clauses, i.e., a conjunctive set of disjunctions of literals, the algorithm could for instance detect when a clause is false under the current partial assignment, that is, when all its literals are set to false by the current partial assignment. Assuming that the input formula is a conjunctive normal form (CNF, a conjunctive set of clauses) significantly simplifies automated reasoning techniques, and the price to pay is reasonable: every formula can be transformed into an equisatisfiable conjunctive normal form in linear time, by introducing new Boolean variables for subformulas, a technique known as Tseitin's transformation [START_REF] Plaisted | A structure preserving clause form translation[END_REF][START_REF] Tseitin | On the Complexity of Derivation in Propositional Calculus[END_REF]. It can be argued that this transformation, even if linear and mostly reversible, potentially hurts the solving since the structure of the formula is somehow lost. In practice, it is easier to find mitigating techniques for this structure loss rather than designing algorithms for arbitrary formulas.

Boolean Constraint Propagation (BCP)

Although we just promised a dramatic improvement in the truth table algorithm by detecting unsatisfiable clauses early, we have not yet mentioned how to concretely detect when a clause becomes unsatisfiable, or conflicting, under a partial assignment. This task has to be done for every clause, and each time the partial assignment is extended: simply iterating over the whole set of clauses is thus impractical. If a partial assignment is extended with, let's say, a valuation to true for a propositional variable p, any clause containing p negatively might become conflicting and only those ones. This thus calls for an indexing of clauses by the negations of their literals. If a partial assignment is extended by setting a literal to true, only the clauses in the corresponding list might actually become conflicting.

Notice that, with such an indexing, every conflicting clause with n literals has been examined n times during the building of the partial assignment conflicting with the clause. And it is only useful the last time, i.e., when detecting the conflict. In fact, if a clause is not yet satisfied by the current partial assignment, it is only necessary that it appears in the list associated to the negation of one of its unassigned literals. To guarantee the detection of all conflicting clauses, it then suffices to enforce the invariant that every non-satisfied clause (that is, every clause without any literal set to true under the current assignment) is indexed by at least one of its unassigned literals, called the watched literal. This requires that, each time a literal is set to false, all the clauses indexed by this literal have to be indexed again by another of its literals that is unassigned or true under the current assignment. If it is not possible to find a replacement literal for a clause, the clause is in conflict with the current partial assignment, and no completion of the assignment can satisfy the CNF.

An obvious improvement is possible: rather than building partial assignments until a clause gets conflicting, it is much more profitable to extend the partial assignment as soon as a clause, called unit, imposes a choice on the assignment. In other words, if all the literals of a clause but one are false under a partial assignment, then the last literal should be set to true. This is called propagation: partial assignment are extended with the aim of satisfying clauses rather than relying on guesses to make the clause true. Again, a possible but inefficient way to detect such propagating clauses would be to check all clauses every time a partial assignment is extended by a new literal. But it is also easy to improve the above technique based on watched literals to also accommodate propagation. To ensure detection of conflicts, it is necessary to have one (watched) unassigned literal per clause. To detect propagation, it suffices to inspect the clauses whose assigned literals are all false when the next but last unassigned literal becomes false. The same technique still works however, using two watched literals instead of one. The invariant becomes: every non-satisfied clause (that is, every clause without any literal set to true under the current assignment) is indexed by two of its unassigned (watched) literals. Every assignment, let's say, of a literal to false, might break the invariant. To repair it, the algorithm checks every clause with as watched literal, and, if it is not satisfied, ensures that it is indexed by two of its unassigned literals. Concretely, the clause is removed from the list associated to and added in the list associated to another of its unassigned literal while ensuring both watched literals are different. If this fails, it is either because there is only one unassigned literal, in which case the other literal has to be assigned positively immediately, or it is because there is no unassigned literals at all, and then the clause is conflicting. Conflicts can indeed still happen: a clause may have all its literals (including both watched literals) falsified by propagation from other clauses before it is itself considered for propagation. In the assignment stack -the stack of assigned literals by chronological order -some recently assigned literals (e.g., by propagation) may have not been yet fully taken into account for propagation.

Compared to the truth table algorithm with conflict detection on partial assignments, there is now less non-determinism in building the partial assignment. Some literals are now assigned by propagation. It can happen however that no literal can be propagated at some point. Then guessing is used to assign an additional literal, which may or may not trigger propagation. The process stops when a conflict occurs, or no more literal is unassigned, in which case the formula is satisfiable. In case of conflict, either no literal has been guessed and the formula is unsatisfiable, or one or several guessed literals have to be changed. Backtracking is the subject of Section 2.1. 3.

Propagation is a central aspect of SAT solving, drastically reducing guessing and promoting deduction. In modern SAT solvers, the solving time is generally dominated by Boolean constraint propagation, and most literal assignments are due to propagation. Watched literals, first introduced in the Chaff [START_REF] Moskewicz | Chaff: Engineering an Efficient SAT Solver[END_REF] SAT solver, were one essential factor of its success.

Using watched literals rather than a full indexing of clauses by literals trades the examination of each clause every time the partial assignment is extended, for a dynamic index instead of a static one. In modern SAT solving, it appears that this indexing is not as dynamic as one might fear. In a sense, thanks to the decision heuristics, the watched literals of a clause remain quite stable, because the order of assignment is also evolving slowly. The watchers stabilize themselves with respect to this order, i.e., they become the literals assigned last, and remain so for some time.

Conflict Analysis

Propagation prevents extending a partial assignment in an obviously wrong way, when a clause imposes the value of one Boolean variable because all but one of its literals are false. Conflicts can still occur, when a same variable can be propagated both positively and negatively by two different clauses. In such a situation, the partial assignment is not extendable to a model of the formula. The clause comprising the negation of all literals in this partial assignment is a logical consequence of the original formula, and therefore adding it to the formula preserves logical equivalence. It may however be possible to add a stronger clause, i.e., a clause containing only a subset of the negation of the literals in the assignment. This clause records the failing (partial) assignment, and the stronger it is, the more total assignments it discards. Furthermore, it would be nice if such a clause would prevent, through propagation, to reach the same state again. In this context also, a stronger clause is always better: it can be propagating earlier, and may cut out a larger part of the search space.

One admissible stronger clause would contain only the negations of decision literals, i.e., only the (negation of) literals in the assignment that have not been propagated but guessed. All the propagated literals are indeed a consequence by propagation of the decision literals. So if any of those propagated literal is false in a model of the formula, at least one of those decision literal should be false. The clause containing only the negations of decision literals in a conflicting partial assignment is a logical consequence of the original formula. Notice also that this clause is propagating in the expected way: it would prevent the decisions that led to the previous conflict to occur again. It would propagate the variable decided last, with the opposite polarity, cutting off the search space that led to the previous conflict.

Among all the decision literals in the assignment stack in a conflict state, not all decision literals actually contributed to the conflict. To analyze this, it suffices to recall for each propagated literal the clauses that forced this propagation. One may then draw a directed implication graph, where each node is a literal, and its parents are the literals that implied the propagation. A node and all its parents thus represent a propagating clause, the parents corresponding to the negated literals in the clause. The directed graph is acyclic, since no propagated literal is indirectly responsible for its own value. All leafs (i.e., nodes without parents) in this graph are decision literals, since all propagated literals have parents. In a conflicting state, there exists a variable such that both polarities are present in the graph. For convenience, consider that there is a special conflict node whose unique parents are those two literals on the same variable. The interesting part of the implication graph is the conflict graph, i.e., the subgraph rooted by this conflict node. The full graph may have disconnected subgraphs, and many leafs without a directed path to the conflict node. Any decision literal that does not occur in the conflict graph did not take part in the chain of propagations that eventually led to the conflict, and can therefore be removed from the conflict clause.

It occurs that using a conflict clause containing only (the negation of) decision literals is often not the best choice. There indeed exists some freedom. Instead of a (decision) literal, one can for instance select all its consequences. Another legitimate conflict subgraph can be obtained by eliminating recursively from the conflict graph all parents of some nodes. Then, the leafs of this subgraph are a subset of the partial assignment that generate the conflict. It might then contain both decision and propagated literals. In practice, the first unique implication point (FUIP) [START_REF] João | GRASP: A new search algorithm for satisfiability[END_REF] technique gives good results. Starting from the conflicting pair of literals, a growing conflict subgraph is built by repeatedly adding the parents of the literal propagated the latest, until there is only one leaf of the subgraph that is a descendant of the last decision. This leaf can be the decision itself, but it can also be a consequence of it that is sufficient (with all other decisions) to cause the conflict. It is called the first unique implication point. Using the FUIP technique is in practice better than collecting all relevant decision literals. Although there is no absolute theoretical reasons to prefer the FUIP, the rationale is that the unique implication point is in some sense the real reason of the conflict; it appears nearer to the conflict than the last decision literal, and continuing collecting reasons of the FUIP might augment the conflict clause with many more literals.

The above techniques keep only one literal at the last decision level, that is, the last decided literal or one literal propagated after this last decision. At previous decision levels however some literals in the conflict clause may imply some others. The conflict graph can also easily be used to remove such implied literals and thus refine the conflict clause to a stronger one [START_REF] Sörensson | Minimizing learned clauses[END_REF]. In practice, this leads to significant speed-ups.

To refer again to truth tables, conflict analysis is a clever way to not try several times assignments that will fail to provide a model for the same reason, or in other words to cache reasons for failing assignments. The only requirement to the added clause is that it should be a consequence of the original set of clauses. In the case of FUIP conflict analysis, the learned clause is indeed a consequence, by resolution, of all the clauses at play in the conflict. As a side note, we can here notice that it is trivial for CDCL solvers to output resolution proofs of unsatisfiability.

An important question is whether CDCL solvers are able to find short proofs, if they exist. Truth tables cannot, of course, because an exponential number of interpretations with respect to the number of propositional variables have to be checked systematically, whatever the formula is. CDCL however, and mainly thanks to clause learning, is as powerful as general resolution [19]: with the right choices, it can find a short proof if there is a short resolution DAG-like proof.

Non-chronological backtracking

If a conflict is reached while building a partial assignment by deciding literals and using propagation, a conflict clause is learned. This clause can, as explained above, be computed using the FUIP technique, in which case it contains only one literal at the last decision level, i.e., either the (negation of the) last decided literal or one literal propagated after this last decision. Actually, having just one literal at the last decision level is a required feature of the conflict clause generation. Remember that, in the truth table algorithm, failed assignments are stored to avoid to check them several time; the conflict clause plays the same role, but with a bonus. There is no need to check if the conflict clause is invalidated. Thanks to propagation, this clause will prevent the same literals to be assigned again, since as soon as all but one literals involved in the previous conflict are assigned to true, the last becomes assigned to false by propagation. The core of the naive truth table algorithm is an iteration on assignments. In CDCL, conflict analysis and propagation together with backtracking play the role of this iteration loop.

Every time a conflict happens, the conflict clause is learned, and the algorithm backtracks the assignment to the earliest decision level where the conflict clause is propagating. Another possibility would be to only backtrack the last and conflicting decision level and propagate from this point on. Besides experimental evidence, there are arguments however in favor of backtracking to the propagation level of the conflict clause. First, since decisions are to some extent arbitrary, it is preferred to assert every implied literal as soon as possible, soon meaning early in the assignment stack; the next conflict might then be more general, not influenced by the dispensable decision levels. Second, the code to support propagation without backtracking to the propagation level would be more complex, and might induce overhead to the algorithm: the watched literals technique is only applicable for the immediate propagation (when the penultimate literal of a clause becomes false), and is not suitable to remember the literals that have been propagated late.

As a final remark on backtracking, notice that, because the learned clause was computed using the FUIP and not the last decision literal, it may happen that the exact same decisions occur again, with the same order (but the stack would differ on the propagated literals). Some early solvers learned all the unique implication points clauses. It was later noticed that just learning the FUIP clause was experimentally better. It may be useful to reevaluate this in the recent contexts though.

Heuristics

Boolean constraint propagation, conflict analysis, learning and non-chronological backtracking are the core of the CDCL algorithm. Some freedom still exists in the implementation of the algorithm, and in particular, in the procedure that decides which Boolean variable to assign first and which polarity to pick. Remember that, for a satisfiable formula, a perfect decision heuristic would pick literals in such a way that the solver builds a full assignment without conflicting and backtracking, that is, in linear time. This is obviously a hard problem, and also due to the efficient data-structures and in particular the watched literal, the amount of knowledge on which to base the decision is limited. For instance, it could make sense to assign to true the literal occurring most often in non-satisfied clauses, but the solver data-structures do not provide this information at low cost. Modern SAT solvers rely on decision heuristics finely tuned to their inner working. A popular heuristic is the Variable State Independent Decaying Sum (VSIDS) [START_REF] Moskewicz | Chaff: Engineering an Efficient SAT Solver[END_REF], which picks the most active variable first, a very active variable being one involved often in the recent conflicts. As a result, the VSIDS heuristic focuses sequentially on groups of tightly coupled variables.

When a variable is picked as a decision, it can be assigned either false or true. It happens that it is better to remember which polarity it has been last assigned, and picking the same polarity for the decision. This process, called phase caching [START_REF] Pipatsrisawat | A lightweight component caching scheme for satisfiability solvers[END_REF] ensures the solver focuses on one part of the search rather than randomly exploring the search space. Assigning a variable by decision to a new polarity might indeed force the search in a completely different area of the search space. Again as it is the case for many techniques in SAT solving, this explanation comes from experimental observation rather than as a property of the algorithm.

If it is often good for a solver to focus on a part of the search space, and exhaust this part before examining another, this might also have drawbacks, and in particular, the solver might be stubborn at solving less relevant parts of the problem. Restarting (see e.g., [21,[START_REF] Huang | The effect of restarts on the efficiency of clause learning[END_REF] for discussions on restart) the solver is beneficial in practice to get out of a corner, and is used quite a lot in modern tools. This is less fundamental for SMT instances than for hard SAT instances, since the SAT abstraction of SMT problems is most often very easy compared to the SAT problems usually given to solvers.

During the search, a solver generates many clauses, and many of them are used at most a couple of times. Learned clauses however slow down the solver, mostly since they have to be handled in the Boolean constraint propagation algorithm. It thus makes sense to periodically eliminate clauses, and modern solvers typically eliminate most of the learned clauses. Notice however that these might, depending on the strategy, break the completeness of the solver. Useful clauses might also be forgotten.

State-of-the-art solvers also use many techniques to simplify the input problem (preprocessing) [START_REF] Eén | Effective preprocessing in SAT through variable and clause elimination[END_REF], or even to simplify the problem within the search (inprocessing) [START_REF] Järvisalo | Inprocessing rules[END_REF]. Many of those techniques are specific to purely Boolean problems and do not apply to SMT. Others are simply not useful for Boolean abstractions of SMT problems. For instance, a lot of effort has been invested to exploit symmetries in Boolean problems [START_REF] Karem | Symmetry and satisfiability[END_REF]. Our symmetry preprocessing technique [START_REF] Déharbe | Exploiting symmetry in SMT problems[END_REF] (see selection of papers on page 65) tailored for SMT is however much easier to express directly at the SMT level rather than relying on this effort for Boolean symmetry breaking.

Drawbacks of modern SAT solving

If a variable appears only positively (or negatively) in a formula, a satisfying assignment can always be modified to assign this variable to true (resp. false). This simple observation leads to the pure literal rule: if an unassigned variable appears pure -i.e., always with the same polarity -in the unsatisfied clauses, it can be asserted with the polarity making all those clauses true. This is not a proper propagation, since it does not necessarily imply that there is no model with the variable having the opposite polarity, but setting the variable with this polarity cannot hurt. Modern SAT solvers do not use the pure literal rule since the optimized CDCL data-structure does not provide the facilities to quickly detect pure literals (under a given partial assignment). Anyway, the pure literal rule does not hold for Boolean abstractions of SMT formulas -a literal might appear pure although it would appear with opposite polarity in theory clauses -so in our context this is a lesser evil. The pure literal rule is however an example of a good technique that could not find its place in CDCL solvers.

The Boolean constraint propagation is triggered by watched literals. An alternative, less efficient, implementation could count, for each clause, the number of positive and negative literals, and could also take note for each unassigned literal, of how many clauses it could contribute to satisfy if assigned. It would trigger propagation when the number of negative literals in a clause with n literals is n -1, and could implement a counter for satisfied clauses with a marginal cost. The CDCL data-structures in the algorithm do not allow to easily detect when all clauses are satisfied. There is furthermore no way to know if a decision actually helps satisfying clauses. As a consequence, some and even many literals in the stack of a satisfying assignment for a CNF might be unnecessary. Finding good partial satisfying assignments for formulas is important in the context of SMT solving in presence of hard theories or for quantifier handling; for instance, a decision procedure that is given a full assignment will have to deal with many literals irrelevant for satisfiability. We have contributed to an efficient algorithm to compute a minimal implicant (a "best" partial assignment) from a full assignment generated by a SAT solver [START_REF] Déharbe | Computing prime implicants[END_REF].

Solving the SMT problem

In the context of Satisfiability Modulo Theories we consider formulas in more expressive languages than SAT. They may contain functions and predicates.

Variables are not only propositional but may take their value in a domain, either partially or fully specified by the theory, or left uninterpreted. As an example, the UFLIA language (Uninterpreted Functions and Linear Integer Arithmetic) of the SMT-LIB includes the usual Boolean connectives, equality, uninterpreted functions and predicates of any arity (including nullary: constants and propositions), the arithmetic comparison operators, and linear expressions on integers; the sort of each argument of each predicate and function symbol, and of the range of each function, can either be integer or one of finitely many uninterpreted sorts. Typical theories handled by SMT solvers include linear (or non-linear) arithmetic on reals and integers, uninterpreted symbols, arrays, bitvectors, abstract data-types and strings. Some SMT solvers can also reason on quantified formulas, but these quantifiers are currently only first-order.

Historically, research on practical SMT started after satisfiability checking for propositional logic, but quite some time before CDCL. For instance, one could arguably set the birth of modern age SMT to the design of the Stanford Pascal Verifier [START_REF] Nelson | Techniques for program verification[END_REF], the Stanford Temporal Prover STeP [23] used internally some SMT techniques, and the SVC solver [18] is an ancestor of the current CVC4 solver. The first SMT solvers using CDCL were adapting older SMT methods to suit CDCL, but they were not designed as extensions of CDCL for SMT. Only quite recently, with Model-Constructing Satisfiability Modulo Theories (MCSAT) [START_REF] Mendonça De Moura | A modelconstructing satisfiability calculus[END_REF], did the SMT community thoroughly try to extend the various phases (propagation, decision, learning) of CDCL to SMT. The success of CDCL is also starting to drive research on CDCL-inspired procedures for first-order logic [25].

In a propositional context with n variables, there are at any time at most 2n possible decisions and learning will produce a clause among 3 n possible ones since each variable may appear in a clause either positively, negatively, or not at all. If clauses are never forgotten, termination is a direct and trivial consequence of this finite space for the search tree. In an SMT context however, and for instance in presence of integer variables, there are an infinite number of possible decisions (e.g., a given variable may be given any integer value) or propagations (e.g., any bound on a variable might be propagated) and the learned facts can also belong to an infinite space since there are an infinite number of non-equivalent linear constraints that can be part of a learned clause. MCSAT [START_REF] Mendonça De Moura | A modelconstructing satisfiability calculus[END_REF] restores completeness with an explicit side condition that learning should produce clauses on a finite and fixed set of atomic formulas. Nonetheless, the freedom given by MCSAT is extremely large, and the success of current MCSAT-based solvers (see e.g., [START_REF] Jovanovic | Cutting to the chase solving linear integer arithmetic[END_REF][START_REF] Jovanović | Solving non-linear arithmetic[END_REF][START_REF] Haller | Deciding floating-point logic with systematic abstraction[END_REF][START_REF] Zeljic | Deciding bit-vector formulas with mcSAT[END_REF]) relies also on carefully designed heuristics. There is probably still a lot to understand how to optimally convert this freedom into a deterministic framework with a small search space. Classic SMT simply imposes the set of literals to be the obviously finite set of atoms occurring in the input formula. Only those literals can be propagated, and decisions are essentially similar to propositional ones.

Another orthogonal approach to SMT stems not from SAT but from firstorder theorem proving (FOL). Driven by the success of SMT, there are several ongoing initiatives [3,[START_REF] Reger | AVATAR modulo theories[END_REF] to combine theory reasoning within the superposition calculus. Again, for historical reasons, I have not worked on this trend, but the future will hopefully show convergence of both approaches; superposition is clearly the way to handle some types of quantifiers.

From SAT to SMT

Letting aside the urge to generalize CDCL to satisfiability modulo theories, a pragmatic approach is quite simple. Remember that Boolean propagation, early conflict detection, and precise conflict analysis are useful aspects for efficiency, but not mandatory for completeness. Applying them only leniently does not break completeness, but breaks down the behavior of the algorithm closer to the naive truth table approach. With this in mind, one can always view an SMT problem as a propositional problem with a hidden set of theory clauses specifying the relation between the atoms. The CDCL algorithm considers atoms as simple Boolean variables, and propagations only occur at the Boolean level, thanks to the clauses from the input problem, but without contribution from the hidden set of theory clauses. Soundness is recovered simply by discarding each set of literals computed as a model by the CDCL algorithm if it is not satisfiable according to the theory. The major advantage of this approach is that the underlying CDCL algorithm takes care of the Boolean structure of the formula, whereas the decision procedure for the theory only has to deal with conjunctive sets of literals. Refuting the tentative CDCL models is again done by adding new clauses to the original problem, these clauses containing only atoms from the input formula, thus guaranteeing termination. The original formula is abstracted down to a propositional one handled by the CDCL algorithm, and successively refined by the decision procedure that provide the missing clauses; the refinement loop somehow progressively reveals the theory clauses lacking from the original formula, and explaining the meaning of the atoms to the CDCL algorithm.

Unfortunately this approach shares several drawbacks that were already pointed out for truth tables. Indeed, the propositional abstraction is most of the time under-constrained: the CDCL algorithm would enumerate a large number of models, and each of them would have to be refuted one by one, pretty much like every interpretation is examined separately in a truth table. A mandatory improvement is for the theory decision procedure to provide, in case of conflict, a strong theory clause, i.e., a clause that does not contain the negation of all literals in the model of the propositional abstraction, but only of a small, as minimal as possible, subset of those literals. For each variable that is not mentioned in a stronger clause, the amount of models the clause can refute is doubled compared to a clause that would spuriously contain a literal on this variable; there is theoretically and experimentally a potential exponential gain.

Other improvements might be useful: the theory decision procedure might declare unsatisfiability of a partial model while it is built by the CDCL algorithm, without waiting for a full model of the propositional abstraction. Obviously, this is only practical if the decision procedure is efficient and will not significantly slow down the underlying CDCL algorithm. The procedure should furthermore be capable of incrementally checking the satisfiability of a set of literals: the amount of computation required to check the satisfiability of a set of literals, and then the same set augmented by a few new literals, is not exceedingly larger than for the last set alone. Also, the procedure should be backtrackable: once a set augmented by a few literals has been checked for satisfiability, only minimal work should be needed for the decision procedure to come back to the state after checking the original set of literals. These features are necessary since the literal stack of the CDCL algorithm will be checked many times for satisfiability by the theory decision procedure, with very minor differences between the successive checks.

Checking the consistency of the literal stack on-the-fly gives to the CDCL algorithm a more immediate knowledge of the hidden, virtual set of theory clauses. However, it is not yet as if those clauses were fully known to CDCL, since no propagation occurs. A decision procedure can feature theory propagation: while being aware of all the atoms in the input formula, it can assert their value in the CDCL stack as soon as it is implied by other literals in the stack. Even for simple decision procedures, this feature might come at a cost: while congruence closure is quasi-linear, congruence closure with full propagation is hard. The current trend in SMT is to do theory propagation with a best effort policy: decision procedures only do easy propagations. Some theories however are better handled with a tighter coupling with propositional reasoning. Indeed, some data-structures are inherently Boolean. This includes bit-vectors (and machine integers) and floats. The difficulty then resides in designing the appropriate techniques to convert the problem into a Boolean one, e.g., using abstraction and lazy translation to SAT [START_REF] Zeljic | Approximations for model construction[END_REF][START_REF] Zeljic | An approximation framework for solvers and decision procedures[END_REF].

Theories of interest

The SMT theory should answer a need for expressivity, have a decidable ground problem, be tractable and have a sufficiently efficient decision procedure for the purpose. The SMT framework ensures that the decision procedure only has to deal with conjunctions of literals.

One of the simplest and most useful theories to consider is the theory of equality and uninterpreted symbols (functions and predicates). It is handled in quasi-linear time by the congruence closure algorithm [START_REF] Nelson | Fast decision procedures based on congruence closure[END_REF]. Despite its simplicity, it is useful in itself to model in an abstract way many aspects of computer systems. It is also at the core of decision procedures for more concrete data-structures, like arrays [START_REF] Stump | A decision procedure for an extensional theory of arrays[END_REF], or inductive data-types and codatatypes [START_REF] Reynolds | A decision procedure for (co)datatypes in SMT solvers[END_REF].

Another obviously interesting set of theories are the arithmetic ones: there are indeed various theories differing by their expressivity and complexity, from difference logic [START_REF] Shuvendu | An efficient Nelson-Oppen decision procedure for difference constraints over rationals[END_REF] which has very efficient decision procedures but is quite inexpressive, to non-linear arithmetic on integers (a.k.a. Hilbert 10th problem) which is undecidable even for conjunctions of ground literals [START_REF] Yu | Diophantine representation of recursively enumerable predicates[END_REF]. In between, a sweet spot is linear arithmetic on mixed integers and reals (or equivalently, rationals). The decision procedure for conjunctive sets of constraints is polynomial for reals and NP-complete for integers (see e.g., [24]), but current decision procedures are efficient for practical cases. Even in the real case, one relies on the simplex method, which is exponential [START_REF] Dutertre | Integrating Simplex with DPLL(T)[END_REF]24] in the worst case; in practice, simplex-based algorithms are more efficient than other algorithms that are optimal in the worst case [24].

Despite important applications -for instance, the B method [2] and the TLA+ [START_REF] Lamport | Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers[END_REF] language use some set theory as their underlying logic -SMT solving on set theory was, at the time of starting writing these lines, surprisingly not very well supported in SMT besides some first results [11] and the existence of a preliminary standard [START_REF] Kröning | A proposal for a theory of finite sets, lists, and maps for the SMT-lib standard[END_REF]. Solvers for set theory based verification platforms (e.g., the prover for Atelier B) use mainly rewriting based heuristic techniques, that can provide good results even for quite evolved proof obli-gations, but are even less predictable than the classical SMT approach and do not provide any guarantee of completeness. This is quite similar to the automation provided within some proof assistants, e.g., within Isabelle [START_REF] Paulson | Isabelle: a generic theorem prover[END_REF], but quite in opposition to the bottom-up SMT approach to add expressivity to SAT solving while maintaining decidability. A set theory in the SMT philosophy would be so restricted in expressivity that it would be of little help in itself. I believe the right approach is, just like for higher-order logic, to translate problems into SMT and progressively extend SMT to natively handle more and more useful constructions to deal with sets. In a sense, this is the line of the very promising approach in [11].

An essential aspect of SMT is that the theory reasoner can actually deal with a combination of theories. It is then possible to consider formulas containing, e.g., both uninterpreted symbols and arithmetic operators. Combination frameworks ensure that a decision procedure for the union of several theories can be built on the decision procedures for the component theories. On the one hand, these combination frameworks provide decidability results for combinations, and on the other, they also provide a modular way to actually build the decision procedures.

Uninterpreted symbols

The theory of equality, also known in the context of SMT as the theory of uninterpreted symbols, has one of the most mature decision procedures for SMT solving: it is efficient and has all the nice features for an optimal integration into the SMT framework.

In a nutshell, a union-find data-structure maintains a partition of terms into congruence classes according to asserted equalities. Possible inconsistencies with asserted disequalities are detected on the fly. A new asserted equality might result in a merge of two partition, if the terms asserted equal were not already in the same partition. The congruence closure algorithm also detects congruence, i.e., it ensures that two terms with the same top symbol and pairwise equal arguments are in the same partition. This is done efficiently by storing in a hash table the signature -the top symbol applied to congruence classes of the arguments -corresponding to each term. Notice that two terms with the same signature should belong to the same congruence class. This hash table can thus serve to detect congruence. Every time the congruence class of a term changes (because of some merge), the signature of its predecessors (the terms having that term as a direct argument) has to be updated. It may happen that the updated signature conflicts with one that is already present in the hash table. If so, the two terms with the same signature should be put in the same class, if they aren't already. Conflict detection with the asserted disequalities is simply done by investigating, each time the class of a term is updated, the disequalities in which it takes part.

The algorithm directly inherits from union-find data-structures its m + n log n complexity for m operations on a partition of n objects assuming constant time operations on the hash table [START_REF] Peter | Variations on the common subexpressions problem[END_REF], thanks also to the fact that congruence and conflict detection can be implemented efficiently. Backtracking can also be done quite efficiently either using persistent data-structures that are designed to be backtrackable, or carefully engineering the algorithm to store in a stack-like manner the necessary information to undo each change.

To produce proofs and small conflicts, it is sufficient to maintain aside a congruence graph. Two classes are merged either because of an asserted equality or because of a congruence between two terms. For each merge, an edge between those two terms is added to the graph, and is labeled by the reason for the merge, that is, either by the asserted equality or by a placeholder standing for congruence. The congruence graph has one and only one path between two terms in the same class, and the equality of those terms is implied, by transitivity (and symmetry and reflexivity) of the equality, by the asserted equalities in the labels and by the equalities between directly connected congruent terms. The congruences themselves are a consequence (by congruence of the equality relation) of the fact that arguments are pairwise equal. From this congruence graph, it is not difficult to build a resolution proof involving only the asserted equalities and instances of the axioms (schemas) of symmetry, transitivity, reflexivity and congruence of equality. Collecting the involved asserted equalities, together with a conflicting disequality, provides a small conflict, although not the smallest one, and not even minimal. Providing the smallest conflict is NP-complete, and providing a minimal one is polynomial, but not linear [58,59]. In practice, producing minimal conflicts rather than the (possibly non-minimal) small ones stemming from the congruence graph does not pay off the computing overhead with today's algorithms.

One last important aspect is theory propagation. Again, congruence closure can handle it very easily. Much like conflict detection, when a relevant equality becomes true because both members are put in a same class, the equality is propagated; it is also easy to propagate the disequalities congruent to some asserted disequality. However, we believe full disequality propagation is a hard problem.1

Arithmetic

Although there are many results worth mentioning about arithmetic in SMT if one wants to be complete, it is not easy to present a mature description of an arithmetic decision procedure to embed in SMT. State-of-the-art SMT solvers use a simplex-based algorithm, often a variant of [START_REF] Dutertre | A Fast Linear-Arithmetic Solver for DPLL(T)[END_REF][START_REF] Dutertre | Integrating Simplex with DPLL(T)[END_REF], to handle linear arithmetic constraints occurring in formulas. It differs from text book simplex algorithms on these points: it is not an optimization algorithm but only finds a satisfiable assignment or concludes unsatisfiability, variable values do not necessarily need to be positive, the algorithm is essentially incremental and backtrackable. In a nutshell, an assignment for variables is maintained, and repaired to take into account every additional constraint incrementally. In contrast to usual linear programming software, it is generally implemented in exact rational arithmetic, and relies on a number of techniques to accommodate integer variables. Probably the best resource to understand the battery of methods useful to tackle linear arithmetic on mixed real and integer constraints as found in SMT is the description of the MathSAT procedure [START_REF] Griggio | A Practical Approach to Satisfiability Modulo Linear Integer Arithmetic[END_REF]. However, I believe there is still place for a lot of improvements. Although current algorithms are not really the bottleneck for practical use of SMT, mixed integer linear programming algorithms, e.g., Gurobi [START_REF]Gurobi Optimization[END_REF], are impressively more efficient than SMT solvers to solve conjunctions of linear arithmetic constraints. In fact, it greatly pays off to integrate a linear programming system into the linear arithmetic decision procedure [START_REF] King | Leveraging linear and mixed integer programming for smt[END_REF]. One can argue that linear programming systems use machine arithmetic, and this accounts for the difference in efficiency. My intuition is that SMT algorithms are simply naive compared to the state-of-the-art in linear programming. The MCSAT approach for linear arithmetic [START_REF] Jovanovic | Cutting to the chase solving linear integer arithmetic[END_REF] also exhibits interesting results; it would be of the highest interest to better understand its relation to the simplex algorithm as implemented in SMT.

Beyond linear arithmetic, and even less mature, are the procedures to handle non-linear arithmetic constraints and transcendental functions. We are actively contributing to this line of research, so we delay giving further information until the second part of this document.

Combining theories

Because of their applications, the input language of SMT solvers naturally often involves several kinds of symbols, related to different objects or theories, e.g., lists, arrays, or absolutely free data-structures, arithmetic constraints, and uninterpreted symbols. While it is possible to design a decision procedure for each of those theories separately, the only conceivable way to design a procedure to deal with sets of literals -remember that the SMT infrastructure allows the procedures to only reason on conjunctive sets of literals -mixing all theories is to proceed in a modular way. Now, given a set of literals mixing several disjoint theories, it is always possible to build an equisatisfiable set such that every literal is either totally or not at all relevant for each theory. Considering uninterpreted symbols and arithmetic, an occurrence of p(x + 1) can be replaced by the two literals p(y) and y = x + 1 while preserving satisfiability (p is an uninterpreted predicate, and y is a fresh symbol of appropriate type). This process is called purification. After purification, one can use the decision procedure for each theory on only the relevant literals. This simple procedure might suffice to detect an unsatisfiable set, but there are cases where it does not. It may indeed happen that there is a model for each theory of the combination, but there is no model for the combination of theories. This simply means it is not possible to build a model for the combination of the theories from the models for each theory. These models either disagree on the domains (they have different cardinalities) or on the interpretation for the shared symbols (and in particular equality).

In order to have a working combination of decision procedures, it is necessary to ensure that, if all decision procedures in the combination find a model, there exists a model also for the combination. This requires the decision procedures to agree both on the domains (i.e., their cardinalities) and on the interpretation of shared symbols. The original Nelson-Oppen combination scheme [START_REF] Nelson | Simplifications by cooperating decision procedures[END_REF][START_REF] Ringeissen | Combinaison de résolution de contraintes[END_REF][START_REF] Tinelli | A new correctness proof of the Nelson-Oppen combination procedure[END_REF] considers disjoint theories: only equality and uninterpreted nullary symbols (called uninterpreted constants, variables, or parameters in the literature) are shared. It furthermore assumes that the theories are stably-infinite, which means that every satisfiable set of literals has a countable infinite model. In this context, it suffices that the decision procedures agree on an arrangement of the shared uninterpreted nullary symbols with respect to equality, e.g., by non-deterministically choosing a priori a partition of these symbols in equivalence classes. Thanks to the stably-infiniteness property, models found by the decision procedures can be made to agree on cardinalities, and on the interpretation of equality.

A priori agreeing on an arrangement, that is, a partition of the shared uninterpreted nullary symbols, is quite an inefficient way to ensure that decision procedures will have matching interpretations of equality. In practice, the decision procedure rather exchange information, and for instance, they propagate entailed equalities between shared terms to each other. For completeness though, and even in the case of simple combinations of disjoint stably-infinite theories, propagating only equalities is not sufficient. Consider for instance a combination including arithmetic and another theory, and five integer terms all between 0 and 3. Inevitably two of them are equal. Assume that the constraints in the other theory enforce those terms to all be distinct. No equality can be shared, but the combination is unsatisfiable. It is also necessary to propagate entailed disjunctions of equalities between shared terms; if such disjunctions are propagated, it is easy to prove that this propagation of information is equivalent to agreeing on a partition of the shared terms. So, for convex theories -theories such that, if a disjunction is entailed, one of the disjunct is entailed -propagating equalities is a complete way to agree on an arrangement. The empty theory (uninterpreted symbols with equality), and linear arithmetic on rationals can be considered as convex. For non-convex theories, it is very impractical and inefficient to detect and propagate entailed disjunctions of equalities. Part of the answer is provided by delayed theory combination [29], where disjunctions are handled by the underlying SAT solver. In the same philosophy, model-based combination [START_REF] Mendonça De Moura | Model-based theory combination[END_REF][START_REF] Caminha | Combining decision procedures by (model-)equality propagation[END_REF] exploits models provided by the individual decision procedures to enable the combination. These models are used to assert which shared terms are equal and which are not. Disagreement on these equalities leads to conflicts, but if an arrangement exists that would satisfy all theories, it will eventually be found after some iterations with the SAT solver.

If theories in a combination are not disjoint, because they share other symbols than equality and nullary uninterpreted symbols, the procedure also has to ensure that those shared symbols are interpreted by all theories in a compatible way. Local theory extensions [START_REF] Sofronie-Stokkermans | Hierarchical reasoning in local theory extensions and applications[END_REF] is a successful and practical framework for some kind of non-disjoint theories. Alternatively, disjoint theories can be combined by reduction to a decidable language [START_REF] Wies | Combining theories with shared set operations[END_REF]. Concretely however, non-disjoint combinations are not yet as commonly implemented as the classical Nelson-Oppen framework for stably-infinite theories. Some of those combinations have a high complexity, are somehow specific, or do not yet have the practical techniques and heuristics to make them work in practice. We will come back to this in the contribution, advances and perspectives part of this document.

Quantifiers

Solving the propositional satisfiability problem, checking the satisfiability of sets of literals with uninterpreted symbols, and combining disjoint theories are I believe mature aspects of SMT. Linear arithmetic decision procedures are satisfactory. Arithmetic beyond the linear case is still in its infancy. From our point of view, two major aspects that still require a lot of work and insight are non-disjoint combinations and, last but not least, handling quantifiers. SMT beyond first-order logic is mainly unexplored and central to our research project.

The Herbrand theorem (see [60] for a many-sorted version with equality) provides a tool to build a complete procedure for first-order logic formulas on the basis of a decision procedure for ground formulas. Indeed it suffices to instantiate an unsatisfiable formula sufficiently many times to get an unsatisfiable ground logical consequence, and a finite number of instances is always enough. The difficulty lies in the fact that, although the amount of necessary instances is finite, they have to be picked within an infinite though enumerable set. Since the set is enumerable, and assuming the ground problem is decidable -as it is for pure first-order logic with equality -a trivial complete procedure is to fairly enumerate instances and check the ground formulas so generated for unsatisfiability. This process will either eventually terminate on an unsatisfiable ground formula, it will terminate for lack of instances in the case of a finite Herbrand domain, or it will run for ever if the original formula is satisfiable. At the dawn of automated reasoning, this has been tried, quickly considered a dead end, and was abandoned in favor of the more promising approach of resolution and superposition theorem proving [10,[START_REF] Nieuwenhuis | Paramodulation-based theorem proving[END_REF]. Modern SAT and SMT solvers are now changing the landscape. The instantiation based SMT solver CVC4 is competitive in the annual competition of firstorder provers, and even strong supporters of superposition are reconsidering instantiation [START_REF] Reger | Instantiation and pretending to be an SMT solver with vampire[END_REF].

Instantiation techniques in SMT often rely on the information provided by the satisfiability check of the ground abstraction of the formula, that is, the formula where all quantified subformulas are abstracted as propositional variables. This information can be a model, or simply a satisfying assignment for the ground atoms. Modern SMT solvers use a portfolio of instantiation techniques. Besides simply enumerating instances -which has its advantages, if done properly; we will come back to this in the perspective part of this document -the oldest technique is probably pattern-based E-matching [START_REF] Nelson | Techniques for program verification[END_REF][START_REF] Detlefs | Simplify: A theorem prover for program checking[END_REF][START_REF] Mendonça De Moura | Efficient E-matching for SMT solvers[END_REF]. Quantified formula are associated with patterns, that is, sets of terms in the quantified formula containing all the quantified variables. Heuristics are designed to find out the effective patterns that will be efficient at finding the right instances of the formulas. Given a satisfying assignment for the ground formula, pattern-based E-matching simply tries to find out terms explicitly mentioned in this assignment which match the patterns, modulo the equalities in the satisfying assignment. This technique is thus perfectly suited to unfold axiomatized definitions.

Model-based quantifier instantiation [START_REF] Ge | Complete instantiation for quantified formulas in satisfiabiliby modulo theories[END_REF] relies on a full model for the ground abstraction of the formula. The quantified formulas are evaluated in this full model, and all instances falsified in the model are added to the ground formula. It should be noted however that generating a full model also introduces quite a lot of arbitrary choices in this model, and thus also introduces randomness in the instantiation generation. As a consequence, many useless instances might actually be added to the ground formula. For instance, a partial model for a formula might leave a certain unary function totally unassigned. Any full model would though provide an assignment for this function, and this assignment would have to be iteratively repaired, by the instantiation generation process, until it agrees with all quantified formulas mentioning the function.

Conflicting instances is a technique that is not sufficient in itself, but that never generate useless instances [START_REF] Reynolds | Finding conflicting instances of quantified formulas in SMT[END_REF]13]. It tries to find, for each formula, an instance that will be sufficient to refute the current satisfying assignment for the ground atoms. Of course, this fails for most quantified formulas, but any instance generated this way is useful. In contrast to the previous two methods, this will not overwhelm the ground SMT solver with many instances.

Contributions, advances and perspectives

In the above, we gave a brief description of the state-of-the-art in SAT and SMT solving. My previous work as well as my current research are mainly focused on advancing this state-of-the-art. Many of my contributions are related to decision procedures and combinations, that is, procedures to decide the satisfiability of sets of literals with interpreted symbols, and ways to combine them into procedures to decide the satisfiability of sets of literals containing symbols from a mixture of decidable fragments. Section 3.1 gives an account of the previous results and planned work in this direction. Although the predilection domain of SMT is decidable fragments, SMT techniques are increasingly extended to also tackle much richer languages, beyond decidable ones. In particular, I have been active in improving quantifier reasoning in SMT (Section 3.3), and a major part of my time in the near future will be devoted to bringing higher-order reasoning capabilities to SMT (Section 3.4). This includes studying the convergence of SMT with other kinds of approaches, notably superposition theorem provers. Computer algebra systems are yet another kind of automated reasoning engine; I have advocated in the past for more synergies between these systems and SMT, and my project includes pursuing this line of research, with the aim to boost arithmetic handling within SMT (Section 3.2). Improving the use of SMT solving not only requires augmenting its expressivity and efficiency, it is equally mandatory to facilitate embeddability of solvers in larger frameworks. Two issues can be pointed out. First, there should be languages and tools to help writing the input problems: this is one of the main goals of the SMT-LIB initiative, to which I contribute as one of the three current SMT-LIB managers. Second, solvers should provide a precise account of their results, i.e., by outputting either models or proofs. I have been very active already in promoting proofs for SMT solvers. The issue is however non trivial and will continue to require work in the future. Since this strongly relates also to the use of SMT in HOL platforms, both proofs and SMT for HOL are discussed together in a unique section (Section 3.4). Section 3.5 mentions the more applicative aspects of SMT to which I contributed.

Decision procedures and combination schemes

Uninterpreted symbols

One of the simplest decision procedure used in SMT decides the satisfiability of conjunctions of literals with only uninterpreted symbols and equality, a.k.a. the empty theory. In one of my very early works [63], we studied how to actually use this decision procedure in an SMT context -at that time, we were using BDDs as underlying procedure for propositional logic instead of CDCL. A key aspect for the success of using a decision procedure in an SMT framework is to be able to extract a small conflict set, i.e., a subset of an unsatisfiable input set of literals which is itself unsatisfiable. The smaller this conflict set is, the stronger the conflict clause is, and the overall convergence towards a model or unsatisfiability is quicker. Computing the smallest conflict set for sets of literals in the empty theory was long believed to be hard, although there was no proof of this. We recently proved it is indeed NP-complete [58, 59], by reduction of the SAT problem; this result is one of the selected papers (see page 65). In practice, we use heuristics to compute small conflict sets. One might be tempted to hope for a better algorithm, but this result states that a perfect technique would anyway be computationally expensive.

Combining theories

Building decision procedures for expressive languages sometimes naturally leads to combining simpler language together. The classical combination framework for theories is due to Nelson and Oppen [START_REF] Nelson | Simplifications by cooperating decision procedures[END_REF] and better understood later by Ringeissen [START_REF] Ringeissen | Combinaison de résolution de contraintes[END_REF] and Tinelli [START_REF] Tinelli | A new correctness proof of the Nelson-Oppen combination procedure[END_REF]. It assumes that the theories in the combination are decidable, disjoint -the only shared function or predicate symbols are the equality predicate and uninterpreted constants, i.e., nullary functions, often called variables in the context of theory combinations -and stably infinite -every satisfiable set of literals is satisfiable in an infinite model. Since my early works, I have contributed to better understand combination frameworks and lift the requirements for combination of theories to work. In an early work [65], I have considered non-stably infinite theories, expressed as a set of interpretations, i.e., not necessarily as a set of axioms. More recently [START_REF] Fontaine | Combination of disjoint theories: Beyond decidability[END_REF], I studied how to build combination frameworks that preserve refutational completeness when combining disjoint but not necessarily decidable theories. I contributed also to a better understanding of Nelson-Oppen in practice, using (model-)equality propagation [START_REF] Caminha | Combining decision procedures by (model-)equality propagation[END_REF][START_REF] Caminha | Combining decision procedures by (model-)equality propagation[END_REF]. Indeed, the Nelson-Oppen framework generally involves exchanging implied disjunctions of equalities, which is not practical. This model-equality propagation framework is quite similar in essence to the better known model-based theory combination approach [START_REF] Mendonça De Moura | Model-based theory combination[END_REF].

Combining first-order fragments

The properties required from the theories in a combination are used to ensure completeness of the combination. The initial set of literals to consider in the union of theories is split in several sets, each considered in one theory. If every of these split sets is satisfiable in its theory, one has to guarantee that there is a model in the union of the theories. For disjoint theories, it is essentially necessary to ensure that cardinalities of the models for the splits sets are reconcilable; it is trivially ensured by the stably infinite property for instance. If one want to avoid this property, some other properties have to be found.

Among decidable theories, it is quite natural to consider the first-order decidable fragments. Most of them are not stably infinite. I have contributed to show however that they have nice properties that compensate the lack of stable infiniteness. I have considered the Ackerman and guarded fragments in [4], the Löwenheim class (monadic first-order logic with equality, but without functions), the Bernays-Schönfinkel-Ramsey class, and the two-variable fragment of first-order logic in [61,62].

It is much more difficult to drop the disjointness requirement for combining theories. However, I have showed that a few interesting cases, namely the Löwenheim and the Bernays-Schönfinkel-Ramsey classes, satisfy an appropriate property that enables non-disjoint combination, sharing unary predicates [START_REF] Chocron | A gentle non-disjoint combination of satisfiability procedures[END_REF] (see selected paper on page 65). It is still an open problem to consider also other first-order decidable classes (e.g., the Ackerman class, the guarded fragment, and the two-variable fragment of first-order logic) in this non-disjoint framework.

I have contributed to other non-disjoint combinations of theories, but theses combination rather relate to data structures, discussed just below.

Combining data structures

From the verification point of view, data structures are, with arithmetic, extremely important to consider for combinations of decidable theories. I have contributed in early works to show that the empty theory [65], the theory of arrays [65], and theories for lists [START_REF] Fontaine | Combining lists with non-stably infinite theories[END_REF] can be combined with non-stably infinite theories. These theories behave sufficiently well not to impose strong conditions like stable infiniteness to the other theories in the combination.

In this context also, non-disjoint combinations are of great interest. It is indeed often the case that data structures involve functions connecting (bridging) them to some arithmetic theory. Consider for instance lists with length, or trees with depth or size. We have contributed to extend combination frameworks for these bridging functions. This is a kind of non-disjoint combination, since the bridging functions are relevant to both theories. Our approach [START_REF] Chocron | Satisfiability modulo non-disjoint combinations of theories connected via bridging functions[END_REF][START_REF] Chocron | A rewriting approach to the combination of data structures with bridging theories[END_REF][START_REF] Chocron | A polite non-disjoint combination method: Theories with bridging functions revisited[END_REF] is based on rewriting and reduction to disjoint combinations.

Project

The ultimate goal in combining theories is, from my point of view, to get a framework to check the satisfiability of formulas in a modular way. This framework should benefit from the properties of some parts of the formulas, for instance, if some part of the formula belongs to a decidable, stable infinite or convex fragment. If parts of the formulas are loosely connected by only a few shared symbols, non-disjoint combination would then enable to reason on those parts separately and in parallel, the framework taking care of exchanging the necessary information between the reasoners. Providing decision procedures to combine decidable fragments should not be the only goal, because in many cases, restricting languages to decidable ones is too much of a constraint for expressivity. Aiming at combination frameworks that maintain refutational completeness, notably when combining arbitrary first-order theories and decidable fragments, is also a valuable goal.

To further extend the expressivity and usefulness of SMT solvers, it seems natural to consider (and combine within the SMT solver) more decision procedures for data structures. In particular, distributed algorithms maintain specific data structures (e.g., distributed token trees for mutual exclusion) and employ variations of common data-structures (e.g., queues). Studying each of these possible data structures separately, and hard-coding each of them in an SMT solver is unfeasible. One solution to tackle this variety is to express those specific data structures using lower-level data structures that are directly supported by the reasoning infrastructure, such as arrays. This approach is unfortunately not very well suited for formal verification, especially when using automated tools: replacing the high-level operations by combinations of operations on low-level data structures makes the proof search prohibitively expensive. We propose a different approach based on plugging user-defined theories describing those specific data structures into SMT solvers, thus enabling the tools to reason on the high-level objects directly rather than on the complex implementation using lower-level constructs.

Enabling SMT solvers to accept plug-in theories poses serious practical, but also and foremost theoretical problems. As previously mentioned already, SMT solvers are based on combination frameworks that require that component theories satisfy precise and rather constraining properties. In order to accept plug-in theories, one must either (1) relax those constraining properties, specify criteria for the theories to be combinable in the framework, and define decision procedures that verify those criteria (like we have proposed in [4,61]) or (2) find new ways to combine arbitrary decision procedures in a sound, if incomplete way. In practice the (semi-)decision procedures for plug-in theories would be implemented using generic automatic theorem provers. Those theories are indeed relatively small sets of quantified formulas, but proofs may be intricate. Saturation first-order theorem provers will explore the theories and assumptions exhaustively in order to find a refutation. They thus provide efficient and refutationally complete reasoning engines. Furthermore, it has been shown that saturation theorem provers can be used to efficiently implement decision procedures for several decidable first-order fragments [7,9,[START_REF] Ganzinger | A superposition decision procedure for the guarded fragment with equality[END_REF][START_REF] Hustadt | A survey of decidable first-order fragments and description logics[END_REF]. For certain theories modeling data structures, it even appears [7,[START_REF] Schulz | On Handling Distinct Objects in the Superposition Calculus[END_REF] that generic first-order provers compete with reasoning modules written specifically to handle those data structures. In that context, a specific decision procedure for a data structure will only need to be implemented if it is worthwhile, that is, if this data-structure occurs frequently in the usual verification tasks, if reasoning on this data structure represents a bottleneck for checking proof obligations, and if a specific decision procedure would bring a significant improvement in complexity or practical efficiency. In this line, we already proposed [START_REF] Fontaine | Combination of disjoint theories: Beyond decidability[END_REF] and mentioned earlier a sound and complete way to combine a refutationally complete procedure and a decision procedure, to build a refutationally complete procedure for the union of a decidable theory and a disjoint arbitrary (not necessarily decidable) theory represented by a finite set of firstorder axioms. We are working to further develop this framework, and to apply it in practice.

Automated reasoning vs. symbolic computation

Reasoning in various fragments of arithmetic is a fundamental and ubiquitous requirement in verification. By arithmetic we here mean any theory whose language includes arithmetic constants and functions (0, 1, +, × but possibly also mod, ÷, exponentiation, trigonometric functions, etc.), interpreted over integer, rational, real or complex numbers (or a mix of those). There are well-known fundamental results about the decidability (and then, complexity) and undecidability of fragments of arithmetic that impose strict limits on the capabilities of automatic tools. For many practical applications, it is however enough to handle restricted subsets of arithmetic.

An important direction of research to extend the expressivity of SMT solvers is the quest for better arithmetic reasoning modules. If linear arithmetic on both integers and reals is quite well integrated in state-of-the-art SMT solvers, there are signs that SMT solvers handle those constraints in far less efficient ways than dedicated tools: the CVC4 solver managed to outperform all others [START_REF] King | Leveraging linear and mixed integer programming for smt[END_REF] by finding an appropriate way to interact with a modestly efficient linear programming tool, despite inappropriate interface (that is, nonincremental, non-backtrackable, non-exact arithmetic) of the linear programming tool. The situation is even worse for non-linear arithmetic. Some inno-vative techniques implemented in Z3 [START_REF] Jovanović | Solving non-linear arithmetic[END_REF] are quite efficient for SMT problems in the SMT-LIB, but non-linear capabilities of SMT solvers currently hardly compare to dedicated tools on their own benchmarks. Non-linear arithmetic is a research subject in its own, with considerable knowledge accumulated over decades. We believe the right way to tackle this problem is to work together with the community of computer algebra, to increase their awareness of our problems, and to come up with solutions that will not reinvent the wheel. Working together might also have as a side effect to better advertise to the computer algebra some techniques that are successful within SMT, e.g. [START_REF] Jovanovic | Cutting to the chase solving linear integer arithmetic[END_REF][START_REF] Jovanović | Solving non-linear arithmetic[END_REF].

I have been very active in bringing the computer algebra and SMT communities together, to share knowledge and techniques. Notably, the SMArT ANR-DFG project I have been coordinating (2014-2017) was along these lines, I was an organizer of the Dagstuhl seminar 15471 on Symbolic Computation and Satisfiability Checking in November 2015, and I am a principal investigator of the SC 2 initiative and the Coordination and Support Action H2020-FETOPEN-2015-CSA 712689 [1].

As a result of the SMArT ANR-DFG project, the veriT solver integrates the computer algebra system Reduce with Redlog as a means to decide the satisfiability of polynomial constraints on the reals. For this cooperation to work, it has been necessary to adapt real quantifier elimination methods for conflict set computation [START_REF] Jaroschek | Adapting real quantifier elimination methods for conflict set computation[END_REF]: it is based on tracing the reasons of unsatisfiability and to compute a small conflict set using the collected information. The results of this cooperation using techniques from [START_REF] Jaroschek | Adapting real quantifier elimination methods for conflict set computation[END_REF] are already good. In a work in progress unpublished at the time of writing these lines, this is further greatly improved by using as a preprocessor a thin layer implementing interval constraint propagation, i.e. a technique that computes over-approximations of the possible values for each variable in the constraints as intervals. These quick over-approximations are exploited fruitfully by the decision procedures that work downstream. Among my previous contributions, we also extended arithmetic reasoning capabilities of SMT solvers by adapting techniques developed in the context of computer algebra, namely subtropical satisfiability [START_REF] Fontaine | Subtropical satisfiability[END_REF]. This heuristic boils down, when checking the satisfiability of a set of constraints, to investigate the constraints only at the extremities of the domain space of the variables: this works surprisingly often to actually find satisfiable points.

Project

My main objective for this line of work is to design decision procedures for rich arithmetic inside SMT solving.

For the linear case, more effort should be put in filling the gap between SMT decision procedures and optimization tools. Optimization tools are indeed typically much faster than SMT to handle conjunctions of constraints. The techniques used there should be carefully analyzed, to evaluate if they can be adapted to an SMT context. On a heuristic side, efficient simple, well known, heuristic techniques that work well for linear arithmetic should also be tried to tackle mixed real-integer polynomial constraints. Of course, the problem is undecidable [START_REF] Yu | Diophantine representation of recursively enumerable predicates[END_REF], but heuristics might be good enough in practice. There might even be criteria to characterize problems that can be solved using these techniques. Among the heuristics to investigate are branch and bound, finite domain analysis, and adapting the method in [31,30] to the non-linear case.

Interval constraint propagation (ICP, see e.g., [START_REF] Fränzle | Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure[END_REF]) is already in use in the veriT solver, bringing significant efficiency improvements for satisfiability modulo polynomial constraints. There are other places where ICP could also lead to efficiency improvements in procedures occurring in computer algebra systems. In particular, we believe this should be investigated in the context of virtual substitution (see e.g., [START_REF] Košta | New concepts for real quantifier elimination by virtual substitution[END_REF]), not only as a preprocessing phase as it is currently in the veriT solver, but with a tighter integration at each step of the procedure. In a similar spirit, decision procedures for polynomial constraints used in the SMT framework might benefit from a tighter integration with the embedded SAT solver. SAT solvers are indeed recognized as being a very efficient way to handle disjunctions and case splits. Some techniques in computer algebra, notably for quantifier elimination, do intensively use case splittings. We believe there is an opportunity to build on SAT solvers, and reuse CDCL techniques for those case splittings.

Quantifier handling is another aspect for which computer algebra techniques and SMT could be combined, to tackle problems currently outside of the scope of each. While SMT deals with quantifiers using trigger or enumerative instantiation, quantifier elimination is at the heart of many computer algebra techniques. It might be possible to use quantifier elimination as found in computer algebra tools, as a mean to deal with some quantifiers found in formulas given to SMT. Currently, most SMT solvers are incomplete when given quantified formulas with quantifiers ranging over real or integer variables.

Just like not everything is linear when considering arithmetic in, e.g., verification tasks, polynomial arithmetic is sometimes not sufficient either. For transcendental functions, a very interesting approach consists in linearizing them incrementally [START_REF] Cimatti | Satisfiability modulo transcendental functions via incremental linearization[END_REF]. The approach could be investigated further, e.g., by rather translating into polynomial constraints of low degree, and then use other usual techniques to handle those polynomial constraints.

When integrated within an SMT framework, it is useful that decision procedure produce proofs, and ideally proofs are small and easy to check. We are also currently investigating proofs for arithmetic decision procedures. In the linear case, Farkas' Lemma (see e.g., [24]) is the basis for providing proofs that are easily checkable; the simplex algorithm -currently at the core of most SMT reasoners for linear arithmetic -readily provide such proofs. Decision procedures for polynomial constraints, e.g., virtual substitution and cylindrical algebraic decomposition, do not readily provide such nice certificates. The Hilbert's Nullstellensatz and Stengle's Positivstellensatz could be used to represent unsatisfiability certificates for sets of polynomial constraints respectively on the complex and on the real numbers. It is currently not clear how to extract Stellensätze for decision procedures. It is however possible to obtain a certificate, when using Gröbner bases as a decision procedure for polynomial constraints over complex numbers. This has for instance been used for Coq [START_REF] Pottier | Connecting gröbner bases programs with coq to do proofs in algebra, geometry and arithmetics[END_REF].

Quantifier reasoning

Proof obligations often contain quantified formulas, for instance to express that a certain property holds for every pair of processes taking part in the distributed algorithm, and these formulas are usually quite large. In contrast to the quantifiers in axiom sets describing plug-in theories, quantifiers that arise in this context should be better handled by Skolemization and ground instantiation. Indeed, those quantifiers usually do not require deep reasoning, but finding the few right instances can be challenging. Guiding the instantiation of the quantified formulas in SMT is currently done by heuristic rules that can account for very efficient quantifier elimination. This approach often works very nicely but sometimes also fails, notably if quantified formulas require instantiation of many variables at the same time. The main state-of-the-art instantiation techniques are E-matching based on triggers [START_REF] Mendonça De Moura | Efficient E-matching for SMT solvers[END_REF][START_REF] Detlefs | Simplify: A Theorem Prover for Program Checking[END_REF][START_REF] Rümmer | E-Matching with free variables[END_REF], finding conflicting instances [START_REF] Reynolds | Finding conflicting instances of quantified formulas in SMT[END_REF] and model-based quantifier instantiation [START_REF] Ge | Complete instantiation for quantified formulas in satisfiabiliby modulo theories[END_REF][START_REF] Reynolds | Quantifier Instantiation Techniques for Finite Model Finding in SMT[END_REF].

The theoretical foundation for instantiation as it is done in SMT solving is simply the Herbrand theorem (see e.g., [60]): a formula in pure first-order logic with equality is satisfiable if and only if the set of all its ground instances is also satisfiable. A recent contribution, yet unpublished when writing these lines, refines the classical Herbrand theorem in the context of SMT to a stronger version that requires considering less instances. E-matching based on triggers and model-based quantifier instantiation were designed to avoid the numerous instances generated by simply using Herbrand instantiation. When done carefully and with the use of this stronger Herbrand theorem, our experiments show however that simple enumerative instantiation is actually quite powerful. Among our recent contributions related to quantifier handling, we showed that the major instantiation techniques can be cast in a unifying framework for handling quantified formulas with equality and uninterpreted functions [13]. This framework reduces instantiation to the problem of E-ground (dis)unification, a variation of the classic rigid E-unification problem. We introduced a sound and complete calculus to solve this problem in practice: Congruence Closure with Free Variables (CCFV). In particular, we now use CCFV to implement finding conflicting instances. This greatly improved the performances of the veriT solver, and was also beneficial for the CVC4 solver.

Project

Many aspects of SMT solving have an engineering aspect, and this is particularly true for quantifier reasoning: among the many instances that are generated, how to sort out the good, useful ones, from those that would only distract the ground solver from its goal? To this aim, it is necessary to evaluate usefulness. Besides instances that are clearly not useful, and those that are very useful, the solver will anyway generate quite a lot of them that might be useful, but will turn out not to be much so. I believe it is of uttermost importance to clean the ground solver of these instance. Currently, neither veriT nor CVC4 implements this. Besides the obvious tedious engineering work necessary to fix this issue, there is also the scientific aspect of evaluating usefulness of instances. In SAT solving, finding out good criteria to eliminate learned clauses was the source of one of the most impressive improvement in SAT solving lately [8].

Since generating irrelevant instances is very harmful for quantifier reasoning in SMT, it is natural to invest efforts in improving the quality of the information provided by the ground solver. This was the motivation behind our work on computing prime implicants [START_REF] Déharbe | Computing prime implicants[END_REF]: prime implicants clear the model from the irrelevant literals, so that instantiation focuses only on relevant literals. In [START_REF] Mendonça De Moura | Efficient E-matching for SMT solvers[END_REF], a notion of relevancy is introduced with a similar objective. I believe more filtering can be valuable. A formula generally comprises both a problem and a set of sentences that describe the context (or theory) to study the problem. In some cases, the context is fixed by the application generating the formulas, and it is not useful to check it for consistency. The most valuable terms to take into account for instantiation are the one strongly related to the problem, and not the ones coming from the context and that are present in each of the generated formulas.

Pure quantified first-order logic is best handled with resolution and superposition-based theorem proving [9]. There has been some attempts to unify such techniques with SMT [START_REF] Mendonça De Moura | Engineering DPLL(T) + saturation[END_REF][START_REF] Mendonça De Moura | Bugs, moles and skeletons: Symbolic reasoning for software development[END_REF]26], but the main approach used in SMT remains instantiation, with quantified formulas reduced to ground ones and refuted with the help of decision procedures for ground formulas. Designing a framework unifying state-of-the-art SMT and superposition techniques is a long term interest of my research. The success of Avatar [START_REF] Voronkov | AVATAR: the architecture for first-order theorem provers[END_REF] confirms that automated reasoning has much to gain in mixing SMT and superposition approaches. Other step stones exist, and for instance, one direction I will follow in the near future is investigating the lifting up of resolutions occurring inside the SMT solver to first-order resolutions.

Some theories (like Presburger arithmetic or the theory of real closed fields) have dedicated quantifier elimination procedures. Unfortunately, those procedures currently do not work well in cooperation with either superposition, or with instantiation. Since adding uninterpreted symbols to arithmetic signature (see e.g., [START_REF] Joseph | Presburger arithmetic with unary predicates is Π 1 1 complete[END_REF]) often breaks decidability of the language, combining theory-specific quantifier elimination procedures with first-order reasoning on uninterpreted symbols will of course not yield decision procedures. It would be nice however (and valuable for many applications) to preserve refutational completeness in practice on the considered first-order theory extended with uninterpreted symbols.

Finding conflicting instances, for which we now use the CCFV algorithm, is very efficient to generate useful instances. Given an assignment for the ground part of the formula, it finds out whether there exists one instance of the quantified formula that would alone contradict this assignment. The underlying CCFV algorithm can be implemented in a complete way to guarantee that if such a single instance exists, it will always be found. Finding conflicting instance however is not a refutationally complete procedure, since one single instance might not always suffice to refute the ground assignment.

We are currently working on extending conflict based instantiation to also be complete in the case when two instances are necessary, and eventually to be complete whatever the number of required instances is. Basically, we plan to use resolution on the quantified formulas and use conflicting instances as before. Completeness is not guaranteed in general, but it might be in certain fragments.

Finally, we believe quantifier handling in automated reasoning can be inspired by the efficient techniques developed in the context of modal logics, and conversely, that the SMT point of view can lead to more expressive modal logics which could be handled efficiently using SMT solvers [5].

SMT for HOL and proofs

Full automatic proving of formulas is not possible in all cases. In general, expert human guidance is necessary at the highest levels of a proof, or to state and prove intermediate lemmas that are used in subtle proof steps. Interactive theorem provers (ITPs) provide the necessary tools to handle those subtle tasks for which human guidance is mandatory. An ITP may also serve as a proof manager, allowing to handle proofs manually, but also delegating some of the proof steps to various automated theorem provers that act as back-ends. I believe this is the right way to provide a convenient verification platform benefiting form the advances in automated reasoning. In particular, the power of SMT solvers should be made available to ITP users.

To maintain high confidence in the verdicts obtained using the platform (i.e., the ITP with its back-ends), we rely on proof-producing back-ends. ITPs are generally based on a very small (a few hundred lines of code) and carefully engineered kernel. Any proof built in the ITP has to be certified through this kernel. If a back-end provides proofs, those proofs can also be certified through the kernel. Any deduced fact, either manually or automatically by a back-end, is thus accepted as a theorem with the same very high level of confidence. A buggy external automated prover, or a buggy conduit between the ITP and the external prover only has as a consequence in the worst case a certification failure, but will never lead to certify a false theorem. The two pioneer works in this approach for SMT are the conduits between HOL-Light and CVC Lite [START_REF] Mclaughlin | Cooperating theorem provers: A case study combining HOL-light and CVC lite[END_REF], and our work between haRVey (the predecessor of veriT) and the Isabelle ITP [START_REF] Fontaine | Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants[END_REF].

The integration of automated deduction tools as back-ends of ITPs includes many engineering tasks, but there are also several theoretical issues to solve for an effective cooperation of tools. First, the size of the proofs output by the solvers should not explode: every proof step should be described succinctly by the output format, and the proof size should be at most linear with respect to reasoning time. Some methods used in highly optimized tools (especially for formula simplification, or Skolemization) are difficult to tackle without specialized rules, but those specialized rules (involving for instance deep inference) would basically be implemented very inefficiently within ITPs, leading in a very inefficient cooperation between the ITPs and the solvers. Second, there exists a trade-off between full (and long) proof traces and smaller "certificates" whose checking may involve a limited amount of proof search. Third, besides trivial simplification methods like pruning the generated proofs, and eliminating redundant deductions, there exist methods to compress proofs that may lead to a significant decrease in proof size, which in turn, could also lead to a significant decrease of the time needed to rebuild the proof inside the ITP. I have contributed to several techniques leading to improved proof size [START_REF] Fontaine | Exploring and exploiting algebraic and graphical properties of resolution[END_REF][START_REF] Fontaine | Compression of propositional resolution proofs via partial regularization[END_REF]. Some of these techniques are now implemented in an independent tool, Skeptic [27]. Although we are not involved in its development, we are still working with the authors of Skeptic on finding new algorithms to further decrease proof sizes in the SMT context.

Another very important issue for the cooperation of ITPs and automated tools is the interface. The input language of SMT solvers is standardized in [START_REF] Ranise | The SMT-LIB standard : Version 1[END_REF]17], and this standard is quite widely accepted. This simplifies the construction of conduits to SMT solvers, since a conduit generating formulas in this standardized language generates formulas suitable for all SMT solvers accepting this standard. For the conduit to be fully functional however, proofs also have to be read from the SMT solver, and replayed back inside the ITP. There is currently no standardized SMT proof format. Together with Aaron Stump, we initiated in 2011 the PxTP series of workshop. One of the objectives of these workshops is specifically to promote the emergence of good proof formats for automated reasoning tools. In [20] we proposed a preliminary proof format for SMT. A lot of work remains however to obtain a proof format accepted by the whole community. The issues are that the format should be simple, versatile to express proofs from various decision procedures, and compact. I believe now that standardization cannot be enforced for proofs, but will come from de facto acceptation of the cleanest way of representing proofs in SMT. Contrary to the input format, it will always be necessary for the SMT solver to produce some work to output a proof.

More recently, I have contributed to a proof infrastructure for the pre-processing of formulas [12]. The main components are a generic contextual recursion algorithm and an extensible set of inference rules. Clausification, skolemization, theory-specific simplifications, and expansion of 'let' expressions are instances of this framework. With suitable data structures, proof generation adds only a linear-time overhead, and proofs can be checked in linear time.

Currently there exist conduits to veriT for Coq, Isabelle, Why3, TLAPS and Rodin. The goal of my project is to improve veriT both on the input and on the output aspects to increase its usefulness in such conduits.

Project

A major part of my future research will be dedicated to Jasmin Blanchette's ERC starting grant Matryoshka2 , to which I am associated as senior collaborator. The Sledgehammer tool for Isabelle is essentially based on eager translation of higher-order proof obligations to first-order formulas that are discharged either by SMT solvers or superposition provers. This tool greatly contributes to improve efficiency of formal proof efforts, but it has limits: sometimes trivial proofs cannot be found because solvers are lost in translation. In the Matryoshka project, we want to augment SMT solvers with higher-order reasoning in a careful manner, to preserve their desirable properties. The approach is application-oriented, based on the available large repositories of interactive verification efforts.

We are currently investigating three aspects. First, we are extending congruence closure and instantiation to tackle higher-order constructions. Second, we are getting inspiration from the automated reasoning capabilities of interactive provers to add new kinds of reasoning methods inside SMT. Indeed, higher-order rewriting as implemented in proof assistants can sometimes be surprisingly good at finding proofs, whereas hammers fail on the same tasks. Last but not least, induction is often a crucial aspect for verification tasks, but this is currently not or insufficiently integrated into SMT solvers.

In the long run, the cooperation between automatic provers, proof assistants, and human users should be less fragmented: currently, users write theorems that are either proved by the assistant or the automatic provers via hammers. The future might well be that assistants and provers work together and rather ask users for input for hard parts of the proofs.

Tools and applications

The primal application of my research was verification of parameterized systems. In [64, 60], I showed that validation of inductive invariants for some kind of parameterized systems is a decidable problem, and SMT solvers are essential components of the decision procedure. Since then, I have been actively developing stand alone tools that can be used as back-ends for verification platform. With the veriT solver [START_REF] Zhang | Decision procedures for term algebras with integer constraints[END_REF] (the system description paper is in the selection of papers on page 65), our goal is to provide a stable tool that implements our research algorithms and make them available in open-source.

On the front-end side, I have been contributing to the integration of SMT solvers in the verification platform Rodin [START_REF] Déharbe | SMT solvers for Rodin[END_REF][START_REF] Déharbe | Integrating SMT solvers in Rodin[END_REF] (see selected paper on page 65). On a set of Event-B models stemming from industrial and academic problems, our techniques decrease by a factor of four the number of proof obligations whose verification requires human interaction. According to users, this is particularly helpful for verification conditions where the major challenge is the combinatorial aspect of the formula. Thanks to the SMT-LIB initiative and to the standard SMT-LIB language, building a plugin to use all SMT solvers is not more difficult than implementing a conduit for just one of them, at least for the common language. For a few years now I have been active as an SMT-LIB manager.

Project

Augmenting SMT with higher-order capabilities and improving proof generation will also improve the usefulness of SMT solvers for applications. I will continue to devote an increasing part of my time for the management of the SMT-LIB, and I am looking forward for the next SMT-LIB version, that should standardize many new features, including higher-order constructs.

Within the Matryoshka project, the objective is to improve SMT support for platforms. The priority targets are Isabelle and TLAPS. Sometimes however applications come from unexpected areas. For instance, SAT solvers are used to check the dependencies of software, or to look over the satisfiability of configurations for vehicles. The future applications for SMT might well be of a surprising nature; it is important to recognize them anyway.

From logic to education in computer science

As computer science reaches maturity, it is necessary to present it differently, packaged so that students can get the basics in a way that give them a deep understanding of the inner workings of modern computer systems and at the same time withhold the awfully specific details real systems are full of. I have been teaching at various levels and for various kinds of students, but I believe all need a more polished presentation of computer science than what is given to them now, which is too tightly tied to rising technologies. For instance, the religious wars between programming languages are particularly strong on the field of education. Maybe it is time to comprehend (again) programming without a specific modern programming language in mind. In the same vein, modern computers are only understandable with a simplified picture in mind. But this picture is not sufficiently well drawn.

I advocate that some basic computer science topics all go very well together: logic, computer structures, assembly language, algorithms and complexity, programming, compilers, and verification. There is some work to invest to present these in a connected way. In a logic course I have been giving to second year students for business informatics and cognitive sciences, I submitted a simple problem of comparing two pieces of code, differing only by the test in a conditional statement; the tests were logically equivalent but more than one student out of two asserted that the two pieces of code were behaving differently although no side effect could account for that. Logic is also strongly linked to computer structures. In a course I am teaching to the same second year students, we build, starting with logic gates, a full working RISC computer, simulated within a software, and that serves as a basis to program in assembly language. And programming this RISC machine in assembly language gives the students a full understanding of how loops, recursion, memory and pointers work. Logic comes again at hand when you show you can actually prove some code you have written, either in the low level, RISC assembly language, or in a higher level code. But again, understanding how the higher level code is translated in assembly language is instrumental to actually prove that the code is correct, since it gives it a clear semantics. This links verification, logic, computer structures and assembly language to some aspects of compilation. I have never taught algorithms and complexity, and I believe it is not easy to teach this to non-scientific students. But again, on a RISC machine, complexity has a precise definition: it is related to the number of basic instructions corresponding to an input of a given size. With a high level language, this notion is not clear at all: instructions deeply embedded in the language have a non trivial (and often not documented) complexity. One school of thought is going away from the details in computer science. I believe we have to get back to details, but on a reconstructed abstraction of reality. Nobody can understand today's combustion engines in details, but understanding well conceived abstractions provides sufficient grounds not to be afraid when approaching the real thing. It is not only necessary to give knowledge to students so that they are able to perform in companies; providing them with a deep understanding of the principles underlying computer science will help them better. And this is not possible to do it anymore on the basis of state-of-the-art computers and programming languages.

Conclusion

It was once a time when logic and automated theorem proving was fully part of what people call artificial intelligence. Today, as I am writing these lines, there is again some diffuse fear that artificial intelligent entities will take over the world. Probably this is not more true than before, but it is true however that modern techniques of artificial intelligence have a deep impact on some scientific areas, and for instance completely modifies the state-of-the-art and techniques for speech recognition, or automatic treatment of natural language. It is not clear yet what impact it will have on automated reasoning. But I firmly believe it will not kill automated reasoning as we know it, just like it will not kill traditional programming. Probably, and this is a fact that is completely absent of my research program, machine learning will find its place in automated reasoning, and will greatly improve it. Perhaps automated reasoning might also find its place in artificial intelligence, as a complement module to rigorously check soundness of deduction, or to efficiently evaluate problems that can be translated to logic?

If we consider the publication of Hoare logic as a birth date [START_REF] Hoare | An Axiomatic Basis of Computer Programming[END_REF], verification will soon turn fifty. Those years saw great hopes, and great disillusionment. Reading today Dijkstra's point of view [START_REF] Edsger | The humble programmer[END_REF] on the failure of programming in 1972 is funny in a sad way: many of his statements are still valid fifty years later. The verifying compiler, once expected as an outcome of the newborn science of verification, never really existed; Tony Hoare quite recently advocated to revive this challenge [START_REF] Hoare | The verifying compiler: A grand challenge for computing research[END_REF]. On the other hand, the situation is not that desperate. There exist verified compilers (see e.g. the CompCert project) and verified kernels, and large companies are surely all aware of and use verification techniques. 3 It is impossible to know how the world would feel like without verification at all, but all major companies do find an economic value in maintaining a formal verification department. Many discoveries (think about quantum mechanics or DNA) are full of promises, and later reveal themselves to be more difficult to use than expected, but anyway lead to great practical advances. We are unable to prove every program easily just like we are unable to solve the Schrödinger equation for all systems. Anyway, the importance of verification and automated reasoning will continue to grow, while the pervasiveness of algorithms, computer systems and the cloud will increase. I do not believe it will one day become easy, but with the same effort, we will push verification much further. I do believe though that one day, automated deduction integrated within interactive theorem proving will discharge most non-creative thinking out of formally verified proofs. Proofs of NP-completeness are often fascinating: they are often not trivial to find although they can be obvious to follow. This is not an exception. The efficiency of satisfiability modulo theories (SMT) solvers is dependent on the capability of theory reasoners to provide small conflict sets, i.e. small unsatisfiable subsets from unsatisfiable sets of literals. We show here the NP-completeness of generating smallest conflict sets for one of the simplest decidable theory, i.e. sets of literals with only uninterpreted symbols and equalities. This is proved using a simple reduction from SAT.

• This result is at the same time hard (involving an extension of the Ramsey theorem) and quite simple to understand. A combination framework should ensure that the decision procedures in the combination share enough information to eventually cooperatively show that the set of formulas is unsatisfiable, or that the sharing of information will eventually stop and a model for the union of formulas can be built. This is similar in the case of disjoint or non-disjoint union of theories, only the shared information changes. For major classes of theories, namely the Löwenheim and Bernays-Schönfinkel-Ramsey classes, the non-disjoint combination of theories sharing only unary predicates (plus constants and the equality) is decidable. The shared information is the cardinality of the set of support of each shared unary predicate, and this is computable for those first-order decidable classes. In this work, we investigate using symmetries in formulas to improve the efficiency of satisfiability checking. This technique is based on the concept of (syntactic) invariance by permutation of constants. An algorithm for solving SMT by taking advantage of such symmetries is presented. The technique in itself is certainly interesting, but this paper is mainly an advocacy for better encoding of problems into SMT. For nearly ten years, many benchmarks in the QF UF category of the SMT-LIB remained undefeated because they were encoded in a way that enforced solvers to study all equivalent permutations of the same easy problems.

• Thomas Bouton, Diego Caminha B. de

Introduction

Satisfiability Modulo Theory solvers are nowadays based on a cooperation between a propositional satisfiability (SAT) solver and a theory reasoner for the combination of theories supported by the SMT solver. The propositional structure of the problem is handled by the SAT solver, whereas the theory reasoner only has to deal with conjunctions of literals. Very schematically (we refer to [1] for more details) the Boolean abstraction of the SMT problem is repeatedly refined by adding theory conflict clauses that eliminate spurious models of the abstraction, until either unsatisfiability is reached, or a model of the SMT formula is found. Refinements can be done by refuting models of the propositional abstraction one at a time. It is, however, much more productive to refute all propositional models that are spurious for the same reason at once. A model of the abstraction is spurious if the set of concrete literals corresponding to the abstracted literals satisfied by this model is unsatisfiable modulo the theory. Given such an unsatisfiable set of concrete literals, the disjunction of the negations of any unsatisfiable subset (a.k.a. core) is a suitable conflict clause. By backtracking and asserting the conflict clause, the SATsolver is prevented from generating the spurious model again. The smaller the clause, the stronger it is and the more spurious models it prevents. Therefore, an optimal conflict clause, corresponding to a minimal unsatisfiable subset of literals (i.e. such that all its proper subsets are satisfiable) or even a minimum one (i.e. smallest among the minimals) is desirable. This feature of the theory reasoners to generate small conflict sets (a name adopted in [1]) from their input is also referred to as proof production [8,9] or explanation generation [10]. Decision procedures for the theory of uninterpreted symbols and equality can be based on congruence closure [7,3,10]. The decision problem is polynomial and even quasi-linear [3] with respect to the number of terms and literals in the input set. Producing minimal conflict sets also takes polynomial time. Indeed, testing if a set S remains unsatisfiable after removal of one of its literals is also polynomial. It suffices then to repeatedly test the |S| literals of S to check if they can be removed. The set S pruned of its unnecessary literals is minimal. One could also profit from the incrementality of the decision procedure [6].

It has also been common knowledge that computing minimum conflict clauses for the theory of uninterpreted symbols and equality is a difficult problem. But, to our best knowledge, the complexity of finding the smallest conflict clause generation for sets of literals with uninterpreted symbols and equalities has never been established. The complexity of the corresponding decision problem (i.e. of whether there exists a conflict clause with size smaller than a given k) is mentioned to be NP-complete in [10] -with a reference to a private communication with Ashish Tiwari -but neither the authors of [10] nor Ashish Tiwari published a written proof of this fact1 .

Our interest in this problem arose from our work on Skeptik [2], a tool for the compression of proofs generated by SAT and SMT solvers. For the sake of moving beyond the purely propositional level, we have developed an algorithm for compressing congruence closure proofs, which consists of regenerating (possibly smaller) congruence closure conflict clauses while traversing the proof. Congruence closure conflict clauses are typically generated from paths in the congruence graph maintained by the congruence closure algorithm [5,10,9]. In order to obtain small conflict clauses, and thereby small congruence clo-sure proofs, we (dynamically) assigned weights to the congruence graph and searched for shortest paths in that graph. The weights of input equations would be 1, whereas the weight of a congruence edge would be the size of an explanation of its equation. This raised the question whether we could construct shortest conflict clauses as shortest paths in such weighted congruence graphs, by applying a polynomial time shortest path algorithm to a graph of polynomial size. We answered this question negatively by proving that the problem of deciding whether a shorter conflict clause exists is NP-hard. The goal of this article is to present this proof. The reason why the shortest path method is not able to find shortest conflict clauses is that the weights for congruence edges can not be accurately determined a priori. A preliminary version was presented at the SMT Workshop 2015 [4].

Preliminaries

We assume knowledge of propositional logic and quantifier-free first-order logic with equality and uninterpreted symbols, and only enumerate the notions and notations used in this article. A literal is either a propositional variable or the negation of a propositional variable. A clause is a disjunctive set of literals. A propositional variable x appears positively (negatively) in a clause

C if x ∈ C (resp. ¬x ∈ C).
The notations { 1 , . . . n } and 1 ∨ • • • ∨ n will be used interchangeably. A clause is tautological if and only if it contains a variable both positively and negatively. We shall tacitly assume that clauses are non-tautological, except when explicitly stated otherwise. Clauses being sets, they cannot contain multiple occurrences of the same literal. A formula in conjunctive normal form (CNF for short) is a conjunctive set of clauses. A total (partial) assignment I for a formula in propositional logic assigns a value in { , ⊥} to each (resp. some) propositional variable(s) in the formula. An assignment I for a formula F is a model of F , denoted I |= F , if it makes the formula F true. A formula is satisfiable if it has a model, it is unsatisfiable otherwise. A total or partial assignment is perfectly defined by the set of literals it makes true. By default, an assignment is total unless explicitly said to be partial. A set of formulas E entails a (set of) formula(s) E , denoted

E |= E , if every model of E is a model of E .
We now define the necessary notions for quantifier-free first-order logic.

Definition 1 (Terms and equations)

A signature Σ is a finite set of function symbols F equipped with an arity function F → N. A constant is a nullary function. A unary function has arity one. Given a signature Σ, the set of terms T Σ is the smallest set containing all constants in F and all terms of the form g(t 1 , . . . , t n ), where g is a function symbol of arity n in F and t 1 , . . . , t n are terms in T Σ . An equation between two terms s, t in T Σ is denoted by s = t.

Signatures commonly include predicate symbols. Everything extends smoothly to signatures with predicates, but to simplify, a quantifier-free first-order logic formula is here just a Boolean combination of equalities between terms; a literal is either an equation or the negation of an equation. The terms t 1 , . . . , t n are direct subterms of g(t 1 , . . . , t n ). The subterm relation is the reflexive and transitive closure of the direct subterm relation. Given a set of equations E, we denote by T (E) the set of terms and subterms occurring in the equations.

An assignment I on some signature maps each constant to an element in a universe U, and each function symbol to a function of appropriate arity on U. By extension, it assigns an element in U to every term, and a value to every equation s = t, namely if I(s) = I(t) and ⊥ otherwise. Like in propositional logic, an assignment on some signature thus gives a truth value to every formula on this signature.

Definition 2 (Congruence relation) Given a set of terms

T closed under the subterm relation, a relation R ⊆ T × T is a congruence if it is -reflexive: (t, t) ∈ R for each t ∈ T ; -symmetric: (s, t) ∈ R if (t, s) ∈ R; -transitive: (r, t) ∈ R if (r, s) ∈ R and (s, t) ∈ R; -compatible: (g(t 1 , . . . , t n ), g(s 1 , . . . , s n )) ∈ R if g is a n-
T ⊆ T Σ , that is, R = {(s, t) | I(s = t) = }.
An equation s = t on terms in a set T can be seen as a singleton relation {(s, t)} ⊆ T ×T . By extension, a set of equations can also be seen as a relation, i.e., the union of the singleton relations. Since congruence relations are closed under intersection, the congruence closure of a set of equations always exists. Also notice that, if (s, t) ∈ E * , then

E |= s = t.
We say that E is an explanation for s = t.

An algorithm computing the congruence closure of a relation is also a decision procedure for the problem of satisfiability of sets of equalities and disequalities in quantifier-free first-order logic with uninterpreted (predicates and) functions. It suffices indeed to compute the congruence closure of all equalities on the terms and subterms occurring in the literals. Then, the set of literals is satisfiable if and only if there is no disequality with both terms in the same class. A model can be built from the congruence closure, on a universe with cardinality equal to the number of classes in the congruence.

Congruence Closure in Practice

The algorithms we consider in the following take as input a set of literals E. Considering complexity, not only the cardinality of the set is important, but also the number of terms and subterms as well as the number of their occurrences. Congruence closure algorithms in modern SMT solvers typically represent terms with Directed Acyclic Graphs (DAGs) using maximal sharing, and not trees. The number of term and subterm occurrences does not matter, but only the number of distinct (sub)terms. The input is also typically not a set, but successive calls to an assertion function with a literal as argument: every repetition of the same literal then matters for complexity. Let us assume, however, that the input is a set E, terms are DAGs with maximal sharing (i.e. identity of atomic symbols and complex terms can be checked in constant time). Therefore, we characterize complexity results in terms of number of literals, terms and subterms of the input set, i.e. |E| and |T (E)|.

Since congruence relations are basically partitions of equivalent terms that additionally satisfy the compatibility property, it is unsurprising that practical congruence closure algorithms, or decision procedures for ground sets of firstorder logic literals, are based on some kind of union-find data-structure. Terms (and subterms) are put into equivalence classes, according to the equalities in the input. The algorithms furthermore check, every time two classes of the partition are merged, whether any new equality induced by compatibility has to be taken into account. Also, it checks that the congruence is consistent with the set of disequalities. We refer the reader to [7,3,10] for more details. The complexity of those algorithms depend on the internal data-structures and on the representation of terms [3]. Algorithms typically implemented in SMT solvers have complexity

O(|E| + (|T (E)| • log |T (E)|)
) assuming constant time operations on the hash table being used to detect new equalities induced by compatibility.

The generation of conflict sets or explanations is based on the congruence graph: its nodes are the terms and subterms considered by the algorithm. An edge in the graph is either a full edge, linking two nodes s and t and labeled by an input equation s = t, or a congruence edge (a dotted edge in the figures in this article), linking two terms with the same leading function symbol and labeled by the compatibility-deduced equality between both terms. The graph has a path between two terms if and only if they belong to the same congruence class. The equality between two terms in the same class is a logical consequence of the set of equations labeling the path. To get an explanation for the equality of two terms in the same class, that is, a set of input equations implying the equality of the two terms, it thus suffices to collect the set of equations labeling a path, and recursively replace any compatibility equation

g(t 1 , . . . , t n ) = g(s 1 , . . . , s n ) by the explanations of t 1 = s 1 ,. . . , t n = s n . Example 1 A congruence graph for two input equations a = f (f (f (a))) and a = f (f (f (f (f (a))))
) is given on Figure 1. Labeling equations are omitted for simplicity. There is a path between a and f (a), so both terms are equal if the a f (a)

f (f (a)) f (f (f (a))) f (f (f (f (a)))) f (f (f (f (f (a)))))
Fig. 1 An example congruence graph input equations hold. To compute an explanation for a = f (a), it suffices to collect the equalities on the path, that is, the input equation a = f (f (f (a)))) and the compatibility equation f (a) = f (f (f (a))). This last equation should then be replaced by the equation between the arguments, i.e., a = f (f (a))) which is consequence, by transitivity, of another compatibility equation and of the other input equation a = f (f (f (f (f (a))))). Hence the explanation will contain both equations.

Practical congruence closure algorithms with explanation build a congruence graph while computing the congruence closure. Every time the decision procedure merges two classes, either because of an input equation or because an equality was deduced due to compatibility, a full-or congruence-edge is added to the graph. Since edges between nodes are only added when their respective congruence classes are merged, the path between two terms in the same class is unique. The explanation that two terms are equal is also unique, but there is no guarantee that this explanation is the smallest one. Indeed, it may happen that the algorithm considers, e.g. equations a = b and b = c before a = c, merging a, b and c before considering the last equation, and thus discarding a = c as redundant: in that case, a = c would have been the smallest proof that a and c are equal, but the congruence graph would only consider the two other equalities. There is not even a guarantee that the explanation is minimal. Again, the congruence closure algorithm can prove that a = f (b) from the input equations b = f (a), f (a) = f (b) and a = b. The redundant equality f (a) = f (b) would be recorded in the congruence graph, and thus be part of the explanation, if it is considered before a = b.

In practice, the congruence closure procedures implemented in SMT solvers produce explanations efficiently: the complexity of the explanation production is quasi-linear with respect to the explanation size, which is at most equal to the size of the input [10]. But the explanations are not optimal, i.e. they are not always the smallest. In fact, they are not even minimal. It is possible to compute minimal explanations in polynomial time; it suffices for instance to compute again the congruence closure iteratively removing every equation in the explanation, to see if it is redundant or not. One could (naively) hope to conceive a different congruence closure algorithm generating the smallest explanation in polynomial time. For example, one might attempt to modify the iterative removal algorithm; or attempt to modify shortest path algorithms and apply them to congruence graphs enriched with redundant equations as labels. However, such attempts would be futile. As proven in the next section, the corresponding decision problem is NP-hard.

NP-Completeness of the Small Conflict Set Problem

The function problem of generating the smallest conflict set corresponds to the decision problem of deciding whether a conflict set with size smaller than a given k exists.

Definition 4 (Small conflict set problem) Given an unsatisfiable set E of literals in quantifier-free first-order logic with equality and k ∈ N, the small conflict set generation problem is the problem of deciding whether there exists an unsatisfiable set

E ⊆ E with |E | ≤ k.
If we had a polynomial-time algorithm α capable of generating the smallest conflict set for any unsatisfiable set E, then we could decide in polynomial time any instance of the small conflict set problem by applying α to E and checking whether α(E) has size smaller than k. However, as proven below, the small conflict set problem is NP-complete and, therefore, polynomial time generation of conflict sets with minimum size is not possible (unless P = NP). Our proof reduces the problem of deciding the satisfiability of a propositional logic formula in conjunctive normal form (SAT) to the small explanation problem.

Definition 5 (Small explanation problem) Given a set of equations E = {s 1 = t 1 , . . . s n = t n }, k ∈ N and a target equation s = t, the small explanation problem is the problem of answering whether there exists a set E such that

E ⊆ E, E |= s = t and |E | ≤ k.
The small explanation problem and the small conflict set problem are closely related: there is a small explanation of size k of s = t from E if and only if there is a small conflict of size k + 1 for E ∪ {s = t}.

In the following we describe a polynomial translation from instances of the propositional satisfiability problem to instances of the small explanation problem. The translation consists of two parts: a translation of propositional formulas, here assumed, without loss of generality, to be in CNF (as shown in Definition 6), and a translation of assignments (as shown in Definition 7). Definition 6 (CNF congruence translation) Let C be a set of propositional clauses {C 1 , . . . C n } using variables x 1 , . . . , x m . The congruence translation E C of C is defined as the set of equations

E C = Connect ∪ 1≤i≤n Clause i with Connect = {c i = c i+1 | 1 ≤ i < n} Clause i = {c i = t i (x j ) | x j appears in C i } ∪ {t i ( j ) = c i | x j appears positively in C i } ∪ {t i (⊥ j ) = c i | x j
C 1 = x 1 ∨ x 2 ∨ ¬x 3 , C 2 = ¬x 2 ∨ x 3 , C 3 = ¬x 1 ∨ ¬x 2 .
Figure 2 represents the congruence translation of C graphically, an edge between two nodes meaning that the set contains an equation between the terms labeling the two nodes.

c1 t1(x2) t1(x1) t1(x3) c 1 t1( 2) t1( 1) t1(⊥3) c2 t2(x2) t2(x3) c 2 t2(⊥2) t2( 3) c3 t3(x1) t3(x2) c 3 t3(⊥1) t3(⊥2)

Definition 7 (Assignment congruence translation)

The assignment congruence translation E I of an assignment I on propositional variables x 1 , . . . , x m is the set of equations

E I = {x j = j | 1 ≤ j ≤ m and I |= x j } ∪ {x j = ⊥ j | 1 ≤ j ≤ m and I |= ¬x j }
For convenience, we also define the set

AssignmentEqs = {x j = j , xj = ⊥ j | 1 ≤ j ≤ m}.
An assignment congruence translation is always a subset of AssignmentEqs. By extension, a subset of AssignmentEqs is said to be an assignment if it is the congruence translation of an assignment, that is, if it does not contain both xj = j and xj = ⊥ j for some j.

E I ∪ E C |= c 1 = c n .
Proof. Let the propositional variables in C be x 1 , . . . , x m .

(⇐) Consider the congruence graph induced by E I ∪ E C . Besides edges directly associated to equalities in the set, the only edges are congruence edges between terms t i (x j ) and either t i ( j ) or t i (⊥ j ). So any path from c 1 to c n would go through such a congruence edge for each i. And such an edge exists for i if and only if the clause i is satisfied by I.

(⇒) If I |= C, then I |= C i for each clause C i ∈ C. Assume I makes true a variable x j , literal of C i (the case of the negation of a variable is handled similarly). Then E I |= t i (x j ) = t i ( j ), and E I ∪ Clause i |= c i = c i . This is true for each i, and thanks to the equations in Connect, one can deduce using transitivity that Proof. E I contains at most m equations, since for no j both I |= x j and I |= ¬x j . The set Connect contains exactly n -1 equations. For every i, the set Clause i contains at most 2m equations, resulting in 2mn equations for all clauses. In total, we thus have

E I ∪ E C |= c 1 = c n .
|E I ∪ E C | ≤ n -1 + m + 2mn.
E I ∪ E C contains at most 2n + 3m + 3mn terms: 2n for c i , c i , 3m for xj , j , ⊥ j and 3mn for all possible combinations of t i (x j ), t i ( j ), t i (⊥ j ).

Considering again Example 3, and particularly Figure 5, any transitivity chain from c 1 to c 3 will pass through c 1 , c 2 , c 2 and c 3 . Any acyclic path from c 1 to c 3 will contain 11 edges: 3 congruence edges, 3 * 2 edges in Clause i for i = 1, 2, 3 and 2 edges from Connect.

Since every interpretation I is such that E I ⊂ AssignmentEqs, one can try to relate the propositional satisfiability problem for a set of clauses C = {C 1 , . . . C n } to finding an explanation of c 1 = c n in AssignmentEqs ∪ E C . However, it is necessary that this explanation does not set xj equal both to j and ⊥ j , i.e. at most one of the two equations xj = j and xj = ⊥ j should be in the explanation. By restricting assignments to total ones, i.e. by enforcing that at least one of the two equations xj = j and xj = ⊥ j belongs to the explanation, it is also possible, with a single cardinality condition on the explanation size, to require that at most one of them belong to the explanation.

Lemma 3 A set of non-tautological clauses

C = {C 1 , . . . C n } using vari- ables x 1 , . . . , x m is satisfiable if and only if there is a set E such that E ⊆ AssignmentEqs ∪ E C , E |= c 1 = c n+m and |E | ≤ 3n + 4m -1, where C is C augmented with the tautological clauses C n+i = x i ∨ ¬x i for i = 1, . . . m.
Proof. (⇒) Consider a total model I for C. We show that there is a set E ⊂ E C , such that together with the congruence translation

E I of I it follows E = E ∪ E I |= c 1 = c n+m and |E | ≤ 3n + 4m -1.
The set E I contains m equations, since it is the congruence translation of a total assignment.

For each clause C i (i = 1 . . . n + m), there is a literal in C i that is satisfied by the model I. Let x j be the variable of that literal.

Suppose I |= x j , then the set E contains equations c i = t i (x j ), t i ( j ) = c i of Clause i . These equations are in Clause i , because x j is the satisfying literal of C i , thus surely x j ∈ C i . From compatibility and the fact that xj = j ∈ E I it follows that E ∪ E I |= t i (x j ) = t i ( j ). Finally, from transitivity and the three equations

c i = t i (x j ), t i (x j ) = t i ( j ), t i ( j ) = c i it follows that E ∪ E I |= c i = c i .
The case I |= x j is symmetric, such that via equations c i = t i (x j ),

t i (x j ) = t i (⊥ j ), t i (⊥ j ) = c i , it follows E ∪ E I |= c i = c i .
In addition to 2 equations for each of the (n + m) clauses, the set E contains all n + m -1 equations of Connect, that is

c i = c i+1 for i = 1 . . . n + m -1. From transitivity it follows that E ∪ E I |= c 1 = c n+m .
In total, E contains 2(n + m) of the sets Clause i , n + m -1 equations from Connect and m equations from E I , i.e. |E| = 3n + 4m -1.

(⇐) Suppose there is a set of equations E ⊆ AssignmentEqs ∪ E C such that E |= c 1 = c n+m and |E | ≤ 3n + 4m -1. E has to contain 2(n + m) equations from Clause i (i = 1 . . . n+m), that is one pair of equations c i = t i (.) and t i (.) = c i for every clause, and n + m -1 equations from Connect, since by construction there is no other possibility to deduce c i = c i . Furthermore, thanks to the tautological clauses, E also has to contain at least xj = j or xj = ⊥ j for each j ∈ {1 . . . m}. Therefore, the cardinality condition |E | ≤ 3n+4m-1 and the fact that E contains 3(n + m)-1 equations from Clause i and Connect, requires that the E contains at most one xj = j or xj = ⊥ j for each j ∈ {1 . . . m}. Therefore, we have that E I = E ∩ AssignmentEqs is the congruence translation of an assignment and Lemma 1 guarantees the existence of a model for C , or equivalently for the original set of clauses C.

Example 4

In Lemma 3, the input formula is augmented with tautological clauses. We demonstrate here the necessity of these extra clauses on the unsatisfiable formula ϕ = (

x 1 ∨ x 2 ) ∧ (¬x 1 ∨ x 2 ) ∧ (x 1 ∨ ¬x 2 ) ∧ (¬x 1 ∨ ¬x 2 ).
Figure 6 shows the congruence translation of ϕ together with a subset of AssignmentEqs that yields an explanation for c 1 = c 4 . This explanation picks, besides the necessary equations from the clause and connect parts, two equations from the AssignmentEqs part. However, this explanation maps x 1 to ⊥ and at the same time, and hence cannot correspond to a (consistent) assignment. With the addition of tautological clauses and because the number of equations in the explanation is upper bounded, spurious explanations of this kind are ruled out. This is illustrated in Figure 7, depicting the congruence translation of ϕ conjoined with the tautological clauses (x 1 ∨ ¬x 1 ) and (x 2 ∨ ¬x 2 ), together with the same subset of AssignmentEqs used in Figure 6. As desired, this subset is not an explanation of c 1 = c 6 , since the transitivity chain stops at t 6 (x 2 ), x 2 being unassigned. In fact, in this congruence graph, there is no explanation of c 1 = c 6 with less than 19 equations. This is as expected, since ϕ is unsatisfiable and 3n + 4m -1 = 19 in our example with n = 4 clauses and m = 2 variables.

c1 t1(x2) t1(x1) c 1 t1( 2) t1( 1) c2 t2(x2) t2(x1) c 2 t2( 2) t2(⊥1) c3 t3(x2) t3(x1) c 3 t3(⊥2) t3( 1) c4 t4(x2) t4(x1) c 4 t4(⊥2) t4(⊥1) x1 1 ⊥1
Fig. 6 The congruence translation of ϕ and a spurious short explanation.

c1 t1(x2) t1(x1) c 1 t1( 2) t1( 1) c2 t2(x2) t2(x1) c 2 t2( 2) t2(⊥1) c3 t3(x2) t3(x1) c 3 t3(⊥2) t3( 1) c4 t4(x2) t4(x1) c 4 t4(⊥2) t4(⊥1) c5 t5(x1) c 5 t5(⊥1) t5( 1) c6 t6(x2) c 6 t6(⊥2) t6( 2) x1 1 ⊥1
Fig. 7 The congruence translation of ϕ with tautological clauses.

Corollary 1 (NP-hardness)

The small explanation problem is NP-hard.

Proof. Propositional satisfiability is NP-hard, and can be reduced in polynomial time to the small explanation problem.

Lemma 4 (NP)

The small explanation problem is in NP.

Proof. Let E be a set of equations and s = t be a target equation. A solution to the explanation problem for some k ∈ N is a subset E ⊆ E, such that

|E | ≤ k. Let n = |T (E)| + |E| and n = |T (E )| + |E |.
We have n ≤ n, since E ⊆ E and every term in E appears also in E. Checking whether E is an explanation of s = t can be done by computing its congruence closure, which is possible in polynomial time in n [7] and thereby also in n.

Theorem 1 (Small explanation NP-completeness) The small explanation problem is NP-complete.

Proof. By corollary 1 and lemma 4.

Theorem 2 (Small conflict NP-completeness) The small conflict set problem is NP-complete.

Proof. The small conflict set problem is at least as hard as the small explanation problem since the small explanation problem has been showed to be reducible to the small conflict set problem. It is also in NP for exactly the same reason that the small explanation problem is.

Conclusion

The conflict set generation feature of congruence algorithms is essential for practical SMT solving. Although one could argue that the important property of the generated conflicts is minimality (i.e. no useless literal is in the conflict), it is also interesting to consider producing the smallest conflict. We have shown that the problem of deciding whether a conflict of a given size exists is NPcomplete. Therefore, it is generally intractable to obtain the smallest conflict.

In [6,8,9], methods to obtain small conflicts, but not necessarily the smallest, are discussed. In practice, it pays off to prioritize speed of the congruence closure algorithm and conflict generation over succinctness of conflicts. However, other applications sensitive to proof size may benefit from other methods prioritizing small conflict size, at a cost of less efficient solving. Thanks to the NP-completeness, one option could be to iteratively encode the small conflict problem into SAT, and use a SAT-solver to find successively smaller conflicts, until the smallest is found. Perhaps an encoding of the problem can be found that differentiates between hard constraints representing relevant instantiations of the axioms of equality as well as the target equation, and soft constraints representing the inclusion of input equations to an explanation. In that case, Max-SAT solvers could be used to find small explanations, in order to leverage efforts that combine decision procedures and optimization techniques.

Introduction

The Rodin platform [10] is an integrated design environment for the formal modeling notation Event-B [2]. Rodin is based on the Eclipse framework [25] and has an extensible architecture, where new features, or new versions of existing features, can be integrated by means of plug-ins. It supports the construction of formal models of systems as well as their refinement using the notation of Event-B, based on first-order logic, typed set theory and integer arithmetic. Event-B models should be consistent; for this purpose, Rodin generates proof obligations that need to be discharged (i.e., proved valid).

The proof obligations are represented internally as sequents, and a sequent calculus forms the basis of the verification machinery. Proof rules are applied to a sequent and produce zero, one or more new, usually simpler, sequents. A proof rule producing no sequent is called a discharging rule. The goal of the verification is to build a proof tree corresponding to the application of the proof rules, where all the leaves are discharging rules. In practice, the proof rules are generated by so-called reasoners. A reasoner is a plug-in that can either be standalone or use existing verification technologies through third-party tools. Most of the time, sequents are not amenable to finite domain encoding, and engines such as model checkers are not appropriate reasoners.

The usability of the Rodin platform, and of formal methods in general, greatly depends on several aspects of the verification activity:

Automation Ideally, the validity status of proof obligations is computed automatically by reasoners. If human interaction is required for discharging valid proof obligations (using an interactive theorem prover), productivity is negatively impacted.

Information Validation of proof obligations should not be sensitive to irrelevant modifications of the model. When modifying the model, large parts of the proof can be preserved if the precise facts used to validate each proof obligation are recorded. It is important that the reasoners are able to provide such sets of relevant facts, since they can then be used to automatically construct new proof rules to be stored and tried for after model changes. Also, other sequents (valid for the same reason) may be discharged by these rules without requiring another call to the reasoner.

In addition, when reasoners are able to generate counter-examples of failed proof obligations, this information can be very valuable to the user as hints to improve the model and the invariants.

Trust When a prover is used, either the tool itself or its results need to be certified; otherwise the confidence in the formal development is jeopardized.

In this paper, we address the application of a verification approach that may potentially fulfill these three requirements: Satisfiability Modulo Theory (SMT) solvers. SMT solvers can automatically handle large formulas of first-order logic with respect to some background theories, or a combination thereof, such as different fragments of arithmetic (linear and non-linear, integer and real), arrays, bit vectors, etc. They have been employed successfully to handle proof obligations with tens of thousands of symbols stemming from software and hardware verification. This paper extends the work presented in [15], and provides details of a translation of Event-B sequents to SMT input. The difficulty essentially lies in the way sets are translated. We here propose two approaches to tackle this challenge. Notice that these approaches could also be applied to other set-based formalisms such as the B method [1], TLA+ [20,19], VDM [16] and Z [27].

The SMT-LIB initiative provides a standard for the input language of SMT solvers, and, in its last version [5], a command language defining a common interface to interact with SMT solvers. We implemented a Rodin plug-in using this interface. The plug-in also extracts from the SMT solvers some additional information such as the relevant hypothesis. Some solvers (e.g. Z3 [12] and veriT [9]) are able to generate a comprehensive proof for validated formulas, which can be verified by a trusted proof checker [3]. In the longer term, besides automation, and information, trust may be obtained using a centralized proof manager. The plug-in is open-source, distributed under the same license as Rodin, and its source code is available in the main Rodin repository. The plug-in is easily installable by users through the update manager of the Rodin platform.

Overview. We start in Section 2 by giving some insights on the techniques employed in SMT solvers. Section 3 presents the translation of Rodin sequents to the SMT-LIB notation. Section 4 illustrates the approach through a simple example. Section 5 presents experimental results, based on the verification activities carried out for a variety of Event-B projects. We conclude by discussing future work. Throughout the paper, formulas are expressed using the Event-B syntax [21], and sentences in SMT-LIB are typeset using a typewriter font.

Solving SMT formulas

In this section, we provide some insight about the internals of SMT solvers, in order to give to the reader an idea of the kind of formulas that can successfully be handled by SMT solvers. A very schematic view of an SMT solver is presented in Figure 1. Basically it is a decision procedure for quantifier-free formulas in a rich language coupled with an instantiation module that handles the quantifiers in the formulas by grounding the problem. For quantified logic, SMT solvers are of course not decision procedures anymore, but they work well in practice if the necessary instances are easy to find and not too numerous.

We refer to [4] for more information about the techniques described in this section and SMT solving in general. There are several SMT solvers supporting quantifiers; the plug-in described in this paper makes use of Alt-Ergo [8], CVC3 [6], Z3 [12], and veriT [9]. This last solver is developed by two of the authors of this paper.

Quantifier-free formulas

Historically, the first goal of SMT solvers was to provide efficient decision procedures for expressive languages, beyond pure propositional logic. Those solvers have always been based on a cooperation of a Boolean engine, nowadays typically a SAT solver (see [7] for more information on SAT solver techniques and tools), and a theory reasoner to check the satisfiability of a set of literals in the considered language. The Boolean engine generates models for the Boolean abstraction of the input formula, whereas the theory reasoner refutes the sets of literals corresponding to these abstract models by conjunctively adding conflict clauses to the propositional abstraction. This exchange runs until either the Boolean abstraction is sufficiently refined for the Boolean reasoner to conclude that the formula is unsatisfiable, or the theory reasoner concludes that the abstract model indeed corresponds to a model of the formula.

The theory reasoners are themselves based on a combination of decision procedures for various fragments. In our context, the relevant decision procedures are congruence closure -to handle uninterpreted predicates and functionsdecision procedure for arrays (typically reduced to some kind of congruence closure), and linear arithmetic. It is possible, using the Nelson-Oppen combination method [22,26], to build a decision procedure for the union of the languages. The theory reasoner used in most SMT solvers is thus able to decide the satisfiability of literals on a language containing a mix of uninterpreted symbols, linear arithmetic symbols, and array operators.

For the theory reasoner and the SAT solver to cooperate successfully, some further techniques are necessary. Among these techniques, if a set of literals is found unsatisfiable, it is most valuable to generate small conflict clauses, in order to refine the Boolean abstraction as strongly as possible. Models of the propositional abstraction are checked for satisfiability while they are being built, so that unsatisfiability can be detected early. Finally, theory propagation, in which the theory reasoner provides hints for the SAT solver decisions, has proved to be very worthwhile in practice.

Instantiation techniques

Within SMT solvers, solving formulas with quantifiers is done by reduction to quantifier-free formulas, using instantiation. Indeed, formula ∀x ϕ(x) stands for a conjunction over all combinations of values for x. Any formula of the form ∀x ϕ(x) ⇒ ϕ(t), for any terms t, can be added conjunctively to the input without changing its truth value. To show that a formula is unsatisfiable, it is thus sufficient to find the right instances of quantified formulas to add to the input. In that context, even if the SMT solver abstracts ∀x ϕ(x) to a Boolean proposition, it is able to reason about the formulas with quantifiers. The quantifier instantiation module is responsible for producing lemmas of the form ∀x ϕ(x) ⇒ ϕ(t). Automatically finding the right instances of quantified formulas is a key issue for the verification of sequents (as well as proof obligations produced in the context of a number of software verification tools). Generating too many instances may overload the solver with useless information and exhaust computing resources. Generating too few instances will result in an "unknown", and useless, verdict. Handling quantifiers within SMT solvers is still a very active research subject, and the methods to handle quantifiers vary greatly from one solver to another. We report here how veriT copes with quantified formulas. Several instantiation techniques are applied in turn: trigger-based, sort-based and superposition techniques.

The trigger-based and sort-based instantiation techniques are applied to topmost quantifiers, that is, to quantifiers that are not themselves in the scope of other quantifiers. Remember that, when checking the satisfiability of formulas, existential quantifiers with positive polarity and universal quantifiers with negative polarity can be eliminated by Skolemization. This satisfiability preserving transformation replaces suitable quantified variables by witnesses, introducing new uninterpreted symbols (constants or functions). In veriT, Skolemization automatically occurs for top-most quantifiers, whereas Skolemizable quantifiers in the scope of non-Skolemizable quantifiers are not eliminated. As a consequence, only Skolem constants are introduced, and no Skolem functions. Instantiation will remove top-most non-Skolemizable quantifiers, some quantifiers in the instance may then become top-most Skolemizable quantifiers in the process, and are in turn eliminated with the introduction of Skolem constants. This strategy is effective in practice.

In a quantified formula Qx ϕ(x), a trigger is a set of terms T = {t 1 , • • • t n } such that the free variables in T are the quantified variables x and each t i is a sub-term of the matrix ϕ(x) of the quantified formula. Trigger-based instantiation consists in finding, in the formula, sets of ground terms T that match T , i.e., such that there is a substitution σ on x, where the homomorphic extension of σ over T yields T . Each such substitution defines an instantiation of the original quantified formula. Some verification systems allow the user to specify instantiation triggers. This is not the case in Rodin, and veriT applies heuristics to annotate quantified formulas with triggers.

If the trigger-based approach does not yield any new instance, veriT falls back to sort-based instantiation. All ground terms in the formula are collected, and each quantified formula is instantiated with every term that has the same type as the quantified variable.

Finally, veriT also features a module to communicate with a superpositionbased first-order logic automated theorem prover, namely the E prover [24]. It is built upon automated deduction techniques such as rewriting, subsumption, and superposition and is capable of identifying the unsatisfiability of a set of quantified and non-quantified formulas. When such a set is found satisfiable, lemmas are extracted from its output and communicated to the other reasoning modules of veriT. The E prover, like many saturation-based first-order provers, is complete for first-order logic with equality.

Unsatisfiable core extraction

Additionally to the satisfiability response, it is possible, in case of an unsatisfiable input, to ask for an unsatisfiable core. It may indeed be very valuable to know which hypotheses are necessary to prove a goal in a verification condition. For instance, the sequent (1) discussed in Section 4 and translated into the SMT input in Figure 6 is valid independently of the assertion labeled grd1; the SMT input associates labels to the hypotheses, guards, and goals, using the reserved SMT-LIB annotation operator !. A solver implementing the SMT-LIB unsatisfiable core feature could thus return the list of hypotheses used to validate the goals. In the case of the example in Figure 6, the guard is not necessary to prove unsatisfiability, and would therefore not belong to a good unsatisfiable core.

Recording unsatisfiable cores for comparison with new proof obligations is particularly useful in our context. Indeed, users of the Rodin platform will want to modify their models and their invariants, resulting in a need of validating again proof obligations mostly but not fully similar to already validated ones. If the changes do not impact the relevant hypotheses and goal of a proof obligation, comparison with the (previous) unsatisfiable core will discharge the proof obligation and the SMT solver will not need to be run again. Also a same unsatisfiable core is likely to discharge similar proof obligations, for instance generated for a similar transition, but differing for the guard.

The unsatisfiable core production for the veriT solver is related to the proof production feature. The solver is indeed able to produce a proof, and it has moreover a facility to prune the proof of unnecessary proof steps and hypotheses. It suffices thus to check the pruned proof and collect all hypotheses in that proof to obtain a super-set of the unsatisfiable core that is often minimal in practice. Other approaches for unsatisfiable core extraction for SMT are presented and discussed in [4].

Translating Event-B to SMT

Figure 2 gives a schematic view of the cooperation framework between Rodin and the SMT solver. Within the Rodin platform, each proof obligation is represented as a sequent, i.e. a set of hypotheses and a conclusion. These sequents are discharged using Event-B proof rules. Our strategy to prove an Event-B sequent is to build an SMT formula, call an SMT solver on this formula, and, on success, introduce a new suitable proof rule. This strategy is presented as a tactic in the Rodin user interface. Since SMT solvers answer the satisfiability question, it is necessary to take the negation of the sequent (to be validated) in order to build a formula to be refuted by the SMT solver. If the SMT solver does not implement unsatisfiable core generation, the proof rule will assert that the full Event-B sequent is valid (and will only be useful for that specific sequent). Otherwise an unsatisfiable core -i.e., the set of facts necessary to RODIN Event B sequent negation of Event B sequent SMT formula SMT response:

• SAT • UNSAT • proof • relevant hypotheses Event B proof rule

SMT solver

Figure 2: Schematic view of the interaction between Rodin and SMT solvers.

prove that the formula is unsatisfiable -is supplied to Rodin, which will extract a stronger Event-B proof rule containing only the necessary hypotheses. This stronger proof rule will hopefully be applicable to other Event-B sequents. If, however, the SMT solver is not successful, the application of the tactic has failed and the proof tree remains unchanged. The SMT-LIB standard proposes several "logics" that specify the interpreted symbols that may be used in the formulas. Currently, however, none of these logics fits exactly the language of the proof obligations generated by Rodin. There exists a proposal for such a logic [18], but the existing SMT solvers do not yet implement corresponding reasoning procedures. Our pragmatic approach is thus to identify subsets of the Event-B logics that may be handled by the current tools, either directly or through some simple transformations. The translation takes as input the Event-B proof obligations. The representation of proof obligations is such that each identifier has been annotated with its type. In the type system, integers and Booleans are predefined, and the user may create new basic sets, or compose existing types with the powerset and Cartesian product constructors. Translating Boolean and arithmetic constructs is mostly straightforward, since a direct syntactic translation may be undertaken for some symbols: Boolean operators and constants, relational operators, and most of arithmetic (division and exponentiation operators are currently translated as uninterpreted symbols). As an example of transformation of an Event-B sequent to an SMT formula, consider the sequent with goal 0 < n + 1 under the hypothesis n ∈ N; the type environment is {n • • Z} and the generated SMT-LIB formula is:

(set-logic AUFLIA) (declare-fun n () Int) (assert (>= n 0)) (assert (not (< 0 (+ n 1)))) (check-sat)
The main issue in the translation of proof obligations to SMT-LIB is the representation of the set-theoretic constructs. We present successively two approaches. The simplest one, presented shortly for completeness, is based on the representation of sets as characteristic predicates [13]. Since SMT solvers handle first-order logic, this approach does not make it possible to reason about sets of sets. The second approach removes this restriction. It uses the ppTrans translator, already available in the Rodin platform; this translator removes most set-theoretic constructs from proof obligations by systematically expanding their definitions.

The λ-based approach

This approach implements and extends the principles proposed in [13] to handle simple sets. Essentially, a set is identified with its characteristic function. For instance the singleton {1} is identified with (λx • • Z | x = 1) and the empty set is identified with the polymorphic λ-expression (λx • • X | FALSE), where X is a type variable. The union of (two) sets is a polymorphic higher-order function (λ(S

1 • • X → BOOL) → (S 2 • • X → BOOL) | (λx • • X | S 1 (x) ∨ S 2 (x))), etc.
SMT-LIB does not provide a facility for λ-expressions, and has limited support for polymorphism. This approach requires several extensions to SMT-LIB: λ-expressions, a polymorphic sort system, and macro-definitions. Those extensions are actually implemented in the veriT parser. Consider the sequent A • • P(Z) A ∪ {a} = A, the translation to this extended SMT-LIB language produces:

(declare-fun A (Int) Bool) (declare-fun a () Int) (define-fun (par (X) (union ((S1 (X Bool)

) (S2 (X Bool))) (X Bool) (lambda ((x X)) (or (S1 x) (S2 x)))))) (define-fun enum ((x Int)) Bool (= x a)) (assert (not (= (union A enum) A))) (check-sat)
where X denotes a sort variable. The function definitions union and enum are inserted by the translator. The former is part of a corpus of definitions for most of the set-theoretic constructs (see [13,14] for details). The latter is created onthe-fly by the translator to denote the set {a}. Both definitions are composed of a list of sorted parameters, the sort of the result, and the body expressing the value of the result. The macro processor implemented in veriT transforms this goal to

(not (forall ((x Int)) (iff (or (A x) (= x a)) (A x))))
i.e., a first-order formula that may then be handled using usual SMT solving techniques. It is also possible to use veriT only as a pre-processor to produce plain SMT-LIB formulas that are amenable to verification using any SMT-LIB compliant solver. As already mentioned, the main drawback of this approach is that sets of sets cannot be handled. It is thus restricted to simple sets and relations. Furthermore its reliance on extensions of the SMT-LIB format creates a dependence on veriT as a macro processor. The next approach lifts these restrictions.

P ::= P ⇒ P | P ≡ P | P ∧ • • • ∧ P | P ∨ • • • ∨ P | ¬P | ∀ L • P | ∃ L • P | A = A | A < A | A ≤ A | M ∈ S | B = B | I = I L ::= I • • • I I ::= Name A ::= A -A | A div A | A mod A | A exp A | A + • • • + A | A × • • • × A | -A | I | IntegerLiteral B ::= true | I M ::= M → M | I | integer | bool S ::= I

The ppTrans approach

Our second approach uses the translator ppTrans provided by the Predicate Prover available in Rodin [17]. This tool translates an Event-B formula to an equivalent formula in a subset of the Event-B mathematical language. The grammar of this subset is shown in Figure 3. Note that the sole set-theoretic symbol is the membership predicate. In addition, the translator performs decomposition of binary relations and purification, namely it separates arithmetic, Boolean and set-theoretic terms. Finally ppTrans performs basic Boolean simplifications on formulas. In the following, we provide details on those transformations, using the notation ϕ ϕ to express that the formula (or sub-term) ϕ is rewritten to ϕ . Not only does this approach make the plug-in independent of veriT, but it is also more general with respect to the translation of relations and functions. However, in the class of formulas suitable for the λ-based approach, ppTrans would produce similar results.

Maplet-hiding variables. The rewriting system implemented in ppTrans cannot directly transform identifiers that are of type Cartesian product. In a preprocessing phase, such identifiers are thus decomposed, so that further rewriting rules may be applied. This decomposition introduces fresh identifiers of scalar type (members of some given set, integers or Booleans) that name the components of the Cartesian product. Technically, this pre-processing is as follows. We assume the existence of an attribute T , such that T (e) is the type of expression e. Also, let fv(e) denote the free identifiers occurring in expression e. The decomposition of the Cartesian product identifiers is specified, assuming an unlimited supply of fresh identifiers (e.g. x 0 , x 1 ,. . . ), using the following two definitions ∇ and ∇ T :

∇(i) = ∇ T (T (i)) if i is a product identifier, i otherwise. ∇ T (T ) = ∇ T (T 1 ) → ∇ T (T 2 ) if ∃T 1 , T 2 •T = T 1 × T 2 , a fresh identifier x i otherwise. For instance, assume x • • Z × (Z × Z); then ∇(x) = x 0 → (x 1 → x 2 ) and fv(∇(x)) = {x 0 , x 1 , x 2 } are fresh identifiers.
The pre-processing behaves as follows:

• Quantified sub-formulas ∀x • ϕ(x), such that x is a product identifier, are rewritten to

∀fv(∇(x)) • ϕ[∇(x)/x],
where e[e /x] denotes expression e where expression e has been substituted for all free occurrences of x.

Ex. ∀a•a = 1 → (2 → 3) ∀a 0 , a 1 , a 2 • a 0 → (a 1 → a 2 ) = 1 → (2 → 3).
• Let ψ denote the top-level formula and let x 1 . . . x n be the free Cartesian product identifiers of ψ. Then:

ψ ∀fv(∇(x 1 )) • • • fv(∇(x n ))• (x 1 = ∇(x 1 ) ∧ • • • x n = ∇(x n )) ⇒ ψ[∇(x 1 )/x 1 ] • • • [∇(x n )/x n ]. Ex. ψ ≡ a = b ∧ a ∈ S with typing {a • • S, b • • S, S • • P(Z × Z)}: ψ ∀x 0 , x 1 , x 2 , x 3 • (a = x 0 → x 1 ∧ b = x 2 → x 3 ) ⇒ (x 0 → x 1 = x 2 → x 3 ∧ x 0 → x 1 ∈ S)
Purification. The goal of this phase is to obtain pure terms, i.e. terms that do not mix symbols of separate syntactic categories: arithmetic, predicate, set, Boolean, and maplet symbols. This is done by introducing new variables. In Event-B, heterogeneous terms result from the application of symbols with a signature with different sorts (e.g. symbol ⊆ yields a predicate from two sets). This phase also eliminates some syntactic sugar. Figure 4 depicts the different syntactic categories, how the Event-B operators relate them, and the effect of desugarization. There is an arrow from category X to category Y if a term from X may have an argument in Y . For instance . ∈ labels the arrow from P to A since the left argument of ∈ may be an arithmetic term, e.g. in x + y ∈ S.

First, let us introduce informally the notation

Q ? P [e * ],
where Q is ∀ or ∃, P a predicate, and e an expression in P such that the syntactic category of e is not the same as that of its parent (identifiers are considered to belong to all syntactic categories). This denotes the possible introduction of the quantifier Q on a fresh variable, so that heterogeneous sub-terms in e are purified, yielding e 1.

∃ ? (a → (1 → 2)) * ∈ S represents ∃x 0 , x 1 •x 0 = 1 ∧ x 1 = 2 ∧ a → (x 0 →
x 1 ) ∈ S as 1 and 2 are not in the same syntactic category as the maplet. 2. ∀ ? (a → b) * ∈ S does not introduce a quantification and denotes a → b ∈ S.

Appendix A presents the rewriting rules implemented in ppTrans. For readability, they are grouped thematically and the presentation order is not the same as the rewriting order. The symbols relating the syntactic categories P (predicates) and S (sets) are reduced to membership (∈) and equality (=) by application of the rules A.1-A.8 (see Appendix A.1). Moreover rules A.1 and A.2 are also applied when the arguments belong to other syntactic categories and are responsible for the elimination of all the occurrences of symbols = and ∈. Applications of the equality symbol between syntactic categories S, M and B are removed by rules A.9-A.18 (Appendix A.2). Due to the symmetry property of equality, ppTrans also applies a symmetric version of each such rule. The symbols that embed arithmetic terms are taken care of with the rules in Appendix A.3. Rules A.19-A.21 first perform purification, and are followed by the application of rules A.22-A.29, responsible for the elimination of the symbols. Appendix A.4 contains rules to rewrite applications of the set membership symbol according to the rightmost argument. Rules A.30-A.39 expand the definitions for the different kinds of relation symbols. Rules A. 40-A.61 handle miscellaneous other cases. Finally, Appendix A.5 presents the rules to rewrite applications of the set membership symbol according to both arguments, where the first argument is always a maplet. Again, through the application of rules A.62 to A.77, several symbols may be eliminated from the proof obligations.

All the rules in Appendix A are either sound purification rules, or the equivalence of the left and right side terms can easily be derived from the definitions (see [1]) of the eliminated symbols. Purification rules (Rules A.17, A.19 -A.21, A.44) eliminate heterogeneous terms and are only applied once. It is not difficult to order all other rules such that no eliminated symbol is introduced in subsequent rules. The rewriting system is thus indeed terminating.

Output to SMT-LIB format. Once ppTrans has completed rewriting, the resulting proof obligation is ready to be output in SMT-LIB format. The translation from ppTrans' output to SMT-LIB follows specific rules for the translation of the set membership operator. For instance assume the input has the following typing environment and formulas:

Typing environment Formulas a • • S b • • T c • • U A • • P(S) r • • P(S × T ) s • • P(S × T × U ) a ∈ A a → b ∈ r a → b → c ∈ s
Firstly, for each basic set found in the proof obligation, the translation produces a sort declaration in SMT-LIB. However, as there is currently no logic in the SMT-LIB with powerset and Cartesian product sort constructors, ppTrans handles them by producing an additional sort declaration for each combination of basic sets (either through powerset or Cartesian product). Translating the typing environment thus produces a sort declaration for each basic set, and combination thereof found in the input. In SMT-LIB, sorts have a name and an arity, which is non-null for polymorphic sorts. The sorts produced have all arity 0, and for the above example, the following is produced:

S (declare-sort S 0) T (declare-sort T 0) U (declare-sort U 0) P(S) (declare-sort PS 0) P(S × T ) (declare-sort PST 0) P(S × T × U ) (declare-sort PSTU 0)
Secondly, for each constant, the translation produces a function declaration of the appropriate sort:

a • • S (declare-fun a () S) b • • T (declare-fun b () T) c • • U (declare-fun c () U) A • • P(S) (declare-fun A () PS) r • • P(S × T ) (declare-fun r () PST) s • • P(S × T × U ) (declare-fun s () PSTU)
Third, for each type occurring at the right-hand side of a membership predicate, the translation produces fresh SMT function symbols: The Event-B atoms can then be translated as follows:

a ∈ A (MS0 a A) a → b ∈ r (MS1 a b r) a → b → c ∈ s (MS2 a b c s) For instance, A∪{a} = A would be translated to ∀x•(x ∈ A∨x = a)⇔x ∈ A, that is, in SMT-LIB format: (forall ((x S)) (= (or (MS0 x A) (= x a)) (MS0 x A)))
While the approach presented here covers the whole Event-B mathematical language and does not require polymorphic types or specific extensions to the SMT-LIB language, the semantics of some Event-B constructs is approximated because some operators become uninterpreted in SMT-LIB (chiefly membership but also some arithmetic operators such as division and exponentiation). However, we can recover their interpretation by adding axioms to the SMT-LIB benchmark, at the risk of decreasing the performance of the SMT solvers. Some experimentation is thus needed to find a good balance between efficiency and completeness.

Indeed, it appears experimentally that including some axioms of set theory to constrain the possible interpretations of the membership predicate greatly improves the number of proof obligations discharged. In particular, the axiom of elementary set (singleton part) is necessary for many Rodin proof obligations. The translator directly instantiates the axiom for all membership predicates. Assuming MS is the membership predicate associated with sorts S and PS, the translation introduces thus the following assertion:

(assert (forall ((x S)) (exists ((X PS)) (and (MS x X) (forall ((y S)) (=> (MS y X) (= y x)))))))
This particular assertion eliminates non-standard interpretations where some singleton sets do not exist. Without it, some formulas are satisfiable because of spurious models and the SMT solvers are unable to refute them.

A small Event-B example

As a concrete example of translation, this section presents the model of a simple job processing system consisting of a job queue and several active jobs. We define a given set JOBS to represent the jobs. The state of the model has two variables: queue (the jobs currently queued) and active (the jobs being processed). This state is constrained by the following invariants:

inv1 : active ⊆ JOBS (typing) inv2 : queue ⊆ JOBS (typing)
inv3 : active ∩ queue = ∅ (a job can not be both active and queued)

One of the events of the system describes that a job leaves the queue and becomes active. It is specified as follows:

Event SCHEDULE = (some queued job j becomes active) any j where grd1 : j ∈ queue (the job j is in the queue) then act1 : active := active ∪ {j } (the job becomes active) act2 : queue := queue \ {j } (the job is removed from the queue) end

To verify that the invariant labeled inv3 is preserved by the SCHEDULE event, the following sequent must be proved valid:

inv1, inv2, inv3, grd1 (active ∪ {j}) active' ∩ (queue \ {j}) queue' = ∅ . (1)
The generated proof obligations thus aims to show that the following formula is unsatisfiable:

active ⊆ JOBS ∧ queue ⊆ JOBS ∧ active ∩ queue = ∅ ∧ j ∈ queue ∧ ¬((active ∪ {j}) ∩ (queue \ {j}) = ∅) .
This proof obligation does not contain sets of sets and both approaches apply. Figure 5 presents the SMT-LIB input obtained when the approach described in section 3.1 is applied. Line 2 contains the declaration of the sort corresponding to the given set JOBS. Lines 3-5 contain the declarations of the uninterpreted function symbols of the proof obligation, and are produced using the typing environment. Note that the sets queue and active are represented by unary predicate symbols. Next, the macros corresponding to the set operators ∅, ∈, (set-logic QF_AUFLIA) (declare-sort JOBS 0) (declare-fun active (JOBS) Bool) (declare-fun queue (JOBS) Bool) (declare-fun j () JOBS) (define-fun (par (X) (emptyset ((x X)) Bool false))) (define-fun (par (X) (in ((x X) (s (X Bool))) Bool (s x)))) (define-fun (par (X) (inter ((s1 (X Bool)) (s2 (X Bool))) (X Bool) (lambda ((x X)) (and (s1 x) (s2 x)))))) (define-fun (par (X) (setminus ((s1 (X Bool)) (s2 (X Bool))) (X Bool) (lambda ((x X)) (and (s1 x) (not (s2 x))))))) (define-fun (par (X) (union ((s1 (X Bool)) (s2 (X Bool))) (X Bool) (lambda ((x X)) (or (s1 x) (s2 x)))))) (define-fun enum ((elem JOBS)) Bool (= elem j)) (define-fun enum0 ((elem0 JOBS)) Bool (= elem0 j)) (assert (= (inter active queue) emptyset)) (assert (in j queue)) (assert (not (= (inter (union active enum) (setminus queue enum0)) emptyset))) (check-sat) (set-logic AUFLIA) (declare-sort JOBS 0) (declare-sort PJ 0) (declare-fun MS (JOBS PJ) Bool) (declare-fun active () PJ) (declare-fun j () JOBS) (declare-fun queue () PJ) (assert (! (forall ((x JOBS))

(not (and (MS x active) (MS x queue)))) :named inv3)) (assert (! (MS j queue) :named grd1)) (assert (! (not (forall ((x0 JOBS))

(not (and (or (MS x0 active ∩, \, and ∪ are defined in lines 6-13. Lines 14-15 are the definitions of a macro that represents the singleton set {j} (it occurs twice in the formula). Lines 16-19 are the result of the translation of the proof obligation itself.

) (= x0 j)) (MS x0 queue) (not (= x0 j)))))) :named goal)) (check-sat)
Figure 6 presents the SMT-LIB input resulting from the translation approach described in section 3.2. Since the proof obligation includes sets of JOBS, a corresponding sort PJ and membership predicate MS are declared in lines 3-4. Then, the function symbols corresponding to the free identifiers of the sequent are declared at lines 5-7. Finally, the hypotheses and the goal of the sequent are translated to named assertions (lines 8-14).

The sequent described in this section is very simple and is easily verified by both Atelier-B provers and SMT solvers. It is noteworthy that the plug-in inspects sequents to decide which approach is applied. When the sequents contains no sets or only simple sets (i.e., no sets of sets), the λ-based approach is applied. Otherwise, the plug-in employs the ppTrans approach. The next section reports experiments with a large number of proof obligations and establishes a better basis to compare the effectiveness of these different verification techniques.

Experimental results

We evaluated experimentally the effectiveness of using SMT solvers as reasoners in the Rodin platform by means of the techniques presented in this paper. This evaluation complements the experiments presented in [15] and reinforces their conclusions. We established a library of 2,456 proof obligations stemming from Event-B developments collected by the European FP7 project Deploy and publicly available on the Deploy repository1 . These developments originate from examples from Abrial's book [2], academic publications, tutorials, as well as industrial case studies.

One main objective of introducing new reasoners in the Rodin platform is to reduce the number of valid proof obligations that need to be discharged interactively by humans. Consequently, the effectiveness of a reasoner is measured by the number of proof obligations proved automatically by the reasoner.

Obviously, effectiveness should depend on the computing resources given to the reasoners. In practice, the amount of memory is seldom a bottleneck, and usually the solvers are limited by setting a timeout on their execution time. In the context of the Rodin platform, the reasoners are executed by synchronous calls, and the longer the time limit, the less responsive is the framework to the user. We have experimented different timeouts and our experiments have shown us that a timeout of one second seems a good trade-off: doubling the timeout to two seconds increases by fewer than 0.1% the number of verified proof obligations, while decreasing the responsiveness of the platform.

Table 1 compares different reasoners on our set of benchmarks. The second column corresponds to Rodin internal normalization and simplification proce-dures. It shows that more than half of the generated proof obligations necessitate advanced theorem-proving capabilities to be discharged. The third column is a special-purpose reasoner, namely Atelier-B provers. They were originally developed for the B method and are also available in the Rodin platform. Although they are extremely effective, the Atelier-B provers now suffer from legacy issues. The last five columns are various SMT solvers applied to the proof obligations generated by the plug-in. The SMT solvers were used with a timeout of one second, on a computer equipped with an Intel Core i7-4770, cadenced at 3.40 GHz, with 24 GB of RAM, and running Ubuntu Linux 12.04. They show decent results, but they are not yet as effective reasoners as the Atelier-B theorem provers. Although this comparison is interesting to evaluate and compare the different reasoners, it is not sufficient to evaluate the effectiveness of the approach presented in this paper. Indeed, nothing prevents users to use several other reasoners once one has failed to achieve its goal. In Table 2, we report how many proof obligations remain unproved after applying the traditional reasoners (Atelier-B theorem provers and the Rodin reasoner) in combination with each SMT solver, and with all SMT solvers. Each of the SMT solvers seems a valuable complement to the special-purpose provers. However, we would also like to know whether the reasoning capacity of some of these solvers is somehow subsumed by another solver, or whether each SMT solver could provide a significant contribution towards reducing the number of proof obligations that need to be discharged by humans. This comparison signals the results obtained when all available reasoners are applied: only 31 proof obligations are unproved, down from 196 resulting from the application of Atelier-B provers. It is also noteworthy that even though each SMT solver is individually less effective than Atelier-B provers, applied altogether, they prove all but 97 proof obligations. The important conclusion of our experiments is that there is strong evidence that SMT solvers complement in an effective and practical way the Atelier B provers, yielding significant improvements in the usability of the Rodin platform and its effectiveness to support the development of Event-B models.

Conclusion

SMT solving is a formal verification technique successfully applied to various domains including verification. SMT solvers do not have built-in support for settheoretic constructs found in Rodin sequents. We presented here a translation approach to tackle this issue. We evaluated experimentally the efficiency of SMT solvers against proof obligations resulting from the translation of Rodin sequents. In our sample of industrial and academic projects, the use of SMT solvers on top of Atelier B provers reduces significantly the number of unverified sequents. This plug-in is available through the integrated software updater of Rodin (instructions at http://wiki.event-b.org/index.php/SMT_Plug-in).

The results are very encouraging and motivate us to progress further by implementing and evaluating new translation approaches, such as representing functions using arrays in the line of [11]. Elaborating strategies to apply different reasoners, based on some characteristics of the sequents is also a promising line of work. Another feature of some SMT solvers is that they can provide models when a formula is satisfiable. In consequence, it would be possible, with additional engineering effort, to use such models to report counter-examples in Rodin.

We believe that the approach presented in this paper could also be applied successfully for other set-based formalisms such as: the B method, TLA+, VDM and Z.

Cooperation of deduction tools is very error-prone, not only because it relies on the correctness of many large and complex tools, but also because of the translations. Certification of proofs in a centralized trusted proof manager would be the answer to this problem. Preliminary works in this direction exist [23].

A Gentle Non-Disjoint Combination of Satisfiability Procedures

Paula Chocron 1,3 , Pascal Fontaine 2 , and Christophe Ringeissen Abstract. A satisfiability problem is often expressed in a combination of theories, and a natural approach consists in solving the problem by combining the satisfiability procedures available for the component theories. This is the purpose of the combination method introduced by Nelson and Oppen. However, in its initial presentation, the Nelson-Oppen combination method requires the theories to be signature-disjoint and stably infinite (to guarantee the existence of an infinite model). The notion of gentle theory has been introduced in the last few years as one solution to go beyond the restriction of stable infiniteness, but in the case of disjoint theories. In this paper, we adapt the notion of gentle theory to the non-disjoint combination of theories sharing only unary predicates (plus constants and the equality). Like in the disjoint case, combining two theories, one of them being gentle, requires some minor assumptions on the other one. We show that major classes of theories, i.e. Löwenheim and Bernays-Schönfinkel-Ramsey, satisfy the appropriate notion of gentleness introduced for this particular non-disjoint combination framework.

Introduction

The design of satisfiability procedures has attracted a lot of interest in the last decade due to their ubiquity in SMT (Satisfiability Modulo Theories [4]) solvers and automated reasoners. A satisfiability problem is very often expressed in a combination of theories, and a very natural approach consists in solving the problem by combining the satisfiability procedures available for each of them. This is the purpose of the combination method introduced by Nelson and Oppen [15]. In its initial presentation, the Nelson-Oppen combination method requires the theories in the combination to be (1) signature-disjoint and (2) stably infinite (to guarantee the existence of an infinite model). These are strong limitations, and many recent advances aim to go beyond disjointness and stable infiniteness. Both corresponding research directions should not be opposed. In both cases, the problems are similar, i.e. building a model of T 1 ∪ T 2 from a model of T 1 and a model of T 2 . This is possible if and only if there exists an isomorphism between the restrictions of the two models to the shared signature [24]. The issue is to define a framework to enforce the existence of this isomorphism. In the particular case of disjoint theories, the isomorphism can be obtained if the domains of the models have the same cardinality, for instance infinite; several classes of kind theories (shiny [25], polite [19], gentle [9]) have been introduced to enforce a (same) domain cardinality on both sides of the combination. For extensions of Nelson-Oppen to non-disjoint cases, e.g. in [24,27], cardinality constraints also arise. In this paper, we focus on non-disjoint combinations for which the isomorphism can be simply constructed by satisfying some cardinality constraints. More precisely, we extend the notion of gentle theory to the non-disjoint combination of theories sharing only unary predicates (plus constants and the equality). Some major classes of theories fit in our non-disjoint combination framework.

Contributions. The first contribution is to introduce a class of P-gentle theories, to combine theories sharing a finite set of unary predicates symbols P. The notion of P-gentle theory extends the one introduced for the disjoint case [9]. Roughly speaking, a P-gentle theory has nice cardinality properties not only for domains of models but also more locally for all Venn regions of shared unary predicates. We present a combination method for unions of P-gentle theories sharing P. The proposed method can also be used to combine a P-gentle theory with another arbitrary theory for which we assume the decidability of satisfiability problems with cardinality constraints. This is a natural extension of previous works on combining non-stably infinite theories, in the straight line of combination methods à la Nelson-Oppen. Two major classes of theories are P-gentle, namely the Löwenheim and Bernays-Schönfinkel-Ramsey (BSR) classes. We characterize precisely the cardinality properties satisfied by Löwenheim theories. As a side contribution, bounds on cardinalities given in [8] have been improved, and we prove that our bounds are optimal. Our new result establishes that Löwenheim theories are P-gentle.

We prove that BSR theories are also P-gentle. This result relies on a nontrivial extension of Ramsey's Theorem on hypergraphs. This extension should be considered as another original contribution, since it may be helpful as a general technique to construct a model preserving the regions. Related Work. Our combination framework is a way to combine theories with sets. The relation between (monadic) logic and sets is as old as logic itself, and this relation is particularly clear for instance considering Aristotle Syllogisms. It is however useful to again study monadic logic, and more particularly the Löwenheim class, and in view of the recent advances in combinations with nondisjoint and non-stably infinite theories.

In [26], the authors focus on the satisfiability problem of unions of theories sharing set operations. The basic idea is to reduce the combination problem into a satisfiability problem in a fragment of arithmetic called BAP A (Boolean Algebra and Presburger Arithmetic). Löwenheim and BSR classes are also considered, but infinite cardinalities were somehow defined out of their reduction scheme, whilst infinite cardinalities are smoothly taken into account in our combination framework. In [26], BSR was shown to be reducible to Presburger. We here give a detailed proof. We believe such a proof is useful since it is more complicated that it may appear. In particular, our proof is based on an original (up to our knowledge) extension of Ramsey's Theorem to accommodate a domain partitioned into (Venn) regions. Finally, the notion of P-gentleness defined and used here is stronger than semi-linearity of Venn-cardinality, and allows non-disjoint combination with more theories, e.g. the guarded fragment.

In [21,22], a locality property is used to properly instantiate axioms connecting two disjoint theories. Hence, the locality is a way to reduce (via instantiation) a non-disjoint combination problem to a disjoint one. In that context, cardinality constraints occur when considering bridging functions over a data structure with some cardinality constraints on the underlying theory of elements [START_REF] Zhang | Decision procedures for term algebras with integer constraints[END_REF]21,23].

In [12], Ghilardi proposed a very general model-theoretic combination framework to obtain a combination method à la Nelson-Oppen when T 1 and T 2 are two compatible extensions of the same shared theory (satisfying some properties). This framework relies on an application of the Robinson Joint Consistency Theorem (roughly speaking, the union of theories is consistent if the intersection is complete). Using this framework, several shared fragments of arithmetic have been successfully considered [12,16,17]. Due to its generality, Ghilardi's approach is free of cardinality constraints.

It is also possible to consider a general semi-decision procedure for the unsatisfiability problem modulo T 1 ∪ T 2 , e.g. a superposition calculus. With the rewrite-based approach initiated in [3], the problem reduces to proving the termination of this calculus. General criteria have been proposed to get modular termination results for superposition, when T 1 and T 2 are either disjoint [2] or non-disjoint [20]. Notice that the superposition calculus can also be used as a deductive engine to entail some cardinality constraints, as shown in [5].

Structure of the paper. Section 2 introduces some classical notations and definitions. In Section 3, we introduce the notion of P-gentle theory and we present the related combination method for unions of theories sharing a (non-empty finite) set P of unary predicate symbols. All the theories in the Löwenheim class and in the BSR class are P-gentle, as shown respectively in Section 4 and in Section 5. A simple example is given in Section 6. The conclusion (Section 7) discusses the current limitations of our approach and mentions some possible directions to investigate. Our extension of Ramsey's Theorem can be found in Appendix A.

Notation and Basic Definitions

A first-order language is a tuple L = V, F, P such that V is an enumerable set of variables, while F and P are sets of function and predicate symbols. Every function and predicate symbol is assigned an arity. Nullary predicate symbols are called proposition symbols, and nullary function symbols are called constant symbols. A first-order language is called relational if it only contains function symbols of arity zero. A relational formula is a formula in a relational language. Terms, atomic formulas and first-order formulas over the language L are defined in the usual way. In particular an atomic formula is either an equality, or a predicate symbol applied to the right number of terms. Formulas are built from atomic formulas, Boolean connectives (¬, ∧, ∨, ⇒, ≡), and quantifiers (∀, ∃). A literal is an atomic formula or the negation of an atomic formula. Free variables are defined in the usual way. A formula with no free variables is closed, and a formula without variables is ground. A universal formula is a closed formula ∀x 1 . . . ∀x n .ϕ where ϕ is quantifier-free. A (finite) theory is a (finite) set of closed formulas. Two theories are disjoint if no predicate symbol in P or function symbol in F appears in both theories, except constants and equality.

An interpretation I for a first-order language L provides a non empty domain D, a total function I[f ] : D r → D for every function symbol f of arity r, a predicate I[p] ⊆ D r for every predicate symbol p of arity r, and an element I[x] ∈ D for every variable x. The cardinality of an interpretation is the cardinality of its domain. The notation I x1/d1,...,xn/dn for x 1 , . . . , x n different variables stands for the interpretation that agrees with I, except that it associates d i ∈ D to the variable x i , 1 ≤ i ≤ n. By extension, an interpretation defines a value in D for every term, and a truth value for every formula. We may write I |= ϕ whenever I[ϕ] = . Given an interpretation I on domain D, the restriction I of I on D ⊆ D is the unique interpretation on D such that I and I interpret predicates, functions and variables the same way on D . An extension I of I is an interpretation on a domain D including D such that I restricted to D is I.

A model of a formula (theory) is an interpretation that evaluates the formula (resp. all formulas in the theory) to true. A formula or theory is satisfiable if it has a model; it is unsatisfiable otherwise. A formula

G is T -satisfiable if it is satisfiable in the theory T , that is, if T ∪ {G} is satisfiable. A T -model of G is a model of T ∪ {G}. A formula G is T -unsatisfiable if it
has no T -models. In our context, a theory T is decidable if the T -satisfiability problem for sets of (ground) literals is decidable in the language of T (extended with fresh constants).

Consider an interpretation I on a language with unary predicates p 1 , . . . , p n and some elements D in the domain of this interpretation. Every element d ∈ D belongs to a Venn region v(d) = v 1 . . . v n ∈ { , ⊥} n where v i = I[p i ](d). We denote by D v ⊆ D the set of elements of D in the Venn region v. Notice also that, for a language with n unary predicates, there are 2 n Venn regions. Given an interpretation I, D c denotes the subset of elements in D associated to constants by I. Naturally, D c v denotes the set of elements associated to constants that are in the Venn region v.

Gentle Theories Sharing Unary Predicates

From now on, we assume that P is a non-empty finite set of unary predicates. A P-union of two theories T 1 and T 2 is a union sharing only P, a set of constants and the equality. There are only a finite number of arrangements for given sets S and P.

Given a theory T whose signature includes P and a model M of T on domain D, the P-cardinality κ is the tuple of cardinalities of all Venn regions of P in M (κ v will denote the cardinality of the Venn region v). The following theorem (specialization of general combination lemmas in e.g. [24,25]) states the completeness of the combination procedure for P-unions of theories: Theorem 1. Consider a P-union of theories T 1 and T 2 whose respective languages L 1 and L 2 share a finite set S of constants, and let L 1 and L 2 be sets of literals, respectively in L 1 and L 2 . Then L 1 ∪ L 2 is T 1 ∪ T 2 -satisfiable if and only if there exist an arrangement A for S and P, and a T i -model M i of A ∪ L i with the same P-cardinality for i = 1, 2.

The spectrum of a theory T is the set of P-cardinalities of its models. The above theorem can thus be restated as:

Corollary 1. The T 1 ∪T 2 -satisfiability problem for sets of literals is decidable if, for any sets of literals A∪L 1 and A∪L 2 it is possible to decide if the intersection of the spectrums of

T 1 ∪ A ∪ L 1 and of T 2 ∪ A ∪ L 2 is non-empty.
To characterize the spectrum of the decidable classes considered in this paper, we introduce the notion of cardinality constraint. A finite cardinality constraint is simply a P-cardinality with only finite cardinalities. An infinite cardinality constraint is given by a P-cardinality κ with only finite cardinalities and a nonempty set of Venn regions V , and stands for all the P-cardinalities κ such that κ v ≥ κ v if v ∈ V , and κ v = κ v otherwise. The spectrum of a finite set of cardinality constraints is the union of all P-cardinalities represented by each cardinality constraint. It is now easy to define the class of theories we are interested in: Definition 2. A theory T is P-gentle if, for every set L of literals in the language of T , the spectrum of T ∪ L is the spectrum of a computable finite set of cardinality constraints.

Notice that a P-gentle theory is (by definition) decidable. To relate the above notion with the gentleness in the disjoint case [9], observe that if p is a unary predicate symbol not occurring in the signature of the theory T , then T ∪ {∀x.p(x)} is {p}-gentle if and only if T is gentle.

If a theory is P-gentle, then it is P -gentle for any non-empty subset P of P. It is thus interesting to have P-gentleness for the largest possible P. Hence, when P is not explicitly given for a theory, we assume that P denotes the set of unary predicates symbols occurring in its signature. In the following sections we show that the Löwenheim theories and the BSR theories are P-gentle.

The union of two P-gentle theories is decidable, as a corollary of the following modularity result: Theorem 2. The class of P-gentle theories is closed under P-union.

Proof. If we consider the P-union of two P-gentle theories with respective spectrums S 1 and S 2 , then we can build some finite set of cardinality constraints whose spectrum is S 1 ∩ S 2 . Some very useful theories are not P-gentle, but in practical cases they can be combined with P-gentle theories. To define more precisely the class of theories T that can be combined with a P-gentle one, let us introduce the T -satisfiability problem with cardinality constraints: given a formula and a finite set of cardinality constraints, the problem amounts to check whether the formula is satisfiable in a model of T whose P-cardinality is in the spectrum of the cardinality constraints. As a direct consequence of Corollary 1: Theorem 3. T ∪ T -satisfiability is decidable if the theory T is P-gentle and T -satisfiability with cardinality constraints is decidable.

Notice that T -satisfiability with cardinality constraints is decidable for most common theories, e.g. the theories handled in SMT solvers. This gives the theoretical ground to add to the SMT solvers any number of P-gentle theories sharing unary predicates.

From the results in the rest of the paper, it will also follow that the nondisjoint union (sharing unary predicates) of BSR and Löwenheim theories with one decidable theory accepting further constraints of the form ∀x . ((¬)p 1 (x) ∧ . . . (¬)p n (x)) ⇒ (x = a 1 ∨ . . . x = a m ) is decidable. For instance, the guarded fragment with equality accepts such further constraints and the superposition calculus provides a decision procedure [11]. Thus any theory in the guarded fragment can be combined with Löwenheim and BSR theories sharing unary predicates.

In the disjoint case, any decidable theory expressed as a finite set of firstorder axioms can be combined with a gentle theory [9]. Here this is not the case anymore. Indeed, consider the theory ψ = ϕ ∨ ∃x p(x) where p does not occur in ϕ; any set of literals is satisfiable in the theory ψ if and only if it is satisfiable in the theory of equality. If the satisfiability problem of literals in the theory ϕ is undecidable, the P-union of ψ and the Löwenheim theory ∀x ¬p(x) will also be undecidable.

The Löwenheim Class

We first review some classical results about this class and refer to [6] for more details. A Löwenheim theory is a finite set of closed formulas in a relational language containing only unary predicates (and no functions except constants). This class is also known as first-order relational monadic logic. Usually one distinguishes the Löwenheim class with and without equality. The Löwenheim class has the finite model property (and is thus decidable) even with equality. Full monadic logic without equality, i.e. the class of finite theories over a language containing symbols (predicates and functions) of arity at most 1, also has the finite model property. Considering monadic logic with equality, the class of finite theories over a language containing only unary predicates and just two unary functions is already undecidable. With only one unary function, however, the class remains decidable [6], but does not have the finite model property anymore. Since the spectrum for this last class is significantly more complicated [13] than for the Löwenheim class we will here only focus on the Löwenheim class with equality (only classes with equality are relevant in our context), that is, without functions. More can be found about monadic first-order logic in [6,8].

In particular, a weaker version of Corollary 2 (given below) can be found in [8].

Previously [9,1], combining theories with non-stably infinite theories took advantage of "pumping" lemmas, allowing -for many decidable fragmentsto build models of arbitrary large cardinalities. The following theorem is such a pumping lemma, but it considers the cardinalities of the Venn regions and not only the global cardinality. Lemma 1. Assume T is a Löwenheim theory with equality. Let q be the number of variables in T . If there exists a model M on domain D with |D v \ D c | ≥ q, then, for each cardinality q ≥ q, there is a model extension or restriction M of M on domain

D such that |D v \ D c | = q and D v = D v for all v = v.
Proof. Two interpretations I (on domain D) and I (on domain D ) for a formula ψ are similar if

-|(D v ∩ D v ) \ D c | ≥ q; -D v = D v for each Venn region v distinct from v; -I[a] = I [a] for each constant in ψ; -I[x] = I [x]
for each variable free in ψ.

Considering M as above, we can build a model M as stated in the theorem, such that M and M are similar. Indeed similarity perfectly defines a model with respect to another, given the cardinalities of the Venn regions.

We now prove that, given a Löwenheim formula ψ (or a set of formulas), two similar interpretations for ψ give the same truth value to ψ and to each sub-formula of ψ.

The proof is by induction on the structure of the (sub-)formula ψ. It is obvious if ψ is atomic, since similar interpretations assign the same value to variables and constants. If ψ is ¬ϕ 1 , ϕ 1 ∨ ϕ 2 , ϕ 1 ∧ ϕ 2 or ϕ 1 ⇒ ϕ 2 , the result holds if it also holds for ϕ 1 and ϕ 2 .

Assume I makes true the formula ψ = ∃x ϕ(x). Then there exists some d ∈ D such that I x/d is a model of ϕ(x). If d ∈ D , then I x/d is similar to I x/d and, by the induction hypothesis, it is a model of ϕ(x); I is thus a model of ψ.

If d / ∈ D , then d ∈ D v and |(D v ∩ D v ) \ D c | ≥ q.
Furthermore, since the whole formula contains at most q variables, ϕ(x) contains at most q -1 free variables besides x. Let x 1 , . . . , x m be those variables. There exists some d

∈ (D v ∩ D v ) \ D c such that d = I[x i ]
for all i ∈ {1, . . . , m}. By structural induction, it is easy to show that I x/d and I x/d give the same truth value to ϕ(x). Furthermore I x/d and I x/d are similar. I is thus a model of ψ. To summarize, if I is a model of ψ, I is also a model of ψ. By symmetry, if I is a model of ψ, I is also a model of ψ. The proof for formulas of the form ∀x ϕ(x) is dual.

Lemma 1 has the following consequence on the acceptable cardinalities for the models of a Löwenheim theory: Corollary 2. Assume T is a Löwenheim theory with equality with n distinct unary predicates. Let r and q be respectively the number of constants and variables in T . If T has a model of some cardinality κ strictly larger than r + 2 n max(0, q -1), then T has models of each cardinality equal or larger than min(κ, r + q 2 n ).

Proof. If a model with such a cardinality exists, then there are Venn regions v such that |D v \ D c | ≥ q. Then the number of elements in these Venn regions can be increased to any arbitrary larger cardinality, thanks to Lemma 1. If κ > r + q 2 n , it means some Venn regions v are such that |D v \ D c | > q, and by eliminating elements in such Venn regions (using again Lemma 1), it is possible to obtain a model of cardinality r + q 2 n .

In [8], the limit is q 2 n , q being the number of constants plus the maximum number of nested quantifiers. Now q is more precisely set to the number of variables, and the constants are counted separately. Moreover, max(0, q -1) replaces the factor q.

The case where q and r are both 0 corresponds to pure propositional logic (Löwenheim theories without variables and constants), where the size of the domain is not relevant. With q = 1 (one variable), there is no way to compare two elements (besides the ones associated to constants) and enforce them to be equal. It is still possible to constrain the domain to be of size at most r, using constraints like ∀x . x = c 1 ∨ . . . ∨ x = c r , but any model with one element not associated to a constant can be extended to a model of arbitrary cardinality (by somehow duplicating any number of time this element). Notice also that it is possible to set a lower bound on the size of the domain that can be r + 2 n . Consider for instance a set of sentences of the form ∃x.(¬)p 1 (x) ∨ . . . (¬)p n (x); there are 2 n such formulas, each enforcing one Venn region to be non-empty.

Using several variables, a Löwenheim formula can enforce upper bounds larger than r on cardinalities. For q = 2, it is indeed easy to build a formula that has only models of cardinality at most (q -1) 2 n = 2 n : ∀x∀y .

0<i<j≤n p i (x) = p j (y) ⇒ x = y.
With a larger number of variables, the following formula (q ≥ 2)

∀x 1 . . . ∀x q . 0<i<j≤n 0<i <j ≤q p i (x i ) = p j (x j ) ⇒ 0<i <j ≤q x i = x j
enforces the cardinality of the domain to be at most (q -1) 2 n . To obtain a formula with constants that accepts only models of cardinality up to r + 2 n max(0, q -1), it suffices to add as a guard in the above formula the conjunctive sets of atoms expressing that the variables are disjoint from the r constants. So the above condition in Corollary 2 is the strongest one.

Besides the finite model property and the decidability of Löwenheim theories, Corollary 2 also directly entails the P-gentleness: Theorem 4. Löwenheim theories on a language with unary predicates in P are P-gentle.

The Bernays-Schönfinkel-Ramsey Class

A Bernays-Schönfinkel-Ramsey (BSR for short) theory is a finite set of formulas of the form ∃ * ∀ * ϕ, where ϕ is a first-order formula which is function-free (but constants are allowed) and quantifier-free. Bernays and Schönfinkel first proved the decidability of this class without equality; Ramsey later proved that it remains decidable with equality. More can be found about BSR theories in [6]. Ramsey also gave some (less known) results about the spectrum of BSR theories [18]. We here give a proof that BSR theories are P-gentle.

For simplicity, we will assume that existential quantifiers are Skolemized. In the following, a BSR theory is thus a finite set of universal function-free closed first-order formulas. Intuitively, this states that the elements not assigned to ground terms (i.e. the constants) can be eliminated from a model of a BSR theory. It is known [18,9] that for any BSR theory T there is a computable finite number k such that if T has a model of cardinality greater or equal to k, then it has a model of any cardinality larger than k. Later in this section, we prove that the same occurs locally for each Venn region.

The notion of n-repetitive models, which we now define, is instrumental for this. Informally, a model is n-repetitive if it is symmetric for those elements of its domain that are not assigned to constants in the theory. Notice that a same interpretation can be n-repetitive for several Venn regions at the same time. Also, the above definition allows D v \ D c to be empty for every v / ∈ V . Previously [9] (without distinguishing regions) we showed that one can decide if a BSR theory T is n-repetitive by building another BSR theory that is satisfiable if and only if T is n-repetitive. The same occurs to n-repetitiveness for Venn regions.

c | ≤ n • d i = d i if d i or d i ∈ D c ∪ v / ∈V D v • v(d i ) = v(d i ) • d i ≺ d j iff d i ≺ d j , if for some v ∈ V , d i , d j ∈ D v \ D c
Theorem 5. Consider a BSR theory T with n variables and a model M on domain D. If M is n-repetitive for the Venn regions V then, for any (finite or infinite) cardinalities

κ v ≥ |D v | (v ∈ V ), T has a model M extension of M on domain D such that |D v | = κ v if v ∈ V and D v = D v for all v / ∈ V .
Proof. Assume that ≺ are the total orders mentioned in Definition 3. We first build an extension M of M as specified in the theorem, and later prove it is a model of T . Let E be the set of new elements E = D \ D, and fix arbitrary total orders (again denoted by ≺) on D v \D c for all v ∈ V that extend the given orders on D v \ D c . Since M is an extension of M, the interpretation of the predicate symbols is already defined when all arguments belong to D. When some arguments belong to E, the truth value of an r-ary predicate p is defined as follows: Now it is possible to state that the full spectrum of a BSR theory only depends on (a finite set of) P-cardinalities κ such that, for all Venn region v, κ v ≤ k for some finite cardinality k only depending on the theory. The proof requires an extension of Ramsey's Theorem which can be found in the appendix A. Theorem 6. Given a BSR theory T with n variables, there exists a number k computable from the theory, such that, if T has a model M on domain D such that |D v \ D c | ≥ k for Venn regions v ∈ V , then it has a model which is n-repetitive for Venn regions V .

-(d 1 , . . . , d r ) ∈ M [p]
Proof. Using Lemma 2, we can assume that T has a (sufficiently large) finite model M on domain D. We can assume without loss of generality that M is such that, for every predicate p of the language, (d 1 , . . . d r ) / ∈ M[p] whenever there are more than n elements in {d 1 , . . . d r } \ D c ; indeed, these interpretations play no role in the truth value of a formula with n variables.

Let ≺ be an order on D\D c . Given two ordered (with respect to ≺) sequences e 1 , . . . , e n and e 1 , . . . , e n of elements in D\D c such that v(e i ) = v(e i ) (1 ≤ i ≤ n), we say that the configurations for e 1 , . . . , e n and e 1 , . . . , e n agree if for every rary predicate p, and for every d The BSR class obviously has the finite model property, and is decidable. Lemma 2 and Theorems 5 and 6 above also prove that BSR theories are (gentle and) P-gentle: Corollary 3. BSR theories on a language including unary predicates in P are P-gentle.

A simple constructive proof of this corollary would consider the finite number of all P-cardinalities κ such that κ v ≤ k (where k comes from Theorem 6). All such P-cardinalities can be understood as cardinality constraints, the extendable Venn regions being the ones for which κ v > k. Of course this construction is highly impractical, since it uses some kind of Ramsey numbers, known to be extremely large. In practice, we believe there are much better constructions: the important elements of the domain are basically only the ones associated to constants, and theoretical upper bounds are not met in non-artificial cases.

Example: Non-Disjoint Combination of Order and Sets

To illustrate the kind of theories that can be handled in our framework, consider a simple yet informative example with a BSR theory defining an ordering < and augmented with clauses connecting the ordering < and the sets p and q (we do not distinguish sets and their related predicates):

T 1 =        ∀x. ¬(x < x) ∀x, y, z. (x < y ∧ y < z) ⇒ x < z
∀x, y. (p(x) ∧ ¬p(y)) ⇒ x < y ∀x, y. (q(x) ∧ ¬q(y)) ⇒ x < y and a Löwenheim theory

T 2 = ∃y∀x. (p(x) ∧ q(x)) ≡ x = y ∀x∃y. p(x) ⇒ (x = y ∧ q(y))
Notice that T 2 is not a BSR theory due to the ∀∃ quantification of its second axiom, but both theories T 1 and T 2 are actually P-gentle. The theory T 1 imposes either p ∩ q or p ∩ q to be empty (we will assume that the domain is non-empty and simplify the cardinality constraints accordingly). The theory T 2 imposes the cardinality of p ∩ q to be exactly 1, and the cardinality of p ∩ q to be at least 1. The following table collects the cardinality constraints:

T 1 T 2 p ∩ q ≥ 0 ≥ 0 ≥ 0 p ∩ q 0 ≥ 0 ≥ 1 p ∩ q ≥ 0 0 ≥ 0 p ∩ q ≥ 0 ≥ 0 1
The theory T 1 ∪T 2 imposes p∩q to be empty, in other words p ⊆ q. Moreover, the cardinality of p ∩ q is 1, and so it implies that the cardinality of p is 1. Hence, the set T 1 ∪ T 2 ∪ {p(a), p(b), a = b} is unsatisfiable. As a final comment, there could be theories using directly the Venn cardinalities as integer variables. For instance, imagine a constraint stating |p| > 1 in a theory including linear arithmetic on integers. This would of course be unsatisfiable with T 1 ∪ T 2 .

Conclusion

The notion of gentleness was initially presented as a tool to combine non-stably infinite disjoint theories. In this paper, we have introduced a notion of Pgentleness which is well-suited for combining theories sharing (besides constants and the equality) only unary predicates in a set P. The major contributions of this paper are that the Löwenheim theories and BSR theories are P-gentle. A corollary is that the non-disjoint union (sharing unary predicates) of Löwenheim theories, BSR theories, and decidable theories accepting further constraints of the form ∀x . ((¬)p 1 (x) ∧ . . . (¬)p n (x)) ⇒ (x = a 1 ∨ . . . x = a m ) is decidable.

Our combination method is limited to shared unary predicates. Unfortunately, the theoretical limitations are strong for a framework sharing predicates with larger arities: for instance even the guarded fragment with two variables and transitivity constraints is undecidable [10], although the guarded fragment (or first-order logic with two variables) is decidable, and transitivity constraints can be expressed in BSR. The problem of combining theories with only a shared dense order has however been successfully solved [12,14]. In that specific case, there is again an implicit infiniteness argument that could be possibly expressed as a form of extended gentleness, to reduce the isomorphism construction problem into solving some appropriate extension of cardinality constraints. A clearly challenging problem is to identify an appropriate extended notion of gentleness for some particular binary predicates.

Also in future works, the reduction approach (Löwenheim and BSR theories can be simplified to a subset of Löwenheim) may be useful as a simplification procedure for sets of formulas that can be seen as non-disjoint (sharing unary predicates only) combinations of BSR, Löwenheim theories and an arbitrary first-order theory: this would of course not provide a decision procedure, but refutational completeness can be preserved. More generally we also plan to study how superposition-based satisfiability procedures could benefit from a non-disjoint (sharing unary predicates) combination point of view. In particular, superposition-based satisfiability procedures could be used as deductive engines with the capability to exchange constraints à la Nelson-Oppen.

The results here are certainly too combinatorially expensive to be directly applicable. However, this paper paves the theoretical grounds for mandatory further works that would make such combinations practical. There are important incentives since the BSR and Löwenheim fragments are quite expressive: for instance, it is possible to extend the language of SMT solvers with sets and cardinalities. Many formal methods are based on logic languages with sets. Expressive decision procedures (even if they are not efficient) including e.g. sets and cardinalities will help proving the often small but many verification conditions stemming from these applications.

Introduction

While the benefit of symmetries has been recognized for the satisfiability problem of propositional logic [15], for constraint programming [9], and for finite model finding [4,7,11], SMT solvers (see [3] for a detailed account of techniques used in SMT solvers) do not yet fully exploit symmetries. Audemard et al. [1] use symmetries as a simplification technique for SMT-based model-checking, and the SMT solver HTP [14] uses some symmetry-based heuristics, but current state-of-the-art solvers do not exploit symmetries to decrease the size of the search space.

In the context of SMT solving, a frequent source of symmetries is when some terms take their value in a given finite set of totally symmetric elements. The idea here is very simple: given a formula G invariant by all permutations of some uninterpreted constants c 0 , . . . , c n , for any model M of G, if term t does not contain these constants and M satisfies t = c i for some i, then there should be a model in which t equals c 0 . While checking for unsatisfiability, it is thus sufficient to look for models assigning t and c 0 to the same value. This simple idea is very effective, especially for formulas generated by finite instantiations of quantified problems. We have implemented our technique in a moderately efficient SMT solver (veriT [5]), and with this addition it outperforms the winners of recent editions of the SMT-COMP [2] contest in the QF UF category. This indicates that detecting symmetries, automatically or based on hints in the input, can be important for provers to reduce the search space that they have to consider, just as some constraint solvers already take symmetry information into account.

Outline. We first introduce notations, then define symmetries and give the main theorem that allows us to reduce the search space. We recast an algorithm to exploit such symmetries in the context of SMT-solvers. Next, the classical pigeonhole problem is analyzed from the perspective of symmetries. Finally, some experimental results, based on the SMT-LIB, are provided and discussed.

Notations

A many-sorted first-order language is a tuple L = S, V, F, P, d such that S is a countable non-empty set of disjoint sorts (or types), V is the (countable) union of disjoint countable sets V τ of variables of sort τ , F is a countably infinite set of function symbols, P is a countably infinite set of predicate symbols, and d assigns a sort in S + to each function symbol f ∈ F and a sort in S * to each predicate symbol p ∈ P. Nullary predicates are propositions, and nullary functions are constants. The set of predicate symbols is assumed to contain a binary predicate = τ for every sort τ ∈ S; since the sort of the equality can be deduced from the sort of the arguments, the symbol = will be used for equality of all sorts. Terms and formulas over the language L are defined in the usual way.

An interpretation for a first-order language L is a pair I = D, I where D assigns a non-empty domain D τ to each sort τ ∈ S and I assigns a meaning to each variable, function, and predicate symbol. As usual, the identity is assigned to the equality symbol. By extension, an interpretation I defines a value I[t] in D τ for every term t of sort τ , and a truth value I[ϕ] in { , ⊥} for every formula ϕ. A model of a formula ϕ is an interpretation I such that I[ϕ] = . The notation I s1/r1,...,sn/rn stands for the interpretation that agrees with I, except that it associates the elements r i of appropriate sort to the symbols s i .

For convenience, we will consider that a theory is a set of interpretations for a given many-sorted language. The theory corresponding to a set of first-order axioms is thus naturally the set of models of the axioms. A theory may leave some predicates and functions uninterpreted: a predicate symbol p (or a function symbol f ) is uninterpreted in a theory T if for every interpretation I in T and for every predicate q (resp., function g) of suitable sort, I p/q belongs to T (resp., I f /g ∈ T ). It is assumed that variables are always uninterpreted in any theory, with a meaning similar to uninterpreted constants. Given a theory T , a formula ϕ is T -satisfiable if it has a model in T . Two formulas are T -equisatisfiable if one formula is T -satisfiable if and only if the other is. A formula ϕ is a logical consequence of a theory T (noted T |= ϕ) if every interpretation in T is a model of ϕ. A formula ϕ is a T -logical consequence of a formula ψ, if every model M ∈ T of ψ is also a model of ϕ; this is noted ψ |= T ϕ. Two formulas ψ and ϕ are T -logically equivalent if they have the same models in T .

Defining symmetries

We now formally introduce the concept of formulas invariant w.r.t. permutations of uninterpreted symbols and study the T -satisfiability problem of such formulas. Intuitively, the formula ϕ is invariant w.r.t. permutations of uninterpreted symbols if, modulo some syntactic normalization, it is left unchanged when the symbols are permuted. Formally, the notion of permutation operators depends on the theory T for which T -satisfiability is considered, because only uninterpreted symbols may be permuted. Definition 1. A permutation operator P on a set R ⊆ F ∪ P of uninterpreted symbols of a language L = S, V, F, P, d is a sort-preserving bijective map from R to R, that is, for each symbol s ∈ R, the sorts of s and P [s] are equal. A permutation operator homomorphically extends to an operator on terms and formulas on the language L.

As an example, a permutation operator on a language containing the three constants c 0 , c 1 , c 2 of identical sort, may map c 0 to c 1 , c 1 to c 2 and c 2 to c 0 .

To formally define that a formula is invariant by a permutation operator modulo some rewriting, the concept of T -preserving rewriting operator is introduced. The last condition of Def. 2 will be useful in Lemma 6. Notice that R must be idempotent, since R • P • R and P • R should be equal for all permutation operators, including the identity permutation operator.

To better motivate the notion of a T -preserving rewriting operator, consider a formula containing a clause t = c 0 ∨ t = c 1 . Obviously this clause is symmetric if t does not contain the constants c 0 and c 1 . However, a permutation operator on the constants c 0 and c 1 would rewrite the formula into t = c 1 ∨ t = c 0 , which is not syntactically equal to the original one. Assuming the existence of some ordering on terms and formulas, a typical T -preserving rewriting operator would reorder arguments of all commutative symbols according to this ordering. With appropriate data structures to represent terms and formulas, it is possible to build an implementation of this T -preserving rewriting operator that runs in linear time with respect to the size of the DAG or tree that represents the formula.

Definition 3. Given a T -preserving rewriting operator R, a permutation operator P on a language L is a symmetry operator of a formula ϕ (a term t) on the language L w.r.

t. R if R[P [ϕ]] and R[ϕ] (resp., R[P [t]] and R[t]) are identical.
Notice that, given a permutation operator P and a linear time T -preserving rewriting operator R satisfying the condition of Def. 3, it is again possible to check in linear time if P is a symmetry operator of a formula w.r.t. R. In the following, we will assume a fixed rewriting operator R and say that P is a symmetry operator if it is a symmetry operator w.r.t. R.

Symmetries could alternatively be defined semantically, stating that a permutation operator P is a symmetry operator if P [ϕ] is T -logically equivalent to ϕ. The above syntactical symmetry implies of course the semantical symmetry. But the problem of checking if a permutation operator is a semantical symmetry operator has the same complexity as the problem of unsatisfiability checking. Indeed, consider the permutation P such that P [c 0 ] = c 1 and P [c 1 ] = c 0 , and a formula ψ defined as c = c 0 ∧ c = c 1 ∧ ψ (where c, c 0 and c 1 do not occur in ψ ).

To check if the permutation operator P is a semantical symmetry operator of ψ, it is necessary to check if formulas ψ and P [ψ] are logically equivalent, which is only the case if ψ is unsatisfiable. Definition 4. A term t (a formula ϕ) is invariant w.r.t. permutations of uninterpreted constants c 0 , . . . , c n if any permutation operator P on c 0 , . . . , c n is a symmetry operator of t (resp. ϕ).

The main theorem follows: it allows one to introduce a symmetry breaking assumption in a formula that is invariant w.r.t. permutations of constants. This assumption will decrease the size of the search space.

Theorem 5. Consider a theory T , uninterpreted constants c 0 , . . . , c n , a formula ϕ that is invariant w.r.t. permutations of c i , . . . , c n , and a term t that is invariant w.r.t. permutations of c i , . . . , c n . If

ϕ |= T t = c 0 ∨ . . . ∨ t = c n , then ϕ is T - satisfiable if and only if ϕ = def ϕ ∧ (t = c 0 ∨ . . . ∨ t = c i )
is also T -satisfiable. Clearly, ϕ is invariant w.r.t. permutations of c i+1 , . . . , c n .

Proof : Let us first prove the theorem for i = 0.

Assume that ϕ ∧ t = c 0 is T -satisfiable, and that M ∈ T is a model of ϕ ∧ t = c 0 ; M is also a model of ϕ, and thus ϕ is T -satisfiable.

Assume now that ϕ is T -satisfiable, and that M ∈ T is a model of ϕ. By assumption there exists some j ∈ {0, . . . , n} such that M |= t = c j , hence M |= ϕ ∧ t = c j . In the case where j = 0, M is also a model of ϕ ∧ t = c 0 . If j = 0, consider the permutation operator P that swaps c 0 and c j . Notice (this can be proved by structural induction on formulas) that, for any formula

. , c n ), ϕ is T -equisatisfiable to ϕ ∧ ¬(t = c 0 ∨ . . . ∨ t = c i-1 ) ∧ t = c i . Formulas ϕ and ϕ ∧ ¬(t = c 0 ∨ . . . ∨ t = c i-1 ) ∨ ϕ ∧ (t = c 0 ∨ . . . ∨ t = c i-1 )
are T -logically equivalent. Since A∨B and A ∨B are T -equisatisfiable whenever

A and A are T -equisatisfiable, ϕ is T -equisatisfiable to ϕ ∧ ¬(t = c 0 ∨ . . . ∨ t = c i-1 ) ∧ t = c i ∨ ϕ ∧ (t = c 0 ∨ . . . ∨ t = c i-1 ) . This last formula is T -logically equivalent to ϕ ∧ (t = c 0 ∨ . . . ∨ t = c i-1 ∨ t = c i )
and thus the theorem holds.

Checking if a permutation is syntactically equal to the original term or formula can be done in linear time. And checking if a formula is invariant w.r.t. permutations of given constants is also linear: only two permutations have to be considered instead of the n! possible permutations. Proof : First notice that any permutation operator on c 0 , . . . , c n can be written as a product of P circ and P swap , because the group of permutations of c 0 , . . . , c n is generated by the circular permutation and the swapping of c 0 and c 1 . Any permutation P of c 0 , . . . , c n can then be rewritten as a product P 1 •• • ••P m , where P i ∈ {P circ , P swap } for i ∈ {1, . . . , m}. It remains to prove that any permutation operator P 1 • • • • • P m is indeed a symmetry operator. This is done inductively. For m = 1 this is trivially true. For the inductive case, assume

P 1 • • • • • P m-1 is a symmetry operator of ϕ, then R[(P 1 • . . . • P m )[ϕ]] ≡ R[P m [(P 1 • • • • • P m-1 )[ϕ]]] ≡ R[P m [R[(P 1 • • • • • P m-1 )[ϕ]]]] ≡ R[P m [ϕ]] ≡ R[ϕ]
P := guess permutations(ϕ); where ≡ stands for syntactical equality. The first equality simply expands the definition of the composition operator •, the second comes from the definition of the T -preserving rewriting operator R, the third uses the inductive hypothesis, and the last uses the fact that P m is either P circ or P swap , that is, also a symmetry operator of ϕ.

SMT with symmetries: an algorithm

Algorithm 1 applies Theorem 5 in order to exhaustively add symmetry breaking assumptions on formulas. First, a set of sets of constants is guessed (line 1) from the formula ϕ by the function guess permutations; each such set of constants {c 0 , . . . , c n } will be successively considered (line 2), and invariance of ϕ w.r.t. permutations of {c 0 , . . . , c n } will be checked (line 3). Notice that function guess permutations(ϕ) gives an approximate solution to the problem of partitioning constants of ϕ into classes {c 0 , . . . , c n } of constants such that ϕ is invariant by permutations. If the T -preserving rewriting operator R is given, then this is a decidable problem. However we have a feeling that, while the problem is still polynomial (it suffices to check all permutations with pairs of constants), only providing an approximate solution is tractable. Function guess permutations should be such that a small number of tentative sets are returned. Every tentative set will be checked in function invariant by permutations (line 3); with appropriate data structures the test is linear with respect to the size of ϕ (as a corollary of Lemma 6).

As a concrete implementation of function guess permutations(ϕ), partitioning the constants in classes that all give the same values to some functions f (ϕ, c) works well in practice, where the functions f compute syntactic information that is unaffected by permutations, i.e. f (ϕ, c) and f (P [ϕ], P [c]) should yield the same results. Obvious examples of such functions are the number of appearances of c in ϕ, or the maximal depth of c within an atom of ϕ, etc. The classes of constants could also take into account the fact that, if ϕ is a large conjunction, with c 0 = c 1 as a conjunct (c 0 and c 1 in the same class), then it should have c i = c j or c j = c i as a conjunct for every pair of different constants c i , c j contained in the class of c 0 and c 1 . In veriT we use a straightforward detection of clusters c 0 , . . . , c n of constants such that there exists an inequality c i = c j for every i = j as a conjunct in the original formula ϕ.

Line 3 checks the invariance of formula ϕ by permutation of c 0 , . . . , c n . In veriT, function invariant by permutations(ϕ, {c 0 , . . . , c n }) simply builds, in linear time, the result of applying a circular permutation of c 0 , . . . , c n to ϕ, and the result of applying a permutation swapping two constants (for instance c 0 and c 1 ). Both obtained formulas, as well as the original one, are normalized by a rewriting operator sorting arguments of conjunctions, disjunctions, and equality according to an arbitrary term ordering. The three formulas should be syntactically equal (this is tested in constant time thanks to the maximal sharing of terms in veriT) for invariant by permutations(ϕ, {c 0 , . . . , c n }) to return true.

Lines 4 to 15 concentrate on breaking the symmetry of {c 0 , . . . , c n }. First a set of terms

T ⊆ t | ϕ |= t = c 0 ∨ . . . ∨ t = c n }
is computed. Again, function select terms(ϕ, {c 0 , . . . , c n }) returns an approximate solution to the problem of getting all terms t such that t = c 0 ∨ . . . ∨ t = c n ; an omission in T would simply restrict the choices for a good candidate on line 7, but would not jeopardize soundness. Again, this is implemented in a straightforward way in veriT.

The loop on lines 6 to 15 introduces a symmetry breaking assumption on every iteration (except perhaps on the last iteration, where a subsumed assumption would be omitted). A candidate symmetry-breaking term t ∈ T is chosen by the call select most promising term(T, ϕ). The efficiency of the SMT solver is very sensitive to this selection function. If the term t is not important for unsatisfiability, then the assumption would simply be useless. In veriT, the selected term is the most frequent constant-free term (i.e. the one with the highest number of clauses in which it appears), or, if no constant-free terms remains, the one with the largest ratio of the number of clauses in which the term appears over the number of constants that will be required to add to cts on line 11; so actually, select most promising term also depends on the set cts.

Function used in(t, {c 0 , . . . , c n }) returns the set of constants in term t. If the term contains constants in {c 0 , . . . , c n } \ cts, then only the remaining constants can be used. On line 10, one of the remaining constants c is chosen nondeterministically: in principle, any of these constants is suitable, but the choice may take into account accidental features that influence the decision heuristics of the SMT solver, such as term orderings.

Finally, if the symmetry breaking assumption ci∈cts t = c i is not subsumed (i.e. if cts = {c 0 , . . . , c n }), then it is conjoined to the original formula.

Theorem 7. The formula ϕ obtained after running Algorithm 1 is T -satisfiable if and only if the original formula ϕ 0 is T -satisfiable.

Proof : If the obtained ϕ is T -satisfiable then ϕ 0 is T -satisfiable since ϕ is a conjunction of ϕ 0 and other formulas (the symmetry breaking assumptions).

Assume that ϕ 0 is T -satisfiable, then ϕ is T -satisfiable, as a direct consequence of Theorem 5. In more details, in lines 6 to 15, ϕ is always invariant by permutation of constants {c 0 , . . . , c n } \ cts, and more strongly, on line 13, ϕ is invariant by permutations of constants in cts as defined in line 9. In lines 4 to 15 any term t ∈ T is such that ϕ |= T t = c 0 ∨ . . . ∨ t = c n . On lines 10 to 14, t is invariant with respect to permutations of constants in cts as defined in line 9. The symmetry breaking assumption conjoined to ϕ in line 13 is, up to the renaming of constants, the symmetry breaking assumption of Theorem 5 and all conditions of applicability of this theorem are fulfilled.

SMT with symmetries: an example

A classical problem with symmetries is the pigeonhole problem. Most SMT or SAT solvers require exponential time to solve this problem; these solvers are strongly linked with the resolution calculus, and an exponential lower bound for the length of resolution proofs of the pigeon-hole principle was proved in [10]. Polynomial-length proofs are possible in stronger proof systems, as shown by Buss [6] for Frege proof systems. An extensive survey on the proof complexity of pigeonhole principles can be found in [13]. Polynomial-length proofs are also possible if the resolution calculus is extended with symmetry rules (as in [12] and in [17]).

We here recast the pigeonhole problem in the SMT language and show that the preprocessing introduced previously transforms the series of problems solved in exponential time with standard SMT solvers into a series of problems solved in polynomial time. This toy problem states that it is impossible to place n + 1 pigeons in n holes. We introduce n uninterpreted constants h 1 , . . . , h n for the n holes, and n + 1 uninterpreted constants p 1 , . . . , p n+1 for the n + 1 pigeons. Each pigeon is required to occupy one hole:

p i = h 1 ∨ . . . ∨ p i = h n
It is also required that distinct pigeons occupy different holes, and this is expressed by the clauses p i = p j for 1 ≤ i < j ≤ n + 1. One can also assume that the holes are distinct, i.e., h i = h j for 1 ≤ i < j ≤ n, although this is not needed for the problem to be unsatisfiable. The generated set of formulas is invariant by permutations of the constants p 1 , . . . , p n+1 , and also by permutations of constants h 1 , . . . , h n ; very basic heuristics would easily guess this invariance. However, it is not obvious from the presentation of the problem that h

i = p 1 ∨ . . . ∨ h i = p n+1 for i ∈ [1.
.n], so any standard function select terms in the previous algorithm will fail to return any selectable term to break the symmetry; this symmetry of p 1 , . . . , p n+1 is not directly usable. It is however most direct to notice that p i = h 1 ∨ . . . ∨ p i = h n ; select terms in the previous algorithm would return the set of {p 1 , . . . , p n+1 }. The set of symmetry breaking clauses could be

p 1 = h 1 p 2 = h 1 ∨ p 2 = h 2 p 3 = h 1 ∨ p 3 = h 2 ∨ p 3 = h 3 . . . p n-1 = h 1 ∨ . . . ∨ p n-1 = h n-1
or any similar set of clauses obtained from these with by applying a permutation operator on p 1 , . . . , p n+1 and a permutation operator on h 1 , . . . , h n . Without need for any advanced theory propagation techniques4 , (n + 1) × n/2 conflict clauses of the form p i = h i ∨ p j = h i ∨ p j = p i with i < j suffice to transform the problem into a purely propositional problem. With the symmetry breaking clauses, the underlying SAT solver then concludes (in polynomial time) the unsatisfiability of the problem using only Boolean Constraint Propagation. Without the symmetry breaking clauses, the SAT solver will have to investigate all n! assignments of n pigeons in n holes, and conclude for each of those assignments that the pigeon n + 1 cannot find any unoccupied hole.

The experimental results, shown in Figure 1, support this analysis: all solvers (including veriT without symmetry heuristics) time out5 on problems of relatively small size, although CVC3 performs significantly better than the other solvers. Using the symmetry heuristics allows veriT to solve much larger problems in insignificant times. In fact, the modified version of veriT solves every instance of the problem with as many as 30 pigeons in less than 0.15 seconds.

Experimental results

In the previous section we showed that detecting and breaking symmetries can sometimes decrease the solving time from exponential to polynomial. We now investigate its use on more realistic problems by evaluating its impact on SMT-LIB benchmarks.

Consider a problem on a finite domain of a given cardinality n, with a set of arbitrarily quantified formulas specifying the properties for the elements of this domain. A trivial way to encode this problem into quantifier-free first-order logic, is to introduce n constants {c 1 , . . . , c n }, add constraints c i = c j for 1 ≤ i < j ≤ n, Skolemize the axioms and recursively replace in the Skolemized formulas the remaining quantifiers Qx.ϕ(x) by conjunctions (if Q is ∀) or disjunctions (if Q is ∃) of all formulas ϕ(c i ) (with 1 ≤ i ≤ n). All terms should also be such that t = c 1 ∨ . . . ∨ t = c n . The set of formulas obtained in this way is naturally invariant w.r.t. permutations of c 1 , . . . , c n . So the problem in its most natural encoding contains symmetries that should be exploited in order to decrease the size of the search space. The QF UF category of the SMT library of benchmarks actually contains many problems of this kind.

Figure 2 presents a scatter plot of the running time of veriT on each formula in the QF UF category. The x axis gives the running times of veriT without the symmetry breaking technique presented in this paper, whereas the times reported on the y axis are the running times of full veriT. It clearly shows a global improvement; this improvement is even more striking when one restricts the comparison to unsatisfiable instances (see Figure 3); no significant trend is observable on satisfiable instances only. We understand this behavior as follows: for some (not all) satisfiable instances, adding the symmetry breaking clauses "randomly" influences the decision heuristics of the SAT solver in such a way that it sometimes takes more time to reach a satisfiable assignment; in any way, if there is a satisfiable assignment, then all permutations of the uninterpreted constants (i.e. the ones for which the formula is invariant) are also satisfiable assignments, and there is no advantage in trying one rather than an other. For unsatisfiable instances, if terms breaking the invariance play a role in the unsatisfiability of the problem, then adding the symmetry breaking clauses always reduces the number of cases to consider, potentially by a factor of n n /n! (where n is the number of constants), and have a negligible impact if the symmetry breaking terms play no role in the unsatisfiability. To compare with the state-of-the-art solvers, we selected all competing solvers in SMT-COMP 2010, adding also Z3 (for which we took the most recent version running on Linux we could find, namely version 2.8), and Yices (which was competing as the 2009 winner). The results are presented in Table 1. Columns T and T are the total time, in seconds, on the QF UF library, excluding and including timeouts, respectively. It is important to notice that these results include the whole QF UF library of benchmarks, that is, with the diamond benchmarks. These benchmarks require some preprocessing heuristic [16] which does not seem to be implemented in CVC3 and MathSAT. This accounts for 83 timeouts in CVC3 and 80 in MathSAT. According to this table, with a 120 seconds timeout, the best solvers on QF UF without the diamond benchmarks are (in decreasing order) veriT with symmetries, Yices, MathSAT, openSMT, CVC3. Exploiting symmetries allowed veriT to jump from the second last to the first place of this ranking. Within 20 seconds, it now solves over 50 benchmarks more than the next-best solver.

Figure 4 presents another view of the same experiment; it clearly shows that veriT is always better (in the number of solved instances within a given timeout) than any other solver except Yices, but it even starts to be more successful that Yices when the timeout is larger than 3 seconds. Scatter plots of veriT against the solvers mentioned above give another comparative view; they are available in Appendix A. Again the benefits on the zone with a time smaller that 3 seconds on both axes is not always clear. Also, bear in mind that the satisfiable instances do not benefit from the technique and still exhibit on the scatter plot the somewhat poor efficiency of veriT without symmetries. But the zone between 3 and 120 seconds on the x axis is clearly more populated than the zone between 3 and 120 seconds on the y axis.

Table 2 presents a summary of the symmetries found in the QF UF benchmark category. Among 6647 problems, 3310 contain symmetries tackled by our method. For 2698 problems, the symmetry involves 5 constants; for most of them, 3 symmetry breaking clauses were added.

The technique presented in this paper is a preprocessing technique, and, as such, it is applicable to the other solvers mentioned here. We conducted an experiment on the QF UF benchmarks augmented with the symmetry breaking clauses. We observed the same kind of impressive improvement for all solvers. The most efficient solvers solve all but very few instances (diamond benchmarks excluded): within a time limit of 120s and on the whole library, Yices only fails for one formula, CVC for 36, and the others fails for 3 or 4 formulas. We also observe a significant decrease in cumulative times, the most impressive being Yices solving the full QF UF library but one formula in around 10 minutes. Scatter plots exhibiting the improvements are available in Appendix B.

Conclusion

Symmetry breaking techniques have been used very successfully in the areas of constraint programming and SAT solving. We here present a study of symmetry breaking in SMT. It has been shown that the technique can account for an exponential decrease of running times on some series of crafted benchmarks, and that it significantly improves performances in practice, on the QF UF category of the SMT library, a category for which the same solver performed fastest in 2009 and 2010. It may be argued that the heuristic has only be shown to be effective on the pigeonhole problem and competition benchmarks in the QF UF category. However, we believe that in their most natural encoding many concrete problems contain symmetries; provers in general and SMT solvers in particular should be aware of those symmetries to avoid unnecessary exponential blowup. We are particularly interested in proof obligations stemming from verification of distributed systems; in this context many processes may be symmetric, and this should translate to symmetries in the corresponding proof obligations. Although the technique is applicable in the presence of quantifiers and interpreted symbols, it appears that symmetries in the other SMT categories are somewhat less trivial, and so, require more clever heuristics for guessing invariance, as well as more sophisticated symmetry breaking tools. This is left for future work. Also, our technique is inherently non-incremental, that is, symmetry breaking assumptions should be retrieved, and checked against new assertions when the SMT solver interacts in an incremental manner with the user. This is not a major issue, but it certainly requires a finer treatment within the SMT solver than simple preprocessing.

The veriT solver is open sourced under the BSD license and is available on http://www.veriT-solver.org.

Introduction

We present the satisfiability modulo theory (SMT) solver veriT, a joint work of University of Nancy, INRIA (Nancy, France) and Federal University of Rio Grande do Norte (Natal, Brazil). veriT provides an open, trustable and reasonably efficient decision procedure for the logic of unquantified formulas over uninterpreted symbols, difference logic over integer and real numbers, and the combination thereof. This corresponds to the logics identified as QF IDL, QF RDL, QF UF and QF UFIDL in the SMT-LIB benchmarks [15,3]. veriT also includes quantifier reasoning capabilities through the integration of a first-order prover and quantifier instantiation heuristics. Finally, veriT has proof-production capabilities; it outputs proofs that may be used or checked by external tools.

veriT is incremental, i.e. after each satisfiability check, new formulas can be added conjunctively to the already checked set of formulas. The input format is the SMT-LIB language [15], but veriT can also be used as a library with an API following the guidelines of [12]. The tool is open-source and distributed under the BSD licence at http://www.verit-solver.org. Internally, the solver is organized to be easily extended by plugging new decision procedures in a Nelson-Oppen like combination schema. Although not (yet) as fast as the solvers performing best in the SMT competition [3], veriT has a decent efficiency. We thus claim that it can already be useful in verification platforms where an opensource license, extensibility, and proof certification are important.

Selected features of the veriT solver and an experimental evaluation of its efficiency are presented in Section 2 and 3, respectively. Future developments are described in Section 4.

System description

The reasoning core of veriT uses a SAT solver [9] to produce models of the Boolean abstraction of the input formula. Such propositional assignments are given to a so-called theory reasoner, responsible for verifying if they are models in the background theory. This theory reasoner is a fully incremental combination of decision procedures à la Nelson and Oppen, where non-convexity of theories is handled using the model-equality propagation technique [7] which integrates model-based guessing [5] in a classical Nelson-Oppen equality exchange. Equality propagation is controlled by the congruence closure algorithm.

The remainder of this section describes some special features of veriT: integration of a third-party first-order prover, extension of the input language with macro definitions, and production of proofs certifying the produced results.

Integrating a first-order prover

As a particular feature inherited from its predecessor haRVey [8] and, to complement very simple instantiation heuristics, the veriT solver includes a first-order logic (FOL) superposition prover. However, veriT greatly improves the integration of the FOL prover with the other decision procedures, notably with congruence closure. Indeed, the first-order prover is seen within the combination à la Nelson-Oppen as a "decision procedure" that takes an arbitrary FOL theory as a parameter. However, due to the cost of running the FOL prover and to its non-incremental nature (when used as a black box), this procedure is called in last resort. A FOL theory is computed from the quantified sub-formulas in the assignment, abstracting ground sub-terms in order to minimize the number of relevant symbols in the theory. In addition, information from congruence closure is used to abstract all subterms in the assignment that do not contain such relevant symbols.

The prover may deduce that the given set of formulas is unsatisfiable. In that case, the deduction tree is parsed to obtain the relevant unsatisfiable subset of the input. A conflict clause is then built using this set and, again, information from the congruence closure data structures. Since the prover is given an upper limit of resources, it always terminates. If the prover terminates without proving the unsatisfaibility of the given set of formulas, ground equalities and deduced ground clauses are identified and propagated back to veriT.

In many cases where the superposition calculus is a decision procedure [2] for the theory represented by the quantified formulas, our technique simulates a Nelson-Oppen combination with on-the-fly purification. It has been shown that first-order generic provers may perform quite well even compared to dedicated decision procedures (see for instance [1]). Currently, the E-prover [16] is used as the first-order prover, and we plan to include Spass [18], which provides better sort handling. Fine-tuning the interplay between the instantiation heuristics and the e-prover is essential for efficiency and remains to be done.

Macros

The input format for veriT is the SMT-LIB language extended with macro definitions. This syntactic sugar is particularly useful for instance to write formulas containing simple sets constructions (see Figure 1). After β-reduction, and after rewriting equalities between predicates and functions (for instance, if p and q are unary predicates, p = q is rewritten as ∀x . p(x) ≡ q(x)), the obtained formula is first-order. Such formulas may contain quantifiers but, if no function is used, they belong to the Bernays-Schönfinkel-Ramsey fragment (the Bernays-Schönfinkel class with equality) which is decidable. veriT can use the embedded FOL prover as a decision procedure for this fragment. In many more intricate cases [10], the resulting formula still belongs to a decidable fragment, but the decision procedure may become very expensive. To be practical, such cases require heuristics that have not yet been implemented in veriT.

This macro feature is indeed used in tools (e.g. CRefine [14]) that generate verification conditions for formal developments in set-based modelling languages, such as Circus [4], and that integrate veriT as a verification engine to discharge these proof obligations.

(benchmark SET008_3p

:logic UNKNOWN :extrasorts (ELMT) :extrapreds ((B ELMT) (C ELMT)) :extramacros ((emptyset (lambda (?v ELMT) . false)) (intersection (lambda (?p (ELMT boolean)) (?q (ELMT boolean)) .

(lambda (?x ELMT) . (and (?p ?x) (?q ?x))))) (difference (lambda (?p (ELMT boolean)) (?q (ELMT boolean)) .

(lambda (?x ELMT) . (and (?p ?x) (not (?q ?x))))))) :formula (not (= (intersection (difference B C) C) emptyset))) Fig. 1. A simple example with the macro capability.

Proofs

Proof production has two goals. First, this feature increases the confidence in the tool, the proofs being checked by an independent module inside veriT. Second, skeptical proof assistants can use such traces to reconstruct proofs of formulas discharged by veriT (see [11]).

In Figure 2, we give an example of a very simple formula, and the proof output by veriT. Each line states a fact that can be assumed to hold. It is identified by a number, followed by a list starting with a label identifying the rule used to deduce the fact, followed by a clause, and optionally ended by numerical parameters. In our context, a clause is a disjunctive list of formulas (not literals), maybe containing a sole formula. The numerical parameters depend on the rule, and may be either identifiers of previous clauses (e.g. in the resolution rule), or other place information. As an example, the and rule (for instance the second line in Figure 2: (and((= a c)) 1 0)) takes two numerical parameters. The first numerical parameter refers to the clause C in a previous numbered rule (i.e. 1 refers to the clause in the input rule, at line 1). This clause C is unit and is hence represented as a list of one formula (the whole input formula in our example), and this formula is a conjunction a 0 ∧ • • • ∧ a n . Obviously, each subformula a 0 , . . . a n is a consequence of C, and the second parameter just gives the identifier of the formula in the new clause, i.e. the second numerical parameter in rule at line 2 indicates the formula at position 0 in the input.

veriT already provides proof production for formulas with arbitrary Boolean structure and uninterpreted functions, and is being extended to linear arithmetics. The first line is the input. Every other fact is either a consequence of previous ones, or is a tautology. The input formula being unsatisfiable, the last deduced fact is the empty clause. In the example, lines 2 to 7 account for the conjunctive normal form transformation. Lines 8, 9, 15, and 16 are tautologies related to the theory of equality. The remaining facts are deduced by resolution from the other ones.

Since every proof-related information is handled through a unique module inside veriT, any proof format for SMT (for instance [17,6]) can be adopted as soon as it becomes a standard. Although our previous experiments [11] showed that the proof size was not the bottleneck for the cooperation with skeptical proof assistants, the implementation of techniques to greatly reduce the size of our proof traces is planned.

Experimental evaluation

We evaluated veriT, CVC3 and Z3 (both using the latest available version in February 2009) against the SMT-LIB benchmarks for QF IDL, QF RDL, QF UF and QF UFIDL (June 2008 version) using an Intel(R) Pentium(R) 4 CPU at 3.00 GHz with 1 GiB of RAM and a timeout of 120 seconds. The following table presents, for each solver, the number of completed benchmarks. This clearly shows that, although veriT is not yet as efficient as competition winning tools [3], its efficiency is decent. The proof production capability of veriT does not come at a cost on efficiency.

Future work

veriT is a new SMT-solver that provides an open framework to generate certifiable proofs without sacrificing too much efficiency. The future developments will notably include features related to efficiency and expressiveness. Considering efficiency aspects, the tool does not yet implement theory propagation [13], a technique that is known to greatly improve the efficiency of SMT solvers. Concerning expressiveness, the linear arithmetic decision procedure currently only handles difference logic; we are now developing a reasoning engine for linear arithmetic based on the Simplex method, which will extend completeness to full linear arithmetic. Quantifier reasoning will be improved by including new instantiation heuristics, as well as adding support for patterns guiding quantifier instantiations. We also plan to integrate the proof production capabilities of the embedded FOL prover with that of veriT.

Finally, we are working on the application of veriT to formal development efforts, mainly of concurrent systems. In that context, the ability to handle sets is very helpful; a major objective is to improve the support for such constructions.

Definition 3 (

 3 Congruence closure) The congruence closure E * of a set of equations E on a set of terms T closed under the subterm relation is the smallest congruence relation on T containing E.

2 Remark 1 Example 2

 212 appears negatively in C i } where c 1 , . . . c n , c 1 , . . . c n , x1 , . . . xm , 1 , . . . m , ⊥ 1 , . . . ⊥ m are distinct constants, and t 1 , . . . t n are distinct unary functions. Note that the constants i and ⊥ i (for 1 ≤ i ≤ m)) should not be confused with the Boolean values and ⊥. The intuitive relationship between these constants and the boolean values is established in Definition 7. The translation of clauses is illustrated by the following example. Consider the set of clauses C

Fig. 2

 2 Fig. 2 The congruence translation E C = Connect ∪ 1≤i≤n Clause i of C.

Example 3 ( 3 Fig. 3 3 Fig. 5 Lemma 1

 333351 Fig. 3 Congruence translation of I

Lemma 2

 2 Consider a (partial or total) assignment I for non-tautological clauses C = {C 1 , . . . C n } on variables x 1 , . . . , x m . |E I ∪ E C | and |T (E I ∪ E C )| are polynomial in n and m.

Figure 1 :

 1 Figure 1: Schematic view of an SMT solver.

Figure 3 :

 3 Figure 3: Grammar of the language produced by ppTrans. The non-terminals are P (predicates), L (list of identifiers), I (identifiers), A (arithmetic expressions), B (Boolean expressions), M (maplet expressions), S (set expressions).

Figure 4 :

 4 Figure 4: The different syntactic categories and the symbols relating them: A for arithmetic expressions, P for predicates, S for set expressions, B for Boolean expressions and M for maplet expressions. ppTrans removes all occurrences of the constructs delimited by doublebrackets.

(

  declare-fun (MS0 (S PS) Bool)) (declare-fun (MS1 (S T PST) Bool)) (declare-fun (MS2 (S T U PSTU)) Bool)

Figure 5 :

 5 Figure 5: SMT-LIB input produced using the λ-based approach.

Figure 6 :

 6 Figure 6: SMT-LIB input produced using the ppTrans approach.

Definition 1 .

 1 An arrangement A for finite sets of constant symbols S and unary predicates P is a maximal satisfiable set of equalities and inequalities a = b or a = b and literals p(a) or ¬p(a), with a, b ∈ S, p ∈ P.

Lemma 2 .

 2 Let T be a BSR theory, and M be a model of T on domain D. Then any restriction M of M on domain D with D c ⊆ D ⊆ D is a model of T . Proof. Consider M and M as above. Since M is a model of T , for each closed formula ∀x 1 . . . x n . ϕ in T (where ϕ is function-free and quantifier-free), and for all d 1 , . . . , d n ∈ D ⊆ D, M x1/d1,...,xn/dn is a model of ϕ. This also means that, for all d 1 , . . . , d n ∈ D , M x1/d1,...,xn/dn is a model of ϕ, and finally that M is a model of ∀x 1 . . . x n . ϕ.

Definition 3 .

 3 An interpretation I on domain D for a BSR theory T is nrepetitive for a set V of Venn regions if, for each v ∈ V , |D v \ D c | ≥ n and there exists a total order ≺ on elements in D v \ D c such that -for every r-ary predicate symbol p in T -for all d 1 , . . . , d r ∈ D, and d 1 , . . . , d r ∈ D with • |{d 1 , . . . , d r } \ D

  we have I[p](d 1 , . . . , d r ) = I[p](d 1 , . . . , d r ).

  for |{d 1 , . . . , d r } \ D c | > n: the interpretation of p over tuples with more than n elements outside D c is fixed arbitrarily. Indeed, such tuples are irrelevant for the evaluation of the formulas of T : terms occurring as arguments of a predicate are either variables or constants, and no more than n variables occur in any formula of T . -otherwise, to determine M [p](d 1 , . . . , d r ), first choose d 1 , . . . d r ∈ D such that d 1 , . . . , d r and d 1 , . . . d r are related to each other just like in Definition 3. This is possible since, for every Venn region v for which the interpretation is repetitive, there are at least n elements in D v \D c . Then (d 1 , . . . , d r ) ∈ M [p] iff (d 1 , . . . , d r ) ∈ M[p]. Observe that all possible choices of d 1 , . . . , d n lead to the same definition because M is n-repetitive.The construction is such that M is also n-repetitive for the same regions. It is also a model of T : all formulas in T are of the form ∀x 1 . . . x m . ϕ(x 1 , . . . , x m ), with m ≤ n. For alld 1 . . . , d m ∈ D , if {d 1 , . . . , d m } ⊆ D then M x1/d 1 ,...,xm/d m [ϕ(x 1 , . . . , x m )] = M x1/d 1 ,...,xm/d m [ϕ(x 1 , . . . , x m )] since M is an extension of M. Otherwise,let d 1 , . . . , d m ∈ D be some elements related to d 1 , . . . , d m like in Definition 3. Since M is n-repetitive, M x1/d 1 ,...,xm/d m [ϕ(x 1 , . . . , x m )] = M x1/d1,...,xm/dm [ϕ(x 1 , . . . , x m )] = M x1/d1,...,xm/dm [ϕ(x 1 , . . . , x m )]. In both cases, M x1/d 1 ,...,xm/d m [ϕ(x 1 , . . . , x m )] evaluates to true, and therefore M is a model of ∀x 1 . . . x n . ϕ(x 1 , . . . , x m ).

  1 , . . . , d r ∈ D c ∪ {e 1 , . . . , e n }, (d 1 , . . . , d r ) ∈ M[p] iff (d 1 , . . . , d r ) ∈ M[p], with d i = e j if d i = e j for some j, and d i = d i otherwise. Notice that there are only a finite number of disagreeing configurations for n elements in D \ D c : more precisely a configuration is determined by at most b = p (n + |D c |) arity(p) Boolean values, where the sum ranges over all predicates in the theory. Thus the number of disagreeing configurations is bounded by C = 2 b . Interpreting configurations as colors, one can use the extension of Ramsey's Theorem given in Appendix A: according to Theorem 7, there is a computable function f such that, for any N ∈ N, if |D \ D c | V ≥ f (n, N, C), then there exists a model on D ⊆ D with |D \ D c | V ≥ N for which configurations agree if they have the same number of elements in each Venn region of V . Taking N = n, this is actually building a n-repetitive restriction of M.

Definition 2 .

 2 A T -preserving rewriting operator R is any transformation operator on terms and formulas such that T |= t = R[t] for any term, and T |= ϕ ⇔ R[ϕ] for any formula ϕ. Moreover, for any permutation operator P , for any term and any formula, R • P • R and R • P should yield identical results.

  ψ, M |= ψ if and only if M c0/dj ,cj /d0 |= P [ψ], where d 0 and d j are respectively M[c 0 ] and M[c j ]. Choosing ψ = def ϕ ∧ t = c j , it follows that M c0/dj ,cj /d0 |= P [ϕ ∧ t = c j ], and thus M c0/dj ,cj /d0 |= P [ϕ] ∧ t = c 0 since t is invariant w.r.t. permutations of c 0 , . . . , c n . Furthermore, since ϕ is invariant w.r.t. permutations of c 0 , . . . , c n , R[P [ϕ]] is ϕ for the fixed T -preserving rewriting operator. Since R is T -preserving, M c0/dj ,cj /d0 |= P [ϕ] if and only ifM c0/dj ,cj /d0 |= R[P [ϕ]],that is, if and only if M c0/dj ,cj /d0 |= ϕ. Finally M c0/dj ,cj /d0 |= ϕ ∧ t = c 0 , and M c0/dj ,cj /d0 belongs to T since c 0 and c j are uninterpreted. The formula ϕ ∧ t = c 0 is thus T -satisfiable.For the general case, notice that ϕ = def ϕ ∧ ¬(t = c 0 ∨ . . . ∨ t = c i-1 ) is invariant w.r.t. permutations of c i , . . . , c n , and ϕ |= T t = c i ∨ . . . ∨ t = c n . By the previous case (applied to the set of constants c i , . . . , c n instead of c 0 , . .

Lemma 6 .

 6 A formula ϕ is invariant w.r.t. permutations of constants c 0 , . . . , c n if both permutation operators -P circ such that P circ [c i ] = c i-1 for i ∈ {1, . . . , n} and P circ [c 0 ] = c n , -P swap such that P swap [c 0 ] = c 1 and P swap [c 1 ] = c 0 are symmetry operators for ϕ.

1 foreach 3 T 4 cts := ∅ ; 5 while T = ∅ ∧ |cts| ≤ n do 6 t 7 T 18 Algorithm 1 :

 134567181 {c0, . . . , cn} ∈ P do 2 if invariant by permutations(ϕ, {c0, . . . , cn}) then := select terms(ϕ, {c0, . . . , cn}) ; := select most promising term(T, ϕ) ; := T \ {t} ; 8 cts := cts ∪ used in(t, {c0, . . . , cn}) ; 9 let c ∈ {c0, . . . , cn} \ cts; 10 cts := cts ∪ {c}; 11 if cts = {c0, . . . , cn} then 12 ϕ := ϕ ∧ c i ∈cts t = ci ; A symmetry breaking preprocessor.

Fig. 1 .

 1 Fig. 1. Some SMT solvers and the pigeonhole problem

Fig. 2 .

 2 Fig.2. Efficiency in solving individual instances: veriT vs. veriT without symmetries on all formulas in the QF UF category. Each point represents a benchmark, and its horizontal and vertical coordinates represent the time necessary to solve it (in seconds). Points on the rightmost and topmost edges represent a timeout.

Fig. 3 .

 3 Fig. 3. Efficiency in solving individual instances: veriT vs. veriT without symmetries on the unsatisfiable instances of the QF UF category.

Fig. 2 .

 2 Fig. 2. A simple example with its proof.

  ings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, July 11-17, 2009, pages 399-404, 2009. Kshitij Bansal, Andrew Reynolds, Clark W. Barrett, and Cesare Tinelli. A new decision procedure for finite sets and cardinality constraints in SMT. In Nicola Olivetti and Ashish Tiwari, editors, International Joint Conference on Automated Reasoning (IJCAR), volume 9706 of Lecture Notes in Computer Science, pages 82-98. Springer, 2016. Selected Papers from the Workshops on Disproving and the Second International Workshop on Pragmatics of Decision Procedures (PDPAR 2004), volume 125 of Electronic Notes in Theoretical Computer Science, pages 37-51, July 2005. Andreas Fellner, Pascal Fontaine, and Bruno Woltzenlogel Paleo. NP-completeness of small conflict set generation for congruence closure. Formal Methods in System Design 51(3): 533-544 (2017)

	Glossary
	BCP Boolean Constraint Propagation
	CDCL Conflict-Driven Clause Learning •
	CNF Conjunctive Normal Form
	of Automated Reasoning, volume I, chapter 12, pages 751-842. Elsevier 3569 of Lecture Notes in Computer Science, pages 61-75. Springer, June DPLL Davis, Puttnam, Logemann and Loveland algorithm
	Science B.V., 2001. 2005. FOL First-Order Logic
	[9] Leo Bachmair and Harald Ganzinger. Rewrite-Based Equational The-[25] Maria Paola Bonacina, Ulrich Furbach, and Viorica Sofronie-[58] Andreas Fellner, Pascal Fontaine, Georg Hofferek, and Bruno Woltzen-FUIP First Unique Implication Point
	orem Proving with Selection and Simplification. Journal of Logic and Computation, 4(3):217-247, 1994. Stokkermans. On first-order model-based reasoning. In Narciso Martí-Oliet, Peter Csaba Ölveczky, and Carolyn L. Talcott, editors, Logic, logel Paleo. NP-completeness of small conflict set generation for con-gruence closure. In Vijay Ganesh and Dejan Jovanović, editors, Inter-ITP Interactive Theorem Prover
	Rewriting, and Concurrency -Essays dedicated to José Meseguer on the MCSAT Model-Constructing Satisfiability Modulo Theories national Workshop on Satisfiability Modulo Theories (SMT), 2015. [10] Leo Bachmair and Harald Ganzinger. Resolution theorem proving. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Au-tomated Reasoning, volume I, chapter 2, pages 19-99. Elsevier Science B.V., 2001. gium, September 2004. [11] [15] Clark Barrett, Daniel Kroening, and Thomas Melham. Problem solving Occasion of His 65th Birthday, volume 9200 of Lecture Notes in Com-[59] Andreas Fellner, Pascal Fontaine, and Bruno Woltzenlogel Paleo. NP-RISC Reduced Instruction Set Computer puter Science, pages 181-204. Springer, 2015. [26] Maria Paola Bonacina, Christopher Lynch, and Leonardo Mendonça de Moura. On deciding satisfiability by theorem proving with specu-lative inferences. Journal of Automated Reasoning, 47(2):161-189, 2011. completeness of small conflict set generation for congruence closure. For-SAT Propositional Satisfiability mal Methods in System Design, 51(3):533-544, December 2017. SMT Satisfiability Modulo Theories [60] Pascal Fontaine. Techniques for verification of concurrent systems with invariants. PhD thesis, Institut Montefiore, Université de Liège, Bel-VSIDS Variable State Independent Decaying Sum
	for the 21st century: Efficient solvers for satisfiability modulo theories.
	Technical Report 3, London Mathematical Society and Smith Institute [31] Martin Bromberger and Christoph Weidenbach. Fast Cube Tests for LIA
	for Industrial Mathematics and System Engineering, June 2014. Knowl-Constraint Solving. In Nicola Olivetti and Ashish Tiwari, editors, Inter-
	edge Transfer Report. national Joint Conference on Automated Reasoning (IJCAR), volume

[12]

Haniel Barbosa, Jasmin Christian Blanchette, and Pascal Fontaine. Scalable fine-grained proofs for formula processing. In Leonardo de Moura, editor, Proc. Conference on Automated Deduction (CADE), volume 10395 of Lecture Notes in Computer Science, pages 398-412. Springer, 2017.

[13] Haniel Barbosa, Pascal Fontaine, and Andrew Reynolds. Congruence closure with free variables. In Axel Legay and Tiziana Margaria, editors, Tools and Algorithms for Construction and Analysis of Systems (TACAS), volume 10206 of Lecture Notes in Computer Science, pages 214-230. Springer, 2017. [14] Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification (CAV), volume 6806 of Lecture Notes in Computer Science, pages 171-177. Springer, 2011. [27] Joseph Boudou, Andreas Fellner, and Bruno Woltzenlogel Paleo. Skeptik: A proof compression system. In Stéphane Demri, Deepak Kapur, and Christoph Weidenbach, editors, International Joint Conference on Automated Reasoning (IJCAR), volume 8562 of Lecture Notes in Computer Science, pages 374-380. Springer, 2014. [28] Thomas Bouton, Diego Caminha B. de Oliveira, David Déharbe, and Pascal Fontaine. veriT: an open, trustable and efficient SMT-solver. In Renate Schmidt, editor, Proc. Conference on Automated Deduction (CADE), volume 5663 of Lecture Notes in Computer Science, pages 151-156, Montreal, Canada, 2009. Springer. [29] Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Silvio Ranise, Peter van Rossum, and Roberto Sebastiani. Efficient satisfiability modulo theories via delayed theory combination. In Kousha Etessami and Sriram K. Rajamani, editors, Computer Aided Verification (CAV), volume 3576 of Lecture Notes in Computer Science, pages 335-349. Springer, 2005. [30] Martin Bromberger, Thomas Sturm, and Christoph Weidenbach. Linear integer arithmetic revisited. In Amy P. Felty and Aart Middeldorp, editors, Proc. Conference on Automated Deduction (CADE), volume 9195 of Lecture Notes in Computer Science, pages 623-637. Springer, 2015. [61] Pascal Fontaine. Combinations of theories for decidable fragments of first-order logic. In Silvio Ghilardi and Roberto Sebastiani, editors, Frontiers of Combining Systems (FroCoS), volume 5749 of Lecture Notes in Computer Science, pages 263-278. Springer, 2009. [62] Pascal Fontaine. Combinations of theories for decidable fragments of first-order logic, 2009. Available at http://www.loria.fr/ ~fontaine/ Fontaine12b.pdf. [63] Pascal Fontaine and E. Pascal Gribomont. Using BDDs with combinations of theories. In Matthias Baaz and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), volume 2514 of Lecture Notes in Computer Science, pages 190-201. Springer-Verlag, 2002. [64] Pascal Fontaine and E. Pascal Gribomont. Decidability of invariant validation for parameterized systems. In Hubert Garavel and John Hatcliff, editors, Tools and Algorithms for Construction and Analysis of Systems (TACAS), volume 2619 of Lecture Notes in Computer Science, pages 97-112. Springer-Verlag, 2003. [65] Pascal Fontaine and E. Pascal Gribomont. Combining non-stably infinite, non-first order theories. In W. Ahrendt, P. Baumgartner, H. de Nivelle, S. Ranise, and C. Tinelli, editors,

  David Déharbe, Pascal Fontaine, Yoann Guyot and Laurent Voisin. Integrating SMT solvers in Rodin. Sci. Comput. Program. 94(2): 130-143 (2014)One of the most often used motivation for automated reasoning is verification. In this work, we investigated the use of SMT in addition to the traditional tools embedded in the Rodin platform for formal development in Event-B. Our contribution is the definition of a translation of Event-B proof obligations to the language of SMT solvers, its implementation in a Rodin plug-in, and an experimental evaluation on a large sample of industrial and academic projects. On this domain, adding SMT solvers to Atelier B provers reduces significantly the number of sequents that need to be proved interactively. SMT solvers are now regularly used within Rodin.

• Paula Chocron, Pascal Fontaine, and Christophe Ringeissen. A Gentle Non-Disjoint Combination of Satisfiability Procedures. In Stéphane Demri, Deepak Kapur and Christoph Weidenbach, editors, In Proc. International Joint Conference on Automated Reasoning (IJCAR), volume 8562 of Lecture Notes in Computer Science (LNCS). pages 122-136, Springer, 2014.

  Oliveira, David Déharbe and Pascal Fontaine. veriT: an open, trustable and efficient SMT-solver. In Renate A. Schmidt, editor, In Proc. Conference on Automated Deduction (CADE). volume 5663 of Lecture Notes in Computer Science (LNCS), pages 151-156. Springer-Verlag, 2009.

This is the published tool description of the veriT solver, which took a significant amount of my time to design and develop. The current version of the solver also owes Haniel Barbosa some impressive improvements, particularly on the quantifier handling aspects. The veriT solver is used as back-end in several platforms, e.g. Isabelle via Sledgehammer and Rodin via the SMT plugin.

Table 1 :

 1 Number of proof obligations discharged by the reasoners.

	Number of	proof obligations	Rodin	Atelier-B	alt-ergo-r217	cvc3-2011-11-21	veriT-dev-r2863	veriT & E-prover	z3-3.2
	2456 1169 2260 2017 2218 2051 2160 2094

Table 2 :

 2 Number of proof obligations not discharged by special-purpose reasoners and by each SMT solver.

	Number of	proof obligations	left	alt-ergo-r217	cvc3-2011-11-21	veriT-dev-r2863	veriT & E-prover	z3-3.2	All SMT solvers
	196		114 61 94 103 92 31

Table 3

 3

	synthesizes a pairwise comparison of the SMT solvers on our universe of proof
	obligations.
		alt-ergo cvc3 veriT veriT+E z3
	alt-ergo	2017	2001 1880	1967	1911
	cvc3	2001	2218 1953	2088	2031
	veriT	1880	1953 2051	1958	1878
	veriT+E	1967	2088 1958	2160	2067
	z3	1911	2031 1878	1972	2094

Table 3 :

 3 Number of proof obligations verified by SMT solver A also discharged by solver B.

3 1

 3 Universidad de Buenos Aires, Argentina 2 INRIA, Université de Lorraine & LORIA, Nancy, France 3 INRIA & LORIA, Nancy, France

Table 1 .

 1 Some SMT solvers on the QF UF category

	80 80-100 100-120	T	T

Table 2 .

 2 Number of solved instances of QF UF within a time limit, for some SMT solvers. Symmetries detected for the QF UF category: nsym indicates the number of constants involved in the symmetry, nc the number of symmetry breaking clauses.

		veriT veriT w/o sym. CVC3 MathSAT OpenSMT Yices Z3
	time (in seconds)
	0.1 5000		5500			6000		6500		7000
					solved instances
	Fig. 4. H H H nc nsym H H	2	3	4	5	6	7	8	9	10	11
		2
			12		8
				24 2668
					22	92	3
						122 166
						156
								17
									11
										5
	10										2
	Total	2	12	24 2698 214 325	17	11	5	2

At the time of writing this lines, we believe the complexity of full disequality propagation is still an open problem.

http://matryoshka.gforge.inria.fr/

In the context of a project with RATP, I was myself quite surprised to realize that many people with a verification background work there.

We contacted both Ashish Tiwari and the authors of[10], who confirmed this.

It would be possible to define a translation without the c i constants, but they ease the presentation.

http://deploy-eprints.ecs.soton.ac.uk

This work has been partially supported by the project ANR-13-IS02-0001-01 of the Agence Nationale de la Recherche, by the European Union Seventh Framework Programme under grant agreement no. 295261 (MEALS), and by the STIC AmSud MISMT

This work was partly supported by the ANR DeCert project and the INRIA-CNPq project SMT-SAVeS.

Theory propagation in veriT is quite basic: only equalities deduced from congruence closure are propagated. pi = hi would never be propagated from pj = hi and pi = pj.

The timeout was set to 120 seconds, using Linux

bits on Intel(R) Xeon(R) CPU E5520 at 2.27GHz, with 24 GBytes of memory.

Acknowledgment. We would like to thank Robert Nieuwenhuis and Ashish Tiwari for discussions and some preliminary ideas that led us to this proof. We are grateful to the anonymous reviewers of this paper and of [4] for their comments. Acknowledgments: This paper is a revised and extended version of [15]. We thank the anonymous reviewers of paper [15] and of this paper for their careful read and their remarks.

Acknowledgements. Experiments presented in this paper were carried out using the Grid'5000 experimental testbed, being developed under the INRIA AL-ADDIN development action with support from CNRS, RENATER and several universities as well as other funding bodies (see https://www.grid5000.fr).

We would like to thank the anonymous reviewers for their helpful comments and suggestions.

Acknowledgments: We would like to thank Stephan Merz for his comments and guidance. The ancestor of the veriT solver, haRVey, was initiated by the third author and Silvio Ranise, to whom we are indebted of several ideas used in veriT. We are also grateful to the anonymous reviewers for their remarks.

This work has been partially supported by the project ANR-13-IS02-0001 of the Agence Nationale de la Recherche, by the H2020-FETOPEN-2016-2017-CSA project SC 2 (712689), by an ÖAW APART Stipendium, by FWF W1255-N23, by ERC Start Grants Graph Games (279307) and Matryoshka (713999), and by FFG project number 845582 (TRUCONF).

$ This work is partly supported by the project ANR-13-IS02-0001-01, the STIC Am-Sud project MISMT, CAPES grant BEX 2347/13-0, CNPq grants 308008/2012-0 and 573964/2008-4 (National Institute of Science and Technology for Software Engineering-INES, www.ines.org.br), and EU funded project ADVANCE (FP7-ICT-287563).

. Elimination of equalities

The notation ∀X T •P (X) stands for ∀fv(∇(e))•P (∇(e)), with T (X) = T .

Elimination of mixed operators

Appendix A.4. Rules based on the right argument of set membership

Elimination of membership in relations

The notation func(f ) specifies that f is a function, and abbreviates:

Other membership rewriting rules

The notation ∀X T •P (X) stands for ∀fv(∇(e))•P (∇(e)), with T (X) = T . Likewise, notation ∃X T •P (X) stands for ∃fv(∇(e))•P (∇(e)), with T (X) = T .

A An Extension of Ramsey's Theorem

We define an n-subset of S to be a subset of n elements of S. An n-hypergraph of S is a set of n-subsets of S. In particular, a 2-hypergraph is an (undirected) graph. The complete n-hypergraph of S is the set of all n-subsets of S, and its size is the cardinality of S. An n-hypergraph G is colored with c colors if there is a coloring function that assigns one color to every n-subset in G. In particular, a colored 2-hypergraph (that is, a colored graph), is a graph where all edges are assigned a color. Consider a set S of elements partitioned into disjoint regions R = {R 1 , . . . R m }. We say that a set S ⊆ S has region size larger than x and note

x for all i ∈ {1, . . . , m}. We also say that an nhypergraph is region-monochromatic if the color of each hyperedge only depends on the number of elements belonging to each region. Two hyperedges are said of the same kind if they have the same number of elements in each region; all hyperedges of the same kind of a region-monochromatic hypergraph thus have the same color. The following extension 4 of Ramsey's Theorem holds: Proof. The full proof can be found in [7].

A veriT and other solvers

Here are scatter plots exhibiting the performances of veriT in solving individual instances of QF UF veriT against some other SMT solvers. B Other solvers on formulas with symmetry breaking clauses

These scatter plots exhibit the gain of efficiency from symmetries for some stateof-the-art solvers. They compare running times on QF UF formulas with symmetry breaking clauses and on original formulas. The following table presents the results of some SMT solvers on QF UF formulas without and with symmetry breaking clauses. 83 timeouts for CVC and 80 for MathSAT are due to the diamond benchmarks.