lexer fix: disable smt-lib conversion for string literals

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 9282486c8dca0796f18454d48704738ac2b23bd0..9c2ac4c1bf68542dba0bd9a9f3558983101ede1a 100644 (file)
--- 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 10c8ba2b958b416bb1663b0b9f1e96504aec22ea..4c69592d49c643a54d93d453d6330f97e8a822da 100644 (file)
--- 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;
                        }
                  }