mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

Fix unsound collapse of symbolic re.range bounds in seq_rewriter

Browse source 
mk_re_range extracts a constant character from each bound and, when
extraction fails, marked the range empty (is_empty = true), collapsing
(re.range lo hi) to the empty regex. For a symbolic bound such as a
String variable `a` in (re.range a "u"), extraction fails even though
`a` may denote a single-character string at solving time. Collapsing to
re.empty is therefore unsound: it turns satisfiable membership
constraints into unsat.

Return BR_FAILED for non-constant bounds instead, leaving the range
node intact for the theory/derivative solver. The sound emptiness
checks for provably non-singleton bounds (min_length > 1, max_length
== 0) and the constant-bound ordering/singleton cases are preserved.

With this fix (simplify (re.range a "u")) yields (re.range a "u")
instead of re.none, and benchmarks that assert satisfiable string
membership over symbolic ranges are no longer reported unsat.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-07-01 03:27:48 -07:00 • committed by GitHub
parent 652402fa1f
commit 7598285dd4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 9 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -4126,13 +4126,20 @@ br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
is_empty = true;
if (max_length(hi) == std::make_pair(true, rational(0)))
is_empty = true;
// Extract constant character bounds. A bound that is neither a constant
// character nor a provably non-singleton string (the length checks above
// already handle the latter) may still denote a singleton string at
// solving time, e.g. a String variable such as `a` in (re.range a "u").
// In that case the range is symbolic and must be left for the theory
// solver: collapsing it to the empty regex here is unsound (it wrongly
// turns satisfiable membership constraints into unsat).
if (!is_empty) {
if (str().is_string(lo, slo) && slo.length() == 1)
clo = slo[0];
else if (str().is_unit(lo, lo1) && m_util.is_const_char(lo1, clo))
;
else
is_empty = true;
return BR_FAILED;
}
if (!is_empty) {
if (str().is_string(hi, shi) && shi.length() == 1)
@ -4140,7 +4147,7 @@ br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
else if (str().is_unit(hi, hi1) && m_util.is_const_char(hi1, chi))
;
else
is_empty = true;
return BR_FAILED;
}
// clo/chi are only meaningful once both bounds were extracted; an early