将 Java 与 Z3 集成 [关闭]答案

【问题标题】：Integrating Java with Z3 [closed]将 Java 与 Z3 集成 [关闭]
【发布时间】：2013-01-25 18:19:40
【问题描述】：

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

【问题讨论】：

基本上你要求人们为你做研究和工作。
互联网上有很多关于这些主题的信息。您可以进行研究，尝试一些事情，如果遇到特定问题，您可以提出问题。比如这个问题：stackoverflow.com/questions/12883107/…
你的意思是，这可行吗？非常感谢您的帮助
可能，但我的意思是你应该做一些研究并尝试一些事情。
好的，有什么问题我就放这里

【解决方案1】：

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

【讨论】：

我有一组数组列表。我想使用 Z3 编写一个约束来从这些数组列表中检索数据