diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp index 8f5831086..e664ab18c 100644 --- a/src/ast/rewriter/seq_derive.cpp +++ b/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 diff --git a/src/ast/rewriter/seq_derive.h b/src/ast/rewriter/seq_derive.h index 676f67f81..bc55e1740 100644 --- a/src/ast/rewriter/seq_derive.h +++ b/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 diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 73a5e6417..6f6a4ea88 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/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) diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 7b8058353..aa4603e6c 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/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.