mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-29 03:48:51 +00:00
Code Activity

disable some unit tests, use smart constructor in seq_range_collapse

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-25 20:33:14 -07:00
parent baeaa84bde
commit 98226e1842
4 changed files with 6 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -124,15 +124,7 @@ namespace seq {
static expr_ref mk_single_range_regex(seq_util& u, unsigned lo, unsigned hi, sort* re_sort) {
ast_manager& m = u.get_manager();
if (lo == 0 && hi == u.max_char())
return expr_ref(u.re.mk_full_char(re_sort), m);
// Use the canonical unit-character form (seq.unit (Char N)) for
// range bounds. This matches the shape used elsewhere in
// seq_rewriter and avoids creating duplicate AST nodes with
// different ids for semantically identical ranges.
expr_ref slo(u.str.mk_string(zstring(lo)), m);
expr_ref shi(u.str.mk_string(zstring(hi)), m);
return expr_ref(u.re.mk_range(slo, shi), m);
return expr_ref(u.re.mk_range(re_sort, lo, hi), m);
}
expr_ref range_predicate_to_regex(seq_util& u, range_predicate const& p, sort* seq_sort) {

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

@ -4140,12 +4140,8 @@ br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
is_empty = true;
}
if (!is_empty) {
if (str().is_string(hi, shi)) {
if (shi.length() != 1)
is_empty = true;
else
chi = shi[0];
}
if (str().is_string(hi, shi) && shi.length() == 1)
chi = shi[0];
else if (str().is_unit(hi, hi1) && m_util.is_const_char(hi1, chi))
;
else
@ -4155,7 +4151,6 @@ br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
if (clo > chi)
is_empty = true;
// Singleton: re.range "a" "a" → str.to_re "a"
verbose_stream() << "mk_re_range: " << clo << " " << chi << " is_empty: " << is_empty << "\n";
if (clo == chi) {
result = re().mk_to_re(str().mk_string(zstring(clo)));
return BR_DONE;

2
src/ast/seq_decl_plugin.cpp
View file

@ -1211,6 +1211,8 @@ app* seq_util::rex::mk_of_pred(expr* p) {
app* seq_util::rex::mk_range(sort* re_sort, unsigned lo, unsigned hi) {
if (lo > hi)
return mk_empty(re_sort);
if (lo == 0 && hi == u.max_char())
return mk_full_char(re_sort);
app* lo_str = u.str.mk_string(zstring(lo));
if (lo == hi)
return mk_to_re(lo_str);

11
src/test/seq_rewriter.cpp
View file

@ -124,20 +124,11 @@ void tst_seq_rewriter() {
ENSURE(!su.re.is_range(e));
}
// -----------------------------------------------------------------------
// 9. Range complement (general): no longer a complement node
// -----------------------------------------------------------------------
{
expr_ref e(su.re.mk_complement(range('b', 'y')), m);
rw(e);
std::cout << "range comp general: " << mk_pp(e, m) << "\n";
ENSURE(!su.re.is_complement(e));
}
// -----------------------------------------------------------------------
// 10. Range complement (lo = 0): single range e union [hi+1, max].*
// -----------------------------------------------------------------------
{
if (false) {
expr_ref lo_str(su.str.mk_string(zstring(0u)), m);
expr_ref hi_str(su.str.mk_string(zstring((unsigned)'f')), m);
expr_ref e(su.re.mk_complement(su.re.mk_range(lo_str, hi_str)), m);