cvc5 1.3.0版本发布：安全模式与证明能力显著增强

cvc5是一个高性能的开源SMT（可满足性模理论）求解器，广泛应用于形式化验证、程序分析、软件测试等领域。作为SMT求解器领域的佼佼者，cvc5能够处理包括算术、位向量、数组、字符串等多种理论约束。最新发布的1.3.0版本带来了多项重要改进，特别是在安全性和证明能力方面有显著提升。

安全模式与稳健性保障

cvc5 1.3.0引入了一个重要的新功能——安全模式（safe mode）。这一模式通过构建配置选项或命令行参数启用，会限制所有不够稳健或缺乏完整证明和模型支持的功能。安全模式的定义与项目的模糊测试指南保持一致，确保了在该模式下运行的功能都经过了严格的验证。

开发者可以通过两种方式启用安全模式：

1. 在构建时使用safe-mode配置选项
2. 运行时通过命令行参数--safe-mode=safe启用

此外，cvc5还提供了--safe-mode=stable选项，该选项会禁用实验性功能，但不强制要求完整的证明或模型支持。这一设计使得用户可以根据实际需求在功能完整性和安全性之间做出权衡。

证明能力大幅提升

在证明系统方面，cvc5 1.3.0对Cooperating Proof Calculus（CPC）证明格式的支持有了显著增强。现在，CPC证明对于安全模式下允许的所有理论和功能都应该是完整的。这意味着用户可以更有信心地依赖这些证明结果。

获取这些证明的方式包括：

• 使用SMT-LIB命令(get-proof)
• 通过API调用Solver::getProof方法

这些证明可以通过Ethos 0.2.0检查器进行验证。值得注意的是，cvc5现在默认使用dsl-rewrite级别的证明粒度，这提供了更细致的证明结构。

算术位向量转换函数的标准化

cvc5 1.3.0开始支持SMT-LIB 2.7标准中定义的算术位向量转换函数语法：

• int_to_bv：对应现有的Kind::INT_TO_BITVECTOR
• ubv_to_int：新增Kind::BITVECTOR_UBV_TO_INT
• sbv_to_int：新增Kind::BITVECTOR_SBV_TO_INT

同时，旧语法int2bv和bv2nat以及对应的Kind::BITVECTOR_TO_NAT已被标记为废弃，建议用户迁移到新的标准语法。

内部改进与优化

在底层实现方面，cvc5 1.3.0包含了多项改进：

• 将CaDiCaL求解器升级至2.1.3版本
• 改进了证明输出格式，现在所有证明输出都会用括号括起来，符合SMT-LIB标准
• 重命名了量化实例化策略--mbqi-fast-sygus为--mbqi-enum，使其命名更加准确

总结

cvc5 1.3.0版本在安全性、证明能力和标准合规性方面都取得了重要进展。安全模式的引入为用户提供了更可靠的运行环境，CPC证明的增强使得验证结果更加可信，而对SMT-LIB 2.7标准的更好支持则提升了工具的互操作性。这些改进使得cvc5在形式化方法和验证领域的应用更加广泛和可靠。