mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

more rewrites for loop #4373

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-04-10 11:15:59 -07:00
parent 1a7c9fa54d
commit f607c15aa2
1 changed files with 11 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -4006,12 +4006,16 @@ br_status seq_rewriter::mk_re_loop(func_decl* f, unsigned num_args, expr* const*
np = f->get_num_parameters();
lo2 = np > 0 ? f->get_parameter(0).get_int() : 0;
hi2 = np > 1 ? f->get_parameter(1).get_int() : lo2;
// (loop a 0 0) = ""
if (np == 2 && lo2 > hi2) {
if (np == 2 && (lo2 > hi2 || hi2 < 0)) {
result = re().mk_empty(args[0]->get_sort());
return BR_DONE;
}
if (np == 2 && hi2 == 0) {
if (np == 1 && lo2 < 0) {
result = re().mk_empty(args[0]->get_sort());
return BR_DONE;
}
// (loop a 0 0) = ""
if (np == 2 && lo2 == 0 && hi2 == 0) {
result = re().mk_to_re(str().mk_empty(re().to_seq(args[0]->get_sort())));
return BR_DONE;
}
@ -4041,6 +4045,10 @@ br_status seq_rewriter::mk_re_loop(func_decl* f, unsigned num_args, expr* const*
result = re().mk_loop(args[0], n1.get_unsigned());
return BR_REWRITE1;
}
if (m_autil.is_numeral(args[1], n1) && n1 < 0) {
result = re().mk_empty(args[0]->get_sort());
return BR_DONE;
}
break;
case 3:
if (m_autil.is_numeral(args[1], n1) && n1.is_unsigned() &&