1 /********************* */
2 /*! \file regexp_operation.cpp
4 ** Original author: Tianyi Liang
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Regular Expresion Operations
14 ** Regular Expresion Operations
17 #include "theory/strings/regexp_operation.h"
18 #include "expr/kind.h"
24 RegExpOpr::RegExpOpr() {
25 d_emptyString
= NodeManager::currentNM()->mkConst( ::CVC4::String("") );
26 // All Charactors = all printable ones 32-126
27 d_char_start
= 'a';//' ';
28 d_char_end
= 'c';//'~';
29 d_sigma
= mkAllExceptOne( '\0' );
30 d_sigma_star
= NodeManager::currentNM()->mkNode( kind::REGEXP_STAR
, d_sigma
);
33 int RegExpOpr::gcd ( int a
, int b
) {
36 c
= a
; a
= b
%a
; b
= c
;
41 bool RegExpOpr::checkConstRegExp( Node r
) {
42 Trace("strings-regexp-cstre") << "RegExp-CheckConstRegExp starts with " << mkString( r
) << std::endl
;
44 if( d_cstre_cache
.find( r
) != d_cstre_cache
.end() ) {
45 ret
= d_cstre_cache
[r
];
47 if(r
.getKind() == kind::STRING_TO_REGEXP
) {
48 Node tmp
= Rewriter::rewrite( r
[0] );
51 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
52 if(!checkConstRegExp(r
[i
])) {
57 d_cstre_cache
[r
] = ret
;
62 // 0-unknown, 1-yes, 2-no
63 int RegExpOpr::delta( Node r
) {
64 Trace("strings-regexp-delta") << "RegExp-Delta starts with " << mkString( r
) << std::endl
;
66 if( d_delta_cache
.find( r
) != d_delta_cache
.end() ) {
67 ret
= d_delta_cache
[r
];
71 case kind::STRING_TO_REGEXP
:
74 if(r
[0] == d_emptyString
) {
84 case kind::REGEXP_CONCAT
:
87 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
88 int tmp
= delta( r
[i
] );
96 if(!flag
&& ret
!= 2) {
101 case kind::REGEXP_OR
:
104 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
105 int tmp
= delta( r
[i
] );
109 } else if(tmp
== 0) {
113 if(!flag
&& ret
!= 1) {
118 case kind::REGEXP_INTER
:
121 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
122 int tmp
= delta( r
[i
] );
126 } else if(tmp
== 0) {
136 case kind::REGEXP_STAR
:
141 case kind::REGEXP_PLUS
:
146 case kind::REGEXP_OPT
:
151 case kind::REGEXP_RANGE
:
157 //TODO: special sym: sigma, none, all
158 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in delta of RegExp." << std::endl
;
159 //AlwaysAssert( false );
160 //return Node::null();
162 d_delta_cache
[r
] = ret
;
164 Trace("strings-regexp-delta") << "RegExp-Delta returns : " << ret
<< std::endl
;
169 Node
RegExpOpr::derivativeSingle( Node r
, CVC4::String c
) {
170 Assert( c
.size() < 2 );
171 Trace("strings-regexp-derivative") << "RegExp-derivative starts with R{ " << mkString( r
) << " }, c=" << c
<< std::endl
;
172 Node retNode
= Node::null();
173 PairDvStr dv
= std::make_pair( r
, c
);
174 if( d_dv_cache
.find( dv
) != d_dv_cache
.end() ) {
175 retNode
= d_dv_cache
[dv
];
176 } else if( c
.isEmptyString() ){
177 int tmp
= delta( r
);
179 retNode
= Node::null();
181 } else if(tmp
== 1) {
184 retNode
= Node::null();
189 case kind::STRING_TO_REGEXP
:
192 if(r
[0] == d_emptyString
) {
193 retNode
= Node::null();
195 if(r
[0].getConst
< CVC4::String
>().getFirstChar() == c
.getFirstChar()) {
196 retNode
= r
[0].getConst
< CVC4::String
>().size() == 1 ? d_emptyString
: NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
,
197 NodeManager::currentNM()->mkConst( r
[0].getConst
< CVC4::String
>().substr(1) ) );
199 retNode
= Node::null();
203 retNode
= Node::null();
208 case kind::REGEXP_CONCAT
:
210 std::vector
< Node
> vec_nodes
;
211 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
212 Node dc
= derivativeSingle(r
[i
], c
);
214 std::vector
< Node
> vec_nodes2
;
215 if(dc
!= d_emptyString
) {
216 vec_nodes2
.push_back( dc
);
218 for(unsigned j
=i
+1; j
<r
.getNumChildren(); ++j
) {
219 if(r
[j
] != d_emptyString
) {
220 vec_nodes2
.push_back( r
[j
] );
223 Node tmp
= vec_nodes2
.size()==0 ? d_emptyString
:
224 ( vec_nodes2
.size()==1 ? vec_nodes2
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, vec_nodes2
) );
225 if(std::find(vec_nodes
.begin(), vec_nodes
.end(), tmp
) == vec_nodes
.end()) {
226 vec_nodes
.push_back( tmp
);
230 if( delta( r
[i
] ) != 1 ) {
234 retNode
= vec_nodes
.size() == 0 ? Node::null() :
235 ( vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_OR
, vec_nodes
) );
238 case kind::REGEXP_OR
:
240 std::vector
< Node
> vec_nodes
;
241 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
242 Node dc
= derivativeSingle(r
[i
], c
);
244 if(std::find(vec_nodes
.begin(), vec_nodes
.end(), dc
) == vec_nodes
.end()) {
245 vec_nodes
.push_back( dc
);
248 Trace("strings-regexp-derivative") << "RegExp-derivative OR R[" << i
<< "]{ " << mkString(r
[i
]) << " returns " << mkString(dc
) << std::endl
;
250 retNode
= vec_nodes
.size() == 0 ? Node::null() :
251 ( vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_OR
, vec_nodes
) );
254 case kind::REGEXP_INTER
:
257 bool flag_sg
= false;
258 std::vector
< Node
> vec_nodes
;
259 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
260 Node dc
= derivativeSingle(r
[i
], c
);
262 if(dc
== d_sigma_star
) {
265 if(std::find(vec_nodes
.begin(), vec_nodes
.end(), dc
) == vec_nodes
.end()) {
266 vec_nodes
.push_back( dc
);
275 if(vec_nodes
.size() == 0 && flag_sg
) {
276 retNode
= d_sigma_star
;
278 retNode
= vec_nodes
.size() == 0 ? Node::null() :
279 ( vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_INTER
, vec_nodes
) );
282 retNode
= Node::null();
286 case kind::REGEXP_STAR
:
288 Node dc
= derivativeSingle(r
[0], c
);
290 retNode
= dc
==d_emptyString
? r
: NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, dc
, r
);
292 retNode
= Node::null();
296 case kind::REGEXP_PLUS
:
298 Node dc
= derivativeSingle(r
[0], c
);
300 retNode
= dc
==d_emptyString
? r
: NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, dc
, r
);
302 retNode
= Node::null();
306 case kind::REGEXP_OPT
:
308 retNode
= derivativeSingle(r
[0], c
);
311 case kind::REGEXP_RANGE
:
313 char ch
= c
.getFirstChar();
314 if (ch
>= r
[0].getConst
< CVC4::String
>().getFirstChar() && ch
<= r
[1].getConst
< CVC4::String
>().getFirstChar() ) {
315 retNode
= d_emptyString
;
317 retNode
= Node::null();
322 //TODO: special sym: sigma, none, all
323 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in derivative of RegExp." << std::endl
;
324 //AlwaysAssert( false );
325 //return Node::null();
327 if(!retNode
.isNull()) {
328 retNode
= Rewriter::rewrite( retNode
);
330 d_dv_cache
[dv
] = retNode
;
332 Trace("strings-regexp-derivative") << "RegExp-derivative returns : " << mkString( retNode
) << std::endl
;
337 bool RegExpOpr::guessLength( Node r
, int &co
) {
340 case kind::STRING_TO_REGEXP
:
343 co
+= r
[0].getConst
< CVC4::String
>().size();
350 case kind::REGEXP_CONCAT
:
352 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
353 if(!guessLength( r
[i
], co
)) {
360 case kind::REGEXP_OR
:
363 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
365 if(!guessLength( r
[i
], cop
)) {
371 g_co
= gcd(g_co
, cop
);
377 case kind::REGEXP_INTER
:
380 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
382 if(!guessLength( r
[i
], cop
)) {
388 g_co
= gcd(g_co
, cop
);
394 case kind::REGEXP_STAR
:
401 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in membership of RegExp." << std::endl
;
406 void RegExpOpr::firstChar( Node r
) {
407 Trace("strings-regexp-firstchar") << "Head characters: ";
408 for(char ch
= d_char_start
; ch
<= d_char_end
; ++ch
) {
410 Node dc
= derivativeSingle(r
, ch
);
412 Trace("strings-regexp-firstchar") << c
<< " (" << mkString(dc
) << ")" << std::endl
;
415 Trace("strings-regexp-firstchar") << std::endl
;
418 bool RegExpOpr::follow( Node r
, CVC4::String c
, std::vector
< char > &vec_chars
) {
421 case kind::STRING_TO_REGEXP
:
424 if(r
[0] != d_emptyString
) {
425 char t1
= r
[0].getConst
< CVC4::String
>().getFirstChar();
426 if(c
.isEmptyString()) {
427 vec_chars
.push_back( t1
);
430 char t2
= c
.getFirstChar();
435 vec_chars
.push_back( c
.substr(1,1).getFirstChar() );
437 vec_chars
.push_back( '\0' );
450 case kind::REGEXP_CONCAT
:
452 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
453 if( follow(r
[i
], c
, vec_chars
) ) {
454 if(vec_chars
[vec_chars
.size() - 1] == '\0') {
455 vec_chars
.pop_back();
456 c
= d_emptyString
.getConst
< CVC4::String
>();
462 vec_chars
.push_back( '\0' );
466 case kind::REGEXP_OR
:
469 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
470 if( follow(r
[i
], c
, vec_chars
) ) {
477 case kind::REGEXP_INTER
:
479 std::vector
< char > vt2
;
480 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
481 std::vector
< char > v_tmp
;
482 if( !follow(r
[i
], c
, v_tmp
) ) {
485 std::vector
< char > vt3(vt2
);
487 std::set_intersection( vt3
.begin(), vt3
.end(), v_tmp
.begin(), v_tmp
.end(), vt2
.begin() );
488 if(vt2
.size() == 0) {
492 vec_chars
.insert( vec_chars
.end(), vt2
.begin(), vt2
.end() );
496 case kind::REGEXP_STAR
:
498 if(follow(r
[0], c
, vec_chars
)) {
499 if(vec_chars
[vec_chars
.size() - 1] == '\0') {
500 if(c
.isEmptyString()) {
503 vec_chars
.pop_back();
504 c
= d_emptyString
.getConst
< CVC4::String
>();
505 return follow(r
[0], c
, vec_chars
);
511 vec_chars
.push_back( '\0' );
517 case kind::REGEXP_PLUS:
522 case kind::REGEXP_OPT:
527 case kind::REGEXP_RANGE:
533 //TODO: special sym: sigma, none, all
534 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in delta of RegExp." << std::endl
;
535 //AlwaysAssert( false );
536 //return Node::null();
541 Node
RegExpOpr::mkAllExceptOne( char exp_c
) {
542 std::vector
< Node
> vec_nodes
;
543 for(char c
=d_char_start
; c
<=d_char_end
; ++c
) {
545 Node n
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, NodeManager::currentNM()->mkConst( ::CVC4::String( c
) ) );
546 vec_nodes
.push_back( n
);
549 return NodeManager::currentNM()->mkNode( kind::REGEXP_OR
, vec_nodes
);
552 Node
RegExpOpr::complement( Node r
) {
553 Trace("strings-regexp-compl") << "RegExp-Compl starts with " << mkString( r
) << std::endl
;
555 if( d_compl_cache
.find( r
) != d_compl_cache
.end() ) {
556 retNode
= d_compl_cache
[r
];
560 case kind::STRING_TO_REGEXP
:
563 if(r
[0] == d_emptyString
) {
564 retNode
= NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, d_sigma
, d_sigma_star
);
566 std::vector
< Node
> vec_nodes
;
567 vec_nodes
.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, d_emptyString
) );
568 CVC4::String s
= r
[0].getConst
<String
>();
569 for(unsigned i
=0; i
<s
.size(); ++i
) {
570 char c
= s
.substr(i
, 1).getFirstChar();
571 Node tmp
= mkAllExceptOne( c
);
573 Node tmph
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
,
574 NodeManager::currentNM()->mkConst( s
.substr(0, i
) ) );
575 tmp
= NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, tmph
, tmp
);
577 tmp
= NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, tmp
, d_sigma_star
);
578 vec_nodes
.push_back( tmp
);
580 Node tmp
= NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, r
, d_sigma
, d_sigma_star
);
581 vec_nodes
.push_back( tmp
);
582 retNode
= NodeManager::currentNM()->mkNode( kind::REGEXP_OR
, vec_nodes
);
585 Trace("strings-error") << "Unsupported string variable: " << r
[0] << " in complement of RegExp." << std::endl
;
586 //AlwaysAssert( false );
587 //return Node::null();
591 case kind::REGEXP_CONCAT
:
593 std::vector
< Node
> vec_nodes
;
594 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
595 Node tmp
= complement( r
[i
] );
596 for(unsigned j
=0; j
<i
; ++j
) {
597 tmp
= NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, r
[j
], tmp
);
599 if(i
!= r
.getNumChildren() - 1) {
600 tmp
= NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, tmp
,
601 NodeManager::currentNM()->mkNode( kind::REGEXP_STAR
, d_sigma
) );
603 vec_nodes
.push_back( tmp
);
605 retNode
= NodeManager::currentNM()->mkNode( kind::REGEXP_OR
, vec_nodes
);
608 case kind::REGEXP_OR
:
610 std::vector
< Node
> vec_nodes
;
611 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
612 Node tmp
= complement( r
[i
] );
613 vec_nodes
.push_back( tmp
);
615 retNode
= NodeManager::currentNM()->mkNode( kind::REGEXP_INTER
, vec_nodes
);
618 case kind::REGEXP_INTER
:
620 std::vector
< Node
> vec_nodes
;
621 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
622 Node tmp
= complement( r
[i
] );
623 vec_nodes
.push_back( tmp
);
625 retNode
= NodeManager::currentNM()->mkNode( kind::REGEXP_OR
, vec_nodes
);
628 case kind::REGEXP_STAR
:
630 retNode
= NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, d_sigma
, d_sigma_star
);
631 Node tmp
= complement( r
[0] );
632 tmp
= NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, r
, tmp
);
633 retNode
= NodeManager::currentNM()->mkNode( kind::REGEXP_INTER
, retNode
, tmp
);
637 //TODO: special sym: sigma, none, all
638 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in complement of RegExp." << std::endl
;
639 //AlwaysAssert( false );
640 //return Node::null();
642 d_compl_cache
[r
] = retNode
;
644 Trace("strings-regexp-compl") << "RegExp-Compl returns : " << mkString( retNode
) << std::endl
;
649 void RegExpOpr::simplify(Node t
, std::vector
< Node
> &new_nodes
) {
650 Assert(t
.getKind() == kind::STRING_IN_REGEXP
);
651 Node str
= Rewriter::rewrite(t
[0]);
652 Node re
= Rewriter::rewrite(t
[1]);
653 simplifyRegExp( str
, re
, new_nodes
);
655 void RegExpOpr::simplifyRegExp( Node s
, Node r
, std::vector
< Node
> &new_nodes
) {
656 std::pair
< Node
, Node
> p(s
, r
);
657 std::map
< std::pair
< Node
, Node
>, Node
>::const_iterator itr
= d_simpl_cache
.find(p
);
658 if(itr
!= d_simpl_cache
.end()) {
659 new_nodes
.push_back( itr
->second
);
664 case kind::STRING_TO_REGEXP
:
666 Node eq
= NodeManager::currentNM()->mkNode( kind::EQUAL
, s
, r
[0] );
667 new_nodes
.push_back( eq
);
668 d_simpl_cache
[p
] = eq
;
671 case kind::REGEXP_CONCAT
:
673 std::vector
< Node
> cc
;
674 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
675 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
676 cc
.push_back( r
[i
][0] );
678 Node sk
= NodeManager::currentNM()->mkSkolem( "rcon_$$", s
.getType(), "created for regular expression concat" );
679 simplifyRegExp( sk
, r
[i
], new_nodes
);
683 Node cc_eq
= s
.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
, cc
) );
684 new_nodes
.push_back( cc_eq
);
685 d_simpl_cache
[p
] = cc_eq
;
688 case kind::REGEXP_OR
:
690 std::vector
< Node
> c_or
;
691 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
692 simplifyRegExp( s
, r
[i
], c_or
);
694 Node eq
= NodeManager::currentNM()->mkNode( kind::OR
, c_or
);
695 new_nodes
.push_back( eq
);
696 d_simpl_cache
[p
] = eq
;
699 case kind::REGEXP_INTER
:
700 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
701 simplifyRegExp( s
, r
[i
], new_nodes
);
704 case kind::REGEXP_STAR
:
706 Node eq
= NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP
, s
, r
);
707 new_nodes
.push_back( eq
);
708 d_simpl_cache
[p
] = eq
;
712 //TODO: special sym: sigma, none, all
713 Trace("strings-preprocess") << "Unsupported term: " << r
<< " in simplifyRegExp." << std::endl
;
721 std::string
RegExpOpr::niceChar( Node r
) {
723 std::string s
= r
.getConst
<CVC4::String
>().toString() ;
724 return s
== "" ? "{E}" : ( s
== " " ? "{ }" : s
);
729 std::string
RegExpOpr::mkString( Node r
) {
736 case kind::STRING_TO_REGEXP
:
738 retStr
+= niceChar( r
[0] );
741 case kind::REGEXP_CONCAT
:
744 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
745 if(i
!= 0) retStr
+= ".";
746 retStr
+= mkString( r
[i
] );
751 case kind::REGEXP_OR
:
757 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
758 if(i
!= 0) retStr
+= "|";
759 retStr
+= mkString( r
[i
] );
765 case kind::REGEXP_INTER
:
768 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
769 if(i
!= 0) retStr
+= "&";
770 retStr
+= mkString( r
[i
] );
775 case kind::REGEXP_STAR
:
777 retStr
+= mkString( r
[0] );
781 case kind::REGEXP_PLUS
:
783 retStr
+= mkString( r
[0] );
787 case kind::REGEXP_OPT
:
789 retStr
+= mkString( r
[0] );
793 case kind::REGEXP_RANGE
:
796 retStr
+= niceChar( r
[0] );
798 retStr
+= niceChar( r
[1] );
803 //TODO: special sym: sigma, none, all
804 Trace("strings-error") << "Unsupported term: " << r
<< " in RegExp." << std::endl
;
805 //AlwaysAssert( false );
806 //return Node::null();
813 }/* CVC4::theory::strings namespace */
814 }/* CVC4::theory namespace */
815 }/* CVC4 namespace */