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

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

HORN)), Z3 将自动调用 Spacer 引擎进行 CHC 公式的求解. Spacer 在学术界和工业界均具有广泛应用. 例如基于
LLVM 的 C++程序验证框架 SeaHorn, 其核心推理引擎依赖 Spacer. 在微软等公司中 Spacer 用于云服务协议和操
作系统组件以及区块链等领域的安全性验证 [72] . Spacer 求解核心算法类似在待验证问题对应的迁移系统上进行
IC3/PDR 模型检测算法, 且它集成了许多求解效率优化技术, 如 Craig 插值、基于模型映射技术 (model based projection)
以及全局引导技术 (global guidance) 等. Spacer 作为最主流的 CHC 求解器之一, 且它具有和 Eldarica 不同的核心
推理算法, 因此我们选取它作为 CHC 求解器的另一代表进行实验. 由于下文即将介绍的 Racer 求解器是基于
Spacer 求解器进行开发, 它在 Spacer 原求解算法基础上实现了专门针对 ADT 和递归函数的求解技术, 因此 Spacer
的求解结果也作为 baseline, 用于分析 Racer 求解技术的效果.
Racer 求解器是加拿大滑铁卢大学的 Govind 等人 [15] 在 2022 年基于 Spacer 实现的 CHC 求解器, 它在 Spacer
算法框架上实现了专门用于处理递归函数和 ADT 类型 CHC 问题算法. 它可以视作 Spacer 求解器的扩展版本, 我
们选择它进行实验比较, 分析其算法在不同类型的实际样例中表现效果.
5.2 实验样例和实验设置
我们在两类样例上进行实验比较, 分别是整数递归函数样例与 ADT 与整数混合理论样例. 其中整数递归函数
样例来自 Hozzová等人 [55] 在 Vampire 中引入整数归纳优化的文献, 以及我们从其他程序验证问题中手工构造的样
例, 这一部分样例均不包含 ADT 类型的问题; ADT 与整数混合理论样例来自 Reynolds 等人 [31] 在 SMT 求解算法
中引入归纳推理的文献以及后续 CHC 领域研究者在 CHC 求解算法中引入 ADT 和递归函数求解的一些相关
文献 [12,15,47] .
● 整数递归函数样例
这一类样例公式中递归函数的参数和返回值为 SMT 理论中的整数. 包括文献 [55] 中 120 个样例和我们手工
构造的 102 个样例, 如表 3 所示.

表 3 整数递归函数样例

样例来源 关键递归函数 待求解性质举例
e
e
e
pow(x,e) = x , x,e ∈ Z, e ⩾ 0 ∀e ∈ Z. e ⩾ 0 → (x·y) = x ·y e
文献[55]样例 sumX(x,y) = x+(x+1)+...+y x,y ∈ Z x ⩽ y ∀x,y ∈ Z 2· sumX(x,y) = y·(y+1)− x·(x−1)
,
,
.
f(0) = 0 f(x) = f(x+1), x ∈ Z ∀x ∈ Z. x ⩾ −10 → f(x) = f(0)
,
x
x
pow2(x) = 2 , x ∈ N ∀x,y ∈ N. 2 x+y = 2 ·2 y
x
;
,
bitLen(x) = bitLen(⌊x/2⌋)+1 x ∈ N, x > 0 bitLen(0) = 0 bitLen(2 ) = x+1 x ∈ N
,
手动构造
fbi(x) = fbi(x−1)+ fbi(x−2) x ∈ N x ⩾ 2;
,
,
∀x ∈ N. fbi(x) = 5· fbi(x−4)+3· fbi(x−5)
,
fbi(0) = 0 fbi(1) = 1

文献 [55] 中 120 个样例可分为 3 类, 分别是幂函数 pow 相关样例、求和函数 sumX 相关样例和赋值函数 f 相
关样例.
e
x e
1) pow 函数定义见表 3 第 1 行, 表示计算 x , 其中 , 均为整数, 且 e ⩾ 0. 这类样例待求解目标公式是各种幂
e
e
e
函数相关的性质, 例如 (x+y) = x ·y 等.
2) 求和函数 sumX 定义见表 3 第 2 行, 表示计算 x+(x+1)+...+y, 其中 x ⩽ y x 和 均为整数. 这类样例待求
,
y
x 和 范围, 求和函数的计算公式是否成立, 如表 3 中所示, ∀x,y ∈ Z. x ⩽ y → 2· sumX(x,
y
解目标公式是设置不同的
y) = y·(y+1)− x·(x−1), 或者固定一个变量 y, 求解 x 不同范围下性质是否成立, 例如 ∀x ∈ Z. x ⩽ (−16) → (2· sumX(x,
0) = −x·(x−1)).
x f(x) = f(x+1). 这个函数背景是
3) 赋值函数 f 定义见表 3 第 3 行, 表示定义函数 f, 有 f(0) = 0, 对任意整数 ,
对程序中的数组进行统一赋值. 这类样例求解目标公式是设置不同的变量范围, 计算 f 需要满足的一些数学性质,
x x ⩾ −10 → f(x) = f(0).
例如任意整数 ,