mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

bug fixes in nullability check

Browse source 
@veanes @cdstanford
This commit is contained in:
Nikolaj Bjorner 2020-11-13 17:05:10 -08:00
parent c15001bf69
commit 9fa17a432a
2 changed files with 5 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2302,17 +2302,17 @@ expr_ref seq_rewriter::is_nullable_rec(expr* r) {
expr_ref seq_rewriter::is_nullable_symbolic_regex(expr* r, sort* seq_sort) {
SASSERT(m_util.is_re(r));
expr* elem = nullptr, * r2 = nullptr, * s = nullptr;
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(r, elem, r2)) {
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);
r = r2;
r1 = r2;
}
if (re().is_to_re(r, s)) {
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

1
src/smt/seq_regex.cpp
View file

@ -323,6 +323,7 @@ namespace smt {
literal is_nullable_lit = th.mk_literal(is_nullable);
ctx.mark_as_relevant(is_nullable_lit);
th.add_axiom(~lit, ~len_s_le_i, is_nullable_lit);
th.add_unhandled_expr(is_nullable);
}
}