Cooking String-Integer Conversions with Noodles
Havlena, Vojtěch, Holík, Lukáš, Lengál, Ondřej, Síč, Juraj · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2024
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.