“A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery” by Abdalrhman Mohamed, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. In Proceedings of the 23^rd International Conference on Formal Methods In Computer-Aided Design (FMCAD '23), (Alexander Nadel and Kristin Yvonne Rozier, eds.), Oct. 2023, pp. 189-198. Ames, IA.
Syntax-guided synthesis (SyGuS) is a recent software synthesis paradigm in which an automated synthesis tool is asked to synthesize a term that satisfies both a semantic and a syntactic specification. We consider a special case of the SyGuS problem, where a term is already known to satisfy the semantic specification but may not satisfy the syntactic one. The goal is then to find an equivalent term that additionally satisfies the syntactic specification, provided by a context-free grammar. We introduce a novel procedure for solving this problem which leverages pattern matching and automated discovery of rewrite rules. We also provide an implementation of the procedure by modifying the SyGuS solver embedded in the cvc5 SMT solver. Our evaluation shows that our new procedure significantly outperforms the state of the art on a large set of SyGuS problems for standard SMT-LIB theories such as bit-vectors, arithmetic, and strings.
BibTeX entry:
@inproceedings{MRB+23,
author = {Abdalrhman Mohamed and Andrew Reynolds and Clark Barrett and
Cesare Tinelli},
editor = {Alexander Nadel and Kristin Yvonne Rozier},
title = {A Procedure for SyGuS Solution Fitting via Matching and
Rewrite Rule Discovery},
booktitle = {Proceedings of the {\it 23^{rd}} International Conference
on Formal Methods In Computer-Aided Design (FMCAD '23)},
pages = {189--198},
publisher = {TU Wien Academic Press},
month = oct,
year = {2023},
doi = {10.34727/2023/isbn.978-3-85448-060-0_27},
note = {Ames, IA},
url = {https://repositum.tuwien.at/handle/20.500.12708/188730}
}
(This webpage was created with bibtex2web.)