Page 58 - 《软件学报》2026年第2期

冯维直 等: 带递归定义的 SMT 公式求解技术综述 537

ADT 和整数混合理论样例的结果如表 6 所示.
待证明的 168 个样例结果显示, 现有求解器则表现均一般. 基于 SMT 求解和归纳推理算法的求解器 (Z3/
cvc5/Vampire) 中求解数最多的工具是 cvc5, 可求解数为 74/168=44.05%. 而相比整数样例, CHC 求解器在 ADT 样
例上的表现较差. 其中求解数最多的工具是 Racer, 它实现了专门针对 ADT 和递归函数的求解算法, 但只能求解
出 39/168=23.21% 的样例. 其原因可能是待证明样例较为依赖归纳推理进行证明, 而当前 CHC 求解器算法中无法
进行自动归纳推理. 另外 CHC 求解器的理论判定算法也无法较好地处理包含 ADT 的问题, 对于复杂的 ADT 理
论样例无法求解出用于证明性质的归纳不变式.

表 6 ADT 和整数混合理论样例不同求解器实验结果

样例类别 总数 Z3 cvc5 Vampire Spacer Racer Eldarica
待证明样例 168 12 74 (44.05%) 51 4 39 (23.21%) 12
性质不成立样例 83 47 32 0 83 81 83
总解出数 251 59 106 51 87 120 95
结果显示, 在性质不成立样例上 CHC 求解器几乎均可以求解全部例子. 这可能得益于 CHC 求解算法中求解
归纳不变式的计算框架. 如 IC3/PDR 框架本身就是模型检测问题中求解反例最优算法之一. 而相比之下, 尽管
SMT 求解器中实现了对递归函数进行有限模型寻找的技术 [50] , 能够求解一部分性质不成立样例, 但它搜索可满足
模型的算法没有更进一步进行专门优化, 从而求解效率远低于 CHC 求解器. 实验中 SMT 求解器 Z3 和 cvc5 需要
对输入文件中定义递归函数的形式进行预处理, 然后调用有限模型寻找方法 (--fmf-fun 参数), 但只能求解 47/83=
56.63% 和 32/83=38.55% 的样例. 自动定理证明器 Vampire 则无法求解出任何样例. 这是由于自动定理证明器没
有实现任何专用于递归函数问题可满足性求解的推理技术, 且相比之下推理系统更适合也更关注进行“证明”任务.
需要注意的是实验发现若 SMT 求解器不开启模型寻找算法, 会和 Vampire 一样无法求解任何问题. 从这一角度来
看, Reynolds 等人在文献 [50] 中提出的递归函数模型寻找算法在帮助 SMT 求解器应对带有递归函数的性质不成
立问题时具有重要作用但有待进一步优化和提升. 另外, 在部分关注 ADT 和递归函数求解的相关文献中 [13,15] , 作
者同样运行 SMT 求解器 Z3 和 cvc5 与 CHC 求解器进行了实验比较, 但文中实验结果显示 SMT 求解器无法解出
任何样例. 实际上这是由于它们没有开启 SMT 求解器的递归函数模型寻找算法.
从 ADT 和整数混合理论样例的实验结果中, 我们可以得出如下结论: 1) 归纳推理技术的使用具有较好的效
果, cvc5 和 Vampire 在开启归纳增强选项后能求解的例子数相比不支持归纳推理的 SMT 求解器 Z3 具有较大优
势, 但依然有超过一半的例子无法被求解, 因此现有求解工具都具有很大提升空间. 求解能力不足的主要原因可能
是由于现有求解器中实现的引理生成技术难以处理长度较大、结构复杂的 ADT 公式, 需要研究更高效的引理生
成算法. 2) SMT 求解器中实现归纳推理增强的 cvc5 求解器, 相比在推理系统中引入归纳推理增强的 Vampire 具
有更好的效果, 其原因可能是 SMT 求解器对 ADT 理论以及混合理论问题的支持更好, 集成了更丰富的优化和求
解算法. 3) CHC 求解算法在 ADT 理论问题的“证明”任务上求解能力有限, 但在“找错”任务上具有很好的效果. 可
能是由于 CHC 求解器对 ADT 理论判定方法的支持还不够成熟. 且 CHC 求解器中仅靠归纳不变式生成和基于展
开的递归函数求解算法来进行验证, 无法替代基于自动归纳推理的验证算法.
两类求解算法对比如下.
值得一提的是, 对于性质证明问题, 尽管单一求解器的求解能力有限, 且 CHC 求解器相比 Z3/cvc5/Vampire 求
解效果稍弱. 但如果考虑每一个样例被任意工具求解的情况, 我们发现 CHC 工具的求解能力可以与其他工具互为
补充. SMT 求解器 (Z3/cvc5) 和自动定理证明器 (Vampire) 主要基于从前提公理推导出性质取反不成立的反证法
思想, 来进行待证明 SMT 问题的求解, 然后通过归纳推理技术处理递归函数; CHC 求解器则主要通过生成可推导
出安全性质成立的归纳不变式等模型检测思想, 来进行待证明 CHC 问题的求解, 然后通过递归函数展开和抽象方
法来处理递归函数. 在表 7 中我们分别统计了这两类求解器在待证明样例上的综合求解效果 (即只考虑前文所述
所有实验样例中排除掉 83 个性质不成立样例的问题). 对每一个样例, 若它能被 Z3/cvc5/Vampire 中任意求解器求