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 Regular Expresion Operations
25 ** 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 std::vector
< Node
> nvec
;
42 d_emptyRegexp
= NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY
, nvec
);
43 // All Charactors = all printable ones 32-126
44 //d_char_start = 'a';//' ';
45 //d_char_end = 'c';//'~';
46 //d_sigma = mkAllExceptOne( '\0' );
47 d_sigma
= NodeManager::currentNM()->mkNode( kind::REGEXP_SIGMA
, nvec
);
48 d_sigma_star
= NodeManager::currentNM()->mkNode( kind::REGEXP_STAR
, d_sigma
);
51 int RegExpOpr::gcd ( int a
, int b
) {
54 c
= a
; a
= b
%a
; b
= c
;
59 bool RegExpOpr::checkConstRegExp( Node r
) {
60 Trace("strings-regexp-cstre") << "RegExp-CheckConstRegExp starts with " << mkString( r
) << std::endl
;
62 if( d_cstre_cache
.find( r
) != d_cstre_cache
.end() ) {
63 ret
= d_cstre_cache
[r
];
65 if(r
.getKind() == kind::STRING_TO_REGEXP
) {
66 Node tmp
= Rewriter::rewrite( r
[0] );
69 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
70 if(!checkConstRegExp(r
[i
])) {
75 d_cstre_cache
[r
] = ret
;
80 // 0-unknown, 1-yes, 2-no
81 int RegExpOpr::delta( Node r
) {
82 Trace("strings-regexp-delta") << "RegExp-Delta starts with " << mkString( r
) << std::endl
;
84 if( d_delta_cache
.find( r
) != d_delta_cache
.end() ) {
85 ret
= d_delta_cache
[r
];
89 case kind::REGEXP_EMPTY
: {
93 case kind::REGEXP_SIGMA
: {
97 case kind::STRING_TO_REGEXP
: {
99 if(r
[0] == d_emptyString
) {
109 case kind::REGEXP_CONCAT
: {
111 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
112 int tmp
= delta( r
[i
] );
116 } else if(tmp
== 0) {
120 if(!flag
&& ret
!= 2) {
125 case kind::REGEXP_UNION
: {
127 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
128 int tmp
= delta( r
[i
] );
132 } else if(tmp
== 0) {
136 if(!flag
&& ret
!= 1) {
141 case kind::REGEXP_INTER
: {
143 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
144 int tmp
= delta( r
[i
] );
148 } else if(tmp
== 0) {
158 case kind::REGEXP_STAR
: {
162 case kind::REGEXP_PLUS
: {
166 case kind::REGEXP_OPT
: {
170 case kind::REGEXP_RANGE
: {
175 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in delta of RegExp." << std::endl
;
177 //return Node::null();
180 d_delta_cache
[r
] = ret
;
182 Trace("strings-regexp-delta") << "RegExp-Delta returns : " << ret
<< std::endl
;
186 Node
RegExpOpr::derivativeSingle( Node r
, CVC4::String c
) {
187 Assert( c
.size() < 2 );
188 Trace("strings-regexp-derivative") << "RegExp-derivative starts with R{ " << mkString( r
) << " }, c=" << c
<< std::endl
;
189 Node retNode
= d_emptyRegexp
;
190 PairDvStr dv
= std::make_pair( r
, c
);
191 if( d_dv_cache
.find( dv
) != d_dv_cache
.end() ) {
192 retNode
= d_dv_cache
[dv
];
193 } else if( c
.isEmptyString() ){
194 int tmp
= delta( r
);
197 retNode
= d_emptyRegexp
;
198 } else if(tmp
== 1) {
201 retNode
= d_emptyRegexp
;
206 case kind::REGEXP_EMPTY
: {
207 retNode
= d_emptyRegexp
;
210 case kind::REGEXP_SIGMA
: {
211 retNode
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, d_emptyString
);
214 case kind::STRING_TO_REGEXP
: {
216 if(r
[0] == d_emptyString
) {
217 retNode
= d_emptyRegexp
;
219 if(r
[0].getConst
< CVC4::String
>().getFirstChar() == c
.getFirstChar()) {
220 retNode
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
,
221 r
[0].getConst
< CVC4::String
>().size() == 1 ? d_emptyString
: NodeManager::currentNM()->mkConst( r
[0].getConst
< CVC4::String
>().substr(1) ) );
223 retNode
= d_emptyRegexp
;
228 retNode
= d_emptyRegexp
;
232 case kind::REGEXP_CONCAT
: {
233 Node rees
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, d_emptyString
);
234 std::vector
< Node
> vec_nodes
;
235 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
236 Node dc
= derivativeSingle(r
[i
], c
);
237 if(dc
!= d_emptyRegexp
) {
238 std::vector
< Node
> vec_nodes2
;
240 vec_nodes2
.push_back( dc
);
242 for(unsigned j
=i
+1; j
<r
.getNumChildren(); ++j
) {
244 vec_nodes2
.push_back( r
[j
] );
247 Node tmp
= vec_nodes2
.size()==0 ? rees
:
248 vec_nodes2
.size()==1 ? vec_nodes2
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, vec_nodes2
);
249 if(std::find(vec_nodes
.begin(), vec_nodes
.end(), tmp
) == vec_nodes
.end()) {
250 vec_nodes
.push_back( tmp
);
254 if( delta( r
[i
] ) != 1 ) {
258 retNode
= vec_nodes
.size() == 0 ? d_emptyRegexp
:
259 ( vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_UNION
, vec_nodes
) );
262 case kind::REGEXP_UNION
: {
263 std::vector
< Node
> vec_nodes
;
264 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
265 Node dc
= derivativeSingle(r
[i
], c
);
266 if(dc
!= d_emptyRegexp
) {
267 if(std::find(vec_nodes
.begin(), vec_nodes
.end(), dc
) == vec_nodes
.end()) {
268 vec_nodes
.push_back( dc
);
271 Trace("strings-regexp-derivative") << "RegExp-derivative OR R[" << i
<< "]{ " << mkString(r
[i
]) << " returns " << mkString(dc
) << std::endl
;
273 retNode
= vec_nodes
.size() == 0 ? d_emptyRegexp
:
274 ( vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_UNION
, vec_nodes
) );
277 case kind::REGEXP_INTER
: {
279 bool flag_sg
= false;
280 std::vector
< Node
> vec_nodes
;
281 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
282 Node dc
= derivativeSingle(r
[i
], c
);
283 if(dc
!= d_emptyRegexp
) {
284 if(dc
== d_sigma_star
) {
287 if(std::find(vec_nodes
.begin(), vec_nodes
.end(), dc
) == vec_nodes
.end()) {
288 vec_nodes
.push_back( dc
);
297 if(vec_nodes
.size() == 0 && flag_sg
) {
298 retNode
= d_sigma_star
;
300 retNode
= vec_nodes
.size() == 0 ? d_emptyRegexp
:
301 ( vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_INTER
, vec_nodes
) );
304 retNode
= d_emptyRegexp
;
308 case kind::REGEXP_STAR
: {
309 Node dc
= derivativeSingle(r
[0], c
);
310 if(dc
!= d_emptyRegexp
) {
311 retNode
= dc
==NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, d_emptyString
) ? r
: NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, dc
, r
);
313 retNode
= d_emptyRegexp
;
318 //TODO: special sym: sigma, none, all
319 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in derivative of RegExp." << std::endl
;
320 Assert( false, "Unsupported Term" );
321 //return Node::null();
324 if(retNode
!= d_emptyRegexp
) {
325 retNode
= Rewriter::rewrite( retNode
);
327 d_dv_cache
[dv
] = retNode
;
329 Trace("strings-regexp-derivative") << "RegExp-derivative returns : " << mkString( retNode
) << std::endl
;
334 bool RegExpOpr::guessLength( Node r
, int &co
) {
337 case kind::STRING_TO_REGEXP
:
340 co
+= r
[0].getConst
< CVC4::String
>().size();
347 case kind::REGEXP_CONCAT
:
349 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
350 if(!guessLength( r
[i
], co
)) {
357 case kind::REGEXP_UNION
:
360 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
362 if(!guessLength( r
[i
], cop
)) {
368 g_co
= gcd(g_co
, cop
);
374 case kind::REGEXP_INTER
:
377 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
379 if(!guessLength( r
[i
], cop
)) {
385 g_co
= gcd(g_co
, cop
);
391 case kind::REGEXP_STAR
:
398 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in membership of RegExp." << std::endl
;
403 void RegExpOpr::firstChar( Node r
) {
404 Trace("strings-regexp-firstchar") << "Head characters: ";
405 for(char ch
= d_char_start
; ch
<= d_char_end
; ++ch
) {
407 Node dc
= derivativeSingle(r
, ch
);
409 Trace("strings-regexp-firstchar") << c
<< " (" << mkString(dc
) << ")" << std::endl
;
412 Trace("strings-regexp-firstchar") << std::endl
;
415 bool RegExpOpr::follow( Node r
, CVC4::String c
, std::vector
< char > &vec_chars
) {
418 case kind::STRING_TO_REGEXP
:
421 if(r
[0] != d_emptyString
) {
422 char t1
= r
[0].getConst
< CVC4::String
>().getFirstChar();
423 if(c
.isEmptyString()) {
424 vec_chars
.push_back( t1
);
427 char t2
= c
.getFirstChar();
432 vec_chars
.push_back( c
.substr(1,1).getFirstChar() );
434 vec_chars
.push_back( '\0' );
447 case kind::REGEXP_CONCAT
:
449 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
450 if( follow(r
[i
], c
, vec_chars
) ) {
451 if(vec_chars
[vec_chars
.size() - 1] == '\0') {
452 vec_chars
.pop_back();
453 c
= d_emptyString
.getConst
< CVC4::String
>();
459 vec_chars
.push_back( '\0' );
463 case kind::REGEXP_UNION
:
466 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
467 if( follow(r
[i
], c
, vec_chars
) ) {
474 case kind::REGEXP_INTER
:
476 std::vector
< char > vt2
;
477 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
478 std::vector
< char > v_tmp
;
479 if( !follow(r
[i
], c
, v_tmp
) ) {
482 std::vector
< char > vt3(vt2
);
484 std::set_intersection( vt3
.begin(), vt3
.end(), v_tmp
.begin(), v_tmp
.end(), vt2
.begin() );
485 if(vt2
.size() == 0) {
489 vec_chars
.insert( vec_chars
.end(), vt2
.begin(), vt2
.end() );
493 case kind::REGEXP_STAR
:
495 if(follow(r
[0], c
, vec_chars
)) {
496 if(vec_chars
[vec_chars
.size() - 1] == '\0') {
497 if(c
.isEmptyString()) {
500 vec_chars
.pop_back();
501 c
= d_emptyString
.getConst
< CVC4::String
>();
502 return follow(r
[0], c
, vec_chars
);
508 vec_chars
.push_back( '\0' );
514 case kind::REGEXP_PLUS:
519 case kind::REGEXP_OPT:
524 case kind::REGEXP_RANGE:
530 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in delta of RegExp." << std::endl
;
531 //AlwaysAssert( false );
532 //return Node::null();
538 Node
RegExpOpr::mkAllExceptOne( char exp_c
) {
539 std::vector
< Node
> vec_nodes
;
540 for(char c
=d_char_start
; c
<=d_char_end
; ++c
) {
542 Node n
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, NodeManager::currentNM()->mkConst( ::CVC4::String( c
) ) );
543 vec_nodes
.push_back( n
);
546 return NodeManager::currentNM()->mkNode( kind::REGEXP_UNION
, vec_nodes
);
550 void RegExpOpr::simplify(Node t
, std::vector
< Node
> &new_nodes
, bool polarity
) {
551 Trace("strings-regexp-simpl") << "RegExp-Simpl starts with " << t
<< ", polarity=" << polarity
<< std::endl
;
552 Assert(t
.getKind() == kind::STRING_IN_REGEXP
);
553 Node str
= Rewriter::rewrite(t
[0]);
554 Node re
= Rewriter::rewrite(t
[1]);
556 simplifyPRegExp( str
, re
, new_nodes
);
558 simplifyNRegExp( str
, re
, new_nodes
);
560 Trace("strings-regexp-simpl") << "RegExp-Simpl returns (" << new_nodes
.size() << "):\n";
561 for(unsigned i
=0; i
<new_nodes
.size(); i
++) {
562 Trace("strings-regexp-simpl") << "\t" << new_nodes
[i
] << std::endl
;
565 void RegExpOpr::simplifyNRegExp( Node s
, Node r
, std::vector
< Node
> &new_nodes
) {
566 std::pair
< Node
, Node
> p(s
, r
);
567 std::map
< std::pair
< Node
, Node
>, Node
>::const_iterator itr
= d_simpl_neg_cache
.find(p
);
568 if(itr
!= d_simpl_neg_cache
.end()) {
569 new_nodes
.push_back( itr
->second
);
575 case kind::REGEXP_EMPTY
: {
579 case kind::REGEXP_SIGMA
: {
580 conc
= d_one
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
)).negate();
583 case kind::STRING_TO_REGEXP
: {
584 conc
= s
.eqNode(r
[0]).negate();
587 case kind::REGEXP_CONCAT
: {
588 //TODO: rewrite empty
589 Node b1
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
590 Node b1v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, b1
);
591 Node g1
= NodeManager::currentNM()->mkNode( kind::AND
, NodeManager::currentNM()->mkNode(kind::GEQ
, b1
, d_zero
),
592 NodeManager::currentNM()->mkNode( kind::GEQ
, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
), b1
) );
593 Node s1
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
594 Node s2
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
595 Node b2v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, s1
, s2
);
596 Node s12
= s
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
, s1
, s2
));
597 Node s1len
= b1
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s1
));
598 Node s1r1
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s1
, r
[0]).negate();
599 if(r
[0].getKind() == kind::STRING_TO_REGEXP
) {
600 s1r1
= s1
.eqNode(r
[0][0]).negate();
601 } else if(r
[0].getKind() == kind::REGEXP_EMPTY
) {
605 if(r
.getNumChildren() > 2) {
606 std::vector
< Node
> nvec
;
607 for(unsigned i
=1; i
<r
.getNumChildren(); i
++) {
608 nvec
.push_back( r
[i
] );
610 r2
= NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
, nvec
);
612 r2
= Rewriter::rewrite(r2
);
613 Node s2r2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s2
, r2
).negate();
614 if(r2
.getKind() == kind::STRING_TO_REGEXP
) {
615 s2r2
= s2
.eqNode(r2
[0]).negate();
616 } else if(r2
.getKind() == kind::REGEXP_EMPTY
) {
620 conc
= NodeManager::currentNM()->mkNode(kind::OR
, s1r1
, s2r2
);
621 conc
= NodeManager::currentNM()->mkNode(kind::AND
, s12
, s1len
, conc
);
622 conc
= NodeManager::currentNM()->mkNode(kind::EXISTS
, b2v
, conc
);
623 conc
= NodeManager::currentNM()->mkNode(kind::IMPLIES
, g1
, conc
);
624 conc
= NodeManager::currentNM()->mkNode(kind::FORALL
, b1v
, conc
);
627 case kind::REGEXP_UNION
: {
628 std::vector
< Node
> c_and
;
629 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
630 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
631 c_and
.push_back( r
[i
][0].eqNode(s
).negate() );
632 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
635 c_and
.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[i
]).negate());
638 conc
= c_and
.size() == 0 ? d_true
:
639 c_and
.size() == 1 ? c_and
[0] : NodeManager::currentNM()->mkNode(kind::AND
, c_and
);
642 case kind::REGEXP_INTER
: {
643 bool emptyflag
= false;
644 std::vector
< Node
> c_or
;
645 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
646 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
647 c_or
.push_back( r
[i
][0].eqNode(s
).negate() );
648 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
652 c_or
.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[i
]).negate());
658 conc
= c_or
.size() == 1 ? c_or
[0] : NodeManager::currentNM()->mkNode(kind::OR
, c_or
);
662 case kind::REGEXP_STAR
: {
663 if(s
== d_emptyString
) {
665 } else if(r
[0].getKind() == kind::REGEXP_EMPTY
) {
666 conc
= s
.eqNode(d_emptyString
).negate();
667 } else if(r
[0].getKind() == kind::REGEXP_SIGMA
) {
670 Node lens
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
);
671 Node sne
= s
.eqNode(d_emptyString
).negate();
672 Node b1
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
673 Node b1v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, b1
);
674 Node g1
= NodeManager::currentNM()->mkNode( kind::AND
, NodeManager::currentNM()->mkNode(kind::GEQ
, b1
, d_one
),
675 NodeManager::currentNM()->mkNode( kind::GEQ
, lens
, b1
) );
677 Node s1
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL
, s
, d_zero
, b1
);
678 Node s2
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL
, s
, b1
, NodeManager::currentNM()->mkNode(kind::MINUS
, lens
, b1
));
679 Node s1r1
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s1
, r
[0]).negate();
680 Node s2r2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s2
, r
).negate();
682 conc
= NodeManager::currentNM()->mkNode(kind::OR
, s1r1
, s2r2
);
683 conc
= NodeManager::currentNM()->mkNode(kind::IMPLIES
, g1
, conc
);
684 conc
= NodeManager::currentNM()->mkNode(kind::FORALL
, b1v
, conc
);
685 conc
= NodeManager::currentNM()->mkNode(kind::AND
, sne
, conc
);
690 Trace("strings-regexp") << "Unsupported term: " << r
<< " in simplifyNRegExp." << std::endl
;
691 Assert( false, "Unsupported Term" );
694 conc
= Rewriter::rewrite( conc
);
695 new_nodes
.push_back( conc
);
696 d_simpl_neg_cache
[p
] = conc
;
699 void RegExpOpr::simplifyPRegExp( Node s
, Node r
, std::vector
< Node
> &new_nodes
) {
700 std::pair
< Node
, Node
> p(s
, r
);
701 std::map
< std::pair
< Node
, Node
>, Node
>::const_iterator itr
= d_simpl_cache
.find(p
);
702 if(itr
!= d_simpl_cache
.end()) {
703 new_nodes
.push_back( itr
->second
);
709 case kind::REGEXP_EMPTY
: {
713 case kind::REGEXP_SIGMA
: {
714 conc
= d_one
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
));
717 case kind::STRING_TO_REGEXP
: {
718 conc
= s
.eqNode(r
[0]);
721 case kind::REGEXP_CONCAT
: {
722 std::vector
< Node
> nvec
;
723 std::vector
< Node
> cc
;
724 bool emptyflag
= false;
725 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
726 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
727 cc
.push_back( r
[i
][0] );
728 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
732 Node sk
= NodeManager::currentNM()->mkSkolem( "rc_$$", s
.getType(), "created for regular expression concat" );
733 Node lem
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, sk
, r
[i
]);
741 Node lem
= s
.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
, cc
) );
743 conc
= nvec
.size() == 1 ? nvec
[0] : NodeManager::currentNM()->mkNode(kind::AND
, nvec
);
747 case kind::REGEXP_UNION
: {
748 std::vector
< Node
> c_or
;
749 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
750 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
751 c_or
.push_back( r
[i
][0].eqNode(s
) );
752 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
755 c_or
.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[i
]));
758 conc
= c_or
.size() == 0 ? d_false
:
759 c_or
.size() == 1 ? c_or
[0] : NodeManager::currentNM()->mkNode(kind::OR
, c_or
);
762 case kind::REGEXP_INTER
: {
763 std::vector
< Node
> c_and
;
764 bool emptyflag
= false;
765 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
766 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
767 c_and
.push_back( r
[i
][0].eqNode(s
) );
768 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
772 c_and
.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[i
]));
778 conc
= c_and
.size() == 1 ? c_and
[0] : NodeManager::currentNM()->mkNode(kind::AND
, c_and
);
782 case kind::REGEXP_STAR
: {
783 if(s
== d_emptyString
) {
785 } else if(r
[0].getKind() == kind::REGEXP_EMPTY
) {
786 conc
= s
.eqNode(d_emptyString
);
787 } else if(r
[0].getKind() == kind::REGEXP_SIGMA
) {
790 Node se
= s
.eqNode(d_emptyString
);
791 Node sinr
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[0]);
792 Node sk1
= NodeManager::currentNM()->mkSkolem( "rs_$$", s
.getType(), "created for regular expression star" );
793 Node sk2
= NodeManager::currentNM()->mkSkolem( "rs_$$", s
.getType(), "created for regular expression star" );
794 Node s1nz
= sk1
.eqNode(d_emptyString
).negate();
795 Node s2nz
= sk2
.eqNode(d_emptyString
).negate();
796 Node s1inr
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, sk1
, r
[0]);
797 Node s2inrs
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, sk2
, r
);
798 Node s12
= s
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
, sk1
, sk2
));
800 conc
= NodeManager::currentNM()->mkNode(kind::AND
, s12
, s1nz
, s2nz
, s1inr
, s2inrs
);
801 conc
= NodeManager::currentNM()->mkNode(kind::OR
, se
, sinr
, conc
);
806 Trace("strings-regexp") << "Unsupported term: " << r
<< " in simplifyPRegExp." << std::endl
;
807 Assert( false, "Unsupported Term" );
810 conc
= Rewriter::rewrite( conc
);
811 new_nodes
.push_back( conc
);
812 d_simpl_cache
[p
] = conc
;
817 std::string
RegExpOpr::niceChar( Node r
) {
819 std::string s
= r
.getConst
<CVC4::String
>().toString() ;
820 return s
== "" ? "{E}" : ( s
== " " ? "{ }" : s
);
825 std::string
RegExpOpr::mkString( Node r
) {
832 case kind::REGEXP_EMPTY
: {
836 case kind::REGEXP_SIGMA
: {
840 case kind::STRING_TO_REGEXP
: {
841 retStr
+= niceChar( r
[0] );
844 case kind::REGEXP_CONCAT
: {
846 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
847 if(i
!= 0) retStr
+= ".";
848 retStr
+= mkString( r
[i
] );
853 case kind::REGEXP_UNION
: {
858 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
859 if(i
!= 0) retStr
+= "|";
860 retStr
+= mkString( r
[i
] );
866 case kind::REGEXP_INTER
: {
868 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
869 if(i
!= 0) retStr
+= "&";
870 retStr
+= mkString( r
[i
] );
875 case kind::REGEXP_STAR
: {
876 retStr
+= mkString( r
[0] );
880 case kind::REGEXP_PLUS
: {
881 retStr
+= mkString( r
[0] );
885 case kind::REGEXP_OPT
: {
886 retStr
+= mkString( r
[0] );
890 case kind::REGEXP_RANGE
: {
892 retStr
+= niceChar( r
[0] );
894 retStr
+= niceChar( r
[1] );
899 Trace("strings-error") << "Unsupported term: " << r
<< " in RegExp." << std::endl
;
900 //AlwaysAssert( false );
901 //return Node::null();
908 }/* CVC4::theory::strings namespace */
909 }/* CVC4::theory namespace */
910 }/* CVC4 namespace */