Weakly Equivalent Arrays

TL;DR

This paper introduces a lazy instantiation algorithm for the theory of arrays that improves decision procedures by focusing on weak equivalence classes, simplifying lemma interpolation and maintaining correctness.

Contribution

It presents a novel algorithm that lazily instantiates lemmas based on weak equivalence classes, enhancing decision procedures for array theories.

Findings

Algorithm correctly decides array theory satisfiability

Lemmas based on weak equivalence are easier to interpolate

Maintains completeness while reducing instantiation complexity

Abstract

The (extensional) theory of arrays is widely used to model systems. Hence, efficient decision procedures are needed to model check such systems. Current decision procedures for the theory of arrays saturate the read-over-write and extensionality axioms originally proposed by McCarthy. Various filters are used to limit the number of axiom instantiations while preserving completeness. We present an algorithm that lazily instantiates lemmas based on weak equivalence classes. These lemmas are easier to interpolate as they only contain existing terms. We formally define weak equivalence and show correctness of the resulting decision procedure.