mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-22 16:40:29 +00:00
Code Activity

use empty sequence regex instead of empty set regex

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-21 16:25:56 -07:00
parent c0ec4259e5
commit f487af3071
1 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -4829,10 +4829,12 @@ br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) {
unsigned lo_v = 0, hi_v = 0;
if (re().is_range(a, lo_v, hi_v)) {
unsigned max_c = u().max_char();
sort* srt = a->get_sort();
sort *srt = a->get_sort(), *seq_sort;
VERIFY(m_util.is_re(a, seq_sort));
bool has_left = (lo_v > 0);
bool has_right = (hi_v < max_c);
auto empty_re = [&]() { return re().mk_empty(srt); };
auto len0_re = [&]() { return re().mk_to_re(str().mk_empty(seq_sort)); };
auto full_re = [&]() { return re().mk_full_seq(srt); };
if (!has_left && !has_right) {
// [0, max_c]: complement is empty
@ -4845,18 +4847,18 @@ br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) {
}
if (!has_left) {
// [0, b]: complement is [b+1, max]
result = re().mk_union(empty_re(), re().mk_concat(re().mk_range(srt, hi_v + 1, max_c), full_re()));
result = re().mk_union(len0_re(), re().mk_concat(re().mk_range(srt, hi_v + 1, max_c), full_re()));
return BR_DONE;
}
if (!has_right) {
// [a, max]: complement is [0, a-1]
result = re().mk_union(empty_re(), re().mk_concat(re().mk_range(srt, 0u, lo_v - 1), full_re()));
result = re().mk_union(len0_re(), re().mk_concat(re().mk_range(srt, 0u, lo_v - 1), full_re()));
return BR_DONE;
}
// General: [a, b] → [0, a-1] ∪ [b+1, max]
auto left = re().mk_range(srt, 0u, lo_v - 1);
auto right = re().mk_range(srt, hi_v + 1, max_c);
result = re().mk_union(empty_re(), re().mk_concat(re().mk_union(left, right), full_re()));
result = re().mk_union(len0_re(), re().mk_concat(re().mk_union(left, right), full_re()));
return BR_DONE;
}
return BR_FAILED;