通过“生成式平等饱和度”（Generative Equality Saturation）支持的方法，验证SMT重写器（SMT Rewriters）在重写空间探索（Rewrite Space Exploration）中的有效性

《Proceedings of the ACM on Programming Languages》：Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative Equality Saturation

SMT求解器重写系统验证方法研究：提出Aries工具，结合模仿突变与演绎重写技术，有效探索并验证重写空间，在Z3和cvc5中检测到27个新问题（22个已解决），重点解决重写系统验证难题。

　　

摘要

可满足性模理论（SMT）求解器被广泛用于程序分析和其他需要自动化推理的应用领域。作为SMT求解器的关键组成部分，重写系统负责简化并转换公式以优化求解过程。SMT求解器的有效性在很大程度上取决于其重写系统的稳健性，因此对其验证至关重要。尽管SMT求解器测试方面取得了持续进展，但重写系统的验证仍然是一个尚未充分探索的领域。我们的实证分析表明，开发人员在确保重写系统的正确性和可靠性方面投入了大量精力。然而，现有的测试技术并未充分解决这一问题。在本文中，我们介绍了一种名为Aries的新技术，用于验证SMT求解器的重写系统。首先，Aries采用了一种称为“模拟变异”的策略，该策略主动重塑输入公式以引发和多样化重写机会。通过将变异后的术语与已知的重写模式进行匹配，Aries可以在后续阶段对重写空间进行彻底探索。其次，Aries利用演绎重写技术，结合生成性等式饱和算法来有效探索重写空间，并生成语义等价的变异体以用于验证。我们将Aries实现为一个实用的验证工具，并在包括Z3和cvc5在内的主流SMT求解器上对其进行了评估。实验结果表明，Aries能够有效识别错误，共发现了27个新问题，其中22个问题已被开发者确认或修复。这些问题大多与重写系统相关，凸显了Aries在探索重写空间方面的强大能力。