基于编译器优化的SMT简化技术：一项深入研究

《ACM Transactions on Software Engineering and Methodology》：Compiler Optimization-Based SMT Simplifications: An In-Depth Study

SMT求解器作为程序验证、修复和合成等领域的核心工具，其预处理中的公式简化直接影响效率。现有方法依赖人工设计启发式，而基于编译器优化的自动化方法仍有提升空间。本文通过迭代搜索优化配置，在大型基准测试中实现较默认求解器2.96倍、SLOT方法2.12倍的加速，并验证机器学习能自动选择最优配置，较Z3和CVC5分别提升15%和54%，最后探讨了编译器优化驱动的SMT简化的未来方向。

　　

摘要AI摘要

要查看此由AI生成的摘要，您必须具有高级访问权限。

了解更多登录

摘要

摘要

符号模型（SMT）求解器在许多领域中都是基础工具，例如程序验证、修复和综合。虽然公式简化是一个直接影响求解器效率的关键预处理步骤，但现有的方法主要依赖于手工制作的启发式规则。最近的进展探索了使用编译器优化来自动化和增强公式简化。尽管这些方法具有潜力，但编译器优化与SMT简化之间的协同作用仍没有得到充分理解和利用。本文全面研究了编译器优化与SMT公式简化之间的相互作用。我们发现，通过迭代搜索优化配置可以显著提高公式简化的效果，在大规模基准测试中，与默认求解器相比，速度提升了2.96倍；与SLOT相比，速度提升了2.12倍。我们还提供了强有力的证据，证明基于机器学习的方法在自动化选择针对特定问题实例的优化配置方面非常有效，在Z3上速度提升了1.15倍，在CVC5上速度提升了1.54倍。最后，我们讨论了提高编译器优化驱动的SMT简化方法适用性和效果的一些有前景的方向。

AI摘要

要查看此由AI生成的纯文本摘要，您必须具有高级访问权限。