From c18aa647e15038e121ac9b2b3f9d99e2225378fc Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Fri, 22 May 2026 15:15:48 +0200 Subject: [PATCH] Removed recursion from regex unwinding --- src/smt/seq/seq_nielsen.cpp | 15 ++++----------- src/smt/seq/seq_nielsen.h | 4 ++-- src/smt/seq_model.cpp | 1 - src/smt/theory_nseq.cpp | 4 ---- 4 files changed, 6 insertions(+), 18 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index ef8552ce5..8fc3a839d 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -346,21 +346,11 @@ namespace seq { for (auto &mem : m_str_mem) { const auto new_str = sg.subst(mem.m_str, s.m_var, s.m_replacement); const auto new_regex = sg.subst(mem.m_regex, s.m_var, s.m_replacement); - std::cout << "Applying substitution " - << mk_pp(s.m_var->get_expr(), graph().m) << " / " - << mk_pp(s.m_replacement->get_expr(), graph().m) << " to " << - mk_pp(new_regex->get_expr(), graph().m) << std::endl; if (new_str != mem.m_str || new_regex != mem.m_regex) { mem.m_str = new_str; mem.m_regex = new_regex; mem.m_dep = m_graph.dep_mgr().mk_join(mem.m_dep, s.m_dep); } - if (new_regex != mem.m_regex) { - std::cout << "Got: " << mk_pp(new_regex->get_expr(), graph().get_manager()) << std::endl; - } - else { - std::cout << "No change!" << std::endl; - } } const unsigned var_id = s.m_var->id(); @@ -4023,9 +4013,12 @@ namespace seq { // euf::snode* fresh_char = m_sg.mk(get_or_create_char_var(first)); - euf::snode* replacement = m_sg.mk_concat(fresh_char, first); + + euf::snode* tail = get_tail(first, 1, true); + euf::snode* replacement = m_sg.mk_concat(fresh_char, tail); nielsen_node* child = mk_child(node); nielsen_edge* e = mk_edge(node, child, false); + const nielsen_subst s(first, replacement, mk_rewrite(a.mk_sub(compute_length_expr(first), a.mk_int(1))), mem.m_dep); e->add_subst(s); child->apply_subst(m_sg, s); diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index c0dc90ba0..7e0ff8fbe 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -464,12 +464,12 @@ namespace seq { struct nielsen_subst { euf::snode* m_var; euf::snode* m_replacement; - euf::snode *m_length = nullptr; // representation of length if this is a sequence variable, null otherwise. + // euf::snode *m_length = nullptr; // representation of length if this is a sequence variable, null otherwise. dep_tracker m_dep; nielsen_subst(): m_var(nullptr), m_replacement(nullptr), m_dep(nullptr) {} nielsen_subst(euf::snode* var, euf::snode* repl, euf::snode* length, dep_tracker const& dep): - m_var(var), m_replacement(repl), m_length(length), m_dep(dep) { + m_var(var), m_replacement(repl)/*, m_length(length)*/, m_dep(dep) { SASSERT(var != nullptr); SASSERT(repl != nullptr); // var may be s_var or s_power; sgraph::subst uses pointer identity matching diff --git a/src/smt/seq_model.cpp b/src/smt/seq_model.cpp index 42dd97afd..2b9ec3b09 100644 --- a/src/smt/seq_model.cpp +++ b/src/smt/seq_model.cpp @@ -211,7 +211,6 @@ namespace smt { unsigned id = var->first()->id(); // TODO - first or just var->id()? SASSERT(!m_var_replacement.contains(id)); m_var_replacement.insert(id, replacement); - std::cout << "Assignment: " << mk_pp(var->get_expr(), m) << ": " << mk_pp(replacement->get_expr(), m) << std::endl; } } diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 8aba2fe45..b9c8a5b56 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -461,12 +461,10 @@ namespace smt { if (!get_fparams().m_nseq_regex_factorization_threshold) return; - std::cout << "Trying " << seq::mem_pp(mem, m); // Boolean Closure Propagations expr* re_expr = mem.m_regex->get_expr(); if (m_seq.re.is_intersection(re_expr)) { - std::cout << "Propagating intersection " << seq::mem_pp(mem, m) << std::endl; for (expr* arg : *to_app(re_expr)) { expr_ref in_r(m_seq.re.mk_in_re(s_expr, arg), m); literal_vector lits; @@ -479,7 +477,6 @@ namespace smt { return; } if (m_seq.re.is_union(re_expr)) { - std::cout << "Propagating union " << seq::mem_pp(mem, m) << std::endl; literal_vector lits; lits.push_back(~mem.lit); for (expr* arg : *to_app(re_expr)) { @@ -496,7 +493,6 @@ namespace smt { zstring s; expr_ref arg(to_app(re_expr)->get_arg(0), m); if (m_seq.str.is_string(arg, s)) { - std::cout << "Propagating const matching " << seq::mem_pp(mem, m) << std::endl; literal_vector lits; lits.push_back(~mem.lit); lits.push_back(mk_literal(m.mk_eq(s_expr, arg)));