Sequence theories are an extension of theories of strings with an infinite alphabet of letters, together with a corresponding alphabet theory (e.g. linear integer arithmetic). Sequences are natural abstractions of extendable arrays, which permit a wealth of operations including append, map, split, and concatenation. In spite of the growing amount of tool support for theories of sequences by leading SMT-solvers, little is known about the decidability of sequence theories, which is in stark contrast to the state of the theories of strings. We show that the decidable theory of strings with concatenation and regular constraints can be extended to the world of sequences over an alphabet theory that forms a Boolean algebra, while preserving decidability. In particular, decidability holds when regular constraints are interpreted as parametric automata (which extend both symbolic automata and variable automata), but fails when interpreted as register automata (even over the alphabet theory of equality). When length constraints are added, the problem is Turing-equivalent to word equations with length (and regular) constraints. Similar investigations are conducted in the presence of symbolic transducers, which naturally model sequence functions like map, split, filter, etc. We have developed a new sequence solver, SeCo, based on parametric automata, and show its efficacy on two classes of benchmarks: (i) invariant checking on array-manipulating programs and parameterized systems, and (ii) benchmarks on symbolic register automata.

翻译：序列理论是字符串理论的扩展，它使用无限字母表以及相应的字母表理论（例如线性整数算术）。序列是可扩展数组的自然抽象，支持附加、映射、拆分和连接等多种操作。尽管领先的SMT求解器对序列理论提供了越来越多的工具支持，但有关序列理论可判定性的研究仍然很少，这与字符串理论的研究现状形成鲜明对比。我们证明，具有连接和正则约束的可判定字符串理论可以扩展到字母表理论构成布尔代数的序列领域，同时保持可判定性。特别地，当正则约束被解释为参数自动机（它同时扩展了符号自动机和可变自动机）时，可判定性成立；但当被解释为寄存器自动机（即使是在相等性字母表理论上）时，可判定性不成立。当添加长度约束时，该问题在Turing等价意义上等价于带长度（和正则）约束的词方程。我们在存在符号换能器的情况下进行了类似的研究，符号换能器能自然地建模序列函数，如映射、拆分、过滤等。我们基于参数自动机开发了一个新的序列求解器SeCo，并在两类基准测试中展示了其有效性：(i) 数组操作程序和参数化系统的不变量检查，以及 (ii) 符号寄存器自动机的基准测试。