Lemmas on Demand for the Extensional Theory of Arrays

Abstract

The quantifier-free extensional theory of arrays ${\mathit{T}}_{\mathit{A}}$ plays an important role in hardware and software verification. In this article we present a novel decision procedure that refines formula abstractions with lemmas on demand. We consider the case where ${\mathit{T}}_{\mathit{A}}$ is combined with a decidable quantifier-free first-order theory ${\mathit{T}}_{\mathit{B}}$ . Unlike traditional lazy SMT approaches, where lemmas are added on the boolean abstraction layer, our decision procedure adds lemmas in ${\mathit{T}}_{\mathit{B}}$ . We discuss our decision procedure in detail. In particular, we prove soundness and completeness, and discuss complexity. We present our decision procedure in a generic context and provide implementation details and optimizations, in particular for bit-vectors. Finally, we report on experiments and discuss related work.