summaryrefslogtreecommitdiff
path: root/src/util/regexp.h
diff options
context:
space:
mode:
authorTianyi Liang <tianyi-liang@uiowa.edu>2014-02-11 18:08:53 -0600
committerTianyi Liang <tianyi-liang@uiowa.edu>2014-02-11 18:08:53 -0600
commitcbf8dffcd17e70d4d4c7d8d1e57bcb16317d246f (patch)
tree5895379da59fb2bfceeff431b11541ea10018494 /src/util/regexp.h
parentbd0072e146a4ca2acc509af59f745dca7a69ef1d (diff)
minor fix for recognizing the tail backslash, still have smt-lib compliance issue.
Diffstat (limited to 'src/util/regexp.h')
-rw-r--r--src/util/regexp.h11
1 files changed, 2 insertions, 9 deletions
diff --git a/src/util/regexp.h b/src/util/regexp.h
index 4942c2652..10c8ba2b9 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -124,7 +124,8 @@ private:
}
}
} else {
- throw CVC4::Exception( "Error String Literal: \"" + s + "\"" );
+ //throw CVC4::Exception( "Error String Literal: \"" + s + "\"" );
+ d_str.push_back( convertCharToUnsignedInt('\\') );
}
} else {
d_str.push_back( convertCharToUnsignedInt(s[i]) );
@@ -138,19 +139,11 @@ public:
String(const std::string &s) {
toInternal(s);
- /*
- for(unsigned int i=0; i<s.size(); ++i) {
- d_str.push_back( convertCharToUnsignedInt(s[i]) );
- }*/
}
String(const char* s) {
std::string stmp(s);
toInternal(stmp);
- /*
- for(unsigned int i=0,len=strlen(s); i<len; ++i) {
- d_str.push_back( convertCharToUnsignedInt(s[i]) );
- }*/
}
String(const char c) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback