Publication result 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

English Title

Cooking String-Integer Conversions with Noodles

Type

Paper in proceedings outside WoS and Scopus

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.

English 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

Key words in English

string solving, string conversions, SMT solving

Authors

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

RIV year

2025

Released

21.08.2024

Publisher

Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik

Location

Pune

Book

Proceedings of SAT'24

Edition

Leibniz International Proceedings in Informatics (LIPIcs)

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