CVC4中反例引导的量词实例化综合
On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4
摘要：
我们介绍的第一个程序合成引擎内实现的SMT求解器。我们提出了一种方法，提取解决方案的功能，从不可满足性证明的否定形式的合成图。我们还讨论了新的反例引导的量词实例化技术，我们使用找到这样的证明实际上是可行的。一类特别重要的规范是单调用属性，我们提出了一个专用的算法。为了支持生成的解决方案的语法限制，我们的方法可以转换到所需的语法形式的解决方案，没有限制。作为一种替代方案，我们展示了如何使用评价函数公理嵌入到代数数据集的约束语法限制，然后使用代数数据类型的决策过程来驱动合成。我们的实验评估的语法指导的合成基准表明，我们的实现在CVC 4 SMT求解器是有竞争力的国家的最先进的合成工具。
英文摘要：
We introduce the first program synthesis engine implemented inside an SMT solver. We present an approach that extracts solution functions from unsatisfiability proofs of the negated form of synthesis conjectures. We also discuss novel counterexample-guided techniques for quantifier instantiation that we use to make finding such proofs practically feasible. A particularly important class of specifications are single-invocation properties, for which we present a dedicated algorithm. To support syntax restrictions on generated solutions, our approach can transform a solution found without restrictions into the desired syntactic form. As an alternative, we show how to use evaluation function axioms to embed syntactic restrictions into constraints over algebraic datatypes, and then use an algebraic datatype decision procedure to drive synthesis. Our experimental evaluation on syntax-guided synthesis benchmarks shows that our implementation in the CVC4 SMT solver is competitive with state-of-the-art tools for synthesis.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
