mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-13 22:41:15 +00:00
Code Activity

more replace rewrites #4084

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-24 00:25:36 -07:00
parent 7597396dd0
commit 03ba268219
2 changed files with 56 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -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;
}