Model-based theory combination. (English) Zbl 1277.03007
Krstić, Sava (ed.) et al., Proceedings of the 5th international workshop on satisfiability modulo theories (SMT 2007), Berlin, Germany, July 1–2, 2007. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 198, No. 2, 37-49 (2008).
Summary: 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.
For the entire collection see [Zbl 1276.68020].
For the entire collection see [Zbl 1276.68020].
MSC:
| 03B35 | Mechanization of proofs and logical operations |
| 03B70 | Logic in computer science |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
References:
| [1] | Ackermann, W., Solvable cases of the decision problem; Ackermann, W., Solvable cases of the decision problem · Zbl 0056.24505 |
| [2] | Barrett, C.; Tinelli, C., CVC3, (Damm, W.; Hermanns, H., CAV’07, Berlin, Germany. CAV’07, Berlin, Germany, LNCS, 4590 (2007)) |
| [3] | Bozzano, M.; Bruttomesso, R.; Cimatti, A.; Junttila, T. A.; Ranise, S.; van Rossum, P.; Sebastiani, R., Efficient theory combination via boolean search, Inf. Comput., 204, 1493-1525 (2006) · Zbl 1137.68578 |
| [4] | Bozzano, M.; Bruttomesso, R.; Cimatti, A.; Junttila, T. A.; van Rossum, P.; Schulz, S.; Sebastiani, R., The MathSAT 3 System, (Nieuwenhuis, R., CADE. CADE, LNCS, 3632 (2005)), 315-321 |
| [5] | Bruttomesso, R., A. Cimatti, A. Franzén, A. Griggio, A. Santuari and R. Sebastiani, To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in UF(E)LPAR; Bruttomesso, R., A. Cimatti, A. Franzén, A. Griggio, A. Santuari and R. Sebastiani, To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in UF(E)LPAR · Zbl 1165.68482 |
| [6] | Bruttomesso, R., A. Cimatti, A. Franzén, A. Griggio and R. Sebastiani, Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative AnalysisLPAR; Bruttomesso, R., A. Cimatti, A. Franzén, A. Griggio and R. Sebastiani, Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative AnalysisLPAR · Zbl 1165.68483 |
| [7] | Detlefs, D.; Nelson, G.; Saxe, J. B., Simplify: a theorem prover for program checking, J. ACM, 52, 365-473 (2005) · Zbl 1323.68462 |
| [8] | Dutertre, B.; de Moura, L., A Fast Linear-Arithmetic Solver for DPLL(T), (CAV’06. CAV’06, LNCS, 4144 (2006)), 81-94 |
| [9] | Dutertre, B.; de Moura, L., The Yices SMT Solver (2006) |
| [10] | Flanagan, C., R. Joshi and J.B. Saxe, An explicating theorem prover for quantified formulas; Flanagan, C., R. Joshi and J.B. Saxe, An explicating theorem prover for quantified formulas |
| [11] | Ganzinger, H.; Hagen, G.; Nieuwenhuis, R.; Oliveras, A.; Tinelli, C., DPLL(T): Fast decision procedures, (CAV’04. CAV’04, LNCS, 3144 (2004)), 175-188 · Zbl 1103.68616 |
| [12] | Nelson, G.; Oppen, D. C., Simplification by cooperating decision procedures, AC Transactions on Programming Languages and Systems, 1, 245-257 (1979) · Zbl 0452.68013 |
| [13] | Nieuwenhuis, R.; Oliveras, A., Fast Congruence Closure and Extensions, Inf. Comput., 2005, 557-580 (2007) · Zbl 1112.68116 |
| [14] | Nieuwenhuis, R.; Oliveras, A.; Tinelli, C., Solving SAT and SAT Modulo Theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T), J. ACM, 53, 937-977 (2006) · Zbl 1326.68164 |
| [15] | Oppen, D. C., Complexity, convexity and combinations of theories, Theor. Comput. Sci., 12, 291-302 (1980) · Zbl 0437.03007 |
| [16] | Rueß, H. and N. Shankar, Solving linear arithmetic constraints; Rueß, H. and N. Shankar, Solving linear arithmetic constraints |
| [17] | Sheini, H.M. and K.A. Sakallah, SMT(LU): a step toward scalability in system verificationICCAD; Sheini, H.M. and K.A. Sakallah, SMT(LU): a step toward scalability in system verificationICCAD |
| [18] | Shostak, R. E., Deciding combinations of theories, J. ACM, 31, 1-12 (1984) · Zbl 0629.68089 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
