Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Tim King, Mathias Preiner
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * The string data type.
14 : : */
15 : :
16 : : #include "cvc5_public.h"
17 : :
18 : : #ifndef CVC5__UTIL__STRING_H
19 : : #define CVC5__UTIL__STRING_H
20 : :
21 : : #include <iosfwd>
22 : : #include <string>
23 : : #include <vector>
24 : :
25 : : #include "util/rational.h"
26 : :
27 : : namespace cvc5::internal {
28 : :
29 : : namespace strings {
30 : : struct StringHashFunction;
31 : : }
32 : :
33 : : /** The cvc5 string class
34 : : *
35 : : * This data structure is the domain of values for the string type. It can also
36 : : * be used as a generic utility for representing strings.
37 : : */
38 : : class String
39 : : {
40 : : friend strings::StringHashFunction;
41 : :
42 : : public:
43 : : /**
44 : : * This is the cardinality of the alphabet that is representable by this
45 : : * class. Notice that this must be greater than or equal to the cardinality
46 : : * of the alphabet that the string theory reasons about.
47 : : *
48 : : * This must be strictly less than std::numeric_limits<unsigned>::max().
49 : : *
50 : : * As per the SMT-LIB standard for strings, we support the first 3 planes of
51 : : * Unicode characters, where 196608 = 3*16^4.
52 : : */
53 : 2224925 : static inline unsigned num_codes() { return 196608; }
54 : : /** constructors for String
55 : : *
56 : : * Internally, a cvc5::internal::String is represented by a vector of unsigned
57 : : * integers (d_str) representing the code points of the characters.
58 : : *
59 : : * To build a string from a C++ string, we may process escape sequences
60 : : * according to the SMT-LIB standard. In particular, if useEscSequences is
61 : : * true, we convert unicode escape sequences:
62 : : * \u d_3 d_2 d_1 d_0
63 : : * \u{d_0}
64 : : * \u{d_1 d_0}
65 : : * \u{d_2 d_1 d_0}
66 : : * \u{d_3 d_2 d_1 d_0}
67 : : * \u{d_4 d_3 d_2 d_1 d_0}
68 : : * where d_0 ... d_4 are hexadecimal digits, to the appropriate character.
69 : : *
70 : : * If useEscSequences is false, then the characters of the constructed
71 : : * cvc5::internal::String correspond one-to-one with the input string.
72 : : */
73 : 170571 : String() = default;
74 : 39732 : explicit String(const std::string& s, bool useEscSequences = false)
75 : 39732 : : d_str(toInternal(s, useEscSequences))
76 : : {
77 : 39732 : }
78 : : explicit String(const std::wstring& s);
79 : : explicit String(const std::u32string& s);
80 : 103104 : explicit String(const char* s, bool useEscSequences = false)
81 : 103104 : : d_str(toInternal(std::string(s), useEscSequences))
82 : : {
83 : 103104 : }
84 : : explicit String(const std::vector<unsigned>& s);
85 : :
86 : 180546 : String& operator=(const String& y) {
87 [ + - ]: 180546 : if (this != &y) {
88 : 180546 : d_str = y.d_str;
89 : : }
90 : 180546 : return *this;
91 : : }
92 : :
93 : : String concat(const String& other) const;
94 : :
95 : 5295447 : bool operator==(const String& y) const { return cmp(y) == 0; }
96 : 142 : bool operator!=(const String& y) const { return cmp(y) != 0; }
97 : 42 : bool operator<(const String& y) const { return cmp(y) < 0; }
98 : : bool operator>(const String& y) const { return cmp(y) > 0; }
99 : 0 : bool operator<=(const String& y) const { return cmp(y) <= 0; }
100 : : bool operator>=(const String& y) const { return cmp(y) >= 0; }
101 : :
102 : : /**
103 : : * Returns true if this string is equal to y for their first n characters.
104 : : * If n is larger than the length of this string or y, this method returns
105 : : * true if and only if this string is equal to y.
106 : : */
107 : : bool strncmp(const String& y, std::size_t n) const;
108 : : /**
109 : : * Returns true if this string is equal to y for their last n characters.
110 : : * Similar to strncmp, if n is larger than the length of this string or y,
111 : : * this method returns true if and only if this string is equal to y.
112 : : */
113 : : bool rstrncmp(const String& y, std::size_t n) const;
114 : :
115 : : /* toString
116 : : * Converts this string to a std::string.
117 : : *
118 : : * The unprintable characters are converted to unicode escape sequences as
119 : : * described above.
120 : : *
121 : : * If useEscSequences is false, the string's printable characters are
122 : : * printed as characters. Notice that for all std::string s having only
123 : : * printable characters, we have that
124 : : * cvc5::internal::String( s ).toString() = s.
125 : : */
126 : : std::string toString(bool useEscSequences = false) const;
127 : : /* toWString
128 : : * Converts this string to a std::wstring.
129 : : *
130 : : * Unlike toString(), this method uses no escape sequences as both this class
131 : : * and std::wstring use 32bit characters.
132 : : */
133 : : std::wstring toWString() const;
134 : : /**
135 : : * Converts this string to a std::u32string.
136 : : *
137 : : * Unlike toString(), this method uses no escape sequences as both this class
138 : : * and std::u32string use 32bit characters.
139 : : */
140 : : std::u32string toU32String() const;
141 : : /** is this the empty string? */
142 : 194677 : bool empty() const { return d_str.empty(); }
143 : : /** is less than or equal to string y */
144 : : bool isLeq(const String& y) const;
145 : : /** Return the length of the string */
146 : 21823663 : std::size_t size() const { return d_str.size(); }
147 : :
148 : : bool isRepeated() const;
149 : : bool tailcmp(const String& y, int& c) const;
150 : :
151 : : /**
152 : : * Return the first position y occurs in this string, or std::string::npos
153 : : * otherwise.
154 : : */
155 : : std::size_t find(const String& y, const std::size_t start = 0) const;
156 : : /**
157 : : * Return the first position y occurs in this string searching from the end,
158 : : * or std::string::npos otherwise.
159 : : */
160 : : std::size_t rfind(const String& y, const std::size_t start = 0) const;
161 : : /** Returns true if y is a prefix of this */
162 : : bool hasPrefix(const String& y) const;
163 : : /** Returns true if y is a suffix of this */
164 : : bool hasSuffix(const String& y) const;
165 : : /** Replace the character at index i in this string with t */
166 : : String update(std::size_t i, const String& t) const;
167 : : /** Replace the first occurrence of s in this string with t */
168 : : String replace(const String& s, const String& t) const;
169 : : /** Return the substring of this string starting at index i */
170 : : String substr(std::size_t i) const;
171 : : /** Return the substring of this string starting at index i with size at most
172 : : * j */
173 : : String substr(std::size_t i, std::size_t j) const;
174 : : /** Return the prefix of this string of size at most i */
175 : 14198 : String prefix(std::size_t i) const { return substr(0, i); }
176 : : /** Return the suffix of this string of size at most i */
177 : 42589 : String suffix(std::size_t i) const { return substr(size() - i, i); }
178 : :
179 : : /** string overlap
180 : : *
181 : : * if overlap returns m>0,
182 : : * then the maximal suffix of this string that is a prefix of y is of length m.
183 : : *
184 : : * For example, if x is "abcdef", then:
185 : : * x.overlap("defg") = 3
186 : : * x.overlap("ab") = 0
187 : : * x.overlap("d") = 0
188 : : * x.overlap("bcdefdef") = 5
189 : : */
190 : : std::size_t overlap(const String& y) const;
191 : : /** string reverse overlap
192 : : *
193 : : * if roverlap returns m>0,
194 : : * then the maximal prefix of this string that is a suffix of y is of length m.
195 : : *
196 : : * For example, if x is "abcdef", then:
197 : : * x.roverlap("aaabc") = 3
198 : : * x.roverlap("def") = 0
199 : : * x.roverlap("d") = 0
200 : : * x.roverlap("defabcde") = 5
201 : : *
202 : : * Notice that x.overlap(y) = y.roverlap(x)
203 : : */
204 : : std::size_t roverlap(const String& y) const;
205 : :
206 : : /**
207 : : * Returns true if this string corresponds in text to a number, for example
208 : : * this returns true for strings "7", "12", "004", "0" and false for strings
209 : : * "abc", "4a", "-4", "".
210 : : */
211 : : bool isNumber() const;
212 : : /** Returns the corresponding rational for the text of this string. */
213 : : Rational toNumber() const;
214 : : /** Get the unsigned representation (code points) of this string */
215 : 293677 : const std::vector<unsigned>& getVec() const { return d_str; }
216 : : /**
217 : : * Get the unsigned (code point) value of the first character in this string
218 : : */
219 : : unsigned front() const;
220 : : /**
221 : : * Get the unsigned (code point) value of the last character in this string
222 : : */
223 : : unsigned back() const;
224 : : /** is the unsigned a digit?
225 : : *
226 : : * This is true for code points between 48 ('0') and 57 ('9').
227 : : */
228 : : static bool isDigit(unsigned character);
229 : : /** is the unsigned a hexadecimal digit?
230 : : *
231 : : * This is true for code points between 48 ('0') and 57 ('9'), code points
232 : : * between 65 ('A') and 70 ('F) and code points between 97 ('a') and 102 ('f).
233 : : */
234 : : static bool isHexDigit(unsigned character);
235 : : /** is the unsigned a printable code point?
236 : : *
237 : : * This is true for Unicode 32 (' ') to 126 ('~').
238 : : */
239 : : static bool isPrintable(unsigned character);
240 : :
241 : : /**
242 : : * Returns the maximum length of string representable by this class.
243 : : * Corresponds to the maximum size of d_str.
244 : : */
245 : : static size_t maxSize();
246 : : private:
247 : : /**
248 : : * Helper for toInternal: add character ch to vector vec, storing a string in
249 : : * internal format. This throws an error if ch is not a printable character,
250 : : * since non-printable characters must be escaped in SMT-LIB.
251 : : */
252 : : static void addCharToInternal(unsigned char ch, std::vector<unsigned>& vec);
253 : : /**
254 : : * Convert the string s to the internal format (vector of code points).
255 : : * The argument useEscSequences is whether to process unicode escape
256 : : * sequences.
257 : : */
258 : : static std::vector<unsigned> toInternal(const std::string& s,
259 : : bool useEscSequences);
260 : :
261 : : /**
262 : : * Returns a negative number if *this < y, 0 if *this and y are equal and a
263 : : * positive number if *this > y.
264 : : */
265 : : int cmp(const String& y) const;
266 : :
267 : : std::vector<unsigned> d_str;
268 : : }; /* class String */
269 : :
270 : : namespace strings {
271 : :
272 : : struct StringHashFunction
273 : : {
274 : : size_t operator()(const cvc5::internal::String& s) const;
275 : : }; /* struct StringHashFunction */
276 : :
277 : : } // namespace strings
278 : :
279 : : std::ostream& operator<<(std::ostream& os, const String& s);
280 : :
281 : : } // namespace cvc5::internal
282 : :
283 : : #endif /* CVC5__UTIL__STRING_H */
|
