third and fourth competitions consisted, in addition to these three
tracks, the PBE track for programming
by examples. The PBE track restricts
semantic constraints to be based
upon only input–output examples.
This track is divided into two: benchmarks using the BV logic, and benchmarks manipulating strings
expressed in the SLIA logic.
The ESolver based on the enumerative search strategy described previously won the first competition. Since
then a number of researchers have
proposed new solution strategies. For
instance, the ICE-DT solver is specialized to learning invariants based on a
novel idea of generalizing from implication counterexamples (as opposed
just positive and negative examples
common in classical learning), and
won the INV track in recent competitions, 8 and the strategy to solve alternation of quantifiers within the SMT
solver CVC4 was modified to produce
witness functions that match the syntactic template leading to a SyGuS
solver that is the most effective current solver for the CLIA and PBE-String tracks. 25 The winner of the
general track in the 2017 competition
is EUSolver, which we will explore.
State of the Art
The formalization of the SyGuS problem and organization of the annual
competition of solvers has been a catalyst for research in search-based program synthesis. We first give an
overview of the progress in solver
technology, then describe the solution strategy employed by the current
winner, and explain a novel application of SyGuS to synthesis of cryptographic circuits resistant to timing
attacks.
Evolution of SyGuS solvers. The
capabilities of SyGuS solvers are
improving from competition to competition. For instance, all instances of
the ICFP benchmarks were solved in
2017 competition, most in less than
10 seconds. In contrast, none of these
were solved in the first competition,
and in the original ICFP competition,
some of these benchmarks were
solved by the participants using enormously large compute clusters.
As another example, recall the
example given earlier of synthesizing
the maximum of two numbers using
the grammar Exp3. For any number n,
we can similarly write a specification
for computing the maximum of n
input arguments. In the first competi-
tion all solvers were able to solve for n
= 2, only one solver was able to solve
for n = 3 and none could solve for n = 4.
The 2017 solvers are capable of solv-
ing for n ≤ 21. Note that the size of the
minimal expression grows quadrati-
cally with n. The size of the expression
generated for n = 21 is 1621. With
regard to the time to solve these
benchmarks, instances with n ≤ 10
are solved within 5s, whereas the solu-
tion for n = 21 required 2100 s.
Trying to understand which SyGuS
instances are easily solved by current
SyGuS solvers, we recall different
aspects of a SyGuS instance: (i) The
grammar can be very general or very
restrictive, depending on the size of
the set of syntactically allowed expres-
sions. (ii) The specification can
require a single or multiple functions
to be simultaneously synthesized. (iii)
The specification can be complete or
partial depending on whether the set
of semantic solutions is a singleton or
not. (iv) The grammar may or may not
allow the use of let for specifying
auxiliary variables. (v) When the spec-
ification has several invocations of
the function to be synthesized, all
invocations may be exactly the same
(in the sense that the sequence of
parameters is the same in all) or there
may be different ways in which the
function is invoked. We refer to the
former as single invocation and to the
latter as multiple invocation. 25 The cat-
egories of benchmarks in which state-
of-the-art solvers excel are those with
a single function invocation, a single
function to synthesize, a complete
specification, no use of let, and a
restricted grammar. Benchmarks of
the CLIA and invariant generation
tracks are also easily handled by cur-
rent solvers, in spite of their grammar
being general.
Enumerative search with decision
trees. When the grammar specifying
the set of allowed expressions
includes conditionals, the desired
solution is typically a tree whose inter-
nal nodes are labeled with tests used
in conditionals and leaves are labeled
with test-free expressions. The key
The formalization of
the SyGuS problem
and organization
of the annual
competition of
solvers has been
a catalyst for
research in search-
based program
synthesis.