How to setup a Java development environment for Z3

Question

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

Note: Written and answered by the author, see Can I answer my own question?.

Potboy

Answer 1

• Z3 is a C++ application with Java bindings. Start by downloading the native distribution, Ubuntu in our case (similar approach should work for macOS), from https://github.com/Z3Prover/z3/releases , for example: z3-4.8.7-x64-ubuntu-16.04.zip.

• 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

• Download the Java example that matches your Z3 version, compile and run it:

$ 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.

• To use the Z3 jar with Maven, install it into the local maven repository:

$ 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

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>

• 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.

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

Potboy

Answer 2

Z3-TurnKey is a nice project which publishes a Maven artifact containing prebuilt native libraries for OS X, Windows and Linux which are linked at runtime.

Bedelia