From 92ec81d1085f861bc296cad95f21eae2351a8172 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 6 Jun 2021 20:30:09 -0700 Subject: [PATCH] #5140 @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 https://github.com/Z3Prover/z3/blob/3da9d91866fa18aee1281a1ea6d2d7ab55589740/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 https://github.com/Z3Prover/z3/blob/3da9d91866fa18aee1281a1ea6d2d7ab55589740/src/ast/rewriter/seq_rewriter.cpp#L485 --- src/ast/rewriter/seq_rewriter.cpp | 13 +++++-------- src/ast/seq_decl_plugin.cpp | 17 ++++++++++++++++- 2 files changed, 21 insertions(+), 9 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 0ca46f082..9049ad971 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -432,6 +432,7 @@ br_status seq_rewriter::mk_bool_app_helper(bool is_and, unsigned n, expr* const* obj_map in_re, not_in_re; bool found_pair = false; + ptr_buffer new_args; for (unsigned i = 0; i < n; ++i) { expr* args_i = args[i]; 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); } } + else + new_args.push_back(args_i); } if (!found_pair) { return BR_FAILED; } - ptr_buffer new_args; + for (auto const & kv : in_re) { expr* x = kv.m_key; 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))); } } - 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); 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); } STRACE("seq_verbose", tout << "is_nullable result: " - << mk_pp(result, m()) << std::endl;); + << result << std::endl;); return result; } diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 5213bbba9..847e56076 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -1269,7 +1269,22 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const { case OP_RE_OPTION: i1 = get_info_rec(e->get_arg(0)); 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_OF_PRED: //TBD: check if the character predicate contains uninterpreted symbols or is nonground or is unsat