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

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

4.3 CHC 求解方法
主流的 CHC 求解方法有两大类: 一类是基于模型检测算法 IC3/PDR [58,59] 的求解方法, 另一类是基于谓词抽象
和 Craig 插值进行抽象精化的方法. 这两类方法都可以认为是将程序视作迁移系统, 然后尝试生成程序的归纳不
变式来完成性质验证.
基于 IC3/PDR 的求解算法: CHC 求解工具 Spacer [60,61] 中实现了基于 IC3/PDR 的求解算法. 该算法与模型检测
中经典的 IC3/PDR 算法思路相同, 可以认为是将 IC3/PDR 算法进行迁移并适配到 CHC 的框架下. 主要原理是将
原问题视作一个迁移系统安全性验证问题. 从初始状态开始迭代构造表示可达状态上近似的归纳公式序列. 每次
检查公式序列中是否存在可达坏状态的反例路径, 根据检查结果精化 (refine) 公式序列, 直到找到真实反例证明性
质违反或者归纳不变式证明性质成立. 此外 Spacer 还加入了模型映射技术 (model based projection)、全局引导
(global guidance) 等优化方法.
基于谓词抽象和 Craig 插值的求解方法: CHC 求解工具 Eldarica [62] 中实现了基于谓词抽象的 CHC 求解算法,
其主要原理是尝试对原霍恩子句构建一个抽象可达图 (abstract reachability graph, ARG). 然后基于 ARG 来获得抽
象的反例路径, 该反例将会被 SMT 求解器进行检查以排除假反例. SMT 检查的结果最终返回一个具体的反例路
径或者一个基于 Craig 插值计算得到的新的谓词. 这一计算过程中, 不同的文献考虑使用和优化不同的插值方法,
如树插值 (tree interpolation), 析取插值 (disjunctive interpolation) 等.
CHC 求解方法所计算的归纳不变式可以视作一种用于辅助证明的引理, 对于某些无法由归纳推理求解的问
题, 通过该方法可能会比较容易生成所需要的辅助引理, 但这一技术依赖比较复杂的判定求解过程, 可能无法高效
生成规模较大或形式较复杂的引理公式.
例 15: 这里我们介绍一个通过 CHC 求解生成引理帮助原命题求解的简单例子 [63] . 考虑如下的函数定义.

1 def posTwice(x: BigInt): BigInt = {
2 if x <= 0 then BigInt (0)
3 else 2 + posTwice(x – 1)
4 } ensuring (res => res != –1)

这个函数在输入 x 小于 0 时返回 0, 在 x 大于等于 0 时计算 2×x. 需要证明的性质是 ∀x. posTwice(x) , −1. 注意
这一个问题实际上无法通过归纳推理求解, 因为原命题太弱, 直接应用归纳假设对证明没有帮助 (例如我们假设
posTwice(x−1) , −1, 那么我们只能得到 posTwice(x) , 1). 而若将该问题转换为如下的 CHC 公式:


∀x. x ⩽ 0 → posTwiceInv(x,0)






∀x,y. posTwiceInv(x−1,y)∧ x > 0 → posTwiceInv(x,y+2) .





 ∀x,y. posTwiceInv(x,y)∧y = −1 → false
注意这里 posTwiceInv 与原来的 posTwice 不同, 它是一个谓词, 且输入两个参数, 分别可以对应原来 posTwice
函数的输入和输出, 实际上它表示一个待求解的归纳不变式. 使用 CHC 求解器则可以求解这一问题, 它将返回“可
满足”, 且生成一个归纳不变式.
(define-fun posTwiceInv((A Int)(B Int)) Bool (>= B 0))
表示原 posTwice 函数的输出总大于等于 0, 该不变式可以视作一个辅助引理, 基于这一个引理, 则原命题可以被容
易地证明.
4.4 使用 CHC 形式表示递归函数
为了与直接输入 SMT 公式的方法进行对比, 我们将按照 CHC 社区常用的方法将 SMT 中的递归定义转换为
CHC 形式, 以定义 list 类型的长度函数为例.