The classical setting of program synthesis has
been to synthesise programs from proofs of logical specifications that relate
the inputs and the outputs of the
program [1]}. Thanks to recent successful trends in formal
verification based on automated reasoning [2]}, [3]}, this
traditional view of program synthesis has been refined to the setting of
syntax-guided synthesis (SyGuS) [4]}. In addition to logical
specifications, SyGuS approaches consider further constraints on the program
template to be synthesised, limiting thus the search space of possible
solutions. A wide range of efficient applications of SyGuS have so far
emerged, for example programming by examples [5]},
component-based synthesis [6]} with learning [7]}
and sketching [8]}.
