Book chapter
Syntax-Guided Rewrite Rule Enumeration for SMT Solvers
Theory and Applications of Satisfiability Testing – SAT 2019, pp.279-297
Lecture Notes in Computer Science, Springer International Publishing
06/29/2019
DOI: 10.1007/978-3-030-24258-9_20
Abstract
The performance of modern Satisfiability Modulo Theories (SMT) solvers relies crucially on efficient decision procedures as well as static simplification techniques, which include large sets of rewrite rules. Manually discovering and implementing rewrite rules is challenging. In this work, we propose a framework that uses enumerative syntax-guided synthesis (SyGuS) to propose rewrite rules that are not implemented in a given SMT solver. We implement this framework in cvc4, a state-of-the-art SMT and SyGuS solver, and evaluate several use cases. We show that some SMT solvers miss rewriting opportunities, or worse, have bugs in their rewriters. We also show that a variation of our approach can be used to test the correctness of a rewriter. Finally, we show that rewrites discovered with this technique lead to significant improvements in cvc4 on both SMT and SyGuS problems over bit-vectors and strings.
Details
- Title: Subtitle
- Syntax-Guided Rewrite Rule Enumeration for SMT Solvers
- Creators
- Andres Nötzli - Stanford UniversityAndrew Reynolds - University of IowaHaniel Barbosa - University of IowaAina Niemetz - Stanford UniversityMathias Preiner - Stanford UniversityClark Barrett - Stanford UniversityCesare Tinelli - University of Iowa
- Resource Type
- Book chapter
- Publication Details
- Theory and Applications of Satisfiability Testing – SAT 2019, pp.279-297
- Publisher
- Springer International Publishing; Cham
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-030-24258-9_20
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 06/29/2019
- Academic Unit
- Computer Science
- Record Identifier
- 9984259431402771
Metrics
21 Record Views