Page 39 - 《软件学报》2026年第2期
P. 39

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


                 NP  完全的  [29] , 对于该问题, Barrett 等人  [3]  于  2007  年在  Oppen  判定算法的基础上提出了一种有效的判定算法, 该
                 方法首先展平公式子句, 对展平得到的子项, 当其数据类型定义包含多个构造子的情况, 猜测其对应的顶层构造
                 子, 逐步地构建约束变量值, 当发现不一致            (inconsistency) 时则回溯, 然后尝试不同的构造子直到判定约束满足或
                 无法再选择, 且为了进一步提升计算效率, 算法中引入了启发式策略来优化顶层构造子的猜测来进行剪枝. 该方法
                 目前已经成为     SMT  求解器对于代数数据类型理论的基本判定方法.
                    例                                                                list 类型上有如下公理:
                       3: 我们用一个简单的例子来解释代数数据类型理论求解基本算法的思路. 假设在
                                                  
                                                  ∀x,y. head(cons(x,y)) = x
                                                                     ,
                                                  
                                                   ∀x,y. tail(cons(x,y)) = y
                 其中,  cons 是构造子,   head 和   tail 是选择子. 待求解公式   φ 是   l = cons(u,v)∧cons(head(l),tail(l)) , l. 那么一个判定过程
                                                                                              {cons(u,v),l}、
                 是基于上述公理构造同余闭包来逐步判断项的等价关系. 首先由                     l = cons(u,v) 和公理, 我们有等价类
                 {head(l),u}、 {tail(l),v}. 于是由同余关系, 应该有  cons(u,v)  和  cons(head(l),tail(l))  在同一等价类中, 即  cons(u,v) =
                 cons(head(l),tail(l)), 这与  cons(head(l),tail(l)) , l  矛盾. 于是待求解公式为不可满足的  (UNSAT) .
                    Reynolds 等人  [4] 对  Barrett 等人  [3] 的方法进一步扩展, 引入一种统一的判定算法, 用于同时支持数据类型
                 (datatype) 理论和对偶数据类型    (codatatype) 理论求解.
                    由于  DPLL(T) 框架在求解    ADT  问题时, 算法中学习到的引理子句可能存在选择子                (selector), 但每个选择子
                 只与一个构造子相关联, 这将造成学习到的引理子句通用性较差, 针对这一问题, Reynolds 等人                       [5] 提出共享选择子
                 (shared selector) 理论用于减少判定过程中项的计算数量, 从而加速求解时间, 但实验表明该方法的适用性不够强,
                 尽管可以显著提升语义引导合成            (SyGus) 问题相关的求解效率, 但对于更一般且公式规模增大的测例集, 该方法
                 提升效果有限.
                    上述这些经典的判定方法主要基于             SMT  求解  lazy  方法, 近年来, 有一些研究者考虑通过       eager 方法来求解代
                 数数据类型公式      [6,7] . Hojjat 等人  [6] 提出将代数数据类型公式归约到等价的未解释函数和线性算术理论公式的方
                 法, 并实现在   Princess 求解器中; 类似的, Shah  等人  [7] 将代数数据类型公式归约到等价的未解释函数理论的公式进
                                       [6]
                 行求解, 但使用与    Hojjat 等人 不同的归约技术去避免引入线性算术理论造成的求解困难, 他们的方法相对传统方法
                 在实验效果上具有一些提升, 但对于包含互递归定义以及多种类型定义且长度较大的复杂公式, 该方法与现有
                 state-of-the-art 的  SMT  求解器  Z3、cvc5  和  Princess 均表现出求解困难, 表明现有的代数数据类型理论求解方法在
                 可扩展性和求解效率上依然存在较大提升空间                [7] .
                  2.3   归纳推理增强技术
                    下面我们介绍基于引理生成的归纳推理增强技术. 带有递归定义函数的问题求解效率十分依赖于在求解方法
                 中引入的归纳推理模式和引理生成技术的效率. 本节首先介绍在量词消去过程中引入归纳推理模式的方法. 第
                 2.4  节我们将介绍辅助证明的引理生成技术.
                    为了便于理解, 例     4  中我们用更接近数学语言的写法替代            SMT  语法, 表示上文中对     list 定义的长度函数.
                    例               len : list → Int:
                       4: 假设长度函数
                                             
                                              len(nil) = 0             (A 1 )
                                             
                                                                           ,
                                             
                                             
                                              ∀x,y. len(cons(x,y)) = 1+len(y) (A 2 )
                 要证明断言    ψ := ∀x. len(x) ⩾ 0.
                                                                                              ψ 不成立的反
                    为证明断言成立, 我们求解        F := {A 1 ,A 2 ,¬ψ} 的可满足性, 若   F  可满足, 表示我们找到一个使断言
                 例, 若   F  不可满足, 表示我们证明断言     ψ 成立.
                    SMT  求解器处理上述问题首先会调用量词消去模块, 对于全称量词, 一般基于                      instantiation (实例化) 技术; 对
                 于存在量词, 则一般基于        Skolemization (斯科伦化) 技术  [30] . 由于待验证断言是一个否定的全称量词公式            (SMT
                 求解器中一般基于德摩根律将其转换为存在量词公式), SMT                    求解器首先会尝试使用 斯科伦化技术对其进行
                 量词消去: 首先可推出引理         (∀x. P(x))∨¬P(k), 这里  k  是一个常数  (这一引理的成立直观上可以理解为等价于
   34   35   36   37   38   39   40   41   42   43   44