Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866918126218641408 |
|---|---|
| author | Hozzová, Petra Bjørner, Nikolaj |
| author_facet | Hozzová, Petra Bjørner, Nikolaj |
| contents | Program synthesis is the task of automatically constructing a program conforming to a given specification. In this paper we focus on synthesis of single-invocation recursion-free functions conforming to a specification given as a logical formula in the presence of uncomputable symbols (i.e., symbols used in the specification but not allowed in the resulting function). We approach the problem via SMT-solving methods: we present a quantifier elimination algorithm using model-based projections for both total and partial function synthesis, working with theories of uninterpreted functions and linear arithmetic and their combination. For this purpose we also extend model-based projection to produce witnesses for these theories. Further, we present procedures tailored for the case of uniquely determined solutions. We implemented a prototype of the algorithms using the SMT-solver Z3, demonstrating their practical efficiency compared to the state of the art. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_16536 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols Hozzová, Petra Bjørner, Nikolaj Logic in Computer Science Program synthesis is the task of automatically constructing a program conforming to a given specification. In this paper we focus on synthesis of single-invocation recursion-free functions conforming to a specification given as a logical formula in the presence of uncomputable symbols (i.e., symbols used in the specification but not allowed in the resulting function). We approach the problem via SMT-solving methods: we present a quantifier elimination algorithm using model-based projections for both total and partial function synthesis, working with theories of uninterpreted functions and linear arithmetic and their combination. For this purpose we also extend model-based projection to produce witnesses for these theories. Further, we present procedures tailored for the case of uniquely determined solutions. We implemented a prototype of the algorithms using the SMT-solver Z3, demonstrating their practical efficiency compared to the state of the art. |
| title | Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2504.16536 |