“CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis” by Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Cesare Tinelli, and Clark Barrett. In Proceedings of the 31^st International Conference on Computer Aided Verification (CAV '19), (Isil Dillig and Serdar Tasiran, eds.), July 2019, pp. 74-83. New York, New York.
We present CVC4SY, a syntax-guided synthesis (SyGuS) solver based on three bounded term enumeration strategies. The first encodes term enumeration as an extension of the quantifier-free theory of algebraic datatypes. The second is based on a highly optimized brute-force algorithm. The third combines elements of the others. Our implementation of the strategies within the satisfiability modulo theories (SMT) solver CVC4 and a heuristic to choose between them leads to significant improvements over state-of-the-art SyGuS solvers.
BibTeX entry:
@inproceedings{RBN+19,
author = {Andrew Reynolds and Haniel Barbosa and Andres N{\"o}tzli and
Cesare Tinelli and Clark Barrett},
editor = {Isil Dillig and Serdar Tasiran},
title = {{CVC4SY}: Smart and Fast Term Enumeration for Syntax-Guided
Synthesis},
booktitle = {Proceedings of the {\it 31^{st}} International Conference
on Computer Aided Verification (CAV '19)},
series = {Lecture Notes in Computer Science},
volume = {11561},
pages = {74--83},
publisher = {Springer International Publishing},
month = jul,
year = {2019},
isbn = {978-3-030-25542-8},
doi = {10.1007/978-3-030-25543-5_5},
note = {New York, New York},
url = {http://theory.stanford.edu/~barrett/pubs/RBN+19.pdf}
}
(This webpage was created with bibtex2web.)