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

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

两种情况, 即原公式为 UNSAT, 或原公式为 SAT 但存在某个控制变量为 false, 而控制变量为 false 代表其对应的
逻辑公式中的项可能存在未解释函数 (即此时对该项的求解结果可能不可信), 于是需要对原公式重新检查, 对原
公式调用求解器, 当返回 UNSAT 时则没有问题, 最终结果为 UNSAT, 当返回 SAT 时, 即有可能出现我们所说未
解释函数造成“假反例”情况, 于是无法得到最终结果, 需要继续对递归函数进行展开, 然后重复上述过程.
该方法适用性有限且不完备, Pham 等人 [65,66] 对 Suter 等人 [32,64] 进行了扩展, 提出了一个对满足“广义充分满射
条件 (generalized sufficient subjectivity condition)”的 catamorphism 完备的基于展开的判定算法, 并将算法实现在开
源工具 RADA 中 [67] . 该方法的一个局限在于实际应用中, 证明所给的递归函数 (catamorphism) 满足广义充分满射
条件不是一个容易的事情, 另外这些工作中没有考虑组合理论问题, 因此提及的逻辑公式中的断言只有等式 (equality),
这些情况限制了该工作的实际应用范围.
CHC 递归函数求解技术: 2022 年 Govind 等人 [15] 将上述基于展开的方法发展到组合理论下带有递归定义的
CHC 问题求解中. 他们将包含递归函数的 CHC 公式进行预处理, 显式地定位出其中的递归函数定义, 然后对递归
函数使用基于递归定义展开的判定算法来进行求解, 并且结合 k-实例化 (k-instantiation) 和未解释函数抽象
(uninterpreted function abstraction) 技术来帮助提升递归定义求解效率. 这两种方法的主要思路是将递归函数进行
有限 k 步展开 (即进行 k 步实例化), 然后对剩下未展开的部分视作一个未解释函数, 这可以视作一种抽象方法, 减
少求解中的公式规模. 该算法实现在工具 Racer 中, 该工具的实现基于 CHC 求解器 Spacer 的求解框架. 这一方法
对于递归函数的处理主要是基于函数定义展开技术, 该技术的缺点在于无法进行自动的归纳推理, 从而可能无法
对许多必须通过归纳推理求解的命题完成自动验证. 那么在实际问题中, 没有归纳推理, 基于归纳不变式和递归函
数展开的 CHC 求解器与基于归纳推理的 SMT 求解器/自动定理证明器相比, 其求解表现究竟能达到什么程度? 在
第 5 节, 我们将收集和构造一个用于递归函数 SMT 求解问题的数据集, 对主流 CHC 求解器, SMT 求解器和自动
定理证明器进行统一实验对比.
5 实 验

我们对目前主流的开源求解器进行统一的实验比较, 以分析这些求解器在应对各种带有递归定义的一阶逻辑
公式时的求解能力. 用于实验的工具分为如下 3 类: 1) SMT 求解器, 包括 Z3 求解器和 cvc5 求解器. 2) 自动定理证
明器 Vampire. 3) CHC 求解器, 包括 Spacer、Eldarica 和 Racer. 用于实验比较的数据集主要分为两类, 一类是背景
理论为整数理论的递归函数问题, 这一类数据集的来源是 Vampire 相关文献 [55] 和我们手工构造. 另一类是背景理
论为 ADT 理论和整数理论混合的递归函数问题, 这一类数据集最早来源于 Reynolds 等人 [31] 为 CVC4 求解器引入
归纳推理的工作, 后续 ADT 和递归函数求解的相关文献 [12,15,47] 都选取了该数据集的部分样例进行实验.
下面我们先对用于实验比较的工具和相关参数进行介绍, 然后介绍用于实验比较的数据集和这些工具在数据
集上的运行结果.
5.1 工具介绍

Z3 求解器是被应用最广泛的 SMT 求解器之一, 通常作为各种程序验证、模型检测和符号执行工具的默认求
解引擎, 最早由微软研究院在 2008 年开发 [23] . 它支持多种背景理论的判定, 包括线性算术、位向量、数组、未解
释函数、ADT 等. 对于递归函数问题的求解, 当递归函数使用 define-fun-rec 定义时, Z3 将对递归函数定义进行展
开, 首先尝试在固定展开次数寻找可满足模型, 若由于展开次数限制导致不可满足, 则增长展开次数. Z3 中没有实
现归纳推理算法, 因此无法应对许多深层的递归函数性质证明问题. 在本文实验中调用 Z3 时直接使用默认设置,
不添加额外参数. 将 Z3 的实验效果作为在递归函数证明问题中的基准线 (baseline), 用于与其他实现了针对递归
函数求解算法的求解器进行对比.
cvc5 求解器 [24] 是 CVC 系列求解器的最新版本. CVC 求解器最初由斯坦福大学和纽约大学的研究团队联合
开发, 是学术界被广泛使用和研究的求解器之一. cvc5 求解器在 2021 年发布, 其主要开发团队来自斯坦福大学、
爱荷华大学和纽约大学等. 相比 Z3 求解器, 它的代码架构更模块化, 易于添加新理论; 并针对字符串、位向量、