z3str3: fix support for re.complement and re.intersection

Author: mtrberzi

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("");

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 {