merge with master

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

src/ast/rewriter/seq_derive.cpp

@@ -188,6 +188,13 @@ namespace seq {
             return mk_union(d1, d2);
         }
 
+        // δ(r1 x r2) = δ(r1) x δ(r2)
+        if (re().is_xor(r, r1, r2)) {
+            expr_ref d1 = derive_rec(r1);
+            expr_ref d2 = derive_rec(r2);
+            return mk_xor(d1, d2);
+        }
+
         // δ(r1 ∩ r2) = δ(r1) ∩ δ(r2)
         if (re().is_intersection(r, r1, r2)) {
             expr_ref d1 = derive_rec(r1);
@@ -615,16 +622,26 @@ namespace seq {
     }
 
     bool derive::pred_implies(expr* a, expr* b) {
-<<<<<<< HEAD
         bool sign_a = m.is_not(a, a);
         bool sign_b = m.is_not(b, b);
         return pred_implies(sign_a, a, sign_b, b);
-=======
-        expr* nota = nullptr, * notb = nullptr;
-        bool sign_a = m.is_not(a, nota);
-        bool sign_b = m.is_not(b, notb);
-        return pred_implies(sign_a, sign_a ? nota : a, sign_b, sign_b ? notb : b);
->>>>>>> b5afa9200e22209daec4b6d64831f89b8b1dc822
+    }
+
+    expr_ref derive::mk_xor(expr *a, expr *b) {
+        return mk_xor_core(a, b);
+    }
+
+    expr_ref derive::mk_xor_core(expr *a, expr *b) {
+        // ITE handling with path pruning (before merge, since ITEs aren't part of sorted chains)
+        if (m.is_ite(a) || m.is_ite(b)) {
+            // Canonical order for non-ITE cases handled by merge below
+            auto xor_op = [&](expr *x, expr *y) { return mk_xor(x, y); };
+            expr_ref r = hoist_ite(a, b, xor_op);
+            if (r)
+                return r;
+        }
+
+        return m_re.mk_xor0(a, b);
     }
 
     expr_ref derive::mk_union(expr* a, expr* b) {
@@ -893,7 +910,6 @@ namespace seq {
         expr* saved_path_expr = m_path_expr;
 
         // Push atoms onto path and check for contradiction or implication
-<<<<<<< HEAD
         lbool result = push_path_atoms(c, sign);
         if (result != l_undef) {
             m_path.shrink(saved_path_sz);
@@ -909,31 +925,6 @@ namespace seq {
             m_intervals.shrink(saved_intervals_sz);
             m_intervals_start = saved_intervals_start;
             return result;
-=======
-        lbool atoms_result = push_path_atoms(c, sign);
-        if (atoms_result == l_false) {
-            m_path.shrink(saved_path_sz);
-            m_intervals.shrink(saved_intervals_sz);
-            m_intervals_start = saved_intervals_start;
-            return l_false;
-        }
-
-        // Update intervals
-        lbool intervals_result = push_intervals_impl(c, sign);
-        if (intervals_result == l_false) {
-            m_path.shrink(saved_path_sz);
-            m_intervals.shrink(saved_intervals_sz);
-            m_intervals_start = saved_intervals_start;
-            return l_false;
-        }
-
-        // If either determined the atom is implied, no need to actually push
-        if (atoms_result == l_true || intervals_result == l_true) {
-            m_path.shrink(saved_path_sz);
-            m_intervals.shrink(saved_intervals_sz);
-            m_intervals_start = saved_intervals_start;
-            return l_true;
->>>>>>> b5afa9200e22209daec4b6d64831f89b8b1dc822
         }
 
         // Update path expression

src/ast/rewriter/seq_derive.h

@@ -138,6 +138,8 @@ namespace seq {
         expr_ref mk_concat(expr* a, expr* b);
         expr_ref mk_complement(expr* a);
         expr_ref mk_complement_core(expr* a);
+        expr_ref mk_xor(expr *a, expr *b);
+        expr_ref mk_xor_core(expr *a, expr *b);
         expr_ref mk_ite(expr* c, expr* t, expr* e);
 
         // Distribute concatenation through ITE/union in derivative

src/ast/rewriter/seq_rewriter.cpp

@@ -3903,6 +3903,48 @@ br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) {
     return BR_FAILED;
 }
 
+expr_ref seq_rewriter::mk_regex_concat(expr *r, expr *s) {
+    sort *seq_sort = nullptr, *ele_sort = nullptr;
+    VERIFY(m_util.is_re(r, seq_sort));
+    VERIFY(u().is_seq(seq_sort, ele_sort));
+    SASSERT(r->get_sort() == s->get_sort());
+    expr_ref result(m());
+    expr *r1, *r2;
+    if (re().is_epsilon(r) || re().is_empty(s))
+        result = s;
+    else if (re().is_epsilon(s) || re().is_empty(r))
+        result = r;
+    else if (re().is_full_seq(r) && re().is_full_seq(s))
+        result = r;
+    else if (re().is_full_char(r) && re().is_full_seq(s))
+        // ..* = .+
+        result = re().mk_plus(re().mk_full_char(ele_sort));
+    else if (re().is_full_seq(r) && re().is_full_char(s))
+        // .*. = .+
+        result = re().mk_plus(re().mk_full_char(ele_sort));
+    else if (re().is_concat(r, r1, r2))
+        // create the resulting concatenation in right-associative form except for the following case
+        // TODO: maintain the following invariant for A ++ B{m,n} + C
+        //       concat(concat(A, B{m,n}), C) (if A != () and C != ())
+        //       concat(B{m,n}, C) (if A == () and C != ())
+        // where A, B, C are regexes
+        // Using & below for Intersection and | for Union
+        // In other words, do not make A ++ B{m,n} into right-assoc form, but keep B{m,n} at the top
+        // This will help to identify this situation in the merge routine:
+        //               concat(concat(A, B{0,m}), C) | concat(concat(A, B{0,n}), C)
+        // simplifies to
+        //               concat(concat(A, B{0,max(m,n)}), C)
+        // analogously:
+        //               concat(concat(A, B{0,m}), C) & concat(concat(A, B{0,n}), C)
+        // simplifies to
+        //               concat(concat(A, B{0,min(m,n)}), C)
+        result = mk_regex_concat(r1, mk_regex_concat(r2, s));
+    else {
+        result = re().mk_concat(r, s);
+    }
+    return result;
+}
+
 bool seq_rewriter::are_complements(expr* r1, expr* r2) const {
     expr* r = nullptr;
     if (re().is_complement(r1, r) && r == r2)

src/ast/rewriter/seq_rewriter.h

@@ -139,14 +139,10 @@ class seq_rewriter {
     // re2automaton   m_re2aut;
     op_cache       m_op_cache;
     expr_ref_vector m_es, m_lhs, m_rhs;
-<<<<<<< HEAD
-    bool           m_coalesce_chars;
-    bool           m_in_bisim { false };
-=======
-    bool           m_coalesce_chars;    
+    bool m_coalesce_chars = false;
+    bool           m_in_bisim { false };   
     unsigned       m_re_deriv_depth { 0 };
     static const unsigned m_max_re_deriv_depth = 512;
->>>>>>> b5afa9200e22209daec4b6d64831f89b8b1dc822
 
     enum length_comparison {
         shorter_c, 
@@ -367,6 +363,13 @@ public:
         return result;
     }
 
+    expr_ref mk_xor0(expr *a, expr *b) {
+        expr_ref result(m());
+        if (mk_re_xor0(a, b, result) == BR_FAILED)
+            result = re().mk_xor(a, b);
+        return result;
+    }
+
     expr_ref mk_union(expr *a, expr *b) {
         expr_ref result(m());
         if (mk_re_union(a, b, result) == BR_FAILED)
@@ -448,7 +451,9 @@ public:
     procedure which relies on each leaf of D(p XOR q) being a coherent
     XOR pair (D_v p) XOR (D_v q).
     */
-    expr_ref mk_brz_derivative(expr* r);
+    expr_ref mk_brz_derivative(expr *r) {
+        return mk_derivative(r);
+    }
 
     // heuristic elimination of element from condition that comes form a derivative.
     // special case optimization for conjunctions of equalities, disequalities and ranges.
@@ -459,6 +464,8 @@ public:
     /* Apply simplifications to the intersection to keep it normalized (r1 and r2 are not normalized)*/
     expr_ref mk_regex_inter_normalize(expr* r1, expr* r2);
 
+    expr_ref mk_regex_concat(expr *r1, expr *r2);
+
     /*
     * Extract some string that is a member of r. 
     * Return true if a valid string was extracted.