Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F26%3A0194210" target="_blank" >RIV/00216305:26230/26:0194210 - isvavai.cz</a>
Výsledek na webu
<a href="https://link.springer.com/chapter/10.1007/978-3-031-90653-4_2" target="_blank" >https://link.springer.com/chapter/10.1007/978-3-031-90653-4_2</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-031-90653-4_2" target="_blank" >10.1007/978-3-031-90653-4_2</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation
Popis výsledku v původním jazyce
Z3-Noodler is a fork of the Z3 SMT solver replacing its string theory implementation with a portfolio of decision procedures and a selection mechanism for choosing among them based on the features of the input formula. In this paper, we give an overview of the used decision procedures, including a novel length-based procedure, and their integration into a robust solver with a good overall performance, as witnessed by Z3-Noodler winning the string division of SMT-COMP'24 by a large margin. We also extended the solver with a support for model generation, which is essential for the use of the solver in practice.
Název v anglickém jazyce
Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation
Popis výsledku anglicky
Z3-Noodler is a fork of the Z3 SMT solver replacing its string theory implementation with a portfolio of decision procedures and a selection mechanism for choosing among them based on the features of the input formula. In this paper, we give an overview of the used decision procedures, including a novel length-based procedure, and their integration into a robust solver with a good overall performance, as witnessed by Z3-Noodler winning the string division of SMT-COMP'24 by a large margin. We also extended the solver with a support for model generation, which is essential for the use of the solver in practice.
Klasifikace
Druh
O - Ostatní výsledky
CEP obor
—
OECD FORD obor
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Návaznosti výsledku
Projekt
<a href="/cs/project/GA23-07565S" target="_blank" >GA23-07565S: Reprezentace Booleovských funkcí pomocí adaptabilní datové struktury</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach
Ostatní
Rok uplatnění
2025
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů