Detail publikačního výsledku

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

Anglický název

Cooking String-Integer Conversions with Noodles

Druh

Stať ve sborníku mimo WoS a Scopus

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.

Anglický 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

Klíčová slova v angličtině

string solving, string conversions, SMT solving

Autoři

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

Rok RIV

2025

Vydáno

21.08.2024

Nakladatel

Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik

Místo

Pune

Kniha

Proceedings of SAT'24

Edice

Leibniz International Proceedings in Informatics (LIPIcs)

ISSN

1868-8969

Periodikum

Leibniz International Proceedings in Informatics

Číslo

305

Stát

Spolková republika Německo

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",
  number="305",
  pages="1--19",
  publisher="Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik",
  address="Pune",
  doi="10.4230/LIPIcs.SAT.2024.14"
}