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

#5140

Browse source 
@veanes
mk_bool_app_helper has a bug:
When it simplifies a disjunction or conjunction of regex membership constraints of the form (and (str.in_re "" R) (str.in_re x Q))
then the first term (str.in_re "" R) is omitted in the result.
You have a test here
3da9d91866/src/ast/rewriter/seq_rewriter.cpp (L438)
that means a regex membership with empty first argument is not put in the two buffers with membership/non-membership.
It isn't put into new_args either because the test bypasses these
3da9d91866/src/ast/rewriter/seq_rewriter.cpp (L485)
This commit is contained in:
Nikolaj Bjorner 2021-06-06 20:30:09 -07:00
parent 3da9d91866
commit 92ec81d108
2 changed files with 21 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -432,6 +432,7 @@ br_status seq_rewriter::mk_bool_app_helper(bool is_and, unsigned n, expr* const*
obj_map<expr, expr*> in_re, not_in_re; obj_map<expr, expr*> in_re, not_in_re;
bool found_pair = false; bool found_pair = false;
ptr_buffer<expr> new_args;
for (unsigned i = 0; i < n; ++i) { for (unsigned i = 0; i < n; ++i) {
expr* args_i = args[i]; expr* args_i = args[i];
expr* x = nullptr, *y = nullptr, *z = nullptr; expr* x = nullptr, *y = nullptr, *z = nullptr;
@ -455,13 +456,15 @@ br_status seq_rewriter::mk_bool_app_helper(bool is_and, unsigned n, expr* const*
found_pair |= in_re.contains(x); found_pair |= in_re.contains(x);
} }
} }
else
new_args.push_back(args_i);
} }
if (!found_pair) { if (!found_pair) {
return BR_FAILED; return BR_FAILED;
} }
ptr_buffer<expr> new_args;
for (auto const & kv : in_re) { for (auto const & kv : in_re) {
expr* x = kv.m_key; expr* x = kv.m_key;
expr* y = kv.m_value; expr* y = kv.m_value;
@ -482,12 +485,6 @@ br_status seq_rewriter::mk_bool_app_helper(bool is_and, unsigned n, expr* const*
new_args.push_back(re().mk_in_re(x, re().mk_complement(y))); new_args.push_back(re().mk_in_re(x, re().mk_complement(y)));
} }
} }
for (unsigned i = 0; i < n; ++i) {
expr* arg = args[i], * x;
if (!str().is_in_re(arg) && !(m().is_not(arg, x) && str().is_in_re(x))) {
new_args.push_back(arg);
}
}
result = is_and ? m().mk_and(new_args) : m().mk_or(new_args); result = is_and ? m().mk_and(new_args) : m().mk_or(new_args);
return BR_REWRITE_FULL; return BR_REWRITE_FULL;
@ -2500,7 +2497,7 @@ expr_ref seq_rewriter::is_nullable(expr* r) {
m_op_cache.insert(_OP_RE_IS_NULLABLE, r, nullptr, result); m_op_cache.insert(_OP_RE_IS_NULLABLE, r, nullptr, result);
} }
STRACE("seq_verbose", tout << "is_nullable result: " STRACE("seq_verbose", tout << "is_nullable result: "
<< mk_pp(result, m()) << std::endl;); << result << std::endl;);
return result; return result;
} }

17
src/ast/seq_decl_plugin.cpp
View file

@ -1269,7 +1269,22 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const {
case OP_RE_OPTION: case OP_RE_OPTION:
i1 = get_info_rec(e->get_arg(0)); i1 = get_info_rec(e->get_arg(0));
return i1.opt(); return i1.opt();
case OP_RE_RANGE: case OP_RE_RANGE: {
lbool is_nullable = l_undef;
bool is_singleton = false;
bool is_interpreted = false;
zstring s1, s2;
expr* r1, *r2;
if (is_range(e, r1, r2) &&
u.str.is_string(r1, s1) && u.str.is_string(r2, s2) &&
s1.length() == 1 && s2.length() == 1 && s1[0] <= s2[0]) {
is_nullable = l_false;
is_singleton = true;
is_interpreted = true;
}
std::cout << is_nullable << "\n";
return info(true, true, is_interpreted, true, true, true, is_singleton, is_nullable, 1, 0);
}
case OP_RE_FULL_CHAR_SET: case OP_RE_FULL_CHAR_SET:
case OP_RE_OF_PRED: case OP_RE_OF_PRED:
//TBD: check if the character predicate contains uninterpreted symbols or is nonground or is unsat //TBD: check if the character predicate contains uninterpreted symbols or is nonground or is unsat