## 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](https://people.csail.mit.edu/asolar/papers/thesis.pdf) tradition.

Install [Z3](/content/Z3Prover/z3/index.html) with its Python 3 bindings. With Homebrew:

```
$ brew install z3 --with-python
```

Install our only Python dependency, [Lark](/content/lark-parser/lark/index.html):

```
$ 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](http://www.cs.wisc.edu/~aws)'s [primer](http://barghouthi.github.io/2017/04/24/synthesis-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

### Resources

[Readme](/content/sampsyo/minisynth#readme-ov-file/index.html)

### License

[MIT license](/content/sampsyo/minisynth#MIT-1-ov-file/index.html)