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

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


                    使用  define-fun-rec 表示递归定义函数: 同样定义     list 类型的长度函数, 可以表示如下.

                 1 (declare-fun-rec len
                 2  ((x list)) Int
                 3   (match x
                 4    ((nil 0)
                 5    ((cons x y) (+ (len y) 1))
                 6   )))
                 7 (assert (not ((forall (x list) (>= (len x) 0)))))
                    以上两种表示方法均为分别从递归函数的基本情况                   (base case) 和递归情况  (recursive case) 进行构造. 表示令

                                                                               y
                 空列表   nil 的长度  len 为  0, 对任意列表   L, 当  L 由类型为  Int  的  x 和类型为  list  的   构造时, 即  L = cons x y 时,  L 的
                      y 加  1. 并对待验证公式取反, 当     SMT  求解返回不可满足时, 则表示原性质必然成立.
                 长度为
                    SMT  求解器对于    define-fun-rec 的函数定义会采取一些特定的策略进行求解, 如           Z3  对于使用   define-fun  的函
                 数定义更倾向于“eager”的展开策略, 将所有对应函数的出现用函数体进行代换; 而对于                       define-fun-rec 则更倾向先
                 作为未解释函数进行保留. 如         cvc5  实现了针对递归定义函数的求解优化选项“--fmf-fun”, 对于           define-fun-rec 的递
                 归定义函数生效, 该技术主要用于找到可满足模型, 下文将进行详细介绍.
                    对于带递归定义的       SMT  公式求解, 待验证断言通常用带全称量词的              SMT  公式表示, 例如若希望验证对任意
                 list 类型, 其长度均大于等于     0, 则待验证断言表示为       ψ := ∀x. len(x) ⩾ 0. 其中  x 类型为  list. 主流工作分为两类: 一
                 类是基于   SMT  求解器的验证工具, 需要先将待验证公式取反, 然后使用                 SMT  求解器求解, 若返回     SAT, 则表明存
                 在一组赋值使该断言不成立, 即存在一组反例; 若返回                UNSAT, 则证明原公式成立. 另一类也是基于自动定理证明
                 系统, 待验证断言作为结论, 若能够在证明系统中推理出该结论, 则成功证明.
                    由于递归定义的结构, 待验证公式的验证往往依赖于归纳推理等技术, 因此在                       SMT  求解器或定理证明系统中引
                 入归纳推理能力是该领域的研究重点, 目前的主要工作可以分为两类: 一类是基于                         SMT  求解的  DPLL( T ) 框架, 在
                 全称量词实例化的过程中对公式进行归纳增强, 并结合子目标生成技术提高求解效率; 另一类是在自动定理证明器
                 的证明系统中引入归纳推理规则, 基于自动定理证明系统对                  SMT  公式进行验证. 下面我们分别对两类工作进行介绍.

                  2   SMT  求解器递归定义求解技术
                    基于  SMT  求解算法验证带递归定义公式的技术包括验证技术 (即返回                    UNSAT  求解进行证明) 和找错技术
                 (即找到可满足解返回       SAT). 基于  SMT  求解的框架, cvc5  在求解带递归定义函数的         SMT  问题时可以利用现代求
                 解器在代数数据类型和整数等背景理论下的高效求解能力. 本节将先介绍用于递归函数问题返回                                UNSAT  的归纳
                 定义增强和引理生成技术, 然后简要介绍和讨论用于递归函数问题返回                       SAT  的模型寻找方法.
                  2.1   DPLL(T) 判定算法
                    DPLL(T) 是目前  SMT  求解的主流判定算法. 它由用于推理特定理论背景可满足性的理论求解器和基于                          DPLL
                 算法来高效推理命题逻辑可满足性的             SAT  求解器组成. 由于求解时先将         SMT  公式视作   SAT  公式进行求解, “按
                 需”使用理论求解器, 因此该方法被称为            lazy  方法.
                    DPLL(T) 伪代码如算法     1. 其中输入为公式     φ in quant_elim 为量词消去函数.  get_model 表示基于  DPLL  算法
                                                        .
                 的  SAT  求解器, 它接受一个命题逻辑公式         F  作为输入, 如果   F  不可满足则返回空     ( none); 如果  F  可满足则返回一
                                               .
                 个可满足文字的合取子句         A, 使得  A ⊨ F check_sat T  表示背景理论  T  的求解器, 它接受一个符号表    Σ 中文字的合取
                                                                                          c
                 子句   ψ 作为输入, 返回可满足或      ψ 中不可满足文字的合取子句         µ. 算法中上标为     c, 如第  8  行  A , 和上标为  a, 如第
                     a
                 2  行  φ , 分别表示具体化  (concretization) 和抽象化  (abstraction) 函数, 其中抽象化函数将一个带背景理论的无量词
                                                                         a c
                 SMT  公式  φ 映射到命题逻辑公式, 具体化表示抽象化函数的逆函数, 即                (φ ) = φ. 算法原理是先将原公式做量词消
   32   33   34   35   36   37   38   39   40   41   42