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
) {
84 Trace("strings-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
];
91 case kind::REGEXP_EMPTY
: {
95 case kind::REGEXP_SIGMA
: {
99 case kind::STRING_TO_REGEXP
: {
101 if(r
[0] == d_emptyString
) {
111 case kind::REGEXP_CONCAT
: {
113 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
114 int tmp
= delta( r
[i
] );
118 } else if(tmp
== 0) {
122 if(!flag
&& ret
!= 2) {
127 case kind::REGEXP_UNION
: {
129 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
130 int tmp
= delta( r
[i
] );
134 } else if(tmp
== 0) {
138 if(!flag
&& ret
!= 1) {
143 case kind::REGEXP_INTER
: {
145 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
146 int tmp
= delta( r
[i
] );
150 } else if(tmp
== 0) {
160 case kind::REGEXP_STAR
: {
164 case kind::REGEXP_PLUS
: {
168 case kind::REGEXP_OPT
: {
172 case kind::REGEXP_RANGE
: {
177 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in delta of RegExp." << std::endl
;
179 //return Node::null();
182 d_delta_cache
[r
] = ret
;
184 Trace("strings-regexp-delta") << "RegExp-Delta returns : " << ret
<< std::endl
;
188 Node
RegExpOpr::derivativeSingle( Node r
, CVC4::String c
) {
189 Assert( c
.size() < 2 );
190 Trace("regexp-deriv") << "RegExp-deriv starts with R{ " << mkString( r
) << " }, c=" << c
<< std::endl
;
191 Node retNode
= d_emptyRegexp
;
192 PairDvStr dv
= std::make_pair( r
, c
);
193 if( d_dv_cache
.find( dv
) != d_dv_cache
.end() ) {
194 retNode
= d_dv_cache
[dv
];
195 } else if( c
.isEmptyString() ){
196 int tmp
= delta( r
);
199 retNode
= d_emptyRegexp
;
200 } else if(tmp
== 1) {
203 retNode
= d_emptyRegexp
;
208 case kind::REGEXP_EMPTY
: {
209 retNode
= d_emptyRegexp
;
212 case kind::REGEXP_SIGMA
: {
213 retNode
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, d_emptyString
);
216 case kind::STRING_TO_REGEXP
: {
218 if(r
[0] == d_emptyString
) {
219 retNode
= d_emptyRegexp
;
221 if(r
[0].getConst
< CVC4::String
>().getFirstChar() == c
.getFirstChar()) {
222 retNode
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
,
223 r
[0].getConst
< CVC4::String
>().size() == 1 ? d_emptyString
: NodeManager::currentNM()->mkConst( r
[0].getConst
< CVC4::String
>().substr(1) ) );
225 retNode
= d_emptyRegexp
;
230 retNode
= d_emptyRegexp
;
234 case kind::REGEXP_CONCAT
: {
235 Node rees
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, d_emptyString
);
236 std::vector
< Node
> vec_nodes
;
237 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
238 Node dc
= derivativeSingle(r
[i
], c
);
239 if(dc
!= d_emptyRegexp
) {
240 std::vector
< Node
> vec_nodes2
;
242 vec_nodes2
.push_back( dc
);
244 for(unsigned j
=i
+1; j
<r
.getNumChildren(); ++j
) {
246 vec_nodes2
.push_back( r
[j
] );
249 Node tmp
= vec_nodes2
.size()==0 ? rees
:
250 vec_nodes2
.size()==1 ? vec_nodes2
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, vec_nodes2
);
251 if(std::find(vec_nodes
.begin(), vec_nodes
.end(), tmp
) == vec_nodes
.end()) {
252 vec_nodes
.push_back( tmp
);
256 if( delta( r
[i
] ) != 1 ) {
260 retNode
= vec_nodes
.size() == 0 ? d_emptyRegexp
:
261 ( vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_UNION
, vec_nodes
) );
264 case kind::REGEXP_UNION
: {
265 std::vector
< Node
> vec_nodes
;
266 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
267 Node dc
= derivativeSingle(r
[i
], c
);
268 if(dc
!= d_emptyRegexp
) {
269 if(std::find(vec_nodes
.begin(), vec_nodes
.end(), dc
) == vec_nodes
.end()) {
270 vec_nodes
.push_back( dc
);
273 Trace("regexp-deriv") << "RegExp-deriv OR R[" << i
<< "]{ " << mkString(r
[i
]) << " returns " << mkString(dc
) << std::endl
;
275 retNode
= vec_nodes
.size() == 0 ? d_emptyRegexp
:
276 ( vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_UNION
, vec_nodes
) );
279 case kind::REGEXP_INTER
: {
281 bool flag_sg
= false;
282 std::vector
< Node
> vec_nodes
;
283 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
284 Node dc
= derivativeSingle(r
[i
], c
);
285 if(dc
!= d_emptyRegexp
) {
286 if(dc
== d_sigma_star
) {
289 if(std::find(vec_nodes
.begin(), vec_nodes
.end(), dc
) == vec_nodes
.end()) {
290 vec_nodes
.push_back( dc
);
299 if(vec_nodes
.size() == 0 && flag_sg
) {
300 retNode
= d_sigma_star
;
302 retNode
= vec_nodes
.size() == 0 ? d_emptyRegexp
:
303 ( vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_INTER
, vec_nodes
) );
306 retNode
= d_emptyRegexp
;
310 case kind::REGEXP_STAR
: {
311 Node dc
= derivativeSingle(r
[0], c
);
312 if(dc
!= d_emptyRegexp
) {
313 retNode
= dc
==NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, d_emptyString
) ? r
: NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, dc
, r
);
315 retNode
= d_emptyRegexp
;
320 //TODO: special sym: sigma, none, all
321 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in derivative of RegExp." << std::endl
;
322 Assert( false, "Unsupported Term" );
323 //return Node::null();
326 if(retNode
!= d_emptyRegexp
) {
327 retNode
= Rewriter::rewrite( retNode
);
329 d_dv_cache
[dv
] = retNode
;
331 Trace("regexp-deriv") << "RegExp-deriv returns : " << mkString( retNode
) << std::endl
;
336 bool RegExpOpr::guessLength( Node r
, int &co
) {
339 case kind::STRING_TO_REGEXP
:
342 co
+= r
[0].getConst
< CVC4::String
>().size();
349 case kind::REGEXP_CONCAT
:
351 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
352 if(!guessLength( r
[i
], co
)) {
359 case kind::REGEXP_UNION
:
362 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
364 if(!guessLength( r
[i
], cop
)) {
370 g_co
= gcd(g_co
, cop
);
376 case kind::REGEXP_INTER
:
379 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
381 if(!guessLength( r
[i
], cop
)) {
387 g_co
= gcd(g_co
, cop
);
393 case kind::REGEXP_STAR
:
400 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in membership of RegExp." << std::endl
;
405 void RegExpOpr::firstChars( Node r
, std::set
<unsigned> &pcset
, SetNodes
&pvset
) {
406 std::map
< Node
, std::pair
< std::set
<unsigned>, SetNodes
> >::const_iterator itr
= d_fset_cache
.find(r
);
407 if(itr
!= d_fset_cache
.end()) {
408 pcset
.insert((itr
->second
).first
.begin(), (itr
->second
).first
.end());
409 pvset
.insert((itr
->second
).second
.begin(), (itr
->second
).second
.end());
411 std::set
<unsigned> cset
;
415 case kind::REGEXP_EMPTY
: {
418 case kind::REGEXP_SIGMA
: {
419 for(unsigned i
=0; i
<d_card
; i
++) {
424 case kind::STRING_TO_REGEXP
: {
425 Node st
= Rewriter::rewrite(r
[0]);
427 CVC4::String s
= st
.getConst
< CVC4::String
>();
431 } else if(st
.getKind() == kind::VARIABLE
) {
434 if(st
[0].isConst()) {
435 CVC4::String s
= st
[0].getConst
< CVC4::String
>();
438 vset
.insert( st
[0] );
443 case kind::REGEXP_CONCAT
: {
444 for(unsigned i
=0; i
<r
.getNumChildren(); i
++) {
445 firstChars(r
[i
], cset
, vset
);
454 case kind::REGEXP_UNION
: {
455 for(unsigned i
=0; i
<r
.getNumChildren(); i
++) {
456 firstChars(r
[i
], cset
, vset
);
460 case kind::REGEXP_INTER
: {
461 //TODO: Overapproximation for now
462 for(unsigned i
=0; i
<r
.getNumChildren(); i
++) {
463 firstChars(r
[i
], cset
, vset
);
467 case kind::REGEXP_STAR
: {
468 firstChars(r
[0], cset
, vset
);
472 Trace("strings-regexp") << "Unsupported term: " << r
<< " in getCharSet." << std::endl
;
473 Assert( false, "Unsupported Term" );
476 pcset
.insert(cset
.begin(), cset
.end());
477 pvset
.insert(vset
.begin(), vset
.end());
478 std::pair
< std::set
<unsigned>, SetNodes
> p(cset
, vset
);
481 Trace("regexp-fset") << "FSET( " << mkString(r
) << " ) = { ";
482 for(std::set
<unsigned>::const_iterator itr
= cset
.begin();
483 itr
!= cset
.end(); itr
++) {
484 Trace("regexp-fset") << CVC4::String::convertUnsignedIntToChar(*itr
) << ",";
486 Trace("regexp-fset") << " }" << std::endl
;
490 bool RegExpOpr::follow( Node r
, CVC4::String c
, std::vector
< char > &vec_chars
) {
493 case kind::STRING_TO_REGEXP
:
496 if(r
[0] != d_emptyString
) {
497 char t1
= r
[0].getConst
< CVC4::String
>().getFirstChar();
498 if(c
.isEmptyString()) {
499 vec_chars
.push_back( t1
);
502 char t2
= c
.getFirstChar();
507 vec_chars
.push_back( c
.substr(1,1).getFirstChar() );
509 vec_chars
.push_back( '\0' );
522 case kind::REGEXP_CONCAT
:
524 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
525 if( follow(r
[i
], c
, vec_chars
) ) {
526 if(vec_chars
[vec_chars
.size() - 1] == '\0') {
527 vec_chars
.pop_back();
528 c
= d_emptyString
.getConst
< CVC4::String
>();
534 vec_chars
.push_back( '\0' );
538 case kind::REGEXP_UNION
:
541 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
542 if( follow(r
[i
], c
, vec_chars
) ) {
549 case kind::REGEXP_INTER
:
551 std::vector
< char > vt2
;
552 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
553 std::vector
< char > v_tmp
;
554 if( !follow(r
[i
], c
, v_tmp
) ) {
557 std::vector
< char > vt3(vt2
);
559 std::set_intersection( vt3
.begin(), vt3
.end(), v_tmp
.begin(), v_tmp
.end(), vt2
.begin() );
560 if(vt2
.size() == 0) {
564 vec_chars
.insert( vec_chars
.end(), vt2
.begin(), vt2
.end() );
568 case kind::REGEXP_STAR
:
570 if(follow(r
[0], c
, vec_chars
)) {
571 if(vec_chars
[vec_chars
.size() - 1] == '\0') {
572 if(c
.isEmptyString()) {
575 vec_chars
.pop_back();
576 c
= d_emptyString
.getConst
< CVC4::String
>();
577 return follow(r
[0], c
, vec_chars
);
583 vec_chars
.push_back( '\0' );
589 case kind::REGEXP_PLUS:
594 case kind::REGEXP_OPT:
599 case kind::REGEXP_RANGE:
605 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in delta of RegExp." << std::endl
;
606 //AlwaysAssert( false );
607 //return Node::null();
613 Node
RegExpOpr::mkAllExceptOne( char exp_c
) {
614 std::vector
< Node
> vec_nodes
;
615 for(char c
=d_char_start
; c
<=d_char_end
; ++c
) {
617 Node n
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, NodeManager::currentNM()->mkConst( ::CVC4::String( c
) ) );
618 vec_nodes
.push_back( n
);
621 return NodeManager::currentNM()->mkNode( kind::REGEXP_UNION
, vec_nodes
);
625 void RegExpOpr::simplify(Node t
, std::vector
< Node
> &new_nodes
, bool polarity
) {
626 Trace("strings-regexp-simpl") << "RegExp-Simpl starts with " << t
<< ", polarity=" << polarity
<< std::endl
;
627 Assert(t
.getKind() == kind::STRING_IN_REGEXP
);
628 Node str
= Rewriter::rewrite(t
[0]);
629 Node re
= Rewriter::rewrite(t
[1]);
631 simplifyPRegExp( str
, re
, new_nodes
);
633 simplifyNRegExp( str
, re
, new_nodes
);
635 Trace("strings-regexp-simpl") << "RegExp-Simpl returns (" << new_nodes
.size() << "):\n";
636 for(unsigned i
=0; i
<new_nodes
.size(); i
++) {
637 Trace("strings-regexp-simpl") << "\t" << new_nodes
[i
] << std::endl
;
640 void RegExpOpr::simplifyNRegExp( Node s
, Node r
, std::vector
< Node
> &new_nodes
) {
641 std::pair
< Node
, Node
> p(s
, r
);
642 std::map
< std::pair
< Node
, Node
>, Node
>::const_iterator itr
= d_simpl_neg_cache
.find(p
);
643 if(itr
!= d_simpl_neg_cache
.end()) {
644 new_nodes
.push_back( itr
->second
);
649 case kind::REGEXP_EMPTY
: {
653 case kind::REGEXP_SIGMA
: {
654 conc
= d_one
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
)).negate();
657 case kind::STRING_TO_REGEXP
: {
658 conc
= s
.eqNode(r
[0]).negate();
661 case kind::REGEXP_CONCAT
: {
662 //TODO: rewrite empty
663 Node b1
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
664 Node b1v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, b1
);
665 Node g1
= NodeManager::currentNM()->mkNode( kind::AND
, NodeManager::currentNM()->mkNode(kind::GEQ
, b1
, d_zero
),
666 NodeManager::currentNM()->mkNode( kind::GEQ
, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
), b1
) );
667 Node s1
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
668 Node s2
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
669 Node b2v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, s1
, s2
);
670 Node s12
= s
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
, s1
, s2
));
671 Node s1len
= b1
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s1
));
672 Node s1r1
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s1
, r
[0]).negate();
673 if(r
[0].getKind() == kind::STRING_TO_REGEXP
) {
674 s1r1
= s1
.eqNode(r
[0][0]).negate();
675 } else if(r
[0].getKind() == kind::REGEXP_EMPTY
) {
679 if(r
.getNumChildren() > 2) {
680 std::vector
< Node
> nvec
;
681 for(unsigned i
=1; i
<r
.getNumChildren(); i
++) {
682 nvec
.push_back( r
[i
] );
684 r2
= NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
, nvec
);
686 r2
= Rewriter::rewrite(r2
);
687 Node s2r2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s2
, r2
).negate();
688 if(r2
.getKind() == kind::STRING_TO_REGEXP
) {
689 s2r2
= s2
.eqNode(r2
[0]).negate();
690 } else if(r2
.getKind() == kind::REGEXP_EMPTY
) {
694 conc
= NodeManager::currentNM()->mkNode(kind::OR
, s1r1
, s2r2
);
695 conc
= NodeManager::currentNM()->mkNode(kind::AND
, s12
, s1len
, conc
);
696 conc
= NodeManager::currentNM()->mkNode(kind::EXISTS
, b2v
, conc
);
697 conc
= NodeManager::currentNM()->mkNode(kind::IMPLIES
, g1
, conc
);
698 conc
= NodeManager::currentNM()->mkNode(kind::FORALL
, b1v
, conc
);
701 case kind::REGEXP_UNION
: {
702 std::vector
< Node
> c_and
;
703 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
704 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
705 c_and
.push_back( r
[i
][0].eqNode(s
).negate() );
706 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
709 c_and
.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[i
]).negate());
712 conc
= c_and
.size() == 0 ? d_true
:
713 c_and
.size() == 1 ? c_and
[0] : NodeManager::currentNM()->mkNode(kind::AND
, c_and
);
716 case kind::REGEXP_INTER
: {
717 bool emptyflag
= false;
718 std::vector
< Node
> c_or
;
719 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
720 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
721 c_or
.push_back( r
[i
][0].eqNode(s
).negate() );
722 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
726 c_or
.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[i
]).negate());
732 conc
= c_or
.size() == 1 ? c_or
[0] : NodeManager::currentNM()->mkNode(kind::OR
, c_or
);
736 case kind::REGEXP_STAR
: {
737 if(s
== d_emptyString
) {
739 } else if(r
[0].getKind() == kind::REGEXP_EMPTY
) {
740 conc
= s
.eqNode(d_emptyString
).negate();
741 } else if(r
[0].getKind() == kind::REGEXP_SIGMA
) {
744 Node lens
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
);
745 Node sne
= s
.eqNode(d_emptyString
).negate();
746 Node b1
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
747 Node b1v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, b1
);
748 Node g1
= NodeManager::currentNM()->mkNode( kind::AND
, NodeManager::currentNM()->mkNode(kind::GEQ
, b1
, d_one
),
749 NodeManager::currentNM()->mkNode( kind::GEQ
, lens
, b1
) );
751 Node s1
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL
, s
, d_zero
, b1
);
752 Node s2
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL
, s
, b1
, NodeManager::currentNM()->mkNode(kind::MINUS
, lens
, b1
));
753 Node s1r1
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s1
, r
[0]).negate();
754 Node s2r2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s2
, r
).negate();
756 conc
= NodeManager::currentNM()->mkNode(kind::OR
, s1r1
, s2r2
);
757 conc
= NodeManager::currentNM()->mkNode(kind::IMPLIES
, g1
, conc
);
758 conc
= NodeManager::currentNM()->mkNode(kind::FORALL
, b1v
, conc
);
759 conc
= NodeManager::currentNM()->mkNode(kind::AND
, sne
, conc
);
764 Trace("strings-regexp") << "Unsupported term: " << r
<< " in simplifyNRegExp." << std::endl
;
765 Assert( false, "Unsupported Term" );
768 conc
= Rewriter::rewrite( conc
);
769 new_nodes
.push_back( conc
);
770 d_simpl_neg_cache
[p
] = conc
;
773 void RegExpOpr::simplifyPRegExp( Node s
, Node r
, std::vector
< Node
> &new_nodes
) {
774 std::pair
< Node
, Node
> p(s
, r
);
775 std::map
< std::pair
< Node
, Node
>, Node
>::const_iterator itr
= d_simpl_cache
.find(p
);
776 if(itr
!= d_simpl_cache
.end()) {
777 new_nodes
.push_back( itr
->second
);
782 case kind::REGEXP_EMPTY
: {
786 case kind::REGEXP_SIGMA
: {
787 conc
= d_one
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
));
790 case kind::STRING_TO_REGEXP
: {
791 conc
= s
.eqNode(r
[0]);
794 case kind::REGEXP_CONCAT
: {
795 std::vector
< Node
> nvec
;
796 std::vector
< Node
> cc
;
797 bool emptyflag
= false;
798 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
799 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
800 cc
.push_back( r
[i
][0] );
801 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
805 Node sk
= NodeManager::currentNM()->mkSkolem( "rc_$$", s
.getType(), "created for regular expression concat" );
806 Node lem
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, sk
, r
[i
]);
814 Node lem
= s
.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
, cc
) );
816 conc
= nvec
.size() == 1 ? nvec
[0] : NodeManager::currentNM()->mkNode(kind::AND
, nvec
);
820 case kind::REGEXP_UNION
: {
821 std::vector
< Node
> c_or
;
822 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
823 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
824 c_or
.push_back( r
[i
][0].eqNode(s
) );
825 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
828 c_or
.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[i
]));
831 conc
= c_or
.size() == 0 ? d_false
:
832 c_or
.size() == 1 ? c_or
[0] : NodeManager::currentNM()->mkNode(kind::OR
, c_or
);
835 case kind::REGEXP_INTER
: {
836 std::vector
< Node
> c_and
;
837 bool emptyflag
= false;
838 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
839 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
840 c_and
.push_back( r
[i
][0].eqNode(s
) );
841 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
845 c_and
.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[i
]));
851 conc
= c_and
.size() == 1 ? c_and
[0] : NodeManager::currentNM()->mkNode(kind::AND
, c_and
);
855 case kind::REGEXP_STAR
: {
856 if(s
== d_emptyString
) {
858 } else if(r
[0].getKind() == kind::REGEXP_EMPTY
) {
859 conc
= s
.eqNode(d_emptyString
);
860 } else if(r
[0].getKind() == kind::REGEXP_SIGMA
) {
863 Node se
= s
.eqNode(d_emptyString
);
864 Node sinr
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[0]);
865 Node sk1
= NodeManager::currentNM()->mkSkolem( "rs_$$", s
.getType(), "created for regular expression star" );
866 Node sk2
= NodeManager::currentNM()->mkSkolem( "rs_$$", s
.getType(), "created for regular expression star" );
867 Node s1nz
= sk1
.eqNode(d_emptyString
).negate();
868 Node s2nz
= sk2
.eqNode(d_emptyString
).negate();
869 Node s1inr
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, sk1
, r
[0]);
870 Node s2inrs
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, sk2
, r
);
871 Node s12
= s
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
, sk1
, sk2
));
873 conc
= NodeManager::currentNM()->mkNode(kind::AND
, s12
, s1nz
, s2nz
, s1inr
, s2inrs
);
874 conc
= NodeManager::currentNM()->mkNode(kind::OR
, se
, sinr
, conc
);
879 Trace("strings-regexp") << "Unsupported term: " << r
<< " in simplifyPRegExp." << std::endl
;
880 Assert( false, "Unsupported Term" );
883 conc
= Rewriter::rewrite( conc
);
884 new_nodes
.push_back( conc
);
885 d_simpl_cache
[p
] = conc
;
889 void RegExpOpr::getCharSet( Node r
, std::set
<unsigned> &pcset
, SetNodes
&pvset
) {
890 std::map
< Node
, std::pair
< std::set
<unsigned>, SetNodes
> >::const_iterator itr
= d_cset_cache
.find(r
);
891 if(itr
!= d_cset_cache
.end()) {
892 pcset
.insert((itr
->second
).first
.begin(), (itr
->second
).first
.end());
893 pvset
.insert((itr
->second
).second
.begin(), (itr
->second
).second
.end());
895 std::set
<unsigned> cset
;
899 case kind::REGEXP_EMPTY
: {
902 case kind::REGEXP_SIGMA
: {
903 for(unsigned i
=0; i
<d_card
; i
++) {
908 case kind::STRING_TO_REGEXP
: {
909 Node st
= Rewriter::rewrite(r
[0]);
911 CVC4::String s
= st
.getConst
< CVC4::String
>();
912 s
.getCharSet( cset
);
913 } else if(st
.getKind() == kind::VARIABLE
) {
916 for(unsigned i
=0; i
<st
.getNumChildren(); i
++) {
917 if(st
[i
].isConst()) {
918 CVC4::String s
= st
[i
].getConst
< CVC4::String
>();
919 s
.getCharSet( cset
);
921 vset
.insert( st
[i
] );
927 case kind::REGEXP_CONCAT
: {
928 for(unsigned i
=0; i
<r
.getNumChildren(); i
++) {
929 getCharSet(r
[i
], cset
, vset
);
933 case kind::REGEXP_UNION
: {
934 for(unsigned i
=0; i
<r
.getNumChildren(); i
++) {
935 getCharSet(r
[i
], cset
, vset
);
939 case kind::REGEXP_INTER
: {
940 //TODO: Overapproximation for now
941 for(unsigned i
=0; i
<r
.getNumChildren(); i
++) {
942 getCharSet(r
[i
], cset
, vset
);
946 case kind::REGEXP_STAR
: {
947 getCharSet(r
[0], cset
, vset
);
951 Trace("strings-regexp") << "Unsupported term: " << r
<< " in getCharSet." << std::endl
;
952 Assert( false, "Unsupported Term" );
955 pcset
.insert(cset
.begin(), cset
.end());
956 pvset
.insert(vset
.begin(), vset
.end());
957 std::pair
< std::set
<unsigned>, SetNodes
> p(cset
, vset
);
960 Trace("regexp-cset") << "CSET( " << mkString(r
) << " ) = { ";
961 for(std::set
<unsigned>::const_iterator itr
= cset
.begin();
962 itr
!= cset
.end(); itr
++) {
963 Trace("regexp-cset") << CVC4::String::convertUnsignedIntToChar(*itr
) << ",";
965 Trace("regexp-cset") << " }" << std::endl
;
969 Node
RegExpOpr::intersectInternal( Node r1
, Node r2
, std::map
< unsigned, std::set
< PairNodes
> > cache
) {
970 std::pair
< Node
, Node
> p(r1
, r2
);
971 std::map
< std::pair
< Node
, Node
>, Node
>::const_iterator itr
= d_inter_cache
.find(p
);
973 if(itr
!= d_inter_cache
.end()) {
974 //Trace("regexp-intersect") << "INTERSECT Case 0: Cached " << std::endl;
977 if(r1
== d_emptyRegexp
|| r2
== d_emptyRegexp
) {
978 Trace("regexp-intersect") << "INTERSECT Case 1: one empty RE" << std::endl
;
979 rNode
= d_emptyRegexp
;
980 } else if(r1
== d_emptySingleton
|| r2
== d_emptySingleton
) {
981 Trace("regexp-intersect") << "INTERSECT Case 2: one empty Singleton" << std::endl
;
982 int r
= delta(r1
== d_emptySingleton
? r2
: r1
);
985 AlwaysAssert( false, "Unsupported Yet, 892 REO" );
987 rNode
= d_emptySingleton
;
989 rNode
= d_emptyRegexp
;
992 Trace("regexp-intersect") << "INTERSECT Case 3: must compare" << std::endl
;
993 std::set
< unsigned > cset
, cset2
;
994 std::vector
< unsigned > cdiff
;
995 std::set
< Node
> vset
;
996 getCharSet(r1
, cset
, vset
);
997 getCharSet(r2
, cset2
, vset
);
999 std::set_symmetric_difference(cset
.begin(), cset
.end(), cset2
.begin(), cset2
.end(), std::back_inserter(cdiff
));
1001 Trace("regexp-intersect") << "INTERSECT Case 3.1: compare" << std::endl
;
1003 firstChars(r1
, cset
, vset
);
1004 std::vector
< Node
> vec_nodes
;
1005 for(std::set
<unsigned>::const_iterator itr
= cset
.begin();
1006 itr
!= cset
.end(); itr
++) {
1007 CVC4::String
c( CVC4::String::convertUnsignedIntToChar(*itr
) );
1008 std::pair
< Node
, Node
> p(r1
, r2
);
1009 if(cache
[ *itr
].find(p
) == cache
[ *itr
].end()) {
1010 Node r1l
= derivativeSingle(r1
, c
);
1011 Node r2l
= derivativeSingle(r2
, c
);
1012 std::map
< unsigned, std::set
< PairNodes
> > cache2(cache
);
1013 PairNodes
p(r1l
, r2l
);
1014 cache2
[ *itr
].insert( p
);
1015 Node rt
= intersectInternal(r1l
, r2l
, cache2
);
1016 rt
= Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
,
1017 NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP
, NodeManager::currentNM()->mkConst(c
)), rt
) );
1018 vec_nodes
.push_back(rt
);
1021 rNode
= vec_nodes
.size()==0 ? d_emptyRegexp
: vec_nodes
.size()==1 ? vec_nodes
[0] :
1022 NodeManager::currentNM()->mkNode(kind::OR
, vec_nodes
);
1023 rNode
= Rewriter::rewrite( rNode
);
1025 Trace("regexp-intersect") << "INTERSECT Case 3.2: diff cset" << std::endl
;
1026 rNode
= d_emptyRegexp
;
1029 //TODO: non-empty var set
1030 AlwaysAssert( false, "Unsupported Yet, 927 REO" );
1033 d_inter_cache
[p
] = rNode
;
1035 Trace("regexp-intersect") << "INTERSECT( " << mkString(r1
) << ", " << mkString(r2
) << " ) = " << mkString(rNode
) << std::endl
;
1038 Node
RegExpOpr::intersect(Node r1
, Node r2
) {
1039 std::map
< unsigned, std::set
< PairNodes
> > cache
;
1040 return intersectInternal(r1
, r2
, cache
);
1043 std::string
RegExpOpr::niceChar( Node r
) {
1045 std::string s
= r
.getConst
<CVC4::String
>().toString() ;
1046 return s
== "" ? "{E}" : ( s
== " " ? "{ }" : s
);
1048 return r
.toString();
1051 std::string
RegExpOpr::mkString( Node r
) {
1056 int k
= r
.getKind();
1058 case kind::REGEXP_EMPTY
: {
1062 case kind::REGEXP_SIGMA
: {
1066 case kind::STRING_TO_REGEXP
: {
1067 retStr
+= niceChar( r
[0] );
1070 case kind::REGEXP_CONCAT
: {
1072 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
1073 //if(i != 0) retStr += ".";
1074 retStr
+= mkString( r
[i
] );
1079 case kind::REGEXP_UNION
: {
1084 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
1085 if(i
!= 0) retStr
+= "|";
1086 retStr
+= mkString( r
[i
] );
1092 case kind::REGEXP_INTER
: {
1094 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
1095 if(i
!= 0) retStr
+= "&";
1096 retStr
+= mkString( r
[i
] );
1101 case kind::REGEXP_STAR
: {
1102 retStr
+= mkString( r
[0] );
1106 case kind::REGEXP_PLUS
: {
1107 retStr
+= mkString( r
[0] );
1111 case kind::REGEXP_OPT
: {
1112 retStr
+= mkString( r
[0] );
1116 case kind::REGEXP_RANGE
: {
1118 retStr
+= niceChar( r
[0] );
1120 retStr
+= niceChar( r
[1] );
1125 Trace("strings-error") << "Unsupported term: " << r
<< " in RegExp." << std::endl
;
1127 //return Node::null();
1134 }/* CVC4::theory::strings namespace */
1135 }/* CVC4::theory namespace */
1136 }/* CVC4 namespace */