Logo image
Back
Synthesising Programs with Non-trivial Constants
Journal article   Open access   Peer reviewed

Synthesising Programs with Non-trivial Constants

Alessandro Abate, Haniel Barbosa, Clark Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds and Cesare Tinelli
Journal of automated reasoning, Vol.67(2), pp.19-19
2023
DOI: 10.1007/s10817-023-09664-4
PMCID: PMC10182957
PMID: 37193313
url
https://doi.org/10.1007/s10817-023-09664-4View
Published (Version of record) Open Access

Abstract

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(T), where T 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(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.
 Automated reasoning Counterexample guided inductive synthesis Program synthesis Satisfiability modulo theories

Details

Metrics

63 Record Views
2 Times Cited - Web of Science
Logo image