Result Details

Cooking String-Integer Conversions with Noodles

HAVLENA, V.; HOLÍK, L.; LENGÁL, O.; SÍČ, J. Cooking String-Integer Conversions with Noodles. Proceedings of SAT'24. Leibniz International Proceedings in Informatics, LIPIcs. Leibniz International Proceedings in Informatics (LIPIcs). Pune: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2024. no. 305, p. 1-19. ISSN: 1868-8969.
Type
conference paper
Language
English
Authors
Havlena Vojtěch, Ing., Ph.D., DITS (FIT)
Holík Lukáš, doc. Mgr., Ph.D., DITS (FIT)
Lengál Ondřej, doc. Ing., Ph.D., DITS (FIT)
Síč Juraj, Mgr., DITS (FIT)
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

Published
2024
Pages
1–19
Journal
Leibniz International Proceedings in Informatics, LIPIcs, no. 305, ISSN 1868-8969
Proceedings
Proceedings of SAT'24
Series
Leibniz International Proceedings in Informatics (LIPIcs)
Conference
The 27th International Conference on Theory and Applications of Satisfiability Testing
Publisher
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Place
Pune
DOI
10.4230/LIPIcs.SAT.2024.14
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"
}
Projects
Efficient Finite Automata for Automated Reasoning, MŠMT, ERC CZ, LL1908, start: 2020-01-01, end: 2024-12-31, completed
Reliable, Secure, and Intelligent Computer Systems, BUT, Vnitřní projekty VUT, FIT-S-23-8151, start: 2023-03-01, end: 2026-02-28, running
Representing Boolean Functions by a Self-Adaptable Data Structure, GACR, Standardní projekty, GA23-07565S, start: 2023-01-01, end: 2025-12-31, running
Research groups
Automata@FIT (RG Automata@FIT)
Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)
Departments
Department of Intelligent Systems (DITS)
Back to top