diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2015-01-08 11:37:58 -0600 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2015-01-08 11:37:58 -0600 |
commit | 0f03904f2fbe4f785c697dc301f48f55919896cd (patch) | |
tree | c9ae16e6761ac0592d9520a94f7dbf037e3fe2d5 /src/theory/strings | |
parent | 740bfad6ab2c3ac6c1f7eec9c8e6f5338abd8eb5 (diff) |
switch ascii encoding to unsigned char
Diffstat (limited to 'src/theory/strings')
-rw-r--r-- | src/theory/strings/regexp_operation.cpp | 58 | ||||
-rw-r--r-- | src/theory/strings/regexp_operation.h | 18 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 10 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_type_rules.h | 2 |
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); |