Detail publikace

Cooking String-Integer Conversions with Noodles

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

Číslo

305

Stát

neuvedeno

Strany od

1

Strany do

19

Strany počet

19

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