CVC4 中用于综合的反例引导量词实例化
计算机科学中的逻辑
2015-06-24 v3
摘要
我们介绍了首个在 SMT 求解器内实现的程序综合引擎。我们提出了一种从综合猜想否定形式的不满足性证明中提取解函数的方法。我们还讨论了用于量词实例化的新型反例引导技术，利用这些技术使寻找此类证明在实际中可行。一类尤其重要的规约是单调用属性，我们为其提出了专用算法。为了支持对生成解的语法限制，我们的方法可将无限制下找到的解转换为所需的语法形式。作为替代，我们展示了如何使用求值函数公理将语法限制嵌入到关于代数数据类型的约束中，然后利用代数数据类型判定过程驱动综合。我们在语法引导综合基准上的实验评估表明，我们在 CVC4 SMT 求解器中的实现与最先进的综合工具具有竞争力。
引用
@article{arxiv.1502.04464,
title = {On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4},
author = {Andrew Reynolds and Morgan Deters and Viktor Kuncak and Cesare Tinelli and Clark Barrett},
journal= {arXiv preprint arXiv:1502.04464},
year = {2015}
}