Publication Details

Cooking String-Integer Conversions with Noodles

HAVLENA, V.; HOLÍK, L.; LENGÁL, O.; SÍČ, J. Cooking String-Integer Conversions with Noodles. Proceedings of SAT'24. Leibniz International Proceedings in Informatics, LIPIcs. Leibniz International Proceedings in Informatics (LIPIcs). Pune: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2024. p. 1-19. ISSN: 1868-8969.
Czech title
Vaření převodů řetězců s nudlemi
Type
conference paper
Language
English
Authors
Havlena Vojtěch, Ing., Ph.D. (DITS)
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Lengál Ondřej, Ing., Ph.D. (DITS)
Síč Juraj, Mgr. (DITS)
Keywords

string solving, string conversions, SMT solving

Abstract

We propose a method for efficient handling string constraints with string-integer
conversions. It extends the recently introduced stabilization-based procedure for
solving string (dis)equations with regular and length constraints. Our approach
is to translate the conversions into a linear integer arithmetic formula,
together with regular constraints and word equations. We have integrated it into
the string solver Z3-Noodler, and our experiments show that it is competitive and
on some established benchmarks even several orders of magnitude faster than the
state of the art.

Published
2024
Pages
1–19
Journal
Leibniz International Proceedings in Informatics, LIPIcs, no. 305, ISSN 1868-8969
Proceedings
Proceedings of SAT'24
Series
Leibniz International Proceedings in Informatics (LIPIcs)
Conference
The 27th International Conference on Theory and Applications of Satisfiability Testing, Pune, IN
Publisher
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Place
Pune
DOI
10.4230/LIPIcs.SAT.2024.14
BibTeX 
@inproceedings{BUT189244,
  author="Vojtěch {Havlena} and Lukáš {Holík} and Ondřej {Lengál} and Juraj {Síč}",
  title="Cooking String-Integer Conversions with Noodles",
  booktitle="Proceedings of SAT'24",
  year="2024",
  series="Leibniz International Proceedings in Informatics (LIPIcs)",
  journal="Leibniz International Proceedings in Informatics, LIPIcs",
  number="305",
  pages="1--19",
  publisher="Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik",
  address="Pune",
  doi="10.4230/LIPIcs.SAT.2024.14",
  issn="1868-8969"
}
Back to top