面向 SyGuS-COMP 2019 的 CVC4SY
计算机科学中的逻辑
2019-07-25 v1
摘要
CVC4Sy 是一个基于有界项枚举以及针对受限片段的量词消去的语法引导综合（SyGuS）求解器。枚举策略基于将项枚举编码为代数数据类型无量词理论的扩展，以及一种高度优化的暴力算法。量词消去策略从综合猜想否定形式的不满足性证明中提取解。它使用近期针对量词实例化的反例引导技术，使寻找此类证明在实践中可行。CVC4Sy 通过扩展可满足性模理论（SMT）求解器 CVC4 来实现这些策略。对给定问题所应用的策略根据其结构启发式地选择。本文档概述了这些技术及其在 SyGuS 求解器 CVC4Sy（SyGuS-Comp 2019 的参赛作品）中的实现。
引用
@article{arxiv.1907.10175,
title = {CVC4SY for SyGuS-COMP 2019},
author = {Andrew Reynolds and Haniel Barbosa and Andres Nötzli and Clark Barrett and Cesare Tinelli},
journal= {arXiv preprint arXiv:1907.10175},
year = {2019}
}