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_emptyRegexp
= NodeManager::currentNM()->mkConst( kind::REGEXP_EMPTY
);
40 d_zero
= NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
41 d_one
= NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
42 // All Charactors = all printable ones 32-126
43 d_char_start
= 'a';//' ';
44 d_char_end
= 'c';//'~';
45 d_sigma
= mkAllExceptOne( '\0' );
46 //d_sigma = NodeManager::currentNM()->mkConst( kind::REGEXP_SIGMA );
47 d_sigma_star
= NodeManager::currentNM()->mkNode( kind::REGEXP_STAR
, d_sigma
);
50 int RegExpOpr::gcd ( int a
, int b
) {
53 c
= a
; a
= b
%a
; b
= c
;
58 bool RegExpOpr::checkConstRegExp( Node r
) {
59 Trace("strings-regexp-cstre") << "RegExp-CheckConstRegExp starts with " << mkString( r
) << std::endl
;
61 if( d_cstre_cache
.find( r
) != d_cstre_cache
.end() ) {
62 ret
= d_cstre_cache
[r
];
64 if(r
.getKind() == kind::STRING_TO_REGEXP
) {
65 Node tmp
= Rewriter::rewrite( r
[0] );
68 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
69 if(!checkConstRegExp(r
[i
])) {
74 d_cstre_cache
[r
] = ret
;
79 // 0-unknown, 1-yes, 2-no
80 int RegExpOpr::delta( Node r
) {
81 Trace("strings-regexp-delta") << "RegExp-Delta starts with " << mkString( r
) << std::endl
;
83 if( d_delta_cache
.find( r
) != d_delta_cache
.end() ) {
84 ret
= d_delta_cache
[r
];
88 case kind::REGEXP_EMPTY
: {
92 case kind::REGEXP_SIGMA
: {
96 case kind::STRING_TO_REGEXP
: {
98 if(r
[0] == d_emptyString
) {
108 case kind::REGEXP_CONCAT
: {
110 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
111 int tmp
= delta( r
[i
] );
115 } else if(tmp
== 0) {
119 if(!flag
&& ret
!= 2) {
124 case kind::REGEXP_UNION
: {
126 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
127 int tmp
= delta( r
[i
] );
131 } else if(tmp
== 0) {
135 if(!flag
&& ret
!= 1) {
140 case kind::REGEXP_INTER
: {
142 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
143 int tmp
= delta( r
[i
] );
147 } else if(tmp
== 0) {
157 case kind::REGEXP_STAR
: {
161 case kind::REGEXP_PLUS
: {
165 case kind::REGEXP_OPT
: {
169 case kind::REGEXP_RANGE
: {
174 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in delta of RegExp." << std::endl
;
175 AlwaysAssert( false );
176 //return Node::null();
179 d_delta_cache
[r
] = ret
;
181 Trace("strings-regexp-delta") << "RegExp-Delta returns : " << ret
<< std::endl
;
185 Node
RegExpOpr::derivativeSingle( Node r
, CVC4::String c
) {
186 Assert( c
.size() < 2 );
187 Trace("strings-regexp-derivative") << "RegExp-derivative starts with R{ " << mkString( r
) << " }, c=" << c
<< std::endl
;
188 Node retNode
= d_emptyRegexp
;
189 PairDvStr dv
= std::make_pair( r
, c
);
190 if( d_dv_cache
.find( dv
) != d_dv_cache
.end() ) {
191 retNode
= d_dv_cache
[dv
];
192 } else if( c
.isEmptyString() ){
193 int tmp
= delta( r
);
196 retNode
= d_emptyRegexp
;
197 } else if(tmp
== 1) {
200 retNode
= d_emptyRegexp
;
205 case kind::REGEXP_EMPTY
: {
206 retNode
= d_emptyRegexp
;
209 case kind::REGEXP_SIGMA
: {
210 retNode
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, d_emptyString
);
213 case kind::STRING_TO_REGEXP
: {
215 if(r
[0] == d_emptyString
) {
216 retNode
= d_emptyRegexp
;
218 if(r
[0].getConst
< CVC4::String
>().getFirstChar() == c
.getFirstChar()) {
219 retNode
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
,
220 r
[0].getConst
< CVC4::String
>().size() == 1 ? d_emptyString
: NodeManager::currentNM()->mkConst( r
[0].getConst
< CVC4::String
>().substr(1) ) );
222 retNode
= d_emptyRegexp
;
227 retNode
= d_emptyRegexp
;
231 case kind::REGEXP_CONCAT
: {
232 Node rees
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, d_emptyString
);
233 std::vector
< Node
> vec_nodes
;
234 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
235 Node dc
= derivativeSingle(r
[i
], c
);
236 if(dc
!= d_emptyRegexp
) {
237 std::vector
< Node
> vec_nodes2
;
239 vec_nodes2
.push_back( dc
);
241 for(unsigned j
=i
+1; j
<r
.getNumChildren(); ++j
) {
243 vec_nodes2
.push_back( r
[j
] );
246 Node tmp
= vec_nodes2
.size()==0 ? rees
:
247 vec_nodes2
.size()==1 ? vec_nodes2
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, vec_nodes2
);
248 if(std::find(vec_nodes
.begin(), vec_nodes
.end(), tmp
) == vec_nodes
.end()) {
249 vec_nodes
.push_back( tmp
);
253 if( delta( r
[i
] ) != 1 ) {
257 retNode
= vec_nodes
.size() == 0 ? d_emptyRegexp
:
258 ( vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_UNION
, vec_nodes
) );
261 case kind::REGEXP_UNION
: {
262 std::vector
< Node
> vec_nodes
;
263 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
264 Node dc
= derivativeSingle(r
[i
], c
);
265 if(dc
!= d_emptyRegexp
) {
266 if(std::find(vec_nodes
.begin(), vec_nodes
.end(), dc
) == vec_nodes
.end()) {
267 vec_nodes
.push_back( dc
);
270 Trace("strings-regexp-derivative") << "RegExp-derivative OR R[" << i
<< "]{ " << mkString(r
[i
]) << " returns " << mkString(dc
) << std::endl
;
272 retNode
= vec_nodes
.size() == 0 ? d_emptyRegexp
:
273 ( vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_UNION
, vec_nodes
) );
276 case kind::REGEXP_INTER
: {
278 bool flag_sg
= false;
279 std::vector
< Node
> vec_nodes
;
280 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
281 Node dc
= derivativeSingle(r
[i
], c
);
282 if(dc
!= d_emptyRegexp
) {
283 if(dc
== d_sigma_star
) {
286 if(std::find(vec_nodes
.begin(), vec_nodes
.end(), dc
) == vec_nodes
.end()) {
287 vec_nodes
.push_back( dc
);
296 if(vec_nodes
.size() == 0 && flag_sg
) {
297 retNode
= d_sigma_star
;
299 retNode
= vec_nodes
.size() == 0 ? d_emptyRegexp
:
300 ( vec_nodes
.size()==1 ? vec_nodes
[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_INTER
, vec_nodes
) );
303 retNode
= d_emptyRegexp
;
307 case kind::REGEXP_STAR
: {
308 Node dc
= derivativeSingle(r
[0], c
);
309 if(dc
!= d_emptyRegexp
) {
310 retNode
= dc
==NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, d_emptyString
) ? r
: NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, dc
, r
);
312 retNode
= d_emptyRegexp
;
317 //TODO: special sym: sigma, none, all
318 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in derivative of RegExp." << std::endl
;
319 Assert( false, "Unsupported Term" );
320 //return Node::null();
323 if(retNode
!= d_emptyRegexp
) {
324 retNode
= Rewriter::rewrite( retNode
);
326 d_dv_cache
[dv
] = retNode
;
328 Trace("strings-regexp-derivative") << "RegExp-derivative returns : " << mkString( retNode
) << std::endl
;
333 bool RegExpOpr::guessLength( Node r
, int &co
) {
336 case kind::STRING_TO_REGEXP
:
339 co
+= r
[0].getConst
< CVC4::String
>().size();
346 case kind::REGEXP_CONCAT
:
348 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
349 if(!guessLength( r
[i
], co
)) {
356 case kind::REGEXP_UNION
:
359 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
361 if(!guessLength( r
[i
], cop
)) {
367 g_co
= gcd(g_co
, cop
);
373 case kind::REGEXP_INTER
:
376 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
378 if(!guessLength( r
[i
], cop
)) {
384 g_co
= gcd(g_co
, cop
);
390 case kind::REGEXP_STAR
:
397 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in membership of RegExp." << std::endl
;
402 void RegExpOpr::firstChar( Node r
) {
403 Trace("strings-regexp-firstchar") << "Head characters: ";
404 for(char ch
= d_char_start
; ch
<= d_char_end
; ++ch
) {
406 Node dc
= derivativeSingle(r
, ch
);
408 Trace("strings-regexp-firstchar") << c
<< " (" << mkString(dc
) << ")" << std::endl
;
411 Trace("strings-regexp-firstchar") << std::endl
;
414 bool RegExpOpr::follow( Node r
, CVC4::String c
, std::vector
< char > &vec_chars
) {
417 case kind::STRING_TO_REGEXP
:
420 if(r
[0] != d_emptyString
) {
421 char t1
= r
[0].getConst
< CVC4::String
>().getFirstChar();
422 if(c
.isEmptyString()) {
423 vec_chars
.push_back( t1
);
426 char t2
= c
.getFirstChar();
431 vec_chars
.push_back( c
.substr(1,1).getFirstChar() );
433 vec_chars
.push_back( '\0' );
446 case kind::REGEXP_CONCAT
:
448 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
449 if( follow(r
[i
], c
, vec_chars
) ) {
450 if(vec_chars
[vec_chars
.size() - 1] == '\0') {
451 vec_chars
.pop_back();
452 c
= d_emptyString
.getConst
< CVC4::String
>();
458 vec_chars
.push_back( '\0' );
462 case kind::REGEXP_UNION
:
465 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
466 if( follow(r
[i
], c
, vec_chars
) ) {
473 case kind::REGEXP_INTER
:
475 std::vector
< char > vt2
;
476 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
477 std::vector
< char > v_tmp
;
478 if( !follow(r
[i
], c
, v_tmp
) ) {
481 std::vector
< char > vt3(vt2
);
483 std::set_intersection( vt3
.begin(), vt3
.end(), v_tmp
.begin(), v_tmp
.end(), vt2
.begin() );
484 if(vt2
.size() == 0) {
488 vec_chars
.insert( vec_chars
.end(), vt2
.begin(), vt2
.end() );
492 case kind::REGEXP_STAR
:
494 if(follow(r
[0], c
, vec_chars
)) {
495 if(vec_chars
[vec_chars
.size() - 1] == '\0') {
496 if(c
.isEmptyString()) {
499 vec_chars
.pop_back();
500 c
= d_emptyString
.getConst
< CVC4::String
>();
501 return follow(r
[0], c
, vec_chars
);
507 vec_chars
.push_back( '\0' );
513 case kind::REGEXP_PLUS:
518 case kind::REGEXP_OPT:
523 case kind::REGEXP_RANGE:
529 //TODO: special sym: sigma, none, all
530 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in delta of RegExp." << std::endl
;
531 //AlwaysAssert( false );
532 //return Node::null();
537 Node
RegExpOpr::mkAllExceptOne( char exp_c
) {
538 std::vector
< Node
> vec_nodes
;
539 for(char c
=d_char_start
; c
<=d_char_end
; ++c
) {
541 Node n
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, NodeManager::currentNM()->mkConst( ::CVC4::String( c
) ) );
542 vec_nodes
.push_back( n
);
545 return NodeManager::currentNM()->mkNode( kind::REGEXP_UNION
, vec_nodes
);
548 Node
RegExpOpr::complement( Node r
) {
549 Trace("strings-regexp-compl") << "RegExp-Compl starts with " << mkString( r
) << std::endl
;
551 if( d_compl_cache
.find( r
) != d_compl_cache
.end() ) {
552 retNode
= d_compl_cache
[r
];
556 case kind::STRING_TO_REGEXP
:
559 if(r
[0] == d_emptyString
) {
560 retNode
= NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, d_sigma
, d_sigma_star
);
562 std::vector
< Node
> vec_nodes
;
563 vec_nodes
.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
, d_emptyString
) );
564 CVC4::String s
= r
[0].getConst
<String
>();
565 for(unsigned i
=0; i
<s
.size(); ++i
) {
566 char c
= s
.substr(i
, 1).getFirstChar();
567 Node tmp
= mkAllExceptOne( c
);
569 Node tmph
= NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP
,
570 NodeManager::currentNM()->mkConst( s
.substr(0, i
) ) );
571 tmp
= NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, tmph
, tmp
);
573 tmp
= NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, tmp
, d_sigma_star
);
574 vec_nodes
.push_back( tmp
);
576 Node tmp
= NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, r
, d_sigma
, d_sigma_star
);
577 vec_nodes
.push_back( tmp
);
578 retNode
= NodeManager::currentNM()->mkNode( kind::REGEXP_UNION
, vec_nodes
);
581 Trace("strings-error") << "Unsupported string variable: " << r
[0] << " in complement of RegExp." << std::endl
;
582 //AlwaysAssert( false );
583 //return Node::null();
587 case kind::REGEXP_CONCAT
:
589 std::vector
< Node
> vec_nodes
;
590 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
591 Node tmp
= complement( r
[i
] );
592 for(unsigned j
=0; j
<i
; ++j
) {
593 tmp
= NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, r
[j
], tmp
);
595 if(i
!= r
.getNumChildren() - 1) {
596 tmp
= NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, tmp
,
597 NodeManager::currentNM()->mkNode( kind::REGEXP_STAR
, d_sigma
) );
599 vec_nodes
.push_back( tmp
);
601 retNode
= NodeManager::currentNM()->mkNode( kind::REGEXP_UNION
, vec_nodes
);
604 case kind::REGEXP_UNION
:
606 std::vector
< Node
> vec_nodes
;
607 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
608 Node tmp
= complement( r
[i
] );
609 vec_nodes
.push_back( tmp
);
611 retNode
= NodeManager::currentNM()->mkNode( kind::REGEXP_INTER
, vec_nodes
);
614 case kind::REGEXP_INTER
:
616 std::vector
< Node
> vec_nodes
;
617 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
618 Node tmp
= complement( r
[i
] );
619 vec_nodes
.push_back( tmp
);
621 retNode
= NodeManager::currentNM()->mkNode( kind::REGEXP_UNION
, vec_nodes
);
624 case kind::REGEXP_STAR
:
626 retNode
= NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, d_sigma
, d_sigma_star
);
627 Node tmp
= complement( r
[0] );
628 tmp
= NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT
, r
, tmp
);
629 retNode
= NodeManager::currentNM()->mkNode( kind::REGEXP_INTER
, retNode
, tmp
);
633 //TODO: special sym: sigma, none, all
634 Trace("strings-error") << "Unsupported term: " << mkString( r
) << " in complement of RegExp." << std::endl
;
635 //AlwaysAssert( false );
636 //return Node::null();
638 d_compl_cache
[r
] = retNode
;
640 Trace("strings-regexp-compl") << "RegExp-Compl returns : " << mkString( retNode
) << std::endl
;
645 void RegExpOpr::simplify(Node t
, std::vector
< Node
> &new_nodes
, bool polarity
) {
646 Trace("strings-regexp-simpl") << "RegExp-Simpl starts with " << t
<< ", polarity=" << polarity
<< std::endl
;
647 Assert(t
.getKind() == kind::STRING_IN_REGEXP
);
648 Node str
= Rewriter::rewrite(t
[0]);
649 Node re
= Rewriter::rewrite(t
[1]);
651 simplifyPRegExp( str
, re
, new_nodes
);
653 simplifyNRegExp( str
, re
, new_nodes
);
655 Trace("strings-regexp-simpl") << "RegExp-Simpl returns (" << new_nodes
.size() << "):\n";
656 for(unsigned i
=0; i
<new_nodes
.size(); i
++) {
657 Trace("strings-regexp-simpl") << "\t" << new_nodes
[i
] << std::endl
;
660 void RegExpOpr::simplifyNRegExp( Node s
, Node r
, std::vector
< Node
> &new_nodes
) {
661 std::pair
< Node
, Node
> p(s
, r
);
662 std::map
< std::pair
< Node
, Node
>, Node
>::const_iterator itr
= d_simpl_neg_cache
.find(p
);
663 if(itr
!= d_simpl_neg_cache
.end()) {
664 new_nodes
.push_back( itr
->second
);
670 case kind::REGEXP_EMPTY
: {
674 case kind::REGEXP_SIGMA
: {
675 conc
= d_one
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
)).negate();
678 case kind::STRING_TO_REGEXP
: {
679 conc
= s
.eqNode(r
[0]).negate();
682 case kind::REGEXP_CONCAT
: {
683 //TODO: rewrite empty
684 Node b1
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
685 Node b1v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, b1
);
686 Node g1
= NodeManager::currentNM()->mkNode( kind::AND
, NodeManager::currentNM()->mkNode(kind::GEQ
, b1
, d_zero
),
687 NodeManager::currentNM()->mkNode( kind::GEQ
, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
), b1
) );
688 Node s1
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
689 Node s2
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
690 Node b2v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, s1
, s2
);
691 Node s12
= s
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
, s1
, s2
));
692 Node s1len
= b1
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s1
));
693 Node s1r1
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s1
, r
[0]).negate();
694 if(r
[0].getKind() == kind::STRING_TO_REGEXP
) {
695 s1r1
= s1
.eqNode(r
[0][0]).negate();
696 } else if(r
[0].getKind() == kind::REGEXP_EMPTY
) {
700 if(r
.getNumChildren() > 2) {
701 std::vector
< Node
> nvec
;
702 for(unsigned i
=1; i
<r
.getNumChildren(); i
++) {
703 nvec
.push_back( r
[i
] );
705 r2
= NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT
, nvec
);
707 r2
= Rewriter::rewrite(r2
);
708 Node s2r2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s2
, r2
).negate();
709 if(r2
.getKind() == kind::STRING_TO_REGEXP
) {
710 s2r2
= s2
.eqNode(r2
[0]).negate();
711 } else if(r2
.getKind() == kind::REGEXP_EMPTY
) {
715 conc
= NodeManager::currentNM()->mkNode(kind::OR
, s1r1
, s2r2
);
716 conc
= NodeManager::currentNM()->mkNode(kind::AND
, s12
, s1len
, conc
);
717 conc
= NodeManager::currentNM()->mkNode(kind::EXISTS
, b2v
, conc
);
718 conc
= NodeManager::currentNM()->mkNode(kind::IMPLIES
, g1
, conc
);
719 conc
= NodeManager::currentNM()->mkNode(kind::FORALL
, b1v
, conc
);
722 case kind::REGEXP_UNION
: {
723 std::vector
< Node
> c_and
;
724 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
725 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
726 c_and
.push_back( r
[i
][0].eqNode(s
).negate() );
727 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
730 c_and
.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[i
]).negate());
733 conc
= c_and
.size() == 0 ? d_true
:
734 c_and
.size() == 1 ? c_and
[0] : NodeManager::currentNM()->mkNode(kind::AND
, c_and
);
737 case kind::REGEXP_INTER
: {
738 bool emptyflag
= false;
739 std::vector
< Node
> c_or
;
740 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
741 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
742 c_or
.push_back( r
[i
][0].eqNode(s
).negate() );
743 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
747 c_or
.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[i
]).negate());
753 conc
= c_or
.size() == 1 ? c_or
[0] : NodeManager::currentNM()->mkNode(kind::OR
, c_or
);
757 case kind::REGEXP_STAR
: {
758 if(s
== d_emptyString
) {
760 } else if(r
[0].getKind() == kind::REGEXP_EMPTY
) {
761 conc
= s
.eqNode(d_emptyString
).negate();
762 } else if(r
[0].getKind() == kind::REGEXP_SIGMA
) {
765 Node lens
= NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
);
766 Node sne
= s
.eqNode(d_emptyString
).negate();
767 Node b1
= NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
768 Node b1v
= NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST
, b1
);
769 Node g1
= NodeManager::currentNM()->mkNode( kind::AND
, NodeManager::currentNM()->mkNode(kind::GEQ
, b1
, d_one
),
770 NodeManager::currentNM()->mkNode( kind::GEQ
, lens
, b1
) );
772 Node s1
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL
, s
, d_zero
, b1
);
773 Node s2
= NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL
, s
, b1
, NodeManager::currentNM()->mkNode(kind::MINUS
, lens
, b1
));
774 //Node s1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
775 //Node s2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
776 //Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, s1, s2);
777 //Node s12 = s.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s1, s2));
778 //Node s1len = b1.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s1));
779 Node s1r1
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s1
, r
[0]).negate();
780 Node s2r2
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s2
, r
).negate();
782 conc
= NodeManager::currentNM()->mkNode(kind::OR
, s1r1
, s2r2
);
783 //conc = NodeManager::currentNM()->mkNode(kind::AND, s12, s1len, conc);
784 //conc = NodeManager::currentNM()->mkNode(kind::EXISTS, b2v, conc);
785 conc
= NodeManager::currentNM()->mkNode(kind::IMPLIES
, g1
, conc
);
786 conc
= NodeManager::currentNM()->mkNode(kind::FORALL
, b1v
, conc
);
787 conc
= NodeManager::currentNM()->mkNode(kind::AND
, sne
, conc
);
792 Trace("strings-regexp") << "Unsupported term: " << r
<< " in simplifyNRegExp." << std::endl
;
793 AlwaysAssert( false, "Unsupported Term" );
796 conc
= Rewriter::rewrite( conc
);
797 new_nodes
.push_back( conc
);
798 d_simpl_neg_cache
[p
] = conc
;
801 void RegExpOpr::simplifyPRegExp( Node s
, Node r
, std::vector
< Node
> &new_nodes
) {
802 std::pair
< Node
, Node
> p(s
, r
);
803 std::map
< std::pair
< Node
, Node
>, Node
>::const_iterator itr
= d_simpl_cache
.find(p
);
804 if(itr
!= d_simpl_cache
.end()) {
805 new_nodes
.push_back( itr
->second
);
811 case kind::REGEXP_EMPTY
: {
815 case kind::REGEXP_SIGMA
: {
816 conc
= d_one
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH
, s
));
819 case kind::STRING_TO_REGEXP
: {
820 conc
= s
.eqNode(r
[0]);
823 case kind::REGEXP_CONCAT
: {
824 std::vector
< Node
> nvec
;
825 std::vector
< Node
> cc
;
826 bool emptyflag
= false;
827 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
828 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
829 cc
.push_back( r
[i
][0] );
830 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
834 Node sk
= NodeManager::currentNM()->mkSkolem( "rc_$$", s
.getType(), "created for regular expression concat" );
835 Node lem
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, sk
, r
[i
]);
843 Node lem
= s
.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
, cc
) );
845 conc
= nvec
.size() == 1 ? nvec
[0] : NodeManager::currentNM()->mkNode(kind::AND
, nvec
);
849 case kind::REGEXP_UNION
: {
850 std::vector
< Node
> c_or
;
851 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
852 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
853 c_or
.push_back( r
[i
][0].eqNode(s
) );
854 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
857 c_or
.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[i
]));
860 conc
= c_or
.size() == 0 ? d_false
:
861 c_or
.size() == 1 ? c_or
[0] : NodeManager::currentNM()->mkNode(kind::OR
, c_or
);
864 case kind::REGEXP_INTER
: {
865 std::vector
< Node
> c_and
;
866 bool emptyflag
= false;
867 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
868 if(r
[i
].getKind() == kind::STRING_TO_REGEXP
) {
869 c_and
.push_back( r
[i
][0].eqNode(s
) );
870 } else if(r
[i
].getKind() == kind::REGEXP_EMPTY
) {
874 c_and
.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[i
]));
880 conc
= c_and
.size() == 1 ? c_and
[0] : NodeManager::currentNM()->mkNode(kind::AND
, c_and
);
884 case kind::REGEXP_STAR
: {
885 if(s
== d_emptyString
) {
887 } else if(r
[0].getKind() == kind::REGEXP_EMPTY
) {
888 conc
= s
.eqNode(d_emptyString
);
889 } else if(r
[0].getKind() == kind::REGEXP_SIGMA
) {
892 Node se
= s
.eqNode(d_emptyString
);
893 Node sinr
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, s
, r
[0]);
894 Node sk1
= NodeManager::currentNM()->mkSkolem( "rs_$$", s
.getType(), "created for regular expression star" );
895 Node sk2
= NodeManager::currentNM()->mkSkolem( "rs_$$", s
.getType(), "created for regular expression star" );
896 Node s1nz
= sk1
.eqNode(d_emptyString
).negate();
897 Node s2nz
= sk2
.eqNode(d_emptyString
).negate();
898 Node s1inr
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, sk1
, r
[0]);
899 Node s2inrs
= NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP
, sk2
, r
);
900 Node s12
= s
.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT
, sk1
, sk2
));
902 conc
= NodeManager::currentNM()->mkNode(kind::AND
, s12
, s1nz
, s2nz
, s1inr
, s2inrs
);
903 conc
= NodeManager::currentNM()->mkNode(kind::OR
, se
, sinr
, conc
);
908 Trace("strings-regexp") << "Unsupported term: " << r
<< " in simplifyPRegExp." << std::endl
;
909 AlwaysAssert( false, "Unsupported Term" );
912 conc
= Rewriter::rewrite( conc
);
913 new_nodes
.push_back( conc
);
914 d_simpl_cache
[p
] = conc
;
919 std::string
RegExpOpr::niceChar( Node r
) {
921 std::string s
= r
.getConst
<CVC4::String
>().toString() ;
922 return s
== "" ? "{E}" : ( s
== " " ? "{ }" : s
);
927 std::string
RegExpOpr::mkString( Node r
) {
934 case kind::REGEXP_EMPTY
: {
938 case kind::REGEXP_SIGMA
: {
942 case kind::STRING_TO_REGEXP
: {
943 retStr
+= niceChar( r
[0] );
946 case kind::REGEXP_CONCAT
: {
948 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
949 if(i
!= 0) retStr
+= ".";
950 retStr
+= mkString( r
[i
] );
955 case kind::REGEXP_UNION
: {
960 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
961 if(i
!= 0) retStr
+= "|";
962 retStr
+= mkString( r
[i
] );
968 case kind::REGEXP_INTER
: {
970 for(unsigned i
=0; i
<r
.getNumChildren(); ++i
) {
971 if(i
!= 0) retStr
+= "&";
972 retStr
+= mkString( r
[i
] );
977 case kind::REGEXP_STAR
: {
978 retStr
+= mkString( r
[0] );
982 case kind::REGEXP_PLUS
: {
983 retStr
+= mkString( r
[0] );
987 case kind::REGEXP_OPT
: {
988 retStr
+= mkString( r
[0] );
992 case kind::REGEXP_RANGE
: {
994 retStr
+= niceChar( r
[0] );
996 retStr
+= niceChar( r
[1] );
1001 Trace("strings-error") << "Unsupported term: " << r
<< " in RegExp." << std::endl
;
1002 //AlwaysAssert( false );
1003 //return Node::null();
1010 }/* CVC4::theory::strings namespace */
1011 }/* CVC4::theory namespace */
1012 }/* CVC4 namespace */