diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-07 10:22:27 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-05-07 10:22:27 -0500 |
commit | db43ae511c2103f1e9718a8954e26cf7866d14a8 (patch) | |
tree | 3d0654dd38d404bbe31c2bd543a003b351d37336 /src/util/regexp.h | |
parent | 884ad1a946ad6a04664ef97121ce1cebb5513d40 (diff) |
Add support for str.code (#1821)
Diffstat (limited to 'src/util/regexp.h')
-rw-r--r-- | src/util/regexp.h | 48 |
1 files changed, 35 insertions, 13 deletions
diff --git a/src/util/regexp.h b/src/util/regexp.h index 42d232259..c8b491475 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -28,21 +28,43 @@ namespace CVC4 { +/** The CVC4 string class + * + * This data structure is the domain of values for the string type. It can also + * be used as a generic utility for representing strings. + */ class CVC4_PUBLIC String { public: - static unsigned convertCharToUnsignedInt(unsigned char c) { - unsigned i = c; - i = i + 191; - return (i >= 256 ? i - 256 : i); - } - static unsigned char convertUnsignedIntToChar(unsigned i) { - unsigned ii = i + 65; - return (unsigned char)(ii >= 256 ? ii - 256 : ii); - } - static bool isPrintable(unsigned i) { - unsigned char c = convertUnsignedIntToChar(i); - return (c >= ' ' && c <= '~'); // isprint( (int)c ); - } + /** + * The start ASCII code. In our string representation below, we represent + * characters using a vector d_vec of unsigned integers. We refer to this as + * the "internal representation" for the string. + * + * We make unsigned integer 0 correspond to the 65th character ("A") in the + * ASCII alphabet to make models intuitive. In particular, say if we have + * a set of string variables that are distinct but otherwise unconstrained, + * then the model may assign them "A", "B", "C", ... + */ + static inline unsigned start_code() { return 65; } + /** + * This is the cardinality of the alphabet that is representable by this + * class. Notice that this must be greater than or equal to the cardinality + * of the alphabet that the string theory reasons about. + */ + static inline unsigned num_codes() { return 256; } + /** + * Convert unsigned char to the unsigned used in the internal representation + * in d_vec below. + */ + static unsigned convertCharToUnsignedInt(unsigned char c); + /** Convert the internal unsigned to a unsigned char. */ + static unsigned char convertUnsignedIntToChar(unsigned i); + /** Does the internal unsigned correspond to a printable character? */ + static bool isPrintable(unsigned i); + /** get the internal unsigned for ASCII code c. */ + static unsigned convertCodeToUnsignedInt(unsigned c); + /** get the ASCII code number that internal unsigned i corresponds to. */ + static unsigned convertUnsignedIntToCode(unsigned i); /** constructors for String * |