On SMT Theory Design: The Case of Sequences

TL;DR

A set of theory design criteria is defined to help determine what makes one variant of a theory better than another and a series of changes to the SMT theory of sequences are proposed as a contribution to the discussion regarding its standardization.

Abstract

Choices in the semantics and the signature of a theory are integral in determining how the theory is used and how challenging it is to reason over it. Our interest in this paper lies in the SMT theory of sequences. Various versions of it exist in the literature and in state-of-the-art SMT solvers, but it has not yet been standardized in the SMT-LIB. We reflect on its existing variants, and we define a set of theory design criteria to help determine what makes one variant of a theory better than another. The criteria we define can be used to appraise theory proposals for other theories as well. Based on these criteria, we propose a series of changes to the SMT theory of sequences as a contribution to the discussion regarding its standardization.

Figures (3)

• Figure 1: Comparison of the semantics of update in $\textsf{Seq}_{\textsf{cvc5}}$ and our proposal: the gray sequence is updated using the white sequence at different offsets.
• Figure 2: Signature of the proposed Sequence theory. The $^{*}$ after a symbol means that the symbol's semantics are as described in the previous subsection. The sequence sorts $\textsf{Seq}\xspace_1 ... \textsf{Seq}\xspace_n$ and $\textsf{Seq}\xspace'$ have elements of the sorts $\textsf{Elem}\xspace_1 ... \textsf{Elem}\xspace_n$ and $\textsf{Elem}\xspace'$ respectively.
• Figure 3: Fragment of the proposed theory of sequences and how its symbols can be reduced to those of $\textsf{Array}_{\textsf{c}}$. $\delta$ represents a default value of the same sort as the return value of $\textsf{nth}\xspace$, which is returned when $\textsf{nth}\xspace$ is applied outside its domain. $\_$ any value of the right sort.