mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

approximate min-length for complements

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-18 22:04:09 -07:00
parent 4857d60c99
commit ed258ca019
1 changed files with 2 additions and 3 deletions

5
src/ast/seq_decl_plugin.cpp
View file

@ -1668,8 +1668,7 @@ seq_util::re::info seq_util::re::mk_info_rec(app* e) const {
case OP_RE_PLUS:
return get_info_rec(e->get_arg(0));
case OP_RE_COMPLEMENT:
i1 = get_info_rec(e->get_arg(0));
return info(i1.min_length > 0 ? 0 : UINT_MAX);
return info(0);
case OP_RE_LOOP:
i1 = get_info_rec(e->get_arg(0));
return info(u.max_mul(i1.min_length, e->get_decl()->get_parameter(0).get_int()));
@ -1687,4 +1686,4 @@ seq_util::re::info seq_util::re::mk_info_rec(app* e) const {
return info(std::min(i1.min_length, i2.min_length));
}
return invalid_info;
}
}