mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

Regex range bug fix (#5601)

Browse source 
* added a missing derivative case for nonground range

* further missing cases and a bug fix in re.to_str
This commit is contained in:
Margus Veanes 2021-10-15 15:30:55 -07:00 committed by GitHub
parent 6302b864c8
commit cb120c93f4
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 50 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -3126,21 +3126,49 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref
}
else if (re().is_range(r, r1, r2)) {
expr_ref range(m());
expr_ref psi(m());
expr_ref psi(m().mk_false(), m());
if (str().is_unit_string(r1, c1) && str().is_unit_string(r2, c2)) {
SASSERT(u().is_char(c1));
SASSERT(u().is_char(c2));
// range represents c1 <= e <= c2
// case: c1 <= e <= c2
range = simplify_path(m().mk_and(u().mk_le(c1, e), u().mk_le(e, c2)));
psi = simplify_path(m().mk_and(path, range));
if (m().is_false(psi))
result = nothing();
else
// D(e,c1..c2) = if (c1<=e<=c2) then () else []
result = re().mk_ite_simplify(range, epsilon(), nothing());
}
else
else if (!str().is_string(r1) && str().is_unit_string(r2, c2)) {
SASSERT(u().is_char(c2));
// r1 nonground: |r1|=1 & r1[0] <= e <= c2
expr_ref one(m_autil.mk_int(1), m());
expr_ref zero(m_autil.mk_int(0), m());
expr_ref r1_length_eq_one(m().mk_eq(str().mk_length(r1), one), m());
expr_ref r1_0(str().mk_nth_i(r1, zero), m());
range = simplify_path(m().mk_and(r1_length_eq_one, m().mk_and(u().mk_le(r1_0, e), u().mk_le(e, c2))));
psi = simplify_path(m().mk_and(path, range));
}
else if (!str().is_string(r2) && str().is_unit_string(r1, c1)) {
SASSERT(u().is_char(c1));
// r2 nonground: |r2|=1 & c1 <= e <= r2_0
expr_ref one(m_autil.mk_int(1), m());
expr_ref zero(m_autil.mk_int(0), m());
expr_ref r2_length_eq_one(m().mk_eq(str().mk_length(r2), one), m());
expr_ref r2_0(str().mk_nth_i(r2, zero), m());
range = simplify_path(m().mk_and(r2_length_eq_one, m().mk_and(u().mk_le(c1, e), u().mk_le(e, r2_0))));
psi = simplify_path(m().mk_and(path, range));
}
else if (!str().is_string(r1) && !str().is_string(r2)) {
// both r1 and r2 nonground: |r1|=1 & |r2|=1 & r1[0] <= e <= r2[0]
expr_ref one(m_autil.mk_int(1), m());
expr_ref zero(m_autil.mk_int(0), m());
expr_ref r1_length_eq_one(m().mk_eq(str().mk_length(r1), one), m());
expr_ref r1_0(str().mk_nth_i(r1, zero), m());
expr_ref r2_length_eq_one(m().mk_eq(str().mk_length(r2), one), m());
expr_ref r2_0(str().mk_nth_i(r2, zero), m());
range = simplify_path(m().mk_and(r1_length_eq_one, m().mk_and(r2_length_eq_one, m().mk_and(u().mk_le(r1_0, e), u().mk_le(e, r2_0)))));
psi = simplify_path(m().mk_and(path, range));
}
if (m().is_false(psi))
result = nothing();
else
result = re().mk_ite_simplify(range, epsilon(), nothing());
}
else if (re().is_union(r, r1, r2))
result = mk_antimirov_deriv_union(mk_antimirov_deriv(e, r1, path), mk_antimirov_deriv(e, r2, path));

28
src/ast/seq_decl_plugin.cpp
View file

@ -1233,11 +1233,11 @@ std::ostream& seq_util::rex::pp::print_unit(std::ostream& out, expr* s) const {
print(out, e);
out << "[" << mk_pp(i, re.m) << "]";
}
else if (re.m.is_value(e))
out << mk_pp(e, re.m);
else if (is_app(e)) {
out << "(" << to_app(e)->get_decl()->get_name().str();
for (expr * arg : *to_app(e))
else if (re.m.is_value(s))
out << mk_pp(s, re.m);
else if (is_app(s)) {
out << "(" << to_app(s)->get_decl()->get_name().str();
for (expr * arg : *to_app(s))
print(out << " ", arg);
out << ")";
}
@ -1266,11 +1266,11 @@ std::ostream& seq_util::rex::pp::print(std::ostream& out, expr* e) const {
else if (re.is_range(e, s, s2))
print_range(out, s, s2);
else if (re.is_epsilon(e))
// &#X03B5; = epsilon
out << (html_encode ? "&#X03B5;" : "()");
// &#x03B5; = epsilon
out << (html_encode ? "&#x03B5;" : "()");
else if (re.is_empty(e))
// &#X2205; = emptyset
out << (html_encode ? "&#X2205;" : "[]");
// &#x2205; = emptyset
out << (html_encode ? "&#x2205;" : "[]");
else if (re.is_concat(e, r1, r2)) {
print(out, r1);
print(out, r2);
@ -1278,7 +1278,7 @@ std::ostream& seq_util::rex::pp::print(std::ostream& out, expr* e) const {
else if (re.is_antimorov_union(e, r1, r2) || re.is_union(e, r1, r2)) {
out << "(";
print(out, r1);
out << (html_encode ? "&#X22C3;" : "|");
out << (html_encode ? "&#x22C3;" : "|");
print(out, r2);
out << ")";
}
@ -1286,7 +1286,7 @@ std::ostream& seq_util::rex::pp::print(std::ostream& out, expr* e) const {
{
out << "(";
print(out, r1);
out << (html_encode ? "&#X22C2;" : "&");
out << (html_encode ? "&#x22C2;" : "&");
print(out, r2);
out << ")";
}
@ -1359,11 +1359,11 @@ std::ostream& seq_util::rex::pp::print(std::ostream& out, expr* e) const {
out << ")";
}
else if (re.m.is_ite(e, s, r1, r2)) {
out << (html_encode ? "(&#X1D422;&#X1D41F; " : "(if ");
out << (html_encode ? "(&#x1D422;&#x1D41F; " : "(if ");
print(out, s);
out << (html_encode ? " &#X1D42D;&#X1D5F5;&#X1D41E;&#X1D427; " : " then ");
out << (html_encode ? " &#x1D42D;&#x1D5F5;&#x1D41E;&#x1D427; " : " then ");
print(out, r1);
out << (html_encode ? " &#X1D41E;&#X1D425;&#X1D600;&#X1D41E; " : " else ");
out << (html_encode ? " &#x1D41E;&#x1D425;&#x1D600;&#x1D41E; " : " else ");
print(out, r2);
out << ")";
}