An instantiation scheme for satisfiability modulo theories. (English) Zbl 1430.68401
Summary: State-of-the-art theory solvers generally rely on an instantiation of the axioms of the theory, and depending on the solvers, this instantiation is more or less explicit. This paper introduces a generic instantiation scheme for solving SMT problems, along with syntactic criteria to identify the classes of clauses for which it is complete. The instantiation scheme itself is simple to implement, and we have produced an implementation of the syntactic criteria that guarantee a given set of clauses can be safely instantiated. We used our implementation to test the completeness of our scheme for several theories of interest in the SMT community, some of which are listed in the last section of this paper.
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
References:
| [1] | Abadi, A., Rabinovich, A., Sagiv, M.: Decidable fragments of many-sorted logic. J. Symb. Comput. 45(2), 153–172 (2010) · Zbl 1183.03007 · doi:10.1016/j.jsc.2009.03.003 |
| [2] | Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log. 10(1), 129–179 (2009) · doi:10.1145/1459010.1459014 |
| [3] | Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Inf. Comput. 183(2), 140–164 (2003) · Zbl 1054.68077 · doi:10.1016/S0890-5401(03)00020-8 |
| [4] | Baader, F., Snyder, W.: Unification theory. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, chapter 8, pp. 445–532. Elsevier Science (2001) · Zbl 1011.68126 |
| [5] | Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 3(4), 217–247 (1994) · Zbl 0814.68117 · doi:10.1093/logcom/4.3.217 |
| [6] | Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, chapter 26, pp. 825–885. IOS Press (2009) |
| [7] | Barrett, C.W., Dill, D.L., Stump, A.: Checking satisfiability of first-order formulas by incremental translation to sat. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 236–249. Springer (2002) · Zbl 1010.68531 |
| [8] | Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: A write-based solver for sat modulo the theory of arrays. In: FMCAD ’08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, pp. 1–8. IEEE Press, Piscataway, NJ, USA (2008) |
| [9] | Bonacina, M.P., Echenim, M.: On variable-inactivity and polynomial T-satisfiability procedures. J. Log. Comput. 18(1), 77–96 (2008) · Zbl 1144.03007 · doi:10.1093/logcom/exm055 |
| [10] | Bonacina, M.P., Echenim, M.: Theory decision by decomposition. J. Symb. Comput. 45(2), 229–260 (2010) · Zbl 1192.68626 · doi:10.1016/j.jsc.2008.10.008 |
| [11] | Bonacina, M.P., Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Decidability and undecidability results for Nelson–Oppen and rewrite-based decision procedures. In: Furbach, U., Shankar, N. (eds.) Proc. IJCAR-3. LNAI, vol. 4130, pp. 513–527. Springer (2006) · Zbl 1222.03011 |
| [12] | Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification. Springer-Verlag New York, Inc., Secaucus, NJ, USA (2007) · Zbl 1126.03001 |
| [13] | Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) Proc. VMCAI-7. LNCS, vol. 3855, pp. 427–442. Springer (2006) · Zbl 1176.68116 |
| [14] | Dantzig, G.B., Eaves, B.C.: Fourier-motzkin elimination and its dual. J. Comb. Theory, Ser. A 14(3), 288–297 (1973) · Zbl 0258.15010 · doi:10.1016/0097-3165(73)90004-6 |
| [15] | Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Commun. ACM 5, 394–397 (1962) · Zbl 0217.54002 · doi:10.1145/368273.368557 |
| [16] | Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960) · Zbl 0212.34203 · doi:10.1145/321033.321034 |
| [17] | de Moura, L., Bjørner, N.: Engineering DPLL(T) + saturation. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR-4. LNAI, vol. 5195, pp. 475–490. Springer (2008) · Zbl 1165.68479 |
| [18] | de Moura, L., Bjørner, N.: Efficient e-matching for SMT solvers. In: Pfenning, F. (ed.) CADE-21. LNCS, vol. 4603, pp. 183–198. Springer (2007) · Zbl 1213.68578 |
| [19] | de Moura, L.M., Bjørner, N.: Generalized, efficient array decision procedures. In: FMCAD, pp. 45–52. IEEE (2009) |
| [20] | de Moura, L.M., Bjørner, N.: Efficient e-matching for SMT solvers. In: Pfenning, F. (ed.) 21st International Conference on Automated Deduction. LNCS, vol. 4603, pp. 183–198. Springer (2007) · Zbl 1213.68578 |
| [21] | Detlefs, D.L., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005) · Zbl 1323.68462 · doi:10.1145/1066100.1066102 |
| [22] | Dutertre, D., de Moura, L.: The YICES SMT-solver. In: SMT-COMP: satisfiability modulo theories competition. Available at http://yices.csl.sri.com (2006) |
| [23] | Echenim, M., Peltier, N.: Instantiation of SMT problems modulo integers. In: AISC 2010 (10th International Conference on Artificial Intelligence and Symbolic Computation). LNCS. Springer (2010) · Zbl 1286.68397 |
| [24] | Ganzinger, H., Korovin, K.: Integrating equational reasoning into instantiation-based theorem proving. In: Computer Science Logic (CSL’04), LNCS, vol. 3210, pp. 71–84. Springer (2004) · Zbl 1095.68111 |
| [25] | Ge, Y., Barrett, C.W., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. Ann. Math. Artif. Intell. 55(1–2), 101–122 (2009) · Zbl 1184.68461 · doi:10.1007/s10472-009-9153-6 |
| [26] | Ge, Y., de Moura, L.M.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306–320. Springer (2009) · Zbl 1242.68280 |
| [27] | Goel, A., Krstić, S., Fuchs, A.: Deciding array formulas with frugal axiom instantiation. In: SMT ’08/BPR ’08: Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning, pp. 12–17. ACM, New York, NY, USA (2008) |
| [28] | Jacobs, S.: Incremental instance generation in local reasoning. In: Baader, F., Ghilardi, S., Hermann, M., Sattler, U., Sofronie-Stokkermans, V. (eds.) Notes 1st CEDAR Workshop, IJCAR 2008, pp. 47–62 (2008) |
| [29] | Jouannaud, J., Kirchner, C.: Solving equations in abstract algebras: a rule based survey of unification. In: Lassez, J.-L., Plotkin, G. (eds.) Essays in Honor of Alan Robinson, pp. 91–99. MIT Press (1991) |
| [30] | Kirchner, C., Kirchner, H., Rusinowitch, M.: Deduction with symbolic constraints. Revue Française d’Intelligence Artificielle 4(3), 9–52 (1990) |
| [31] | Kirchner, H., Ranise, S., Ringeissen, C., Tran, D.-K.: Automatic combinability of rewriting-based satisfiability procedures. In: Hermann, M., Voronkov, A. (eds.) Proc. LPAR-13. LNCS, vol. 4246, pp. 542–556. Springer (2006) · Zbl 1165.68490 |
| [32] | Lee, S., Plaisted, D.A.: Eliminating duplication with the hyper-linking strategy. J. Autom. Reason. 9, 25–42 (1992) · Zbl 0784.68077 · doi:10.1007/BF00247825 |
| [33] | Lynch, C., Tran, D.-K.: Automatic decidability and combinability revisited. In: Pfenning, F. (ed.) CADE-21. LNAI, vol. 4603, pp. 328–344. Springer (2007) · Zbl 1213.68573 |
| [34] | Plaisted, D.A., Zhu, Y.: Ordered semantic hyperlinking. J. Autom. Reason. 25(3), 167–217 (2000) · Zbl 0959.68115 · doi:10.1023/A:1006376231563 |
| [35] | Ranise, S., Deharbe, D.: Applying light-weight theorem proving to debugging and verifying pointer programs. In: Proc. of the 4th Workshop on First-order Theorem Proving (FTP’03). Electronic Notes in Theoretical Computer Science, vol. 86 (2003) · Zbl 1261.68106 |
| [36] | Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.: A decision procedure for an extensional theory of arrays. In: LICS ’01: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p. 29. IEEE Computer Society, Washington, DC, USA (2001) |
| [37] | Waldmann, U., Prevosto, V.: SPASS+T. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) Proc. ESCoR Workshop, FLoc 2006. CEUR Workshop Proceedings, vol. 192, pp. 18–33 (2006) |
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.
