语法引导综合中枚举搜索和符号搜索的并行化
Reconciling Enumerative and Symbolic Search in Syntax-Guided Synthesis
摘要：
语法引导的综合旨在找到一个既满足语义规范又满足用户提供的结构假设的程序。对于语法引导的综合，有两种主要的搜索策略：具体搜索，它系统地或随机地枚举所有可能的解决方案，和符号搜索，它与约束求解器交互以解决综合问题。在本文中，我们提出了一个concolic综合框架，结合了最好的两个世界。基于一个决策树表示，我们的框架的工作原理是枚举树的高度从最小的可能的一个到较大的。对于每个固定的高度，框架象征性地通过反例引导的归纳合成方法搜索解决方案。为了补偿concolic合成框架的指数爆破问题，我们确定了两个片段的合成问题，并开发纯粹的象征性和更有效的程序。这两个片段是可判定的，因为这些过程是终止和完成的。我们实现了我们的合成程序，并在一系列基准上与最先进的合成器进行了比较。实验结果表明，我们的算法是有前途的。
英文摘要：
Syntax-guided synthesis aims to find a program satisfying semantic specification as well as user-provided structural hypothesis. For syntax-guided synthesis there are two main search strategies: concrete search, which systematically or stochastically enumerates all possible solutions, and symbolic search, which interacts with a constraint solver to solve the synthesis problem. In this paper, we propose a concolic synthesis framework which combines the best of the two worlds. Based on a decision tree representation, our framework works by enumerating tree heights from the smallest possible one to larger ones. For each fixed height, the framework symbolically searches a solution through the counterexample-guided inductive synthesis approach. To compensate the exponential blow-up problem with the concolic synthesis framework, we identify two fragments of synthesis problems and develop purely symbolic and more efficient procedures. The two fragments are decidable as these procedures are terminating and complete. We implemented our synthesis procedures and compared with state-of-the-art synthesizers on a range of benchmarks. Experiments show that our algorithms are promising.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
