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.
Cite
CITATION STYLE
Reynolds, A., Barbosa, H., Nötzli, A., Barrett, C., & Tinelli, C. (2019). CVC4SY: Smart and fast term enumeration for syntax-guided synthesis. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11562 LNCS, pp. 74–83). Springer Verlag. https://doi.org/10.1007/978-3-030-25543-5_5
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
