SyGuS Techniques in the Core of an SMT Solver
Andrew Reynolds (1), Cesare Tinelli (2) ((1) University of Iowa, (2), University of Iowa)
TL;DR
This paper reviews recent methods for integrating syntax-guided synthesis (SyGuS) algorithms into SMT solvers, categorizing conjectures and techniques for different classes to enhance solver capabilities.
Contribution
It introduces a structured overview of SyGuS techniques within SMT solvers, defining classes of conjectures and tailored methods for each, advancing the understanding of synthesis integration.
Findings
Categorization of synthesis conjectures
Techniques tailored to each conjecture class
Enhanced SMT solver capabilities
Abstract
We give an overview of recent techniques for implementing syntax-guided synthesis (SyGuS) algorithms in the core of Satisfiability Modulo Theories (SMT) solvers. We define several classes of synthesis conjectures and corresponding techniques that can be used when dealing with each class of conjecture.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.