The sources are now available on GitHub. Please use GitHub's issue tracker to report bugs or suggest improvements. Questions should be asked on Stack Overflow, preferably tagged with [z3] and [scala].

The Scala API is available at http://lara.epfl.ch/~psuter/jniz3/. You probably want to look at the classes Z3Context to start, and Z3Theory if your interest is to write theory plugins. The function names are usually very close to their C equivalent (you can consult the C API here). One notable difference is that functions return multiple arguments when needed rather than using by-reference arguments. This convention is applied systematically. Not all functions in the C API have a Scala equivalent yet (for instance, bit-vectors have no counterpart yet).

Examples of usage of Z3 from Scala can be found here.

We're not actively developing the Java library. However, the JNI bindings are common for the Scala and Java API, so the effort required to write the Java library is minimal (eg. you do not need to know anything about the JNI). Let us know if you are interested in doing that.

You can get the latest z3.jar (including the Scala class files, the Java class files and the C bindings) from here. Note that we don't currently distribute the sources.

You'll need the shared library libz3.so or z3.dll. See Microsoft Research's website http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html.

Currently, the bindings are compiled against Z3 2.15 (we have not seen changes in the API since version 2.11, though). Note that the Linux version reports 2.16 as the version number.

We try hard to make all functions safe by wrapping Z3 pointers into proper classes, so that all calls can by typechecked by Scala/Java. However, there are always ways to break things. Be aware of the following (from: G. Tan et al., Safe Java Native Interface, IEEE Symp. on Secure Software Engineering, 2006):

“When a type-safe language interacts with an unsafe language in the same address space, in general, the overall application becomes unsafe.”

You have been warned.

When you use the jar file, it will unpack the required native bindings (libjniz3.so for *nix variants, and jniz3.dll for Windows) to a temporary directory. This is required for the JVM to be able to load the library, as it can only load libraries from the OS file system. A directory JNIZ3_????-??-??, where the question marks are replaced by the date, is created in the default temporary directory (/tmp/, C:\users\UserName\AppData\Local\Temp for Windows 7, etc.). Warning: currently, if you use two different versions of z3.jar the same day, you run the risk of triggering UnsatisfiableLinkError exceptions. We will probably fix this in future releases by attaching the version number to the temporary directory.

The current version works on architectures running a variant of Linux or Windows. We have not personally tested the library on 64bit architectures yet and would appreciate any feedback on that subject. In theory, it should work.

Aside from the z3.dll shared library, you will need two libraries that come as part of the Microsoft Visual C++ 2010 Redistributable Package.

Z3 is written and maintained by Microsoft Research. The project is lead by Leonardo de Moura and Nikolaj Bjørner. The Scala interface and JNI bindings are written by Philippe Suter, with contributions from Ali Sinan Köksal and Robin Steiger.

(The following is a non-exhaustive list of changes.)

1.1   2010-12-03   Included DLL for Windows, Z3AST instances can be built easily from others using overloaded operators, support for the SMT LIB parser interface.
1.0   2010-09-16   Initial release.