mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

augment axiomatization for substr to fix #2366

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-07-12 11:12:01 +01:00
parent 1ba6d16c61
commit 79e4b84507
2 changed files with 57 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -653,6 +653,7 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
bool constantBase = m_util.str.is_string(a, s);
bool constantPos = m_autil.is_numeral(b, pos);
bool constantLen = m_autil.is_numeral(c, len);
bool lengthPos = m_util.str.is_length(b) || m_autil.is_add(b);
// case 1: pos<0 or len<=0
@ -693,6 +694,42 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
return BR_DONE;
}
// extract(a + b + c, len(a + b), s) -> extract(c, 0, s)
// extract(a + b + c, len(a) + len(b), s) -> extract(c, 0, s)
if (lengthPos) {
m_lhs.reset();
expr_ref_vector lens(m()), other(m());
m_util.str.get_concat(a, m_lhs);
get_lengths(b, lens, other, pos);
unsigned rsz = lens.size();
unsigned i = 0;
for (; i < rsz; ++i) {
expr* lhs = m_lhs.get(i);
if (lens.contains(lhs)) {
lens.erase(lhs);
}
else if (m_util.str.is_unit(lhs) && pos.is_pos()) {
pos -= rational(1);
}
else {
break;
}
}
if (i == 0) return BR_FAILED;
expr_ref t1(m()), t2(m());
t1 = m_util.str.mk_concat(m_lhs.size() - i, m_lhs.c_ptr() + i);
t2 = m_autil.mk_int(pos);
for (expr* rhs : lens) {
t2 = m_autil.mk_add(t2, m_util.str.mk_length(rhs));
}
for (expr* rhs : other) {
t2 = m_autil.mk_add(t2, m_util.str.mk_length(rhs));
}
result = m_util.str.mk_substr(t1, t2, c);
return BR_REWRITE2;
}
if (!constantPos) {
return BR_FAILED;
}
@ -740,6 +777,25 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
return BR_REWRITE3;
}
void seq_rewriter::get_lengths(expr* e, expr_ref_vector& lens, expr_ref_vector& other, rational& pos) {
expr* arg = nullptr;
rational pos1;
if (m_autil.is_add(e)) {
for (expr* arg1 : *to_app(e)) {
get_lengths(arg1, lens, other, pos);
}
}
else if (m_util.str.is_length(e, arg)) {
lens.push_back(arg);
}
else if (m_autil.is_numeral(e, pos1)) {
pos += pos1;
}
else {
other.push_back(e);
}
}
bool seq_rewriter::cannot_contain_suffix(expr* a, expr* b) {
if (m_util.str.is_unit(a) && m_util.str.is_unit(b) && m().are_distinct(a, b)) {