Preprint
On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4
ArXiv.org
02/16/2015
DOI: 10.48550/arxiv.1502.04464
Abstract
We introduce the first program synthesis engine implemented inside an SMT
solver. We present an approach that extracts solution functions from
unsatisfiability proofs of the negated form of synthesis conjectures. We also
discuss novel counterexample-guided techniques for quantifier instantiation
that we use to make finding such proofs practically feasible. A particularly
important class of specifications are single-invocation properties, for which
we present a dedicated algorithm. To support syntax restrictions on generated
solutions, our approach can transform a solution found without restrictions
into the desired syntactic form. As an alternative, we show how to use
evaluation function axioms to embed syntactic restrictions into constraints
over algebraic datatypes, and then use an algebraic datatype decision procedure
to drive synthesis. Our experimental evaluation on syntax-guided synthesis
benchmarks shows that our implementation in the CVC4 SMT solver is competitive
with state-of-the-art tools for synthesis.
Details
- Title: Subtitle
- On Counterexample Guided Quantifier Instantiation for Synthesis in CVC4
- Creators
- Andrew Reynolds - École Polytechnique Fédérale de LausanneMorgan DetersViktor KuncakCesare TinelliClark Barrett
- Resource Type
- Preprint
- Publication Details
- ArXiv.org
- DOI
- 10.48550/arxiv.1502.04464
- ISSN
- 2331-8422
- Language
- English
- Date posted
- 02/16/2015
- Academic Unit
- Computer Science
- Record Identifier
- 9984410842302771
Metrics
3 Record Views