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 to empty language

Browse source 
mk_re_range collapsed a re.range to the empty language whenever either
bound was not a constant single character. For a symbolic bound such as
(re.range "a" (ite (= a "") "z" "")) this is unsound: the bound may
evaluate to a valid character, so the range is not empty. This caused
z3 to return unsat on a satisfiable benchmark (iss-5142/small.smt2).

Only decide the range here when both bounds are concrete characters
(applying the exact empty/singleton/range semantics). When either bound
is a non-constant term, return BR_FAILED and leave the range for the
theory solver / derivative engine, which already handles symbolic
bounds. Provably-empty constant bounds are still caught by the existing
min_length/max_length checks.

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

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

@ -4126,35 +4126,44 @@ 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;
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;
}
if (!is_empty) {
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
is_empty = true;
}
// clo/chi are only meaningful once both bounds were extracted; an early
// is_empty (from the length checks) leaves them at their default 0, so the
// is_empty return must come before the singleton/ordering checks below.
if (!is_empty && clo > chi)
is_empty = true;
// A bound whose length is provably not 1 forces the whole range to denote
// the empty language, regardless of the other endpoint.
if (is_empty) {
sort* srt = re().mk_re(lo->get_sort());
result = re().mk_empty(srt);
return BR_DONE;
}
// Resolve each bound to a concrete character. A bound that is not a
// constant single character (e.g. a symbolic term such as an ite) cannot
// be decided here: leave the range untouched for the theory solver rather
// than assuming it denotes the empty language. Collapsing a symbolic range
// to empty is unsound, since the bound may evaluate to a valid character.
bool lo_is_char = false, hi_is_char = false;
if (str().is_string(lo, slo) && slo.length() == 1) {
clo = slo[0];
lo_is_char = true;
}
else if (str().is_unit(lo, lo1) && m_util.is_const_char(lo1, clo))
lo_is_char = true;
if (str().is_string(hi, shi) && shi.length() == 1) {
chi = shi[0];
hi_is_char = true;
}
else if (str().is_unit(hi, hi1) && m_util.is_const_char(hi1, chi))
hi_is_char = true;
if (!lo_is_char || !hi_is_char)
return BR_FAILED;
// Both endpoints are concrete characters: apply the exact semantics.
if (clo > chi) {
sort* srt = re().mk_re(lo->get_sort());
result = re().mk_empty(srt);
return BR_DONE;
}
// Singleton: re.range "a" "a" → str.to_re "a"
if (clo == chi) {
result = re().mk_to_re(str().mk_string(zstring(clo)));