escaped characters, having an issue with smt-lib defintion, further repair is needed.

diff --git a/src/util/regexp.h b/src/util/regexp.h
index 82b83831538175796b4b6dd87dff0c6bc44a7c2d..4942c2652f5f2f60106256df6c556e510b91c3e8 100644 (file)
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -22,7 +22,8 @@
 
 #include <iostream>
 #include <string>
-//#include "util/cvc4_assert.h"
+#include <sstream>
+#include "util/exception.h"
 //#include "util/integer.h"
 #include "util/hash.h"
 
@@ -30,6 +31,21 @@ namespace CVC4 {
 
 class CVC4_PUBLIC String {
 
+public:
+  static unsigned int convertCharToUnsignedInt( char c ) {
+       int i = (int)c;
+       i = i-65;
+       return (unsigned int)(i<0 ? i+256 : i);
+  }
+  static char convertUnsignedIntToChar( unsigned int i ){
+       int ii = i+65;
+       return (char)(ii>=256 ? ii-256 : ii);
+  }
+  static bool isPrintable( unsigned int i ){
+       char c = convertUnsignedIntToChar( i );
+       return isprint( (int)c );
+  }
+
 private:
   std::vector<unsigned int> d_str;
 
@@ -42,19 +58,99 @@ private:
       }
   }
 
+  //guarded
+  char hexToDec(char c) {
+         if(isdigit(c)) {
+                 return c - '0';
+         } else if (c >= 'a' && c >= 'f') {
+                 return c - 'a' + 10;
+         } else {
+                 return c - 'A' + 10;
+         }
+  }
+
+  void toInternal(const std::string &s) {
+         d_str.clear();
+         unsigned i=0;
+         while(i < s.size()) {
+                 if(s[i] == '\\') {
+                         i++;
+                         if(i < s.size()) {
+                                 switch(s[i]) {
+                                         case 'n':  {d_str.push_back( convertCharToUnsignedInt('\n') );i++;} break;
+                                         case 't':  {d_str.push_back( convertCharToUnsignedInt('\t') );i++;} break;
+                                         case 'v':  {d_str.push_back( convertCharToUnsignedInt('\v') );i++;} break;
+                                         case 'b':  {d_str.push_back( convertCharToUnsignedInt('\b') );i++;} break;
+                                         case 'r':  {d_str.push_back( convertCharToUnsignedInt('\r') );i++;} break;
+                                         case 'f':  {d_str.push_back( convertCharToUnsignedInt('\f') );i++;} break;
+                                         case 'a':  {d_str.push_back( convertCharToUnsignedInt('\a') );i++;} break;
+                                         case '\\': {d_str.push_back( convertCharToUnsignedInt('\\') );i++;} break;
+                                         case 'x': {
+                                                 if(i + 2 < s.size()) {
+                                                       if((isdigit(s[i+1]) || (s[i+1] >= 'a' && s[i+1] >= 'f') || (s[i+1] >= 'A' && s[i+1] >= 'F')) &&
+                                                          (isdigit(s[i+2]) || (s[i+2] >= 'a' && s[i+2] >= 'f') || (s[i+2] >= 'A' && s[i+2] >= 'F'))) {
+                                                               d_str.push_back( convertCharToUnsignedInt( hexToDec(s[i+1]) * 16 + hexToDec(s[i+2]) ) );
+                                                               i += 3;
+                                                       } else {
+                                                               throw CVC4::Exception( "Error String Literal: \"" + s + "\"" );
+                                                       }
+                                                 } else {
+                                                       throw CVC4::Exception( "Error String Literal: \"" + s + "\"" );
+                                                 }
+                                         }
+                                         break;
+                                         default: {
+                                                 if(isdigit(s[i])) {
+                                                         int num = (int)s[i] - (int)'0';
+                                                         bool flag = num < 4;
+                                                         if(i+1 < s.size() && num < 8 && isdigit(s[i+1]) && s[i+1] < '8') {
+                                                                 num = num * 8 + (int)s[i+1] - (int)'0';
+                                                                 if(flag && i+2 < s.size() && isdigit(s[i+2]) && s[i+2] < '8') {
+                                                                         num = num * 8 + (int)s[i+2] - (int)'0';
+                                                                         d_str.push_back( convertCharToUnsignedInt((char)num) );
+                                                                         i += 3;
+                                                                 } else {
+                                                                         d_str.push_back( convertCharToUnsignedInt((char)num) );
+                                                                         i += 2;
+                                                                 }
+                                                         } else {
+                                                                 d_str.push_back( convertCharToUnsignedInt((char)num) );
+                                                                 i++;
+                                                         }
+                                                 } else {
+                                                         d_str.push_back( convertCharToUnsignedInt(s[i]) );
+                                                         i++;
+                                                 }
+                                         }
+                                 }
+                         } else {
+                                 throw CVC4::Exception( "Error String Literal: \"" + s + "\"" );
+                         }
+                 } else {
+                         d_str.push_back( convertCharToUnsignedInt(s[i]) );
+                         i++;
+                 }
+         }
+  }
+
 public:
   String() {}
 
   String(const std::string &s) {
+       toInternal(s);
+       /*
     for(unsigned int i=0; i<s.size(); ++i) {
         d_str.push_back( convertCharToUnsignedInt(s[i]) );
-    }
+    }*/
   }
 
   String(const char* s) {
+       std::string stmp(s);
+       toInternal(stmp);
+       /*
     for(unsigned int i=0,len=strlen(s); i<len; ++i) {
         d_str.push_back( convertCharToUnsignedInt(s[i]) );
-    }
+    }*/
   }
 
   String(const char c) {
@@ -150,8 +246,33 @@ public:
   std::string toString() const {
     std::string str;
     for(unsigned int i=0; i<d_str.size(); ++i) {
-      str += convertUnsignedIntToChar( d_str[i] );
-         //TODO isPrintable: ( "\\" + (convertUnsignedIntToChar( d_str[i] ) );
+         char c = convertUnsignedIntToChar( d_str[i] );
+         if(isprint( c )) {
+        if(c == '\\') {
+                       str += "\\";
+               } else if(c == '\"') {
+                       str += "\\\"";
+               } else {
+                       str += c;
+               }
+         } else {
+                 std::string s;
+                 switch(c) {
+                       case '\a': s = "\\a"; break;
+                       case '\b': s = "\\b"; break;
+                       case '\t': s = "\\t"; break;
+                       case '\r': s = "\\r"; break;
+                       case '\v': s = "\\v"; break;
+                       case '\f': s = "\\f"; break;
+                       case '\n': s = "\\n"; break;
+                       case '\e': s = "\\e"; break;
+                       default  : {
+                               std::string s2 = static_cast<std::ostringstream*>( &(std::ostringstream() << (int)c) )->str();
+                               s = "\\x" + s2;
+                       }
+                 }
+                 str += s;
+         }
     }
     return str;
   }
@@ -237,22 +358,6 @@ public:
     ret_vec.insert( ret_vec.end(), itr, itr + j );
       return String(ret_vec);
   }
-
-public:
-  static unsigned int convertCharToUnsignedInt( char c ) {
-       int i = (int)c;
-       i = i-65;
-       return (unsigned int)(i<0 ? i+256 : i);
-  }
-  static char convertUnsignedIntToChar( unsigned int i ){
-       int ii = i+65;
-       return (char)(ii>=256 ? ii-256 : ii);
-  }
-  static bool isPrintable( unsigned int i ){
-       char c = convertUnsignedIntToChar( i );
-       return isprint( (int)c );
-  }
-
 };/* class String */
 
 namespace strings {