Differences

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

--- jniz3 [2011/07/29 16:36]
philippe.suter
+++ jniz3 [2011/08/03 14:37]
vkuncak
@@ Line 1: / Line 1: @@
-====== Scala^Z3: Integration of Scala and Z3 ======
+====== Redirect ======
-===== Distribution =====
-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.
-===== Installation =====
-You can get the sources from [[http://github.com/psuter/ScalaZ3|GitHub]]. We also plan to make precompiled versions available for download in the future.
-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.19 (we have not seen changes in the API since version 2.11, though).
-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 (''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.).
-===== Applicability =====
-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).
-==== 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]].
+See [[scalaz3|this page]].