mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 15:16:29 +00:00
Code Activity

Remove is_nullable_rec from seq_rewriter, delegate to derive::nullable

Browse source
This commit is contained in:
copilot-swe-agent[bot] 2026-06-10 18:53:55 +00:00 • committed by Nikolaj Bjorner
parent 70a9dbfae2
commit 1e906ba585
4 changed files with 8 additions and 117 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/rewriter/seq_derive.cpp
View file

@ -519,8 +519,7 @@ namespace seq {
m_br.mk_not(is_nullable(r1), result);
}
else if (re().is_to_re(r, r1)) {
SASSERT(u().is_seq(r1->get_sort()));
result = m.mk_eq(u().str.mk_empty(r1->get_sort()), r1);
result = is_nullable(r1);
}
else if (m.is_ite(r, cond, r1, r2)) {
m_br.mk_ite(cond, is_nullable(r1), is_nullable(r2), result);

5
src/ast/rewriter/seq_derive.h
View file

@ -182,6 +182,11 @@ namespace seq {
*/
expr_ref operator()(expr* r);
/**
* Nullable check: returns a Boolean expression that is true iff r accepts the empty string.
*/
expr_ref nullable(expr* r) { return is_nullable(r); }
};
}

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

@ -2605,7 +2605,7 @@ expr_ref seq_rewriter::is_nullable(expr* r) {
<< mk_pp(r, m()) << std::endl;);
expr_ref result(m_op_cache.find(_OP_RE_IS_NULLABLE, r, nullptr, nullptr), m());
if (!result) {
result = is_nullable_rec(r);
result = m_derive.nullable(r);
m_op_cache.insert(_OP_RE_IS_NULLABLE, r, nullptr, nullptr, result);
}
STRACE(seq_verbose, tout << "is_nullable result: "
@ -2613,118 +2613,8 @@ expr_ref seq_rewriter::is_nullable(expr* r) {
return result;
}
expr_ref seq_rewriter::is_nullable_rec(expr* r) {
SASSERT(m_util.is_re(r) || m_util.is_seq(r));
expr* r1 = nullptr, *r2 = nullptr, *cond = nullptr;
sort* seq_sort = nullptr;
unsigned lo = 0, hi = 0;
zstring s1;
expr_ref result(m());
if (re().is_concat(r, r1, r2) ||
re().is_intersection(r, r1, r2)) {
m_br.mk_and(is_nullable(r1), is_nullable(r2), result);
}
else if (re().is_union(r, r1, r2) || re().is_antimirov_union(r, r1, r2)) {
m_br.mk_or(is_nullable(r1), is_nullable(r2), result);
}
else if (re().is_diff(r, r1, r2)) {
m_br.mk_not(is_nullable(r2), result);
m_br.mk_and(result, is_nullable(r1), result);
}
else if (re().is_xor(r, r1, r2)) {
// Null(r1 XOR r2) = Null(r1) XOR Null(r2)
expr_ref n1(is_nullable(r1), m());
expr_ref n2(is_nullable(r2), m());
// Simplify when either operand is a boolean literal so the
// bisimulation procedure can use the answer directly.
if (m().is_true(n1))
result = mk_not(m(), n2);
else if (m().is_false(n1))
result = n2;
else if (m().is_true(n2))
result = mk_not(m(), n1);
else if (m().is_false(n2))
result = n1;
else
result = m().mk_xor(n1, n2);
}
else if (re().is_star(r) ||
re().is_opt(r) ||
re().is_full_seq(r) ||
re().is_epsilon(r) ||
(re().is_loop(r, r1, lo) && lo == 0) ||
(re().is_loop(r, r1, lo, hi) && lo == 0)) {
result = m().mk_true();
}
else if (re().is_full_char(r) ||
re().is_empty(r) ||
re().is_of_pred(r) ||
re().is_range(r)) {
result = m().mk_false();
}
else if (re().is_plus(r, r1) ||
(re().is_loop(r, r1, lo) && lo > 0) ||
(re().is_loop(r, r1, lo, hi) && lo > 0) ||
(re().is_reverse(r, r1))) {
result = is_nullable(r1);
}
else if (re().is_complement(r, r1)) {
m_br.mk_not(is_nullable(r1), result);
}
else if (re().is_to_re(r, r1)) {
result = is_nullable(r1);
}
else if (m().is_ite(r, cond, r1, r2)) {
m_br.mk_ite(cond, is_nullable(r1), is_nullable(r2), result);
}
else if (m_util.is_re(r, seq_sort)) {
result = is_nullable_symbolic_regex(r, seq_sort);
}
else if (str().is_concat(r, r1, r2)) {
m_br.mk_and(is_nullable(r1), is_nullable(r2), result);
}
else if (str().is_empty(r)) {
result = m().mk_true();
}
else if (str().is_unit(r)) {
result = m().mk_false();
}
else if (str().is_string(r, s1)) {
result = m().mk_bool_val(s1.length() == 0);
}
else {
SASSERT(m_util.is_seq(r));
result = m().mk_eq(str().mk_empty(r->get_sort()), r);
}
return result;
}
expr_ref seq_rewriter::is_nullable_symbolic_regex(expr* r, sort* seq_sort) {
SASSERT(m_util.is_re(r));
expr* elem = nullptr, *r1 = r, * r2 = nullptr, * s = nullptr;
expr_ref elems(str().mk_empty(seq_sort), m());
expr_ref result(m());
while (re().is_derivative(r1, elem, r2)) {
if (str().is_empty(elems))
elems = str().mk_unit(elem);
else
elems = str().mk_concat(str().mk_unit(elem), elems);
r1 = r2;
}
if (re().is_to_re(r1, s)) {
// r is nullable
// iff after taking the derivatives the remaining sequence is empty
// iff the inner sequence equals to the sequence of derivative elements in reverse
result = m().mk_eq(elems, s);
return result;
}
// the default case when either r is not a derivative
// or when the nested derivatives are not applied to a sequence
result = re().mk_in_re(str().mk_empty(seq_sort), r);
return result;
}
/*
/ ()
Push reverse inwards (whenever possible).
*/
br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) {

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

@ -178,7 +178,6 @@ class seq_rewriter {
void replace_all_subvectors(expr_ref_vector const& as, expr_ref_vector const& bs, expr* c, expr_ref_vector& result);
// Calculate derivative, memoized and enforcing a normal form
expr_ref is_nullable_rec(expr* r);
expr_ref mk_der_op(decl_kind k, expr* a, expr* b);
expr_ref mk_der_op_rec(decl_kind k, expr* a, expr* b);
expr_ref mk_der_concat(expr* a, expr* b);
@ -189,8 +188,6 @@ class seq_rewriter {
expr_ref mk_der_cond(expr* cond, expr* ele, sort* seq_sort);
expr_ref mk_der_antimirov_union(expr* r1, expr* r2);
bool ite_bdds_compatible(expr* a, expr* b);
/* if r has the form deriv(en..deriv(e1,to_re(s))..) returns 's = [e1..en]' else returns '() in r'*/
expr_ref is_nullable_symbolic_regex(expr* r, sort* seq_sort);
#ifdef Z3DEBUG
bool check_deriv_normal_form(expr* r, int level = 3);
#endif