Efficient theory combination via boolean search
| Autor: | Silvio Ranise, Roberto Bruttomesso, Roberto Sebastiani, Tommi Junttila, Alessandro Cimatti, Marco Bozzano, Peter van Rossum |
|---|---|
| Rok vydání: | 2006 |
| Předmět: |
Theoretical computer science
Computer science Modulo Satisfiability Computer Science Applications Theoretical Computer Science Boolean algebra Schema (genetic algorithms) Algebra symbols.namesake Computational Theory and Mathematics Integer Simple (abstract algebra) Satisfiability modulo theories symbols Variety (universal algebra) Security of Systems Information Systems |
| Zdroj: | Information and Computation, 10, 10, pp. 1493-2525 Information and Computation, 10, 1493-2525 |
| ISSN: | 0890-5401 |
| DOI: | 10.1016/j.ic.2005.05.011 |
| Popis: | Many approaches to deciding the satisfiability of quantifier-free formulae with respect to a background theory T—also known as Satisfiability Modulo Theory, or SMT(T)—rely on the integration between an enumerator of truth assignments and a decision procedure for conjunction of literals in T. When the background theory T is the combination T1∪T2 of two simpler theories, the approach is typically instantiated by means of a theory combination schema (e.g. Nelson–Oppen, Shostak). In this paper we propose a new approach to SMT(T1∪T2), where the enumerator of truth assignments is integrated with two decision procedures, one for T1 and one for T2, acting independently from each other. The key idea is to search for a truth assignment not only to the atoms occurring in the formula, but also to all the equalities between variables which are shared between the theories. This approach is simple and expressive: for instance, no modification is required to handle non-convex theories (as opposed to traditional Nelson-Oppen combinations which require a mechanism for splitting). Furthermore, it can be made practical by leveraging on state-of-the-art boolean and SMT search techniques, and on theory layering (i.e., cheaper reasoning first, and more often). We provide thorough experimental evidence to support our claims: we instantiate the framework with two decision procedures for the combinations of Equality and Uninterpreted Functions (EUF) and Linear Arithmetic (LA), both for (the convex case of) reals and for (the non-convex case of) integers; we analyze the impact of the different optimizations on a variety of test cases; and we compare the approach with state-of-the-art competitor tools, showing that our implemented tool compares positively with them, sometimes with dramatic gains in performance. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect