Preprint
CVC4SY for SyGuS-COMP 2019
ArXiv.org
07/23/2019
DOI: 10.48550/arxiv.1907.10175
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.
Details
- Title: Subtitle
- CVC4SY for SyGuS-COMP 2019
- Creators
- Andrew ReynoldsHaniel BarbosaAndres NötzliClark BarrettCesare Tinelli
- Resource Type
- Preprint
- Publication Details
- ArXiv.org
- DOI
- 10.48550/arxiv.1907.10175
- ISSN
- 2331-8422
- Language
- English
- Date posted
- 07/23/2019
- Academic Unit
- Computer Science
- Record Identifier
- 9984411071602771
Metrics
1 Record Views