Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Andres Noetzli
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 : : * Implementation of utility functions for words.
14 : : */
15 : :
16 : : #include "theory/strings/word.h"
17 : :
18 : : #include "expr/sequence.h"
19 : : #include "util/string.h"
20 : :
21 : : using namespace cvc5::internal::kind;
22 : :
23 : : namespace cvc5::internal {
24 : : namespace theory {
25 : : namespace strings {
26 : :
27 : 4022790 : Node Word::mkEmptyWord(TypeNode tn)
28 : : {
29 [ + + ]: 4022790 : if (tn.isString())
30 : : {
31 : 3941630 : std::vector<unsigned> vec;
32 : 7883260 : return tn.getNodeManager()->mkConst(String(vec));
33 : : }
34 [ + - ]: 81156 : else if (tn.isSequence())
35 : : {
36 : 81156 : std::vector<Node> seq;
37 : : return tn.getNodeManager()->mkConst(
38 : 162312 : Sequence(tn.getSequenceElementType(), seq));
39 : : }
40 : 0 : Unimplemented();
41 : : return Node::null();
42 : : }
43 : :
44 : 72366 : Node Word::mkWordFlatten(const std::vector<Node>& xs)
45 : : {
46 [ - + ][ - + ]: 72366 : Assert(!xs.empty());
[ - - ]
47 : 72366 : NodeManager* nm = xs[0].getNodeManager();
48 : 72366 : Kind k = xs[0].getKind();
49 [ + + ]: 72366 : if (k == Kind::CONST_STRING)
50 : : {
51 : 71149 : std::vector<unsigned> vec;
52 [ + + ]: 211800 : for (TNode x : xs)
53 : : {
54 [ - + ][ - + ]: 140651 : Assert(x.getKind() == Kind::CONST_STRING);
[ - - ]
55 : 140651 : String sx = x.getConst<String>();
56 : 140651 : const std::vector<unsigned>& vecc = sx.getVec();
57 : 140651 : vec.insert(vec.end(), vecc.begin(), vecc.end());
58 : : }
59 : 142298 : return nm->mkConst(String(vec));
60 : : }
61 [ + - ]: 1217 : else if (k == Kind::CONST_SEQUENCE)
62 : : {
63 : 2434 : std::vector<Node> seq;
64 : 1217 : TypeNode tn = xs[0].getType();
65 [ + + ]: 3650 : for (TNode x : xs)
66 : : {
67 [ - + ][ - + ]: 2433 : Assert(x.getType() == tn);
[ - - ]
68 : 2433 : const Sequence& sx = x.getConst<Sequence>();
69 : 2433 : const std::vector<Node>& vecc = sx.getVec();
70 : 2433 : seq.insert(seq.end(), vecc.begin(), vecc.end());
71 : : }
72 : : return nm->mkConst(
73 : 2434 : Sequence(tn.getSequenceElementType(), seq));
74 : : }
75 : 0 : Unimplemented();
76 : : return Node::null();
77 : : }
78 : :
79 : 2109930 : size_t Word::getLength(TNode x)
80 : : {
81 : 2109930 : Kind k = x.getKind();
82 [ + + ]: 2109930 : if (k == Kind::CONST_STRING)
83 : : {
84 : 2084420 : return x.getConst<String>().size();
85 : : }
86 [ + - ]: 25506 : else if (k == Kind::CONST_SEQUENCE)
87 : : {
88 : 25506 : return x.getConst<Sequence>().size();
89 : : }
90 : 0 : Unimplemented() << "Word::getLength on " << x;
91 : : return 0;
92 : : }
93 : :
94 : 139371 : std::vector<Node> Word::getChars(TNode x)
95 : : {
96 : 139371 : Kind k = x.getKind();
97 : 139371 : std::vector<Node> ret;
98 : 139371 : NodeManager* nm = x.getNodeManager();
99 [ + + ]: 139371 : if (k == Kind::CONST_STRING)
100 : : {
101 : 271234 : std::vector<unsigned> ccVec;
102 : 135617 : const std::vector<unsigned>& cvec = x.getConst<String>().getVec();
103 [ + + ]: 396638 : for (unsigned chVal : cvec)
104 : : {
105 : 261021 : ccVec.clear();
106 : 261021 : ccVec.push_back(chVal);
107 : 522042 : Node ch = nm->mkConst(String(ccVec));
108 : 261021 : ret.push_back(ch);
109 : : }
110 : 135617 : return ret;
111 : : }
112 [ + - ]: 3754 : else if (k == Kind::CONST_SEQUENCE)
113 : : {
114 : 7508 : TypeNode t = x.getConst<Sequence>().getType();
115 : 3754 : const Sequence& sx = x.getConst<Sequence>();
116 : 3754 : const std::vector<Node>& vec = sx.getVec();
117 [ + + ]: 7764 : for (const Node& v : vec)
118 : : {
119 : 8020 : ret.push_back(nm->mkConst(Sequence(t, {v})));
120 : : }
121 : 3754 : return ret;
122 : : }
123 : 0 : Unimplemented();
124 : : return ret;
125 : : }
126 : :
127 : 1118 : Node Word::getNth(TNode x, size_t n)
128 : : {
129 : 1118 : Kind k = x.getKind();
130 [ - + ]: 1118 : if (k == Kind::CONST_STRING)
131 : : {
132 : 0 : const std::vector<unsigned>& vec = x.getConst<String>().getVec();
133 : 0 : Assert(n < vec.size());
134 : 0 : return x.getNodeManager()->mkConstInt(vec[n]);
135 : : }
136 [ + - ]: 1118 : else if (k == Kind::CONST_SEQUENCE)
137 : : {
138 : 1118 : const std::vector<Node>& vec = x.getConst<Sequence>().getVec();
139 [ - + ][ - + ]: 1118 : Assert(n < vec.size());
[ - - ]
140 : 1118 : return vec[n];
141 : : }
142 : 0 : Unimplemented();
143 : : return Node::null();
144 : : }
145 : :
146 [ + + ][ + + ]: 475866 : bool Word::isEmpty(TNode x) { return x.isConst() && getLength(x) == 0; }
[ + + ][ - - ]
147 : :
148 : 29780 : bool Word::strncmp(TNode x, TNode y, std::size_t n)
149 : : {
150 : 29780 : Kind k = x.getKind();
151 [ + + ]: 29780 : if (k == Kind::CONST_STRING)
152 : : {
153 [ - + ][ - + ]: 29710 : Assert(y.getKind() == Kind::CONST_STRING);
[ - - ]
154 : 59420 : String sx = x.getConst<String>();
155 : 59420 : String sy = y.getConst<String>();
156 : 29710 : return sx.strncmp(sy, n);
157 : : }
158 [ + - ]: 70 : else if (k == Kind::CONST_SEQUENCE)
159 : : {
160 [ - + ][ - + ]: 70 : Assert(y.getKind() == Kind::CONST_SEQUENCE);
[ - - ]
161 : 70 : const Sequence& sx = x.getConst<Sequence>();
162 : 70 : const Sequence& sy = y.getConst<Sequence>();
163 : 70 : return sx.strncmp(sy, n);
164 : : }
165 : 0 : Unimplemented();
166 : : return false;
167 : : }
168 : :
169 : 27294 : bool Word::rstrncmp(TNode x, TNode y, std::size_t n)
170 : : {
171 : 27294 : Kind k = x.getKind();
172 [ + + ]: 27294 : if (k == Kind::CONST_STRING)
173 : : {
174 [ - + ][ - + ]: 27147 : Assert(y.getKind() == Kind::CONST_STRING);
[ - - ]
175 : 54294 : String sx = x.getConst<String>();
176 : 54294 : String sy = y.getConst<String>();
177 : 27147 : return sx.rstrncmp(sy, n);
178 : : }
179 [ + - ]: 147 : else if (k == Kind::CONST_SEQUENCE)
180 : : {
181 [ - + ][ - + ]: 147 : Assert(y.getKind() == Kind::CONST_SEQUENCE);
[ - - ]
182 : 147 : const Sequence& sx = x.getConst<Sequence>();
183 : 147 : const Sequence& sy = y.getConst<Sequence>();
184 : 147 : return sx.rstrncmp(sy, n);
185 : : }
186 : 0 : Unimplemented();
187 : : return false;
188 : : }
189 : :
190 : 93632 : std::size_t Word::find(TNode x, TNode y, std::size_t start)
191 : : {
192 : 93632 : Kind k = x.getKind();
193 [ + + ]: 93632 : if (k == Kind::CONST_STRING)
194 : : {
195 [ - + ][ - + ]: 91319 : Assert(y.getKind() == Kind::CONST_STRING);
[ - - ]
196 : 182638 : String sx = x.getConst<String>();
197 : 182638 : String sy = y.getConst<String>();
198 : 91319 : return sx.find(sy, start);
199 : : }
200 [ + - ]: 2313 : else if (k == Kind::CONST_SEQUENCE)
201 : : {
202 [ - + ][ - + ]: 2313 : Assert(y.getKind() == Kind::CONST_SEQUENCE);
[ - - ]
203 : 2313 : const Sequence& sx = x.getConst<Sequence>();
204 : 2313 : const Sequence& sy = y.getConst<Sequence>();
205 : 2313 : return sx.find(sy, start);
206 : : }
207 : 0 : Unimplemented();
208 : : return 0;
209 : : }
210 : :
211 : 16745 : std::size_t Word::rfind(TNode x, TNode y, std::size_t start)
212 : : {
213 : 16745 : Kind k = x.getKind();
214 [ + + ]: 16745 : if (k == Kind::CONST_STRING)
215 : : {
216 [ - + ][ - + ]: 16491 : Assert(y.getKind() == Kind::CONST_STRING);
[ - - ]
217 : 32982 : String sx = x.getConst<String>();
218 : 32982 : String sy = y.getConst<String>();
219 : 16491 : return sx.rfind(sy, start);
220 : : }
221 [ + - ]: 254 : else if (k == Kind::CONST_SEQUENCE)
222 : : {
223 [ - + ][ - + ]: 254 : Assert(y.getKind() == Kind::CONST_SEQUENCE);
[ - - ]
224 : 254 : const Sequence& sx = x.getConst<Sequence>();
225 : 254 : const Sequence& sy = y.getConst<Sequence>();
226 : 254 : return sx.rfind(sy, start);
227 : : }
228 : 0 : Unimplemented();
229 : : return 0;
230 : : }
231 : :
232 : 5876 : bool Word::hasPrefix(TNode x, TNode y)
233 : : {
234 : 5876 : Kind k = x.getKind();
235 [ + + ]: 5876 : if (k == Kind::CONST_STRING)
236 : : {
237 [ - + ][ - + ]: 5868 : Assert(y.getKind() == Kind::CONST_STRING);
[ - - ]
238 : 11736 : String sx = x.getConst<String>();
239 : 11736 : String sy = y.getConst<String>();
240 : 5868 : return sx.hasPrefix(sy);
241 : : }
242 [ + - ]: 8 : else if (k == Kind::CONST_SEQUENCE)
243 : : {
244 [ - + ][ - + ]: 8 : Assert(y.getKind() == Kind::CONST_SEQUENCE);
[ - - ]
245 : 8 : const Sequence& sx = x.getConst<Sequence>();
246 : 8 : const Sequence& sy = y.getConst<Sequence>();
247 : 8 : return sx.hasPrefix(sy);
248 : : }
249 : 0 : Unimplemented();
250 : : return false;
251 : : }
252 : :
253 : 18416 : bool Word::hasSuffix(TNode x, TNode y)
254 : : {
255 : 18416 : Kind k = x.getKind();
256 [ + + ]: 18416 : if (k == Kind::CONST_STRING)
257 : : {
258 [ - + ][ - + ]: 18180 : Assert(y.getKind() == Kind::CONST_STRING);
[ - - ]
259 : 36360 : String sx = x.getConst<String>();
260 : 36360 : String sy = y.getConst<String>();
261 : 18180 : return sx.hasSuffix(sy);
262 : : }
263 [ + - ]: 236 : else if (k == Kind::CONST_SEQUENCE)
264 : : {
265 [ - + ][ - + ]: 236 : Assert(y.getKind() == Kind::CONST_SEQUENCE);
[ - - ]
266 : 236 : const Sequence& sx = x.getConst<Sequence>();
267 : 236 : const Sequence& sy = y.getConst<Sequence>();
268 : 236 : return sx.hasSuffix(sy);
269 : : }
270 : 0 : Unimplemented();
271 : : return false;
272 : : }
273 : :
274 : 208 : Node Word::update(TNode x, std::size_t i, TNode t)
275 : : {
276 : 208 : NodeManager* nm = x.getNodeManager();
277 : 208 : Kind k = x.getKind();
278 [ + + ]: 208 : if (k == Kind::CONST_STRING)
279 : : {
280 [ - + ][ - + ]: 166 : Assert(t.getKind() == Kind::CONST_STRING);
[ - - ]
281 : 332 : String sx = x.getConst<String>();
282 : 166 : String st = t.getConst<String>();
283 : 332 : return nm->mkConst(String(sx.update(i, st)));
284 : : }
285 [ + - ]: 42 : else if (k == Kind::CONST_SEQUENCE)
286 : : {
287 [ - + ][ - + ]: 42 : Assert(t.getKind() == Kind::CONST_SEQUENCE);
[ - - ]
288 : 42 : const Sequence& sx = x.getConst<Sequence>();
289 : 42 : const Sequence& st = t.getConst<Sequence>();
290 : 84 : Sequence res = sx.update(i, st);
291 : 42 : return nm->mkConst(res);
292 : : }
293 : 0 : Unimplemented();
294 : : return Node::null();
295 : : }
296 : 3 : Node Word::replace(TNode x, TNode y, TNode t)
297 : : {
298 : 3 : NodeManager* nm = x.getNodeManager();
299 : 3 : Kind k = x.getKind();
300 [ + - ]: 3 : if (k == Kind::CONST_STRING)
301 : : {
302 [ - + ][ - + ]: 3 : Assert(y.getKind() == Kind::CONST_STRING);
[ - - ]
303 [ - + ][ - + ]: 3 : Assert(t.getKind() == Kind::CONST_STRING);
[ - - ]
304 : 6 : String sx = x.getConst<String>();
305 : 6 : String sy = y.getConst<String>();
306 : 3 : String st = t.getConst<String>();
307 : 6 : return nm->mkConst(String(sx.replace(sy, st)));
308 : : }
309 [ - - ]: 0 : else if (k == Kind::CONST_SEQUENCE)
310 : : {
311 : 0 : Assert(y.getKind() == Kind::CONST_SEQUENCE);
312 : 0 : Assert(t.getKind() == Kind::CONST_SEQUENCE);
313 : 0 : const Sequence& sx = x.getConst<Sequence>();
314 : 0 : const Sequence& sy = y.getConst<Sequence>();
315 : 0 : const Sequence& st = t.getConst<Sequence>();
316 : 0 : Sequence res = sx.replace(sy, st);
317 : 0 : return nm->mkConst(res);
318 : : }
319 : 0 : Unimplemented();
320 : : return Node::null();
321 : : }
322 : 12988 : Node Word::substr(TNode x, std::size_t i)
323 : : {
324 : 12988 : NodeManager* nm = x.getNodeManager();
325 : 12988 : Kind k = x.getKind();
326 [ + + ]: 12988 : if (k == Kind::CONST_STRING)
327 : : {
328 : 12920 : String sx = x.getConst<String>();
329 : 25840 : return nm->mkConst(String(sx.substr(i)));
330 : : }
331 [ + - ]: 68 : else if (k == Kind::CONST_SEQUENCE)
332 : : {
333 : 68 : const Sequence& sx = x.getConst<Sequence>();
334 : 136 : Sequence res = sx.substr(i);
335 : 68 : return nm->mkConst(res);
336 : : }
337 : 0 : Unimplemented();
338 : : return Node::null();
339 : : }
340 : 63501 : Node Word::substr(TNode x, std::size_t i, std::size_t j)
341 : : {
342 : 63501 : NodeManager* nm = x.getNodeManager();
343 : 63501 : Kind k = x.getKind();
344 [ + + ]: 63501 : if (k == Kind::CONST_STRING)
345 : : {
346 : 63146 : String sx = x.getConst<String>();
347 : 126292 : return nm->mkConst(String(sx.substr(i, j)));
348 : : }
349 [ + - ]: 355 : else if (k == Kind::CONST_SEQUENCE)
350 : : {
351 : 355 : const Sequence& sx = x.getConst<Sequence>();
352 : 710 : Sequence res = sx.substr(i, j);
353 : 355 : return nm->mkConst(res);
354 : : }
355 : 0 : Unimplemented();
356 : : return Node::null();
357 : : }
358 : :
359 : 22424 : Node Word::prefix(TNode x, std::size_t i) { return substr(x, 0, i); }
360 : :
361 : 28839 : Node Word::suffix(TNode x, std::size_t i)
362 : : {
363 : 28839 : NodeManager* nm = x.getNodeManager();
364 : 28839 : Kind k = x.getKind();
365 [ + + ]: 28839 : if (k == Kind::CONST_STRING)
366 : : {
367 : 28788 : String sx = x.getConst<String>();
368 : 57576 : return nm->mkConst(String(sx.suffix(i)));
369 : : }
370 [ + - ]: 51 : else if (k == Kind::CONST_SEQUENCE)
371 : : {
372 : 51 : const Sequence& sx = x.getConst<Sequence>();
373 : 102 : Sequence res = sx.suffix(i);
374 : 51 : return nm->mkConst(res);
375 : : }
376 : 0 : Unimplemented();
377 : : return Node::null();
378 : : }
379 : :
380 : 2870 : bool Word::hasOverlap(TNode x, TNode y, bool rev)
381 : : {
382 : 2870 : Kind k = x.getKind();
383 [ + + ]: 2870 : if (k == Kind::CONST_STRING)
384 : : {
385 [ - + ][ - + ]: 2800 : Assert(y.getKind() == Kind::CONST_STRING);
[ - - ]
386 : 2800 : const String& sx = x.getConst<String>();
387 : 2800 : const String& sy = y.getConst<String>();
388 [ + + ]: 2800 : if (sx.empty())
389 : : {
390 : 64 : return false;
391 : : }
392 [ + + ]: 2736 : if (rev)
393 : : {
394 [ + + ][ + + ]: 69 : return (sx.find(sy) != std::string::npos || sx.roverlap(sy) != 0);
395 : : }
396 [ + + ][ + + ]: 2667 : return (sx.find(sy) != std::string::npos || sx.overlap(sy) != 0);
397 : : }
398 [ + - ]: 70 : else if (k == Kind::CONST_SEQUENCE)
399 : : {
400 [ - + ][ - + ]: 70 : Assert(y.getKind() == Kind::CONST_SEQUENCE);
[ - - ]
401 : 70 : const Sequence& sx = x.getConst<Sequence>();
402 : 70 : const Sequence& sy = y.getConst<Sequence>();
403 [ + + ]: 70 : if (sx.empty())
404 : : {
405 : 3 : return false;
406 : : }
407 [ - + ]: 67 : if (rev)
408 : : {
409 [ - - ][ - - ]: 0 : return (sx.find(sy) != std::string::npos || sx.roverlap(sy) != 0);
410 : : }
411 [ + - ][ + + ]: 67 : return (sx.find(sy) != std::string::npos || sx.overlap(sy) != 0);
412 : : }
413 : 0 : Unimplemented();
414 : : return false;
415 : : }
416 : :
417 : 11 : bool Word::hasBidirectionalOverlap(TNode x, TNode y)
418 : : {
419 : 11 : return hasOverlap(x, y, false) || hasOverlap(y, x, false);
420 : : }
421 : :
422 : 8248 : std::size_t Word::overlap(TNode x, TNode y)
423 : : {
424 : 8248 : Kind k = x.getKind();
425 [ + + ]: 8248 : if (k == Kind::CONST_STRING)
426 : : {
427 [ - + ][ - + ]: 8148 : Assert(y.getKind() == Kind::CONST_STRING);
[ - - ]
428 : 16296 : String sx = x.getConst<String>();
429 : 16296 : String sy = y.getConst<String>();
430 : 8148 : return sx.overlap(sy);
431 : : }
432 [ + - ]: 100 : else if (k == Kind::CONST_SEQUENCE)
433 : : {
434 [ - + ][ - + ]: 100 : Assert(y.getKind() == Kind::CONST_SEQUENCE);
[ - - ]
435 : 100 : const Sequence& sx = x.getConst<Sequence>();
436 : 100 : const Sequence& sy = y.getConst<Sequence>();
437 : 100 : return sx.overlap(sy);
438 : : }
439 : 0 : Unimplemented();
440 : : return 0;
441 : : }
442 : :
443 : 4205 : std::size_t Word::roverlap(TNode x, TNode y)
444 : : {
445 : 4205 : Kind k = x.getKind();
446 [ + + ]: 4205 : if (k == Kind::CONST_STRING)
447 : : {
448 [ - + ][ - + ]: 4183 : Assert(y.getKind() == Kind::CONST_STRING);
[ - - ]
449 : 8366 : String sx = x.getConst<String>();
450 : 8366 : String sy = y.getConst<String>();
451 : 4183 : return sx.roverlap(sy);
452 : : }
453 [ + - ]: 22 : else if (k == Kind::CONST_SEQUENCE)
454 : : {
455 [ - + ][ - + ]: 22 : Assert(y.getKind() == Kind::CONST_SEQUENCE);
[ - - ]
456 : 22 : const Sequence& sx = x.getConst<Sequence>();
457 : 22 : const Sequence& sy = y.getConst<Sequence>();
458 : 22 : return sx.roverlap(sy);
459 : : }
460 : 0 : Unimplemented();
461 : : return 0;
462 : : }
463 : :
464 : 0 : bool Word::isRepeated(TNode x)
465 : : {
466 : 0 : Kind k = x.getKind();
467 [ - - ]: 0 : if (k == Kind::CONST_STRING)
468 : : {
469 : 0 : return x.getConst<String>().isRepeated();
470 : : }
471 [ - - ]: 0 : else if (k == Kind::CONST_SEQUENCE)
472 : : {
473 : 0 : return x.getConst<Sequence>().isRepeated();
474 : : }
475 : 0 : Unimplemented();
476 : : return false;
477 : : }
478 : :
479 : 17766 : Node Word::splitConstant(TNode x, TNode y, size_t& index, bool isRev)
480 : : {
481 [ + - ][ + - ]: 35532 : Assert(x.isConst() && y.isConst());
[ - + ][ - - ]
482 : 17766 : size_t lenA = getLength(x);
483 : 17766 : size_t lenB = getLength(y);
484 [ + + ]: 17766 : index = lenA <= lenB ? 1 : 0;
485 [ + + ]: 17766 : size_t lenShort = index == 1 ? lenA : lenB;
486 : 17766 : bool cmp = isRev ? rstrncmp(x, y, lenShort) : strncmp(x, y, lenShort);
487 [ + + ]: 17766 : if (cmp)
488 : : {
489 [ + + ]: 23508 : Node l = index == 0 ? x : y;
490 [ + + ]: 11754 : if (isRev)
491 : : {
492 : 5889 : size_t new_len = getLength(l) - lenShort;
493 : 5889 : return substr(l, 0, new_len);
494 : : }
495 : : else
496 : : {
497 : 5865 : return substr(l, lenShort);
498 : : }
499 : : }
500 : : // not the same prefix/suffix
501 : 6012 : return Node::null();
502 : : }
503 : :
504 : 168 : Node Word::reverse(TNode x)
505 : : {
506 : 168 : NodeManager* nm = x.getNodeManager();
507 : 168 : Kind k = x.getKind();
508 [ + + ]: 168 : if (k == Kind::CONST_STRING)
509 : : {
510 : 272 : String sx = x.getConst<String>();
511 : 136 : std::vector<unsigned> nvec = sx.getVec();
512 : 136 : std::reverse(nvec.begin(), nvec.end());
513 : 272 : return nm->mkConst(String(nvec));
514 : : }
515 [ + - ]: 32 : else if (k == Kind::CONST_SEQUENCE)
516 : : {
517 : 32 : const Sequence& sx = x.getConst<Sequence>();
518 : 32 : const std::vector<Node>& vecc = sx.getVec();
519 : 64 : std::vector<Node> vecr(vecc.begin(), vecc.end());
520 : 32 : std::reverse(vecr.begin(), vecr.end());
521 : 64 : Sequence res(sx.getType(), vecr);
522 : 32 : return nm->mkConst(res);
523 : : }
524 : 0 : Unimplemented();
525 : : return Node::null();
526 : : }
527 : :
528 : : } // namespace strings
529 : : } // namespace theory
530 : : } // namespace cvc5::internal
|
