mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 17:14:07 +00:00
Code Activity

improved regex merging avoiding unsat nontermination (#5728)

Browse source
This commit is contained in:
Margus Veanes 2021-12-20 17:44:06 -08:00 committed by GitHub
parent e0d6e04493
commit 1d9aad6ea9
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -3331,7 +3331,7 @@ expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) {
SASSERT(m_util.is_re(r2));
expr_ref result(m());
std::function<bool(expr*, expr*&, expr*&)> test = [&](expr* t, expr*& a, expr*& b) { return re().is_union(t, a, b); };
std::function<expr* (expr*, expr*)> compose = [&](expr* r1, expr* r2) { return re().mk_union(r1, r2); };
std::function<expr* (expr*, expr*)> compose = [&](expr* r1, expr* r2) { return (is_subset(r1, r2) ? r2 : (is_subset(r2, r1) ? r1 : re().mk_union(r1, r2))); };
if (r1 == r2 || re().is_empty(r2) || re().is_full_seq(r1))
result = r1;
else if (re().is_empty(r1) || re().is_full_seq(r2))
@ -3353,7 +3353,7 @@ expr_ref seq_rewriter::mk_regex_inter_normalize(expr* r1, expr* r2) {
if (re().is_epsilon(r2))
std::swap(r1, r2);
std::function<bool(expr*, expr*&, expr*&)> test = [&](expr* t, expr*& a, expr*& b) { return re().is_intersection(t, a, b); };
std::function<expr* (expr*, expr*)> compose = [&](expr* r1, expr* r2) { return re().mk_inter(r1, r2); };
std::function<expr* (expr*, expr*)> compose = [&](expr* r1, expr* r2) { return (is_subset(r1, r2) ? r1 : (is_subset(r2, r1) ? r2 : re().mk_inter(r1, r2))); };
if (r1 == r2 || re().is_empty(r1) || re().is_full_seq(r2))
result = r1;
else if (re().is_empty(r2) || re().is_full_seq(r1))
@ -4598,6 +4598,8 @@ bool seq_rewriter::is_subset(expr* r1, expr* r2) const {
return true;
if (re().is_full_seq(r2))
return true;
if (re().is_dot_plus(r2) && re().get_info(r1).nullable == l_false)
return true;
if (is_concat(r1, ra1, ra2, ra3) &&
is_concat(r2, rb1, rb2, rb3) && ra1 == rb1 && ra2 == rb2) {
r1 = ra3;