Counterexample Guided Quantifier Instantiation for Synthesis in SMT

by Andrew Reynolds, Morgan Deters, Viktor Kuncak, Clark Barrett, Cesare Tinelli
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:
Counterexample Guided Quantifier Instantiation for Synthesis in SMT (Andrew Reynolds, Morgan Deters, Viktor Kuncak, Clark Barrett, Cesare Tinelli), In Proceedings of the 27th International Conference on Computer Aided Verification (CAV ’15) (Daniel Kroening, Corina S. Puasuareanu, eds.), Springer, volume 9206, 2015. (San Francisco, CA)
Bibtex Entry:
@inproceedings{RDK+15,
  url       = "http://www.cs.stanford.edu/~barrett/pubs/RDK+15.pdf",
  author    = "Andrew Reynolds and Morgan Deters and Viktor Kuncak and Clark Barrett and Cesare Tinelli",
  title     = "Counterexample Guided Quantifier Instantiation for Synthesis in {SMT}",
  booktitle = "Proceedings of the 27th International Conference on Computer Aided Verification (CAV '15)",
  volume    = 9206,
  number    = 2,
  editor    = "Daniel Kroening and Corina S. Pu{a}su{a}reanu",
  pages     = "198--216",
  series    = "Lecture Notes in Computer Science",
  publisher = "Springer",
  month     = jul,
  year      = 2015,
  note      = "San Francisco, CA",
  category  = "Conference Publications",
  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