mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-12 01:56:22 +00:00
Code Activity

Dangling length constraints could mess up model construction

Browse source
This commit is contained in:
CEisenhofer 2026-07-03 15:06:46 +02:00
parent 87df0b941b
commit 628302d423
1 changed files with 38 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

63
src/smt/seq_model.cpp
View file

@ -493,44 +493,57 @@ namespace smt {
// into the product search).
euf::snode const* re = nullptr;
if (!m_view_vars.contains(key) && m_var_regex.find(key, re) && re) {
expr* re_expr = re->get_expr();
SASSERT(re_expr);
expr* const re_base = re->get_expr(); // intersection of ALL the var's plain regexes
SASSERT(re_base);
expr_ref len_expr(m_seq.str.mk_length(var->get_expr()), m);
rational len_val;
bool has_len = get_arith_value(len_expr, len_val);
CTRACE(seq, !has_len, tout << "no value associated with " << mk_pp(len_expr, m) << "\n";);
// Find some word in `r`. some_string_in_re can fail (l_undef / l_false)
// on regexes it does not fully support (Boolean closure, complement,
// large length-intersected shapes); fall back to a derivative-automaton
// BFS that builds an accepting word directly.
auto find_word = [&](expr* r, expr_ref& witness) -> bool {
zstring str;
lbool wr = m_rewriter.some_string_in_re(r, str);
if (wr == l_true) { witness = m_seq.str.mk_string(str); return true; }
// do NOT overwrite `witness` from `str`, which some_string_in_re
// left untouched (still empty) on failure.
return derivative_witness(m_sg.mk(r), witness) == l_true;
};
expr_ref witness(m);
bool ok = false;
// First honour the arith-assigned length so the model stays
// length-consistent with the outer solver.
if (has_len && len_val.is_unsigned()) {
unsigned n = len_val.get_unsigned();
expr_ref loop(m_seq.re.mk_loop(m_seq.re.mk_full_char(re_expr->get_sort()), n, n), m);
re_expr = m_seq.re.mk_inter(re_expr, loop);
expr_ref loop(m_seq.re.mk_loop(m_seq.re.mk_full_char(re_base->get_sort()), n, n), m);
expr_ref re_len(m_seq.re.mk_inter(re_base, loop), m);
ok = find_word(re_len, witness);
}
zstring str;
expr_ref witness(m);
// We checked non-emptiness during Nielsen already
lbool wr = m_rewriter.some_string_in_re(re_expr, str);
if (wr == l_true) {
witness = m_seq.str.mk_string(str);
}
else {
// some_seq_in_re can fail (l_undef / l_false) on regexes it does
// not fully support — notably projection operators (re.proj),
// but also some plain Boolean-closure / large length-intersected
// shapes. Fall back to a derivative-automaton BFS that builds an
// accepting word of the requested length directly. It sets
// `witness` itself -- do NOT overwrite it from `str`, which
// some_string_in_re left untouched (i.e. still empty) on failure.
wr = derivative_witness(m_sg.mk(re_expr), witness);
}
if (wr == l_true) {
// The arith length is only loosely coupled to the (branch-specific,
// intersected) regex when the exact length set is not encoded (Parikh
// off, or a Boolean-closure shape whose interval bound is looser than
// its true length set). The outer solver can then commit an
// UNACHIEVABLE len(var) — no word of that length exists in the
// intersection — and the length-constrained search above fails. The
// benchmark's validity depends on the regex memberships, NOT on that
// (unconstrained) length, so retry ignoring the length: any word in the
// full intersection is a sound witness (its length becomes len(var)).
// Without this retry we fall through to the "n a's" filler below, which
// ignores the regex entirely and yields an INVALID model.
if (!ok)
ok = find_word(re_base, witness);
if (ok) {
m_trail.push_back(witness);
m_factory->register_value(witness);
return witness;
}
IF_VERBOSE(1, verbose_stream() << "witness extraction failed for " << mk_pp(var->get_expr(), m)
<< " : " << wr << " with len " << (has_len ? len_val.to_string() : "unknown") << "\n" << mk_pp(re_expr, m) << "\n");
<< " with len " << (has_len ? len_val.to_string() : "unknown") << "\n" << mk_pp(re_base, m) << "\n");
// Last resort: do not crash model construction. model_validate (if
// enabled) will flag an inconsistent witness; otherwise fall through
// to the length-respecting fallback below.