Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
scalaz3 [2011/10/20 16:41] philippe.suter |
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]. | 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 ===== | ===== Paper and Presentation ===== | ||
| Information on (a version) of this library is available in | 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]] | * [[http://lara.epfl.ch/~kuncak/talks/ScalaZ3.ppsx|Powerpoint Slides]] | ||
| ===== 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). | + | 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 55: | Line 56: | ||
| 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). | 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). | ||
| + | |||
| Line 61: | Line 63: | ||
| ===== Authors ===== | ===== 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]]. |