mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 03:15:50 +00:00
Code Activity

fix #5784

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-01-21 03:08:03 +01:00
parent 17280846f8
commit 007af9cb8a
1 changed files with 24 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -5572,42 +5572,37 @@ bool seq_rewriter::min_length(expr_ref_vector const& es, unsigned& len) {
}
bool seq_rewriter::max_length(expr* e, rational& len) {
if (str().is_unit(e)) {
len = 1;
return true;
}
if (str().is_at(e)) {
len = 1;
return true;
}
ptr_buffer<expr> es;
es.push_back(e);
len = 0;
zstring s;
if (str().is_string(e, s)) {
len = rational(s.length());
return true;
}
if (str().is_empty(e)) {
len = 0;
return true;
}
expr* s1 = nullptr, *i = nullptr, *l = nullptr;
rational n;
if (str().is_extract(e, s1, i, l) && m_autil.is_numeral(l, n) && !n.is_neg()) {
len = n;
return true;
}
if (str().is_concat(e)) {
rational l(0);
len = 0;
for (expr* arg : *to_app(e)) {
if (!max_length(arg, l))
return false;
len += l;
while (!es.empty()) {
e = es.back();
es.pop_back();
if (str().is_unit(e))
len += 1;
else if (str().is_at(e))
len += 1;
else if (str().is_string(e, s))
len += rational(s.length());
else if (str().is_extract(e, s1, i, l) && m_autil.is_numeral(l, n) && !n.is_neg())
len += n;
else if (str().is_empty(e))
continue;
else if (str().is_concat(e)) {
for (expr* arg : *to_app(e))
es.push_back(arg);
}
return true;
else
return false;
}
return false;
return true;
}
bool seq_rewriter::is_string(unsigned n, expr* const* es, zstring& s) const {
zstring s1;
expr* e;