Tags:Arrays, Satisfiability Modulo Theories and Sequences
Abstract:
The SMT (Satisfiability Modulo Theories) theory of arrays is well established and widely used, various decision procedures and extensions have been developed for it. However, recent works suggest that it is more efficient to develop tailored reasoning for some theories, such as sequences and strings, rather than reasoning over them through axiomatization over the theory of arrays. In this paper, we are interested in reasoning over n-indexed sequences as they are found in some programming languages such as Ada. We propose an SMT theory of n-indexed sequences, and we explore different ways to represent and reason over n-indexed sequences using existing theories, as well as tailored calculi for the theory.