text: /*********************                                                        */
  /*! \file regexp.cpp
   ** \verbatim
   ** Top contributors (to current version):
   **   Morgan Deters, Tianyi Liang, Tim King
   ** This file is part of the CVC4 project.
   ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
   ** in the top-level source directory) and their institutional affiliations.
   ** All rights reserved.  See the file COPYING in the top-level source
   ** directory for licensing information.\endverbatim
   **
   ** \brief [[ Add one-line brief description here ]]
   **
   ** [[ Add lengthier description here ]]
   ** \todo document this file
   **/
  
  #include "util/regexp.h"
  
  #include <iomanip>
  #include <iostream>
  
  using namespace std;
  
  namespace CVC4 {
  
  void String::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(isxdigit(s[i+1]) && isxdigit(s[i+2])) {
                  d_str.push_back( convertCharToUnsignedInt( hexToDec(s[i+1]) * 16 + hexToDec(s[i+2]) ) );
                  i += 3;
                } else {
                  throw CVC4::Exception( "Illegal String Literal: \"" + s + "\"" );
                }
              } else {
                throw CVC4::Exception( "Illegal String Literal: \"" + s + "\", must have two digits after \\x" );
              }
            }
            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((unsigned char)num) );
                    i += 3;
                  } else {
                    d_str.push_back( convertCharToUnsignedInt((unsigned char)num) );
                    i += 2;
                  }
                } else {
                  d_str.push_back( convertCharToUnsignedInt((unsigned char)num) );
                  i++;
                }
              } else if((unsigned)s[i] > 127) {
                throw CVC4::Exception( "Illegal String Literal: \"" + s + "\", must use escaped sequence" );
              } else {
                d_str.push_back( convertCharToUnsignedInt(s[i]) );
                i++;
              }
            }
          }
        } else {
          throw CVC4::Exception( "should be handled by lexer: \"" + s + "\"" );
          //d_str.push_back( convertCharToUnsignedInt('\\') );
        }
      } else if((unsigned)s[i] > 127) {
        throw CVC4::Exception( "Illegal String Literal: \"" + s + "\", must use escaped sequence" );
      } else {
        d_str.push_back( convertCharToUnsignedInt(s[i]) );
        i++;
      }
    }
  }
  
  void String::getCharSet(std::set<unsigned char> &cset) const {
    for(std::vector<unsigned int>::const_iterator itr = d_str.begin();
      itr != d_str.end(); itr++) {
        cset.insert( convertUnsignedIntToChar(*itr) );
      }
  }
  
  std::size_t String::overlap(String &y) const {
    std::size_t i = d_str.size() < y.size() ? d_str.size() : y.size();
    for(; i>0; i--) {
      String s = suffix(i);
      String p = y.prefix(i);
      if(s == p) {
        return i;
      }
    }
    return i;
  }
  
  std::string String::toString() const {
    std::string str;
    for(unsigned int i=0; i<d_str.size(); ++i) {
      unsigned 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::stringstream ss;
            ss << std::setfill ('0') << std::setw(2) << std::hex << ((int)c);
            std::string t = ss.str();
            t = t.substr(t.size()-2, 2);
            s = "\\x" + t;
            //std::string s2 = static_cast<std::ostringstream*>( &(std::ostringstream() << (int)c) )->str();
          }
        }
        str += s;
      }
    }
    return str;
  }
  
  std::ostream& operator <<(std::ostream& os, const String& s) {
    return os << "\"" << s.toString() << "\"";
  }
  
  std::ostream& operator<<(std::ostream& out, const RegExp& s) {
    return out << "regexp(" << s.getType() << ')';
  }
  
  }/* CVC4 namespace */
  