CVC4SY: Smart and Fast Term Enumeration for Syntax-Guided Synthesis

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.

Abstract

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