how to do synthesis about souper HOT 5 CLOSED

Note that using the simplest cost function (number of instructions) we have no way to prefer "add nsw" over "add". So I suspect we'll need something a bit more fine-grained.

from souper.

A few more papers to read:
http://research.microsoft.com/en-us/um/people/sumitg/pubs/oopsla10_synthesis.pdf
http://people.csail.mit.edu/asolar/papers/asplos06-final.pdf
http://www.eecs.berkeley.edu/~sseshia/pubdir/synth-icse10.pdf

from souper.

As far as I can tell none of these papers is handing quantifiers to the solver, but rather they're doing guess-verify loops where each iteration adds a counterexample.

from souper.

I think my patch #167 is ready for the initial review. Please give the synthesis a try and let me know if you encounter any problems. You must use z3 or any other solver that produces models.

from souper.

Implemented in 21ed266.

from souper.