normalization of union/intersection

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/rewriter/seq_rewriter.cpp

@@ -416,6 +416,9 @@ br_status seq_rewriter::mk_bool_app(func_decl* f, unsigned n, expr* const* args,
         return mk_bool_app_helper(true, n, args, result);
     case OP_OR:
         return mk_bool_app_helper(false, n, args, result);
+    case OP_EQ:
+        SASSERT(n == 2);
+        // return mk_eq_helper(args[0], args[1], result);
     default:
         return BR_FAILED;
     }
@@ -492,7 +495,27 @@ br_status seq_rewriter::mk_bool_app_helper(bool is_and, unsigned n, expr* const*
         }
     }
     
-    result = is_and ? m().mk_and(new_args.size(), new_args.c_ptr()) : m().mk_or(new_args.size(), new_args.c_ptr());
+    result = is_and ? m().mk_and(new_args) : m().mk_or(new_args);
+    return BR_REWRITE_FULL;
+}
+
+br_status seq_rewriter::mk_eq_helper(expr* a, expr* b, expr_ref& result) {
+    expr* sa = nullptr, *ra = nullptr, *sb = nullptr, *rb = nullptr;
+    if (str().is_in_re(b))
+        std::swap(a, b);
+    if (!str().is_in_re(a, sa, ra))
+        return BR_FAILED;
+    bool is_not = m().is_not(b, b);
+    if (!str().is_in_re(b, sb, rb))
+        return BR_FAILED;
+    if (sa != sb)
+        return BR_FAILED;
+    // sa in ra = sb in rb;
+    // sa in (ra n rb) u (C(ra) n C(rb))
+    if (is_not)
+        rb = re().mk_complement(rb);
+    expr* r = re().mk_union(re().mk_inter(ra, rb), re().mk_inter(re().mk_complement(ra), re().mk_complement(rb)));
+    result = re().mk_in_re(sa, r);
     return BR_REWRITE_FULL;
 }
 
@@ -2870,6 +2893,35 @@ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) {
         result = b;
         return BR_DONE;
     }
+    expr* ac = nullptr, *bc = nullptr;
+    expr* a1 = nullptr, *a2 = nullptr;
+    expr* b1 = nullptr, *b2 = nullptr;
+    // ensure union is right-associative
+    // and swap-sort entries 
+    if (re().is_union(a, a1, a2)) {
+        result = re().mk_union(a1, re().mk_union(a2, b));
+        return BR_REWRITE2;
+    }
+    auto mk_full = [&]() { return re().mk_full_seq(m().get_sort(a)); };
+    auto get_id = [&](expr* e) { re().is_complement(e, e); return e->get_id(); };
+    if (re().is_union(b, b1, b2)) {
+        if (a == b1) {
+            result = b;
+            return BR_DONE;
+        }
+        if (re().is_complement(a, ac) && b1 == ac) {
+            result = mk_full();
+            return BR_DONE;
+        }
+        if (re().is_complement(b1, bc) && a == bc) {
+            result = mk_full();
+            return BR_DONE;
+        }
+        if (get_id(a) > get_id(b1)) {
+            result = re().mk_union(b1, re().mk_union(a, b2));
+            return BR_REWRITE2;
+        }
+    }
     return BR_FAILED;
 }
 
@@ -2891,6 +2943,10 @@ br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) {
         result = re().mk_empty(m().get_sort(a));
         return BR_DONE;
     }
+    if (re().is_complement(a, e1)) {
+        result = e1;
+        return BR_DONE;
+    }
     return BR_FAILED;
 }
 
@@ -2923,9 +2979,38 @@ br_status seq_rewriter::mk_re_inter(expr* a, expr* b, expr_ref& result) {
         return BR_DONE;
     }
     expr* ac = nullptr, *bc = nullptr;
+    expr* a1 = nullptr, *a2 = nullptr;
+    expr* b1 = nullptr, *b2 = nullptr;
+
+    // ensure intersection is right-associative
+    // and swap-sort entries 
+    if (re().is_intersection(a, a1, a2)) {
+        result = re().mk_inter(a1, re().mk_inter(a2, b));
+        return BR_REWRITE2;
+    }
+    auto mk_empty = [&]() { return re().mk_empty(m().get_sort(a)); };
+    auto get_id = [&](expr* e) { re().is_complement(e, e); return e->get_id(); };
+    if (re().is_intersection(b, b1, b2)) {
+        if (a == b1) {
+            result = b;
+            return BR_DONE;
+        }
+        if (re().is_complement(a, ac) && b1 == ac) {
+            result = mk_empty();
+            return BR_DONE;
+        }
+        if (re().is_complement(b1, bc) && a == bc) {
+            result = mk_empty();
+            return BR_DONE;
+        }
+        if (get_id(a) > get_id(b1)) {
+            result = re().mk_inter(b1, re().mk_inter(a, b2));
+            return BR_REWRITE2;
+        }
+    }
     if ((re().is_complement(a, ac) && ac == b) ||
         (re().is_complement(b, bc) && bc == a)) {
-        result = re().mk_empty(m().get_sort(a));
+        result = mk_empty();
         return BR_DONE;
     }
     if (re().is_to_re(b)) 

src/ast/rewriter/seq_rewriter.h

@@ -238,6 +238,7 @@ class seq_rewriter {
     bool rewrite_contains_pattern(expr* a, expr* b, expr_ref& result);
 
     br_status mk_bool_app_helper(bool is_and, unsigned n, expr* const* args, expr_ref& result);
+    br_status mk_eq_helper(expr* a, expr* b, expr_ref& result);
 
     bool cannot_contain_prefix(expr* a, expr* b);
     bool cannot_contain_suffix(expr* a, expr* b);

src/ast/rewriter/th_rewriter.cpp

@@ -203,7 +203,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
                 if (st != BR_FAILED)
                     return st;
             }
-            if ((k == OP_AND || k == OP_OR) && m_seq_rw.u().has_re()) {
+            if ((k == OP_AND || k == OP_OR /*|| k == OP_EQ*/) && m_seq_rw.u().has_re()) {
                 st = m_seq_rw.mk_bool_app(f, num, args, result); 
                 if (st != BR_FAILED)
                     return st;

src/smt/seq_regex.cpp

@@ -304,11 +304,10 @@ namespace smt {
         literal_vector lits;    
         for (unsigned i = 0; i < m_s_in_re.size(); ++i) {
             auto const& entry = m_s_in_re[i];
-            std::cout << "CHECK " << i << " " << mk_pp(s, m) << " " << mk_pp(entry.m_s, m) << "\n";
-            enode* n1 = th.ensure_enode(entry.m_s);
-            enode* n2 = th.ensure_enode(s);
             if (!entry.m_active)
                 continue;
+            enode* n1 = th.ensure_enode(entry.m_s);
+            enode* n2 = th.ensure_enode(s);
             if (n1->get_root() != n2->get_root())
                 continue;
             if (entry.m_re == regex)