java - 将 Java 与 Z3 集成

Question

我想问一下，如何将 Java 与 SMT Z3 求解器集成？如果不仅要描述理论问题，而且还要描述一些实施经验，那就太好了。

Answer 1

不确定您正在寻找什么样的集成，但我想我应该提到我们目前正在为 Z3 开发 Java API。这可以在 Z3 的不稳定分支中预览，在Z3 最新源代码中获得。这还没有在任何二进制包中分发，因此您必须自己构建源代码。它基本上以 jar 包 (+DLL) 的形式提供，源代码附带了如何在示例/java 中使用它的示例。