Differences

This shows you the differences between two versions of the page.

--- jniz3 [2011/07/29 16:31]
philippe.suter
+++ jniz3 [2011/08/03 14:37]
vkuncak
@@ Line 1: / Line 1: @@
-====== Scala^Z3: Integration of Scala and Z3 ======
-===== Distribution =====
+See [[scalaz3|this page]].
-The sources are now available on [[https://github.com/psuter/ScalaZ3|GitHub]]. Please use GitHub's issue tracker to report bugs or suggest improvements. Questions should be asked on [[http://stackoverflow.com/|Stack Overflow]], preferably tagged with [z3] and [scala].
-===== 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 [[http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html|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 ====
-Examples of usage of Z3 from Scala can be found [[jniz3-scala-examples|here]].
-===== Java =====
-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.
-===== Download =====
-You can get the latest ''z3.jar'' (including the Scala class files, the Java class files and the C bindings) from [[http://lara.epfl.ch/~psuter/jniz3|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.
-===== Temporary Files =====
-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.
-===== Applicability =====
-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.
-==== Windows Usage Notes ====
-Aside from the ''z3.dll'' shared library, you will need two libraries that come as part of the
-[[http://www.microsoft.com/downloads/en/details.aspx?displaylang=en&FamilyID=a7b7a05e-6de6-4d3a-a423-37bf0912db84|Microsoft Visual C++ 2010 Redistributable Package]].
-===== Authors =====
-Z3 is written and maintained by Microsoft Research. The project is lead by [[http://research.microsoft.com/~leonardo|Leonardo de Moura]] and [[http://research.microsoft.com/~nbjorner|Nikolaj Bjørner]]. The Scala interface and JNI bindings are written by [[http://lara.epfl.ch/~psuter/|Philippe Suter]], with contributions from [[http://people.epfl.ch/alisinan.koksal|Ali Sinan Köksal]] and [[http://people.epfl.ch/robin.steiger|Robin Steiger]].
-===== Change Log =====
-(The following is a non-exhaustive list of changes.)
-.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.
-.0   2010-09-16   Initial release.