From 8f4e7f49618f3893c2ef228fcd3aefbdfa1b6a7b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 3 Sep 2019 23:47:25 -0700 Subject: [PATCH] fix #2533 Signed-off-by: Nikolaj Bjorner --- src/ast/for_each_expr.cpp | 2 +- src/ast/rewriter/seq_rewriter.cpp | 39 +++++++++++++++++++++++-------- 2 files changed, 30 insertions(+), 11 deletions(-) diff --git a/src/ast/for_each_expr.cpp b/src/ast/for_each_expr.cpp index dd8a546f9..36df206cf 100644 --- a/src/ast/for_each_expr.cpp +++ b/src/ast/for_each_expr.cpp @@ -87,7 +87,7 @@ subterms::iterator& subterms::iterator::operator++() { m_es.push_back(arg); } } - while (m_visited.is_marked(m_es.back())) { + while (!m_es.empty() && m_visited.is_marked(m_es.back())) { m_es.pop_back(); } return *this; diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 6ee1e07ea..94a15e7f4 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -547,7 +547,7 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case _OP_STRING_STRIDOF: UNREACHABLE(); } - CTRACE("seq_verbose", st != BR_FAILED, tout << result << "\n";); + CTRACE("seq_verbose", st != BR_FAILED, tout << f->get_name() << " " << result << "\n";); return st; } @@ -1142,16 +1142,35 @@ br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& resu result = m_util.str.mk_concat(c, a); return BR_REWRITE1; } - - if (m_util.str.is_string(b, s2)) { - m_lhs.reset(); - m_util.str.get_concat(a, m_lhs); - if (!m_lhs.empty() && m_util.str.is_string(m_lhs.get(0), s1) && - s1.contains(s2)) { - m_lhs[0] = m_util.str.mk_string(s1.replace(s2, s3)); - result = m_util.str.mk_concat(m_lhs.size(), m_lhs.c_ptr()); - return BR_REWRITE1; + + m_lhs.reset(); + m_util.str.get_concat(a, m_lhs); + + // a = "", |b| > 0 -> replace("",b,c) = "" + if (m_lhs.empty()) { + unsigned len = 0; + m_util.str.get_concat(b, m_lhs); + min_length(m_lhs.size(), m_lhs.c_ptr(), len); + if (len > 0) { + result = a; + return BR_DONE; } + return BR_FAILED; + } + + // a := b + rest + if (m_lhs.get(0) == b) { + m_lhs[0] = c; + result = m_util.str.mk_concat(m_lhs.size(), m_lhs.c_ptr()); + return BR_REWRITE1; + } + + // a : a' + rest string, b is string, c is string, a' contains b + if (m_util.str.is_string(b, s2) && m_util.str.is_string(c, s3) && + m_util.str.is_string(m_lhs.get(0), s1) && s1.contains(s2) ) { + m_lhs[0] = m_util.str.mk_string(s1.replace(s2, s3)); + result = m_util.str.mk_concat(m_lhs.size(), m_lhs.c_ptr()); + return BR_REWRITE1; } return BR_FAILED;