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

Information on (a version) of this library is available in

• A.S. Köksal, V. Kuncak, P. Suter. Scala to the Power of Z3. CADE 2011 (System Description) PDF
• Powerpoint Slides

The Scala API is available at http://lara.epfl.ch/~psuter/ScalaZ3/. 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 sources from GitHub. Precompiled versions are also available from there.

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

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 (libscalaz3.so for *nix variants, and scalaz3.dll for Windows) in 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 SCALAZ3_??????, where the question marks are replaced by a hash of the library version, is created in the default temporary directory (/tmp/, C:\users\UserName\AppData\Local\Temp for Windows 7, etc.).

The current version works on architectures running a variant of Linux or Windows. It works regardless of the underlying architecture (32 or 64bit), *as long as* the JVM uses the same architecture: you cannot use the library with a 32bit JVM running on a 64bit machine).

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