Synapse

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.

Publications

• James Bornholt, Emina Torlak, Dan Grossman, and Luis Ceze. Optimizing Synthesis with Metasketches. In Proc. of the 43rd ACM Symposium on Principles of Programming Languages (POPL), Jan 2016. [pdf] [slides]

Software

The source code is hosted on GitHub at https://github.com/uwplse/synapse.

The artifact for the POPL 2016 paper is available here.