From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Tue, 11 Feb 2014 22:35:17 +0000 (-0600)
Subject: escaped characters, having an issue with smt-lib defintion, further repair is needed.
X-Git-Tag: cvc5-1.0.0~7095^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ff739bd2e4227ec3254226de86df3b39e2fa23a9;p=cvc5.git

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 82b838315..4942c2652 100644
--- 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 {