Publication detail

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

CHOCHOLATÝ, D. HAVLENA, V. HOLÍK, L. HRANIČKA, J. LENGÁL, O. SÍČ, J.

Original Title

Type

article in a collection out of WoS and Scopus

Language

English

Original Abstract

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.

Keywords

SMT, string constraints, noodlification, automata, SMT solver

Authors

CHOCHOLATÝ, D.; HAVLENA, V.; HOLÍK, L.; HRANIČKA, J.; LENGÁL, O.; SÍČ, J.

Released

3. 5. 2025

Publisher

Springer Verlag

Location

Hamilton

ISBN

0302-9743

Periodical

Lecture Notes in Computer Science

Number

15697

State

Federal Republic of Germany

Pages from

Pages to

Pages count

BibTex

@inproceedings{BUT194210,
  author="David {Chocholatý} and Vojtěch {Havlena} and Lukáš {Holík} and Jan {Hranička} and Ondřej {Lengál} and Juraj {Síč}",
  title="Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation",
  booktitle="Proceedings of TACAS'25",
  year="2025",
  journal="Lecture Notes in Computer Science",
  number="15697",
  pages="23--44",
  publisher="Springer Verlag",
  address="Hamilton",
  doi="10.1007/978-3-031-90653-4\{_}2",
  issn="0302-9743"
}