Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation

Result code in 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>

Result on the web

<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>

Result language

angličtina

Original language name

Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation

Original language description

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.

Czech name

—

Czech description

—

Type

O - Miscellaneous

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

<a href="/en/project/GA23-07565S" target="_blank" >GA23-07565S: Representing Boolean Functions by a Self-Adaptable Data Structure</a><br>

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Publication year

2025

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů