GitXplorerGitXplorer
s

z3.rkt

public
19 stars
11 forks
1 issues

Commits

List of commits on branch master.
Unverified
769a734f9751ba2053bdff194d951ca6b21cea9c

Add the Platinum Blonde Sudoku problem as an example

ssunshowers committed 12 years ago
Unverified
9717bfddc399127f286f1f3d9b14b60ff483b568

Remove note about the doc directory and add one about the Downloads section

ssunshowers committed 12 years ago
Unverified
64a0b99d2fdd6c81234803a38dd9f855dbe8f2b7

Remove doc subdirectory

ssunshowers committed 12 years ago
Unverified
a2525e75fbadb9a89de83e98c9cd8744a4cd539f

Add a comment about config arguments

ssunshowers committed 12 years ago
Unverified
2407478a58b696bf73449bd6182960da9ba7fd73

Fix the contract and add an error for arity

ssunshowers committed 12 years ago
Unverified
054fb5e79f06d97fe68219d3febf48f63bc9038e

Add support for arbitrary keyword arguments

ssunshowers committed 12 years ago

README

The README file for this repository.

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.