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

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


                 ADT  和量词等理论的推理效率进行了优化和最新算法的集成. 对于递归函数求解, 它实现了用于求解递归函数可
                 满足模型的“有限模型寻找”算法, 以及用于证明递归函数性质的归纳推理与引理生成算法, 是目前唯一能够较好
                 地支持归纳推理证明的主流          SMT  求解器. cvc5  求解带递归函数    SMT  问题的主要参数选项如表         1.

                                                 表 1 cvc5  归纳推理参数选项

                      选项                                         说明
                    --fmf-fun  使用finite-model-finding技术求解使用define-fun-rec定义的递归函数可满足性问题
                    --dt-stc-ind  在代数数据类型的问题中基于结构归纳对存在量词消去进行归纳增强
                    --int-wf-ind  通过良基归纳对整数理论进行归纳推理增强技术
                              使用所有的归纳推理技术. 实际上同时支持了上述两种数据类型理论上的归纳推理技术, 根据公式中项的具
                    --quant-ind
                              体理论自动选择合适的归纳模式
                  --conjecture-gen  在归纳证明中生成候选子句
                              在带量词问题的推理中尽可能多的尝试各种内置实例化技术. 由于在cvc5中进行归纳推理可以视作在量词
                 --full-saturate-quant 消去过程中的一种优化技术, 例子中待验证命题都是包含全称量词的断言, 因此在实验中开启这一选项易于
                              求解器尽可能产生结果而不直接返回unknown

                    Vampire 自动定理证明器最早由        Voronkov  于  20  世纪  90  年代在瑞典乌普萨拉大学主导开发, 之后经过多次
                 代码重构和版本升级. 目前的版本由            Voronkov  和  Kovács 带领英国曼切斯特大学和维也纳技术大学的研究团队
                 从  2014  年开始进行开发, 并进行维护      [68] . Vampire 是一阶逻辑定理证明领域的代表性工具, 在自动定理证明领域
                 的  CASC  竞赛中多次获奖. 相比     Z3  和  cvc5  等  SMT  求解器, 它的主要特点是基于    superposition  演算的推理引擎,
                 并在处理带有量词公式时具有相对更高的求解效率                  [11] . 但  SMT  求解器  (尤其是  Z3) 在工业级应用上更广泛和成
                 熟, 且支持更广泛的      SMT  理论, 相比之下   Vampire 更多流行于学术界, 且目前还不支持浮点数、位向量和字符串
                 理论求解   [69] . 对于递归函数问题, Vampire 中实现了众多用于归纳推理证明的算法              (详见第   3  节), 主要参数选项如
                 表  2. 由于  Vampire 的参数选项较多, 开发者实现了易于用户使用的            portfolio  运行模式, 并提供了专门用于归纳推
                 理的策略组合. 这一模式下可以使          Vampire 通过在多核并行运行多种归纳参数策略, 提高求解成功率. 我们在实验
                 中选择使用这一模式.

                                               表 2 Vampire 归纳推理参数选项

                                    选项                                          说明
                            --induction int/struct/both/none           选择对应理论的归纳证明模式
                     --structural_induction_kind one/two/three/rec_def/all  选择在代数数据类型项的归纳中使用哪一种归纳公理
                          --induction_on_complex_terms on/off            在复杂项上应用归纳推理
                               --induction_gen on/off                 在归纳推理规则中应用IndGen规则
                        --int_induction_interval infinite/finite/both  在归纳推理规则中应用IndHRW规则
                         --induction_hypothesis_rewriting on/off       选择整数归纳技术中的归纳规则
                          --int_induction_default_bound on/off       在整数归纳规则中选择默认的区间界

                    Eldarica 求解器最早由   Hojjat 等人  [62,70] 于  2013  年在瑞典乌普萨拉大学和瑞士洛桑联邦理工学院         (EPFL) 开
                 发. 它接受  SMTLIB、Prolog  格式的  Horn  子句和部分   Scala 与  C  程序作为输入. 通过结合插值、谓词抽象和反例
                 引导的抽象精化技术来求解程序验证问题. Eldarica 是求解能力最强的                  CHC  求解器之一, 在   2024  年  CHC  求解竞
                 赛  CHC-COMP  中  (Spacer 求解器未参加), Eldarica 在  LIA、LIA-Arrays、LIA-ADT-Arrays 等多个理论背景赛道
                 中求解数最优     [71] . 选取  Eldarica 作为  CHC  求解器的代表之一进行实验, 与其他求解器进行比较, 用以分析在实际
                 样例中   CHC  求解方法在求解递归函数问题时的表现能力与优劣.
                    Spacer 求解器是另一代表性的       CHC  求解器. 它最早由美国卡耐基梅隆大学            (CMU) 的  Komuravelli 等人  [60,61]
                 在  2013  年左右完成原型工具开发. 之后       Gurfinkel 团队与微软研究院的     Bjørner 团队合作将   Spacer 代码进行整合,
                 合并到   Z3  的官方代码库中, 成为     Z3  的核心  CHC  求解引擎. 当输入逻辑为“Horn”时       (SMTLIB  中写作  (set-logic
   48   49   50   51   52   53   54   55   56   57   58