Conference proceeding
A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery
2023 Formal Methods in Computer-Aided Design (FMCAD), pp.189-198
10/24/2023
DOI: 10.34727/2023/isbn.978-3-85448-060-0_27
Abstract
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
Details
- Title: Subtitle
- A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery
- Creators
- Abdalrhman Mohamed - Stanford UniversityAndrew Reynolds - University of IowaClark Barrett - Stanford UniversityCesare Tinelli - University of Iowa
- Resource Type
- Conference proceeding
- Publication Details
- 2023 Formal Methods in Computer-Aided Design (FMCAD), pp.189-198
- DOI
- 10.34727/2023/isbn.978-3-85448-060-0_27
- eISSN
- 2708-7824
- Publisher
- FMCAD Association and individual authors
- Language
- English
- Date published
- 10/24/2023
- Academic Unit
- Computer Science
- Record Identifier
- 9984528129302771
Metrics
146 Record Views