Folders and files
| Name | Last commit message | Last commit date |
|---|---|---|
| [README.md](/content/sampsyo/minisynth/blob/master/README.md "README.md"/index.html) | [Use pip3](/content/sampsyo/minisynth/commit/ed614d2e87f742faa524e4cbd74001485a65dd5c "Use pip3"/index.html) | 8 years agoMay 9, 2018 |
| [ex0.py](/content/sampsyo/minisynth/blob/master/ex0.py "ex0.py"/index.html) | [Add tiny little Z3 examples](/content/sampsyo/minisynth/commit/567f8609c69ce6892699151cc90fdb90dae49686 "Add tiny little Z3 examples"/index.html) | 8 years agoMay 8, 2018 |
| [ex1.py](/content/sampsyo/minisynth/blob/master/ex1.py "ex1.py"/index.html) | [Solve function](/content/sampsyo/minisynth/commit/23e9e848a355ee55e47d6c39e617fc83820ab6b8 "Solve function"/index.html) | 8 years agoMay 8, 2018 |
| [ex2.py](/content/sampsyo/minisynth/blob/master/ex2.py "ex2.py"/index.html) | [Move optimization to AST traversal](/content/sampsyo/minisynth/commit/8f90200670eff678512de030b9fbe19eb66658e2 "Move optimization to AST traversal"/index.html) | 7 years agoMay 5, 2019 |
| [ex3.py](/content/sampsyo/minisynth/blob/master/ex3.py "ex3.py"/index.html) | [Move optimization to AST traversal](/content/sampsyo/minisynth/commit/8f90200670eff678512de030b9fbe19eb66658e2 "Move optimization to AST traversal"/index.html) | 7 years agoMay 5, 2019 |
minsynth
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 ex0.py
Run a simple example to see how to synthesize values, which is stolen from Aws Albarghouthi's primer:
$ python3 ex1.py
Run a more complete synthesis engine for a little arithmetic language:
$ python3 ex2.py < sketches/s1.txt
About
program synthesis is possible