A Divide-and-Conquer Approach to Syntax-Guided Synthesis

Program synthesis aims to generate programs automatically from user-provided specifications. One critical research thrust is called Syntax-Guideds Synthesis. In addition to semantic specifications, the user should also provide a syntactic template of the desired program, which helps the synthesizer reduce the search space. The traditional symbolic approaches, such as CounterExample-Guided Inductive Synthesis (CEGIS) framework, does not scale to large search spaces. The goal of this project is to explore a compositional, divide-n-conquer approach that heuristically divides the synthesis task into subtasks and solves them separately. The idea is to decompose the function to be synthesized by creating a set of auxiliary functions. In this way, the whole synthesis task can be reduced to synthesizing the auxiliary functions. The auxiliary functions are of bounded size and hence can be encoded into a logic constraint in linear-integer arithmetic and solved by modern Satisfiability-Modulo-Theories (SMT) solvers. In each iteration of the synthesis algorithm, an auxiliary function is synthesized and added into the syntax for synthesizing other auxiliary functions. The algorithms repeats until a syntax-correct implementation equivalent to the reference implementation is found. Preliminary experimental results show that this approach is promising