mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-22 15:05:51 +00:00
Code Activity

fold functionality into seq_range_collapse

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-07-15 20:04:48 -07:00
parent 9fb2b491d6
commit 2db625606d
2 changed files with 97 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

104
src/ast/rewriter/seq_range_collapse.cpp
View file

@ -21,6 +21,74 @@ Authors:
namespace seq {
// Cofactor path condition `pred` (a Boolean over x = (:var 0)) -> the canonical
// range_predicate (union of ranges) of the characters satisfying it. Returns
// false on a construct outside {true,false,and,or,not,=,char.<=} over x.
static bool pred_to_rp(ast_manager &m, seq_util &sq, expr *x, expr *pred,
seq::range_predicate &out) {
unsigned maxc = sq.max_char();
expr *a = nullptr, *b = nullptr;
unsigned c = 0;
if (m.is_true(pred)) {
out = seq::range_predicate::top(maxc);
return true;
}
if (m.is_false(pred)) {
out = seq::range_predicate::empty(maxc);
return true;
}
if (m.is_eq(pred, a, b)) {
if (a == x && sq.is_const_char(b, c)) {
out = seq::range_predicate::singleton(c, maxc);
return true;
}
if (b == x && sq.is_const_char(a, c)) {
out = seq::range_predicate::singleton(c, maxc);
return true;
}
return false;
}
if (sq.is_char_le(pred, a, b)) {
if (b == x && sq.is_const_char(a, c)) {
out = seq::range_predicate::range(c, maxc, maxc);
return true;
}
if (a == x && sq.is_const_char(b, c)) {
out = seq::range_predicate::range(0, c, maxc);
return true;
}
return false;
}
if (m.is_not(pred, a)) {
seq::range_predicate s(maxc);
if (!pred_to_rp(m, sq, x, a, s))
return false;
out = ~s;
return true;
}
if (m.is_and(pred)) {
out = seq::range_predicate::top(maxc);
for (expr *arg : *to_app(pred)) {
seq::range_predicate s(maxc);
if (!pred_to_rp(m, sq, x, arg, s))
return false;
out = out & s;
}
return true;
}
if (m.is_or(pred)) {
out = seq::range_predicate::empty(maxc);
for (expr *arg : *to_app(pred)) {
seq::range_predicate s(maxc);
if (!pred_to_rp(m, sq, x, arg, s))
return false;
out = out | s;
}
return true;
}
return false;
}
bool regex_to_range_predicate(seq_util& u, expr* r, range_predicate& out) {
// The range algebra only models sets of single characters over the
// unsigned character domain [0, max_char]. Guard against any regex
@ -35,6 +103,7 @@ namespace seq {
unsigned const max_char = u.max_char();
auto& re = u.re;
auto &m = u.get_manager();
if (re.is_empty(r)) {
out = range_predicate::empty(max_char);
@ -72,8 +141,10 @@ namespace seq {
expr *a = nullptr, *b = nullptr, *c = nullptr;
if (re.is_union(r, a, b)) {
range_predicate pa(max_char), pb(max_char);
if (!regex_to_range_predicate(u, a, pa)) return false;
if (!regex_to_range_predicate(u, b, pb)) return false;
if (!regex_to_range_predicate(u, a, pa))
return false;
if (!regex_to_range_predicate(u, b, pb))
return false;
out = pa | pb;
return true;
}
@ -97,12 +168,22 @@ namespace seq {
if (re.is_intersection(r, a, b)) {
range_predicate pa(max_char), pb(max_char);
if (!regex_to_range_predicate(u, a, pa)) return false;
if (!regex_to_range_predicate(u, b, pb)) return false;
if (!regex_to_range_predicate(u, a, pa))
return false;
if (!regex_to_range_predicate(u, b, pb))
return false;
out = pa & pb;
return true;
}
if (re.is_of_pred(r, a)) {
sort *char_sort = nullptr;
VERIFY(u.is_seq(seq_sort, char_sort));
expr_ref var(m.mk_var(0, char_sort), m);
if (pred_to_rp(m, u, var, a, out))
return true;
}
// NOTE: re.complement is intentionally NOT handled here.
// re.complement is the SEQUENCE-level complement: its language
@ -130,6 +211,8 @@ namespace seq {
expr_ref range_predicate_to_regex(seq_util& u, range_predicate const& p, sort* seq_sort) {
ast_manager& m = u.get_manager();
sort* re_sort = u.re.mk_re(seq_sort);
sort *char_sort = nullptr;
VERIFY(u.is_seq(seq_sort, char_sort));
if (p.is_empty())
return expr_ref(u.re.mk_empty(re_sort), m);
unsigned const n = p.num_ranges();
@ -145,16 +228,15 @@ namespace seq {
// when it has to combine our materialized output with another
// (id-sorted) regex set.
expr_ref_vector ranges(m);
expr_ref bound(m.mk_var(0, char_sort), m);
symbol char_sym("ch");
auto &ch = u.get_char_plugin();
for (unsigned i = 0; i < n; ++i) {
auto [lo, hi] = p[i];
ranges.push_back(mk_single_range_regex(u, lo, hi, re_sort));
ranges.push_back(m.mk_and(ch.mk_le(ch.mk_char(lo), bound), ch.mk_le(bound, ch.mk_char(hi))));
}
std::sort(ranges.data(), ranges.data() + ranges.size(),
[](expr* a, expr* b) { return a->get_id() < b->get_id(); });
expr_ref acc(ranges.get(n - 1), m);
for (unsigned i = n - 1; i-- > 0; )
acc = expr_ref(u.re.mk_union(ranges.get(i), acc), m);
return acc;
expr_ref body(m.mk_or(ranges), m);
return expr_ref(m.mk_lambda(1, &char_sort, &char_sym, body), m);
}
}

5
src/ast/seq_decl_plugin.h
View file

@ -228,6 +228,9 @@ public:
unsigned max_mul(unsigned x, unsigned y) const;
ast_manager& get_manager() const { return m; }
char_decl_plugin &get_char_plugin() const {
return ch;
}
sort* mk_char_sort() const { return seq.char_sort(); }
sort* mk_string_sort() const { return seq.string_sort(); }
@ -239,7 +242,7 @@ public:
bool is_re(sort* s) const { return is_sort_of(s, m_fid, RE_SORT); }
bool is_re(sort* s, sort*& seq) const { return is_sort_of(s, m_fid, RE_SORT) && (seq = to_sort(s->get_parameter(0).get_ast()), true); }
bool is_seq(expr* e) const { return is_seq(e->get_sort()); }
bool is_seq(sort* s, sort*& seq) const { return is_seq(s) && (seq = to_sort(s->get_parameter(0).get_ast()), true); }
bool is_seq(sort* s, sort*& ch) const { return is_seq(s) && (ch = to_sort(s->get_parameter(0).get_ast()), true); }
bool is_re(expr* e) const { return is_re(e->get_sort()); }
bool is_re(expr* e, sort*& seq) const { return is_re(e->get_sort(), seq); }
bool is_const_char(expr* e, unsigned& c) const;