JavaSMT 3：在 Java 中与 SMT 求解器交互

满足性模理论（SMT）是一种具有许多应用的使能技术，特别是在计算机辅助验证中。

由于不同的实现具有不同的优势，因此通常需要能够用一个求解器替换另一个求解器。遗憾的是，求解器的 API 大不相同，切换到不同的求解器并不容易（锁定效应）。为了解决这个问题，我们开发了 JavaSMT，这是一个独立于求解器的框架，它统一了使用一组 SMT 求解器的 API。

JavaSMT提供了跨多个后端求解器的通用 API 层来解决这些问题。我们基于 Java 的方法仅产生最小的开销，同时提供对大多数求解器功能的访问。JavaSMT在GitHub上的Apache 2.0许可证下可用。

大多数 SMT 求解器都是用 C/C++ 编写的，因此使用这些低级语言与它们进行交互是最简单的方法。但是，对高级语言的支持很少。几个 SMT 求解器最突出的语言绑定是 Python，因为它直接允许访问 C 代码并避免异步垃圾回收等自动内存管理操作。Java 的绑定可用于某些 SMT 求解器。

PySMT 是一个基于 Python 的项目，旨在使用已安装的 SMT 求解器的本机 API 快速制作算法原型。它能够在没有后端 SMT 求解器的情况下执行公式操作，并且还支持将布尔公式转换为普通 SAT 问题，然后应用 SAT 求解器或 BDD 库。

jSMTLIB 、Scala SMT-LIB 和 ScalaSMT 是用 Java 或 Scala 编写的独立于求解器的库，并通过 SMT-LIB2 与 SMT 求解器进行交互。Scala SMT-LIB 和 ScalaSMT 允许使用额外的领域特定语言与 SMT 求解器交互，并将 Scala 语法重写为有效的 SMT-LIB2 并返回。两者都部分扩展了SMT-LIB2标准。

JavaSMT为各种SMT求解器提供了一个通用的API架构，由几个组件组成： 作为公共上下文，我们使用 SolverContext 来加载底层 SMT 求解器并定义所有已创建对象的范围和生存期。只要上下文可用，我们就会跟踪本机 SMT 求解器库的内存区域。

当上下文关闭时，将释放相应的内存，垃圾回收将擦除所有未使用的对象。在给定的上下文中，JavaSMT提供了用于在各种理论中创建公式的FormulaManager和用于解决SMT查询的ProverEnvironment。

每个 ProverEnvironment 代表一个求解器堆栈，并允许推送/弹出布尔公式并检查它们的满足性（困难部分）。这遵循增量求解的思想（如果底层 SMT 求解器支持它）。在满足性检查之后，ProverEnvironment 提供了接收给定公式的模型、插值或不满足核心的方法。

JavaSMT保证了使用单个FormulaManager构建的公式可以在多个ProverEnvironment中使用，例如，可以将相同的公式推送到多个不同的ProverEnvironment中并求解。与独立 ProverEnvironment的交互从多个线程工作。但是，某些 SMT 求解器需要同步（例如，锁定交错用法），而其他求解器不需要外部同步（这允许并发使用）。

在JavaSMT中可用的八个SMT求解器中，只有Princess 和SMTInterpol “易于”集成，因为它们分别是用Scala和Java编写的。

这些求解器还使用 Java 虚拟机（JVM）的可用内存管理和垃圾回收。所有其他求解器都是用 C/C++ 编写的，需要一个 Java 原生接口 （JNI） 包装器来与 JavaSMT 接口。

对于公式操作，JavaSMT 访问公式的组件，例如运算符和操作数。我们不需要完全访问 SMT 求解器的内部数据结构，而只需要有限地访问最基本的部分。只有 Boolector 不提供必要的 API。

我们贡献了JavaSMT 3，这是用于SMT求解器的第三代统一Java API。该软件包现在包含更多的 SMT 求解器、改进的构建过程以及对 MacOS 和 Windows 的支持。

使用JavaSMT的最突出的应用程序是验证框架CPAchecker（一个广泛使用的软件项目）。仅在 GitHub 上就有 73 个分支），JavaSMT 最初就是为此开发的。

未来，我们计划支持更多的 SMT 求解器、操作系统和硬件架构，同时保持用户界面的稳定性。我们希望更多的Java应用程序的研究人员和开发人员可以通过方便而强大的API从SMT求解中受益。