CVC4SY for SyGuS-COMP 2019

TL;DR

CVC4Sy is a syntax-guided synthesis solver that combines enumerative techniques and quantifier elimination, leveraging SMT solving and heuristics to efficiently solve synthesis problems, demonstrated in the SyGuS-Comp 2019 competition.

Contribution

This paper introduces CVC4Sy, a novel SyGuS solver integrating enumerative and quantifier elimination strategies within an SMT framework, optimized for competitive performance.

Findings

Effective enumeration via algebraic datatypes encoding

Quantifier elimination from unsatisfiability proofs

Heuristic problem classification for strategy selection

Abstract

CVC4Sy is a syntax-guided synthesis (SyGuS) solver based on bounded term enumeration and, for restricted fragments, quantifier elimination. The enumerative strategies are based on encoding term enumeration as an extension of the quantifier-free theory of algebraic datatypes and on a highly optimized brute-force algorithm. The quantifier elimination strategy extracts solutions from unsatisfiability proofs of the negated form of synthesis conjectures. It uses recent counterexample-guided techniques for quantifier instantiation that make finding such proofs practically feasible. CVC4Sy implements these strategies by extending the satisfiability modulo theories (SMT) solver CVC4. The strategy to be applied on a given problem is chosen heuristically based on the problem's structure. This document gives an overview of these techniques and their implementation in the SyGuS Solver CVC4Sy, an entry for SyGuS-Comp 2019.