From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Wed, 12 Feb 2014 04:50:08 +0000 (-0600)
Subject: lexer fix: disable smt-lib conversion for string literals
X-Git-Tag: cvc5-1.0.0~7092
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d5e776a4119ee765b21cfc2f3c31abcd1c07d4e8;p=cvc5.git

lexer fix: disable smt-lib conversion for string literals
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 9282486c8..9c2ac4c1b 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -196,7 +196,7 @@ parseCommand returns [CVC4::Command* cmd = NULL]
     /* This extended command has to be in the outermost production so that
      * the RPAREN_TOK is properly eaten and we are in a good state to read
      * the included file's tokens. */
-  | LPAREN_TOK INCLUDE_TOK str[name] RPAREN_TOK
+  | LPAREN_TOK INCLUDE_TOK str[name,true] RPAREN_TOK
     { if(!PARSER_STATE->canIncludeFile()) {
         PARSER_STATE->parseError("include-file feature was disabled for this run.");
       }
@@ -708,7 +708,7 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr]
     { sexpr = SExpr(Integer(AntlrInput::tokenText($INTEGER_LITERAL))); }
   | DECIMAL_LITERAL
     { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
-  | str[s]
+  | str[s,false]
     { sexpr = SExpr(s); }
 //  | LPAREN_TOK STRCST_TOK
 //      ( INTEGER_LITERAL {
@@ -1025,7 +1025,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
       std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
       expr = MK_CONST( BitVector(binString, 2) ); }
 
-  | str[s]
+  | str[s,false]
     { expr = MK_CONST( ::CVC4::String(s) ); }
 
     // NOTE: Theory constants go here
@@ -1169,31 +1169,33 @@ termList[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr]
 /**
  * Matches a string, and strips off the quotes.
  */
-str[std::string& s]
+str[std::string& s, bool fsmtlib]
   : STRING_LITERAL
     { s = AntlrInput::tokenText($STRING_LITERAL);
       /* strip off the quotes */
       s = s.substr(1, s.size() - 2);
-      /* handle SMT-LIB standard escapes '\\' and '\"' */
-      char* p_orig = strdup(s.c_str());
-      char *p = p_orig, *q = p_orig;
-      while(*q != '\0') {
-        if(*q == '\\') {
-          ++q;
-          if(*q == '\\' || *q == '"') {
-            *p++ = *q++;
-          } else {
-            assert(*q != '\0');
-            *p++ = '\\';
-            *p++ = *q++;
-          }
-        } else {
-          *p++ = *q++;
-        }
-      }
-      *p = '\0';
-      s = p_orig;
-      free(p_orig);
+	  if(fsmtlib) {
+		  /* handle SMT-LIB standard escapes '\\' and '\"' */
+		  char* p_orig = strdup(s.c_str());
+		  char *p = p_orig, *q = p_orig;
+		  while(*q != '\0') {
+			if(*q == '\\') {
+			  ++q;
+			  if(*q == '\\' || *q == '"') {
+				*p++ = *q++;
+			  } else {
+				assert(*q != '\0');
+				*p++ = '\\';
+				*p++ = *q++;
+			  }
+			} else {
+			  *p++ = *q++;
+			}
+		  }
+		  *p = '\0';
+		  s = p_orig;
+		  free(p_orig);
+	  }
     }
   ;
 
diff --git a/src/util/regexp.h b/src/util/regexp.h
index 10c8ba2b9..4c69592d4 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -124,8 +124,8 @@ private:
 					  }
 				  }
 			  } else {
-				  //throw CVC4::Exception( "Error String Literal: \"" + s + "\"" );
-				  d_str.push_back( convertCharToUnsignedInt('\\') );
+				  throw CVC4::Exception( "should be handled by lexer: \"" + s + "\"" );
+				  //d_str.push_back( convertCharToUnsignedInt('\\') );
 			  }
 		  } else {
 			  d_str.push_back( convertCharToUnsignedInt(s[i]) );
@@ -242,7 +242,7 @@ public:
 	  char c = convertUnsignedIntToChar( d_str[i] );
 	  if(isprint( c )) {
         if(c == '\\') {
-			str += "\\";
+			str += "\\\\";
 		} else if(c == '\"') {
 			str += "\\\"";
 		} else {
@@ -261,6 +261,9 @@ public:
 			case '\e': s = "\\e"; break;
 			default  : {
 				std::string s2 = static_cast<std::ostringstream*>( &(std::ostringstream() << (int)c) )->str();
+				if(s2.size() == 1) {
+					s2 = "0" + s2;
+				}
 				s = "\\x" + s2;
 			}
 		  }