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 d_sigma
= NodeManager::currentNM()->mkNode( kind::REGEXP_SIGMA
, nvec
);
45 d_sigma_star
= NodeManager::currentNM()->mkNode( kind::REGEXP_STAR
, d_sigma
);
49 int RegExpOpr::gcd ( int a
, int b
) {
52 c
= a
; a
= b
%a
; b
= c
;
57 bool RegExpOpr::checkConstRegExp( Node r
) {
58 Trace("strings-regexp-cstre") << "RegExp-CheckConstRegExp starts with " << mkString( r
) << std::endl
;
60 if( d_cstre_cache
.find( r
) != d_cstre_cache
.end() ) {
61 ret
= d_cstre_cache
[r
];
63 if(r
.getKind() == kind::STRING_TO_REGEXP
) {
64 Node tmp
= Rewriter::rewrite( r
[0] );
67 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
68 if(!checkConstRegExp(r
[i
])) {
73 d_cstre_cache
[r
] = ret
;
78 // 0-unknown, 1-yes, 2-no
79 int RegExpOpr::delta( Node r
, Node
&exp
) {
80 Trace("regexp-delta") << "RegExp-Delta starts with " << mkString( r
) << std::endl
;
82 if( d_delta_cache
.find( r
) != d_delta_cache
.end() ) {
83 ret
= d_delta_cache
[r
].first
;
84 exp
= d_delta_cache
[r
].second
;
88 case kind::REGEXP_EMPTY
: {
92 case kind::REGEXP_SIGMA
: {
96 case kind::STRING_TO_REGEXP
: {
97 Node tmp
= Rewriter::rewrite(r
[0]);
99 if(tmp
== d_emptyString
) {
106 if(tmp
.getKind() == kind::STRING_CONCAT
) {
107 for(unsigned i
=0; i
<tmp
.getNumChildren(); i
++) {
108 if(tmp
[i
].isConst()) {
115 exp
= r
[0].eqNode(d_emptyString
);
120 case kind::REGEXP_CONCAT
: {
122 std::vector
< Node
> vec_nodes
;
123 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
125 int tmp
= delta( r
[i
], exp2
);
129 } else if(tmp
== 0) {
130 vec_nodes
.push_back( exp2
);
138 exp
= vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode(kind::AND
, vec_nodes
);
143 case kind::REGEXP_UNION
: {
145 std::vector
< Node
> vec_nodes
;
146 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
148 int tmp
= delta( r
[i
], exp2
);
152 } else if(tmp
== 0) {
153 vec_nodes
.push_back( exp2
);
161 exp
= vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode(kind::OR
, vec_nodes
);
166 case kind::REGEXP_INTER
: {
168 std::vector
< Node
> vec_nodes
;
169 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
171 int tmp
= delta( r
[i
], exp2
);
175 } else if(tmp
== 0) {
176 vec_nodes
.push_back( exp2
);
184 exp
= vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode(kind::AND
, vec_nodes
);
189 case kind::REGEXP_STAR
: {
193 case kind::REGEXP_PLUS
: {
194 ret
= delta( r
[0], exp
);
197 case kind::REGEXP_OPT
: {
201 case kind::REGEXP_RANGE
: {
206 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in delta of RegExp." << std::endl
;
208 //return Node::null();
212 exp
= Rewriter::rewrite(exp
);
214 std::pair
< int, Node
> p(ret
, exp
);
215 d_delta_cache
[r
] = p
;
217 Trace("regexp-delta") << "RegExp-Delta returns : " << ret
<< std::endl
;
221 // 0-unknown, 1-yes, 2-no
222 int RegExpOpr::derivativeS( Node r
, CVC4::String c
, Node
&retNode
) {
223 Assert( c
.size() < 2 );
224 Trace("regexp-deriv") << "RegExp-deriv starts with R{ " << mkString( r
) << " }, c=" << c
<< std::endl
;
227 retNode
= d_emptyRegexp
;
229 PairNodeStr dv
= std::make_pair( r
, c
);
230 if( d_deriv_cache
.find( dv
) != d_deriv_cache
.end() ) {
231 retNode
= d_deriv_cache
[dv
].first
;
232 ret
= d_deriv_cache
[dv
].second
;
233 } else if( c
.isEmptyString() ) {
235 ret
= delta( r
, expNode
);
237 retNode
= NodeManager::currentNM()->mkNode(kind::ITE
, expNode
, r
, d_emptyRegexp
);
238 } else if(ret
== 1) {
241 std::pair
< Node
, int > p(retNode
, ret
);
242 d_deriv_cache
[dv
] = p
;
244 switch( r
.getKind() ) {
245 case kind::REGEXP_EMPTY
: {
249 case kind::REGEXP_SIGMA
: {
250 retNode
= d_emptySingleton
;
253 case kind::STRING_TO_REGEXP
: {
254 Node tmp
= Rewriter::rewrite(r
[0]);
256 if(tmp
== d_emptyString
) {
259 if(tmp
.getConst
< CVC4::String
>().getFirstChar() == c
.getFirstChar()) {
260 retNode
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
,
261 tmp
.getConst
< CVC4::String
>().size() == 1 ? d_emptyString
: NodeManager::currentNM()->mkConst( tmp
.getConst
< CVC4::String
>().substr(1) ) );
269 if(tmp
.getKind() == kind::STRING_CONCAT
) {
272 if(t2
.getConst
< CVC4::String
>().getFirstChar() == c
.getFirstChar()) {
273 Node n
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
,
274 tmp
.getConst
< CVC4::String
>().size() == 1 ? d_emptyString
: NodeManager::currentNM()->mkConst( tmp
.getConst
< CVC4::String
>().substr(1) ) );
275 std::vector
< Node
> vec_nodes
;
276 vec_nodes
.push_back(n
);
277 for(unsigned i
=1; i
<tmp
.getNumChildren(); i
++) {
278 vec_nodes
.push_back(tmp
[i
]);
280 retNode
= NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
, vec_nodes
);
287 std::vector
< Node
> vec_nodes
;
288 for(unsigned i
=1; i
<tmp
.getNumChildren(); i
++) {
289 vec_nodes
.push_back(tmp
[i
]);
291 rest
= NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
, vec_nodes
);
295 Node sk
= NodeManager::currentNM()->mkSkolem( "rsp", NodeManager::currentNM()->stringType(), "Split RegExp" );
296 retNode
= NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP
, sk
);
298 retNode
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
, retNode
, rest
));
300 Node exp
= tmp
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
,
301 NodeManager::currentNM()->mkConst(c
), sk
));
302 retNode
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE
, exp
, retNode
, d_emptyRegexp
));
307 case kind::REGEXP_CONCAT
: {
308 std::vector
< Node
> vec_nodes
;
309 std::vector
< Node
> delta_nodes
;
311 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
314 int rt
= derivativeS(r
[i
], c
, dc
);
319 std::vector
< Node
> vec_nodes2
;
320 if(dc
!= d_emptySingleton
) {
321 vec_nodes2
.push_back( dc
);
323 for(unsigned j
=i
+1; j
<r
.getNumChildren(); ++j
) {
324 if(r
[j
] != d_emptySingleton
) {
325 vec_nodes2
.push_back( r
[j
] );
328 Node tmp
= vec_nodes2
.size()==0 ? d_emptySingleton
:
329 vec_nodes2
.size()==1 ? vec_nodes2
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, vec_nodes2
);
330 if(dnode
!= d_true
) {
331 tmp
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE
, dnode
, tmp
, d_emptyRegexp
));
334 if(std::find(vec_nodes
.begin(), vec_nodes
.end(), tmp
) == vec_nodes
.end()) {
335 vec_nodes
.push_back( tmp
);
339 int rt2
= delta( r
[i
], exp3
);
341 dnode
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND
, dnode
, exp3
));
342 } else if( rt2
== 2 ) {
346 retNode
= vec_nodes
.size() == 0 ? d_emptyRegexp
:
347 ( vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_UNION
, vec_nodes
) );
348 if(retNode
== d_emptyRegexp
) {
353 case kind::REGEXP_UNION
: {
354 std::vector
< Node
> vec_nodes
;
355 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
357 int rt
= derivativeS(r
[i
], c
, dc
);
362 if(std::find(vec_nodes
.begin(), vec_nodes
.end(), dc
) == vec_nodes
.end()) {
363 vec_nodes
.push_back( dc
);
366 Trace("regexp-deriv") << "RegExp-deriv OR R[" << i
<< "]{ " << mkString(r
[i
]) << " returns " << mkString(dc
) << std::endl
;
368 retNode
= vec_nodes
.size() == 0 ? d_emptyRegexp
:
369 ( vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_UNION
, vec_nodes
) );
370 if(retNode
== d_emptyRegexp
) {
375 case kind::REGEXP_INTER
: {
377 bool flag_sg
= false;
378 std::vector
< Node
> vec_nodes
;
379 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
381 int rt
= derivativeS(r
[i
], c
, dc
);
388 if(dc
== d_sigma_star
) {
391 if(std::find(vec_nodes
.begin(), vec_nodes
.end(), dc
) == vec_nodes
.end()) {
392 vec_nodes
.push_back( dc
);
397 if(vec_nodes
.size() == 0 && flag_sg
) {
398 retNode
= d_sigma_star
;
400 retNode
= vec_nodes
.size() == 0 ? d_emptyRegexp
:
401 ( vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_INTER
, vec_nodes
) );
402 if(retNode
== d_emptyRegexp
) {
407 retNode
= d_emptyRegexp
;
412 case kind::REGEXP_STAR
: {
414 ret
= derivativeS(r
[0], c
, dc
);
415 retNode
= dc
==d_emptyRegexp
? dc
: (dc
==d_emptySingleton
? r
: NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, dc
, r
));
419 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in derivative of RegExp." << std::endl
;
420 Assert( false, "Unsupported Term" );
423 if(retNode
!= d_emptyRegexp
) {
424 retNode
= Rewriter::rewrite( retNode
);
426 std::pair
< Node
, int > p(retNode
, ret
);
427 d_deriv_cache
[dv
] = p
;
430 Trace("regexp-deriv") << "RegExp-deriv returns : " << mkString( retNode
) << std::endl
;
434 Node
RegExpOpr::derivativeSingle( Node r
, CVC4::String c
) {
435 Assert( c
.size() < 2 );
436 Trace("regexp-deriv") << "RegExp-deriv starts with R{ " << mkString( r
) << " }, c=" << c
<< std::endl
;
437 Node retNode
= d_emptyRegexp
;
438 PairNodeStr dv
= std::make_pair( r
, c
);
439 if( d_dv_cache
.find( dv
) != d_dv_cache
.end() ) {
440 retNode
= d_dv_cache
[dv
];
441 } else if( c
.isEmptyString() ){
443 int tmp
= delta( r
, exp
);
446 retNode
= d_emptyRegexp
;
447 } else if(tmp
== 1) {
450 retNode
= d_emptyRegexp
;
455 case kind::REGEXP_EMPTY
: {
456 retNode
= d_emptyRegexp
;
459 case kind::REGEXP_SIGMA
: {
460 retNode
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, d_emptyString
);
463 case kind::STRING_TO_REGEXP
: {
465 if(r
[0] == d_emptyString
) {
466 retNode
= d_emptyRegexp
;
468 if(r
[0].getConst
< CVC4::String
>().getFirstChar() == c
.getFirstChar()) {
469 retNode
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
,
470 r
[0].getConst
< CVC4::String
>().size() == 1 ? d_emptyString
: NodeManager::currentNM()->mkConst( r
[0].getConst
< CVC4::String
>().substr(1) ) );
472 retNode
= d_emptyRegexp
;
477 retNode
= d_emptyRegexp
;
481 case kind::REGEXP_CONCAT
: {
482 Node rees
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, d_emptyString
);
483 std::vector
< Node
> vec_nodes
;
484 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
485 Node dc
= derivativeSingle(r
[i
], c
);
486 if(dc
!= d_emptyRegexp
) {
487 std::vector
< Node
> vec_nodes2
;
489 vec_nodes2
.push_back( dc
);
491 for(unsigned j
=i
+1; j
<r
.getNumChildren(); ++j
) {
493 vec_nodes2
.push_back( r
[j
] );
496 Node tmp
= vec_nodes2
.size()==0 ? rees
:
497 vec_nodes2
.size()==1 ? vec_nodes2
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, vec_nodes2
);
498 if(std::find(vec_nodes
.begin(), vec_nodes
.end(), tmp
) == vec_nodes
.end()) {
499 vec_nodes
.push_back( tmp
);
503 if( delta( r
[i
], exp
) != 1 ) {
507 retNode
= vec_nodes
.size() == 0 ? d_emptyRegexp
:
508 ( vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_UNION
, vec_nodes
) );
511 case kind::REGEXP_UNION
: {
512 std::vector
< Node
> vec_nodes
;
513 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
514 Node dc
= derivativeSingle(r
[i
], c
);
515 if(dc
!= d_emptyRegexp
) {
516 if(std::find(vec_nodes
.begin(), vec_nodes
.end(), dc
) == vec_nodes
.end()) {
517 vec_nodes
.push_back( dc
);
520 Trace("regexp-deriv") << "RegExp-deriv OR R[" << i
<< "]{ " << mkString(r
[i
]) << " returns " << mkString(dc
) << std::endl
;
522 retNode
= vec_nodes
.size() == 0 ? d_emptyRegexp
:
523 ( vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_UNION
, vec_nodes
) );
526 case kind::REGEXP_INTER
: {
528 bool flag_sg
= false;
529 std::vector
< Node
> vec_nodes
;
530 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
531 Node dc
= derivativeSingle(r
[i
], c
);
532 if(dc
!= d_emptyRegexp
) {
533 if(dc
== d_sigma_star
) {
536 if(std::find(vec_nodes
.begin(), vec_nodes
.end(), dc
) == vec_nodes
.end()) {
537 vec_nodes
.push_back( dc
);
546 if(vec_nodes
.size() == 0 && flag_sg
) {
547 retNode
= d_sigma_star
;
549 retNode
= vec_nodes
.size() == 0 ? d_emptyRegexp
:
550 ( vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_INTER
, vec_nodes
) );
553 retNode
= d_emptyRegexp
;
557 case kind::REGEXP_STAR
: {
558 Node dc
= derivativeSingle(r
[0], c
);
559 if(dc
!= d_emptyRegexp
) {
560 retNode
= dc
==NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, d_emptyString
) ? r
: NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, dc
, r
);
562 retNode
= d_emptyRegexp
;
567 //TODO: special sym: sigma, none, all
568 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in derivative of RegExp." << std::endl
;
569 Assert( false, "Unsupported Term" );
570 //return Node::null();
573 if(retNode
!= d_emptyRegexp
) {
574 retNode
= Rewriter::rewrite( retNode
);
576 d_dv_cache
[dv
] = retNode
;
578 Trace("regexp-deriv") << "RegExp-deriv returns : " << mkString( retNode
) << std::endl
;
583 bool RegExpOpr::guessLength( Node r
, int &co
) {
586 case kind::STRING_TO_REGEXP
:
589 co
+= r
[0].getConst
< CVC4::String
>().size();
596 case kind::REGEXP_CONCAT
:
598 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
599 if(!guessLength( r
[i
], co
)) {
606 case kind::REGEXP_UNION
:
609 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
611 if(!guessLength( r
[i
], cop
)) {
617 g_co
= gcd(g_co
, cop
);
623 case kind::REGEXP_INTER
:
626 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
628 if(!guessLength( r
[i
], cop
)) {
634 g_co
= gcd(g_co
, cop
);
640 case kind::REGEXP_STAR
:
647 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in membership of RegExp." << std::endl
;
652 void RegExpOpr::firstChars( Node r
, std::set
<unsigned> &pcset
, SetNodes
&pvset
) {
653 std::map
< Node
, std::pair
< std::set
<unsigned>, SetNodes
> >::const_iterator itr
= d_fset_cache
.find(r
);
654 if(itr
!= d_fset_cache
.end()) {
655 pcset
.insert((itr
->second
).first
.begin(), (itr
->second
).first
.end());
656 pvset
.insert((itr
->second
).second
.begin(), (itr
->second
).second
.end());
658 std::set
<unsigned> cset
;
662 case kind::REGEXP_EMPTY
: {
665 case kind::REGEXP_SIGMA
: {
666 for(unsigned i
=0; i
<d_card
; i
++) {
671 case kind::STRING_TO_REGEXP
: {
672 Node st
= Rewriter::rewrite(r
[0]);
674 CVC4::String s
= st
.getConst
< CVC4::String
>();
678 } else if(st
.getKind() == kind::VARIABLE
) {
681 if(st
[0].isConst()) {
682 CVC4::String s
= st
[0].getConst
< CVC4::String
>();
685 vset
.insert( st
[0] );
690 case kind::REGEXP_CONCAT
: {
691 for(unsigned i
=0; i
<r
.getNumChildren(); i
++) {
692 firstChars(r
[i
], cset
, vset
);
695 int r
= delta( n
, exp
);
702 case kind::REGEXP_UNION
: {
703 for(unsigned i
=0; i
<r
.getNumChildren(); i
++) {
704 firstChars(r
[i
], cset
, vset
);
708 case kind::REGEXP_INTER
: {
709 //TODO: Overapproximation for now
710 for(unsigned i
=0; i
<r
.getNumChildren(); i
++) {
711 firstChars(r
[i
], cset
, vset
);
715 case kind::REGEXP_STAR
: {
716 firstChars(r
[0], cset
, vset
);
720 Trace("strings-regexp") << "Unsupported term: " << r
<< " in getCharSet." << std::endl
;
721 Assert( false, "Unsupported Term" );
724 pcset
.insert(cset
.begin(), cset
.end());
725 pvset
.insert(vset
.begin(), vset
.end());
726 std::pair
< std::set
<unsigned>, SetNodes
> p(cset
, vset
);
729 Trace("regexp-fset") << "FSET( " << mkString(r
) << " ) = { ";
730 for(std::set
<unsigned>::const_iterator itr
= cset
.begin();
731 itr
!= cset
.end(); itr
++) {
732 Trace("regexp-fset") << CVC4::String::convertUnsignedIntToChar(*itr
) << ",";
734 Trace("regexp-fset") << " }" << std::endl
;
738 bool RegExpOpr::follow( Node r
, CVC4::String c
, std::vector
< char > &vec_chars
) {
741 case kind::STRING_TO_REGEXP
:
744 if(r
[0] != d_emptyString
) {
745 char t1
= r
[0].getConst
< CVC4::String
>().getFirstChar();
746 if(c
.isEmptyString()) {
747 vec_chars
.push_back( t1
);
750 char t2
= c
.getFirstChar();
755 vec_chars
.push_back( c
.substr(1,1).getFirstChar() );
757 vec_chars
.push_back( '\0' );
770 case kind::REGEXP_CONCAT
:
772 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
773 if( follow(r
[i
], c
, vec_chars
) ) {
774 if(vec_chars
[vec_chars
.size() - 1] == '\0') {
775 vec_chars
.pop_back();
776 c
= d_emptyString
.getConst
< CVC4::String
>();
782 vec_chars
.push_back( '\0' );
786 case kind::REGEXP_UNION
:
789 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
790 if( follow(r
[i
], c
, vec_chars
) ) {
797 case kind::REGEXP_INTER
:
799 std::vector
< char > vt2
;
800 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
801 std::vector
< char > v_tmp
;
802 if( !follow(r
[i
], c
, v_tmp
) ) {
805 std::vector
< char > vt3(vt2
);
807 std::set_intersection( vt3
.begin(), vt3
.end(), v_tmp
.begin(), v_tmp
.end(), vt2
.begin() );
808 if(vt2
.size() == 0) {
812 vec_chars
.insert( vec_chars
.end(), vt2
.begin(), vt2
.end() );
816 case kind::REGEXP_STAR
:
818 if(follow(r
[0], c
, vec_chars
)) {
819 if(vec_chars
[vec_chars
.size() - 1] == '\0') {
820 if(c
.isEmptyString()) {
823 vec_chars
.pop_back();
824 c
= d_emptyString
.getConst
< CVC4::String
>();
825 return follow(r
[0], c
, vec_chars
);
831 vec_chars
.push_back( '\0' );
837 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in delta of RegExp." << std::endl
;
838 //AlwaysAssert( false );
839 //return Node::null();
845 Node
RegExpOpr::mkAllExceptOne( char exp_c
) {
846 std::vector
< Node
> vec_nodes
;
847 for(char c
=d_char_start
; c
<=d_char_end
; ++c
) {
849 Node n
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, NodeManager::currentNM()->mkConst( ::CVC4::String( c
) ) );
850 vec_nodes
.push_back( n
);
853 return NodeManager::currentNM()->mkNode( kind::REGEXP_UNION
, vec_nodes
);
857 void RegExpOpr::simplify(Node t
, std::vector
< Node
> &new_nodes
, bool polarity
) {
858 Trace("strings-regexp-simpl") << "RegExp-Simpl starts with " << t
<< ", polarity=" << polarity
<< std::endl
;
859 Assert(t
.getKind() == kind::STRING_IN_REGEXP
);
860 Node str
= Rewriter::rewrite(t
[0]);
861 Node re
= Rewriter::rewrite(t
[1]);
863 simplifyPRegExp( str
, re
, new_nodes
);
865 simplifyNRegExp( str
, re
, new_nodes
);
867 Trace("strings-regexp-simpl") << "RegExp-Simpl returns (" << new_nodes
.size() << "):\n";
868 for(unsigned i
=0; i
<new_nodes
.size(); i
++) {
869 Trace("strings-regexp-simpl") << "\t" << new_nodes
[i
] << std::endl
;
872 void RegExpOpr::simplifyNRegExp( Node s
, Node r
, std::vector
< Node
> &new_nodes
) {
873 std::pair
< Node
, Node
> p(s
, r
);
874 std::map
< std::pair
< Node
, Node
>, Node
>::const_iterator itr
= d_simpl_neg_cache
.find(p
);
875 if(itr
!= d_simpl_neg_cache
.end()) {
876 new_nodes
.push_back( itr
->second
);
881 case kind::REGEXP_EMPTY
: {
885 case kind::REGEXP_SIGMA
: {
886 conc
= d_one
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
)).negate();
889 case kind::STRING_TO_REGEXP
: {
890 conc
= s
.eqNode(r
[0]).negate();
893 case kind::REGEXP_CONCAT
: {
894 //TODO: rewrite empty
895 Node lens
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
);
896 Node b1
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
897 Node b1v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, b1
);
898 Node g1
= NodeManager::currentNM()->mkNode( kind::AND
, NodeManager::currentNM()->mkNode(kind::GEQ
, b1
, d_zero
),
899 NodeManager::currentNM()->mkNode( kind::GEQ
, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
), b1
) );
900 Node s1
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL
, s
, d_zero
, b1
));
901 Node s2
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL
, s
, b1
, NodeManager::currentNM()->mkNode(kind::MINUS
, lens
, b1
)));
902 Node s1r1
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s1
, r
[0]).negate();
903 if(r
[0].getKind() == kind::STRING_TO_REGEXP
) {
904 s1r1
= s1
.eqNode(r
[0][0]).negate();
905 } else if(r
[0].getKind() == kind::REGEXP_EMPTY
) {
909 if(r
.getNumChildren() > 2) {
910 std::vector
< Node
> nvec
;
911 for(unsigned i
=1; i
<r
.getNumChildren(); i
++) {
912 nvec
.push_back( r
[i
] );
914 r2
= NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
, nvec
);
916 r2
= Rewriter::rewrite(r2
);
917 Node s2r2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s2
, r2
).negate();
918 if(r2
.getKind() == kind::STRING_TO_REGEXP
) {
919 s2r2
= s2
.eqNode(r2
[0]).negate();
920 } else if(r2
.getKind() == kind::REGEXP_EMPTY
) {
924 conc
= NodeManager::currentNM()->mkNode(kind::OR
, s1r1
, s2r2
);
925 conc
= NodeManager::currentNM()->mkNode(kind::IMPLIES
, g1
, conc
);
926 conc
= NodeManager::currentNM()->mkNode(kind::FORALL
, b1v
, conc
);
929 case kind::REGEXP_UNION
: {
930 std::vector
< Node
> c_and
;
931 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
932 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
933 c_and
.push_back( r
[i
][0].eqNode(s
).negate() );
934 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
937 c_and
.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[i
]).negate());
940 conc
= c_and
.size() == 0 ? d_true
:
941 c_and
.size() == 1 ? c_and
[0] : NodeManager::currentNM()->mkNode(kind::AND
, c_and
);
944 case kind::REGEXP_INTER
: {
945 bool emptyflag
= false;
946 std::vector
< Node
> c_or
;
947 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
948 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
949 c_or
.push_back( r
[i
][0].eqNode(s
).negate() );
950 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
954 c_or
.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[i
]).negate());
960 conc
= c_or
.size() == 1 ? c_or
[0] : NodeManager::currentNM()->mkNode(kind::OR
, c_or
);
964 case kind::REGEXP_STAR
: {
965 if(s
== d_emptyString
) {
967 } else if(r
[0].getKind() == kind::REGEXP_EMPTY
) {
968 conc
= s
.eqNode(d_emptyString
).negate();
969 } else if(r
[0].getKind() == kind::REGEXP_SIGMA
) {
972 Node lens
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
);
973 Node sne
= s
.eqNode(d_emptyString
).negate();
974 Node b1
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
975 Node b1v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, b1
);
976 Node g1
= NodeManager::currentNM()->mkNode( kind::AND
, NodeManager::currentNM()->mkNode(kind::GEQ
, b1
, d_one
),
977 NodeManager::currentNM()->mkNode( kind::GEQ
, lens
, b1
) );
979 Node s1
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL
, s
, d_zero
, b1
);
980 Node s2
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL
, s
, b1
, NodeManager::currentNM()->mkNode(kind::MINUS
, lens
, b1
));
981 Node s1r1
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s1
, r
[0]).negate();
982 Node s2r2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s2
, r
).negate();
984 conc
= NodeManager::currentNM()->mkNode(kind::OR
, s1r1
, s2r2
);
985 conc
= NodeManager::currentNM()->mkNode(kind::IMPLIES
, g1
, conc
);
986 conc
= NodeManager::currentNM()->mkNode(kind::FORALL
, b1v
, conc
);
987 conc
= NodeManager::currentNM()->mkNode(kind::AND
, sne
, conc
);
992 Trace("strings-regexp") << "Unsupported term: " << r
<< " in simplifyNRegExp." << std::endl
;
993 Assert( false, "Unsupported Term" );
996 conc
= Rewriter::rewrite( conc
);
997 new_nodes
.push_back( conc
);
998 d_simpl_neg_cache
[p
] = conc
;
1001 void RegExpOpr::simplifyPRegExp( Node s
, Node r
, std::vector
< Node
> &new_nodes
) {
1002 std::pair
< Node
, Node
> p(s
, r
);
1003 std::map
< std::pair
< Node
, Node
>, Node
>::const_iterator itr
= d_simpl_cache
.find(p
);
1004 if(itr
!= d_simpl_cache
.end()) {
1005 new_nodes
.push_back( itr
->second
);
1007 int k
= r
.getKind();
1010 case kind::REGEXP_EMPTY
: {
1014 case kind::REGEXP_SIGMA
: {
1015 conc
= d_one
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
));
1018 case kind::STRING_TO_REGEXP
: {
1019 conc
= s
.eqNode(r
[0]);
1022 case kind::REGEXP_CONCAT
: {
1023 std::vector
< Node
> nvec
;
1024 std::vector
< Node
> cc
;
1025 bool emptyflag
= false;
1026 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
1027 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
1028 cc
.push_back( r
[i
][0] );
1029 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
1033 Node sk
= NodeManager::currentNM()->mkSkolem( "rc", s
.getType(), "created for regular expression concat" );
1034 Node lem
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, sk
, r
[i
]);
1035 nvec
.push_back(lem
);
1042 Node lem
= s
.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
, cc
) );
1043 nvec
.push_back(lem
);
1044 conc
= nvec
.size() == 1 ? nvec
[0] : NodeManager::currentNM()->mkNode(kind::AND
, nvec
);
1048 case kind::REGEXP_UNION
: {
1049 std::vector
< Node
> c_or
;
1050 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
1051 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
1052 c_or
.push_back( r
[i
][0].eqNode(s
) );
1053 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
1056 c_or
.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[i
]));
1059 conc
= c_or
.size() == 0 ? d_false
:
1060 c_or
.size() == 1 ? c_or
[0] : NodeManager::currentNM()->mkNode(kind::OR
, c_or
);
1063 case kind::REGEXP_INTER
: {
1064 std::vector
< Node
> c_and
;
1065 bool emptyflag
= false;
1066 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
1067 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
1068 c_and
.push_back( r
[i
][0].eqNode(s
) );
1069 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
1073 c_and
.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[i
]));
1079 conc
= c_and
.size() == 1 ? c_and
[0] : NodeManager::currentNM()->mkNode(kind::AND
, c_and
);
1083 case kind::REGEXP_STAR
: {
1084 if(s
== d_emptyString
) {
1086 } else if(r
[0].getKind() == kind::REGEXP_EMPTY
) {
1087 conc
= s
.eqNode(d_emptyString
);
1088 } else if(r
[0].getKind() == kind::REGEXP_SIGMA
) {
1091 Node se
= s
.eqNode(d_emptyString
);
1092 Node sinr
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[0]);
1093 Node sk1
= NodeManager::currentNM()->mkSkolem( "rs", s
.getType(), "created for regular expression star" );
1094 Node sk2
= NodeManager::currentNM()->mkSkolem( "rs", s
.getType(), "created for regular expression star" );
1095 Node s1nz
= sk1
.eqNode(d_emptyString
).negate();
1096 Node s2nz
= sk2
.eqNode(d_emptyString
).negate();
1097 Node s1inr
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, sk1
, r
[0]);
1098 Node s2inrs
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, sk2
, r
);
1099 Node s12
= s
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
, sk1
, sk2
));
1101 conc
= NodeManager::currentNM()->mkNode(kind::AND
, s12
, s1nz
, s2nz
, s1inr
, s2inrs
);
1102 conc
= NodeManager::currentNM()->mkNode(kind::OR
, se
, sinr
, conc
);
1107 Trace("strings-regexp") << "Unsupported term: " << r
<< " in simplifyPRegExp." << std::endl
;
1108 Assert( false, "Unsupported Term" );
1111 conc
= Rewriter::rewrite( conc
);
1112 new_nodes
.push_back( conc
);
1113 d_simpl_cache
[p
] = conc
;
1117 void RegExpOpr::getCharSet( Node r
, std::set
<unsigned> &pcset
, SetNodes
&pvset
) {
1118 std::map
< Node
, std::pair
< std::set
<unsigned>, SetNodes
> >::const_iterator itr
= d_cset_cache
.find(r
);
1119 if(itr
!= d_cset_cache
.end()) {
1120 pcset
.insert((itr
->second
).first
.begin(), (itr
->second
).first
.end());
1121 pvset
.insert((itr
->second
).second
.begin(), (itr
->second
).second
.end());
1123 std::set
<unsigned> cset
;
1125 int k
= r
.getKind();
1127 case kind::REGEXP_EMPTY
: {
1130 case kind::REGEXP_SIGMA
: {
1131 for(unsigned i
=0; i
<d_card
; i
++) {
1136 case kind::STRING_TO_REGEXP
: {
1137 Node st
= Rewriter::rewrite(r
[0]);
1139 CVC4::String s
= st
.getConst
< CVC4::String
>();
1140 s
.getCharSet( cset
);
1141 } else if(st
.getKind() == kind::VARIABLE
) {
1144 for(unsigned i
=0; i
<st
.getNumChildren(); i
++) {
1145 if(st
[i
].isConst()) {
1146 CVC4::String s
= st
[i
].getConst
< CVC4::String
>();
1147 s
.getCharSet( cset
);
1149 vset
.insert( st
[i
] );
1155 case kind::REGEXP_CONCAT
: {
1156 for(unsigned i
=0; i
<r
.getNumChildren(); i
++) {
1157 getCharSet(r
[i
], cset
, vset
);
1161 case kind::REGEXP_UNION
: {
1162 for(unsigned i
=0; i
<r
.getNumChildren(); i
++) {
1163 getCharSet(r
[i
], cset
, vset
);
1167 case kind::REGEXP_INTER
: {
1168 //TODO: Overapproximation for now
1169 for(unsigned i
=0; i
<r
.getNumChildren(); i
++) {
1170 getCharSet(r
[i
], cset
, vset
);
1174 case kind::REGEXP_STAR
: {
1175 getCharSet(r
[0], cset
, vset
);
1179 Trace("strings-regexp") << "Unsupported term: " << r
<< " in getCharSet." << std::endl
;
1180 Assert( false, "Unsupported Term" );
1183 pcset
.insert(cset
.begin(), cset
.end());
1184 pvset
.insert(vset
.begin(), vset
.end());
1185 std::pair
< std::set
<unsigned>, SetNodes
> p(cset
, vset
);
1186 d_cset_cache
[r
] = p
;
1188 Trace("regexp-cset") << "CSET( " << mkString(r
) << " ) = { ";
1189 for(std::set
<unsigned>::const_iterator itr
= cset
.begin();
1190 itr
!= cset
.end(); itr
++) {
1191 Trace("regexp-cset") << CVC4::String::convertUnsignedIntToChar(*itr
) << ",";
1193 Trace("regexp-cset") << " }" << std::endl
;
1198 Node
RegExpOpr::intersectInternal( Node r1
, Node r2
, std::map
< unsigned, std::set
< PairNodes
> > cache
, bool &spflag
) {
1201 return Node::null();
1203 std::pair
< Node
, Node
> p(r1
, r2
);
1204 std::map
< std::pair
< Node
, Node
>, Node
>::const_iterator itr
= d_inter_cache
.find(p
);
1206 if(itr
!= d_inter_cache
.end()) {
1207 rNode
= itr
->second
;
1211 } else if(r1
== d_emptyRegexp
|| r2
== d_emptyRegexp
) {
1212 rNode
= d_emptyRegexp
;
1213 } else if(r1
== d_emptySingleton
|| r2
== d_emptySingleton
) {
1215 int r
= delta((r1
== d_emptySingleton
? r2
: r1
), exp
);
1220 rNode
= d_emptySingleton
;
1222 rNode
= d_emptyRegexp
;
1225 std::set
< unsigned > cset
, cset2
;
1226 std::set
< Node
> vset
, vset2
;
1227 getCharSet(r1
, cset
, vset
);
1228 getCharSet(r2
, cset2
, vset2
);
1229 if(vset
.empty() && vset2
.empty()) {
1231 firstChars(r1
, cset
, vset
);
1232 std::vector
< Node
> vec_nodes
;
1233 for(std::set
<unsigned>::const_iterator itr
= cset
.begin();
1234 itr
!= cset
.end(); itr
++) {
1235 CVC4::String
c( CVC4::String::convertUnsignedIntToChar(*itr
) );
1236 std::pair
< Node
, Node
> p(r1
, r2
);
1237 if(cache
[ *itr
].find(p
) == cache
[ *itr
].end()) {
1238 Node r1l
= derivativeSingle(r1
, c
);
1239 Node r2l
= derivativeSingle(r2
, c
);
1240 std::map
< unsigned, std::set
< PairNodes
> > cache2(cache
);
1241 PairNodes
p(r1l
, r2l
);
1242 cache2
[ *itr
].insert( p
);
1243 Node rt
= intersectInternal(r1l
, r2l
, cache2
, spflag
);
1246 return Node::null();
1248 rt
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
,
1249 NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP
, NodeManager::currentNM()->mkConst(c
)), rt
) );
1250 vec_nodes
.push_back(rt
);
1253 rNode
= vec_nodes
.size()==0 ? d_emptyRegexp
: vec_nodes
.size()==1 ? vec_nodes
[0] :
1254 NodeManager::currentNM()->mkNode(kind::REGEXP_UNION
, vec_nodes
);
1255 rNode
= Rewriter::rewrite( rNode
);
1257 //TODO: non-empty var set
1261 d_inter_cache
[p
] = rNode
;
1263 Trace("regexp-intersect") << "INTERSECT( " << mkString(r1
) << ", " << mkString(r2
) << " ) = " << mkString(rNode
) << std::endl
;
1266 Node
RegExpOpr::intersect(Node r1
, Node r2
, bool &spflag
) {
1267 std::map
< unsigned, std::set
< PairNodes
> > cache
;
1268 return intersectInternal(r1
, r2
, cache
, spflag
);
1271 Node
RegExpOpr::complement(Node r
, int &ret
) {
1274 if(d_compl_cache
.find(r
) != d_compl_cache
.end()) {
1275 rNode
= d_compl_cache
[r
].first
;
1276 ret
= d_compl_cache
[r
].second
;
1278 if(r
== d_emptyRegexp
) {
1279 rNode
= d_sigma_star
;
1280 } else if(r
== d_emptySingleton
) {
1281 rNode
= NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
, d_sigma
, d_sigma_star
);
1282 } else if(!checkConstRegExp(r
)) {
1283 //TODO: var to be extended
1286 std::set
<unsigned> cset
;
1288 firstChars(r
, cset
, vset
);
1289 std::vector
< Node
> vec_nodes
;
1290 for(unsigned i
=0; i
<d_card
; i
++) {
1291 CVC4::String c
= CVC4::String::convertUnsignedIntToChar(i
);
1292 Node n
= NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP
, NodeManager::currentNM()->mkConst(c
));
1294 if(cset
.find(i
) == cset
.end()) {
1298 derivativeS(r
, c
, r2
);
1302 r2
= complement(r2
, rt
);
1305 n
= Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
, n
, r2
));
1306 vec_nodes
.push_back(n
);
1308 rNode
= vec_nodes
.size()==0? d_emptyRegexp
: vec_nodes
.size()==1? vec_nodes
[0] :
1309 NodeManager::currentNM()->mkNode(kind::REGEXP_UNION
, vec_nodes
);
1311 rNode
= Rewriter::rewrite(rNode
);
1312 std::pair
< Node
, int > p(rNode
, ret
);
1313 d_compl_cache
[r
] = p
;
1315 Trace("regexp-compl") << "COMPL( " << mkString(r
) << " ) = " << mkString(rNode
) << ", ret=" << ret
<< std::endl
;
1319 void RegExpOpr::splitRegExp(Node r
, std::vector
< PairNodes
> &pset
) {
1320 Assert(checkConstRegExp(r
));
1321 if(d_split_cache
.find(r
) != d_split_cache
.end()) {
1322 pset
= d_split_cache
[r
];
1324 switch( r
.getKind() ) {
1325 case kind::REGEXP_EMPTY
: {
1328 case kind::REGEXP_OPT
: {
1329 PairNodes
tmp(d_emptySingleton
, d_emptySingleton
);
1330 pset
.push_back(tmp
);
1332 case kind::REGEXP_RANGE
:
1333 case kind::REGEXP_SIGMA
: {
1334 PairNodes
tmp1(d_emptySingleton
, r
);
1335 PairNodes
tmp2(r
, d_emptySingleton
);
1336 pset
.push_back(tmp1
);
1337 pset
.push_back(tmp2
);
1340 case kind::STRING_TO_REGEXP
: {
1341 Assert(r
[0].isConst());
1342 CVC4::String s
= r
[0].getConst
< CVC4::String
>();
1343 PairNodes
tmp1(d_emptySingleton
, r
);
1344 pset
.push_back(tmp1
);
1345 for(unsigned i
=1; i
<s
.size(); i
++) {
1346 CVC4::String s1
= s
.substr(0, i
);
1347 CVC4::String s2
= s
.substr(i
);
1348 Node n1
= NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP
, NodeManager::currentNM()->mkConst(s1
));
1349 Node n2
= NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP
, NodeManager::currentNM()->mkConst(s2
));
1350 PairNodes
tmp3(n1
, n2
);
1351 pset
.push_back(tmp3
);
1353 PairNodes
tmp2(r
, d_emptySingleton
);
1354 pset
.push_back(tmp2
);
1357 case kind::REGEXP_CONCAT
: {
1358 for(unsigned i
=0; i
<r
.getNumChildren(); i
++) {
1359 std::vector
< PairNodes
> tset
;
1360 splitRegExp(r
[i
], tset
);
1361 std::vector
< Node
> hvec
;
1362 std::vector
< Node
> tvec
;
1363 for(unsigned j
=0; j
<=i
; j
++) {
1364 hvec
.push_back(r
[j
]);
1366 for(unsigned j
=i
; j
<r
.getNumChildren(); j
++) {
1367 tvec
.push_back(r
[j
]);
1369 for(unsigned j
=0; j
<tset
.size(); j
++) {
1370 hvec
[i
] = tset
[j
].first
;
1371 tvec
[0] = tset
[j
].second
;
1372 Node r1
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
, hvec
) );
1373 Node r2
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
, tvec
) );
1374 PairNodes
tmp2(r1
, r2
);
1375 pset
.push_back(tmp2
);
1380 case kind::REGEXP_UNION
: {
1381 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
1382 std::vector
< PairNodes
> tset
;
1383 splitRegExp(r
[i
], tset
);
1384 pset
.insert(pset
.end(), tset
.begin(), tset
.end());
1388 case kind::REGEXP_INTER
: {
1389 bool spflag
= false;
1391 for(unsigned i
=1; i
<r
.getNumChildren(); i
++) {
1392 tmp
= intersect(tmp
, r
[i
], spflag
);
1394 splitRegExp(tmp
, pset
);
1397 case kind::REGEXP_STAR
: {
1398 std::vector
< PairNodes
> tset
;
1399 splitRegExp(r
[0], tset
);
1400 PairNodes
tmp1(d_emptySingleton
, d_emptySingleton
);
1401 pset
.push_back(tmp1
);
1402 for(unsigned i
=0; i
<tset
.size(); i
++) {
1403 Node r1
= tset
[i
].first
==d_emptySingleton
? r
: NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
, r
, tset
[i
].first
);
1404 Node r2
= tset
[i
].second
==d_emptySingleton
? r
: NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
, tset
[i
].second
, r
);
1405 PairNodes
tmp2(r1
, r2
);
1406 pset
.push_back(tmp2
);
1410 case kind::REGEXP_PLUS
: {
1411 std::vector
< PairNodes
> tset
;
1412 splitRegExp(r
[0], tset
);
1413 for(unsigned i
=0; i
<tset
.size(); i
++) {
1414 Node r1
= NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
, r
, tset
[i
].first
);
1415 Node r2
= NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
, tset
[i
].second
, r
);
1416 PairNodes
tmp2(r1
, r2
);
1417 pset
.push_back(tmp2
);
1422 Trace("strings-error") << "Unsupported term: " << r
<< " in splitRegExp." << std::endl
;
1424 //return Node::null();
1427 d_split_cache
[r
] = pset
;
1432 std::string
RegExpOpr::niceChar( Node r
) {
1434 std::string s
= r
.getConst
<CVC4::String
>().toString() ;
1435 return s
== "" ? "{E}" : ( s
== " " ? "{ }" : s
.size()>1? "("+s
+")" : s
);
1437 std::string ss
= "$" + r
.toString();
1441 std::string
RegExpOpr::mkString( Node r
) {
1446 int k
= r
.getKind();
1448 case kind::REGEXP_EMPTY
: {
1452 case kind::REGEXP_SIGMA
: {
1456 case kind::STRING_TO_REGEXP
: {
1457 retStr
+= niceChar( r
[0] );
1460 case kind::REGEXP_CONCAT
: {
1462 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
1463 //if(i != 0) retStr += ".";
1464 retStr
+= mkString( r
[i
] );
1469 case kind::REGEXP_UNION
: {
1474 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
1475 if(i
!= 0) retStr
+= "|";
1476 retStr
+= mkString( r
[i
] );
1482 case kind::REGEXP_INTER
: {
1484 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
1485 if(i
!= 0) retStr
+= "&";
1486 retStr
+= mkString( r
[i
] );
1491 case kind::REGEXP_STAR
: {
1492 retStr
+= mkString( r
[0] );
1496 case kind::REGEXP_PLUS
: {
1497 retStr
+= mkString( r
[0] );
1501 case kind::REGEXP_OPT
: {
1502 retStr
+= mkString( r
[0] );
1506 case kind::REGEXP_RANGE
: {
1508 retStr
+= niceChar( r
[0] );
1510 retStr
+= niceChar( r
[1] );
1515 Trace("strings-error") << "Unsupported term: " << r
<< " in RegExp." << std::endl
;
1517 //return Node::null();
1524 }/* CVC4::theory::strings namespace */
1525 }/* CVC4::theory namespace */
1526 }/* CVC4 namespace */