mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-26 02:25:32 +00:00
Code Activity

fix max/min length to handle concatenation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-10-09 16:20:32 -07:00
parent f1b8376739
commit 0fc9f1d46a
1 changed files with 8 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ast/seq_decl_plugin.cpp
View file

@ -932,7 +932,10 @@ unsigned seq_util::str::min_length(expr* s) const {
return 0u;
};
while (is_concat(s, s1, s2)) {
result += get_length(s1);
if (is_concat(s1))
result += min_length(s1);
else
result += get_length(s1);
s = s2;
}
result += get_length(s);
@ -960,7 +963,10 @@ unsigned seq_util::str::max_length(expr* s) const {
return UINT_MAX;
};
while (is_concat(s, s1, s2)) {
result = u.max_plus(get_length(s1), result);
if (is_concat(s1))
result = u.max_plus(max_length(s1), result);
else
result = u.max_plus(get_length(s1), result);
s = s2;
}
result = u.max_plus(get_length(s), result);