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

z3str3: fix support for re.complement and re.intersection
Z3Prover · Apr 29, 2020 · b0ffad9 · b0ffad9
2 parents 0fb6a7c + d21911c
commit b0ffad9
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 1 deletion.
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
@@ -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("");

diff --git a/src/smt/theory_str_regex.cpp b/src/smt/theory_str_regex.cpp
@@ -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 {