From 2793c3af2c2cae7e6e780e829fa6fbc15317aead Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 24 Apr 2020 00:48:02 -0700 Subject: [PATCH] more replace rewrites #4084 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 64 +++++++++++++++---------------- 1 file changed, 31 insertions(+), 33 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 710ccff4be6..de0f5be079b 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1420,45 +1420,43 @@ br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& resu } // is b a prefix of m_lhs at position i? - - unsigned i = 0; - for (; i < m_lhs.size(); ++i) { - lbool is_prefix = l_true; - for (unsigned j = 0; j < m_rhs.size(); ++j) { - if (i + j >= m_lhs.size()) { - expr_ref a1(m_util.str.mk_concat(i, m_lhs.c_ptr(), sort_a), m()); - expr_ref a2(m_util.str.mk_concat(m_lhs.size()-i, m_lhs.c_ptr()+i, sort_a), m()); - result = m().mk_ite(m().mk_eq(a2, b), m_util.str.mk_concat(a1, c), a); - return BR_REWRITE_FULL; - } + auto compare_at_i = [&](unsigned i) { + for (unsigned j = 0; j < m_rhs.size() && i + j < m_lhs.size(); ++j) { expr* b0 = m_rhs.get(j); - expr* a0 = m_lhs.get(i+j); - if (!m_util.str.is_unit(b0) || !m_util.str.is_unit(a0)) { - is_prefix = l_undef; - break; - } + expr* a0 = m_lhs.get(i + j); if (m().are_equal(a0, b0)) continue; - if (m().are_distinct(a0, b0)) { - is_prefix = l_false; - break; - } - is_prefix = l_undef; - break; + if (!m_util.str.is_unit(b0) || !m_util.str.is_unit(a0)) + return l_undef; + if (m().are_distinct(a0, b0)) + return l_false; + return l_undef; } - if (is_prefix == l_undef) - break; - if (is_prefix == l_false) + return l_true; + }; + + unsigned i = 0; + for (; i < m_lhs.size(); ++i) { + lbool cmp = compare_at_i(i); + if (cmp == l_false && m_util.str.is_unit(m_lhs.get(i))) continue; - expr_ref_vector es(m()); - //std::cout << i << " " << m_lhs << "\n"; - //std::cout << "rhs: " << m_rhs << "\n"; - es.append(i, m_lhs.c_ptr()); - es.push_back(c); - es.append(m_lhs.size()-i-m_rhs.size(), m_lhs.c_ptr()+i+m_rhs.size()); - result = m_util.str.mk_concat(es, sort_a); - return BR_REWRITE_FULL; + if (cmp == l_true && m_lhs.size() < i + m_rhs.size()) { + expr_ref a1(m_util.str.mk_concat(i, m_lhs.c_ptr(), sort_a), m()); + expr_ref a2(m_util.str.mk_concat(m_lhs.size()-i, m_lhs.c_ptr()+i, sort_a), m()); + result = m().mk_ite(m().mk_eq(a2, b), m_util.str.mk_concat(a1, c), a); + return BR_REWRITE_FULL; + } + if (cmp == l_true) { + expr_ref_vector es(m()); + es.append(i, m_lhs.c_ptr()); + es.push_back(c); + es.append(m_lhs.size()-i-m_rhs.size(), m_lhs.c_ptr()+i+m_rhs.size()); + result = m_util.str.mk_concat(es, sort_a); + return BR_REWRITE_FULL; + } + break; } + if (i > 0) { expr_ref a1(m_util.str.mk_concat(i, m_lhs.c_ptr(), sort_a), m()); expr_ref a2(m_util.str.mk_concat(m_lhs.size()-i, m_lhs.c_ptr()+i, sort_a), m());