| Summary: | <p>Program synthesis is the mechanised construction of software. One of the main difficulties is the efficient exploration of the very large solution space, and tools often require a user-provided syntactic restriction of the search space. Writing such templates is often challenging, particularly since any constants required in the solution must be given in the template. In this dissertation we explore the research hypothesis that synthesis of programs without provision of such syntactic templates is computationally feasible using methods based on CounterExample Guided Inductive Synthesis (CEGIS). </p>
<p>The key contribution of this dissertation is a new approach to program synthesis that combines the strengths of a counterexample-guided inductive synthesizer with those of a theory solver, exploring the solution space more efficiently without relying on user guidance. We call this approach CEGIS(T ), where T is a first-order theory. Notably, since the publication of CEGIS(T ), a variant of the algorithm has been implemented inside leading synthesis solver CVC4. CEGIS(T) is as complete (or incomplete) as CEGIS, and it does not affect worst-case run-time complexity considerations. </p>
<p>In combination with the development of CEGIS(T ), we introduced several algorith- mic improvements that enhance both the performance of CEGIS(T ) and the baseline CEGIS algorithm. The first of these improvements is a significant change to the way we encode the synthesis problem for the SAT-based synthesis component of CEGIS in order to produce smaller formulae that can be more efficiently solved by SAT and SMT solvers. The second of these improvements is the use of incremental satisfiability solving in the synthesis component of CEGIS. Incremental satisfiability solving allows the SAT solver to re-use clauses learnt in previous CEGIS iterations, thus reducing the time per synthesis iteration.</p>
<p>We evaluate our contributions on a set of benchmarks taken from the Syntax Guided Synthesis Competition, and note that CEGIS(T ) is able to solve benchmarks which elude a standard implementation of CEGIS, specifically benchmarks that contain non-trivial constants. We find that the novel proposed encoding provides a substantial speed-up on all the benchmarks that require synthesising a program of length greater than one instruction. The use of incremental first-order solving in CEGIS decreases the solving time in some cases but not all, and we hypothesise that these are the benchmarks on which SAT-solver pre-processing is less important.</p>
|
|---|