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

PDF

Related Concepts

Enumeration Computer science Solver Satisfiability modulo theories Modulo Term (time) Syntax Heuristic Extension (predicate logic) Satisfiability Programming language Theoretical computer science Algebraic number Boolean satisfiability problem State (computer science) Bounded function Algorithm Discrete mathematics Mathematics Artificial intelligence Quantum mechanics Mathematical analysis Physics

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

YOU? · · 2019 · Open Access · · DOI: https://doi.org/10.1007/978-3-030-25543-5_5 · OA: W2956992268

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.