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

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

1 (assert (not (forall ((x list) (y list))
2 (= (len(append x y)) (+ (len x) (len y)))
3 ))) ; prove
此时作为待证明问题, 目标是令 SMT 求解器返回 UNSAT, 表示该断言不成立, 由反证法知原性质成立. 将断
言进行简单修改得到:

1 (assert (not (forall ((x list) (y list))
2 (= (len(append x y)) (+ (+ (len x) (len y)) 1))
3 ))) ; find cex

表 4 ADT 理论和整数理论混合样例

类别 样例
递归数据结构 list := nil | cons(x : Int, y : list)
len(nil,0) = 0
∀x : Int,y : list. len(cons(x,y)) = 1+len(y)

递归函数
∀x : list. append(nil, x) = x
∀x : Int,y : list,z : list. append(cons(x,y),z) = cons(x,(append(y,z)))
∀x : list,y : list. len((append(x,y))) = len(append(y, x))
待求解性质
∀x : list,y : list. len((append(x,y))) = len(x)+len(y)

∀x : list,y : list. len((append(x,y))) = len(x)+len(y)+1 作为性质不成立问题, 目标是令 SMT
此时表示的性质为
求解器返回 SAT, 表示它能找到一个模型, 使得该断言成立, 从而对应的性质不成立.
实验设置如下: 我们在 20 核内存 64 GB 的 xeon gold 5115@2.4 GHz 处理器上进行实验. 设置每个例子的时
间限制为 300 s. 所有样例统一表示为通用的 SMTLIB 格式, 且其中递归函数是使用公理表示 (即不使用 define-fun-
rec, 而是通过多条 assert 断言来表示). 通用的 SMTLIB 格式作为 Z3 求解器, cvc5 求解器和 Vampire 自动定理证
明器的输入. 然后样例将由通用的 SMTLIB 格式转换为 CHC 形式, 作为 Eldarica、Spacer 和 Racer 这 3 种 CHC
求解器的输入.
对于整数递归函数样例, 我们运行和对比第 5.1 节中除 Racer 求解器以外的所有工具, 不对比 Racer 的原因是
目前 Racer 的使用需要先通过相关文献 [15] 提供的脚本, 对原 CHC 公式进行预处理, 将其中用公理表示定义的递
归函数体进行自动转换, 显式地表示成 Racer 可以处理的特定形式. 然后 Racer 才能对这些递归函数体进行识别
和调用专用算法求解. 否则 Racer 无法调用特定算法, 将和 Spacer 表现一样. 而目前预处理脚本和 Racer 工具不支
持本文整数样例中的递归函数定义, 只能支持 ADT 和整数混合理论样例的问题, 因此我们只在混合理论样例中才
考虑 Racer 工具. 对于其他工具, 除 cvc5 求解器和 Vampire 自动定理证明器以外, 均直接使用默认命令选项. cvc5
求解器使用归纳推理增强和子引理生成的命令选项: --quant-ind --conjecture-gen --full-saturate-quant. Vampire 自动
定理证明器使用 portfolio 模式的归纳推理策略 (其中包含了专用于整数归纳推理算法的命令), 命令选项为: --mode
portfolio --schedule induction.
对于 ADT 和整数混合理论样例, 我们运行第 5.1 节中所有工具, 其中: 1) 在运行 Racer 工具求解前, 先通过
Racer 文献 [15] 提供的预处理脚本将原 CHC 公式中的递归函数定义转换为 Racer 需要的形式. 2) 对于 168 个待证
明问题, 运行所有工具, 其中 cvc5 和 Vampire 使用如整数样例一样的命令选项, 其他工具均使用默认命令. 3) 对
于 83 个性质不成立的问题, 由于 cvc5 和 Z3 求解器实现了用于递归函数问题的有限模型寻找 (finite-model-
finding) 技术, 根据文献 [50] 报告, 该技术有利于可满足性问题的求解, 但需要输入显式定义的递归函数, 因此我们
先将这些问题中通过公理断言表示的递归函数定义转换成由 define-fun-rec 表示的递归函数定义, 然后再调用
cvc5 和 Z3 进行求解. cvc5 在命令选项中加入--fmf-fun 参数, 表示调用有限模型寻找技术, 其他参数选项均和之前