mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

fix #7252

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-06-13 17:52:17 -07:00
parent 35c1cacf44
commit a6b502779b
2 changed files with 15 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -3201,6 +3201,7 @@ expr_ref seq_rewriter::mk_antimirov_deriv(expr* e, expr* r, expr* path) {
void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref& result) { void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref& result) {
sort* seq_sort = nullptr, * ele_sort = nullptr; sort* seq_sort = nullptr, * ele_sort = nullptr;
expr_ref _r(r, m()), _path(path, m());
VERIFY(m_util.is_re(r, seq_sort)); VERIFY(m_util.is_re(r, seq_sort));
VERIFY(m_util.is_seq(seq_sort, ele_sort)); VERIFY(m_util.is_seq(seq_sort, ele_sort));
SASSERT(ele_sort == e->get_sort()); SASSERT(ele_sort == e->get_sort());
@ -3347,8 +3348,10 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref
else if (re().is_loop(r, r1, lo, hi)) { else if (re().is_loop(r, r1, lo, hi)) {
if ((lo == 0 && hi == 0) || hi < lo) if ((lo == 0 && hi == 0) || hi < lo)
result = nothing(); result = nothing();
else else {
result = mk_antimirov_deriv_concat(mk_antimirov_deriv(e, r1, path), re().mk_loop_proper(r1, (lo == 0 ? 0 : lo - 1), hi - 1)); expr_ref t(re().mk_loop_proper(r1, (lo == 0 ? 0 : lo - 1), hi - 1), m());
result = mk_antimirov_deriv_concat(mk_antimirov_deriv(e, r1, path), t);
}
} }
else if (re().is_opt(r, r1)) else if (re().is_opt(r, r1))
result = mk_antimirov_deriv(e, r1, path); result = mk_antimirov_deriv(e, r1, path);
@ -3414,15 +3417,18 @@ expr_ref seq_rewriter::mk_antimirov_deriv_intersection(expr* e, expr* d1, expr*
expr_ref seq_rewriter::mk_antimirov_deriv_concat(expr* d, expr* r) { expr_ref seq_rewriter::mk_antimirov_deriv_concat(expr* d, expr* r) {
expr_ref result(m()); expr_ref result(m());
// Take reference count of r and d
expr_ref _r(r, m()), _d(d, m()); expr_ref _r(r, m()), _d(d, m());
expr* c, * t, * e; expr* c, * t, * e;
if (m().is_ite(d, c, t, e)) if (m().is_ite(d, c, t, e)) {
result = m().mk_ite(c, mk_antimirov_deriv_concat(t, r), mk_antimirov_deriv_concat(e, r)); auto r2 = mk_antimirov_deriv_concat(e, r);
auto r1 = mk_antimirov_deriv_concat(t, r);
result = m().mk_ite(c, r1, r2);
}
else if (re().is_union(d, t, e)) else if (re().is_union(d, t, e))
result = mk_antimirov_deriv_union(mk_antimirov_deriv_concat(t, r), mk_antimirov_deriv_concat(e, r)); result = mk_antimirov_deriv_union(mk_antimirov_deriv_concat(t, r), mk_antimirov_deriv_concat(e, r));
else else
result = mk_re_append(d, r); result = mk_re_append(d, r);
SASSERT(result.get());
return result; return result;
} }

6
src/ast/seq_decl_plugin.cpp
View file

@ -1164,11 +1164,13 @@ expr* seq_util::rex::mk_loop_proper(expr* r, unsigned lo, unsigned hi)
// avoid creating a loop with both bounds 0 // avoid creating a loop with both bounds 0
// such an expression is invalid as a loop // such an expression is invalid as a loop
// it is BY DEFINITION = epsilon // it is BY DEFINITION = epsilon
return mk_epsilon(seq_sort); r = mk_epsilon(seq_sort);
return r;
} }
if (lo == 1 && hi == 1) if (lo == 1 && hi == 1) {
// do not create a loop unless it actually is a loop // do not create a loop unless it actually is a loop
return r; return r;
}
parameter params[2] = { parameter(lo), parameter(hi) }; parameter params[2] = { parameter(lo), parameter(hi) };
return m.mk_app(m_fid, OP_RE_LOOP, 2, params, 1, &r); return m.mk_app(m_fid, OP_RE_LOOP, 2, params, 1, &r);
} }