mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

Merge pull request #4092 from mtrberzi/regex-compl-inter

Browse source 
z3str3: fix support for re.complement and re.intersection
This commit is contained in:
Murphy Berzish 2020-04-29 10:13:20 -05:00 • committed by GitHub
commit b0ffad95b0
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 17 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/smt/theory_str.cpp
View file

@ -2069,6 +2069,18 @@ namespace smt {
return zstring("(.*)");
} else if (u.re.is_full_char(a_regex)) {
return zstring("str.allchar");
} else if (u.re.is_intersection(a_regex)) {
expr * a0;
expr * a1;
u.re.is_intersection(a_regex, a0, a1);
zstring a0str = get_std_regex_str(a0);
zstring a1str = get_std_regex_str(a1);
return zstring("(") + a0str + zstring("&&") + a1str + zstring(")");
} else if (u.re.is_complement(a_regex)) {
expr * body;
u.re.is_complement(a_regex, body);
zstring bodyStr = get_std_regex_str(body);
return zstring("(^") + bodyStr + zstring(")");
} else {
TRACE("str", tout << "BUG: unrecognized regex term " << mk_pp(regex, get_manager()) << std::endl;);
UNREACHABLE(); return zstring("");

6
src/smt/theory_str_regex.cpp
View file

@ -902,7 +902,11 @@ namespace smt {
return true;
} else if (u.re.is_complement(re)) {
// TODO can we do better?
return false;
return false;
} else if (u.re.is_intersection(re)) {
return false;
} else if (u.re.is_complement(re)) {
return false;
} else if (u.re.is_loop(re, sub1, lo, hi) || u.re.is_loop(re, sub1, lo)) {
return check_regex_length_linearity_helper(sub1, already_star);
} else {