From 8f74296cf290ab8d2535762a40c14ee3dc2b9270 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Thu, 28 May 2026 16:29:33 +0200 Subject: [PATCH] Output substitutions in dot --- src/smt/seq/seq_nielsen_pp.cpp | 73 ++++++++++++++++++++++++++++++++++ src/smt/seq_model.cpp | 12 +++--- 2 files changed, 78 insertions(+), 7 deletions(-) diff --git a/src/smt/seq/seq_nielsen_pp.cpp b/src/smt/seq/seq_nielsen_pp.cpp index 937388cbe..1b17aa918 100644 --- a/src/smt/seq/seq_nielsen_pp.cpp +++ b/src/smt/seq/seq_nielsen_pp.cpp @@ -620,6 +620,70 @@ namespace seq { || r == backtrack_reason::smt; } + // Render the current substitution of the original (root) variables at `node`. + // Walks the parent-edge chain from the root down to `node`, composing the + // edge substitutions exactly the way seq_model::extract_assignments does, + // and prints each root variable together with its current value (the image + // of the variable after applying all substitutions on the root-to-node path). + // Only variables whose value actually changed are shown. Purely for display: + // the values are computed on demand and any snodes created during + // substitution are harmless (the sgraph is monotone within a scope). + static void render_current_subst(std::ostream& out, nielsen_node const* node, + nielsen_node const* root, + u_map const& parent_edge, + euf::sgraph& sg, + obj_map& names, uint64_t& next_id, + ast_manager& m) { + if (!root) + return; + + // collect the original variables present in the root node's constraints + ptr_vector vars; + uint_set seen; + auto add_vars = [&](euf::snode* s) { + if (!s) + return; + for (euf::snode* t : s->collect_tokens()) + if (t->is_var() && !seen.contains(t->id())) { + seen.insert(t->id()); + vars.push_back(t); + } + }; + for (auto const& eq : root->str_eqs()) { add_vars(eq.m_lhs); add_vars(eq.m_rhs); } + for (auto const& deq : root->str_deqs()) { add_vars(deq.m_lhs); add_vars(deq.m_rhs); } + for (auto const& mem : root->str_mems()) add_vars(mem.m_str); + if (vars.empty()) + return; + + // collect edges along the root-to-node path (path[0] is node's parent edge) + ptr_vector path; + uint_set visited; + for (nielsen_node const* cur = node; cur != root && !visited.contains(cur->id()); ) { + visited.insert(cur->id()); + nielsen_edge* pe = nullptr; + if (!parent_edge.find(cur->id(), pe)) + break; + path.push_back(pe); + cur = pe->src(); + } + + bool any = false; + for (euf::snode* var : vars) { + euf::snode* val = var; + // apply substitutions in root-to-node order (path is node-to-root) + for (unsigned i = path.size(); i-- > 0; ) + for (nielsen_subst const& s : path[i]->subst()) + val = sg.subst(val, s.m_var, s.m_replacement); + if (val == var) + continue; // unchanged: variable is still free at this node + if (!any) { out << "
Subst:
"; any = true; } + out << snode_label_html(var, names, next_id, m) + << " → " + << snode_label_html(val, names, next_id, m) + << "
"; + } + } + // gives a graphviz graph representation of the Nielsen graph, for debugging std::ostream& nielsen_graph::to_dot(std::ostream& out) const { @@ -636,11 +700,20 @@ namespace seq { uint64_t next_id = 0; out << "digraph G {\n"; + // map each node to an incoming edge so the root-to-node substitution + // path can be reconstructed (m_parent_edge is not maintained). + u_map parent_edge; + for (nielsen_node const* n : m_nodes) + for (nielsen_edge* e : n->outgoing()) + parent_edge.insert(e->tgt()->id(), e); + // --- nodes --- for (nielsen_node const* n : m_nodes) { out << " " << n->id() << " [label=<" << n->id() << ": "; n->to_html(out, names, next_id, m); + // append the current substitution of the root variables at this node + render_current_subst(out, n, m_root, parent_edge, m_sg, names, next_id, m); // append conflict reason if this is a direct conflict if (n->is_currently_conflict()) out << "
" << reason_to_str(n->reason()); diff --git a/src/smt/seq_model.cpp b/src/smt/seq_model.cpp index 2b9ec3b09..5c93aedf7 100644 --- a/src/smt/seq_model.cpp +++ b/src/smt/seq_model.cpp @@ -390,10 +390,10 @@ namespace smt { // unconstrained or regex-constrained: delegate to mk_fresh_value val = mk_fresh_value(var); - if (val) { - m_trail.push_back(val); - m_var_values.insert(key, val); - } + 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); return val; } @@ -432,8 +432,7 @@ namespace smt { expr* seq_model::mk_fresh_value(euf::snode* var) { SASSERT(var->get_expr()); - if (!m_seq.is_seq(var->get_expr())) - return nullptr; + SASSERT(m_seq.is_seq(var->get_expr())); auto srt = var->get_expr()->get_sort(); // check if this variable has regex constraints @@ -443,7 +442,6 @@ namespace smt { expr* re_expr = re->get_expr(); SASSERT(re_expr); - arith_util arith(m); 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);