diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-11-21 12:36:44 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-12-03 13:54:24 -0600 |
| commit | dcd8e4f1ae0dbc30ce2dda9662f74a3c86a26471 (patch) | |
| tree | f7a640352372dcafcd70d181958722e337ae7e02 /src/theory/strings/regexp_operation.cpp | |
| parent | 0f3345061b504b86a00a6aa66fff239000ebcef3 (diff) | |
string fmf changes
Diffstat (limited to 'src/theory/strings/regexp_operation.cpp')
| -rw-r--r-- | src/theory/strings/regexp_operation.cpp | 78 |
1 files changed, 78 insertions, 0 deletions
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index a3921bb42..f26037cf0 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -30,6 +30,14 @@ RegExpOpr::RegExpOpr() { d_sigma_star = NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, d_sigma );
}
+int RegExpOpr::gcd ( int a, int b ) {
+ int c;
+ while ( a != 0 ) {
+ c = a; a = b%a; b = c;
+ }
+ return b;
+}
+
bool RegExpOpr::checkConstRegExp( Node r ) {
Trace("strings-regexp-cstre") << "RegExp-CheckConstRegExp starts with " << mkString( r ) << std::endl;
bool ret = true;
@@ -325,6 +333,76 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) { return retNode;
}
+//TODO:
+bool RegExpOpr::guessLength( Node r, int &co ) {
+ int k = r.getKind();
+ switch( k ) {
+ case kind::STRING_TO_REGEXP:
+ {
+ if(r[0].isConst()) {
+ co += r[0].getConst< CVC4::String >().size();
+ return true;
+ } else {
+ return false;
+ }
+ }
+ break;
+ case kind::REGEXP_CONCAT:
+ {
+ for(unsigned i=0; i<r.getNumChildren(); ++i) {
+ if(!guessLength( r[i], co)) {
+ return false;
+ }
+ }
+ return true;
+ }
+ break;
+ case kind::REGEXP_OR:
+ {
+ int g_co;
+ for(unsigned i=0; i<r.getNumChildren(); ++i) {
+ int cop = 0;
+ if(!guessLength( r[i], cop)) {
+ return false;
+ }
+ if(i == 0) {
+ g_co = cop;
+ } else {
+ g_co = gcd(g_co, cop);
+ }
+ }
+ return true;
+ }
+ break;
+ case kind::REGEXP_INTER:
+ {
+ int g_co;
+ for(unsigned i=0; i<r.getNumChildren(); ++i) {
+ int cop = 0;
+ if(!guessLength( r[i], cop)) {
+ return false;
+ }
+ if(i == 0) {
+ g_co = cop;
+ } else {
+ g_co = gcd(g_co, cop);
+ }
+ }
+ return true;
+ }
+ break;
+ case kind::REGEXP_STAR:
+ {
+ co = 0;
+ return true;
+ }
+ break;
+ default:
+ Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in membership of RegExp." << std::endl;
+ return false;
+ }
+}
+
void RegExpOpr::firstChar( Node r ) {
Trace("strings-regexp-firstchar") << "Head characters: ";
for(char ch = d_char_start; ch <= d_char_end; ++ch) {
|