Differences

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

--- scalaz3 [2011/08/03 14:44]
vkuncak
+++ scalaz3 [2012/02/27 12:30]
philippe.suter
@@ Line 4: / Line 4: @@
 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].
 ===== Paper and Presentation =====
 Information on (a version) of this library is available in
-  * [[http://lara.epfl.ch/~kuncak/papers/KoeksalETAL11ScalaZ3.html|CADE System Description]]
+  * A.S. Köksal, V. Kuncak, P. Suter. //Scala to the Power of Z3//. CADE 2011 (System Description) [[http://lara.epfl.ch/~kuncak/papers/KoeksalETAL11ScalaZ3.html|PDF]]
   * [[http://lara.epfl.ch/~kuncak/talks/ScalaZ3.ppsx|Powerpoint Slides]]
 ===== 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).
+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 [[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).
@@ Line 26: / Line 27: @@
 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.
@@ Line 35: / Line 37: @@
 ===== 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 can get the sources from [[http://github.com/psuter/ScalaZ3|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 2.19 (we have not seen changes in the API since version 2.11, though).
+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):
@@ Line 55: / Line 57: @@
 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^Z3 interface and the 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]].
+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^Z3 interface and the JNI bindings are written by [[http://lara.epfl.ch/~psuter/|Philippe Suter]], with contributions from [[http://www.eecs.berkeley.edu/~koksal/|Ali Sinan Köksal]] and [[http://people.epfl.ch/robin.steiger|Robin Steiger]].