diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 044ee4523..d19886d31 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -4147,6 +4147,20 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { *************************************************/ + +expr_ref seq_rewriter::mk_symmetric_diff(expr* r1, expr* r2) { + expr_ref r(m()); + if (r1 == r2) + r = re().mk_empty(r1->get_sort()); + else if (re().is_empty(r1)) + r = r2; + else if (re().is_empty(r2)) + r = r1; + else + r = re().mk_union(re().mk_diff(r1, r2), re().mk_diff(r2, r1)); + return r; +} + /* * pattern match against all ++ "abc" ++ all ++ "def" ++ all regexes. */ diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 5612c5a69..d55392bc3 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -379,6 +379,8 @@ public: return result; } + expr_ref mk_symmetric_diff(expr *r1, expr *r2); + /** * check if regular expression is of the form all ++ s ++ all ++ t + u ++ all, where, s, t, u are sequences */ diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index b6be9b93c..f466dd200 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -2870,32 +2870,28 @@ namespace seq { expr_ref left(m); expr_ref right(m); - if (i == 0) left = seq.re.mk_epsilon(str_sort); + if (i == 0) + left = seq.re.mk_epsilon(str_sort); else { - expr_ref_vector left_args(m); - for (unsigned j = 0; j < i; ++j) left_args.push_back(to_app(r)->get_arg(j)); - if (left_args.size() == 1) left = left_args.get(0); - else left = m.mk_app(seq.get_family_id(), OP_RE_CONCAT, left_args.size(), left_args.data()); + for (unsigned j = 0; j < i; ++j) { + auto arg = to_app(r)->get_arg(j); + left = left ? seq.re.mk_concat(left, arg) : arg; + } } - if (i == num_args - 1) right = seq.re.mk_epsilon(str_sort); + if (i == num_args - 1) + right = seq.re.mk_epsilon(str_sort); else { - expr_ref_vector right_args(m); - for (unsigned j = i + 1; j < num_args; ++j) right_args.push_back(to_app(r)->get_arg(j)); - if (right_args.size() == 1) right = right_args.get(0); - else right = m.mk_app(seq.get_family_id(), OP_RE_CONCAT, right_args.size(), right_args.data()); + for (unsigned j = i + 1; j < num_args; ++j) { + auto arg = to_app(r)->get_arg(j); + right = right ? seq.re.mk_concat(right, arg) : arg; + } } - for (auto const& pair : tau_arg) { - expr_ref p(m), q(m); - if (seq.re.is_epsilon(left)) p = pair.m_p; - else if (seq.re.is_epsilon(pair.m_p)) p = left; - else p = seq.re.mk_concat(left, pair.m_p); - - if (seq.re.is_epsilon(right)) q = pair.m_q; - else if (seq.re.is_epsilon(pair.m_q)) q = right; - else q = seq.re.mk_concat(pair.m_q, right); - + for (auto const &[tp, tq] : tau_arg) { + seq_rewriter rw(m); + auto p = rw.mk_re_append(left, tp); + auto q = rw.mk_re_append(tq, right); result.push_back(tau_pair(p, q, m)); } } @@ -2913,14 +2909,10 @@ namespace seq { tau_pairs tau_body; compute_tau(m, seq, sg, body, tau_body); - for (auto const& pair : tau_body) { - expr_ref p(m), q(m); - if (seq.re.is_epsilon(pair.m_p)) p = r; - else p = seq.re.mk_concat(r, pair.m_p); - - if (seq.re.is_epsilon(pair.m_q)) q = r; - else q = seq.re.mk_concat(pair.m_q, r); - + for (auto const &[tp, tq] : tau_body) { + seq_rewriter rw(m); + auto p = rw.mk_re_append(r, tp); + auto q = rw.mk_re_append(tq, r); result.push_back(tau_pair(p, q, m)); } } diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 4c9b19ae1..b24f47664 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -388,15 +388,8 @@ namespace smt { } expr_ref seq_regex::symmetric_diff(expr* r1, expr* r2) { - expr_ref r(m); - if (r1 == r2) - r = re().mk_empty(r1->get_sort()); - else if (re().is_empty(r1)) - r = r2; - else if (re().is_empty(r2)) - r = r1; - else - r = re().mk_union(re().mk_diff(r1, r2), re().mk_diff(r2, r1)); + seq_rewriter rw(m); + auto r = rw.mk_symmetric_diff(r1, r2); rewrite(r); return r; } diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 3fcb17adf..68cc8eb77 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -232,10 +232,9 @@ namespace smt { auto e2 = n2->get_expr(); TRACE(seq, tout << mk_pp(e1, m) << " == " << mk_pp(e2, m) << "\n"); if (m_seq.is_re(e1)) { - seq_rewriter rw(m); - expr_ref s(m), r(m); - r = m_seq.re.mk_union(m_seq.re.mk_diff(e1, e2), m_seq.re.mk_diff(e2, e1)); - switch (rw.some_seq_in_re(r, s)) { + expr_ref s(m); + auto r = m_rewriter.mk_symmetric_diff(e1, e2); + switch (m_rewriter.some_seq_in_re(r, s)) { case l_false: // regexes are equivalent: nothing to do return; @@ -277,15 +276,15 @@ namespace smt { auto e2 = n2->get_expr(); TRACE(seq, tout << mk_pp(e1, m) << " != " << mk_pp(e2, m) << "\n"); if (m_seq.is_re(e1)) { - seq_rewriter rw(m); - expr_ref s(m), r(m); - r = m_seq.re.mk_union(m_seq.re.mk_diff(e1, e2), m_seq.re.mk_diff(e2, e1)); - switch (rw.some_seq_in_re(r, s)) { + expr_ref s(m); + auto r = m_rewriter.mk_symmetric_diff(e1, e2); + switch (m_rewriter.some_seq_in_re(r, s)) { case l_false: { + enode_pair_vector eqs; auto lit = mk_eq(e1, e2, false); literal_vector lits; - lits.push_back(lit); - ctx.mk_th_axiom(get_id(), lits.size(), lits.data()); + lits.push_back(~lit); + set_conflict(eqs, lits); break; } case l_true: