如何为 Z3 设置 Java 开发环境

Question

如何为 Z3 SMT 求解器设置 Java 开发环境？

注意： 由作者撰写并回答，请参阅我可以回答我自己的问题吗？.

Answer 1

• Z3 是一个带有 Java 绑定的 C++ 应用程序。通过下载本机分布的，Ubuntu在我们的例子（类似的方法应该适用于MacOS工作），从开始 https://github.com/Z3Prover/z3/releases，例如：z3-4.8.7-x64-ubuntu-16.04.zip。

• 将构建解压缩到Z3_DIR. 为了简化事情，有以下出口：

 export Z3_DIR=<some_path>/z3-4.8.7-x64-ubuntu-16.04
 export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:$Z3_DIR/bin

• 下载与您的 Z3 版本匹配的 Java 示例，编译并运行它：

 export Z3_DIR=<some_path>/z3-4.8.7-x64-ubuntu-16.04
 export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:$Z3_DIR/bin

如果一切顺利，您应该会看到示例执行时没有错误。

• 要将 Z3 jar 与 Maven 一起使用，请将其安装到本地 Maven 存储库中：

$ curl https://raw.githubusercontent.com/Z3Prover/z3/z3-4.8.7/examples/java/JavaExample.java > JavaExample.java
$ javac -cp $Z3_DIR/bin/com.microsoft.z3.jar JavaExample.java
$ java -cp $Z3_DIR/bin/com.microsoft.z3.jar:. JavaExample

命名为A罐子z3-4.8.7.jar将创造<mavenrepo>/repository/com/microsoft/z3/4.8.7/。它可以作为依赖项添加到 Maven 项目中：

$ mvn install:install-file \
   -Dfile=$Z3_DIR/bin/com.microsoft.z3.jar \
   -DgroupId=com.microsoft \
   -DartifactId=z3 \
   -Dversion=4.8.7 \
   -Dpackaging=jar \
   -DgeneratePom=true

• 很高兴有 Z3 API Java 源代码，它们可以在 Github 上找到：https : //github.com/Z3Prover/z3/tree/z3-4.8.7/src/api/java。请注意，文件夹结构与包名称不匹配，因此您可能希望在将文件com/microsoft/z3 注册到 IDE 之前将其复制到。

编辑 - macOS 不幸的是，DYLD_LIBRARY_PATH在 macOS 上设置库路径 ( ) 不起作用，有关详细信息和解决方案，请参见此处：https : //github.com/Z3Prover/z3/issues/294