##
The Problem

The Syntax-Guided Synthesis problem (SyGuS, in short) is specified with respect to a background theory T such as Linear-Integer-Arithmetic that fixes the types of variables, operations on types, and their interpretation.

To synthesize a function f of a given type, the input consists of
(1) a semantic constraint given as a formula \(\varphi\) built from symbols in T along with f, and (2) a syntactic constraint given as a set E of expressions from theory T specified by a context-free grammar. The computational problem then is to find an expression e in E so that the specification \(\varphi\)[f/e] is valid.

Here is a small example. Here is the full syntax.

You can find more details (papers, slides and talks) here.

The public benchmarks as well as three initial solvers (enumerative, symbolic, and stochastic) are available in StarExec for you to experiment with. The initial solvers initial solvers source code, as well as source code of parser for SyGuS-IF are available on github.