Publication detail

Cooking String-Integer Conversions with Noodles

HAVLENA, V. HOLÍK, L. LENGÁL, O. SÍČ, J.

Original Title

Cooking String-Integer Conversions with Noodles

Type

article in a collection out of WoS and Scopus

Language

English

Original 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.

Keywords

string solving, string conversions, SMT solving

Authors

HAVLENA, V.; HOLÍK, L.; LENGÁL, O.; SÍČ, J.

Released

21. 8. 2024

Publisher

Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik

Location

Pune

ISBN

1868-8969

Periodical

Leibniz International Proceedings in Informatics, LIPIcs

Number

305

State

unknown

Pages from

1

Pages to

19

Pages count

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