mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-22 01:49:36 +00:00
Code Activity

code simplification, fix conflict in new_diseq_eh

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-04-21 10:17:43 +02:00
parent 352b14fe2b
commit 8cc85a7d7b
5 changed files with 47 additions and 47 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/ast/rewriter/seq_rewriter.cpp
View file

@ -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. * pattern match against all ++ "abc" ++ all ++ "def" ++ all regexes.
*/ */

2
src/ast/rewriter/seq_rewriter.h
View file

@ -379,6 +379,8 @@ public:
return result; 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 * check if regular expression is of the form all ++ s ++ all ++ t + u ++ all, where, s, t, u are sequences
*/ */

48
src/smt/seq/seq_nielsen.cpp
View file

@ -2870,32 +2870,28 @@ namespace seq {
expr_ref left(m); expr_ref left(m);
expr_ref right(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 { else {
expr_ref_vector left_args(m); for (unsigned j = 0; j < i; ++j) {
for (unsigned j = 0; j < i; ++j) left_args.push_back(to_app(r)->get_arg(j)); auto arg = to_app(r)->get_arg(j);
if (left_args.size() == 1) left = left_args.get(0); left = left ? seq.re.mk_concat(left, arg) : arg;
else left = m.mk_app(seq.get_family_id(), OP_RE_CONCAT, left_args.size(), left_args.data()); }
} }
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 { else {
expr_ref_vector right_args(m); for (unsigned j = i + 1; j < num_args; ++j) {
for (unsigned j = i + 1; j < num_args; ++j) right_args.push_back(to_app(r)->get_arg(j)); auto arg = to_app(r)->get_arg(j);
if (right_args.size() == 1) right = right_args.get(0); right = right ? seq.re.mk_concat(right, arg) : arg;
else right = m.mk_app(seq.get_family_id(), OP_RE_CONCAT, right_args.size(), right_args.data()); }
} }
for (auto const& pair : tau_arg) { for (auto const &[tp, tq] : tau_arg) {
expr_ref p(m), q(m); seq_rewriter rw(m);
if (seq.re.is_epsilon(left)) p = pair.m_p; auto p = rw.mk_re_append(left, tp);
else if (seq.re.is_epsilon(pair.m_p)) p = left; auto q = rw.mk_re_append(tq, right);
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);
result.push_back(tau_pair(p, q, m)); result.push_back(tau_pair(p, q, m));
} }
} }
@ -2913,14 +2909,10 @@ namespace seq {
tau_pairs tau_body; tau_pairs tau_body;
compute_tau(m, seq, sg, body, tau_body); compute_tau(m, seq, sg, body, tau_body);
for (auto const& pair : tau_body) { for (auto const &[tp, tq] : tau_body) {
expr_ref p(m), q(m); seq_rewriter rw(m);
if (seq.re.is_epsilon(pair.m_p)) p = r; auto p = rw.mk_re_append(r, tp);
else p = seq.re.mk_concat(r, pair.m_p); auto q = rw.mk_re_append(tq, r);
if (seq.re.is_epsilon(pair.m_q)) q = r;
else q = seq.re.mk_concat(pair.m_q, r);
result.push_back(tau_pair(p, q, m)); result.push_back(tau_pair(p, q, m));
} }
} }

11
src/smt/seq_regex.cpp
View file

@ -388,15 +388,8 @@ namespace smt {
} }
expr_ref seq_regex::symmetric_diff(expr* r1, expr* r2) { expr_ref seq_regex::symmetric_diff(expr* r1, expr* r2) {
expr_ref r(m); seq_rewriter rw(m);
if (r1 == r2) auto r = rw.mk_symmetric_diff(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));
rewrite(r); rewrite(r);
return r; return r;
} }

19
src/smt/theory_nseq.cpp
View file

@ -232,10 +232,9 @@ namespace smt {
auto e2 = n2->get_expr(); auto e2 = n2->get_expr();
TRACE(seq, tout << mk_pp(e1, m) << " == " << mk_pp(e2, m) << "\n"); TRACE(seq, tout << mk_pp(e1, m) << " == " << mk_pp(e2, m) << "\n");
if (m_seq.is_re(e1)) { if (m_seq.is_re(e1)) {
seq_rewriter rw(m); expr_ref s(m);
expr_ref s(m), r(m); auto r = m_rewriter.mk_symmetric_diff(e1, e2);
r = m_seq.re.mk_union(m_seq.re.mk_diff(e1, e2), m_seq.re.mk_diff(e2, e1)); switch (m_rewriter.some_seq_in_re(r, s)) {
switch (rw.some_seq_in_re(r, s)) {
case l_false: case l_false:
// regexes are equivalent: nothing to do // regexes are equivalent: nothing to do
return; return;
@ -277,15 +276,15 @@ namespace smt {
auto e2 = n2->get_expr(); auto e2 = n2->get_expr();
TRACE(seq, tout << mk_pp(e1, m) << " != " << mk_pp(e2, m) << "\n"); TRACE(seq, tout << mk_pp(e1, m) << " != " << mk_pp(e2, m) << "\n");
if (m_seq.is_re(e1)) { if (m_seq.is_re(e1)) {
seq_rewriter rw(m); expr_ref s(m);
expr_ref s(m), r(m); auto r = m_rewriter.mk_symmetric_diff(e1, e2);
r = m_seq.re.mk_union(m_seq.re.mk_diff(e1, e2), m_seq.re.mk_diff(e2, e1)); switch (m_rewriter.some_seq_in_re(r, s)) {
switch (rw.some_seq_in_re(r, s)) {
case l_false: { case l_false: {
enode_pair_vector eqs;
auto lit = mk_eq(e1, e2, false); auto lit = mk_eq(e1, e2, false);
literal_vector lits; literal_vector lits;
lits.push_back(lit); lits.push_back(~lit);
ctx.mk_th_axiom(get_id(), lits.size(), lits.data()); set_conflict(eqs, lits);
break; break;
} }
case l_true: case l_true: