From a895548b9999ef07637077fc3aada4483be6380b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 19 Mar 2026 16:39:37 -0700 Subject: [PATCH] cleanup Signed-off-by: Nikolaj Bjorner --- src/ast/euf/euf_snode.h | 3 ++ src/smt/seq/seq_nielsen.cpp | 79 ++++++++++++++++++------------------- 2 files changed, 41 insertions(+), 41 deletions(-) diff --git a/src/ast/euf/euf_snode.h b/src/ast/euf/euf_snode.h index a67644168..8b79cd1a4 100644 --- a/src/ast/euf/euf_snode.h +++ b/src/ast/euf/euf_snode.h @@ -116,6 +116,9 @@ namespace euf { bool is_char() const { return m_kind == snode_kind::s_char; } bool is_var() const { return m_kind == snode_kind::s_var; } bool is_unit() const { return m_kind == snode_kind::s_unit; } + bool is_char_or_unit() const { + return m_kind == snode_kind::s_char || m_kind == snode_kind::s_unit; + } bool is_concat() const { return m_kind == snode_kind::s_concat; } bool is_power() const { return m_kind == snode_kind::s_power; } bool is_star() const { return m_kind == snode_kind::s_star; } diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 085a5567b..370927572 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -198,32 +198,26 @@ namespace seq { m_char_ranges.reset(); m_var_lb.reset(); m_var_ub.reset(); - for (auto const& eq : parent.m_str_eq) - m_str_eq.push_back(str_eq(eq.m_lhs, eq.m_rhs, eq.m_dep)); - for (auto const& mem : parent.m_str_mem) - m_str_mem.push_back(str_mem(mem.m_str, mem.m_regex, mem.m_history, mem.m_id, mem.m_dep)); - for (auto const& ic : parent.m_int_constraints) - m_int_constraints.push_back(ic); + m_str_eq.append(parent.m_str_eq); + m_str_mem.append(parent.m_str_mem); + m_int_constraints.append(parent.m_int_constraints); // clone character disequalities - for (auto const& kv : parent.m_char_diseqs) { - ptr_vector diseqs; - for (euf::snode* s : kv.m_value) { - diseqs.push_back(s); - } - m_char_diseqs.insert(kv.m_key, diseqs); - } + + for (auto const &[k,v] : parent.m_char_diseqs) + m_char_diseqs.insert(k, v); + // clone character ranges - for (auto const& kv : parent.m_char_ranges) { - m_char_ranges.insert(kv.m_key, kv.m_value.clone()); - } + for (auto const &[k, v] : parent.m_char_ranges) + m_char_ranges.insert(k, v.clone()); + // clone per-variable integer bounds - for (auto const& kv : parent.m_var_lb) { - m_var_lb.insert(kv.m_key, kv.m_value); - } - for (auto const& kv : parent.m_var_ub) { - m_var_ub.insert(kv.m_key, kv.m_value); - } + for (auto const &[k, v] : parent.m_var_lb) + m_var_lb.insert(k, v); + + for (auto const &[k, v] : parent.m_var_ub) + m_var_ub.insert(k, v); + // clone regex occurrence tracking m_regex_occurrence = parent.m_regex_occurrence; } @@ -239,23 +233,28 @@ namespace seq { return false; } - // NSB review: optimize sg.subst to apply join only if the substitution had an effect. void nielsen_node::apply_subst(euf::sgraph& sg, nielsen_subst const& s) { if (!s.m_var) return; - for (unsigned i = 0; i < m_str_eq.size(); ++i) { - str_eq& eq = m_str_eq[i]; - eq.m_lhs = sg.subst(eq.m_lhs, s.m_var, s.m_replacement); - eq.m_rhs = sg.subst(eq.m_rhs, s.m_var, s.m_replacement); - eq.m_dep = m_graph.dep_mgr().mk_join(eq.m_dep, s.m_dep); - eq.sort(); + for (auto &eq : m_str_eq) { + auto new_lhs = sg.subst(eq.m_lhs, s.m_var, s.m_replacement); + auto new_rhs = sg.subst(eq.m_rhs, s.m_var, s.m_replacement); + if (new_lhs != eq.m_lhs || new_rhs != eq.m_rhs) { + eq.m_lhs = new_lhs; + eq.m_rhs = new_rhs; + eq.m_dep = m_graph.dep_mgr().mk_join(eq.m_dep, s.m_dep); + eq.sort(); + } } - for (unsigned i = 0; i < m_str_mem.size(); ++i) { - str_mem& mem = m_str_mem[i]; - mem.m_str = sg.subst(mem.m_str, s.m_var, s.m_replacement); - // regex is typically ground, but apply subst for generality - mem.m_regex = sg.subst(mem.m_regex, s.m_var, s.m_replacement); - mem.m_dep = m_graph.dep_mgr().mk_join(mem.m_dep, s.m_dep); + + for (auto &mem : m_str_mem) { + auto new_str = sg.subst(mem.m_str, s.m_var, s.m_replacement); + auto new_regex = sg.subst(mem.m_regex, s.m_var, s.m_replacement); + 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); + } } // VarBoundWatcher: propagate bounds on s.m_var to variables in s.m_replacement watch_var_bounds(s); @@ -388,7 +387,7 @@ namespace seq { unsigned const_len = 0; euf::snode_vector var_tokens; for (euf::snode* t : tokens) { - if (t->is_char() || t->is_unit()) + if (t->is_char_or_unit()) ++const_len; else if (t->is_var()) var_tokens.push_back(t); @@ -479,14 +478,12 @@ namespace seq { if (!s.m_var) return; // replace occurrences of s.m_var with s.m_val in all string constraints - for (unsigned i = 0; i < m_str_eq.size(); ++i) { - str_eq& eq = m_str_eq[i]; + for (auto &eq : m_str_eq) { eq.m_lhs = sg.subst(eq.m_lhs, s.m_var, s.m_val); - eq.m_rhs = sg.subst(eq.m_rhs, s.m_var, s.m_val); + eq.m_rhs = sg.subst(eq.m_rhs, s.m_var, s.m_val); eq.sort(); } - for (unsigned i = 0; i < m_str_mem.size(); ++i) { - str_mem& mem = m_str_mem[i]; + for (auto &mem : m_str_mem) { mem.m_str = sg.subst(mem.m_str, s.m_var, s.m_val); mem.m_regex = sg.subst(mem.m_regex, s.m_var, s.m_val); }