Synthesiz3 This：基于SMT的不可计算符号合成方法
计算机科学中的逻辑
2025-08-19 v3
摘要
程序合成是自动构造符合给定规范的程序的任务。本文聚焦于在存在不可计算符号（即用于规范但不允许出现在结果函数中的符号）的规范下，合成符合规范的单调用递归自由函数。我们通过SMT求解方法来处理该问题：我们提出了一种基于模型投影的量子消除算法，用于总函数和部分函数的合成，适用于无解释函数和线性算术理论及其组合。在此基础上，我们还扩展了模型投影，以为这些理论提供证据。进一步，我们针对唯一确定解的情况提供了量身定制的程序。我们使用SMT求解器Z3实现了算法的原型，展示了其相对于当前最先进技术的实际效率。
引用
@article{arxiv.2504.16536,
title = {Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols},
author = {Petra Hozzová and Nikolaj Bjørner},
journal= {arXiv preprint arXiv:2504.16536},
year = {2025}
}
备注
This is the version of this paper accepted for FMCAD 2025