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

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

Sup 推理系统一般包含如下推理规则: superposition 规则 (Sup)、binary resolution 规则 (Bin)、 equality
resolution 规则 (ER) 等. 这里我们简单介绍这些规则对应的推理公式.
A∨C ¬B∨ D
θ
● Binary resolution 规则: (Bin), 其中 是 A 和 B 的 mgu.
(C ∨ D)θ
l , r ∨C
θ
● Equality resolution 规则: (ER), 其中 是 l 和 的 r mgu.
Cθ
l = r ∨C t[s] = u∨ D l = r ∨C t[s] , u∨ D l = r ∨C L[s]∨ D
● Superposition 规则: (Sup1), (Sup2), (Sup3), 其中
(t[r] = u∨C ∨ D)θ (t[r] , u∨C ∨ D)θ (L[r]∨C ∨ D)θ
s 的 mgu, ,
θ 是 l 和 lθ ≻ rθ t[s]θ ≻ uθ 且 L 不是等式.

l = r C[lθ]∨ D
● Demodulation 规则: (Dem), 其中 lθ ≻ rθ 且 C[lθ]∨ D ≻ lθ = rθ. 这一条规则是化简规则, 是
C[rθ]∨ D
superposition 规则的一个特例.
这里我们给出一些直观解释来理解上述规则.
Binary resolution 规则, 即归结规则 (或翻译为消解规则), 是一种基本的推理规则, 表示若 A 和 B 存在合一子
替换, 由于 Aθ = Bθ, 那么可以将 Aθ 和 (¬B)θ 消解, 于是 (C ∨ D)θ 必然成立.
Equality resolution 规则类似归结规则, 但它引入了等式符号. 该规则比较简单: 如果 l , r ∨C 成立, 那么对任
r
l
意模型, 要么 C 成立, 要么 l , r 成立. 如果 l , r 成立, 那么 lθ , rθ 成立, 若 和 存在 mgu 为 θ, 那么 lθ = rθ, 出现矛
Cθ 成立.
盾. 于是此时必然有
Superposition 规则以 Sup1 为例, 它通过等式 l = r 来做重写. 等式 t[s] = u 表示某个位置的子项为 的项 t, 有
s
t = u. 如果 和 是可合一的, 存在 mgu 为 θ, 即 lθ = sθ. 该规则表示如下推理: 对前提子句的任意模型, 如果上下文
s
l
θ
s
C 和 D 都是 false, 那么必然有 l = r 和 t[s] = u 同时为 true. 由于 sθ = lθ, 那么将 用 替换后, 基于等式关系有
D 都为 false 时必然为 true. 这一个规则可以被视
sθ = lθ = rθ. 于是 t[s]θ = t[r]θ, 从而 t[r]θ = uθ, 即 (t[r] = u)θ 在 C 和
作一种有条件重写 (conditional rewriting), 即假设 C 和 D 均为 false 时, t 的子项 可被 l = r 重写. Superposition 规
s
则可以认为是提供了一种应用等式关系和变量替换来对原公式中的子句进行化简和消去的方法.
基于推理系统对公式进行证明需要一个合适的算法来进行反证的过程, 即如何在前提条件构成的搜索空间中
组织对空子句的搜索. 进行证明推导一般使用 saturation-based proof search 推理框架, 我们将在第 3.1 节中进行
介绍.
1.5 在 SMT 中表示带有递归定义函数的问题
对于带有递归定义函数的程序验证问题, 传统方法是通过程序分析技术来处理递归定义, 生成尽可能简单的
SMT 公式 (一般为无量词不包含递归函数定义的简单公式) 交给底层 SMT 求解器进行求解 (在本文第 4.5 节将对
这类方法进行介绍). 近些年来, 研究者开始关注直接在求解器中处理带有递归结构的 SMT 公式.
基于 SMTLIB 标准语法对递归定义函数进行表示, 通常是将函数体表示为全称量词和未解释函数组成的公
理断言. 从 2016 年开始, SMTLIB 标准语法支持使用 define-fun-rec 直接定义递归函数, 下面分别展示使用公理断
言和 define-fun-rec 在 SMT 公式中表示递归定义函数的例子, 并假设待验证性质为对任意 list 类型的参数 x, 其长

度大于等于 0, 即 ∀x : list. len(x) ⩾ 0. 在本文的例子中我们两种写法都会有所涉及.
使用公理表示递归定义函数: 例如我们在 SMT 的 ADT 理论中定义 list 类型: declare-datatypes list = nil|
cons(head : int,tail : list). 然后在 SMT 中定义 list 类型的长度函数 len : list → int, 使用 SMTLIB 标准格式进行公理
定义如下.

1 (declare-fun len(list))
2 (assert (= (len nil) 0))
3 (assert ((forall ((x Int) (y Int)) (= (len(cons x y)) (+ (len y) 1)))))
4 (assert (not ((forall (x list) (>= (len x) 0)))))