Case split is a core proof rule in current decision procedures for the theory of string constraints. Its use is the primary cause of the state space explosion in string constraint solving, since it is the only rule that creates branches in the proof tree. Moreover, explicit handling of the case split rule may cause recomputation of the same tasks in multiple branches of the proof tree. In this paper, we propose a symbolic algorithm that significantly reduces such a redundancy. In particular, we encode a string constraint as a regular language and proof rules as rational transducers. This allows us to perform similar steps in the proof tree only once, alleviating the state space explosion. We also extend the encoding to handle arbitrary Boolean combinations of string constraints, length constraints, and regular constraints. In our experimental results, we validate that our technique works in many practical cases where other state-of-the-art solvers fail to provide an answer; our Python prototype implementation solved over 50 % of string constraints that could not be solved by the other tools.

翻译：情形分裂是当前字符串约束理论决策过程中的核心证明规则。由于它是证明树中唯一会产生分支的规则，其使用是导致字符串约束求解中状态空间爆炸的主要原因。此外，情形分裂规则的显式处理可能导致在证明树的多个分支中重复计算相同的任务。本文提出了一种能显著降低此类冗余的符号算法。具体而言，我们将字符串约束编码为正则语言，将证明规则编码为有理变换器。这使得我们能够将证明树中的相似步骤仅执行一次，从而缓解状态空间爆炸问题。我们还扩展了该编码以处理字符串约束、长度约束和正则约束的任意布尔组合。实验结果表明，我们的技术能够在许多其他先进求解器无法给出答案的实际案例中有效工作；我们基于Python的原型实现成功求解了超过50%的其他工具无法求解的字符串约束。