From 7d7199dec62c819fdc4a789176d09613ba78c562 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Thu, 28 May 2026 18:02:41 +0200 Subject: [PATCH] use expr id when doing model construction and not internal id --- src/smt/seq/seq_nielsen.h | 6 ++++++ src/smt/seq/seq_nielsen_pp.cpp | 14 +++++++++---- src/smt/seq_model.cpp | 37 ++++++++++++++++++---------------- src/smt/seq_model.h | 5 ----- 4 files changed, 36 insertions(+), 26 deletions(-) diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 8322ea69a..4294380d5 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -602,6 +602,12 @@ namespace seq { void add_side_constraint(constraint const& ic) { if (ic.fml.m().is_true(ic.fml)) return; + expr* a, * b; + if (ic.fml.m().is_and(ic.fml, a, b)) { + add_side_constraint(constraint(a, ic.dep, ic.fml.m())); + add_side_constraint(constraint(b, ic.dep, ic.fml.m())); + return; + } m_side_constraints.push_back(ic); } vector const& side_constraints() const { return m_side_constraints; } diff --git a/src/smt/seq/seq_nielsen_pp.cpp b/src/smt/seq/seq_nielsen_pp.cpp index 1b17aa918..808fc1fb2 100644 --- a/src/smt/seq/seq_nielsen_pp.cpp +++ b/src/smt/seq/seq_nielsen_pp.cpp @@ -168,7 +168,7 @@ namespace seq { return val.to_string(); if (!is_app(e)) { std::ostringstream os; - os << mk_pp(e, m); + os << mk_bounded_pp(e, m); return dot_html_escape(os.str()); } app* a = to_app(e); @@ -241,7 +241,9 @@ namespace seq { if (names.contains(x)) { return "|" + names[x] + "|"; } - std::string s = dot_html_escape(to_app(x)->get_decl()->get_name().str()) + std::to_string(next_id++); + std::stringstream ss; + ss << mk_bounded_pp(x, m); + std::string s = ss.str(); names.insert(x, s); return "|" + s + "|"; } @@ -254,7 +256,9 @@ namespace seq { return dot_html_escape(a->get_decl()->get_name().str()); if (names.contains(e)) return names[e]; - std::string s = dot_html_escape(to_app(e)->get_decl()->get_name().str()) + std::to_string(next_id++); + std::stringstream ss; + ss << mk_bounded_pp(e, m); + std::string s = dot_html_escape(ss.str()); names.insert(e, s); return s; @@ -462,7 +466,9 @@ namespace seq { else if (names.contains(e)) result += names[e]; else { - std::string s = dot_html_escape(to_app(e)->get_decl()->get_name().str()) + std::to_string(next_id++); + std::stringstream ss; + ss << mk_bounded_pp(e, m); + std::string s = dot_html_escape(ss.str()); names.insert(e, s); result += s; } diff --git a/src/smt/seq_model.cpp b/src/smt/seq_model.cpp index 5c93aedf7..371bb782a 100644 --- a/src/smt/seq_model.cpp +++ b/src/smt/seq_model.cpp @@ -79,6 +79,15 @@ namespace smt { } }; + // Stable key for a variable snode. The sgraph may hold several distinct + // snode objects for the same hash-consed expression (e.g. one created at + // internalization and one re-created during the Nielsen search), so snode + // ids are NOT a reliable key. Expressions are perfectly shared, so their + // id is stable across all snodes that denote the same term. + static unsigned var_key(euf::snode* n) { + return n->first()->get_expr()->get_id(); + } + seq_model::seq_model(ast_manager& m, context& ctx, seq_util& seq, seq_rewriter& rw, euf::sgraph& sg) : m(m), m_ctx(ctx), m_seq(seq), m_rewriter(rw), m_sg(sg), m_trail(m) @@ -95,7 +104,6 @@ namespace smt { m_factory = alloc(seq_factory, m, m_seq.get_family_id(), mg.get_model()); mg.register_factory(m_factory); - register_existing_values(nielsen); 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); @@ -112,6 +120,7 @@ namespace smt { model_value_proc* seq_model::mk_value(enode* n, model_generator& mg) { app* e = n->get_expr(); + if (!m_seq.is_seq(e) && !m_seq.is_re(e) && !m_seq.str.is_nth_u(e)) return nullptr; @@ -208,7 +217,10 @@ namespace smt { IF_VERBOSE(1, verbose_stream() << "nseq extract_assignments: " << bindings.size() << " bindings\n";); for (auto const &[var, replacement] : bindings) { SASSERT(var); - unsigned id = var->first()->id(); // TODO - first or just var->id()? + // Key by expression id, not snode id: the sgraph may hold two distinct + // snode objects for the same (hash-consed) expression, so snode ids are + // not a stable key across the substitution trees we traverse here. + unsigned id = var_key(var); SASSERT(!m_var_replacement.contains(id)); m_var_replacement.insert(id, replacement); } @@ -247,8 +259,8 @@ namespace smt { // when using the dependencies to build a value for n we should // map the values that are passed in to the sub-terms that are listed as dependencies. // sub-terms are under concat, power and unit - euf::snode *replacement = nullptr; - if (m_var_replacement.find(curr->id(), replacement)) + euf::snode *replacement = nullptr; + if (m_var_replacement.find(var_key(curr), replacement)) todo.push_back(replacement); } else { @@ -344,7 +356,7 @@ namespace smt { } else if (curr->is_var()) { euf::snode *replacement = nullptr; - if (m_var_replacement.find(curr->id(), replacement)) { + if (m_var_replacement.find(var_key(curr), replacement)) { // outer variable: its value is the value of its replacement. expr* rv = nullptr; if (!resolve(replacement, rv)) { @@ -374,23 +386,15 @@ namespace smt { return expr_ref(result, m); } - void seq_model::register_existing_values(seq::nielsen_graph& nielsen) { - seq::nielsen_node const* root = nielsen.root(); - if (!root) - return; - // TODO - need to traverse sub-expressions for values. - } - expr* seq_model::get_var_value(euf::snode* var) { SASSERT(var); - unsigned key = var->first()->id(); + const unsigned key = var_key(var); expr* val = nullptr; if (m_var_values.find(key, val)) return val; // unconstrained or regex-constrained: delegate to mk_fresh_value val = mk_fresh_value(var); - std::cout << "Fresh value for " << mk_pp(var->get_expr(), m) << " : " << mk_pp(val, m) << std::endl; SASSERT(val); m_trail.push_back(val); m_var_values.insert(key, val); @@ -437,7 +441,7 @@ namespace smt { // check if this variable has regex constraints euf::snode* re = nullptr; - unsigned key = var->first()->id(); + unsigned key = var_key(var); if (m_var_regex.find(key, re) && re) { expr* re_expr = re->get_expr(); SASSERT(re_expr); @@ -509,8 +513,7 @@ namespace smt { if (mem.is_trivial(sat_node)) continue; // empty string in nullable regex: already satisfied, no variable to constrain VERIFY(mem.is_primitive()); // everything else should have been eliminated already - euf::snode* first = mem.m_str->first(); - unsigned id = first->id(); + unsigned id = var_key(mem.m_str); euf::snode* existing = nullptr; if (m_var_regex.find(id, existing) && existing) { // intersect with existing constraint: diff --git a/src/smt/seq_model.h b/src/smt/seq_model.h index c2d5f8a64..2d2e75834 100644 --- a/src/smt/seq_model.h +++ b/src/smt/seq_model.h @@ -106,11 +106,6 @@ namespace smt { // Collect enode dependencies required to evaluate an snode value. void collect_dependencies(euf::snode* n, ptr_vector& deps) const; - - // register all string literals appearing in the constraint store - // with the factory to avoid collisions with fresh values. - void register_existing_values(seq::nielsen_graph& nielsen); - // look up or compute the value for an snode variable. // If no assignment exists, delegates to mk_fresh_value. expr* get_var_value(euf::snode* var);