diff --git a/src/ast/rewriter/seq_range_collapse.cpp b/src/ast/rewriter/seq_range_collapse.cpp index 8bd725cbe..5ad71a5a9 100644 --- a/src/ast/rewriter/seq_range_collapse.cpp +++ b/src/ast/rewriter/seq_range_collapse.cpp @@ -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); } } diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 9de2c0152..fd5696f49 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -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;