如何为Z3设置Java开发环境

Question

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

注意：本文由作者撰写和回答，详见我可以回答自己的问题吗？。

- David Soroko

Answer 1

• Z3是一个带有Java绑定的C++应用程序。首先从https://github.com/Z3Prover/z3/releases下载本机分发版，例如Ubuntu（类似的方法也适用于macOS），例如：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示例，编译并运行：

$ 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

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

• 要在Maven中使用Z3 jar，请将其安装到本地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-4.8.7.jar的jar包创建在<mavenrepo>/repository/com/microsoft/z3/4.8.7/中。它可以作为依赖项添加到Maven项目中：

     <dependency>
         <groupId>com.microsoft</groupId>
         <artifactId>z3</artifactId>
         <version>4.8.7</version>
     </dependency>

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

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

- David Soroko

Answer 2

Z3-TurnKey是一个很好的项目，它发布了一个Maven构件，其中包含预先构建的本地库，用于OS X、Windows和Linux，在运行时进行链接。

- breandan