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

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

1 ; 定义原递归函数为谓词
2 (define-fun lenCHC(list Int) Bool)
3 ; 编码函数定义
4 (assert (forall ((x list))
5 (=> (= x nil)
6 (lenCHC x 0))))
7 (assert ((forall ((h Int) (t list) (x list) (y0 Int) (y1 Int))
8 (=> (and (lenCHC t y0) (= y1 (+ y0 1)) (= x (cons h t)))
9 (lenCHC x y1)))))
10 ; 编码待验证断言
11 (assert ((forall ((x list) (y Int))
12 (=> (and (lenCHC x y) (< y 0))
13 false))))

如上, 将原参数为 list 的 len 函数 len(x : list) 定义为二元谓词 lenCHC(x : list,y : Int), 令 len(x) = y 等价于
lenCHC(x,y) = true. 用 definite 子句表示递归定义. 本例中两条断言分别编码原递归函数 len 在基本情况和递归情
况下的构造. 对于待验证性质则表示为 goal 子句. 注意此时与 SMT 求解的方法不同, 在 SMT 求解中返回不可满
足对应待验证性质被证明成立. 而在 CHC 公式的表示中, 我们已经用反证的方式定义了待验证性质. 因此当 CHC
求解器返回可满足时, 表示它找到一个归纳不变式, 不变式对应于一个 CHC 公式的模型, 使得我们的 goal 子句成
立, 这表明我们通过反证的方式证明了待验证性质成立. 而如果 CHC 求解器返回不可满足, 将表示它找到一个令
待验证公式取反成立的反例, 即待验证公式不成立. 对于带有递归函数的 SMT 问题, 通过如上方式转换成 CHC 形
式后, 就可以通过本节所介绍的 CHC 求解方法进行求解.

4.5 基于展开和抽象的递归函数求解技术
尽管在第 4.3 和 4.4 节中, 我们介绍了可以直接通过通用的 CHC 求解算法来求解递归函数问题, 但为了提高
求解效率, 2022 年 Govind 等人 [15] 提出在 CHC 求解器中设计专用于处理递归函数结构的算法. 这一算法思路最早
来源于 2010 年 Suter 等人 [32,64] 的相关工作. 本节中我们首先介绍早期基于展开的递归函数求解算法, 最后介绍在
CHC 求解框架中引入基于展开和未解释函数抽象的 CHC 求解方法.
早期基于展开的递归函数求解算法, Suter 等人 [32,64] 从 2010 年的工作开始研究带有递归定义函数的一阶逻辑
公式判定算法, 由于当时 SMT 标准还处于早期阶段, 因此他们的工作没有直接支持 SMT 公式或集成到 SMT 求
解器中, 但他们提出了一种针对包含递归定义函数的无量词代数数据结构理论一阶逻辑公式的判定算法, 该算法
主要在后续被一些程序验证的工作如 Scala 验证工具 Leon/Stainless、CHC 求解器 [15] 所继承, 可能对于 SMT 类似
形式的公式求解具有一些思路上的启发意义.
下面我们对该方法进行介绍, Suter 等人 [32,64] 考虑无量词代数数据类型理论的 SMT 公式中包含 catamorphism
的问题. 其方法所能处理的公式主要为无量词代数数据类型理论的公式, 一般不涉及理论组合 (如整数理论等).
catamorphism 类似函数式编程语言中的 fold 函数, 可以认为是一类特定的递归函数, 但其范围足够覆盖较为常见
的递归函数, 如计算 tree 高度的递归定义函数、计算 list 元素集合的递归定义和计算 list 的长度等. Suter 等人 [32,64]
提供了一种基础方法来推导包含 catamorphism 的 ADT 公式, 主要思路即对 catamorphism 基于递归函数的定义进
行有限步展开, 在展开过程中, 还未展开的递归部分被视作未解释函数, 为了处理引入未解释函数带来的“假反例”情
况, 再在展开过程中引入一个 Bool 类型的“控制变量”的集合, 每个控制变量对应一个逻辑公式中的项, 但这个项
不包含未解释函数时, 则控制变量为 true, 代表结果可信任, 否则为 false. 将控制变量集合合取原公式. 当求解器返
回 SAT 结果时, 此时控制变量必然全为 true, 我们可以相信 SAT 这一结果; 当求解器返回 UNSAT 结果时, 可能有