switch ascii encoding to unsigned char

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 2197cd648320ac354665d3edeb3ebf1c5209ab50..72a64ab78fe05fe25f06604ec260ff9d53f24269 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -215,10 +215,12 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     }
 
     case kind::CONST_STRING: {
-      const std::vector<unsigned int>& s = n.getConst<String>().getVec();
+      //const std::vector<unsigned int>& s = n.getConst<String>().getVec();
+      std::string s = n.getConst<String>().toString();
       out << '"';
       for(size_t i = 0; i < s.size(); ++i) {
-        char c = String::convertUnsignedIntToChar(s[i]);
+        //char c = String::convertUnsignedIntToChar(s[i]);
+        char c = s[i];
         if(c == '"') {
           if(d_variant == z3str_variant || d_variant == smt2_0_variant) {
             out << "\\\"";

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 3846c0c073fca4d4828add83919c22103666500e..e09f47f0f767aae608d322b4ca51e1845f841199 100644 (file)
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -651,14 +651,14 @@ bool RegExpOpr::guessLength( Node r, int &co ) {
   }
 }
 
-void RegExpOpr::firstChars( Node r, std::set<char> &pcset, SetNodes &pvset ) {
+void RegExpOpr::firstChars( Node r, std::set<unsigned char> &pcset, SetNodes &pvset ) {
   Trace("regexp-fset") << "Start FSET(" << mkString(r) << ")" << std::endl;
-  std::map< Node, std::pair< std::set<char>, SetNodes > >::const_iterator itr = d_fset_cache.find(r);
+  std::map< Node, std::pair< std::set<unsigned char>, SetNodes > >::const_iterator itr = d_fset_cache.find(r);
   if(itr != d_fset_cache.end()) {
     pcset.insert((itr->second).first.begin(), (itr->second).first.end());
     pvset.insert((itr->second).second.begin(), (itr->second).second.end());
   } else {
-    std::set<char> cset;
+    std::set<unsigned char> cset;
     SetNodes vset;
     int k = r.getKind();
     switch( k ) {
@@ -666,7 +666,7 @@ void RegExpOpr::firstChars( Node r, std::set<char> &pcset, SetNodes &pvset ) {
         break;
       }
       case kind::REGEXP_SIGMA: {
-        for(char i='\0'; i<=d_lastchar; i++) {
+        for(unsigned char i='\0'; i<=d_lastchar; i++) {
           cset.insert(i);
         }
         break;
@@ -727,13 +727,13 @@ void RegExpOpr::firstChars( Node r, std::set<char> &pcset, SetNodes &pvset ) {
     }
     pcset.insert(cset.begin(), cset.end());
     pvset.insert(vset.begin(), vset.end());
-    std::pair< std::set<char>, SetNodes > p(cset, vset);
+    std::pair< std::set<unsigned char>, SetNodes > p(cset, vset);
     d_fset_cache[r] = p;
   }
 
   if(Trace.isOn("regexp-fset")) {
     Trace("regexp-fset") << "END FSET(" << mkString(r) << ") = {";
-    for(std::set<char>::const_iterator itr = pcset.begin();
+    for(std::set<unsigned char>::const_iterator itr = pcset.begin();
       itr != pcset.end(); itr++) {
         if(itr != pcset.begin()) {
           Trace("regexp-fset") << ",";
@@ -744,19 +744,19 @@ void RegExpOpr::firstChars( Node r, std::set<char> &pcset, SetNodes &pvset ) {
   }
 }
 
-bool RegExpOpr::follow( Node r, CVC4::String c, std::vector< char > &vec_chars ) {
+bool RegExpOpr::follow( Node r, CVC4::String c, std::vector< unsigned char > &vec_chars ) {
   int k = r.getKind();
   switch( k ) {
     case kind::STRING_TO_REGEXP:
     {
       if(r[0].isConst()) {
         if(r[0] != d_emptyString) {
-          char t1 = r[0].getConst< CVC4::String >().getFirstChar();
+          unsigned char t1 = r[0].getConst< CVC4::String >().getFirstChar();
           if(c.isEmptyString()) {
             vec_chars.push_back( t1 );
             return true;
           } else {
-            char t2 = c.getFirstChar();
+            unsigned char t2 = c.getFirstChar();
             if(t1 != t2) {
               return false;
             } else {
@@ -805,13 +805,13 @@ bool RegExpOpr::follow( Node r, CVC4::String c, std::vector< char > &vec_chars )
       break;
     case kind::REGEXP_INTER:
     {
-      std::vector< char > vt2;
+      std::vector< unsigned char > vt2;
       for(unsigned i=0; i<r.getNumChildren(); ++i) {
-        std::vector< char > v_tmp;
+        std::vector< unsigned char > v_tmp;
         if( !follow(r[i], c, v_tmp) ) {
           return false;
         }
-        std::vector< char > vt3(vt2);
+        std::vector< unsigned char > vt3(vt2);
         vt2.clear();
         std::set_intersection( vt3.begin(), vt3.end(), v_tmp.begin(), v_tmp.end(), vt2.begin() );
         if(vt2.size() == 0) {
@@ -851,9 +851,9 @@ bool RegExpOpr::follow( Node r, CVC4::String c, std::vector< char > &vec_chars )
   }
 }
 
-Node RegExpOpr::mkAllExceptOne( char exp_c ) {
+Node RegExpOpr::mkAllExceptOne( unsigned char exp_c ) {
   std::vector< Node > vec_nodes;
-  for(char c=d_char_start; c<=d_char_end; ++c) {
+  for(unsigned char c=d_char_start; c<=d_char_end; ++c) {
     if(c != exp_c ) {
       Node n = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst( ::CVC4::String( c ) ) );
       vec_nodes.push_back( n );
@@ -1123,13 +1123,13 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes
   }
 }
 
-void RegExpOpr::getCharSet( Node r, std::set<char> &pcset, SetNodes &pvset ) {
-  std::map< Node, std::pair< std::set<char>, SetNodes > >::const_iterator itr = d_cset_cache.find(r);
+void RegExpOpr::getCharSet( Node r, std::set<unsigned char> &pcset, SetNodes &pvset ) {
+  std::map< Node, std::pair< std::set<unsigned char>, SetNodes > >::const_iterator itr = d_cset_cache.find(r);
   if(itr != d_cset_cache.end()) {
     pcset.insert((itr->second).first.begin(), (itr->second).first.end());
     pvset.insert((itr->second).second.begin(), (itr->second).second.end());
   } else {
-    std::set<char> cset;
+    std::set<unsigned char> cset;
     SetNodes vset;
     int k = r.getKind();
     switch( k ) {
@@ -1137,15 +1137,15 @@ void RegExpOpr::getCharSet( Node r, std::set<char> &pcset, SetNodes &pvset ) {
         break;
       }
       case kind::REGEXP_SIGMA: {
-        for(char i='\0'; i<=d_lastchar; i++) {
+        for(unsigned char i='\0'; i<=d_lastchar; i++) {
           cset.insert(i);
         }
         break;
       }
       case kind::REGEXP_RANGE: {
-        char a = r[0].getConst<String>().getFirstChar();
-        char b = r[1].getConst<String>().getFirstChar();
-        for(char i=a; i<=b; i++) {
+        unsigned char a = r[0].getConst<String>().getFirstChar();
+        unsigned char b = r[1].getConst<String>().getFirstChar();
+        for(unsigned char i=a; i<=b; i++) {
           cset.insert(i);
         }
         break;
@@ -1200,11 +1200,11 @@ void RegExpOpr::getCharSet( Node r, std::set<char> &pcset, SetNodes &pvset ) {
     }
     pcset.insert(cset.begin(), cset.end());
     pvset.insert(vset.begin(), vset.end());
-    std::pair< std::set<char>, SetNodes > p(cset, vset);
+    std::pair< std::set<unsigned char>, SetNodes > p(cset, vset);
     d_cset_cache[r] = p;
 
     Trace("regexp-cset") << "CSET( " << mkString(r) << " ) = { ";
-    for(std::set<char>::const_iterator itr = cset.begin();
+    for(std::set<unsigned char>::const_iterator itr = cset.begin();
       itr != cset.end(); itr++) {
         Trace("regexp-cset") << (*itr) << ",";
       }
@@ -1382,8 +1382,8 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node >
         rNode = itrcache->second;
       } else {
         Trace("regexp-int-debug") << " ... normal without cache" << std::endl;
-        std::vector< char > cset;
-        std::set< char > cset1, cset2;
+        std::vector< unsigned char > cset;
+        std::set< unsigned char > cset1, cset2;
         std::set< Node > vset1, vset2;
         firstChars(r1, cset1, vset1);
         firstChars(r2, cset2, vset2);
@@ -1406,7 +1406,7 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node >
         }
         if(Trace.isOn("regexp-int-debug")) {
           Trace("regexp-int-debug") << "Try CSET(" << cset.size() << ") = {";
-          for(std::vector<char>::const_iterator itr = cset.begin();
+          for(std::vector<unsigned char>::const_iterator itr = cset.begin();
             itr != cset.end(); itr++) {
             //CVC4::String c( *itr );
             if(itr != cset.begin()) {
@@ -1417,7 +1417,7 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node >
           Trace("regexp-int-debug") << std::endl;
         }
         std::map< PairNodes, Node > cacheX;
-        for(std::vector<char>::const_iterator itr = cset.begin();
+        for(std::vector<unsigned char>::const_iterator itr = cset.begin();
           itr != cset.end(); itr++) {
           CVC4::String c( *itr );
           Trace("regexp-int-debug") << "Try character " << c << " ... " << std::endl;
@@ -1555,11 +1555,11 @@ Node RegExpOpr::complement(Node r, int &ret) {
       //TODO: var to be extended
       ret = 0;
     } else {
-      std::set<char> cset;
+      std::set<unsigned char> cset;
       SetNodes vset;
       firstChars(r, cset, vset);
       std::vector< Node > vec_nodes;
-      for(char i=0; i<=d_lastchar; i++) {
+      for(unsigned char i=0; i<=d_lastchar; i++) {
         CVC4::String c(i);
         Node n = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(c));
         Node r2;

diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index d170bd17aed6f9f3481d4618e458b0d45e2097f1..da84ed04ce3d29deccf4104da66555a5f7e220a7 100644 (file)
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -39,7 +39,7 @@ class RegExpOpr {
   typedef std::pair< Node, Node > PairNodes;
 
 private:
-  const char d_lastchar;
+  const unsigned char d_lastchar;
   Node d_emptyString;
   Node d_true;
   Node d_false;
@@ -49,8 +49,8 @@ private:
   Node d_one;
   CVC4::Rational RMAXINT;
 
-  char d_char_start;
-  char d_char_end;
+  unsigned char d_char_start;
+  unsigned char d_char_end;
   Node d_sigma;
   Node d_sigma_star;
 
@@ -61,8 +61,8 @@ private:
   std::map< PairNodeStr, std::pair< Node, int > > d_deriv_cache;
   std::map< Node, std::pair< Node, int > > d_compl_cache;
   std::map< Node, bool > d_cstre_cache;
-  std::map< Node, std::pair< std::set<char>, std::set<Node> > > d_cset_cache;
-  std::map< Node, std::pair< std::set<char>, std::set<Node> > > d_fset_cache;
+  std::map< Node, std::pair< std::set<unsigned char>, std::set<Node> > > d_cset_cache;
+  std::map< Node, std::pair< std::set<unsigned char>, std::set<Node> > > d_fset_cache;
   std::map< PairNodes, Node > d_inter_cache;
   std::map< Node, Node > d_rm_inter_cache;
   std::map< Node, bool > d_norv_cache;
@@ -72,20 +72,20 @@ private:
   void simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes );
   std::string niceChar( Node r );
   int gcd ( int a, int b );
-  Node mkAllExceptOne( char c );
+  Node mkAllExceptOne( unsigned char c );
   bool isPairNodesInSet(std::set< PairNodes > &s, Node n1, Node n2);
 
-  void getCharSet( Node r, std::set<char> &pcset, SetNodes &pvset );
+  void getCharSet( Node r, std::set<unsigned char> &pcset, SetNodes &pvset );
   bool containC2(unsigned cnt, Node n);
   Node convert1(unsigned cnt, Node n);
   void convert2(unsigned cnt, Node n, Node &r1, Node &r2);
   bool testNoRV(Node r);
   Node intersectInternal( Node r1, Node r2, std::map< PairNodes, Node > cache, unsigned cnt );
   Node removeIntersection(Node r);
-  void firstChars( Node r, std::set<char> &pcset, SetNodes &pvset );
+  void firstChars( Node r, std::set<unsigned char> &pcset, SetNodes &pvset );
 
   //TODO: for intersection
-  bool follow( Node r, CVC4::String c, std::vector< char > &vec_chars );
+  bool follow( Node r, CVC4::String c, std::vector< unsigned char > &vec_chars );
 
   /*class CState {
   public:

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 9f683640685aee4e8d216b71132b4686591b47e3..6960659e85b29e3004f1aab33e1a693fb8598305 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -729,9 +729,9 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i
     }
     case kind::REGEXP_RANGE: {
       if(s.size() == index_start + 1) {
-        char a = r[0].getConst<String>().getFirstChar();
-        char b = r[1].getConst<String>().getFirstChar();
-        char c = s.getLastChar();
+        unsigned char a = r[0].getConst<String>().getFirstChar();
+        unsigned char b = r[1].getConst<String>().getFirstChar();
+        unsigned char c = s.getLastChar();
         return (a <= c && c <= b);
       } else {
         return false;
@@ -1130,8 +1130,8 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) {
           node[0]);
   } else if(node.getKind() == kind::REGEXP_RANGE) {
     std::vector< Node > vec_nodes;
-    char c = node[0].getConst<String>().getFirstChar();
-    char end = node[1].getConst<String>().getFirstChar();
+    unsigned char c = node[0].getConst<String>().getFirstChar();
+    unsigned char end = node[1].getConst<String>().getFirstChar();
     for(; c<=end; ++c) {
       Node n = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst( ::CVC4::String( c ) ) );
       vec_nodes.push_back( n );

diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 55059fa77decabafcb86fff232e1a0d96e8f3701..e053f48da232ec7604acef32f22b3098b5ec53a5 100644 (file)
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -349,7 +349,7 @@ public:
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
       TNode::iterator it = n.begin();
-      char ch[2];
+      unsigned char ch[2];
 
       for(int i=0; i<2; ++i) {
         TypeNode t = (*it).getType(check);

diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index 1c672d4b9fb43535b4ed233d9102b4002d51cdbd..24e894678d60f810f083e813b9b036adb1ea920d 100644 (file)
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -60,14 +60,14 @@ void String::toInternal(const std::string &s) {
                 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) );
+                  d_str.push_back( convertCharToUnsignedInt((unsigned char)num) );
                   i += 3;
                 } else {
-                  d_str.push_back( convertCharToUnsignedInt((char)num) );
+                  d_str.push_back( convertCharToUnsignedInt((unsigned char)num) );
                   i += 2;
                 }
               } else {
-                d_str.push_back( convertCharToUnsignedInt((char)num) );
+                d_str.push_back( convertCharToUnsignedInt((unsigned char)num) );
                 i++;
               }
             } else if((unsigned)s[i] > 127) {
@@ -91,7 +91,7 @@ void String::toInternal(const std::string &s) {
   }
 }
 
-void String::getCharSet(std::set<char> &cset) const {
+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) );
@@ -113,7 +113,7 @@ std::size_t String::overlap(String &y) const {
 std::string String::toString() const {
   std::string str;
   for(unsigned int i=0; i<d_str.size(); ++i) {
-    char c = convertUnsignedIntToChar( d_str[i] );
+    unsigned char c = convertUnsignedIntToChar( d_str[i] );
       if(isprint( c )) {
       if(c == '\\') {
         str += "\\\\";

diff --git a/src/util/regexp.h b/src/util/regexp.h
index 26d468a30ff063620025276c2e43434e7844b2e6..c5a094f8c1fbb3111da0ce2eaba4ca09bf83cd02 100644 (file)
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -33,35 +33,36 @@ 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 unsigned convertCharToUnsignedInt( unsigned char c ) {
+    unsigned i = c;
+    i = i + 191;
+    return (i>=256 ? i-256 : i);
   }
-  static char convertUnsignedIntToChar( unsigned int i ){
-    int ii = i+65;
-    return (char)(ii>=256 ? ii-256 : ii);
+  static unsigned char convertUnsignedIntToChar( unsigned i ){
+    unsigned ii = i+65;
+    return (unsigned char)(ii>=256 ? ii-256 : ii);
   }
-  static bool isPrintable( unsigned int i ){
-    char c = convertUnsignedIntToChar( i );
-    return isprint( (int)c );
+  static bool isPrintable( unsigned i ){
+    unsigned char c = convertUnsignedIntToChar( i );
+    return (c>=' ' && c<='~');//isprint( (int)c );
   }
 
 private:
-  std::vector<unsigned int> d_str;
+  std::vector<unsigned> d_str;
 
-  bool isVecSame(const std::vector<unsigned int> &a, const std::vector<unsigned int> &b) const {
+  bool isVecSame(const std::vector<unsigned> &a, const std::vector<unsigned> &b) const {
     if(a.size() != b.size()) return false;
     else {
-      for(unsigned int i=0; i<a.size(); ++i)
-        if(a[i] != b[i]) return false;
-      return true;
+      return std::equal(a.begin(), a.end(), b.begin());
+      //for(unsigned int i=0; i<a.size(); ++i)
+        //if(a[i] != b[i]) return false;
+      //return true;
     }
   }
 
   //guarded
-  char hexToDec(char c) {
-    if(isdigit(c)) {
+  unsigned char hexToDec(unsigned char c) {
+    if(c>='0' && c<='9') {
       return c - '0';
     } else if (c >= 'a' && c <= 'f') {
       return c - 'a' + 10;
@@ -85,11 +86,11 @@ public:
     toInternal(stmp);
   }
 
-  String(const char c) {
+  String(const unsigned char c) {
     d_str.push_back( convertCharToUnsignedInt(c) );
   }
 
-  String(const std::vector<unsigned int> &s) : d_str(s) { }
+  String(const std::vector<unsigned> &s) : d_str(s) { }
 
   ~String() {}
 
@@ -197,15 +198,15 @@ public:
    */
   std::string toString() const;
 
-  unsigned size() const {
+  std::size_t size() const {
     return d_str.size();
   }
 
-  char getFirstChar() const {
+  unsigned char getFirstChar() const {
     return convertUnsignedIntToChar( d_str[0] );
   }
 
-  char getLastChar() const {
+  unsigned char getLastChar() const {
     assert(d_str.size() != 0);
     return convertUnsignedIntToChar( d_str[d_str.size() - 1] );
   }
@@ -239,7 +240,7 @@ public:
     if(y.d_str.size() == 0) return start;
     if(d_str.size() == 0) return std::string::npos;
     std::size_t ret = std::string::npos;
-    for(std::size_t i = start; i <= d_str.size() - y.d_str.size(); i++) {
+    /*for(std::size_t i = start; i <= d_str.size() - y.d_str.size(); i++) {
       if(d_str[i] == y.d_str[0]) {
         std::size_t j=0;
         for(; j<y.d_str.size(); j++) {
@@ -250,6 +251,10 @@ public:
           break;
         }
       }
+    }*/
+    std::vector<unsigned>::const_iterator itr = std::search(d_str.begin(), d_str.end(), y.d_str.begin(), y.d_str.end());
+    if(itr != d_str.end()) {
+      ret = itr - d_str.begin();
     }
     return ret;
   }
@@ -293,7 +298,7 @@ public:
   bool isNumber() const {
    if(d_str.size() == 0) return false;
    for(unsigned int i=0; i<d_str.size(); ++i) {
-     char c = convertUnsignedIntToChar( d_str[i] );
+     unsigned char c = convertUnsignedIntToChar( d_str[i] );
      if(c<'0' || c>'9') {
        return false;
      }
@@ -304,7 +309,7 @@ public:
    if(isNumber()) {
      int ret=0;
      for(unsigned int i=0; i<d_str.size(); ++i) {
-       char c = convertUnsignedIntToChar( d_str[i] );
+       unsigned char c = convertUnsignedIntToChar( d_str[i] );
        ret = ret * 10 + (int)c - (int)'0';
      }
      return ret;
@@ -313,9 +318,9 @@ public:
    }
   }
 
-  void getCharSet(std::set<char> &cset) const;
+  void getCharSet(std::set<unsigned char> &cset) const;
 
-  std::vector<unsigned int> getVec() const {
+  std::vector<unsigned> getVec() const {
     return d_str;
   }
 };/* class String */