mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-07 22:42:20 +00:00
Code Activity

Track maximum regex lengths

Browse source 
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 2bcccba7-ac7d-476e-8dfe-718a21d37554
This commit is contained in:
Nikolaj Bjorner 2026-08-05 12:15:55 -07:00
parent 249778137d
commit a6ca7d53d4
6 changed files with 78 additions and 64 deletions
Download patch file Download diff file Expand all files Collapse all files

91
src/ast/seq_decl_plugin.cpp
View file

@ -826,18 +826,6 @@ app* seq_util::mk_char_bit(expr* e, unsigned i) {
return m.mk_app(f, 1, &e);
}
unsigned seq_util::max_plus(unsigned x, unsigned y) const {
if (x + y < x || x + y < y)
return UINT_MAX;
return x + y;
}
unsigned seq_util::max_mul(unsigned x, unsigned y) const {
uint64_t r = ((uint64_t)x)*((uint64_t)y);
return (r > UINT_MAX) ? UINT_MAX : (unsigned)r;
}
bool seq_util::is_const_char(expr* e, unsigned& c) const {
return ch.is_const_char(e, c);
}
@ -1076,12 +1064,12 @@ unsigned seq_util::str::max_length(expr* s) const {
};
while (is_concat(s, s1, s2)) {
if (is_concat(s1))
result = u.max_plus(max_length(s1), result);
result = add_truncate(max_length(s1), result);
else
result = u.max_plus(get_length(s1), result);
result = add_truncate(get_length(s1), result);
s = s2;
}
result = u.max_plus(get_length(s), result);
result = add_truncate(get_length(s), result);
return result;
}
@ -1092,26 +1080,7 @@ unsigned seq_util::rex::min_length(expr* r) const {
unsigned seq_util::rex::max_length(expr* r) const {
SASSERT(u.is_re(r));
expr* r1 = nullptr, *r2 = nullptr, *s = nullptr;
unsigned lo = 0, hi = 0;
if (is_empty(r))
return 0;
if (is_concat(r, r1, r2))
return u.max_plus(max_length(r1), max_length(r2));
if (is_union(r, r1, r2) || m.is_ite(r, s, r1, r2))
return std::max(max_length(r1), max_length(r2));
if (is_intersection(r, r1, r2))
return std::min(max_length(r1), max_length(r2));
if (is_diff(r, r1, r2) || is_reverse(r, r1) || is_opt(r, r1))
return max_length(r1);
if (is_loop(r, r1, lo, hi))
return u.max_mul(hi, max_length(r1));
if (is_to_re(r, s))
return u.str.max_length(s);
if (is_range(r) || is_of_pred(r) || is_full_char(r))
return 1;
// Else: star, plus, complement, full_seq, loop(r,r1,lo), derivative
return UINT_MAX;
return get_info(r).max_length;
}
/**
@ -1671,9 +1640,9 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const {
if (e->get_family_id() == u.get_family_id()) {
switch (e->get_decl()->get_decl_kind()) {
case OP_RE_EMPTY_SET:
return info(true, l_false, UINT_MAX, false);
return info(true, l_false, UINT_MAX, 0, false);
case OP_RE_FULL_SEQ_SET:
return info(true, l_true, 0, true);
return info(true, l_true, 0, UINT_MAX, true);
case OP_RE_STAR:
i1 = get_info_rec(e->get_arg(0));
return i1.star();
@ -1686,14 +1655,14 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const {
if (u.str.is_string(e->get_arg(0), slo) && slo.length() == 1 &&
u.str.is_string(e->get_arg(1), shi) && shi.length() == 1 &&
slo[0] <= shi[0])
return info(true, l_false, 1, true);
return info(true, l_false, 1, 1, true);
// Symbolic or unknown: not classical
return info(true, l_false, 1, false);
return info(true, l_false, 1, 1, false);
}
case OP_RE_FULL_CHAR_SET:
case OP_RE_OF_PRED:
//TBD: check if the character predicate contains uninterpreted symbols or is nonground or is unsat
return info(true, l_false, 1, false);
return info(true, l_false, 1, 1, false);
case OP_RE_CONCAT:
if (e->get_num_args() == 1)
return get_info_rec(e->get_arg(0));
@ -1722,7 +1691,7 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const {
min_length = u.str.min_length(e->get_arg(0));
is_value = m.is_value(e->get_arg(0));
nullable = (is_value && min_length == 0 ? l_true : (min_length > 0 ? l_false : l_undef));
return info(is_value, nullable, min_length, true);
return info(is_value, nullable, min_length, u.str.max_length(e->get_arg(0)), true);
case OP_RE_REVERSE:
return get_info_rec(e->get_arg(0));
case OP_RE_PLUS:
@ -1788,6 +1757,7 @@ std::ostream& seq_util::rex::info::display(std::ostream& out) const {
out << "info("
<< "nullable=" << (nullable == l_true ? "T" : (nullable == l_false ? "F" : "U")) << ", "
<< "min_length=" << min_length << ", "
<< "max_length=" << max_length << ", "
<< "classical=" << (classical ? "T" : "F") << ")";
}
else if (is_valid())
@ -1808,13 +1778,13 @@ std::string seq_util::rex::info::str() const {
seq_util::rex::info seq_util::rex::info::star() const {
//if is_known() is false then all mentioned properties will remain false
return seq_util::rex::info(interpreted, l_true, 0, classical);
return seq_util::rex::info(interpreted, l_true, 0, max_length == 0 ? 0 : UINT_MAX, classical);
}
seq_util::rex::info seq_util::rex::info::plus() const {
if (is_known()) {
//plus never occurs in a normalized regex
return info(interpreted, nullable, min_length, classical);
return info(interpreted, nullable, min_length, max_length == 0 ? 0 : UINT_MAX, classical);
}
else
return *this;
@ -1823,14 +1793,14 @@ seq_util::rex::info seq_util::rex::info::plus() const {
seq_util::rex::info seq_util::rex::info::opt() const {
// if is_known() is false then all mentioned properties will remain false
// optional construct never occurs in a normalized regex
return seq_util::rex::info(interpreted, l_true, 0, classical);
return seq_util::rex::info(interpreted, l_true, 0, max_length, classical);
}
seq_util::rex::info seq_util::rex::info::complement() const {
if (is_known()) {
lbool compl_nullable = (nullable == l_true ? l_false : (nullable == l_false ? l_true : l_undef));
unsigned compl_min_length = (compl_nullable == l_false ? 1 : 0);
return info(interpreted, compl_nullable, compl_min_length, false);
return info(interpreted, compl_nullable, compl_min_length, UINT_MAX, false);
}
else
return *this;
@ -1839,12 +1809,15 @@ seq_util::rex::info seq_util::rex::info::complement() const {
seq_util::rex::info seq_util::rex::info::concat(seq_util::rex::info const& rhs, bool lhs_is_concat) const {
if (is_known()) {
if (rhs.is_known()) {
unsigned m = min_length + rhs.min_length;
if (m < min_length || m < rhs.min_length)
m = UINT_MAX;
lbool is_nullable = l_undef;
if (nullable == l_true && rhs.nullable == l_true)
is_nullable = l_true;
if (nullable == l_false || rhs.nullable == l_false)
is_nullable = l_false;
return info(interpreted && rhs.interpreted,
((nullable == l_false || rhs.nullable == l_false) ? l_false : ((nullable == l_true && rhs.nullable == l_true) ? l_true : l_undef)),
m,
is_nullable,
add_truncate(min_length, rhs.min_length),
add_truncate(max_length, rhs.max_length),
classical && rhs.classical);
}
else
@ -1860,6 +1833,7 @@ seq_util::rex::info seq_util::rex::info::disj(seq_util::rex::info const& rhs) co
return info(interpreted && rhs.interpreted,
((nullable == l_true || rhs.nullable == l_true) ? l_true : ((nullable == l_false && rhs.nullable == l_false) ? l_false : l_undef)),
std::min(min_length, rhs.min_length),
std::max(max_length, rhs.max_length),
classical && rhs.classical);
}
else
@ -1872,6 +1846,7 @@ seq_util::rex::info seq_util::rex::info::conj(seq_util::rex::info const& rhs) co
return info(interpreted && rhs.interpreted,
((nullable == l_true && rhs.nullable == l_true) ? l_true : ((nullable == l_false || rhs.nullable == l_false) ? l_false : l_undef)),
std::max(min_length, rhs.min_length),
std::min(max_length, rhs.max_length),
false);
}
else
@ -1886,7 +1861,8 @@ seq_util::rex::info seq_util::rex::info::diff(seq_util::rex::info const& rhs) co
if (rhs.is_known()) {
return info(interpreted & rhs.interpreted,
((nullable == l_true && rhs.nullable == l_false) ? l_true : ((nullable == l_false || rhs.nullable == l_false) ? l_false : l_undef)),
std::max(min_length, rhs.min_length),
min_length,
max_length,
false);
}
else
@ -1906,6 +1882,7 @@ seq_util::rex::info seq_util::rex::info::xor_(seq_util::rex::info const& rhs) co
return info(interpreted & rhs.interpreted,
xor_nullable,
0,
UINT_MAX,
false);
}
else
@ -1924,6 +1901,7 @@ seq_util::rex::info seq_util::rex::info::orelse(seq_util::rex::info const& i) co
return info(false,
((nullable == l_true && i.nullable == l_true) ? l_true : ((nullable == l_false && i.nullable == l_false) ? l_false : l_undef)),
std::min(min_length, i.min_length),
std::max(max_length, i.max_length),
classical && i.classical);
}
else
@ -1935,12 +1913,10 @@ seq_util::rex::info seq_util::rex::info::orelse(seq_util::rex::info const& i) co
seq_util::rex::info seq_util::rex::info::loop(unsigned lower, unsigned upper) const {
if (is_known()) {
unsigned m = min_length * lower;
// Code review: this is not a complete overflow check.
if (m > 0 && (m < min_length || m < lower))
m = UINT_MAX;
unsigned m = mul_truncate(min_length, lower);
unsigned max_l = mul_truncate(max_length, upper);
lbool loop_nullable = (nullable == l_true || lower == 0 ? l_true : nullable);
return info(interpreted, loop_nullable, m, classical);
return info(interpreted, loop_nullable, m, max_l, classical);
}
else
return *this;
@ -1955,8 +1931,7 @@ seq_util::rex::info& seq_util::rex::info::operator=(info const& other) {
interpreted = other.interpreted;
nullable = other.nullable;
min_length = other.min_length;
max_length = other.max_length;
classical = other.classical;
return *this;
}

8
src/ast/seq_decl_plugin.h
View file

@ -225,9 +225,6 @@ class seq_util {
public:
unsigned max_plus(unsigned x, unsigned y) const;
unsigned max_mul(unsigned x, unsigned y) const;
ast_manager& get_manager() const { return m; }
char_decl_plugin &get_char_plugin() const {
return ch;
@ -451,6 +448,8 @@ public:
lbool nullable { l_undef };
/* Lower bound on the length of all accepted words. */
unsigned min_length { 0 };
/* Upper bound on the length of all accepted words, or UINT_MAX if unknown. */
unsigned max_length { UINT_MAX };
/* Classical regular expression: does not use complement, intersection, diff, or the empty language (fail). */
bool classical { true };
@ -471,11 +470,13 @@ public:
info(bool is_interpreted,
lbool is_nullable,
unsigned min_l,
unsigned max_l,
bool is_classical) :
known(l_true),
interpreted(is_interpreted),
nullable(is_nullable),
min_length(min_l),
max_length(max_l),
classical(is_classical) {}
/*
@ -664,4 +665,3 @@ public:
inline std::ostream& operator<<(std::ostream& out, seq_util::rex::pp const & p) { return p.display(out); }
inline std::ostream& operator<<(std::ostream& out, seq_util::rex::info const& p) { return p.display(out); }

2
src/smt/seq_regex.cpp
View file

@ -493,7 +493,7 @@ namespace smt {
// Rule 1: use min_length to prune search
unsigned min_len = re().min_length(r);
unsigned min_len_plus_i = u().max_plus(min_len, idx);
unsigned min_len_plus_i = add_truncate(min_len, idx);
literal len_s_ge_min = th.m_ax.mk_ge(th.mk_len(s), min_len_plus_i);
// Acc(s,i,r) ==> |s| >= i + minlength(r)
th.propagate_lit(nullptr, 1, &lit, len_s_ge_min);

28
src/test/seq_rewriter.cpp
View file

@ -18,6 +18,7 @@ Tests:
20. Solver: contradictory constant lexical bounds are unsatisfiable
22. re.loop with bounds as arguments agrees with the indexed form
23. (Σ*·S)* is flattened to () | Σ*·S
24. Regex info tracks inferred maximal lengths
--*/
#include "ast/arith_decl_plugin.h"
@ -349,5 +350,32 @@ void tst_seq_rewriter() {
ENSURE(i2.nullable == l_false && i2.min_length == 2);
}
// -----------------------------------------------------------------------
// 24. Regex info tracks inferred maximal lengths.
// -----------------------------------------------------------------------
{
expr_ref empty(su.re.mk_empty(re_sort), m);
expr_ref epsilon(su.re.mk_to_re(su.str.mk_empty(str_sort)), m);
expr_ref ab(su.re.mk_to_re(su.str.mk_string("ab")), m);
expr_ref abc(su.re.mk_to_re(su.str.mk_string("abc")), m);
expr_ref intersection(su.re.mk_inter(ab, abc), m);
expr_ref union_(su.re.mk_union(ab, abc), m);
expr_ref complement(su.re.mk_complement(ab), m);
expr_ref loop(su.re.mk_loop_proper(abc, 2, 4), m);
ENSURE(su.re.get_info(empty).max_length == 0);
ENSURE(su.re.get_info(epsilon).max_length == 0);
ENSURE(su.re.get_info(intersection).max_length == 2);
ENSURE(su.re.get_info(union_).max_length == 3);
ENSURE(su.re.get_info(complement).max_length == UINT_MAX);
ENSURE(su.re.get_info(loop).max_length == 12);
seq_util::rex::info large(true, l_false, 1, UINT_MAX / 2 + 1, true);
ENSURE(large.loop(1, 2).max_length == UINT_MAX);
seq_util::rex::info almost_max(true, l_false, 1, UINT_MAX - 1, true);
seq_util::rex::info two(true, l_false, 1, 2, true);
ENSURE(almost_max.concat(two, false).max_length == UINT_MAX);
}
std::cout << "tst_seq_rewriter: all tests passed\n";
}

11
src/util/util.cpp
View file

@ -119,6 +119,16 @@ unsigned uint64_log2(uint64_t v) {
return r;
}
unsigned mul_truncate(unsigned a, unsigned b) {
auto r = (uint64_t)a * (uint64_t)b;
return r > UINT_MAX ? UINT_MAX : (unsigned)r;
}
unsigned add_truncate(unsigned a, unsigned b) {
auto r = (uint64_t)a + (uint64_t)b;
return r > UINT_MAX ? UINT_MAX : (unsigned)r;
}
bool product_iterator_next(unsigned n, unsigned const * sz, unsigned * it) {
for (unsigned i = 0; i < n; ++i) {
it[i]++;
@ -160,4 +170,3 @@ void escaped::display(std::ostream & out) const {
}
}
}

2
src/util/util.h
View file

@ -109,6 +109,8 @@ static inline unsigned next_power_of_two(unsigned v) {
*/
unsigned log2(unsigned v);
unsigned uint64_log2(uint64_t v);
unsigned mul_truncate(unsigned a, unsigned b);
unsigned add_truncate(unsigned a, unsigned b);
static_assert(sizeof(unsigned) == 4, "unsigned are 32 bits");