mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-14 09:45:36 +00:00
Code Activity

Regex fix

Browse source
This commit is contained in:
CEisenhofer 2026-07-27 16:13:30 +02:00
parent d1e1d6cb80
commit c9877081ad
2 changed files with 21 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
scripts/compare_seq_solvers.py
View file

@ -37,6 +37,8 @@ COMMON_ARGS = ["model_validate=true"]
# All three configurations are always run.
SOLVERS = {
"nseq": ["smt.string_solver=nseq", "smt.nseq.parikh=false", "smt.nseq.eager=false",
"smt.nseq.regex_factorization_threshold=0", "smt.nseq.regex_factorization_eager=false", "smt.nseq.regex_dynamic_decomposition=false"],
"nseq_md": ["smt.string_solver=nseq", "smt.nseq.parikh=false", "smt.nseq.eager=false",
"smt.nseq.regex_factorization_threshold=10000000", "smt.nseq.regex_factorization_eager=false", "smt.nseq.regex_dynamic_decomposition=false"],
"nseq_md2": ["smt.string_solver=nseq", "smt.nseq.parikh=false", "smt.nseq.eager=false",
@ -374,4 +376,4 @@ def main():
if __name__ == "__main__":
main()
main()

18
src/smt/seq/seq_nielsen.cpp
View file

@ -6172,6 +6172,11 @@ namespace seq {
for (str_mem const& mem : m_root->str_mems()) {
SASSERT(seq.is_re(mem.m_regex->get_expr()));
// Views never denote L(m_regex) — see generate_node_length_constraints.
// (The root only ever carries plain memberships; kept for safety.)
if (!mem.is_plain())
continue;
unsigned min_len = 0, max_len = UINT_MAX;
compute_regex_length_interval(mem.m_regex, min_len, max_len);
@ -6357,6 +6362,19 @@ namespace seq {
for (str_mem const& mem : node->str_mems()) {
SASSERT(m_seq.is_re(mem.m_regex->get_expr()));
// A land-state view s ∈_{Q_ν,{root}} state does NOT denote the
// plain language of `state`: it collects the words that *walk*
// from `state` to `root` inside Q_ν, which is neither a sub- nor a
// superset of L(state). Its plain min/max length interval is
// therefore unsound in BOTH directions — e.g. the stabilizer view
// (state == root) always admits ε even when L(state) has min
// length > 0, which would kill exactly the landing branch that
// absorbs a cycle lap (spurious UNSAT). The correct length
// abstraction for views is emitted on the pinning edge by
// add_view_length_constraints (compute_view_length_info).
if (!mem.is_plain())
continue;
unsigned min_len = 0, max_len = UINT_MAX;
compute_regex_length_interval(mem.m_regex, min_len, max_len);