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.



The source code is hosted on GitHub at

The artifact for the POPL 2016 paper is available here.