From c9877081ad99a68985a7db3c3a124816c784e700 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Mon, 27 Jul 2026 16:13:30 +0200 Subject: [PATCH] Regex fix --- scripts/compare_seq_solvers.py | 4 +++- src/smt/seq/seq_nielsen.cpp | 18 ++++++++++++++++++ 2 files changed, 21 insertions(+), 1 deletion(-) diff --git a/scripts/compare_seq_solvers.py b/scripts/compare_seq_solvers.py index 3f547f49ab..4b305c64e2 100644 --- a/scripts/compare_seq_solvers.py +++ b/scripts/compare_seq_solvers.py @@ -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() \ No newline at end of file diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 53ecfe3b31..86c4ca7d38 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -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);