2026-08-19T20:45:49Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20536 2024-08-19T06:03:42Z ddc:004 open_access

Cooking String-Integer Conversions with Noodles Havlena, Vojtěch Holík, Lukáš Lengál, Ondřej Síč, Juraj string solving string conversions SMT solving 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Vojtěch Havlena and Lukáš Holík and Ondřej Lengál and Juraj Síč 2024 Is Part Of LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2024.14 urn:nbn:de:0030-drops-205365 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.14 eng https://creativecommons.org/licenses/by/4.0/legalcode