Synthesising programs with non-trivial constants

Alessandro Abate, Haniel Barbosa, Clark Barrett, Christina David*, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds, Cesare Tinelli

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

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. While useful in general, such syntactic restrictions provide little help for the generation of programs that contain non-trivial constants, unless the user is able to provide the constants in advance. This is a fundamentally difficult task for state-of-the-art synthesisers. We propose a new approach to the synthesis of programs with nontrivial constants that combines the strengths of a counterexample-guided inductive synthesiser 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 afirst-order theory. We present two exemplars, one based on Fourier-Motzkin (FM)variable elimination and one based on first-order satisfiability. We demonstrate the practical value of CEGIS(T ) by automatically synthesising programs for a set of intricate benchmarks. Additionally, we present a case study where we integrate CEGIS(T ) within the mature synthesiser CVC4 and show that CEGIS(T ) improves CVC4’s results.
Original languageEnglish
Article number19
Pages (from-to)1-25
JournalJournal of Automated Reasoning
Issue number2
Publication statusPublished - 13 May 2023


Dive into the research topics of 'Synthesising programs with non-trivial constants'. Together they form a unique fingerprint.

Cite this