Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Racket bindings for Z3
Racket
Branch: master

Fetching latest commit…

Cannot retrieve the latest commit at this time

Failed to load latest commit information.
examples
tests
.gitattributes
.gitignore
.hgignore
LICENSE
README.md
builtins.rkt
derived.rkt
main.rkt
parser.rkt
run-tests.rkt
utils.rkt
z3-wrapper.rkt
z3.rkt.sublime-project

README.md

z3.rkt: Racket bindings for Z3

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.

Installing

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.

License

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.

Something went wrong with that request. Please try again.