Cozy 1

1. how does auto-tune happen? What is tuned?
2. how is a program synthesized? (enumeration and some checks to filter out illegal ones)

Efficient implementation of this retrieval operation requires the use of an interval tree, a collection that is not found in any common collections library.

synthesize outlines, pick data representations, and generate concrete code

it looks like that outline is very functional. AllWhere doesn't make sense in one look. but the concept of guard is very interesting.

? cleanup(cache, examples)

the cost model cost allows many candidate programs to be dropped in calls to cleanup , pruning the search space drastically.

About CEGIS: split the hard program into two simpler ones: synthesizer and verifier

1. the synthesizer takes a finite set of input exampels and finds P such that P behaves correctly on the given examples.
2. the verifier either proves that P is correct or finds a concrete counter-example i

The cleanup procedure groups programs by equivalence class based on their behavior on the examples and sorts each equivalence class by cost. Whenever two programs in an equivalence class have different costs cleanup removes the worse one. These optimizations never cause Cozy to skip plans since the cost model is monotonic.