Portal de Periódicos da CAPES

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

2019; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-030-25543-5_5

1611-3349

Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark Barrett, Cesare Tinelli,

Model-Driven Software Engineering Techniques

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.