Synthesising Programs with Non-trivial Constants

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 non-trivial 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( 𝒯 ), where 𝒯 is a first-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( 𝒯 ) by automatically synthesising programs for a set of intricate benchmarks. Additionally, we present a case study where we integrate CEGIS( 𝒯 ) within the mature synthesiser CVC4 and show that CEGIS( 𝒯 ) improves CVC4’s results.