如何为Z3设置Java开发环境 [英] How to setup a Java development environment for Z3

问题描述

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

How to setup a Java development environment for the Z3 SMT solver?

注意: 作者撰写并回答，请参见我可以回答自己的问题吗?.

推荐答案

• Z3是具有Java绑定的C ++应用程序.首先从 https:/下载本机发行版(在我们的情况下，Ubuntu(适用于macOS))/github.com/Z3Prover/z3/releases ，例如: z3-4.8.7-x64-ubuntu-16.04.zip .

  将内部版本解压缩到 Z3_DIR .为简化起见，请进行以下导出:

  Unzip the build to a Z3_DIR . To simplify things, have the following exports:

   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
  

  如果一切都很好，您应该看到示例在执行时没有错误.

  If all is well, you should see the example executing without errors.

  • 要将Z3 jar与Maven一起使用，请将其安装到本地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
  

  将在< mavenrepo>/repository/com/microsoft/z3/4.8.7/中创建一个名为 z3-4.8.7.jar 的jar.可以将它作为依赖项添加到Maven项目中:

  A jar named z3-4.8.7.jar will be created in <mavenrepo>/repository/com/microsoft/z3/4.8.7/. It can be added to a maven project as dependency:

       <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 .
  • It is nice to have the Z3 API Java sources handy, these are available on Github: https://github.com/Z3Prover/z3/tree/z3-4.8.7/src/api/java . Note that the folder structure doesn't match the package name so you may want to copy the files to com/microsoft/z3 before registering them with an IDE.

  编辑-macOS 不幸的是，在macOS上设置库路径( DYLD_LIBRARY_PATH )不起作用，有关一些详细信息和解决方案，请参见此处:

  EDIT - macOS Unfortunately setting library path (DYLD_LIBRARY_PATH) on macOS doesn't work, for some details and a solution see here: https://github.com/Z3Prover/z3/issues/294

  这篇关于如何为Z3设置Java开发环境的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！