Abate Alessandro, Barbosa Haniel, Barrett Clark, David Cristina, Kesseli Pascal, Kroening Daniel, Polgreen Elizabeth, Reynolds Andrew, Tinelli Cesare
University of Oxford, Oxford, UK.
Universidade Federal de Minas Gerais, Belo Horizonte, Minas Gerais Brazil.
J Autom Reason. 2023;67(2):19. doi: 10.1007/s10817-023-09664-4. Epub 2023 May 13.
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.
程序合成是软件的机械化构建。主要困难之一是对非常大的解空间进行有效探索，并且工具通常需要用户提供对搜索空间的句法限制。虽然总体上很有用，但这种句法限制对于生成包含非平凡常量的程序帮助不大，除非用户能够提前提供这些常量。对于最先进的合成器来说，这是一项从根本上就很困难的任务。我们提出了一种用于合成具有非平凡常量的程序的新方法，该方法结合了反例引导的归纳合成器和理论求解器的优势，在不依赖用户指导的情况下更有效地探索解空间。我们将这种方法称为CEGIS( )，其中 是一个一阶理论。我们给出了两个示例，一个基于傅里叶 - 莫兹金（FM）变量消去法，另一个基于一阶可满足性。我们通过为一组复杂的基准自动合成程序来证明CEGIS( )的实用价值。此外，我们展示了一个案例研究，即在成熟的合成器CVC4中集成CEGIS( )，并表明CEGIS( )改进了CVC4的结果。
