ICSE 2020 (series) / FormaliSE 2020 (series) / FormaliSE 2020 /
Rule-based Word Equation Solving
We present a transformation-system-based technique in the framework of string solving, by reformulating a classical combinatorics on words result, the Lemma of Levi. We further enrich the induced rules by simplification steps based on results from the combinatorial theory of word equations, as well as by the addition of linear length constraints. This transformation-system approach cannot solve all equations efficiently by itself, so our final approach integrates existing string solvers, which are called based on heuristics. Experimental evaluation shows that this technique is useful as an inprocessing method for existing solvers.