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
);
700 int r
= delta( n
, exp
);
708 case kind::REGEXP_UNION
: {
709 for(unsigned i
=0; i
<r
.getNumChildren(); i
++) {
710 firstChars(r
[i
], cset
, vset
);
714 case kind::REGEXP_INTER
: {
715 //TODO: Overapproximation for now
716 for(unsigned i
=0; i
<r
.getNumChildren(); i
++) {
717 firstChars(r
[i
], cset
, vset
);
721 case kind::REGEXP_STAR
: {
722 firstChars(r
[0], cset
, vset
);
726 Trace("strings-regexp") << "Unsupported term: " << r
<< " in getCharSet." << std::endl
;
727 Assert( false, "Unsupported Term" );
730 pcset
.insert(cset
.begin(), cset
.end());
731 pvset
.insert(vset
.begin(), vset
.end());
732 std::pair
< std::set
<unsigned>, SetNodes
> p(cset
, vset
);
735 Trace("regexp-fset") << "FSET( " << mkString(r
) << " ) = { ";
736 for(std::set
<unsigned>::const_iterator itr
= cset
.begin();
737 itr
!= cset
.end(); itr
++) {
738 Trace("regexp-fset") << CVC4::String::convertUnsignedIntToChar(*itr
) << ",";
740 Trace("regexp-fset") << " }" << std::endl
;
744 bool RegExpOpr::follow( Node r
, CVC4::String c
, std::vector
< char > &vec_chars
) {
747 case kind::STRING_TO_REGEXP
:
750 if(r
[0] != d_emptyString
) {
751 char t1
= r
[0].getConst
< CVC4::String
>().getFirstChar();
752 if(c
.isEmptyString()) {
753 vec_chars
.push_back( t1
);
756 char t2
= c
.getFirstChar();
761 vec_chars
.push_back( c
.substr(1,1).getFirstChar() );
763 vec_chars
.push_back( '\0' );
776 case kind::REGEXP_CONCAT
:
778 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
779 if( follow(r
[i
], c
, vec_chars
) ) {
780 if(vec_chars
[vec_chars
.size() - 1] == '\0') {
781 vec_chars
.pop_back();
782 c
= d_emptyString
.getConst
< CVC4::String
>();
788 vec_chars
.push_back( '\0' );
792 case kind::REGEXP_UNION
:
795 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
796 if( follow(r
[i
], c
, vec_chars
) ) {
803 case kind::REGEXP_INTER
:
805 std::vector
< char > vt2
;
806 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
807 std::vector
< char > v_tmp
;
808 if( !follow(r
[i
], c
, v_tmp
) ) {
811 std::vector
< char > vt3(vt2
);
813 std::set_intersection( vt3
.begin(), vt3
.end(), v_tmp
.begin(), v_tmp
.end(), vt2
.begin() );
814 if(vt2
.size() == 0) {
818 vec_chars
.insert( vec_chars
.end(), vt2
.begin(), vt2
.end() );
822 case kind::REGEXP_STAR
:
824 if(follow(r
[0], c
, vec_chars
)) {
825 if(vec_chars
[vec_chars
.size() - 1] == '\0') {
826 if(c
.isEmptyString()) {
829 vec_chars
.pop_back();
830 c
= d_emptyString
.getConst
< CVC4::String
>();
831 return follow(r
[0], c
, vec_chars
);
837 vec_chars
.push_back( '\0' );
843 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in delta of RegExp." << std::endl
;
844 //AlwaysAssert( false );
845 //return Node::null();
851 Node
RegExpOpr::mkAllExceptOne( char exp_c
) {
852 std::vector
< Node
> vec_nodes
;
853 for(char c
=d_char_start
; c
<=d_char_end
; ++c
) {
855 Node n
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, NodeManager::currentNM()->mkConst( ::CVC4::String( c
) ) );
856 vec_nodes
.push_back( n
);
859 return NodeManager::currentNM()->mkNode( kind::REGEXP_UNION
, vec_nodes
);
863 void RegExpOpr::simplify(Node t
, std::vector
< Node
> &new_nodes
, bool polarity
) {
864 Trace("strings-regexp-simpl") << "RegExp-Simpl starts with " << t
<< ", polarity=" << polarity
<< std::endl
;
865 Assert(t
.getKind() == kind::STRING_IN_REGEXP
);
866 Node str
= Rewriter::rewrite(t
[0]);
867 Node re
= Rewriter::rewrite(t
[1]);
869 simplifyPRegExp( str
, re
, new_nodes
);
871 simplifyNRegExp( str
, re
, new_nodes
);
873 Trace("strings-regexp-simpl") << "RegExp-Simpl returns (" << new_nodes
.size() << "):\n";
874 for(unsigned i
=0; i
<new_nodes
.size(); i
++) {
875 Trace("strings-regexp-simpl") << "\t" << new_nodes
[i
] << std::endl
;
878 void RegExpOpr::simplifyNRegExp( Node s
, Node r
, std::vector
< Node
> &new_nodes
) {
879 std::pair
< Node
, Node
> p(s
, r
);
880 std::map
< std::pair
< Node
, Node
>, Node
>::const_iterator itr
= d_simpl_neg_cache
.find(p
);
881 if(itr
!= d_simpl_neg_cache
.end()) {
882 new_nodes
.push_back( itr
->second
);
887 case kind::REGEXP_EMPTY
: {
891 case kind::REGEXP_SIGMA
: {
892 conc
= d_one
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
)).negate();
895 case kind::STRING_TO_REGEXP
: {
896 conc
= s
.eqNode(r
[0]).negate();
899 case kind::REGEXP_CONCAT
: {
900 //TODO: rewrite empty
901 Node b1
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
902 Node b1v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, b1
);
903 Node g1
= NodeManager::currentNM()->mkNode( kind::AND
, NodeManager::currentNM()->mkNode(kind::GEQ
, b1
, d_zero
),
904 NodeManager::currentNM()->mkNode( kind::GEQ
, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
), b1
) );
905 Node s1
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
906 Node s2
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
907 Node b2v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, s1
, s2
);
908 Node s12
= s
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
, s1
, s2
));
909 Node s1len
= b1
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s1
));
910 Node s1r1
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s1
, r
[0]).negate();
911 if(r
[0].getKind() == kind::STRING_TO_REGEXP
) {
912 s1r1
= s1
.eqNode(r
[0][0]).negate();
913 } else if(r
[0].getKind() == kind::REGEXP_EMPTY
) {
917 if(r
.getNumChildren() > 2) {
918 std::vector
< Node
> nvec
;
919 for(unsigned i
=1; i
<r
.getNumChildren(); i
++) {
920 nvec
.push_back( r
[i
] );
922 r2
= NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
, nvec
);
924 r2
= Rewriter::rewrite(r2
);
925 Node s2r2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s2
, r2
).negate();
926 if(r2
.getKind() == kind::STRING_TO_REGEXP
) {
927 s2r2
= s2
.eqNode(r2
[0]).negate();
928 } else if(r2
.getKind() == kind::REGEXP_EMPTY
) {
932 conc
= NodeManager::currentNM()->mkNode(kind::OR
, s1r1
, s2r2
);
933 conc
= NodeManager::currentNM()->mkNode(kind::AND
, s12
, s1len
, conc
);
934 conc
= NodeManager::currentNM()->mkNode(kind::EXISTS
, b2v
, conc
);
935 conc
= NodeManager::currentNM()->mkNode(kind::IMPLIES
, g1
, conc
);
936 conc
= NodeManager::currentNM()->mkNode(kind::FORALL
, b1v
, conc
);
939 case kind::REGEXP_UNION
: {
940 std::vector
< Node
> c_and
;
941 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
942 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
943 c_and
.push_back( r
[i
][0].eqNode(s
).negate() );
944 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
947 c_and
.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[i
]).negate());
950 conc
= c_and
.size() == 0 ? d_true
:
951 c_and
.size() == 1 ? c_and
[0] : NodeManager::currentNM()->mkNode(kind::AND
, c_and
);
954 case kind::REGEXP_INTER
: {
955 bool emptyflag
= false;
956 std::vector
< Node
> c_or
;
957 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
958 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
959 c_or
.push_back( r
[i
][0].eqNode(s
).negate() );
960 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
964 c_or
.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[i
]).negate());
970 conc
= c_or
.size() == 1 ? c_or
[0] : NodeManager::currentNM()->mkNode(kind::OR
, c_or
);
974 case kind::REGEXP_STAR
: {
975 if(s
== d_emptyString
) {
977 } else if(r
[0].getKind() == kind::REGEXP_EMPTY
) {
978 conc
= s
.eqNode(d_emptyString
).negate();
979 } else if(r
[0].getKind() == kind::REGEXP_SIGMA
) {
982 Node lens
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
);
983 Node sne
= s
.eqNode(d_emptyString
).negate();
984 Node b1
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
985 Node b1v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, b1
);
986 Node g1
= NodeManager::currentNM()->mkNode( kind::AND
, NodeManager::currentNM()->mkNode(kind::GEQ
, b1
, d_one
),
987 NodeManager::currentNM()->mkNode( kind::GEQ
, lens
, b1
) );
989 Node s1
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL
, s
, d_zero
, b1
);
990 Node s2
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL
, s
, b1
, NodeManager::currentNM()->mkNode(kind::MINUS
, lens
, b1
));
991 Node s1r1
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s1
, r
[0]).negate();
992 Node s2r2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s2
, r
).negate();
994 conc
= NodeManager::currentNM()->mkNode(kind::OR
, s1r1
, s2r2
);
995 conc
= NodeManager::currentNM()->mkNode(kind::IMPLIES
, g1
, conc
);
996 conc
= NodeManager::currentNM()->mkNode(kind::FORALL
, b1v
, conc
);
997 conc
= NodeManager::currentNM()->mkNode(kind::AND
, sne
, conc
);
1002 Trace("strings-regexp") << "Unsupported term: " << r
<< " in simplifyNRegExp." << std::endl
;
1003 Assert( false, "Unsupported Term" );
1006 conc
= Rewriter::rewrite( conc
);
1007 new_nodes
.push_back( conc
);
1008 d_simpl_neg_cache
[p
] = conc
;
1011 void RegExpOpr::simplifyPRegExp( Node s
, Node r
, std::vector
< Node
> &new_nodes
) {
1012 std::pair
< Node
, Node
> p(s
, r
);
1013 std::map
< std::pair
< Node
, Node
>, Node
>::const_iterator itr
= d_simpl_cache
.find(p
);
1014 if(itr
!= d_simpl_cache
.end()) {
1015 new_nodes
.push_back( itr
->second
);
1017 int k
= r
.getKind();
1020 case kind::REGEXP_EMPTY
: {
1024 case kind::REGEXP_SIGMA
: {
1025 conc
= d_one
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
));
1028 case kind::STRING_TO_REGEXP
: {
1029 conc
= s
.eqNode(r
[0]);
1032 case kind::REGEXP_CONCAT
: {
1033 std::vector
< Node
> nvec
;
1034 std::vector
< Node
> cc
;
1035 bool emptyflag
= false;
1036 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
1037 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
1038 cc
.push_back( r
[i
][0] );
1039 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
1043 Node sk
= NodeManager::currentNM()->mkSkolem( "rc_$$", s
.getType(), "created for regular expression concat" );
1044 Node lem
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, sk
, r
[i
]);
1045 nvec
.push_back(lem
);
1052 Node lem
= s
.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
, cc
) );
1053 nvec
.push_back(lem
);
1054 conc
= nvec
.size() == 1 ? nvec
[0] : NodeManager::currentNM()->mkNode(kind::AND
, nvec
);
1058 case kind::REGEXP_UNION
: {
1059 std::vector
< Node
> c_or
;
1060 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
1061 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
1062 c_or
.push_back( r
[i
][0].eqNode(s
) );
1063 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
1066 c_or
.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[i
]));
1069 conc
= c_or
.size() == 0 ? d_false
:
1070 c_or
.size() == 1 ? c_or
[0] : NodeManager::currentNM()->mkNode(kind::OR
, c_or
);
1073 case kind::REGEXP_INTER
: {
1074 std::vector
< Node
> c_and
;
1075 bool emptyflag
= false;
1076 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
1077 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
1078 c_and
.push_back( r
[i
][0].eqNode(s
) );
1079 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
1083 c_and
.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[i
]));
1089 conc
= c_and
.size() == 1 ? c_and
[0] : NodeManager::currentNM()->mkNode(kind::AND
, c_and
);
1093 case kind::REGEXP_STAR
: {
1094 if(s
== d_emptyString
) {
1096 } else if(r
[0].getKind() == kind::REGEXP_EMPTY
) {
1097 conc
= s
.eqNode(d_emptyString
);
1098 } else if(r
[0].getKind() == kind::REGEXP_SIGMA
) {
1101 Node se
= s
.eqNode(d_emptyString
);
1102 Node sinr
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[0]);
1103 Node sk1
= NodeManager::currentNM()->mkSkolem( "rs_$$", s
.getType(), "created for regular expression star" );
1104 Node sk2
= NodeManager::currentNM()->mkSkolem( "rs_$$", s
.getType(), "created for regular expression star" );
1105 Node s1nz
= sk1
.eqNode(d_emptyString
).negate();
1106 Node s2nz
= sk2
.eqNode(d_emptyString
).negate();
1107 Node s1inr
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, sk1
, r
[0]);
1108 Node s2inrs
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, sk2
, r
);
1109 Node s12
= s
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
, sk1
, sk2
));
1111 conc
= NodeManager::currentNM()->mkNode(kind::AND
, s12
, s1nz
, s2nz
, s1inr
, s2inrs
);
1112 conc
= NodeManager::currentNM()->mkNode(kind::OR
, se
, sinr
, conc
);
1117 Trace("strings-regexp") << "Unsupported term: " << r
<< " in simplifyPRegExp." << std::endl
;
1118 Assert( false, "Unsupported Term" );
1121 conc
= Rewriter::rewrite( conc
);
1122 new_nodes
.push_back( conc
);
1123 d_simpl_cache
[p
] = conc
;
1127 void RegExpOpr::getCharSet( Node r
, std::set
<unsigned> &pcset
, SetNodes
&pvset
) {
1128 std::map
< Node
, std::pair
< std::set
<unsigned>, SetNodes
> >::const_iterator itr
= d_cset_cache
.find(r
);
1129 if(itr
!= d_cset_cache
.end()) {
1130 pcset
.insert((itr
->second
).first
.begin(), (itr
->second
).first
.end());
1131 pvset
.insert((itr
->second
).second
.begin(), (itr
->second
).second
.end());
1133 std::set
<unsigned> cset
;
1135 int k
= r
.getKind();
1137 case kind::REGEXP_EMPTY
: {
1140 case kind::REGEXP_SIGMA
: {
1141 for(unsigned i
=0; i
<d_card
; i
++) {
1146 case kind::STRING_TO_REGEXP
: {
1147 Node st
= Rewriter::rewrite(r
[0]);
1149 CVC4::String s
= st
.getConst
< CVC4::String
>();
1150 s
.getCharSet( cset
);
1151 } else if(st
.getKind() == kind::VARIABLE
) {
1154 for(unsigned i
=0; i
<st
.getNumChildren(); i
++) {
1155 if(st
[i
].isConst()) {
1156 CVC4::String s
= st
[i
].getConst
< CVC4::String
>();
1157 s
.getCharSet( cset
);
1159 vset
.insert( st
[i
] );
1165 case kind::REGEXP_CONCAT
: {
1166 for(unsigned i
=0; i
<r
.getNumChildren(); i
++) {
1167 getCharSet(r
[i
], cset
, vset
);
1171 case kind::REGEXP_UNION
: {
1172 for(unsigned i
=0; i
<r
.getNumChildren(); i
++) {
1173 getCharSet(r
[i
], cset
, vset
);
1177 case kind::REGEXP_INTER
: {
1178 //TODO: Overapproximation for now
1179 for(unsigned i
=0; i
<r
.getNumChildren(); i
++) {
1180 getCharSet(r
[i
], cset
, vset
);
1184 case kind::REGEXP_STAR
: {
1185 getCharSet(r
[0], cset
, vset
);
1189 Trace("strings-regexp") << "Unsupported term: " << r
<< " in getCharSet." << std::endl
;
1190 Assert( false, "Unsupported Term" );
1193 pcset
.insert(cset
.begin(), cset
.end());
1194 pvset
.insert(vset
.begin(), vset
.end());
1195 std::pair
< std::set
<unsigned>, SetNodes
> p(cset
, vset
);
1196 d_cset_cache
[r
] = p
;
1198 Trace("regexp-cset") << "CSET( " << mkString(r
) << " ) = { ";
1199 for(std::set
<unsigned>::const_iterator itr
= cset
.begin();
1200 itr
!= cset
.end(); itr
++) {
1201 Trace("regexp-cset") << CVC4::String::convertUnsignedIntToChar(*itr
) << ",";
1203 Trace("regexp-cset") << " }" << std::endl
;
1208 Node
RegExpOpr::intersectInternal( Node r1
, Node r2
, std::map
< unsigned, std::set
< PairNodes
> > cache
, bool &spflag
) {
1211 return Node::null();
1214 std::pair
< Node
, Node
> p(r1
, r2
);
1215 std::map
< std::pair
< Node
, Node
>, Node
>::const_iterator itr
= d_inter_cache
.find(p
);
1217 if(itr
!= d_inter_cache
.end()) {
1218 rNode
= itr
->second
;
1222 } else if(r1
== d_emptyRegexp
|| r2
== d_emptyRegexp
) {
1223 Trace("regexp-intersect") << "INTERSECT Case 1: one empty RE" << std::endl
;
1224 rNode
= d_emptyRegexp
;
1225 } else if(r1
== d_emptySingleton
|| r2
== d_emptySingleton
) {
1226 Trace("regexp-intersect") << "INTERSECT Case 2: one empty Singleton" << std::endl
;
1228 int r
= delta((r1
== d_emptySingleton
? r2
: r1
), exp
);
1232 //Assert( false, "Unsupported Yet, 892 REO" );
1234 rNode
= d_emptySingleton
;
1236 rNode
= d_emptyRegexp
;
1239 Trace("regexp-intersect") << "INTERSECT Case 3: must compare" << std::endl
;
1240 std::set
< unsigned > cset
, cset2
;
1241 std::vector
< unsigned > cdiff
;
1242 std::set
< Node
> vset
;
1243 getCharSet(r1
, cset
, vset
);
1244 getCharSet(r2
, cset2
, vset
);
1246 std::set_symmetric_difference(cset
.begin(), cset
.end(), cset2
.begin(), cset2
.end(), std::back_inserter(cdiff
));
1248 Trace("regexp-intersect") << "INTERSECT Case 3.1: compare" << std::endl
;
1250 firstChars(r1
, cset
, vset
);
1251 std::vector
< Node
> vec_nodes
;
1252 for(std::set
<unsigned>::const_iterator itr
= cset
.begin();
1253 itr
!= cset
.end(); itr
++) {
1254 CVC4::String
c( CVC4::String::convertUnsignedIntToChar(*itr
) );
1255 std::pair
< Node
, Node
> p(r1
, r2
);
1256 if(cache
[ *itr
].find(p
) == cache
[ *itr
].end()) {
1257 Node r1l
= derivativeSingle(r1
, c
);
1258 Node r2l
= derivativeSingle(r2
, c
);
1259 std::map
< unsigned, std::set
< PairNodes
> > cache2(cache
);
1260 PairNodes
p(r1l
, r2l
);
1261 cache2
[ *itr
].insert( p
);
1262 Node rt
= intersectInternal(r1l
, r2l
, cache2
, spflag
);
1265 return Node::null();
1267 rt
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
,
1268 NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP
, NodeManager::currentNM()->mkConst(c
)), rt
) );
1269 vec_nodes
.push_back(rt
);
1272 rNode
= vec_nodes
.size()==0 ? d_emptyRegexp
: vec_nodes
.size()==1 ? vec_nodes
[0] :
1273 NodeManager::currentNM()->mkNode(kind::REGEXP_UNION
, vec_nodes
);
1274 rNode
= Rewriter::rewrite( rNode
);
1276 Trace("regexp-intersect") << "INTERSECT Case 3.2: diff cset" << std::endl
;
1277 rNode
= d_emptyRegexp
;
1280 //TODO: non-empty var set
1282 //Assert( false, "Unsupported Yet, 927 REO" );
1286 d_inter_cache
[p
] = rNode
;
1288 Trace("regexp-intersect") << "INTERSECT( " << mkString(r1
) << ", " << mkString(r2
) << " ) = " << mkString(rNode
) << std::endl
;
1291 Node
RegExpOpr::intersect(Node r1
, Node r2
, bool &spflag
) {
1292 std::map
< unsigned, std::set
< PairNodes
> > cache
;
1293 return intersectInternal(r1
, r2
, cache
, spflag
);
1297 Node
RegExpOpr::complement(Node r
, int &ret
) {
1300 if(d_compl_cache
.find(r
) != d_compl_cache
.end()) {
1301 rNode
= d_compl_cache
[r
].first
;
1302 ret
= d_compl_cache
[r
].second
;
1304 if(r
== d_emptyRegexp
) {
1305 rNode
= d_sigma_star
;
1306 } else if(r
== d_emptySingleton
) {
1307 rNode
= NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
, d_sigma
, d_sigma_star
);
1308 } else if(!checkConstRegExp(r
)) {
1309 //TODO: var to be extended
1312 std::set
<unsigned> cset
;
1314 firstChars(r
, cset
, vset
);
1315 Assert(!vset
.empty(), "Regexp 1298 Error");
1316 std::vector
< Node
> vec_nodes
;
1317 for(unsigned i
=0; i
<d_card
; i
++) {
1318 CVC4::String c
= CVC4::String::convertUnsignedIntToChar(i
);
1319 Node n
= NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP
, NodeManager::currentNM()->mkConst(c
));
1321 if(cset
.find(i
) == cset
.end()) {
1325 derivativeS(r
, c
, r2
);
1329 r2
= complement(r2
, rt
);
1332 n
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
, n
, r2
));
1333 vec_nodes
.push_back(n
);
1335 rNode
= vec_nodes
.size()==0? d_emptyRegexp
: vec_nodes
.size()==1? vec_nodes
[0] :
1336 NodeManager::currentNM()->mkNode(kind::REGEXP_UNION
, vec_nodes
);
1338 std::pair
< Node
, int > p(rNode
, ret
);
1339 d_compl_cache
[r
] = p
;
1341 Trace("regexp-compl") << "COMPL( " << mkString(r
) << " ) = " << mkString(rNode
) << ", ret=" << ret
<< std::endl
;
1345 std::string
RegExpOpr::niceChar( Node r
) {
1347 std::string s
= r
.getConst
<CVC4::String
>().toString() ;
1348 return s
== "" ? "{E}" : ( s
== " " ? "{ }" : s
);
1350 return r
.toString();
1353 std::string
RegExpOpr::mkString( Node r
) {
1358 int k
= r
.getKind();
1360 case kind::REGEXP_EMPTY
: {
1364 case kind::REGEXP_SIGMA
: {
1368 case kind::STRING_TO_REGEXP
: {
1369 retStr
+= niceChar( r
[0] );
1372 case kind::REGEXP_CONCAT
: {
1374 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
1375 //if(i != 0) retStr += ".";
1376 retStr
+= mkString( r
[i
] );
1381 case kind::REGEXP_UNION
: {
1386 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
1387 if(i
!= 0) retStr
+= "|";
1388 retStr
+= mkString( r
[i
] );
1394 case kind::REGEXP_INTER
: {
1396 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
1397 if(i
!= 0) retStr
+= "&";
1398 retStr
+= mkString( r
[i
] );
1403 case kind::REGEXP_STAR
: {
1404 retStr
+= mkString( r
[0] );
1408 case kind::REGEXP_PLUS
: {
1409 retStr
+= mkString( r
[0] );
1413 case kind::REGEXP_OPT
: {
1414 retStr
+= mkString( r
[0] );
1418 case kind::REGEXP_RANGE
: {
1420 retStr
+= niceChar( r
[0] );
1422 retStr
+= niceChar( r
[1] );
1427 Trace("strings-error") << "Unsupported term: " << r
<< " in RegExp." << std::endl
;
1429 //return Node::null();
1436 }/* CVC4::theory::strings namespace */
1437 }/* CVC4::theory namespace */
1438 }/* CVC4 namespace */