diff options
Diffstat (limited to 'src/theory/strings/regexp_operation.cpp')
| -rw-r--r-- | src/theory/strings/regexp_operation.cpp | 530 |
1 files changed, 330 insertions, 200 deletions
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index e608a0533..6869e45f3 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -34,10 +34,16 @@ namespace strings { RegExpOpr::RegExpOpr() {
d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
+ d_true = NodeManager::currentNM()->mkConst( true );
+ d_false = NodeManager::currentNM()->mkConst( false );
+ d_emptyRegexp = NodeManager::currentNM()->mkConst( kind::REGEXP_EMPTY );
+ d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
+ d_one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
// All Charactors = all printable ones 32-126
d_char_start = 'a';//' ';
d_char_end = 'c';//'~';
d_sigma = mkAllExceptOne( '\0' );
+ //d_sigma = NodeManager::currentNM()->mkConst( kind::REGEXP_SIGMA );
d_sigma_star = NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, d_sigma );
}
@@ -79,8 +85,15 @@ int RegExpOpr::delta( Node r ) { } else {
int k = r.getKind();
switch( k ) {
- case kind::STRING_TO_REGEXP:
- {
+ case kind::REGEXP_EMPTY: {
+ ret = 2;
+ break;
+ }
+ case kind::REGEXP_SIGMA: {
+ ret = 2;
+ break;
+ }
+ case kind::STRING_TO_REGEXP: {
if(r[0].isConst()) {
if(r[0] == d_emptyString) {
ret = 1;
@@ -90,10 +103,9 @@ int RegExpOpr::delta( Node r ) { } else {
ret = 0;
}
- }
break;
- case kind::REGEXP_CONCAT:
- {
+ }
+ case kind::REGEXP_CONCAT: {
bool flag = false;
for(unsigned i=0; i<r.getNumChildren(); ++i) {
int tmp = delta( r[i] );
@@ -107,10 +119,9 @@ int RegExpOpr::delta( Node r ) { if(!flag && ret != 2) {
ret = 1;
}
- }
break;
- case kind::REGEXP_OR:
- {
+ }
+ case kind::REGEXP_UNION: {
bool flag = false;
for(unsigned i=0; i<r.getNumChildren(); ++i) {
int tmp = delta( r[i] );
@@ -124,10 +135,9 @@ int RegExpOpr::delta( Node r ) { if(!flag && ret != 1) {
ret = 2;
}
- }
break;
- case kind::REGEXP_INTER:
- {
+ }
+ case kind::REGEXP_INTER: {
bool flag = true;
for(unsigned i=0; i<r.getNumChildren(); ++i) {
int tmp = delta( r[i] );
@@ -142,33 +152,29 @@ int RegExpOpr::delta( Node r ) { if(flag) {
ret = 1;
}
- }
break;
- case kind::REGEXP_STAR:
- {
- ret = 1;
}
+ case kind::REGEXP_STAR: {
+ ret = 1;
break;
- case kind::REGEXP_PLUS:
- {
- ret = delta( r[0] );
}
+ case kind::REGEXP_PLUS: {
+ ret = delta( r[0] );
break;
- case kind::REGEXP_OPT:
- {
- ret = 1;
}
+ case kind::REGEXP_OPT: {
+ ret = 1;
break;
- case kind::REGEXP_RANGE:
- {
- ret = 2;
}
+ case kind::REGEXP_RANGE: {
+ ret = 2;
break;
- default:
- //TODO: special sym: sigma, none, all
+ }
+ default: {
Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in delta of RegExp." << std::endl;
- //AlwaysAssert( false );
+ AlwaysAssert( false );
//return Node::null();
+ }
}
d_delta_cache[r] = ret;
}
@@ -176,63 +182,69 @@ int RegExpOpr::delta( Node r ) { return ret;
}
-//null - no solution
Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) {
Assert( c.size() < 2 );
Trace("strings-regexp-derivative") << "RegExp-derivative starts with R{ " << mkString( r ) << " }, c=" << c << std::endl;
- Node retNode = Node::null();
+ Node retNode = d_emptyRegexp;
PairDvStr dv = std::make_pair( r, c );
if( d_dv_cache.find( dv ) != d_dv_cache.end() ) {
retNode = d_dv_cache[dv];
} else if( c.isEmptyString() ){
int tmp = delta( r );
if(tmp == 0) {
- retNode = Node::null();
// TODO variable
+ retNode = d_emptyRegexp;
} else if(tmp == 1) {
retNode = r;
} else {
- retNode = Node::null();
+ retNode = d_emptyRegexp;
}
} else {
int k = r.getKind();
switch( k ) {
- case kind::STRING_TO_REGEXP:
- {
+ case kind::REGEXP_EMPTY: {
+ retNode = d_emptyRegexp;
+ break;
+ }
+ case kind::REGEXP_SIGMA: {
+ retNode = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, d_emptyString );
+ break;
+ }
+ case kind::STRING_TO_REGEXP: {
if(r[0].isConst()) {
if(r[0] == d_emptyString) {
- retNode = Node::null();
+ retNode = d_emptyRegexp;
} else {
if(r[0].getConst< CVC4::String >().getFirstChar() == c.getFirstChar()) {
- retNode = r[0].getConst< CVC4::String >().size() == 1 ? d_emptyString : NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP,
- NodeManager::currentNM()->mkConst( r[0].getConst< CVC4::String >().substr(1) ) );
+ retNode = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP,
+ r[0].getConst< CVC4::String >().size() == 1 ? d_emptyString : NodeManager::currentNM()->mkConst( r[0].getConst< CVC4::String >().substr(1) ) );
} else {
- retNode = Node::null();
+ retNode = d_emptyRegexp;
}
}
} else {
- retNode = Node::null();
// TODO variable
+ retNode = d_emptyRegexp;
}
- }
break;
- case kind::REGEXP_CONCAT:
- {
+ }
+ case kind::REGEXP_CONCAT: {
+ Node rees = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, d_emptyString );
std::vector< Node > vec_nodes;
for(unsigned i=0; i<r.getNumChildren(); ++i) {
Node dc = derivativeSingle(r[i], c);
- if(!dc.isNull()) {
+ if(dc != d_emptyRegexp) {
std::vector< Node > vec_nodes2;
- if(dc != d_emptyString) {
+ if(dc != rees) {
vec_nodes2.push_back( dc );
}
for(unsigned j=i+1; j<r.getNumChildren(); ++j) {
- if(r[j] != d_emptyString) {
+ if(r[j] != rees) {
vec_nodes2.push_back( r[j] );
}
}
- Node tmp = vec_nodes2.size()==0 ? d_emptyString :
- ( vec_nodes2.size()==1 ? vec_nodes2[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, vec_nodes2 ) );
+ Node tmp = vec_nodes2.size()==0 ? rees :
+ vec_nodes2.size()==1 ? vec_nodes2[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, vec_nodes2 );
if(std::find(vec_nodes.begin(), vec_nodes.end(), tmp) == vec_nodes.end()) {
vec_nodes.push_back( tmp );
}
@@ -242,34 +254,32 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) { break;
}
}
- retNode = vec_nodes.size() == 0 ? Node::null() :
- ( vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes ) );
- }
+ retNode = vec_nodes.size() == 0 ? d_emptyRegexp :
+ ( vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_UNION, vec_nodes ) );
break;
- case kind::REGEXP_OR:
- {
+ }
+ case kind::REGEXP_UNION: {
std::vector< Node > vec_nodes;
for(unsigned i=0; i<r.getNumChildren(); ++i) {
Node dc = derivativeSingle(r[i], c);
- if(!dc.isNull()) {
+ if(dc != d_emptyRegexp) {
if(std::find(vec_nodes.begin(), vec_nodes.end(), dc) == vec_nodes.end()) {
vec_nodes.push_back( dc );
}
}
Trace("strings-regexp-derivative") << "RegExp-derivative OR R[" << i << "]{ " << mkString(r[i]) << " returns " << mkString(dc) << std::endl;
}
- retNode = vec_nodes.size() == 0 ? Node::null() :
- ( vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes ) );
- }
+ retNode = vec_nodes.size() == 0 ? d_emptyRegexp :
+ ( vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_UNION, vec_nodes ) );
break;
- case kind::REGEXP_INTER:
- {
+ }
+ case kind::REGEXP_INTER: {
bool flag = true;
bool flag_sg = false;
std::vector< Node > vec_nodes;
for(unsigned i=0; i<r.getNumChildren(); ++i) {
Node dc = derivativeSingle(r[i], c);
- if(!dc.isNull()) {
+ if(dc != d_emptyRegexp) {
if(dc == d_sigma_star) {
flag_sg = true;
} else {
@@ -286,56 +296,31 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) { if(vec_nodes.size() == 0 && flag_sg) {
retNode = d_sigma_star;
} else {
- retNode = vec_nodes.size() == 0 ? Node::null() :
+ retNode = vec_nodes.size() == 0 ? d_emptyRegexp :
( vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_INTER, vec_nodes ) );
}
} else {
- retNode = Node::null();
+ retNode = d_emptyRegexp;
}
- }
break;
- case kind::REGEXP_STAR:
- {
- Node dc = derivativeSingle(r[0], c);
- if(!dc.isNull()) {
- retNode = dc==d_emptyString ? r : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, dc, r );
- } else {
- retNode = Node::null();
- }
}
- break;
- case kind::REGEXP_PLUS:
- {
+ case kind::REGEXP_STAR: {
Node dc = derivativeSingle(r[0], c);
- if(!dc.isNull()) {
- retNode = dc==d_emptyString ? r : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, dc, r );
+ if(dc != d_emptyRegexp) {
+ retNode = dc==NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, d_emptyString ) ? r : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, dc, r );
} else {
- retNode = Node::null();
+ retNode = d_emptyRegexp;
}
- }
- break;
- case kind::REGEXP_OPT:
- {
- retNode = derivativeSingle(r[0], c);
- }
break;
- case kind::REGEXP_RANGE:
- {
- char ch = c.getFirstChar();
- if (ch >= r[0].getConst< CVC4::String >().getFirstChar() && ch <= r[1].getConst< CVC4::String >().getFirstChar() ) {
- retNode = d_emptyString;
- } else {
- retNode = Node::null();
- }
}
- break;
- default:
+ default: {
//TODO: special sym: sigma, none, all
Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in derivative of RegExp." << std::endl;
- //AlwaysAssert( false );
+ Assert( false, "Unsupported Term" );
//return Node::null();
+ }
}
- if(!retNode.isNull()) {
+ if(retNode != d_emptyRegexp) {
retNode = Rewriter::rewrite( retNode );
}
d_dv_cache[dv] = retNode;
@@ -368,7 +353,7 @@ bool RegExpOpr::guessLength( Node r, int &co ) { return true;
}
break;
- case kind::REGEXP_OR:
+ case kind::REGEXP_UNION:
{
int g_co;
for(unsigned i=0; i<r.getNumChildren(); ++i) {
@@ -474,7 +459,7 @@ bool RegExpOpr::follow( Node r, CVC4::String c, std::vector< char > &vec_chars ) return true;
}
break;
- case kind::REGEXP_OR:
+ case kind::REGEXP_UNION:
{
bool flag = false;
for(unsigned i=0; i<r.getNumChildren(); ++i) {
@@ -557,7 +542,7 @@ Node RegExpOpr::mkAllExceptOne( char exp_c ) { vec_nodes.push_back( n );
}
}
- return NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes );
+ return NodeManager::currentNM()->mkNode( kind::REGEXP_UNION, vec_nodes );
}
Node RegExpOpr::complement( Node r ) {
@@ -590,7 +575,7 @@ Node RegExpOpr::complement( Node r ) { }
Node tmp = NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, r, d_sigma, d_sigma_star );
vec_nodes.push_back( tmp );
- retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes );
+ retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_UNION, vec_nodes );
}
} else {
Trace("strings-error") << "Unsupported string variable: " << r[0] << " in complement of RegExp." << std::endl;
@@ -613,10 +598,10 @@ Node RegExpOpr::complement( Node r ) { }
vec_nodes.push_back( tmp );
}
- retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes );
+ retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_UNION, vec_nodes );
}
break;
- case kind::REGEXP_OR:
+ case kind::REGEXP_UNION:
{
std::vector< Node > vec_nodes;
for(unsigned i=0; i<r.getNumChildren(); ++i) {
@@ -633,7 +618,7 @@ Node RegExpOpr::complement( Node r ) { Node tmp = complement( r[i] );
vec_nodes.push_back( tmp );
}
- retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes );
+ retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_UNION, vec_nodes );
}
break;
case kind::REGEXP_STAR:
@@ -657,13 +642,163 @@ Node RegExpOpr::complement( Node r ) { }
//simplify
-void RegExpOpr::simplify(Node t, std::vector< Node > &new_nodes) {
+void RegExpOpr::simplify(Node t, std::vector< Node > &new_nodes, bool polarity) {
+ Trace("strings-regexp-simpl") << "RegExp-Simpl starts with " << t << ", polarity=" << polarity << std::endl;
Assert(t.getKind() == kind::STRING_IN_REGEXP);
Node str = Rewriter::rewrite(t[0]);
Node re = Rewriter::rewrite(t[1]);
- simplifyRegExp( str, re, new_nodes );
+ if(polarity) {
+ simplifyPRegExp( str, re, new_nodes );
+ } else {
+ simplifyNRegExp( str, re, new_nodes );
+ }
+ Trace("strings-regexp-simpl") << "RegExp-Simpl returns (" << new_nodes.size() << "):\n";
+ for(unsigned i=0; i<new_nodes.size(); i++) {
+ Trace("strings-regexp-simpl") << "\t" << new_nodes[i] << std::endl;
+ }
}
-void RegExpOpr::simplifyRegExp( Node s, Node r, std::vector< Node > &new_nodes ) {
+void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes ) {
+ std::pair < Node, Node > p(s, r);
+ std::map < std::pair< Node, Node >, Node >::const_iterator itr = d_simpl_neg_cache.find(p);
+ if(itr != d_simpl_neg_cache.end()) {
+ new_nodes.push_back( itr->second );
+ return;
+ } else {
+ int k = r.getKind();
+ Node conc;
+ switch( k ) {
+ case kind::REGEXP_EMPTY: {
+ conc = d_true;
+ break;
+ }
+ case kind::REGEXP_SIGMA: {
+ conc = d_one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s)).negate();
+ break;
+ }
+ case kind::STRING_TO_REGEXP: {
+ conc = s.eqNode(r[0]).negate();
+ break;
+ }
+ case kind::REGEXP_CONCAT: {
+ //TODO: rewrite empty
+ Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
+ Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);
+ Node g1 = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode(kind::GEQ, b1, d_zero),
+ NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s), b1 ) );
+ Node s1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
+ Node s2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
+ Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, s1, s2);
+ Node s12 = s.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s1, s2));
+ Node s1len = b1.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s1));
+ Node s1r1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s1, r[0]).negate();
+ if(r[0].getKind() == kind::STRING_TO_REGEXP) {
+ s1r1 = s1.eqNode(r[0][0]).negate();
+ } else if(r[0].getKind() == kind::REGEXP_EMPTY) {
+ s1r1 = d_true;
+ }
+ Node r2 = r[1];
+ if(r.getNumChildren() > 2) {
+ std::vector< Node > nvec;
+ for(unsigned i=1; i<r.getNumChildren(); i++) {
+ nvec.push_back( r[i] );
+ }
+ r2 = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, nvec);
+ }
+ r2 = Rewriter::rewrite(r2);
+ Node s2r2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s2, r2).negate();
+ if(r2.getKind() == kind::STRING_TO_REGEXP) {
+ s2r2 = s2.eqNode(r2[0]).negate();
+ } else if(r2.getKind() == kind::REGEXP_EMPTY) {
+ s2r2 = d_true;
+ }
+
+ conc = NodeManager::currentNM()->mkNode(kind::OR, s1r1, s2r2);
+ conc = NodeManager::currentNM()->mkNode(kind::AND, s12, s1len, conc);
+ conc = NodeManager::currentNM()->mkNode(kind::EXISTS, b2v, conc);
+ conc = NodeManager::currentNM()->mkNode(kind::IMPLIES, g1, conc);
+ conc = NodeManager::currentNM()->mkNode(kind::FORALL, b1v, conc);
+ break;
+ }
+ case kind::REGEXP_UNION: {
+ std::vector< Node > c_and;
+ for(unsigned i=0; i<r.getNumChildren(); ++i) {
+ if(r[i].getKind() == kind::STRING_TO_REGEXP) {
+ c_and.push_back( r[i][0].eqNode(s).negate() );
+ } else if(r[i].getKind() == kind::REGEXP_EMPTY) {
+ continue;
+ } else {
+ c_and.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s, r[i]).negate());
+ }
+ }
+ conc = c_and.size() == 0 ? d_true :
+ c_and.size() == 1 ? c_and[0] : NodeManager::currentNM()->mkNode(kind::AND, c_and);
+ break;
+ }
+ case kind::REGEXP_INTER: {
+ bool emptyflag = false;
+ std::vector< Node > c_or;
+ for(unsigned i=0; i<r.getNumChildren(); ++i) {
+ if(r[i].getKind() == kind::STRING_TO_REGEXP) {
+ c_or.push_back( r[i][0].eqNode(s).negate() );
+ } else if(r[i].getKind() == kind::REGEXP_EMPTY) {
+ emptyflag = true;
+ break;
+ } else {
+ c_or.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s, r[i]).negate());
+ }
+ }
+ if(emptyflag) {
+ conc = d_true;
+ } else {
+ conc = c_or.size() == 1 ? c_or[0] : NodeManager::currentNM()->mkNode(kind::OR, c_or);
+ }
+ break;
+ }
+ case kind::REGEXP_STAR: {
+ if(s == d_emptyString) {
+ conc = d_false;
+ } else if(r[0].getKind() == kind::REGEXP_EMPTY) {
+ conc = s.eqNode(d_emptyString).negate();
+ } else if(r[0].getKind() == kind::REGEXP_SIGMA) {
+ conc = d_false;
+ } else {
+ Node lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s);
+ Node sne = s.eqNode(d_emptyString).negate();
+ Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
+ Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);
+ Node g1 = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode(kind::GEQ, b1, d_one),
+ NodeManager::currentNM()->mkNode( kind::GEQ, lens, b1 ) );
+ //internal
+ Node s1 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, d_zero, b1);
+ Node s2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, b1, NodeManager::currentNM()->mkNode(kind::MINUS, lens, b1));
+ //Node s1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
+ //Node s2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
+ //Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, s1, s2);
+ //Node s12 = s.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s1, s2));
+ //Node s1len = b1.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s1));
+ Node s1r1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s1, r[0]).negate();
+ Node s2r2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s2, r).negate();
+
+ conc = NodeManager::currentNM()->mkNode(kind::OR, s1r1, s2r2);
+ //conc = NodeManager::currentNM()->mkNode(kind::AND, s12, s1len, conc);
+ //conc = NodeManager::currentNM()->mkNode(kind::EXISTS, b2v, conc);
+ conc = NodeManager::currentNM()->mkNode(kind::IMPLIES, g1, conc);
+ conc = NodeManager::currentNM()->mkNode(kind::FORALL, b1v, conc);
+ conc = NodeManager::currentNM()->mkNode(kind::AND, sne, conc);
+ }
+ break;
+ }
+ default: {
+ Trace("strings-regexp") << "Unsupported term: " << r << " in simplifyNRegExp." << std::endl;
+ AlwaysAssert( false, "Unsupported Term" );
+ }
+ }
+ conc = Rewriter::rewrite( conc );
+ new_nodes.push_back( conc );
+ d_simpl_neg_cache[p] = conc;
+ }
+}
+void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes ) {
std::pair < Node, Node > p(s, r);
std::map < std::pair< Node, Node >, Node >::const_iterator itr = d_simpl_cache.find(p);
if(itr != d_simpl_cache.end()) {
@@ -671,34 +806,24 @@ void RegExpOpr::simplifyRegExp( Node s, Node r, std::vector< Node > &new_nodes ) return;
} else {
int k = r.getKind();
+ Node conc;
switch( k ) {
- case kind::REGEXP_EMPTY:
- {
- Node eq = NodeManager::currentNM()->mkConst( false );
- new_nodes.push_back( eq );
- d_simpl_cache[p] = eq;
- }
+ case kind::REGEXP_EMPTY: {
+ conc = d_false;
break;
- case kind::REGEXP_SIGMA:
- {
- Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
- Node eq = one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s));
- new_nodes.push_back( eq );
- d_simpl_cache[p] = eq;
}
+ case kind::REGEXP_SIGMA: {
+ conc = d_one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s));
break;
- case kind::STRING_TO_REGEXP:
- {
- Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, r[0] );
- new_nodes.push_back( eq );
- d_simpl_cache[p] = eq;
}
+ case kind::STRING_TO_REGEXP: {
+ conc = s.eqNode(r[0]);
break;
- case kind::REGEXP_CONCAT:
- {
+ }
+ case kind::REGEXP_CONCAT: {
+ std::vector< Node > nvec;
std::vector< Node > cc;
bool emptyflag = false;
- Node ff = NodeManager::currentNM()->mkConst( false );
for(unsigned i=0; i<r.getNumChildren(); ++i) {
if(r[i].getKind() == kind::STRING_TO_REGEXP) {
cc.push_back( r[i][0] );
@@ -706,71 +831,87 @@ void RegExpOpr::simplifyRegExp( Node s, Node r, std::vector< Node > &new_nodes ) emptyflag = true;
break;
} else {
- Node sk = NodeManager::currentNM()->mkSkolem( "rcon_$$", s.getType(), "created for regular expression concat" );
- simplifyRegExp( sk, r[i], new_nodes );
- if(new_nodes.size() != 0) {
- if(new_nodes[new_nodes.size() - 1] == ff) {
- emptyflag = true;
- break;
- }
- }
- cc.push_back( sk );
+ Node sk = NodeManager::currentNM()->mkSkolem( "rc_$$", s.getType(), "created for regular expression concat" );
+ Node lem = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, sk, r[i]);
+ nvec.push_back(lem);
+ cc.push_back(sk);
}
}
if(emptyflag) {
- new_nodes.push_back( ff );
- d_simpl_cache[p] = ff;
+ conc = d_false;
} else {
- Node cc_eq = s.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, cc) );
- new_nodes.push_back( cc_eq );
- d_simpl_cache[p] = cc_eq;
+ Node lem = s.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, cc) );
+ nvec.push_back(lem);
+ conc = nvec.size() == 1 ? nvec[0] : NodeManager::currentNM()->mkNode(kind::AND, nvec);
}
- }
break;
- case kind::REGEXP_OR:
- {
+ }
+ case kind::REGEXP_UNION: {
std::vector< Node > c_or;
for(unsigned i=0; i<r.getNumChildren(); ++i) {
- simplifyRegExp( s, r[i], c_or );
+ if(r[i].getKind() == kind::STRING_TO_REGEXP) {
+ c_or.push_back( r[i][0].eqNode(s) );
+ } else if(r[i].getKind() == kind::REGEXP_EMPTY) {
+ continue;
+ } else {
+ c_or.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s, r[i]));
+ }
}
- Node eq = NodeManager::currentNM()->mkNode( kind::OR, c_or );
- new_nodes.push_back( eq );
- d_simpl_cache[p] = eq;
- }
+ conc = c_or.size() == 0 ? d_false :
+ c_or.size() == 1 ? c_or[0] : NodeManager::currentNM()->mkNode(kind::OR, c_or);
break;
- case kind::REGEXP_INTER:
- {
- Node nfalse = NodeManager::currentNM()->mkConst( false );
+ }
+ case kind::REGEXP_INTER: {
+ std::vector< Node > c_and;
+ bool emptyflag = false;
for(unsigned i=0; i<r.getNumChildren(); ++i) {
- simplifyRegExp( s, r[i], new_nodes );
- if(new_nodes.size() != 0) {
- if(new_nodes[new_nodes.size() - 1] == nfalse) {
- break;
- }
+ if(r[i].getKind() == kind::STRING_TO_REGEXP) {
+ c_and.push_back( r[i][0].eqNode(s) );
+ } else if(r[i].getKind() == kind::REGEXP_EMPTY) {
+ emptyflag = true;
+ break;
+ } else {
+ c_and.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s, r[i]));
}
}
- }
+ if(emptyflag) {
+ conc = d_false;
+ } else {
+ conc = c_and.size() == 1 ? c_and[0] : NodeManager::currentNM()->mkNode(kind::AND, c_and);
+ }
break;
- case kind::REGEXP_STAR:
- {
- Node eq;
- if(r[0].getKind() == kind::REGEXP_EMPTY) {
- eq = NodeManager::currentNM()->mkConst( false );
+ }
+ case kind::REGEXP_STAR: {
+ if(s == d_emptyString) {
+ conc = d_true;
+ } else if(r[0].getKind() == kind::REGEXP_EMPTY) {
+ conc = s.eqNode(d_emptyString);
} else if(r[0].getKind() == kind::REGEXP_SIGMA) {
- eq = NodeManager::currentNM()->mkConst( true );
+ conc = d_true;
} else {
- eq = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, s, r );
+ Node se = s.eqNode(d_emptyString);
+ Node sinr = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s, r[0]);
+ Node sk1 = NodeManager::currentNM()->mkSkolem( "rs_$$", s.getType(), "created for regular expression star" );
+ Node sk2 = NodeManager::currentNM()->mkSkolem( "rs_$$", s.getType(), "created for regular expression star" );
+ Node s1nz = sk1.eqNode(d_emptyString).negate();
+ Node s2nz = sk2.eqNode(d_emptyString).negate();
+ Node s1inr = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, sk1, r[0]);
+ Node s2inrs = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, sk2, r);
+ Node s12 = s.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sk1, sk2));
+
+ conc = NodeManager::currentNM()->mkNode(kind::AND, s12, s1nz, s2nz, s1inr, s2inrs);
+ conc = NodeManager::currentNM()->mkNode(kind::OR, se, sinr, conc);
}
- new_nodes.push_back( eq );
- d_simpl_cache[p] = eq;
- }
- break;
- default:
- //TODO: special sym: sigma, none, all
- Trace("strings-preprocess") << "Unsupported term: " << r << " in simplifyRegExp." << std::endl;
- Assert( false );
break;
+ }
+ default: {
+ Trace("strings-regexp") << "Unsupported term: " << r << " in simplifyPRegExp." << std::endl;
+ AlwaysAssert( false, "Unsupported Term" );
+ }
}
+ conc = Rewriter::rewrite( conc );
+ new_nodes.push_back( conc );
+ d_simpl_cache[p] = conc;
}
}
@@ -790,33 +931,28 @@ std::string RegExpOpr::mkString( Node r ) { } else {
int k = r.getKind();
switch( k ) {
- case kind::REGEXP_EMPTY:
- {
+ case kind::REGEXP_EMPTY: {
retStr += "Empty";
- }
break;
- case kind::REGEXP_SIGMA:
- {
- retStr += "{W}";
}
+ case kind::REGEXP_SIGMA: {
+ retStr += "{W}";
break;
- case kind::STRING_TO_REGEXP:
- {
- retStr += niceChar( r[0] );
}
+ case kind::STRING_TO_REGEXP: {
+ retStr += niceChar( r[0] );
break;
- case kind::REGEXP_CONCAT:
- {
+ }
+ case kind::REGEXP_CONCAT: {
retStr += "(";
for(unsigned i=0; i<r.getNumChildren(); ++i) {
if(i != 0) retStr += ".";
retStr += mkString( r[i] );
}
retStr += ")";
- }
break;
- case kind::REGEXP_OR:
- {
+ }
+ case kind::REGEXP_UNION: {
if(r == d_sigma) {
retStr += "{A}";
} else {
@@ -827,47 +963,41 @@ std::string RegExpOpr::mkString( Node r ) { }
retStr += ")";
}
- }
break;
- case kind::REGEXP_INTER:
- {
+ }
+ case kind::REGEXP_INTER: {
retStr += "(";
for(unsigned i=0; i<r.getNumChildren(); ++i) {
if(i != 0) retStr += "&";
retStr += mkString( r[i] );
}
retStr += ")";
- }
break;
- case kind::REGEXP_STAR:
- {
+ }
+ case kind::REGEXP_STAR: {
retStr += mkString( r[0] );
retStr += "*";
- }
break;
- case kind::REGEXP_PLUS:
- {
+ }
+ case kind::REGEXP_PLUS: {
retStr += mkString( r[0] );
retStr += "+";
- }
break;
- case kind::REGEXP_OPT:
- {
+ }
+ case kind::REGEXP_OPT: {
retStr += mkString( r[0] );
retStr += "?";
- }
break;
- case kind::REGEXP_RANGE:
- {
+ }
+ case kind::REGEXP_RANGE: {
retStr += "[";
retStr += niceChar( r[0] );
retStr += "-";
retStr += niceChar( r[1] );
retStr += "]";
- }
break;
+ }
default:
- //TODO: special sym: sigma, none, all
Trace("strings-error") << "Unsupported term: " << r << " in RegExp." << std::endl;
//AlwaysAssert( false );
//return Node::null();
|