cvc5 1.2.1版本发布：SMT求解器的安全性与证明能力提升

cvc5是一款开源的SMT(Satisfiability Modulo Theories)求解器，它能够处理一阶逻辑公式的可满足性问题，并支持多种理论组合。作为自动化推理领域的重要工具，cvc5广泛应用于形式化验证、程序分析、人工智能等领域。最新发布的1.2.1版本在证明系统、安全性选项和语言解析等方面带来了多项改进。

证明系统增强

cvc5 1.2.1版本对CPC证明签名进行了更新，使得Ethos 0.1.1版本能够验证cvc5生成的证明。这一改进增强了证明系统的兼容性和可靠性，为形式化验证提供了更坚实的基础。

此外，新版本显著扩展了证明覆盖范围，特别是在启用--safe-options选项时允许的理论范围内。这意味着用户在使用安全选项时，能够获得更全面的证明支持，增强了系统的可信度。

安全性选项优化

1.2.1版本对--safe-options选项进行了重要调整，现在该选项会默认禁用实验性理论及其扩展。这些实验性理论包括：

• 包(bag)理论
• 有限域理论
• 分离逻辑理论
• 高阶等式理论扩展
• 算术理论中的超越函数、整数与运算和幂函数扩展
• 数组理论中的常量数组扩展

值得注意的是，这些理论在默认情况下仍然是启用的。如果用户确实需要使用这些实验性理论，可以在设置--safe-options之前，通过特定选项(如--arith-exp)来启用它们。

API与功能增强

新版本在API层面增加了SymbolManager::getNamedTerms()方法，允许用户检索通过SMT-LIB属性:named命名的术语集合。这一功能增强了符号管理的灵活性，便于用户跟踪和操作特定术语。

在解析方面，新增了--parsing-mode选项，提供了比默认模式更严格或更宽松的解析配置。原有的--strict-parsing选项现在作为--parsing-mode=strict的别名存在。在宽松解析模式下(--parsing-mode=lenient)，系统能够解析以.或@开头的符号，这些符号通常用于内部新引入的符号表示。

其他重要改进

1.2.1版本修复了set.filter求解器中的一个正确性缺陷，确保了该操作的语义准确性。在输出方面，当使用-o pre-asserts或-o post-asserts标签打印时，系统现在会确保声明以确定性顺序输出，提高了结果的可预测性。

此外，cvc5将内置的CaDiCaL SAT求解器升级到了2.0.0版本，这一更新可能会带来性能上的提升和功能上的改进。

总结

cvc5 1.2.1版本通过增强证明系统、优化安全选项、扩展API功能和改进解析能力，进一步提升了这一SMT求解器的可靠性和实用性。特别是对实验性理论的明确划分和安全选项的调整，使得用户能够更清晰地控制系统的行为，在保证安全性的同时不牺牲灵活性。这些改进使得cvc5在形式化验证和相关领域的应用中更加值得信赖。