一句话:扩展自适应模式匹配自动机以支持非线性模式,通过交错变量一致性检查与匹配来减少匹配步骤。
高效模式匹配是项重写引擎的基础。将模式预处理为有限确定性自动机,可在单次遍历输入项的相关部分后判定匹配。多数基于自动机的方法局限于线性模式(每个变量至多出现一次),并需额外的后处理步骤来检查变量一致性。本文表明,将变量一致性检查与模式匹配阶段交错进行可减少找到所有匹配所需的步骤。为此,我们在Sekar等人提出的自适应模式匹配自动机基础上扩展了一致性检查。我们证明所得确定性模式匹配自动机是正确的,并给出若干示例展示可实现的步骤缩减。
Efficient pattern matching is fundamental for practical term rewrite engines. By preprocessing the given patterns into a finite deterministic automaton the matching patterns can be decided in a single traversal of the relevant parts of the input term. Most automaton-based techniques are restricted to linear patterns, where each variable occurs at most once, and require an additional post-processing step to check so-called variable consistency. However, we can show that interleaving the variable consistency and pattern matching phases can reduce the number of required steps to find all matches. Therefore, we take the existing adaptive pattern matching automata as introduced by Sekar et al and extend these with consistency checks. We prove that the resulting deterministic pattern matching automaton is correct, and show several examples where some reduction can be achieved.