“Syntax-Guided Rewrite Rule Enumeration for SMT Solvers” by Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark Barrett, and Cesare Tinelli. In Proceedings of the 22^nd International Conference on Theory and Applications of Satisfiability Testing (SAT '19), (Mikolá\u{s} Janota and Inês Lynce, eds.), July 2019, pp. 279-297. Lisbon, Portugal.
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.
BibTeX entry:
@inproceedings{NRB+19,
author = {Andres N{\"o}tzli and Andrew Reynolds and Haniel Barbosa and
Aina Niemetz and Mathias Preiner and Clark Barrett and Cesare
Tinelli},
editor = {Mikol{\'a}\u{s} Janota and In{\^e}s Lynce},
title = {Syntax-Guided Rewrite Rule Enumeration for SMT Solvers},
booktitle = {Proceedings of the {\it 22^{nd}} International Conference
on Theory and Applications of Satisfiability Testing (SAT '19)},
series = {Lecture Notes in Computer Science},
volume = {11628},
pages = {279--297},
publisher = {Springer},
month = jul,
year = {2019},
isbn = {978-3-030-24257-2},
doi = {10.1007/978-3-030-24258-9_20},
note = {Lisbon, Portugal},
url = {http://theory.stanford.edu/~barrett/pubs/NRB+19.pdf}
}
(This webpage was created with bibtex2web.)