deciding array formulas with frugal axiom instantiation
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.
decision procedures the theory of arrays satisfiability modulo theories