projects / cvc5.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
string fmf changes
[cvc5.git] / src / theory / strings / regexp_operation.cpp
1 /********************* */
2 /*! \file regexp_operation.CPP
3 ** \verbatim
4 ** Original author: Tianyi Liang
5 ** Major contributors: Tianyi Liang, Andrew Reynolds
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2013-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
11 **
12 ** \brief Regular Expresion Operations
13 **
14 ** Regular Expresion Operations
15 **/
16
17 #include "theory/strings/regexp_operation.h"
18 #include "expr/kind.h"
19
20 namespace CVC4 {
21 namespace theory {
22 namespace strings {
23
24 RegExpOpr::RegExpOpr() {
25 d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
26 // All Charactors = all printable ones 32-126
27 d_char_start = 'a';//' ';
28 d_char_end = 'c';//'~';
29 d_sigma = mkAllExceptOne( '\0' );
30 d_sigma_star = NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, d_sigma );
31 }
32
33 int RegExpOpr::gcd ( int a, int b ) {
34 int c;
35 while ( a != 0 ) {
36 c = a; a = b%a; b = c;
37 }
38 return b;
39 }
40
41 bool RegExpOpr::checkConstRegExp( Node r ) {
42 Trace("strings-regexp-cstre") << "RegExp-CheckConstRegExp starts with " << mkString( r ) << std::endl;
43 bool ret = true;
44 if( d_cstre_cache.find( r ) != d_cstre_cache.end() ) {
45 ret = d_cstre_cache[r];
46 } else {
47 if(r.getKind() == kind::STRING_TO_REGEXP) {
48 Node tmp = Rewriter::rewrite( r[0] );
49 ret = tmp.isConst();
50 } else {
51 for(unsigned i=0; i<r.getNumChildren(); ++i) {
52 if(!checkConstRegExp(r[i])) {
53 ret = false; break;
54 }
55 }
56 }
57 d_cstre_cache[r] = ret;
58 }
59 return ret;
60 }
61
62 // 0-unknown, 1-yes, 2-no
63 int RegExpOpr::delta( Node r ) {
64 Trace("strings-regexp-delta") << "RegExp-Delta starts with " << mkString( r ) << std::endl;
65 int ret = 0;
66 if( d_delta_cache.find( r ) != d_delta_cache.end() ) {
67 ret = d_delta_cache[r];
68 } else {
69 int k = r.getKind();
70 switch( k ) {
71 case kind::STRING_TO_REGEXP:
72 {
73 if(r[0].isConst()) {
74 if(r[0] == d_emptyString) {
75 ret = 1;
76 } else {
77 ret = 2;
78 }
79 } else {
80 ret = 0;
81 }
82 }
83 break;
84 case kind::REGEXP_CONCAT:
85 {
86 bool flag = false;
87 for(unsigned i=0; i<r.getNumChildren(); ++i) {
88 int tmp = delta( r[i] );
89 if(tmp == 2) {
90 ret = 2;
91 break;
92 } else if(tmp == 0) {
93 flag = true;
94 }
95 }
96 if(!flag && ret != 2) {
97 ret = 1;
98 }
99 }
100 break;
101 case kind::REGEXP_OR:
102 {
103 bool flag = false;
104 for(unsigned i=0; i<r.getNumChildren(); ++i) {
105 int tmp = delta( r[i] );
106 if(tmp == 1) {
107 ret = 1;
108 break;
109 } else if(tmp == 0) {
110 flag = true;
111 }
112 }
113 if(!flag && ret != 1) {
114 ret = 2;
115 }
116 }
117 break;
118 case kind::REGEXP_INTER:
119 {
120 bool flag = true;
121 for(unsigned i=0; i<r.getNumChildren(); ++i) {
122 int tmp = delta( r[i] );
123 if(tmp == 2) {
124 ret = 2; flag=false;
125 break;
126 } else if(tmp == 0) {
127 flag=false;
128 break;
129 }
130 }
131 if(flag) {
132 ret = 1;
133 }
134 }
135 break;
136 case kind::REGEXP_STAR:
137 {
138 ret = 1;
139 }
140 break;
141 case kind::REGEXP_PLUS:
142 {
143 ret = delta( r[0] );
144 }
145 break;
146 case kind::REGEXP_OPT:
147 {
148 ret = 1;
149 }
150 break;
151 case kind::REGEXP_RANGE:
152 {
153 ret = 2;
154 }
155 break;
156 default:
157 //TODO: special sym: sigma, none, all
158 Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in delta of RegExp." << std::endl;
159 //AlwaysAssert( false );
160 //return Node::null();
161 }
162 d_delta_cache[r] = ret;
163 }
164 Trace("strings-regexp-delta") << "RegExp-Delta returns : " << ret << std::endl;
165 return ret;
166 }
167
168 //null - no solution
169 Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) {
170 Assert( c.size() < 2 );
171 Trace("strings-regexp-derivative") << "RegExp-derivative starts with R{ " << mkString( r ) << " }, c=" << c << std::endl;
172 Node retNode = Node::null();
173 PairDvStr dv = std::make_pair( r, c );
174 if( d_dv_cache.find( dv ) != d_dv_cache.end() ) {
175 retNode = d_dv_cache[dv];
176 } else if( c.isEmptyString() ){
177 int tmp = delta( r );
178 if(tmp == 0) {
179 retNode = Node::null();
180 // TODO variable
181 } else if(tmp == 1) {
182 retNode = r;
183 } else {
184 retNode = Node::null();
185 }
186 } else {
187 int k = r.getKind();
188 switch( k ) {
189 case kind::STRING_TO_REGEXP:
190 {
191 if(r[0].isConst()) {
192 if(r[0] == d_emptyString) {
193 retNode = Node::null();
194 } else {
195 if(r[0].getConst< CVC4::String >().getFirstChar() == c.getFirstChar()) {
196 retNode = r[0].getConst< CVC4::String >().size() == 1 ? d_emptyString : NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP,
197 NodeManager::currentNM()->mkConst( r[0].getConst< CVC4::String >().substr(1) ) );
198 } else {
199 retNode = Node::null();
200 }
201 }
202 } else {
203 retNode = Node::null();
204 // TODO variable
205 }
206 }
207 break;
208 case kind::REGEXP_CONCAT:
209 {
210 std::vector< Node > vec_nodes;
211 for(unsigned i=0; i<r.getNumChildren(); ++i) {
212 Node dc = derivativeSingle(r[i], c);
213 if(!dc.isNull()) {
214 std::vector< Node > vec_nodes2;
215 if(dc != d_emptyString) {
216 vec_nodes2.push_back( dc );
217 }
218 for(unsigned j=i+1; j<r.getNumChildren(); ++j) {
219 if(r[j] != d_emptyString) {
220 vec_nodes2.push_back( r[j] );
221 }
222 }
223 Node tmp = vec_nodes2.size()==0 ? d_emptyString :
224 ( vec_nodes2.size()==1 ? vec_nodes2[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, vec_nodes2 ) );
225 if(std::find(vec_nodes.begin(), vec_nodes.end(), tmp) == vec_nodes.end()) {
226 vec_nodes.push_back( tmp );
227 }
228 }
229
230 if( delta( r[i] ) != 1 ) {
231 break;
232 }
233 }
234 retNode = vec_nodes.size() == 0 ? Node::null() :
235 ( vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes ) );
236 }
237 break;
238 case kind::REGEXP_OR:
239 {
240 std::vector< Node > vec_nodes;
241 for(unsigned i=0; i<r.getNumChildren(); ++i) {
242 Node dc = derivativeSingle(r[i], c);
243 if(!dc.isNull()) {
244 if(std::find(vec_nodes.begin(), vec_nodes.end(), dc) == vec_nodes.end()) {
245 vec_nodes.push_back( dc );
246 }
247 }
248 Trace("strings-regexp-derivative") << "RegExp-derivative OR R[" << i << "]{ " << mkString(r[i]) << " returns " << mkString(dc) << std::endl;
249 }
250 retNode = vec_nodes.size() == 0 ? Node::null() :
251 ( vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes ) );
252 }
253 break;
254 case kind::REGEXP_INTER:
255 {
256 bool flag = true;
257 bool flag_sg = false;
258 std::vector< Node > vec_nodes;
259 for(unsigned i=0; i<r.getNumChildren(); ++i) {
260 Node dc = derivativeSingle(r[i], c);
261 if(!dc.isNull()) {
262 if(dc == d_sigma_star) {
263 flag_sg = true;
264 } else {
265 if(std::find(vec_nodes.begin(), vec_nodes.end(), dc) == vec_nodes.end()) {
266 vec_nodes.push_back( dc );
267 }
268 }
269 } else {
270 flag = false;
271 break;
272 }
273 }
274 if(flag) {
275 if(vec_nodes.size() == 0 && flag_sg) {
276 retNode = d_sigma_star;
277 } else {
278 retNode = vec_nodes.size() == 0 ? Node::null() :
279 ( vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_INTER, vec_nodes ) );
280 }
281 } else {
282 retNode = Node::null();
283 }
284 }
285 break;
286 case kind::REGEXP_STAR:
287 {
288 Node dc = derivativeSingle(r[0], c);
289 if(!dc.isNull()) {
290 retNode = dc==d_emptyString ? r : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, dc, r );
291 } else {
292 retNode = Node::null();
293 }
294 }
295 break;
296 case kind::REGEXP_PLUS:
297 {
298 Node dc = derivativeSingle(r[0], c);
299 if(!dc.isNull()) {
300 retNode = dc==d_emptyString ? r : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, dc, r );
301 } else {
302 retNode = Node::null();
303 }
304 }
305 break;
306 case kind::REGEXP_OPT:
307 {
308 retNode = derivativeSingle(r[0], c);
309 }
310 break;
311 case kind::REGEXP_RANGE:
312 {
313 char ch = c.getFirstChar();
314 if (ch >= r[0].getConst< CVC4::String >().getFirstChar() && ch <= r[1].getConst< CVC4::String >().getFirstChar() ) {
315 retNode = d_emptyString;
316 } else {
317 retNode = Node::null();
318 }
319 }
320 break;
321 default:
322 //TODO: special sym: sigma, none, all
323 Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in derivative of RegExp." << std::endl;
324 //AlwaysAssert( false );
325 //return Node::null();
326 }
327 if(!retNode.isNull()) {
328 retNode = Rewriter::rewrite( retNode );
329 }
330 d_dv_cache[dv] = retNode;
331 }
332 Trace("strings-regexp-derivative") << "RegExp-derivative returns : " << mkString( retNode ) << std::endl;
333 return retNode;
334 }
335
336 //TODO:
337 bool RegExpOpr::guessLength( Node r, int &co ) {
338 int k = r.getKind();
339 switch( k ) {
340 case kind::STRING_TO_REGEXP:
341 {
342 if(r[0].isConst()) {
343 co += r[0].getConst< CVC4::String >().size();
344 return true;
345 } else {
346 return false;
347 }
348 }
349 break;
350 case kind::REGEXP_CONCAT:
351 {
352 for(unsigned i=0; i<r.getNumChildren(); ++i) {
353 if(!guessLength( r[i], co)) {
354 return false;
355 }
356 }
357 return true;
358 }
359 break;
360 case kind::REGEXP_OR:
361 {
362 int g_co;
363 for(unsigned i=0; i<r.getNumChildren(); ++i) {
364 int cop = 0;
365 if(!guessLength( r[i], cop)) {
366 return false;
367 }
368 if(i == 0) {
369 g_co = cop;
370 } else {
371 g_co = gcd(g_co, cop);
372 }
373 }
374 return true;
375 }
376 break;
377 case kind::REGEXP_INTER:
378 {
379 int g_co;
380 for(unsigned i=0; i<r.getNumChildren(); ++i) {
381 int cop = 0;
382 if(!guessLength( r[i], cop)) {
383 return false;
384 }
385 if(i == 0) {
386 g_co = cop;
387 } else {
388 g_co = gcd(g_co, cop);
389 }
390 }
391 return true;
392 }
393 break;
394 case kind::REGEXP_STAR:
395 {
396 co = 0;
397 return true;
398 }
399 break;
400 default:
401 Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in membership of RegExp." << std::endl;
402 return false;
403 }
404 }
405
406 void RegExpOpr::firstChar( Node r ) {
407 Trace("strings-regexp-firstchar") << "Head characters: ";
408 for(char ch = d_char_start; ch <= d_char_end; ++ch) {
409 CVC4::String c(ch);
410 Node dc = derivativeSingle(r, ch);
411 if(!dc.isNull()) {
412 Trace("strings-regexp-firstchar") << c << " (" << mkString(dc) << ")" << std::endl;
413 }
414 }
415 Trace("strings-regexp-firstchar") << std::endl;
416 }
417
418 bool RegExpOpr::follow( Node r, CVC4::String c, std::vector< char > &vec_chars ) {
419 int k = r.getKind();
420 switch( k ) {
421 case kind::STRING_TO_REGEXP:
422 {
423 if(r[0].isConst()) {
424 if(r[0] != d_emptyString) {
425 char t1 = r[0].getConst< CVC4::String >().getFirstChar();
426 if(c.isEmptyString()) {
427 vec_chars.push_back( t1 );
428 return true;
429 } else {
430 char t2 = c.getFirstChar();
431 if(t1 != t2) {
432 return false;
433 } else {
434 if(c.size() >= 2) {
435 vec_chars.push_back( c.substr(1,1).getFirstChar() );
436 } else {
437 vec_chars.push_back( '\0' );
438 }
439 return true;
440 }
441 }
442 } else {
443 return false;
444 }
445 } else {
446 return false;
447 }
448 }
449 break;
450 case kind::REGEXP_CONCAT:
451 {
452 for(unsigned i=0; i<r.getNumChildren(); ++i) {
453 if( follow(r[i], c, vec_chars) ) {
454 if(vec_chars[vec_chars.size() - 1] == '\0') {
455 vec_chars.pop_back();
456 c = d_emptyString.getConst< CVC4::String >();
457 }
458 } else {
459 return false;
460 }
461 }
462 vec_chars.push_back( '\0' );
463 return true;
464 }
465 break;
466 case kind::REGEXP_OR:
467 {
468 bool flag = false;
469 for(unsigned i=0; i<r.getNumChildren(); ++i) {
470 if( follow(r[i], c, vec_chars) ) {
471 flag=true;
472 }
473 }
474 return flag;
475 }
476 break;
477 case kind::REGEXP_INTER:
478 {
479 std::vector< char > vt2;
480 for(unsigned i=0; i<r.getNumChildren(); ++i) {
481 std::vector< char > v_tmp;
482 if( !follow(r[i], c, v_tmp) ) {
483 return false;
484 }
485 std::vector< char > vt3(vt2);
486 vt2.clear();
487 std::set_intersection( vt3.begin(), vt3.end(), v_tmp.begin(), v_tmp.end(), vt2.begin() );
488 if(vt2.size() == 0) {
489 return false;
490 }
491 }
492 vec_chars.insert( vec_chars.end(), vt2.begin(), vt2.end() );
493 return true;
494 }
495 break;
496 case kind::REGEXP_STAR:
497 {
498 if(follow(r[0], c, vec_chars)) {
499 if(vec_chars[vec_chars.size() - 1] == '\0') {
500 if(c.isEmptyString()) {
501 return true;
502 } else {
503 vec_chars.pop_back();
504 c = d_emptyString.getConst< CVC4::String >();
505 return follow(r[0], c, vec_chars);
506 }
507 } else {
508 return true;
509 }
510 } else {
511 vec_chars.push_back( '\0' );
512 return true;
513 }
514 }
515 break;
516 /*
517 case kind::REGEXP_PLUS:
518 {
519 ret = delta( r[0] );
520 }
521 break;
522 case kind::REGEXP_OPT:
523 {
524 ret = 1;
525 }
526 break;
527 case kind::REGEXP_RANGE:
528 {
529 ret = 2;
530 }
531 break;*/
532 default:
533 //TODO: special sym: sigma, none, all
534 Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in delta of RegExp." << std::endl;
535 //AlwaysAssert( false );
536 //return Node::null();
537 return false;
538 }
539 }
540
541 Node RegExpOpr::mkAllExceptOne( char exp_c ) {
542 std::vector< Node > vec_nodes;
543 for(char c=d_char_start; c<=d_char_end; ++c) {
544 if(c != exp_c ) {
545 Node n = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst( ::CVC4::String( c ) ) );
546 vec_nodes.push_back( n );
547 }
548 }
549 return NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes );
550 }
551
552 Node RegExpOpr::complement( Node r ) {
553 Trace("strings-regexp-compl") << "RegExp-Compl starts with " << mkString( r ) << std::endl;
554 Node retNode = r;
555 if( d_compl_cache.find( r ) != d_compl_cache.end() ) {
556 retNode = d_compl_cache[r];
557 } else {
558 int k = r.getKind();
559 switch( k ) {
560 case kind::STRING_TO_REGEXP:
561 {
562 if(r[0].isConst()) {
563 if(r[0] == d_emptyString) {
564 retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, d_sigma, d_sigma_star );
565 } else {
566 std::vector< Node > vec_nodes;
567 vec_nodes.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, d_emptyString ) );
568 CVC4::String s = r[0].getConst<String>();
569 for(unsigned i=0; i<s.size(); ++i) {
570 char c = s.substr(i, 1).getFirstChar();
571 Node tmp = mkAllExceptOne( c );
572 if(i != 0 ) {
573 Node tmph = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP,
574 NodeManager::currentNM()->mkConst( s.substr(0, i) ) );
575 tmp = NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, tmph, tmp );
576 }
577 tmp = NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, tmp, d_sigma_star );
578 vec_nodes.push_back( tmp );
579 }
580 Node tmp = NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, r, d_sigma, d_sigma_star );
581 vec_nodes.push_back( tmp );
582 retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes );
583 }
584 } else {
585 Trace("strings-error") << "Unsupported string variable: " << r[0] << " in complement of RegExp." << std::endl;
586 //AlwaysAssert( false );
587 //return Node::null();
588 }
589 }
590 break;
591 case kind::REGEXP_CONCAT:
592 {
593 std::vector< Node > vec_nodes;
594 for(unsigned i=0; i<r.getNumChildren(); ++i) {
595 Node tmp = complement( r[i] );
596 for(unsigned j=0; j<i; ++j) {
597 tmp = NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, r[j], tmp );
598 }
599 if(i != r.getNumChildren() - 1) {
600 tmp = NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, tmp,
601 NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, d_sigma ) );
602 }
603 vec_nodes.push_back( tmp );
604 }
605 retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes );
606 }
607 break;
608 case kind::REGEXP_OR:
609 {
610 std::vector< Node > vec_nodes;
611 for(unsigned i=0; i<r.getNumChildren(); ++i) {
612 Node tmp = complement( r[i] );
613 vec_nodes.push_back( tmp );
614 }
615 retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_INTER, vec_nodes );
616 }
617 break;
618 case kind::REGEXP_INTER:
619 {
620 std::vector< Node > vec_nodes;
621 for(unsigned i=0; i<r.getNumChildren(); ++i) {
622 Node tmp = complement( r[i] );
623 vec_nodes.push_back( tmp );
624 }
625 retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes );
626 }
627 break;
628 case kind::REGEXP_STAR:
629 {
630 retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, d_sigma, d_sigma_star );
631 Node tmp = complement( r[0] );
632 tmp = NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, r, tmp );
633 retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_INTER, retNode, tmp );
634 }
635 break;
636 default:
637 //TODO: special sym: sigma, none, all
638 Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in complement of RegExp." << std::endl;
639 //AlwaysAssert( false );
640 //return Node::null();
641 }
642 d_compl_cache[r] = retNode;
643 }
644 Trace("strings-regexp-compl") << "RegExp-Compl returns : " << mkString( retNode ) << std::endl;
645 return retNode;
646 }
647
648 std::string RegExpOpr::niceChar( Node r ) {
649 if(r.isConst()) {
650 std::string s = r.getConst<CVC4::String>().toString() ;
651 return s == "" ? "{E}" : ( s == " " ? "{ }" : s );
652 } else {
653 return r.toString();
654 }
655 }
656 std::string RegExpOpr::mkString( Node r ) {
657 std::string retStr;
658 if(r.isNull()) {
659 retStr = "EmptySet";
660 } else {
661 int k = r.getKind();
662 switch( k ) {
663 case kind::STRING_TO_REGEXP:
664 {
665 retStr += niceChar( r[0] );
666 }
667 break;
668 case kind::REGEXP_CONCAT:
669 {
670 retStr += "(";
671 for(unsigned i=0; i<r.getNumChildren(); ++i) {
672 if(i != 0) retStr += ".";
673 retStr += mkString( r[i] );
674 }
675 retStr += ")";
676 }
677 break;
678 case kind::REGEXP_OR:
679 {
680 if(r == d_sigma) {
681 retStr += "{A}";
682 } else {
683 retStr += "(";
684 for(unsigned i=0; i<r.getNumChildren(); ++i) {
685 if(i != 0) retStr += "|";
686 retStr += mkString( r[i] );
687 }
688 retStr += ")";
689 }
690 }
691 break;
692 case kind::REGEXP_INTER:
693 {
694 retStr += "(";
695 for(unsigned i=0; i<r.getNumChildren(); ++i) {
696 if(i != 0) retStr += "&";
697 retStr += mkString( r[i] );
698 }
699 retStr += ")";
700 }
701 break;
702 case kind::REGEXP_STAR:
703 {
704 retStr += mkString( r[0] );
705 retStr += "*";
706 }
707 break;
708 case kind::REGEXP_PLUS:
709 {
710 retStr += mkString( r[0] );
711 retStr += "+";
712 }
713 break;
714 case kind::REGEXP_OPT:
715 {
716 retStr += mkString( r[0] );
717 retStr += "?";
718 }
719 break;
720 case kind::REGEXP_RANGE:
721 {
722 retStr += "[";
723 retStr += niceChar( r[0] );
724 retStr += "-";
725 retStr += niceChar( r[1] );
726 retStr += "]";
727 }
728 break;
729 default:
730 //TODO: special sym: sigma, none, all
731 Trace("strings-error") << "Unsupported term: " << r << " in RegExp." << std::endl;
732 //AlwaysAssert( false );
733 //return Node::null();
734 }
735 }
736
737 return retStr;
738 }
739
740 }/* CVC4::theory::strings namespace */
741 }/* CVC4::theory namespace */
742 }/* CVC4 namespace */