Publication Details
Solving Not-Substring Constraint with Flat Abstraction
Atig Mohamed F. (Uppsala)
Bui Phi Diep (Uppsala)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Chen Yu-Fang (ASIN)
Wu Zhilin (Chinese Academy of Sciences)
CEGAR, string constraints, strings
Not-substring is currently among the least supported types of string constraints, and existing solvers use only relatively crude heuristics. Yet, not-substring occurs relatively often in practical examples and is useful in encoding other types of constraints. In this paper, we propose a systematic way to solve not-substring using the Counter-Example Guided Abstraction Refinement (CEGAR) framework based on flat abstraction. In such a framework, the domain of string variables is restricted to flat languages and subsequently, the whole constraints can be expressed as linear arithmetic formulae. We show that non-substring constraints can be flattened efficiently, and provide experimental evidence that the proposed solution for not-substring is competitive with the state-of-the-art string solvers.
@INPROCEEDINGS{FITPUB12676, author = "A. Parosh Abdulla and F. Mohamed Atig and Diep Phi Bui and Luk\'{a}\v{s} Hol\'{i}k and Yu-Fang Chen and Zhilin Wu", title = "Solving Not-Substring Constraint with Flat Abstraction", pages = "305--320", booktitle = "Programming Languages and Systems - 19th Asian Symposium, APLAS 2021, Chicago, IL, USA, October 17-18, 2021, Proceedings", series = "13008", year = 2021, location = "Berl\'{i}n, DE", publisher = "Springer International Publishing", ISBN = "978-3-030-89051-3", doi = "10.1007/978-3-030-89051-3\_17", language = "english", url = "https://www.fit.vut.cz/research/publication/12676" }