An SMT Theory for n-Indexed Sequences

TL;DR

This paper introduces a new SMT theory specifically for n-indexed sequences, aiming to improve reasoning efficiency over sequences in programming languages like Ada by exploring various representations and calculi.

Contribution

It proposes a novel SMT theory for n-indexed sequences and investigates different methods for representing and reasoning about them, tailored for programming language applications.

Findings

Developed a new SMT theory for n-indexed sequences.

Explored multiple representations and reasoning techniques.

Enhanced reasoning efficiency for sequence-based problems.

Abstract

The SMT (Satisfiability Modulo Theories) theory of arrays is well-established and widely used, with variousdecision procedures and extensions developed for it. However, recent works suggest that developing tailoredreasoning for some theories, such as sequences and strings, is more efficient than reasoning over them throughaxiomatization over the theory of arrays. In this paper, we are interested in reasoning over n-indexed sequences asthey are found in some programming languages, such as Ada. We propose an SMT theory of n-indexed sequencesand explore different ways to represent and reason over n-indexed sequences using existing theories, as well astailored calculi for the theory.