Abstract
Satisfiability Modulo Theories (SMT) solvers have proven highly scalable, efficient and suitable for integrating theory reasoning. However, for numerous applications from program analysis and verification, the ground fragment is insufficient, as proof obligations often include quantifiers. A well known approach for quantifier reasoning uses a matching algorithm that works against an E-graph to instantiate quantified variables. This paper introduces algorithms that identify matches on E-graphs incrementally and efficiently. In particular, we introduce an index that works on E-graphs, called E-matching code trees that combine features of substitution and code trees, used in saturation based theorem provers. E-matching code trees allow performing matching against several patterns simultaneously. The code trees are combined with an additional index, called the inverted path index, which filters E-graph terms that may potentially match patterns when the E-graph is updated. Experimental results show substantial performance improvements over existing state-of-the-art SMT solvers.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175–188. Springer, Heidelberg (2004)
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005)
Barrett, C., Berezin, S.: CVC Lite: A New Implementation of the Cooperating Validity Checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, Springer, Heidelberg (2004)
Moskal, M., Lopuszański, J.: Fast quantifier reasoning with lazy proof explication (2006), http://nemerle.org/~malekith/smt/smt-tr-1.pdf
Flanagan, C., Joshi, R., Saxe, J.B.: An explicating theorem prover for quantified formulas. Technical Report HPL-2004-199, HP Laboratories, Palo Alto (2004)
Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)
Ball, T., Lahiri, S.K., Musuvathi, M.: Zap: Automated theorem proving for software analysis. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 2–22. Springer, Heidelberg (2005)
Nelson, G.: Techniques for program verification. Technical Report CSL81-10, Xerox Palo Alto Research Center (1981)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: PLDI, pp. 234–245 (2002)
DeLine, R., Leino, K.R.M.: BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report 2005-70, Microsoft Research (2005)
Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)
Kozen, D.: Complexity of finitely presented algebras. In: STOC, pp. 164–177 (1977)
Slagle, J.R.: Automatic theorem proving with built-in theories including equality, partial ordering, and sets. J. of the ACM 19(1), 120–135 (1972)
Stickel, M.E.: Automated deduction by theory resolution. J. Autom. Reasoning 1(4), 333–355 (1985)
Baalen, J.V., Roach, S.: Using decision procedures to accelerate domain-specific deductive synthesis systems. In: Flener, P. (ed.) LOPSTR 1998. LNCS, vol. 1559, pp. 61–82. Springer, Heidelberg (1999)
Waldmann, U., Prevosto, V.: SPASS+T. In: ESCoR, pp. 18–33 (2006)
Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: On a rewriting approach to satisfiability procedures: Extension, combination of theories and an experimental appraisal. In: Gramlich, B. (ed.) Frontiers of Combining Systems. LNCS (LNAI), vol. 3717, pp. 65–80. Springer, Heidelberg (2005)
de Moura, L., Bjørner, N.: Efficient E-matching for SMT solvers. Technical report, Microsoft Research (to appear)
Aït-Kaci, H.: Warren’s abstract machine: a tutorial reconstruction. MIT Press, Cambridge (1991)
Voronkov, A.: The anatomy of vampire implementing bottom-up procedures with code trees. J. Autom. Reasoning 15(2), 237–265 (1995)
Riazanov, A., Voronkov, A.: Vampire 1.1 (system description). In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 376–380. Springer, Heidelberg (2001)
Graf, P., Meyer, C.: Advanced indexing operations on substitution trees. In: McRobbie, M.A., Slaney, J.K. (eds.) Automated Deduction - Cade-13. LNCS, vol. 1104, pp. 553–567. Springer, Heidelberg (1996)
Ganzinger, H., Nieuwenhuis, R., Nivela, P.: Context trees. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 242–256. Springer, Heidelberg (2001)
Bloom, B.H.: Space/time trade-offs in hash coding with allowable errors. Commun. ACM 13(7), 422–426 (1970)
Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Automation of Reasoning 2: Classical Papers on Computational Logic, pp. 466–483. Springer, Heidelberg (1983)
Leino, K.R.M., Musuvathi, M., Ou, X.: A two-tier technique for supporting quantifiers in a lazily proof-explicating theorem prover. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, Springer, Heidelberg (2005)
Ranise, S., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2006), http://www.SMT-LIB.org
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Moura, L., Bjørner, N. (2007). Efficient E-Matching for SMT Solvers. In: Pfenning, F. (eds) Automated Deduction – CADE-21. CADE 2007. Lecture Notes in Computer Science(), vol 4603. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73595-3_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-73595-3_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73594-6
Online ISBN: 978-3-540-73595-3
eBook Packages: Computer ScienceComputer Science (R0)