Reductions for Strings and Regular Expressions Revisited
Reductions for Strings and Regular Expressions Revisited
复制标题
DOI：
10.34727/2020/isbn.978-3-85448-042-6_30
复制
发表时间：
2020-09
期刊：
影响因子：
--
通讯作者：
Andrew Reynolds;Andres Nötzli;Clark W. Barrett;C. Tinelli
中科院分区：
文献类型：
--
作者：
Andrew Reynolds;Andres Nötzli;Clark W. Barrett;C. Tinelli
形式方法中的求解器支持的字符串理论包含了大量的算子。字符串解算器通常将运算符简化为核心片段，并在该片段上实现半判定过程，而不是实现直接对所有运算符进行推理的半判定过程。这些削减大大增加了限制条件的数量，因此必须谨慎行事才能取得良好的业绩。我们提出了从正则表达式到字符串约束的新的约简，并提出了一个框架来最小化当前字符串约束约简中引入的新变量。正则表达式约束的减少使字符串解算器能够处理此类约束的重要片段，而无需对正则表达式使用专门的推理。最小化减少的约束中的变量数量使核心求解器求解这些约束的成本大大降低。对我们在CVC4中实现这两种技术的实验评估表明，它们显著提高了求解器的性能。CVC4是一种最先进的SMT求解器，它广泛支持字符串理论。
The theory of strings supported by solvers in formal methods contains a large number of operators. Instead of implementing a semi-decision procedure that reasons about all the operators directly, string solvers often reduce operators to a core fragment and implement a semi-decision procedure over that fragment. These reductions considerably increase the number of constraints and thus have to be done carefully to achieve good performance. We propose novel reductions from regular expressions to string constraints and a framework for minimizing the introduction of new variables in current reductions of string constraints. The reductions of regular expression constraints enable string solvers to handle a significant fragment of such constraints without using dedicated reasoning over regular expressions. Minimizing the number of variables in the reduced constraints makes those constraints significantly cheaper to solve by the core solver. An experimental evaluation of our implementation of both techniques in cvc4, a state-of-the-art SMT solver with extensive support for the theory of strings, shows that they significantly improve the solver's performance.