Smtlink 2.0

Smtlink 是 ACL2 结合可满足性模理论（Satisfiability Modulo Theories, SMT）求解器的扩展。我们曾在 ACL2'2015 上展示过其早期版本。Smtlink 2.0 在可靠性、可扩展性、易用性以及所支持的类型范围和关联理论求解器方面相较初始版本做了重大改进。大多数希望使用 SMT 求解器证明的定理必须首先被翻译为仅使用 SMT 求解器支持的基元操作——该翻译包括函数展开和类型推断。Smtlink 2.0 通过使用由已验证子句处理器和计算提示执行的一系列步骤来进行此翻译。这些步骤被确保是可靠的。从 ACL2 到 Z3 的 Python 接口的最终音译需要一个可信子句处理器。这相比最初作为单一、整体式可信子句处理器实现的 Smtlink 在可靠性和可扩展性上是一大改进。Smtlink 2.0 通过使用 Z3 的数组和用户自定义数据类型，提供了对 FTY defprod、deflist、defalist 和 defoption 类型的支持。我们已识别出常见使用模式，并简化了使用 Smtlink 所需的配置和提示信息。