From d8a6ea1321cd52b0d2f1f3c06f959b61b78539fb Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Wed, 18 Mar 2026 16:08:02 +0100 Subject: [PATCH] Fixed crasb if regex is reported SAT by pre-check --- src/smt/seq/seq_nielsen.h | 4 +++- src/smt/seq_model.cpp | 6 ++++-- src/smt/seq_model.h | 2 +- src/smt/theory_nseq.cpp | 19 +++++++++---------- 4 files changed, 17 insertions(+), 14 deletions(-) diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 9dce0ffec..d8b612e84 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -783,7 +783,7 @@ namespace seq { // Regex membership module: stabilizers, emptiness checks, language // inclusion, derivatives. Allocated in the constructor; owned by this graph. - seq::seq_regex* m_seq_regex = nullptr; + seq_regex* m_seq_regex = nullptr; // ----------------------------------------------- // Modification counter for substitution length tracking. @@ -835,6 +835,8 @@ namespace seq { nielsen_node* root() const { return m_root; } void set_root(nielsen_node* n) { m_root = n; } + void set_sat_node(nielsen_node* n) { m_sat_node = n; } + // satisfying leaf node (set by solve() when result is sat) nielsen_node* sat_node() const { return m_sat_node; } // path of edges from root to sat_node (set when sat_node is set) diff --git a/src/smt/seq_model.cpp b/src/smt/seq_model.cpp index e0204e8c2..8e54559b1 100644 --- a/src/smt/seq_model.cpp +++ b/src/smt/seq_model.cpp @@ -30,7 +30,7 @@ namespace smt { : m(m), m_seq(seq), m_rewriter(rw), m_sg(sg), m_trail(m) {} - void seq_model::init(model_generator& mg, seq::nielsen_graph& nielsen, seq_state const& state) { + void seq_model::init(model_generator& mg, seq::nielsen_graph& nielsen) { m_var_values.reset(); m_var_regex.reset(); m_trail.reset(); @@ -41,7 +41,9 @@ namespace smt { mg.register_factory(m_factory); register_existing_values(nielsen); - collect_var_regex_constraints(nielsen.sat_node()); + seq::nielsen_node* sat_node = nielsen.sat_node(); + SASSERT(sat_node); // in case we report sat, this has to point to a satisfied Nielsen node! + collect_var_regex_constraints(sat_node); // solve integer constraints from the sat_path FIRST so that // m_int_model is available when snode_to_value evaluates power exponents diff --git a/src/smt/seq_model.h b/src/smt/seq_model.h index 5702a70ff..f1676d45c 100644 --- a/src/smt/seq_model.h +++ b/src/smt/seq_model.h @@ -75,7 +75,7 @@ namespace smt { // Allocates seq_factory, registers it with mg, collects // existing string literals, and extracts variable assignments // from the satisfying Nielsen leaf node. - void init(model_generator& mg, seq::nielsen_graph& nielsen, seq_state const& state); + void init(model_generator& mg, seq::nielsen_graph& nielsen); // Phase 2: build a model_value_proc for the given enode. // Returns nullptr if the enode is not a sequence/string sort. diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 4730e8fe1..a339abd7b 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -390,11 +390,10 @@ namespace smt { m_nielsen.set_parikh_enabled(get_fparams().m_nseq_parikh); // Regex membership pre-check: before running DFS, check intersection - // emptiness for each variable's regex constraints. This handles + // emptiness for each variable's regex constraints. This handles // regex-only problems that the DFS cannot efficiently solve. if (get_fparams().m_nseq_regex_precheck) { - lbool precheck = check_regex_memberships_precheck(); - switch (precheck) { + switch (check_regex_memberships_precheck()) { case l_true: // conflict was asserted inside check_regex_memberships_precheck IF_VERBOSE(1, verbose_stream() << "nseq final_check: regex precheck UNSAT\n";); @@ -402,6 +401,7 @@ namespace smt { case l_false: // all regex constraints satisfiable, no word eqs/diseqs → SAT IF_VERBOSE(1, verbose_stream() << "nseq final_check: regex precheck SAT\n";); + m_nielsen.set_sat_node(m_nielsen.root()); return FC_DONE; default: break; @@ -482,7 +482,7 @@ namespace smt { // ----------------------------------------------------------------------- void theory_nseq::init_model(model_generator& mg) { - m_model.init(mg, m_nielsen, m_state); + m_model.init(mg, m_nielsen); } model_value_proc* theory_nseq::mk_value(enode* n, model_generator& mg) { @@ -797,18 +797,17 @@ namespace smt { // Group membership indices by variable snode id. // Only consider memberships whose string snode is a plain variable (s_var). u_map var_to_mems; - bool all_var_str = true; + bool all_primitive = true; for (unsigned i = 0; i < mems.size(); ++i) { auto const& mem = mems[i]; - if (!mem.m_str || !mem.m_regex) - continue; - if (mem.m_str->is_var()) { + SASSERT(mem.m_str && mem.m_regex); + if (mem.is_primitive()) { auto& vec = var_to_mems.insert_if_not_there(mem.m_str->id(), unsigned_vector()); vec.push_back(i); } else - all_var_str = false; + all_primitive = false; } if (var_to_mems.empty()) @@ -860,7 +859,7 @@ namespace smt { // All variables' regex intersections are non-empty. // If there are no word equations and no disequalities, variables are // independent and each can be assigned a witness string → SAT. - if (all_var_str && m_state.str_eqs().empty() && m_state.diseqs().empty() && !has_unhandled_preds()) { + if (all_primitive && m_state.str_eqs().empty() && m_state.diseqs().empty() && !has_unhandled_preds()) { TRACE(seq, tout << "nseq regex precheck: all intersections non-empty, " << "no word eqs/diseqs → SAT\n";); return l_false; // signals SAT (non-empty / satisfiable)