mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-21 08:00:27 +00:00
Code Activity

Add mk_range(sort*, unsigned, unsigned) smart constructor to seq_util::rex

Browse source
This commit is contained in:
copilot-swe-agent[bot] 2026-06-12 04:06:20 +00:00 • committed by GitHub
parent ee164a2705
commit 569468d9f8
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 17 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -3334,10 +3334,7 @@ expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) {
lo2_v <= hi1_v + 1 && lo1_v <= hi2_v + 1) {
unsigned new_lo = std::min(lo1_v, lo2_v);
unsigned new_hi = std::max(hi1_v, hi2_v);
if (new_lo == new_hi)
result = re().mk_to_re(str().mk_string(zstring(new_lo)));
else
result = re().mk_range(str().mk_string(zstring(new_lo)), str().mk_string(zstring(new_hi)));
result = re().mk_range(r1->get_sort(), new_lo, new_hi);
}
else
result = merge_regex_sets(r1, r2, re().mk_full_seq(r1->get_sort()), test, compose);
@ -3376,12 +3373,7 @@ expr_ref seq_rewriter::mk_regex_inter_normalize(expr* r1, expr* r2) {
if (re().is_range(r1, lo1_v, hi1_v) && re().is_range(r2, lo2_v, hi2_v)) {
unsigned new_lo = std::max(lo1_v, lo2_v);
unsigned new_hi = std::min(hi1_v, hi2_v);
if (new_lo > new_hi)
result = re().mk_empty(r1->get_sort());
else if (new_lo == new_hi)
result = re().mk_to_re(str().mk_string(zstring(new_lo)));
else
result = re().mk_range(str().mk_string(zstring(new_lo)), str().mk_string(zstring(new_hi)));
result = re().mk_range(r1->get_sort(), new_lo, new_hi);
}
else
result = merge_regex_sets(r1, r2, re().mk_empty(r1->get_sort()), test, compose);
@ -4828,17 +4820,17 @@ 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_range(str().mk_string(zstring(hi_v + 1)), str().mk_string(zstring(max_c)));
result = re().mk_range(srt, hi_v + 1, max_c);
return BR_REWRITE1;
}
if (!has_right) {
// [a, max]: complement is [0, a-1]
result = re().mk_range(str().mk_string(zstring(0u)), str().mk_string(zstring(lo_v - 1)));
result = re().mk_range(srt, 0u, lo_v - 1);
return BR_REWRITE1;
}
// General: [a, b] → [0, a-1] ∪ [b+1, max]
auto left = re().mk_range(str().mk_string(zstring(0u)), str().mk_string(zstring(lo_v - 1)));
auto right = re().mk_range(str().mk_string(zstring(hi_v + 1)), str().mk_string(zstring(max_c)));
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(left, right);
return BR_REWRITE1;
}

9
src/ast/seq_decl_plugin.cpp
View file

@ -1208,6 +1208,15 @@ app* seq_util::rex::mk_of_pred(expr* p) {
return m.mk_app(m_fid, OP_RE_OF_PRED, 0, nullptr, 1, &p);
}
app* seq_util::rex::mk_range(sort* re_sort, unsigned lo, unsigned hi) {
if (lo > hi)
return mk_empty(re_sort);
app* lo_str = u.str.mk_string(zstring(lo));
if (lo == hi)
return mk_to_re(lo_str);
return mk_range(lo_str, u.str.mk_string(zstring(hi)));
}
bool seq_util::rex::is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi) const {
if (is_loop(n)) {
app const* a = to_app(n);

2
src/ast/seq_decl_plugin.h
View file

@ -521,6 +521,8 @@ public:
app* mk_to_re(expr* s) { return m.mk_app(m_fid, OP_SEQ_TO_RE, 1, &s); }
app* mk_in_re(expr* s, expr* r) { return m.mk_app(m_fid, OP_SEQ_IN_RE, s, r); }
app* mk_range(expr* s1, expr* s2) { return m.mk_app(m_fid, OP_RE_RANGE, s1, s2); }
// Smart constructor: returns re.empty / str.to_re / re.range based on lo vs hi.
app* mk_range(sort* re_sort, unsigned lo, unsigned hi);
app* mk_concat(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_CONCAT, r1, r2); }
app* mk_union(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_UNION, r1, r2); }
app* mk_inter(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_INTERSECT, r1, r2); }