“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.)