mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-16 07:45:27 +00:00
Code Activity

turn on Unicode parsing when they fit in 8 bits

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-05-22 10:41:19 -07:00
parent b7d7ff38cb
commit d1d14111cb
1 changed files with 9 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ast/seq_decl_plugin.cpp
View file

@ -82,7 +82,6 @@ static bool is_escape_char(char const *& s, unsigned& result) {
return true; return true;
} }
#if Z3_USE_UNICODE
if (*(s+1) == 'u' && *(s+2) == '{') { if (*(s+1) == 'u' && *(s+2) == '{') {
result = 0; result = 0;
for (unsigned i = 0; i < 5; ++i) { for (unsigned i = 0; i < 5; ++i) {
@ -90,8 +89,12 @@ static bool is_escape_char(char const *& s, unsigned& result) {
result = 16*result + d1; result = 16*result + d1;
} }
else if (*(s+3+i) == '}') { else if (*(s+3+i) == '}') {
#if !Z3_USE_UNICODE
if (result > 255)
throw default_exception("unicode characters outside of byte range are not supported");
#endif
s += 4 + i; s += 4 + i;
return true; return true;
} }
else { else {
break; break;
@ -110,10 +113,13 @@ static bool is_escape_char(char const *& s, unsigned& result) {
break; break;
} }
} }
#if !Z3_USE_UNICODE
if (result > 255)
throw default_exception("unicode characters outside of byte range are not supported");
#endif
s += 3 + i; s += 3 + i;
return true; return true;
} }
#endif
switch (*(s + 1)) { switch (*(s + 1)) {
case 'a': case 'a':
result = '\a'; result = '\a';