summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/printer/smt2/smt2_printer.cpp6
-rw-r--r--src/theory/strings/regexp_operation.cpp58
-rw-r--r--src/theory/strings/regexp_operation.h18
-rw-r--r--src/theory/strings/theory_strings_rewriter.cpp10
-rw-r--r--src/theory/strings/theory_strings_type_rules.h2
-rw-r--r--src/util/regexp.cpp10
-rw-r--r--src/util/regexp.h59
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<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 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);
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<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 26d468a30..c5a094f8c 100644
--- 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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback