Deciding array formulas with frugal axiom instantiation

ABSTRACT

How to efficiently reason about arrays in an automated solver based on decision procedures? The most efficient SMT solvers of the day implement "lazy axiom instantiation": treat the array operations read and write as uninterpreted, but supply at appropriate times appropriately many---not too many, not too few---instances of array axioms as additional clauses. We give a precise account of this approach, specifying "how many" is enough for correctness, and showing how to be frugal and correct.

References

1. Decision Procedure Toolkit. www.sourceforge.net/projects/DPT, 2008.
2. A. Armando, S. Ranise, and M. Rusinowitch. A rewriting approach to satisfiability procedures. Inf. Comput., 183(2):140--164, 2003.
3. C. Barrett and S. Berezin. CVC Lite: A new implementation of the cooperating validity checker. In Computer Aided Verification (CAV), vol. 3114 of LNCS, pp. 515--518. Springer, 2004.
4. C. Barrett, R. Nieuwenhuis, A. Oliveras, and C. Tinelli. Splitting on demand in SAT Modulo Theories. In Logic for Programming, Artificial Intelligence and Reasoning (LPAR), vol. 4246 of LNCS, pp. 512--526. Springer, 2006.
5. C. Barrett, S. Ranise, A. Stump, and C. Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org, 2008.
6. M. Bozzano et al. Efficient theory combination via boolean search. Inf. Comput., 204(10):1493--1525, 2006.
7. A. R. Bradley, Z. Manna, and H. B. Sipma. What's decidable about arrays? In Verification, Model Checking, and Abstract Interpretation: (VMCAI), vol. 3855 of LNCS, pp. 427--442. Springer, 2006.
8. R. Bryant, S. Lahiri, and S. Seshia. Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In Computer Aided Verification (CAV), vol. 2404 of LNCS, pp. 78--92. Springer, 2002.
9. D. Detlefs, G. Nelson, and J. B. Saxe. Simplify: A theorem prover for program checking. Journal of the ACM, 52(3):365--473, 2005.
10. B. Dutertre and L. de Moura. The YICES SMT solver. Technical report, SRI International, 2006.
11. L. de Moura and N. Bjørner. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), vol. 4963 of LNCS, pp. 337--340. Springer, 2008.
12. S. Ghilardi, E. Nicolini, S. Ranise, and D. Zucchelli. Decision procedures for extensions of the theory of arrays. Annals of Mathematics and Artificial Intelligence, 50(3--4):231--254, 2007.
13. D. Kapur and C. G. Zarba. A reduction approach to decision procedures. Technical Report TR-CS-1005-44, University of New Mexico, 2005.
14. S. Krstić and A. Goel. Architecting solvers for SAT Modulo Theories: Nelson-Oppen with DPLL. In FroCoS, vol. 4720 of LNCS, pp. 1--27. Springer, 2007.
15. S. Krstić, A. Goel, J. Grundy, and C. Tinelli. Combined satisfiability modulo parametric theories. In TACAS, vol. 4424 of LNCS, pp. 602--617. Springer, 2007.
16. S. Lahiri and S. Qadeer. Back to the future: revisiting precise program verification using SMT solvers. SIGPLAN Not., 43(1):171--182, 2008.
17. G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245--257, 1979.
18. R. Nieuwenhuis, A. Oliveras, and C. Tinelli. Solving SAT and SAT Modulo Theories: from an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T). Journal of the ACM, 53(6):937--977, Nov. 2006.
19. R. Sebastiani. Lazy satisfiability modulo theories. Journal on Satisfiability, Boolean Modeling and Computation (JSAT), 3:141--224, 2007.
20. A. Stump, D. L. Dill, C. W. Barrett, and J. Levitt. A decision procedure for an extensional theory of arrays. In Logic in Computer Science: 16th IEEE Symposium, LICS, pp. 29--37. IEEE Press, 2001.

Index Terms

• Theory of computation

  • Logic

  • Models of computation

    • Computability