A Decision Procedure for String to Code Point Conversion

Andrew Reynolds; Andres Nötzli; Clark Barrett; Cesare Tinelli

doi:10.1007/978-3-030-51074-9_13

Back

A Decision Procedure for String to Code Point Conversion

Journal article

Open access

Peer reviewed

A Decision Procedure for String to Code Point Conversion

Andrew Reynolds, Andres Nötzli, Clark Barrett and Cesare Tinelli

Automated Reasoning, Vol.12166, pp.218-237

05/30/2020

DOI: 10.1007/978-3-030-51074-9_13

Files and links (1)

url

https://doi.org/10.1007/978-3-030-51074-9_13View

Published (Version of record) Open Access

Abstract

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.

Details

Title: Subtitle: A Decision Procedure for String to Code Point Conversion
Creators: Andrew Reynolds - University of Iowa
Andres Nötzli - Stanford University
Clark Barrett - Stanford University
Cesare Tinelli - University of Iowa
Resource Type: Journal article
Publication Details: Automated Reasoning, Vol.12166, pp.218-237
DOI: 10.1007/978-3-030-51074-9_13
eISBN: 9783030510749; 3030510743
ISSN: 0302-9743
eISSN: 1611-3349
Language: English
Date published: 05/30/2020
Academic Unit: Computer Science
Record Identifier: 9984259438902771

Metrics

70 Record Views

3 Times Cited - Web of Science