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

Abstract

We present cvc 4 sy , 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 cvc 4 and a heuristic to choose between them leads to significant improvements over state-of-the-art SyGuS solvers.