Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail publikace
HAVLENA, V. HOLÍK, L. LENGÁL, O. SÍČ, J.
Originální název
Cooking String-Integer Conversions with Noodles
Typ
článek ve sborníku mimo WoS a Scopus
Jazyk
angličtina
Originální abstrakt
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.
Klíčová slova
string solving, string conversions, SMT solving
Autoři
HAVLENA, V.; HOLÍK, L.; LENGÁL, O.; SÍČ, J.
Vydáno
21. 8. 2024
Nakladatel
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Místo
Pune
ISSN
1868-8969
Periodikum
Leibniz International Proceedings in Informatics, LIPIcs
Stát
neuvedeno
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", publisher="Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik", address="Pune", issn="1868-8969" }