Arrays are ubiquitous in the context of software verication. However, eective reasoning over arrays is still rare in CP, as local reasoning is dramatically ill-conditioned for constraints over arrays. In this paper, we propose an approach com- bining both global symbolic reasoning and local consistency ltering in order to solve constraint systems involving arrays (with accesses, updates and size constraints) and nite-domain constraints over their elements and indexes. Our approach, named fdcc, is based on a combination of a congruence closure algorithm for the standard theory of arrays and a CP solver over nite domains. The tricky part of the work lies in the bi- directional communication mechanism between both solvers. We identify the signicant information to share, and design ways to master the communication overhead. Exper- iments on random instances show that fdcc solves more formulas than any portfolio combination of the two solvers taken in isolation, while overhead is kept reasonable.
Deductive methods and SMT frameworks. It is well known in the SMT community that solving formulas over arrays and integer arithmetic in an efficient way through NO is difficult. Indeed, handling in a correct way requires to propagate all , which may be much more expensive than satisfiability checking @cite_26 . Delayed theory combination @cite_13 @cite_26 requires only the propagation of implied equalities, at the price of adding new boolean variables for all potential equalities between variables. Model-based theory combination @cite_2 aims at mitigating this potential overhead through lazy propagation of equalities.
@cite_26 @cite_13 @cite_2
2276124093 1515930456 2110780548
Most state-of-the-art approaches for Satisfiability Modulo Theories @math rely on the integration between a SAT solver and a decision procedure for sets of literals in the background theory @math . Often @math is the combination @math of two (or more) simpler theories @math , s.t. the specific @math must be combined. Up to a few years ago, the standard approach to @math was to integrate the SAT solver with one combined @math , obtained from two distinct @math by means of evolutions of Nelson and Oppen's (NO) combination procedure, in which the @math deduce and exchange interface equalities. Nowadays many state-of-the-art SMT solvers use evolutions of a more recent @math procedure called Delayed Theory Combination (DTC), in which each @math interacts directly and only with the SAT solver, in such a way that part or all of the (possibly very expensive) reasoning effort on interface equalities is delegated to the SAT solver itself. In this paper we present a comparative analysis of DTC vs. NO for @math . On the one hand, we explain the advantages of DTC in exploiting the power of modern SAT solvers to reduce the search. On the other hand, we show that the extra amount of Boolean search required to the SAT solver can be controlled. In fact, we prove two novel theoretical results, for both convex and non-convex theories and for different deduction capabilities of the @math , which relate the amount of extra Boolean search required to the SAT solver by DTC with the number of deductions and case-splits required to the @math by NO in order to perform the same tasks: (i) under the same hypotheses of deduction capabilities of the @math required by NO, DTC causes no extra Boolean search; (ii) using @math with limited or no deduction capabilities, the extra Boolean search required can be reduced down to a negligible amount by controlling the quality of the @math -conflict sets returned by the @math . The problem of deciding the satisfiability of a quantifier-free formula with respect to a background theory, also known as Satisfiability Modulo Theories (SMT), is gaining increasing relevance in verification: representation capabilities beyond propositional logic allow for a natural modeling of real-world problems (e.g., pipeline and RTL circuits verification, proof obligations in software systems). In this paper, we focus on the case where the background theory is the combination T1∪T2 of two simpler theories. Many SMT procedures combine a boolean model enumeration with a decision procedure for T1∪T2, where conjunctions of literals can be decided by an integration schema such as Nelson-Oppen, via a structured exchange of interface formulae (e.g., equalities in the case of convex theories, disjunctions of equalities otherwise). We propose a new approach for SMT(T1∪T2), called Delayed Theory Combination, which does not require a decision procedure for T1∪T2, but only individual decision procedures for T1 and T2, which are directly integrated into the boolean model enumerator. This approach is much simpler and natural, allows each of the solvers to be implemented and optimized without taking into account the others, and it nicely encompasses the case of non-convex theories. We show the effectiveness of the approach by a thorough experimental comparison. Traditional methods for combining theory solvers rely on capabilities of the solvers to produce all implied equalities or a pre-processing step that introduces additional literals into the search space. This paper introduces a combination method that incrementally reconciles models maintained by each theory. We evaluate the practicality and efficiency of this approach.