1 /********************* */
3 /*! \file regexp_operation.cpp
7 ** Original author: Tianyi Liang
9 ** Major contributors: none
11 ** Minor contributors (to current version): none
13 ** This file is part of the CVC4 project.
15 ** Copyright (c) 2009-2013 New York University and The University of Iowa
17 ** See the file COPYING in the top-level source directory for licensing
19 ** information.\endverbatim
23 ** \brief Symbolic Regular Expresion Operations
25 ** Symbolic Regular Expresion Operations
28 #include "theory/strings/regexp_operation.h"
29 #include "expr/kind.h"
35 RegExpOpr::RegExpOpr() {
36 d_emptyString
= NodeManager::currentNM()->mkConst( ::CVC4::String("") );
37 d_true
= NodeManager::currentNM()->mkConst( true );
38 d_false
= NodeManager::currentNM()->mkConst( false );
39 d_zero
= NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
40 d_one
= NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
41 d_emptySingleton
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, d_emptyString
);
42 std::vector
< Node
> nvec
;
43 d_emptyRegexp
= NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY
, nvec
);
44 // All Charactors = all printable ones 32-126
45 //d_char_start = 'a';//' ';
46 //d_char_end = 'c';//'~';
47 //d_sigma = mkAllExceptOne( '\0' );
48 d_sigma
= NodeManager::currentNM()->mkNode( kind::REGEXP_SIGMA
, nvec
);
49 d_sigma_star
= NodeManager::currentNM()->mkNode( kind::REGEXP_STAR
, d_sigma
);
53 int RegExpOpr::gcd ( int a
, int b
) {
56 c
= a
; a
= b
%a
; b
= c
;
61 bool RegExpOpr::checkConstRegExp( Node r
) {
62 Trace("strings-regexp-cstre") << "RegExp-CheckConstRegExp starts with " << mkString( r
) << std::endl
;
64 if( d_cstre_cache
.find( r
) != d_cstre_cache
.end() ) {
65 ret
= d_cstre_cache
[r
];
67 if(r
.getKind() == kind::STRING_TO_REGEXP
) {
68 Node tmp
= Rewriter::rewrite( r
[0] );
71 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
72 if(!checkConstRegExp(r
[i
])) {
77 d_cstre_cache
[r
] = ret
;
82 // 0-unknown, 1-yes, 2-no
83 int RegExpOpr::delta( Node r
, Node
&exp
) {
84 Trace("regexp-delta") << "RegExp-Delta starts with " << mkString( r
) << std::endl
;
86 if( d_delta_cache
.find( r
) != d_delta_cache
.end() ) {
87 ret
= d_delta_cache
[r
].first
;
88 exp
= d_delta_cache
[r
].second
;
92 case kind::REGEXP_EMPTY
: {
96 case kind::REGEXP_SIGMA
: {
100 case kind::STRING_TO_REGEXP
: {
101 Node tmp
= Rewriter::rewrite(r
[0]);
103 if(tmp
== d_emptyString
) {
110 if(tmp
.getKind() == kind::STRING_CONCAT
) {
111 for(unsigned i
=0; i
<tmp
.getNumChildren(); i
++) {
112 if(tmp
[i
].isConst()) {
119 exp
= r
[0].eqNode(d_emptyString
);
124 case kind::REGEXP_CONCAT
: {
126 std::vector
< Node
> vec_nodes
;
127 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
129 int tmp
= delta( r
[i
], exp2
);
133 } else if(tmp
== 0) {
134 vec_nodes
.push_back( exp2
);
142 exp
= vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode(kind::AND
, vec_nodes
);
147 case kind::REGEXP_UNION
: {
149 std::vector
< Node
> vec_nodes
;
150 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
152 int tmp
= delta( r
[i
], exp2
);
156 } else if(tmp
== 0) {
157 vec_nodes
.push_back( exp2
);
165 exp
= vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode(kind::OR
, vec_nodes
);
170 case kind::REGEXP_INTER
: {
172 std::vector
< Node
> vec_nodes
;
173 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
175 int tmp
= delta( r
[i
], exp2
);
179 } else if(tmp
== 0) {
180 vec_nodes
.push_back( exp2
);
188 exp
= vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode(kind::AND
, vec_nodes
);
193 case kind::REGEXP_STAR
: {
197 case kind::REGEXP_PLUS
: {
198 ret
= delta( r
[0], exp
);
201 case kind::REGEXP_OPT
: {
205 case kind::REGEXP_RANGE
: {
210 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in delta of RegExp." << std::endl
;
212 //return Node::null();
216 exp
= Rewriter::rewrite(exp
);
218 std::pair
< int, Node
> p(ret
, exp
);
219 d_delta_cache
[r
] = p
;
221 Trace("regexp-delta") << "RegExp-Delta returns : " << ret
<< std::endl
;
225 // 0-unknown, 1-yes, 2-no
226 int RegExpOpr::derivativeS( Node r
, CVC4::String c
, Node
&retNode
) {
227 Assert( c
.size() < 2 );
228 Trace("regexp-deriv") << "RegExp-deriv starts with R{ " << mkString( r
) << " }, c=" << c
<< std::endl
;
231 retNode
= d_emptyRegexp
;
233 PairNodeStr dv
= std::make_pair( r
, c
);
234 if( d_deriv_cache
.find( dv
) != d_deriv_cache
.end() ) {
235 retNode
= d_deriv_cache
[dv
].first
;
236 ret
= d_deriv_cache
[dv
].second
;
237 } else if( c
.isEmptyString() ) {
239 ret
= delta( r
, expNode
);
241 retNode
= NodeManager::currentNM()->mkNode(kind::ITE
, expNode
, r
, d_emptyRegexp
);
242 } else if(ret
== 1) {
245 std::pair
< Node
, int > p(retNode
, ret
);
246 d_deriv_cache
[dv
] = p
;
248 switch( r
.getKind() ) {
249 case kind::REGEXP_EMPTY
: {
253 case kind::REGEXP_SIGMA
: {
254 retNode
= d_emptySingleton
;
257 case kind::STRING_TO_REGEXP
: {
258 Node tmp
= Rewriter::rewrite(r
[0]);
260 if(tmp
== d_emptyString
) {
263 if(tmp
.getConst
< CVC4::String
>().getFirstChar() == c
.getFirstChar()) {
264 retNode
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
,
265 tmp
.getConst
< CVC4::String
>().size() == 1 ? d_emptyString
: NodeManager::currentNM()->mkConst( tmp
.getConst
< CVC4::String
>().substr(1) ) );
273 if(tmp
.getKind() == kind::STRING_CONCAT
) {
276 if(t2
.getConst
< CVC4::String
>().getFirstChar() == c
.getFirstChar()) {
277 Node n
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
,
278 tmp
.getConst
< CVC4::String
>().size() == 1 ? d_emptyString
: NodeManager::currentNM()->mkConst( tmp
.getConst
< CVC4::String
>().substr(1) ) );
279 std::vector
< Node
> vec_nodes
;
280 vec_nodes
.push_back(n
);
281 for(unsigned i
=1; i
<tmp
.getNumChildren(); i
++) {
282 vec_nodes
.push_back(tmp
[i
]);
284 retNode
= NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
, vec_nodes
);
291 std::vector
< Node
> vec_nodes
;
292 for(unsigned i
=1; i
<tmp
.getNumChildren(); i
++) {
293 vec_nodes
.push_back(tmp
[i
]);
295 rest
= NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
, vec_nodes
);
299 Node sk
= NodeManager::currentNM()->mkSkolem( "rsp", NodeManager::currentNM()->stringType(), "Split RegExp" );
300 retNode
= NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP
, sk
);
302 retNode
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
, retNode
, rest
));
304 Node exp
= tmp
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
,
305 NodeManager::currentNM()->mkConst(c
), sk
));
306 retNode
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE
, exp
, retNode
, d_emptyRegexp
));
311 case kind::REGEXP_CONCAT
: {
312 std::vector
< Node
> vec_nodes
;
313 std::vector
< Node
> delta_nodes
;
315 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
318 int rt
= derivativeS(r
[i
], c
, dc
);
323 std::vector
< Node
> vec_nodes2
;
324 if(dc
!= d_emptySingleton
) {
325 vec_nodes2
.push_back( dc
);
327 for(unsigned j
=i
+1; j
<r
.getNumChildren(); ++j
) {
328 if(r
[j
] != d_emptySingleton
) {
329 vec_nodes2
.push_back( r
[j
] );
332 Node tmp
= vec_nodes2
.size()==0 ? d_emptySingleton
:
333 vec_nodes2
.size()==1 ? vec_nodes2
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, vec_nodes2
);
334 if(dnode
!= d_true
) {
335 tmp
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE
, dnode
, tmp
, d_emptyRegexp
));
338 if(std::find(vec_nodes
.begin(), vec_nodes
.end(), tmp
) == vec_nodes
.end()) {
339 vec_nodes
.push_back( tmp
);
343 int rt2
= delta( r
[i
], exp3
);
345 dnode
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND
, dnode
, exp3
));
346 } else if( rt2
== 2 ) {
350 retNode
= vec_nodes
.size() == 0 ? d_emptyRegexp
:
351 ( vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_UNION
, vec_nodes
) );
352 if(retNode
== d_emptyRegexp
) {
357 case kind::REGEXP_UNION
: {
358 std::vector
< Node
> vec_nodes
;
359 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
361 int rt
= derivativeS(r
[i
], c
, dc
);
366 if(std::find(vec_nodes
.begin(), vec_nodes
.end(), dc
) == vec_nodes
.end()) {
367 vec_nodes
.push_back( dc
);
370 Trace("regexp-deriv") << "RegExp-deriv OR R[" << i
<< "]{ " << mkString(r
[i
]) << " returns " << mkString(dc
) << std::endl
;
372 retNode
= vec_nodes
.size() == 0 ? d_emptyRegexp
:
373 ( vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_UNION
, vec_nodes
) );
374 if(retNode
== d_emptyRegexp
) {
379 case kind::REGEXP_INTER
: {
381 bool flag_sg
= false;
382 std::vector
< Node
> vec_nodes
;
383 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
385 int rt
= derivativeS(r
[i
], c
, dc
);
392 if(dc
== d_sigma_star
) {
395 if(std::find(vec_nodes
.begin(), vec_nodes
.end(), dc
) == vec_nodes
.end()) {
396 vec_nodes
.push_back( dc
);
401 if(vec_nodes
.size() == 0 && flag_sg
) {
402 retNode
= d_sigma_star
;
404 retNode
= vec_nodes
.size() == 0 ? d_emptyRegexp
:
405 ( vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_INTER
, vec_nodes
) );
406 if(retNode
== d_emptyRegexp
) {
411 retNode
= d_emptyRegexp
;
416 case kind::REGEXP_STAR
: {
418 ret
= derivativeS(r
[0], c
, dc
);
419 retNode
= dc
==d_emptyRegexp
? dc
: (dc
==d_emptySingleton
? r
: NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, dc
, r
));
423 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in derivative of RegExp." << std::endl
;
424 Assert( false, "Unsupported Term" );
427 if(retNode
!= d_emptyRegexp
) {
428 retNode
= Rewriter::rewrite( retNode
);
430 std::pair
< Node
, int > p(retNode
, ret
);
431 d_deriv_cache
[dv
] = p
;
434 Trace("regexp-deriv") << "RegExp-deriv returns : " << mkString( retNode
) << std::endl
;
438 Node
RegExpOpr::derivativeSingle( Node r
, CVC4::String c
) {
439 Assert( c
.size() < 2 );
440 Trace("regexp-deriv") << "RegExp-deriv starts with R{ " << mkString( r
) << " }, c=" << c
<< std::endl
;
441 Node retNode
= d_emptyRegexp
;
442 PairNodeStr dv
= std::make_pair( r
, c
);
443 if( d_dv_cache
.find( dv
) != d_dv_cache
.end() ) {
444 retNode
= d_dv_cache
[dv
];
445 } else if( c
.isEmptyString() ){
447 int tmp
= delta( r
, exp
);
450 retNode
= d_emptyRegexp
;
451 } else if(tmp
== 1) {
454 retNode
= d_emptyRegexp
;
459 case kind::REGEXP_EMPTY
: {
460 retNode
= d_emptyRegexp
;
463 case kind::REGEXP_SIGMA
: {
464 retNode
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, d_emptyString
);
467 case kind::STRING_TO_REGEXP
: {
469 if(r
[0] == d_emptyString
) {
470 retNode
= d_emptyRegexp
;
472 if(r
[0].getConst
< CVC4::String
>().getFirstChar() == c
.getFirstChar()) {
473 retNode
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
,
474 r
[0].getConst
< CVC4::String
>().size() == 1 ? d_emptyString
: NodeManager::currentNM()->mkConst( r
[0].getConst
< CVC4::String
>().substr(1) ) );
476 retNode
= d_emptyRegexp
;
481 retNode
= d_emptyRegexp
;
485 case kind::REGEXP_CONCAT
: {
486 Node rees
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, d_emptyString
);
487 std::vector
< Node
> vec_nodes
;
488 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
489 Node dc
= derivativeSingle(r
[i
], c
);
490 if(dc
!= d_emptyRegexp
) {
491 std::vector
< Node
> vec_nodes2
;
493 vec_nodes2
.push_back( dc
);
495 for(unsigned j
=i
+1; j
<r
.getNumChildren(); ++j
) {
497 vec_nodes2
.push_back( r
[j
] );
500 Node tmp
= vec_nodes2
.size()==0 ? rees
:
501 vec_nodes2
.size()==1 ? vec_nodes2
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, vec_nodes2
);
502 if(std::find(vec_nodes
.begin(), vec_nodes
.end(), tmp
) == vec_nodes
.end()) {
503 vec_nodes
.push_back( tmp
);
507 if( delta( r
[i
], exp
) != 1 ) {
511 retNode
= vec_nodes
.size() == 0 ? d_emptyRegexp
:
512 ( vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_UNION
, vec_nodes
) );
515 case kind::REGEXP_UNION
: {
516 std::vector
< Node
> vec_nodes
;
517 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
518 Node dc
= derivativeSingle(r
[i
], c
);
519 if(dc
!= d_emptyRegexp
) {
520 if(std::find(vec_nodes
.begin(), vec_nodes
.end(), dc
) == vec_nodes
.end()) {
521 vec_nodes
.push_back( dc
);
524 Trace("regexp-deriv") << "RegExp-deriv OR R[" << i
<< "]{ " << mkString(r
[i
]) << " returns " << mkString(dc
) << std::endl
;
526 retNode
= vec_nodes
.size() == 0 ? d_emptyRegexp
:
527 ( vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_UNION
, vec_nodes
) );
530 case kind::REGEXP_INTER
: {
532 bool flag_sg
= false;
533 std::vector
< Node
> vec_nodes
;
534 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
535 Node dc
= derivativeSingle(r
[i
], c
);
536 if(dc
!= d_emptyRegexp
) {
537 if(dc
== d_sigma_star
) {
540 if(std::find(vec_nodes
.begin(), vec_nodes
.end(), dc
) == vec_nodes
.end()) {
541 vec_nodes
.push_back( dc
);
550 if(vec_nodes
.size() == 0 && flag_sg
) {
551 retNode
= d_sigma_star
;
553 retNode
= vec_nodes
.size() == 0 ? d_emptyRegexp
:
554 ( vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_INTER
, vec_nodes
) );
557 retNode
= d_emptyRegexp
;
561 case kind::REGEXP_STAR
: {
562 Node dc
= derivativeSingle(r
[0], c
);
563 if(dc
!= d_emptyRegexp
) {
564 retNode
= dc
==NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, d_emptyString
) ? r
: NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, dc
, r
);
566 retNode
= d_emptyRegexp
;
571 //TODO: special sym: sigma, none, all
572 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in derivative of RegExp." << std::endl
;
573 Assert( false, "Unsupported Term" );
574 //return Node::null();
577 if(retNode
!= d_emptyRegexp
) {
578 retNode
= Rewriter::rewrite( retNode
);
580 d_dv_cache
[dv
] = retNode
;
582 Trace("regexp-deriv") << "RegExp-deriv returns : " << mkString( retNode
) << std::endl
;
587 bool RegExpOpr::guessLength( Node r
, int &co
) {
590 case kind::STRING_TO_REGEXP
:
593 co
+= r
[0].getConst
< CVC4::String
>().size();
600 case kind::REGEXP_CONCAT
:
602 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
603 if(!guessLength( r
[i
], co
)) {
610 case kind::REGEXP_UNION
:
613 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
615 if(!guessLength( r
[i
], cop
)) {
621 g_co
= gcd(g_co
, cop
);
627 case kind::REGEXP_INTER
:
630 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
632 if(!guessLength( r
[i
], cop
)) {
638 g_co
= gcd(g_co
, cop
);
644 case kind::REGEXP_STAR
:
651 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in membership of RegExp." << std::endl
;
656 void RegExpOpr::firstChars( Node r
, std::set
<unsigned> &pcset
, SetNodes
&pvset
) {
657 std::map
< Node
, std::pair
< std::set
<unsigned>, SetNodes
> >::const_iterator itr
= d_fset_cache
.find(r
);
658 if(itr
!= d_fset_cache
.end()) {
659 pcset
.insert((itr
->second
).first
.begin(), (itr
->second
).first
.end());
660 pvset
.insert((itr
->second
).second
.begin(), (itr
->second
).second
.end());
662 std::set
<unsigned> cset
;
666 case kind::REGEXP_EMPTY
: {
669 case kind::REGEXP_SIGMA
: {
670 for(unsigned i
=0; i
<d_card
; i
++) {
675 case kind::STRING_TO_REGEXP
: {
676 Node st
= Rewriter::rewrite(r
[0]);
678 CVC4::String s
= st
.getConst
< CVC4::String
>();
682 } else if(st
.getKind() == kind::VARIABLE
) {
685 if(st
[0].isConst()) {
686 CVC4::String s
= st
[0].getConst
< CVC4::String
>();
689 vset
.insert( st
[0] );
694 case kind::REGEXP_CONCAT
: {
695 for(unsigned i
=0; i
<r
.getNumChildren(); i
++) {
696 firstChars(r
[i
], cset
, vset
);
699 int r
= delta( n
, exp
);
706 case kind::REGEXP_UNION
: {
707 for(unsigned i
=0; i
<r
.getNumChildren(); i
++) {
708 firstChars(r
[i
], cset
, vset
);
712 case kind::REGEXP_INTER
: {
713 //TODO: Overapproximation for now
714 for(unsigned i
=0; i
<r
.getNumChildren(); i
++) {
715 firstChars(r
[i
], cset
, vset
);
719 case kind::REGEXP_STAR
: {
720 firstChars(r
[0], cset
, vset
);
724 Trace("strings-regexp") << "Unsupported term: " << r
<< " in getCharSet." << std::endl
;
725 Assert( false, "Unsupported Term" );
728 pcset
.insert(cset
.begin(), cset
.end());
729 pvset
.insert(vset
.begin(), vset
.end());
730 std::pair
< std::set
<unsigned>, SetNodes
> p(cset
, vset
);
733 Trace("regexp-fset") << "FSET( " << mkString(r
) << " ) = { ";
734 for(std::set
<unsigned>::const_iterator itr
= cset
.begin();
735 itr
!= cset
.end(); itr
++) {
736 Trace("regexp-fset") << CVC4::String::convertUnsignedIntToChar(*itr
) << ",";
738 Trace("regexp-fset") << " }" << std::endl
;
742 bool RegExpOpr::follow( Node r
, CVC4::String c
, std::vector
< char > &vec_chars
) {
745 case kind::STRING_TO_REGEXP
:
748 if(r
[0] != d_emptyString
) {
749 char t1
= r
[0].getConst
< CVC4::String
>().getFirstChar();
750 if(c
.isEmptyString()) {
751 vec_chars
.push_back( t1
);
754 char t2
= c
.getFirstChar();
759 vec_chars
.push_back( c
.substr(1,1).getFirstChar() );
761 vec_chars
.push_back( '\0' );
774 case kind::REGEXP_CONCAT
:
776 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
777 if( follow(r
[i
], c
, vec_chars
) ) {
778 if(vec_chars
[vec_chars
.size() - 1] == '\0') {
779 vec_chars
.pop_back();
780 c
= d_emptyString
.getConst
< CVC4::String
>();
786 vec_chars
.push_back( '\0' );
790 case kind::REGEXP_UNION
:
793 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
794 if( follow(r
[i
], c
, vec_chars
) ) {
801 case kind::REGEXP_INTER
:
803 std::vector
< char > vt2
;
804 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
805 std::vector
< char > v_tmp
;
806 if( !follow(r
[i
], c
, v_tmp
) ) {
809 std::vector
< char > vt3(vt2
);
811 std::set_intersection( vt3
.begin(), vt3
.end(), v_tmp
.begin(), v_tmp
.end(), vt2
.begin() );
812 if(vt2
.size() == 0) {
816 vec_chars
.insert( vec_chars
.end(), vt2
.begin(), vt2
.end() );
820 case kind::REGEXP_STAR
:
822 if(follow(r
[0], c
, vec_chars
)) {
823 if(vec_chars
[vec_chars
.size() - 1] == '\0') {
824 if(c
.isEmptyString()) {
827 vec_chars
.pop_back();
828 c
= d_emptyString
.getConst
< CVC4::String
>();
829 return follow(r
[0], c
, vec_chars
);
835 vec_chars
.push_back( '\0' );
841 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in delta of RegExp." << std::endl
;
842 //AlwaysAssert( false );
843 //return Node::null();
849 Node
RegExpOpr::mkAllExceptOne( char exp_c
) {
850 std::vector
< Node
> vec_nodes
;
851 for(char c
=d_char_start
; c
<=d_char_end
; ++c
) {
853 Node n
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, NodeManager::currentNM()->mkConst( ::CVC4::String( c
) ) );
854 vec_nodes
.push_back( n
);
857 return NodeManager::currentNM()->mkNode( kind::REGEXP_UNION
, vec_nodes
);
861 void RegExpOpr::simplify(Node t
, std::vector
< Node
> &new_nodes
, bool polarity
) {
862 Trace("strings-regexp-simpl") << "RegExp-Simpl starts with " << t
<< ", polarity=" << polarity
<< std::endl
;
863 Assert(t
.getKind() == kind::STRING_IN_REGEXP
);
864 Node str
= Rewriter::rewrite(t
[0]);
865 Node re
= Rewriter::rewrite(t
[1]);
867 simplifyPRegExp( str
, re
, new_nodes
);
869 simplifyNRegExp( str
, re
, new_nodes
);
871 Trace("strings-regexp-simpl") << "RegExp-Simpl returns (" << new_nodes
.size() << "):\n";
872 for(unsigned i
=0; i
<new_nodes
.size(); i
++) {
873 Trace("strings-regexp-simpl") << "\t" << new_nodes
[i
] << std::endl
;
876 void RegExpOpr::simplifyNRegExp( Node s
, Node r
, std::vector
< Node
> &new_nodes
) {
877 std::pair
< Node
, Node
> p(s
, r
);
878 std::map
< std::pair
< Node
, Node
>, Node
>::const_iterator itr
= d_simpl_neg_cache
.find(p
);
879 if(itr
!= d_simpl_neg_cache
.end()) {
880 new_nodes
.push_back( itr
->second
);
885 case kind::REGEXP_EMPTY
: {
889 case kind::REGEXP_SIGMA
: {
890 conc
= d_one
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
)).negate();
893 case kind::STRING_TO_REGEXP
: {
894 conc
= s
.eqNode(r
[0]).negate();
897 case kind::REGEXP_CONCAT
: {
898 //TODO: rewrite empty
899 Node b1
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
900 Node b1v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, b1
);
901 Node g1
= NodeManager::currentNM()->mkNode( kind::AND
, NodeManager::currentNM()->mkNode(kind::GEQ
, b1
, d_zero
),
902 NodeManager::currentNM()->mkNode( kind::GEQ
, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
), b1
) );
903 Node s1
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
904 Node s2
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
905 Node b2v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, s1
, s2
);
906 Node s12
= s
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
, s1
, s2
));
907 Node s1len
= b1
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s1
));
908 Node s1r1
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s1
, r
[0]).negate();
909 if(r
[0].getKind() == kind::STRING_TO_REGEXP
) {
910 s1r1
= s1
.eqNode(r
[0][0]).negate();
911 } else if(r
[0].getKind() == kind::REGEXP_EMPTY
) {
915 if(r
.getNumChildren() > 2) {
916 std::vector
< Node
> nvec
;
917 for(unsigned i
=1; i
<r
.getNumChildren(); i
++) {
918 nvec
.push_back( r
[i
] );
920 r2
= NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
, nvec
);
922 r2
= Rewriter::rewrite(r2
);
923 Node s2r2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s2
, r2
).negate();
924 if(r2
.getKind() == kind::STRING_TO_REGEXP
) {
925 s2r2
= s2
.eqNode(r2
[0]).negate();
926 } else if(r2
.getKind() == kind::REGEXP_EMPTY
) {
930 conc
= NodeManager::currentNM()->mkNode(kind::OR
, s1r1
, s2r2
);
931 conc
= NodeManager::currentNM()->mkNode(kind::AND
, s12
, s1len
, conc
);
932 conc
= NodeManager::currentNM()->mkNode(kind::EXISTS
, b2v
, conc
);
933 conc
= NodeManager::currentNM()->mkNode(kind::IMPLIES
, g1
, conc
);
934 conc
= NodeManager::currentNM()->mkNode(kind::FORALL
, b1v
, conc
);
937 case kind::REGEXP_UNION
: {
938 std::vector
< Node
> c_and
;
939 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
940 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
941 c_and
.push_back( r
[i
][0].eqNode(s
).negate() );
942 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
945 c_and
.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[i
]).negate());
948 conc
= c_and
.size() == 0 ? d_true
:
949 c_and
.size() == 1 ? c_and
[0] : NodeManager::currentNM()->mkNode(kind::AND
, c_and
);
952 case kind::REGEXP_INTER
: {
953 bool emptyflag
= false;
954 std::vector
< Node
> c_or
;
955 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
956 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
957 c_or
.push_back( r
[i
][0].eqNode(s
).negate() );
958 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
962 c_or
.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[i
]).negate());
968 conc
= c_or
.size() == 1 ? c_or
[0] : NodeManager::currentNM()->mkNode(kind::OR
, c_or
);
972 case kind::REGEXP_STAR
: {
973 if(s
== d_emptyString
) {
975 } else if(r
[0].getKind() == kind::REGEXP_EMPTY
) {
976 conc
= s
.eqNode(d_emptyString
).negate();
977 } else if(r
[0].getKind() == kind::REGEXP_SIGMA
) {
980 Node lens
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
);
981 Node sne
= s
.eqNode(d_emptyString
).negate();
982 Node b1
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
983 Node b1v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, b1
);
984 Node g1
= NodeManager::currentNM()->mkNode( kind::AND
, NodeManager::currentNM()->mkNode(kind::GEQ
, b1
, d_one
),
985 NodeManager::currentNM()->mkNode( kind::GEQ
, lens
, b1
) );
987 Node s1
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL
, s
, d_zero
, b1
);
988 Node s2
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL
, s
, b1
, NodeManager::currentNM()->mkNode(kind::MINUS
, lens
, b1
));
989 Node s1r1
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s1
, r
[0]).negate();
990 Node s2r2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s2
, r
).negate();
992 conc
= NodeManager::currentNM()->mkNode(kind::OR
, s1r1
, s2r2
);
993 conc
= NodeManager::currentNM()->mkNode(kind::IMPLIES
, g1
, conc
);
994 conc
= NodeManager::currentNM()->mkNode(kind::FORALL
, b1v
, conc
);
995 conc
= NodeManager::currentNM()->mkNode(kind::AND
, sne
, conc
);
1000 Trace("strings-regexp") << "Unsupported term: " << r
<< " in simplifyNRegExp." << std::endl
;
1001 Assert( false, "Unsupported Term" );
1004 conc
= Rewriter::rewrite( conc
);
1005 new_nodes
.push_back( conc
);
1006 d_simpl_neg_cache
[p
] = conc
;
1009 void RegExpOpr::simplifyPRegExp( Node s
, Node r
, std::vector
< Node
> &new_nodes
) {
1010 std::pair
< Node
, Node
> p(s
, r
);
1011 std::map
< std::pair
< Node
, Node
>, Node
>::const_iterator itr
= d_simpl_cache
.find(p
);
1012 if(itr
!= d_simpl_cache
.end()) {
1013 new_nodes
.push_back( itr
->second
);
1015 int k
= r
.getKind();
1018 case kind::REGEXP_EMPTY
: {
1022 case kind::REGEXP_SIGMA
: {
1023 conc
= d_one
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
));
1026 case kind::STRING_TO_REGEXP
: {
1027 conc
= s
.eqNode(r
[0]);
1030 case kind::REGEXP_CONCAT
: {
1031 std::vector
< Node
> nvec
;
1032 std::vector
< Node
> cc
;
1033 bool emptyflag
= false;
1034 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
1035 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
1036 cc
.push_back( r
[i
][0] );
1037 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
1041 Node sk
= NodeManager::currentNM()->mkSkolem( "rc", s
.getType(), "created for regular expression concat" );
1042 Node lem
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, sk
, r
[i
]);
1043 nvec
.push_back(lem
);
1050 Node lem
= s
.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
, cc
) );
1051 nvec
.push_back(lem
);
1052 conc
= nvec
.size() == 1 ? nvec
[0] : NodeManager::currentNM()->mkNode(kind::AND
, nvec
);
1056 case kind::REGEXP_UNION
: {
1057 std::vector
< Node
> c_or
;
1058 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
1059 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
1060 c_or
.push_back( r
[i
][0].eqNode(s
) );
1061 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
1064 c_or
.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[i
]));
1067 conc
= c_or
.size() == 0 ? d_false
:
1068 c_or
.size() == 1 ? c_or
[0] : NodeManager::currentNM()->mkNode(kind::OR
, c_or
);
1071 case kind::REGEXP_INTER
: {
1072 std::vector
< Node
> c_and
;
1073 bool emptyflag
= false;
1074 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
1075 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
1076 c_and
.push_back( r
[i
][0].eqNode(s
) );
1077 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
1081 c_and
.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[i
]));
1087 conc
= c_and
.size() == 1 ? c_and
[0] : NodeManager::currentNM()->mkNode(kind::AND
, c_and
);
1091 case kind::REGEXP_STAR
: {
1092 if(s
== d_emptyString
) {
1094 } else if(r
[0].getKind() == kind::REGEXP_EMPTY
) {
1095 conc
= s
.eqNode(d_emptyString
);
1096 } else if(r
[0].getKind() == kind::REGEXP_SIGMA
) {
1099 Node se
= s
.eqNode(d_emptyString
);
1100 Node sinr
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[0]);
1101 Node sk1
= NodeManager::currentNM()->mkSkolem( "rs", s
.getType(), "created for regular expression star" );
1102 Node sk2
= NodeManager::currentNM()->mkSkolem( "rs", s
.getType(), "created for regular expression star" );
1103 Node s1nz
= sk1
.eqNode(d_emptyString
).negate();
1104 Node s2nz
= sk2
.eqNode(d_emptyString
).negate();
1105 Node s1inr
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, sk1
, r
[0]);
1106 Node s2inrs
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, sk2
, r
);
1107 Node s12
= s
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
, sk1
, sk2
));
1109 conc
= NodeManager::currentNM()->mkNode(kind::AND
, s12
, s1nz
, s2nz
, s1inr
, s2inrs
);
1110 conc
= NodeManager::currentNM()->mkNode(kind::OR
, se
, sinr
, conc
);
1115 Trace("strings-regexp") << "Unsupported term: " << r
<< " in simplifyPRegExp." << std::endl
;
1116 Assert( false, "Unsupported Term" );
1119 conc
= Rewriter::rewrite( conc
);
1120 new_nodes
.push_back( conc
);
1121 d_simpl_cache
[p
] = conc
;
1125 void RegExpOpr::getCharSet( Node r
, std::set
<unsigned> &pcset
, SetNodes
&pvset
) {
1126 std::map
< Node
, std::pair
< std::set
<unsigned>, SetNodes
> >::const_iterator itr
= d_cset_cache
.find(r
);
1127 if(itr
!= d_cset_cache
.end()) {
1128 pcset
.insert((itr
->second
).first
.begin(), (itr
->second
).first
.end());
1129 pvset
.insert((itr
->second
).second
.begin(), (itr
->second
).second
.end());
1131 std::set
<unsigned> cset
;
1133 int k
= r
.getKind();
1135 case kind::REGEXP_EMPTY
: {
1138 case kind::REGEXP_SIGMA
: {
1139 for(unsigned i
=0; i
<d_card
; i
++) {
1144 case kind::STRING_TO_REGEXP
: {
1145 Node st
= Rewriter::rewrite(r
[0]);
1147 CVC4::String s
= st
.getConst
< CVC4::String
>();
1148 s
.getCharSet( cset
);
1149 } else if(st
.getKind() == kind::VARIABLE
) {
1152 for(unsigned i
=0; i
<st
.getNumChildren(); i
++) {
1153 if(st
[i
].isConst()) {
1154 CVC4::String s
= st
[i
].getConst
< CVC4::String
>();
1155 s
.getCharSet( cset
);
1157 vset
.insert( st
[i
] );
1163 case kind::REGEXP_CONCAT
: {
1164 for(unsigned i
=0; i
<r
.getNumChildren(); i
++) {
1165 getCharSet(r
[i
], cset
, vset
);
1169 case kind::REGEXP_UNION
: {
1170 for(unsigned i
=0; i
<r
.getNumChildren(); i
++) {
1171 getCharSet(r
[i
], cset
, vset
);
1175 case kind::REGEXP_INTER
: {
1176 //TODO: Overapproximation for now
1177 for(unsigned i
=0; i
<r
.getNumChildren(); i
++) {
1178 getCharSet(r
[i
], cset
, vset
);
1182 case kind::REGEXP_STAR
: {
1183 getCharSet(r
[0], cset
, vset
);
1187 Trace("strings-regexp") << "Unsupported term: " << r
<< " in getCharSet." << std::endl
;
1188 Assert( false, "Unsupported Term" );
1191 pcset
.insert(cset
.begin(), cset
.end());
1192 pvset
.insert(vset
.begin(), vset
.end());
1193 std::pair
< std::set
<unsigned>, SetNodes
> p(cset
, vset
);
1194 d_cset_cache
[r
] = p
;
1196 Trace("regexp-cset") << "CSET( " << mkString(r
) << " ) = { ";
1197 for(std::set
<unsigned>::const_iterator itr
= cset
.begin();
1198 itr
!= cset
.end(); itr
++) {
1199 Trace("regexp-cset") << CVC4::String::convertUnsignedIntToChar(*itr
) << ",";
1201 Trace("regexp-cset") << " }" << std::endl
;
1206 Node
RegExpOpr::intersectInternal( Node r1
, Node r2
, std::map
< unsigned, std::set
< PairNodes
> > cache
, bool &spflag
) {
1209 return Node::null();
1211 std::pair
< Node
, Node
> p(r1
, r2
);
1212 std::map
< std::pair
< Node
, Node
>, Node
>::const_iterator itr
= d_inter_cache
.find(p
);
1214 if(itr
!= d_inter_cache
.end()) {
1215 rNode
= itr
->second
;
1219 } else if(r1
== d_emptyRegexp
|| r2
== d_emptyRegexp
) {
1220 rNode
= d_emptyRegexp
;
1221 } else if(r1
== d_emptySingleton
|| r2
== d_emptySingleton
) {
1223 int r
= delta((r1
== d_emptySingleton
? r2
: r1
), exp
);
1228 rNode
= d_emptySingleton
;
1230 rNode
= d_emptyRegexp
;
1233 std::set
< unsigned > cset
, cset2
;
1234 std::set
< Node
> vset
, vset2
;
1235 getCharSet(r1
, cset
, vset
);
1236 getCharSet(r2
, cset2
, vset2
);
1237 if(vset
.empty() && vset2
.empty()) {
1239 firstChars(r1
, cset
, vset
);
1240 std::vector
< Node
> vec_nodes
;
1241 for(std::set
<unsigned>::const_iterator itr
= cset
.begin();
1242 itr
!= cset
.end(); itr
++) {
1243 CVC4::String
c( CVC4::String::convertUnsignedIntToChar(*itr
) );
1244 std::pair
< Node
, Node
> p(r1
, r2
);
1245 if(cache
[ *itr
].find(p
) == cache
[ *itr
].end()) {
1246 Node r1l
= derivativeSingle(r1
, c
);
1247 Node r2l
= derivativeSingle(r2
, c
);
1248 std::map
< unsigned, std::set
< PairNodes
> > cache2(cache
);
1249 PairNodes
p(r1l
, r2l
);
1250 cache2
[ *itr
].insert( p
);
1251 Node rt
= intersectInternal(r1l
, r2l
, cache2
, spflag
);
1254 return Node::null();
1256 rt
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
,
1257 NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP
, NodeManager::currentNM()->mkConst(c
)), rt
) );
1258 vec_nodes
.push_back(rt
);
1261 rNode
= vec_nodes
.size()==0 ? d_emptyRegexp
: vec_nodes
.size()==1 ? vec_nodes
[0] :
1262 NodeManager::currentNM()->mkNode(kind::REGEXP_UNION
, vec_nodes
);
1263 rNode
= Rewriter::rewrite( rNode
);
1265 //TODO: non-empty var set
1269 d_inter_cache
[p
] = rNode
;
1271 Trace("regexp-intersect") << "INTERSECT( " << mkString(r1
) << ", " << mkString(r2
) << " ) = " << mkString(rNode
) << std::endl
;
1274 Node
RegExpOpr::intersect(Node r1
, Node r2
, bool &spflag
) {
1275 std::map
< unsigned, std::set
< PairNodes
> > cache
;
1276 return intersectInternal(r1
, r2
, cache
, spflag
);
1279 Node
RegExpOpr::complement(Node r
, int &ret
) {
1282 if(d_compl_cache
.find(r
) != d_compl_cache
.end()) {
1283 rNode
= d_compl_cache
[r
].first
;
1284 ret
= d_compl_cache
[r
].second
;
1286 if(r
== d_emptyRegexp
) {
1287 rNode
= d_sigma_star
;
1288 } else if(r
== d_emptySingleton
) {
1289 rNode
= NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
, d_sigma
, d_sigma_star
);
1290 } else if(!checkConstRegExp(r
)) {
1291 //TODO: var to be extended
1294 std::set
<unsigned> cset
;
1296 firstChars(r
, cset
, vset
);
1297 std::vector
< Node
> vec_nodes
;
1298 for(unsigned i
=0; i
<d_card
; i
++) {
1299 CVC4::String c
= CVC4::String::convertUnsignedIntToChar(i
);
1300 Node n
= NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP
, NodeManager::currentNM()->mkConst(c
));
1302 if(cset
.find(i
) == cset
.end()) {
1306 derivativeS(r
, c
, r2
);
1310 r2
= complement(r2
, rt
);
1313 n
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
, n
, r2
));
1314 vec_nodes
.push_back(n
);
1316 rNode
= vec_nodes
.size()==0? d_emptyRegexp
: vec_nodes
.size()==1? vec_nodes
[0] :
1317 NodeManager::currentNM()->mkNode(kind::REGEXP_UNION
, vec_nodes
);
1319 rNode
= Rewriter::rewrite(rNode
);
1320 std::pair
< Node
, int > p(rNode
, ret
);
1321 d_compl_cache
[r
] = p
;
1323 Trace("regexp-compl") << "COMPL( " << mkString(r
) << " ) = " << mkString(rNode
) << ", ret=" << ret
<< std::endl
;
1327 std::string
RegExpOpr::niceChar( Node r
) {
1329 std::string s
= r
.getConst
<CVC4::String
>().toString() ;
1330 return s
== "" ? "{E}" : ( s
== " " ? "{ }" : s
.size()>1? "("+s
+")" : s
);
1332 std::string ss
= "$" + r
.toString();
1336 std::string
RegExpOpr::mkString( Node r
) {
1341 int k
= r
.getKind();
1343 case kind::REGEXP_EMPTY
: {
1347 case kind::REGEXP_SIGMA
: {
1351 case kind::STRING_TO_REGEXP
: {
1352 retStr
+= niceChar( r
[0] );
1355 case kind::REGEXP_CONCAT
: {
1357 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
1358 //if(i != 0) retStr += ".";
1359 retStr
+= mkString( r
[i
] );
1364 case kind::REGEXP_UNION
: {
1369 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
1370 if(i
!= 0) retStr
+= "|";
1371 retStr
+= mkString( r
[i
] );
1377 case kind::REGEXP_INTER
: {
1379 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
1380 if(i
!= 0) retStr
+= "&";
1381 retStr
+= mkString( r
[i
] );
1386 case kind::REGEXP_STAR
: {
1387 retStr
+= mkString( r
[0] );
1391 case kind::REGEXP_PLUS
: {
1392 retStr
+= mkString( r
[0] );
1396 case kind::REGEXP_OPT
: {
1397 retStr
+= mkString( r
[0] );
1401 case kind::REGEXP_RANGE
: {
1403 retStr
+= niceChar( r
[0] );
1405 retStr
+= niceChar( r
[1] );
1410 Trace("strings-error") << "Unsupported term: " << r
<< " in RegExp." << std::endl
;
1412 //return Node::null();
1419 }/* CVC4::theory::strings namespace */
1420 }/* CVC4::theory namespace */
1421 }/* CVC4 namespace */