program synthesis is possible
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Type Name Latest commit message Commit time
Failed to load latest commit information.


These are supporting materials for a lecture on program synthesis in the Sketch tradition.

Install Z3 with its Python 3 bindings. With Homebrew:

$ brew install z3 --with-python

Install our only Python dependency, Lark:

$ pip3 install --user lark-parser

Witness the magic of Z3:

$ python3

Run a simple example to see how to synthesize values, which is stolen from Aws Albarghouthi's primer:

$ python3

Run a more complete synthesis engine for a little arithmetic language:

$ python3 < sketches/s1.txt