switch ascii encoding to unsigned char

4 files changed, 44 insertions, 44 deletions

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 3846c0c07..e09f47f0f 100644
--- 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 d170bd17a..da84ed04c 100644
--- 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 9f6836406..6960659e8 100644
--- 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 55059fa77..e053f48da 100644
--- 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);