TY - GEN
T1 - Counterexample-guided quantifier instantiation for synthesis in SMT
AU - Reynolds, Andrew
AU - Deters, Morgan
AU - Kuncak, Viktor
AU - Tinelli, Cesare
AU - Barrett, Clark
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2015.
PY - 2015
Y1 - 2015
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84951154325&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84951154325&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-21668-3_12
DO - 10.1007/978-3-319-21668-3_12
M3 - Conference contribution
AN - SCOPUS:84951154325
SN - 9783319216676
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 198
EP - 216
BT - Computer Aided Verification - 27th International Conference, CAV 2015, Proceedings
A2 - Păsăreanu, Corina S.
A2 - Kroening, Daniel
PB - Springer Verlag
T2 - 27th International Conference on Computer Aided Verification, CAV 2015
Y2 - 18 July 2015 through 24 July 2015
ER -