diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-11-11 19:45:07 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-11-11 19:45:07 -0600 |
| commit | 3e8490e19b90e57decbfb380001407bcc7d84ca4 (patch) | |
| tree | 5d85782eac5817d53f064d55dba628979a88644a /src/theory/strings/regexp_operation.cpp | |
| parent | 88e9e4a93f0b4b180af94dc4cff931400eb862f1 (diff) | |
length lemma is changed, var-split lemma is changed
Diffstat (limited to 'src/theory/strings/regexp_operation.cpp')
| -rw-r--r-- | src/theory/strings/regexp_operation.cpp | 136 |
1 files changed, 70 insertions, 66 deletions
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index fa686dd9f..a3921bb42 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -237,7 +237,7 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) { vec_nodes.push_back( dc );
}
}
- Trace("strings-regexp-derivative") << "RegExp-derivative OR R[" << i << "]{ " << mkString(r[i]) << " returns " << (dc.isNull() ? "NULL" : mkString(dc) ) << std::endl;
+ 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 ) );
@@ -321,7 +321,7 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) { }
d_dv_cache[dv] = retNode;
}
- Trace("strings-regexp-derivative") << "RegExp-derivative returns : " << ( retNode.isNull() ? "NULL" : mkString( retNode ) ) << std::endl;
+ Trace("strings-regexp-derivative") << "RegExp-derivative returns : " << mkString( retNode ) << std::endl;
return retNode;
}
@@ -577,79 +577,83 @@ std::string RegExpOpr::niceChar( Node r ) { }
std::string RegExpOpr::mkString( Node r ) {
std::string retStr;
- int k = r.getKind();
- switch( k ) {
- case kind::STRING_TO_REGEXP:
- {
- retStr += niceChar( r[0] );
- }
- break;
- case kind::REGEXP_CONCAT:
- {
- retStr += "(";
- for(unsigned i=0; i<r.getNumChildren(); ++i) {
- if(i != 0) retStr += ".";
- retStr += mkString( r[i] );
+ if(r.isNull()) {
+ retStr = "EmptySet";
+ } else {
+ int k = r.getKind();
+ switch( k ) {
+ case kind::STRING_TO_REGEXP:
+ {
+ retStr += niceChar( r[0] );
}
- retStr += ")";
- }
- break;
- case kind::REGEXP_OR:
- {
- if(r == d_sigma) {
- retStr += "{A}";
- } else {
+ break;
+ case kind::REGEXP_CONCAT:
+ {
retStr += "(";
for(unsigned i=0; i<r.getNumChildren(); ++i) {
- if(i != 0) retStr += "|";
+ if(i != 0) retStr += ".";
retStr += mkString( r[i] );
}
retStr += ")";
}
- }
- break;
- case kind::REGEXP_INTER:
- {
- retStr += "(";
- for(unsigned i=0; i<r.getNumChildren(); ++i) {
- if(i != 0) retStr += "&";
- retStr += mkString( r[i] );
+ break;
+ case kind::REGEXP_OR:
+ {
+ if(r == d_sigma) {
+ retStr += "{A}";
+ } else {
+ retStr += "(";
+ for(unsigned i=0; i<r.getNumChildren(); ++i) {
+ if(i != 0) retStr += "|";
+ retStr += mkString( r[i] );
+ }
+ retStr += ")";
+ }
}
- retStr += ")";
- }
- break;
- case kind::REGEXP_STAR:
- {
- retStr += mkString( r[0] );
- retStr += "*";
- }
- break;
- case kind::REGEXP_PLUS:
- {
- retStr += mkString( r[0] );
- retStr += "+";
- }
- break;
- case kind::REGEXP_OPT:
- {
- retStr += mkString( r[0] );
- retStr += "?";
- }
- break;
- case kind::REGEXP_RANGE:
- {
- retStr += "[";
- retStr += niceChar( r[0] );
- retStr += "-";
- retStr += niceChar( r[1] );
- retStr += "]";
+ break;
+ 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:
+ {
+ retStr += mkString( r[0] );
+ retStr += "*";
+ }
+ break;
+ case kind::REGEXP_PLUS:
+ {
+ retStr += mkString( r[0] );
+ retStr += "+";
+ }
+ break;
+ case kind::REGEXP_OPT:
+ {
+ retStr += mkString( r[0] );
+ retStr += "?";
+ }
+ break;
+ 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();
}
- break;
- default:
- //TODO: special sym: sigma, none, all
- Trace("strings-error") << "Unsupported term: " << r << " in RegExp." << std::endl;
- //AlwaysAssert( false );
- //return Node::null();
}
return retStr;
|