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

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

来寻找相关子目标公式, 此时枚举的候选公式中剩下的公式称为被过滤 (filtered) 公式. 下面分别介绍枚举的基本
方法和过滤候选公式的启发式技术.
枚举子目标公式: 首先定义公式项的 size 为项中函数应用次数加上重复变量的数量. 例如对于 f(g(x,y)), 函数
g 作用于参数 x 与 , g(x,y), 没有重复变量, 则 f(g(x,y)) 的 size 为 2. 而 g(x, f(x)), 出现函数 f 和 g, 且 x 重复
y f 作用于
出现, 于是 size 为 3. 令形如 ∀¯x. f(¯x) = g(¯x) 的 size 是 max(size( f(¯x)), size(g(¯x))). 例如 φ 1 = ∀x,y. f(g(x,y)) = h(f(x), f(y)),
左边的 size 为 2, 右边 f(x) 和 f(y) 两次函数应用, 加上函数 h, size 为 3, 于是 φ 1 的 size 为 3. 从 size 为 0 开始, 对 size
R
为 n 枚举所有可能的子目标集合 S n , 称其为候选子目标集合. 对每个 n, 通过启发式技术确定一个子集 S ⊆ S n ,
n
称该子集为相关子集, 剩下的公式集合称为被过滤子集. 随着 n 增长不断构造相关子集作为子目标引理, 用于辅助
n 的上界 (实际中一般使用 3). 下面介绍 Reynolds 等人 [31] 所使用的过滤技术.
归纳推理, 直到达到某个固定的
过滤候选子目标: 主要有 3 种启发式过滤技术.
1) 基于激活断言 (active conjecture) 过滤. 对于一个项 t 如果对当前的文字集合 M 和原问题符号表 Σ, 可以推
t
s
出存在某些 Σ 中的项 , 使得 t = s, 则称 是非激活的 (inactive), 否则为激活的 (active). 在 M 中出现的形如
f(t 1 ,...,t n ) 的项, 若其中至少有一个项 t i 是激活的, 则称这个 f 项为 M 中基础相关 (ground-relevant) 的项. 如果一
t
t
个 Σ 中的项 能够被泛化为一个基础相关项 s, 则称 是相关项, 这里的泛化指在 M 中可推出 (t = s)σ 成立, σ 是某
t 中自由变量映射为基项的替换. 最后在枚举生成候选子目标的过程中, 只保留相关的项. 进行这一步过滤的
个将
′
Σ
直观是对原命题进行斯科伦化后会在原问题的符号表 Σ 中引入斯科伦常数 k, 构成扩展符号表 . 此时原问题的
公理和 SMT 对应的代数数据类型或整数背景理论无法推导扩展后的符号表 Σ 所构成的公式. 基于这一观察, 在
′
Σ 项的候选子目标, 尤其是那些无法在当前上下文中推出等
′
进行过滤时应该尽可能生成仅可泛化到扩展符号表
价于原符号表 Σ 项的子目标公式.
例 5: 考虑代数数据类型和等式的混合理论 T . 定义了数据类型 nat 和 list. 并假设符号表 Σ 中包含函数 plus、
app、 rev 和 sum 分别表示自然数的加法、对列表添加元素、列表的反转以及将列表的元素求和. 令 A 是这些函
数上的公理, 包括:


sum(nil) = O
 ,

∀x,y. sum(cons(x,y)) = plus(x, sum(y))

要证明断言 ψ := ∀x. sum(rev(x)) = sum(x).
那么在例 5 中, 对 ¬ψ 进行斯科伦化得到 ¬sum(rev(k)) = k k 为斯科伦常数. 要证明例 5 实际上需要生成合适
,
的子目标公式, 这里我们暂时不介绍整个具体的求解过程, 而是以本例介绍过滤技术的相关概念. 假设在求解的某
个阶段, 得到当前上下文子句集合为 M = {sum(k) = O, sum(rev(k)) = s(O),rev(k) = nil}. 此时在 M 中没有形如 k = x
的公式, k 是激活的项, 那么 sum(k) 是基础相关项, 由于 sum(x) 可以泛化为 sum(k), 则 sum(x) 是相关项. 在候选子
目标中包括这一项的公式将会保留. 而由于 M 中有 rev(k) = nil 这一公式, 那么 sum(rev(k)) 不是基础相关项, 于是
∀x. sum(rev(x)) = t, 其中 表示任意项, 这样的候选子目标将会被过滤. 直观上我
t
sum(rev(x)) 不是相关项. 那么形如
们可以理解为这些形如被过滤的子目标的公式可以轻易地在判定过程中由当前上下文推出, 而无需作为专门的子
目标公式引入.
2) 基于规范性 (canonicity) 过滤. 这一技术的直观是将 SMT 求解器中对等式理论和代数数据类型理论基于同
余闭包对公式中的项划分等价类进行推导的方法进行扩展. 通过构造等价类的方式来过滤同一等价类中多余的
项. 假设当前上下文 M 中的一个由非基础 (non-ground) 的 Σ 项组成的等式集合 . 维护一个 U 上的同余闭包 U ,
∗
U
∀[FV(t i )∪ FV(t j )]. t i = t j . 在每个等价类中选择一个具有最
其中的每一个等价类 {t 1 ,...,t n }, 对任意 i, j ∈ {1,...,n} 有
小 size 的项, 令其为代表项 (representative term). 称 U 中的一个项是规范的 (canonical) 当且仅当它是其中一个等
∗
价类的代表项, 称其为不规范 (non-canonical) 当且仅当它在 U 中且不是代表项. 那么在枚举候选子目标时, 对于
∗
那些包含至少一个不规范 (non-canonical) 子项的子目标, 将会被过滤掉.
例 6: 假设上下文 M = {∀x. app(x,nil) = x}. 可以构造等式集合 U = {app(x,nil) = x}, 于是同余闭包 U 包含两个
∗
等价类 {x,app(x,nil)} 和 {nil}. 假设对某一个候选子目标 φ := ∀x. rev(app(rev(x),nil)) = x. 引入 φ 中的所有子项, 同