From 03ba26821947edc61163d1975d8b6675b1118cbf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 24 Apr 2020 00:25:36 -0700 Subject: [PATCH] more replace rewrites #4084 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 55 +++++++++++++++++++++++++++++++ src/ast/seq_decl_plugin.h | 1 + 2 files changed, 56 insertions(+) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 2ed819355..710ccff4b 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1410,6 +1410,61 @@ br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& resu result = m_util.str.mk_concat(m_lhs.size(), m_lhs.c_ptr(), sort_a); return BR_REWRITE1; } + m_lhs.reset(); + m_rhs.reset(); + m_util.str.get_concat_units(a, m_lhs); + m_util.str.get_concat_units(b, m_rhs); + if (m_rhs.empty()) { + result = m_util.str.mk_concat(c, a); + return BR_REWRITE1; + } + + // 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; + } + 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; + } + if (m().are_equal(a0, b0)) + continue; + if (m().are_distinct(a0, b0)) { + is_prefix = l_false; + break; + } + is_prefix = l_undef; + break; + } + if (is_prefix == l_undef) + break; + if (is_prefix == l_false) + 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 (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()); + result = m_util.str.mk_concat(a1, m_util.str.mk_replace(a2, b, c)); + return BR_REWRITE_FULL; + } return BR_FAILED; } diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 7fb119951..56bffa195 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -281,6 +281,7 @@ public: app* mk_suffix(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_SUFFIX, 2, es); } app* mk_index(expr* a, expr* b, expr* i) const { expr* es[3] = { a, b, i}; return m.mk_app(m_fid, OP_SEQ_INDEX, 3, es); } app* mk_last_index(expr* a, expr* b) const { expr* es[2] = { a, b}; return m.mk_app(m_fid, OP_SEQ_LAST_INDEX, 2, es); } + app* mk_replace(expr* a, expr* b, expr* c) const { expr* es[3] = { a, b, c}; return m.mk_app(m_fid, OP_SEQ_REPLACE, 3, es); } app* mk_unit(expr* u) const { return m.mk_app(m_fid, OP_SEQ_UNIT, 1, &u); } app* mk_char(zstring const& s, unsigned idx) const; app* mk_itos(expr* i) const { return m.mk_app(m_fid, OP_STRING_ITOS, 1, &i); }