Many applications of program synthesis require generated programs to optimal with respect to a desired cost metric, such as program size. This project develops metasketches, a general framework for specifying and solving optimal synthesis problems. Metasketches make the search strategy a part of the problem definition by specifying a fragmentation of the search space into an ordered set of classic sketches. We provide two cooperating search algorithms to effectively solve metasketches. A global optimizing search coordinates the activities of local searches, which execute an incremental form of counterexample-guided inductive synthesis to incorporate information sent from the global search. Synapse is an implementation of these algorithms that effectively solves optimal synthesis problems with a variety of different cost functions. In addition, metasketches can be used to accelerate classic (non-optimal) synthesis by explicitly controlling the search strategy, and Synapse solves classic synthesis problems that state-of-the-art tools cannot.
James Bornholt, Emina Torlak, Dan Grossman, and Luis Ceze. Optimizing Synthesis with Metasketches. In Proceedings of the 43rd ACM Symposium on Principles of Programming Languages (POPL), Jan 2016. [pdf] [slides]
The source code is hosted on Github at https://github.com/uwplse/synapse.
The artifact for the POPL 2016 paper is available here.