We aim to provide a reasonably complete and easy-to-use implementation of Z3 on Racket. The documentation is rather incomplete right now, but here's what's working:
- Basic assertions on integers, booleans, arrays and integer lists
- Custom datatypes: only scalar datatypes supported right now
- Extracting values from generated models
- A few examples, including Sudoku, n-queens, and bounded model checking for quicksort
Check out the tests and examples subdirectories for examples. For a
slightly more involved example, see numbermind,
a small web app written using this library.
Important things to do:
- Better model navigation
- Assertions on other types of lists and other non-scalar datatypes
- More examples, a more comprehensive test suite
- Better debugging and printing
Pull requests are always welcome!
Please see the Downloads section for a downloadable copy of the paper we submitted to TFP'12.
z3.rkt requires Z3 4.0, which you can download for your platform from the
Microsoft Research
site.
We work on Windows, Mac and Linux. You need to copy or create a symlink to z3.dll,
libz3.so or libz3.dylib in this directory.
Licensed under the Simplified BSD License. See the LICENSE file for more details.
Please note that this license does not apply to Z3, only to these bindings.