Publication Details

Cooking String-Integer Conversions with Noodles

HAVLENA Vojtěch, HOLÍK Lukáš, LENGÁL Ondřej and SÍČ Juraj. Cooking String-Integer Conversions with Noodles. In: Proceedings of SAT'24. Leibniz International Proceedings in Informatics (LIPIcs). Pune: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2024, pp. 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 FIT BUT)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Síč Juraj, Mgr. (DITS FIT BUT)
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, IN
DOI
10.4230/LIPIcs.SAT.2024.14
BibTeX 
@INPROCEEDINGS{FITPUB13240,
   author = "Vojt\v{e}ch Havlena and Luk\'{a}\v{s} Hol\'{i}k and Ond\v{r}ej Leng\'{a}l and Juraj S\'{i}\v{c}",
   title = "Cooking String-Integer Conversions with Noodles",
   pages = "1--19",
   booktitle = "Proceedings of SAT'24",
   series = "Leibniz International Proceedings in Informatics (LIPIcs)",
   journal = "Leibniz International Proceedings in Informatics (LIPIcs)",
   number = 305,
   year = 2024,
   location = "Pune, IN",
   publisher = "Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik",
   ISSN = "1868-8969",
   doi = "10.4230/LIPIcs.SAT.2024.14",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/13240"
}
Back to top