From cdcdf263f17750a550776752e6f8371dcd4348d0 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 16 Mar 2026 19:05:35 +0000 Subject: [PATCH] replace dep_tracker uint_set with scoped_dependency_manager Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/smt/seq/seq_nielsen.cpp | 29 ++++++++++++------------- src/smt/seq/seq_nielsen.h | 42 +++++++++++++++++++++++++++++-------- src/smt/theory_nseq.cpp | 16 +++++++------- 3 files changed, 56 insertions(+), 31 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index a747debf4..5d1d8e7cd 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -229,7 +229,7 @@ namespace seq { 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 |= s.m_dep; + 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) { @@ -237,7 +237,7 @@ namespace seq { 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 |= s.m_dep; + 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); @@ -548,8 +548,7 @@ namespace seq { void nielsen_graph::add_str_eq(euf::snode* lhs, euf::snode* rhs) { if (!m_root) m_root = mk_node(); - dep_tracker dep; - dep.insert(m_root->str_eqs().size()); + dep_tracker dep = m_dep_mgr.mk_leaf({dep_source::kind::eq, m_num_input_eqs}); str_eq eq(lhs, rhs, dep); eq.sort(); m_root->add_str_eq(eq); @@ -559,8 +558,7 @@ namespace seq { void nielsen_graph::add_str_mem(euf::snode* str, euf::snode* regex) { if (!m_root) m_root = mk_node(); - dep_tracker dep; - dep.insert(m_root->str_eqs().size() + m_root->str_mems().size()); + dep_tracker dep = m_dep_mgr.mk_leaf({dep_source::kind::mem, m_num_input_mems}); euf::snode* history = m_sg.mk_empty_seq(str->get_sort()); unsigned id = next_mem_id(); m_root->add_str_mem(str_mem(str, regex, history, id, dep)); @@ -597,6 +595,7 @@ namespace seq { m_mod_cnt.reset(); m_len_var_cache.clear(); m_len_vars.reset(); + m_dep_mgr.reset(); } std::ostream& nielsen_graph::display(std::ostream& out) const { @@ -3141,7 +3140,7 @@ namespace seq { // constant, ConstNumUnwinding (priority 4) handles it with both // n=0 and n≥1 branches. euf::snode* power = nullptr; - dep_tracker dep; + dep_tracker dep = m_dep_mgr.mk_empty(); for (str_eq const& eq : node->str_eqs()) { if (eq.is_trivial()) continue; if (!eq.m_lhs || !eq.m_rhs) continue; @@ -3924,21 +3923,23 @@ namespace seq { if (!n->is_currently_conflict()) continue; for (str_eq const& eq : n->str_eqs()) - deps |= eq.m_dep; + deps = m_dep_mgr.mk_join(deps, eq.m_dep); for (str_mem const& mem : n->str_mems()) - deps |= mem.m_dep; + deps = m_dep_mgr.mk_join(deps, mem.m_dep); } } void nielsen_graph::explain_conflict(unsigned_vector& eq_indices, unsigned_vector& mem_indices) const { SASSERT(m_root); - dep_tracker deps; + dep_tracker deps = m_dep_mgr.mk_empty(); collect_conflict_deps(deps); - for (unsigned b : deps) { - if (b < m_num_input_eqs) - eq_indices.push_back(b); + vector vs; + m_dep_mgr.linearize(deps, vs); + for (dep_source const& d : vs) { + if (d.m_kind == dep_source::kind::eq) + eq_indices.push_back(d.index); else - mem_indices.push_back(b - m_num_input_eqs); + mem_indices.push_back(d.index); } } diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 12092e772..2174a6ea3 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -98,8 +98,9 @@ Abstract: ------------------------------------ 1. dep_tracker (DependencyTracker): ZIPT's DependencyTracker is a .NET class using a BitArray-like structure for tracking constraint origins. - Z3 uses uint_set (a dense bitvector from util/uint_set.h) for the same - purpose. The |=/subset_of/empty semantics are equivalent. + Z3 uses scoped_dependency_manager (an arena-based binary + join tree from util/dependency.h) where each leaf carries a dep_source + value identifying the originating eq or mem constraint by kind and index. 2. Substitution application (nielsen_node::apply_subst): ZIPT uses an immutable, functional style -- Apply() returns a new constraint if @@ -234,6 +235,7 @@ Author: #include "util/vector.h" #include "util/uint_set.h" +#include "util/dependency.h" #include "util/map.h" #include "util/lbool.h" #include "ast/ast.h" @@ -300,10 +302,25 @@ namespace seq { children_failed, }; - // dependency tracker: bitvector tracking which input constraints - // contributed to deriving a given constraint - // mirrors ZIPT's DependencyTracker - using dep_tracker = uint_set; + // source of a dependency: identifies an input constraint by kind and index. + // kind::eq means a string equality, kind::mem means a regex membership. + // index is the 0-based position in the input eq or mem list respectively. + struct dep_source { + enum class kind { eq, mem } m_kind; + unsigned index; + bool operator==(dep_source const& o) const { + return m_kind == o.m_kind && index == o.index; + } + }; + + // Arena-based dependency manager: builds an immutable tree of dep_source + // leaves joined by binary join nodes. Memory is managed via a region; + // call dep_manager::reset() to release all allocations at once. + using dep_manager = scoped_dependency_manager; + + // dep_tracker is a pointer into the dep_manager's arena. + // nullptr represents the empty dependency set. + using dep_tracker = dep_manager::dependency*; // ----------------------------------------------- // character-level substitution @@ -786,6 +803,10 @@ namespace seq { // Pins the fresh length variable expressions so they aren't garbage collected. expr_ref_vector m_len_vars; + // Arena for dep_tracker nodes. Declared mutable so that const methods + // (e.g., explain_conflict) can call mk_join / linearize. + mutable dep_manager m_dep_mgr; + public: // Construct with a caller-supplied solver. Ownership is NOT transferred; // the caller is responsible for keeping the solver alive. @@ -798,6 +819,9 @@ namespace seq { seq_util& seq() { return m_seq; } seq_util const& seq() const { return m_seq; } + dep_manager& dep_mgr() { return m_dep_mgr; } + dep_manager const& dep_mgr() const { return m_dep_mgr; } + // node management nielsen_node* mk_node(); nielsen_node* mk_child(nielsen_node* parent); @@ -838,7 +862,7 @@ namespace seq { // generate next unique regex membership id unsigned next_mem_id() { return m_next_mem_id++; } - // number of input constraints (for dep_tracker bit mapping) + // number of input constraints (used for indexing dep_source leaves) unsigned num_input_eqs() const { return m_num_input_eqs; } unsigned num_input_mems() const { return m_num_input_mems; } @@ -868,8 +892,8 @@ namespace seq { // collect dependency information from conflicting constraints void collect_conflict_deps(dep_tracker& deps) const; - // explain a conflict: partition the set bits into str_eq indices - // (bits 0..num_eqs-1) and str_mem indices (bits num_eqs..num_eqs+num_mems-1). + // explain a conflict: partition the dep_source leaves into str_eq indices + // (kind::eq) and str_mem indices (kind::mem). // Must be called after solve() returns unsat. void explain_conflict(unsigned_vector& eq_indices, unsigned_vector& mem_indices) const; diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 8b64f811b..08a8cc3d0 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -457,17 +457,17 @@ namespace smt { // ----------------------------------------------------------------------- void theory_nseq::deps_to_lits(seq::dep_tracker const& deps, enode_pair_vector& eqs, literal_vector& lits) { - unsigned num_input_eqs = m_nielsen.num_input_eqs(); - for (unsigned b : deps) { - if (b < num_input_eqs) { - eq_source const& src = m_state.get_eq_source(b); + vector vs; + m_nielsen.dep_mgr().linearize(deps, vs); + for (seq::dep_source const& d : vs) { + if (d.m_kind == seq::dep_source::kind::eq) { + eq_source const& src = m_state.get_eq_source(d.index); if (src.m_n1->get_root() == src.m_n2->get_root()) eqs.push_back({src.m_n1, src.m_n2}); } else { - unsigned mem_idx = b - num_input_eqs; - if (mem_idx < m_nielsen_to_state_mem.size()) { - unsigned state_mem_idx = m_nielsen_to_state_mem[mem_idx]; + if (d.index < m_nielsen_to_state_mem.size()) { + unsigned state_mem_idx = m_nielsen_to_state_mem[d.index]; mem_source const& src = m_state.get_mem_source(state_mem_idx); SASSERT(ctx.get_assignment(src.m_lit) == l_true); lits.push_back(src.m_lit); @@ -485,7 +485,7 @@ namespace smt { } void theory_nseq::explain_nielsen_conflict() { - seq::dep_tracker deps; + seq::dep_tracker deps = m_nielsen.dep_mgr().mk_empty(); m_nielsen.collect_conflict_deps(deps); add_conflict_clause(deps); }