Treffer: Synthesising Programs with Non-trivial Constants
Abate, A, Barbosa, H, Barrett, C, David, C, Kesseli, P, Kroening, D, Polgreen, E, Reynolds, A & Tinelli, C 2023, ' Synthesising programs with non-trivial constants ', Journal of Automated Reasoning, vol. 67, no. 2, 19, pp. 1-25 . https://doi.org/10.1007/s10817-023-09664-4
0168-7433
URL: http://creativecommons.org/licenses/by/4.0/Open AccessThis article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/ (http://creativecommons.org/licenses/by/4.0/) .
Weitere Informationen
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($$\mathcal {T}$$ T ), where $$\mathcal {T}$$ 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($$\mathcal {T}$$ T ) by automatically synthesising programs for a set of intricate benchmarks. Additionally, we present a case study where we integrate CEGIS($$\mathcal {T}$$ T ) within the mature synthesiser CVC4 and show that CEGIS($$\mathcal {T}$$ T ) improves CVC4’s results.