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

510 软件学报 2026 年第 37 卷第 2 期

行表示, 通常是如下方式 (涉及的例子和细节详见第 1.5 节): 在 SMTLIB 标准格式中, 使用 declare-fun 声明函数
名, 然后用带有全称量词和未解释函数 (uninterpreted function, UF) 的公理断言来表示函数体. 从 2016 年开始,
SMTLIB 支持通过 define-fun-rec 的关键字直接定义递归函数, 主流 SMT 求解器比如 Z3 和 cvc5 在识别到输入带
有 define-fun-rec 的函数定义时, 会采取一些特定求解策略. 验证目标被取反作为一条 assert 语句, SMT 求解器求
解返回不可满足, 则认为验证目标得证. 两种方式在语义上可以认为是等价的.
通用的一阶逻辑公式求解框架: 现有的一阶逻辑公式自动求解工具在求解带有背景理论的一阶逻辑公式时,
通常是将可满足性判定算法和特定背景理论的求解技术相结合, 主要的一阶逻辑公式可满足性判定框架如下.
1) 影响力最大, 使用最广泛的是 SMT 求解器, 一般基于 DPLL (Davis-Putnam-Logemann-Loveland) 判定算法,
用于求解带背景理论的主流算法是 DPLL(T) 算法. 该算法求解原理是先不考虑背景理论, 将 SMT 公式视作 SAT
公式进行求解, 可满足时需再结合背景理论求解器验证解的相容性.
除 SMT 求解器外, 自动定理证明工具和 CHC 求解器同样可以进行一阶逻辑公式的求解, 现在主流的定理证
明工具通常可以直接读入 SMTLIB 格式的 SMT 公式作为输入, 而 CHC 求解器则需要先将 SMT 公式转换成 CHC
形式再进行输入. 本文将不局限于 SMT 求解器, 还会介绍基于自动定理证明器和 CHC 求解器来处理带递归函数
SMT 问题的方法和工具.
2) 自动定理证明器一般基于 superposition 推理系统, 通过 saturation-based proof search 的证明框架来推导目
标公式的可满足性. 对带有背景理论的一阶逻辑公式进行推理, 一般是将背景理论公理作为推理规则加入推理系
统中. 用于推理带量词和背景理论的主流框架是 AVATAR 框架. 它结合了 SAT/SMT 求解器来提升在可满足性证
明框架中进行公式推理的能力.
3) CHC 求解器的求解原理可以视作求解 CHC 公式所表达的迁移系统是否满足安全性质. 通常使用基于软件
模型检测的方法, 结合谓词抽象、插值等技术来生成归纳不变式, 从而证明安全性质. CHC 求解器中一般也会集
成通用 SMT 求解器, 并基于 SMT 求解器来提供对背景理论的支持, 不同的求解器则可能针对特定的背景理论问
题实现专门的优化算法.
对递归定义问题的求解方法: 对于递归定义的处理, 递归数据结构和递归函数分别涉及对 ADT 理论和带有全
称量词的未解释函数理论的求解. 在本文中我们将从 SMT 求解器、自动定理证明器和 CHC 求解器这 3 方面对这
些特定背景理论的主流求解算法进行介绍.
1) 递归数据结构求解: 程序中的递归数据结构在逻辑公式层次一般用 ADT 理论公式进行表示.
SMT 求解器处理 ADT 理论公式的主流方法是基于 DPLL( T ) 算法. 该算法将 SAT 的 DPLL 算法与 ADT 背
[2]
景理论的判定算法相结合. ADT 理论的判定算法最早由 Oppen 提出, 其主要原理是将 ADT 结构进行展开, 对展
开的项构造同余闭包和等价关系来完成可满足性的判定. Barrett 等人 [3] 在这一判定算法基础上引入一些启发式策
略, 对计算效率进行了优化, 目前已经成为 SMT 求解器中实现 ADT 理论求解器的主流方法. Reynolds 等人 [4,5] 在
上述方法上进一步扩展, 提出 codatatype 和共享选择子 (shared selector) 理论, 提升 ADT 理论的表达能力和求解效
率. 上述基于 DPLL(T) 的判定算法被称为 lazy 方法, 作为主流 SMT 求解器如 Z3 和 cvc5 等用于进行 ADT 理论公
式的主要方法. 此外有研究考虑先将 ADT 结构消去再进行求解 eager 方法 [6,7] , 主要原理是将带有 ADT 的一阶逻
辑公式归约到等价的未解释函数和线性算术理论公式, 该方法实现在 SMT 求解器 Princess 中 [6] .
自动定理证明器求解 ADT 理论公式, 将基于 ADT 的构造子、选择子、子项等结构定义理论公理, 基于理论
[8]
公理扩展推理系统的推理规则. 近年来比较经典的工作是 Cruanes 和 Kovács 等人 [9] 对 superposition 推理系统进
行扩展, 使其支持 ADT 理论和归纳推理的工作, 分别实现在自动定理证明工具 Zipperposition [10] 和 Vampire [11] 中.
CHC 求解器求解 ADT 理论公式时, 需要将 CHC 求解框架和背景理论判定器结合, 其中背景理论判定器往往
依赖 CHC 求解器中集成的 SMT 求解器. 为了提高求解效率, 有些 CHC 求解器中实现了专门针对 ADT 理论问题的
优化算法. De Angelis 等人 [12,13] 提出一种转换算法, 可以将 CHC 公式中的 ADT 类型和对应的 CHC 公式转换成由
其他基础类型, 如整数和未解释谓词表示的公式, 并保持可满足性, 该方法实现在 VeriMAP 求解系统中. Kostyukov
等人 [14] 通过将公式中的符号都转换为未解释函数, 然后将 CHC 求解中需要推理不变式的问题归约为在 tree auto-