“A Decision Procedure for String to Code Point Conversion” by Andrew Reynolds, Andres Nötzli, Clark Barrett, and Cesare Tinelli. In Proceedings of the 9^th International Joint Conference on Automated Reasoning (IJCAR '20), (Nicolas Peltier and Viorica Sofronie-Stokkermans, eds.), July 2020, pp. 218-237.
In text encoding standards such as Unicode, text strings are sequences of code points, each of which can be represented as a natural number. We present a decision procedure for a concatenation-free theory of strings that includes length and a conversion function from strings to integer code points. Furthermore, we show how many common string operations, such as conversions between lowercase and uppercase, can be naturally encoded using this conversion function. We describe our implementation of this approach in the SMT solver CVC4, which contains a high-performance string subsolver, and show that the use of a native procedure for code points significantly improves its performance with respect to other state-of-the-art string solvers.
BibTeX entry:
@inproceedings{RNB+20-IJCAR,
author = {Andrew Reynolds and Andres N{\"o}tzli and Clark Barrett and
Cesare Tinelli},
editor = {Nicolas Peltier and Viorica Sofronie-Stokkermans},
title = {A Decision Procedure for String to Code Point Conversion},
booktitle = {Proceedings of the {\it 9^{th}} International Joint
Conference on Automated Reasoning (IJCAR '20)},
series = {Lecture Notes in Computer Science},
volume = {12166},
pages = {218--237},
publisher = {Springer International Publishing},
month = jul,
year = {2020},
isbn = {978-3-030-51074-9},
url = {http://theory.stanford.edu/~barrett/pubs/RNB+20-IJCAR.pdf}
}
(This webpage was created with bibtex2web.)