Refutation-based synthesis in SMT

by Andrew Reynolds, Viktor Kuncak, Cesare Tinelli, Clark Barrett, Morgan Deters
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.
Reference:
Refutation-based synthesis in SMT (Andrew Reynolds, Viktor Kuncak, Cesare Tinelli, Clark Barrett, Morgan Deters), In Formal Methods in System Design, Springer US, 2017.
Bibtex Entry:
@article{reynolds2017refutation,
  title={Refutation-based synthesis in SMT},
  author={Reynolds, Andrew and Kuncak, Viktor and Tinelli, Cesare and Barrett, Clark and Deters, Morgan},
  journal={Formal Methods in System Design},
  pages={1--30},
  year={2017},
  publisher={Springer US},
  url="http://homepage.divms.uiowa.edu/~ajreynol/fmsd17.pdf",
  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."
}

Fork me on GitHub