From 0f03904f2fbe4f785c697dc301f48f55919896cd Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Thu, 8 Jan 2015 11:37:58 -0600 Subject: [PATCH] switch ascii encoding to unsigned char --- src/printer/smt2/smt2_printer.cpp | 6 +- src/theory/strings/regexp_operation.cpp | 58 +++++++++--------- src/theory/strings/regexp_operation.h | 18 +++--- .../strings/theory_strings_rewriter.cpp | 10 ++-- .../strings/theory_strings_type_rules.h | 2 +- src/util/regexp.cpp | 10 ++-- src/util/regexp.h | 59 ++++++++++--------- 7 files changed, 85 insertions(+), 78 deletions(-) diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 2197cd648..72a64ab78 100644 --- 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& s = n.getConst().getVec(); + //const std::vector& s = n.getConst().getVec(); + std::string s = n.getConst().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 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 &pcset, SetNodes &pvset ) { +void RegExpOpr::firstChars( Node r, std::set &pcset, SetNodes &pvset ) { Trace("regexp-fset") << "Start FSET(" << mkString(r) << ")" << std::endl; - std::map< Node, std::pair< std::set, SetNodes > >::const_iterator itr = d_fset_cache.find(r); + std::map< Node, std::pair< std::set, 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 cset; + std::set cset; SetNodes vset; int k = r.getKind(); switch( k ) { @@ -666,7 +666,7 @@ void RegExpOpr::firstChars( Node r, std::set &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 &pcset, SetNodes &pvset ) { } pcset.insert(cset.begin(), cset.end()); pvset.insert(vset.begin(), vset.end()); - std::pair< std::set, SetNodes > p(cset, vset); + std::pair< std::set, SetNodes > p(cset, vset); d_fset_cache[r] = p; } if(Trace.isOn("regexp-fset")) { Trace("regexp-fset") << "END FSET(" << mkString(r) << ") = {"; - for(std::set::const_iterator itr = pcset.begin(); + for(std::set::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 &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 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 &pcset, SetNodes &pvset ) { - std::map< Node, std::pair< std::set, SetNodes > >::const_iterator itr = d_cset_cache.find(r); +void RegExpOpr::getCharSet( Node r, std::set &pcset, SetNodes &pvset ) { + std::map< Node, std::pair< std::set, 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 cset; + std::set cset; SetNodes vset; int k = r.getKind(); switch( k ) { @@ -1137,15 +1137,15 @@ void RegExpOpr::getCharSet( Node r, std::set &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().getFirstChar(); - char b = r[1].getConst().getFirstChar(); - for(char i=a; i<=b; i++) { + unsigned char a = r[0].getConst().getFirstChar(); + unsigned char b = r[1].getConst().getFirstChar(); + for(unsigned char i=a; i<=b; i++) { cset.insert(i); } break; @@ -1200,11 +1200,11 @@ void RegExpOpr::getCharSet( Node r, std::set &pcset, SetNodes &pvset ) { } pcset.insert(cset.begin(), cset.end()); pvset.insert(vset.begin(), vset.end()); - std::pair< std::set, SetNodes > p(cset, vset); + std::pair< std::set, SetNodes > p(cset, vset); d_cset_cache[r] = p; Trace("regexp-cset") << "CSET( " << mkString(r) << " ) = { "; - for(std::set::const_iterator itr = cset.begin(); + for(std::set::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::const_iterator itr = cset.begin(); + for(std::vector::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::const_iterator itr = cset.begin(); + for(std::vector::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 cset; + std::set 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, std::set > > d_cset_cache; - std::map< Node, std::pair< std::set, std::set > > d_fset_cache; + std::map< Node, std::pair< std::set, std::set > > d_cset_cache; + std::map< Node, std::pair< std::set, std::set > > 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 &pcset, SetNodes &pvset ); + void getCharSet( Node r, std::set &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 &pcset, SetNodes &pvset ); + void firstChars( Node r, std::set &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().getFirstChar(); - char b = r[1].getConst().getFirstChar(); - char c = s.getLastChar(); + unsigned char a = r[0].getConst().getFirstChar(); + unsigned char b = r[1].getConst().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().getFirstChar(); - char end = node[1].getConst().getFirstChar(); + unsigned char c = node[0].getConst().getFirstChar(); + unsigned char end = node[1].getConst().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); diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp index 1c672d4b9..24e894678 100644 --- 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 &cset) const { +void String::getCharSet(std::set &cset) const { for(std::vector::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=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 d_str; + std::vector d_str; - bool isVecSame(const std::vector &a, const std::vector &b) const { + bool isVecSame(const std::vector &a, const std::vector &b) const { if(a.size() != b.size()) return false; else { - for(unsigned int i=0; i='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 &s) : d_str(s) { } + String(const std::vector &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::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'9') { return false; } @@ -304,7 +309,7 @@ public: if(isNumber()) { int ret=0; for(unsigned int i=0; i &cset) const; + void getCharSet(std::set &cset) const; - std::vector getVec() const { + std::vector getVec() const { return d_str; } };/* class String */ -- 2.30.2