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

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

SMT求解器作为程序验证、修复和合成的核心工具，其预处理中的公式简化直接影响效率。本文通过迭代搜索优化编译器配置，在大型基准测试中实现几何平均2.96倍于默认求解器、2.12倍于SLOT的速度提升，并验证机器学习可自动适配优化配置，较Z3和CVC5分别提升15%和54%。研究揭示了编译器优化与SMT简化的协同潜力，并提出多模态融合优化框架和动态配置存储器作为未来方向。

　　

摘要AI 摘要

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

了解更多登录

摘要

摘要

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

AI 摘要

AI 生成的摘要（实验性）

此摘要是使用自动化工具生成的，不是由文章作者撰写或审核的。它旨在帮助发现、帮助读者评估相关性，并协助来自相关研究领域的读者理解本文的工作。它旨在补充作者提供的摘要，后者仍然是论文的官方摘要。完整文章才是权威版本。点击此处了解更多。

点击 此处 对此摘要的准确性、清晰度和实用性进行评论。您的反馈将有助于改进未来的版本。

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