From ef22ae8871c1a036600182f15f2c7ada81775bcc Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Mon, 16 Mar 2026 15:52:18 -0700
Subject: [PATCH] Replace dep_tracker uint_set with
 scoped_dependency_manager<dep_source> in seq_nielsen (#9014)

* Initial plan

* replace dep_tracker uint_set with scoped_dependency_manager<dep_source>

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* fix test build: update dep_tracker usages in test files and seq_state.h

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/smt/seq/seq_nielsen.cpp |  29 +++---
 src/smt/seq/seq_nielsen.h   |  52 +++++++---
 src/smt/seq/seq_state.h     |   4 +-
 src/smt/theory_nseq.cpp     |  16 ++--
 src/test/nseq_basic.cpp     |   2 +-
 src/test/seq_nielsen.cpp    | 186 +++++++++++++++++++-----------------
 src/test/seq_parikh.cpp     |  37 ++++---
 7 files changed, 184 insertions(+), 142 deletions(-)

diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 7de3e84c5..75391812f 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 {
@@ -3146,7 +3145,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;
@@ -3929,21 +3928,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<dep_source, false> 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..faabdfb72 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<dep_source> (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_source>;
+
+    // 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
@@ -337,7 +354,7 @@ namespace seq {
         euf::snode* m_rhs;
         dep_tracker m_dep;
 
-        str_eq(): m_lhs(nullptr), m_rhs(nullptr) {}
+        str_eq(): m_lhs(nullptr), m_rhs(nullptr), m_dep(nullptr) {}
         str_eq(euf::snode* lhs, euf::snode* rhs, dep_tracker const& dep):
             m_lhs(lhs), m_rhs(rhs), m_dep(dep) {}
 
@@ -364,7 +381,7 @@ namespace seq {
         unsigned    m_id;       // unique identifier
         dep_tracker m_dep;
 
-        str_mem(): m_str(nullptr), m_regex(nullptr), m_history(nullptr), m_id(UINT_MAX) {}
+        str_mem(): m_str(nullptr), m_regex(nullptr), m_history(nullptr), m_id(UINT_MAX), m_dep(nullptr) {}
         str_mem(euf::snode* str, euf::snode* regex, euf::snode* history, unsigned id, dep_tracker const& dep):
             m_str(str), m_regex(regex), m_history(history), m_id(id), m_dep(dep) {}
 
@@ -387,7 +404,7 @@ namespace seq {
         euf::snode* m_replacement;
         dep_tracker m_dep;
 
-        nielsen_subst(): m_var(nullptr), m_replacement(nullptr) {}
+        nielsen_subst(): m_var(nullptr), m_replacement(nullptr), m_dep(nullptr) {}
         nielsen_subst(euf::snode* var, euf::snode* repl, dep_tracker const& dep):
             m_var(var), m_replacement(repl), m_dep(dep) {
             SASSERT(var != nullptr);
@@ -417,7 +434,7 @@ namespace seq {
         dep_tracker m_dep;   // tracks which input constraints contributed
         length_kind m_kind;  // determines propagation strategy
 
-        length_constraint(ast_manager& m): m_expr(m), m_kind(length_kind::nonneg) {}
+        length_constraint(ast_manager& m): m_expr(m), m_dep(nullptr), m_kind(length_kind::nonneg) {}
         length_constraint(expr* e, dep_tracker const& dep, length_kind kind, ast_manager& m):
             m_expr(e, m), m_dep(dep), m_kind(kind) {}
     };
@@ -443,7 +460,7 @@ namespace seq {
         dep_tracker          m_dep;    // tracks which input constraints contributed
 
         int_constraint(ast_manager& m):
-            m_lhs(m), m_rhs(m), m_kind(int_constraint_kind::eq) {}
+            m_lhs(m), m_rhs(m), m_kind(int_constraint_kind::eq), m_dep(nullptr) {}
         int_constraint(expr* lhs, expr* rhs, int_constraint_kind kind, dep_tracker const& dep, ast_manager& m):
             m_lhs(lhs, m), m_rhs(rhs, m), m_kind(kind), m_dep(dep) {}
 
@@ -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/seq/seq_state.h b/src/smt/seq/seq_state.h
index 29ace6308..6069472f7 100644
--- a/src/smt/seq/seq_state.h
+++ b/src/smt/seq/seq_state.h
@@ -78,13 +78,13 @@ namespace smt {
         }
 
         void add_str_eq(euf::snode* lhs, euf::snode* rhs, enode* n1, enode* n2) {
-            seq::dep_tracker dep;
+            seq::dep_tracker dep = nullptr;
             m_str_eqs.push_back(seq::str_eq(lhs, rhs, dep));
             m_eq_sources.push_back({n1, n2});
         }
 
         void add_str_mem(euf::snode* str, euf::snode* regex, sat::literal lit) {
-            seq::dep_tracker dep;
+            seq::dep_tracker dep = nullptr;
             m_str_mems.push_back(seq::str_mem(str, regex, nullptr, m_next_mem_id++, dep));
             m_mem_sources.push_back({lit});
         }
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index d62565fce..7cc482cfe 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -453,17 +453,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<seq::dep_source, false> 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);
@@ -481,7 +481,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);
     }
diff --git a/src/test/nseq_basic.cpp b/src/test/nseq_basic.cpp
index 8474c1d27..23265e39f 100644
--- a/src/test/nseq_basic.cpp
+++ b/src/test/nseq_basic.cpp
@@ -126,7 +126,7 @@ static void test_nseq_node_satisfied() {
 
     // add a trivial equality
     euf::snode* empty = sg.mk_empty_seq(su.str.mk_string_sort());
-    seq::dep_tracker dep;
+    seq::dep_tracker dep = nullptr;
     seq::str_eq eq(empty, empty, dep);
     node->add_str_eq(eq);
     SASSERT(node->str_eqs().size() == 1);
diff --git a/src/test/seq_nielsen.cpp b/src/test/seq_nielsen.cpp
index 067f6fd61..4933b080d 100644
--- a/src/test/seq_nielsen.cpp
+++ b/src/test/seq_nielsen.cpp
@@ -34,37 +34,35 @@ public:
 
 };
 
-// test dep_tracker (uint_set) basic operations
+// test dep_tracker (dependency_manager<dep_source>) basic operations
 static void test_dep_tracker() {
     std::cout << "test_dep_tracker\n";
 
+    seq::dep_manager dm;
+
     // empty tracker
-    seq::dep_tracker d0;
-    SASSERT(d0.empty());
+    seq::dep_tracker d0 = dm.mk_empty();
+    SASSERT(d0 == nullptr);
 
-    // tracker with one bit set
-    seq::dep_tracker d1;
-    d1.insert(3);
-    SASSERT(!d1.empty());
+    // tracker with one leaf
+    seq::dep_tracker d1 = dm.mk_leaf({seq::dep_source::kind::eq, 3});
+    SASSERT(d1 != nullptr);
 
-    // tracker with another bit
-    seq::dep_tracker d2;
-    d2.insert(5);
-    SASSERT(!d2.empty());
+    // tracker with another leaf
+    seq::dep_tracker d2 = dm.mk_leaf({seq::dep_source::kind::mem, 5});
+    SASSERT(d2 != nullptr);
 
     // merge
-    seq::dep_tracker d3 = d1;
-    d3 |= d2;
-    SASSERT(!d3.empty());
-    SASSERT(d1.subset_of(d3));
-    SASSERT(d2.subset_of(d3));
-    SASSERT(!d2.subset_of(d1));
+    seq::dep_tracker d3 = dm.mk_join(d1, d2);
+    SASSERT(d3 != nullptr);
+    SASSERT(dm.contains(d3, {seq::dep_source::kind::eq, 3}));
+    SASSERT(dm.contains(d3, {seq::dep_source::kind::mem, 5}));
+    SASSERT(!dm.contains(d1, {seq::dep_source::kind::mem, 5}));
 
-    // equality
-    seq::dep_tracker d4;
-    d4.insert(3);
-    SASSERT(d1 == d4);
-    SASSERT(d1 != d2);
+    // another leaf with same value as d1
+    seq::dep_tracker d4 = dm.mk_leaf({seq::dep_source::kind::eq, 3});
+    SASSERT(dm.contains(d4, {seq::dep_source::kind::eq, 3}));
+    SASSERT(!dm.contains(d4, {seq::dep_source::kind::mem, 5}));
 }
 
 // test str_eq constraint creation and operations
@@ -81,11 +79,10 @@ static void test_str_eq() {
     euf::snode* a = sg.mk_char('A');
     euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort());
 
-    seq::dep_tracker dep; dep.insert(0);
+    seq::dep_tracker dep = nullptr;
 
     // basic equality
     seq::str_eq eq1(x, y, dep);
-    SASSERT(!eq1.is_trivial());
     SASSERT(eq1.contains_var(x));
     SASSERT(eq1.contains_var(y));
     SASSERT(!eq1.contains_var(a));
@@ -128,7 +125,7 @@ static void test_str_mem() {
     expr_ref star_fc(seq.re.mk_full_seq(str_sort), m);
     euf::snode* regex = sg.mk(star_fc);
 
-    seq::dep_tracker dep; dep.insert(1);
+    seq::dep_tracker dep = nullptr;
     seq::str_mem mem(x, regex, e, 0, dep);
 
     // x in regex is primitive (x is a single variable)
@@ -157,9 +154,7 @@ static void test_nielsen_subst() {
     euf::snode* a = sg.mk_char('A');
     euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort());
 
-    seq::dep_tracker dep;
-
-    // eliminating substitution: x -> A (x does not appear in A)
+    seq::dep_tracker dep = nullptr;
     seq::nielsen_subst s1(x, a, dep);
     SASSERT(s1.is_eliminating());
 
@@ -202,7 +197,7 @@ static void test_nielsen_node() {
     SASSERT(root->reason() == seq::backtrack_reason::unevaluated);
 
     // add constraints
-    seq::dep_tracker dep;
+    seq::dep_tracker dep = nullptr;
     root->add_str_eq(seq::str_eq(x, y, dep));
     root->add_str_eq(seq::str_eq(sg.mk_concat(x, a), sg.mk_concat(a, y), dep));
     SASSERT(root->str_eqs().size() == 2);
@@ -239,7 +234,7 @@ static void test_nielsen_edge() {
 
     // create parent and child nodes
     seq::nielsen_node* parent = ng.mk_node();
-    seq::dep_tracker dep;
+    seq::dep_tracker dep = nullptr;
     parent->add_str_eq(seq::str_eq(x, y, dep));
 
     seq::nielsen_node* child = ng.mk_child(parent);
@@ -317,7 +312,7 @@ static void test_nielsen_subst_apply() {
 
     // create node with constraint: concat(x, A) = concat(B, y)
     seq::nielsen_node* node = ng.mk_node();
-    seq::dep_tracker dep;
+    seq::dep_tracker dep = nullptr;
     euf::snode* xa = sg.mk_concat(x, a);
     euf::snode* by = sg.mk_concat(b, y);
     node->add_str_eq(seq::str_eq(xa, by, dep));
@@ -379,7 +374,7 @@ static void test_nielsen_expansion() {
     seq::nielsen_node* root = ng.root();
     SASSERT(root->str_eqs().size() == 1);
 
-    seq::dep_tracker dep;
+    seq::dep_tracker dep = nullptr;
 
     // branch 1: x -> eps (eliminating, progress)
     euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort());
@@ -1417,49 +1412,61 @@ static void test_solve_conflict_deps() {
     auto result = ng.solve();
     SASSERT(result == seq::nielsen_graph::search_result::unsat);
 
-    seq::dep_tracker deps;
+    seq::dep_tracker deps = ng.dep_mgr().mk_empty();
     ng.collect_conflict_deps(deps);
     // deps should be non-empty since there's a conflict
-    SASSERT(!deps.empty());
+    SASSERT(deps != nullptr);
 }
 
-// test dep_tracker (uint_set) iteration
+// test dep_tracker (dependency_manager<dep_source>) linearize
 static void test_dep_tracker_get_set_bits() {
     std::cout << "test_dep_tracker_get_set_bits\n";
 
-    // empty tracker has no bits
-    seq::dep_tracker d0;
-    unsigned_vector bits0;
-    for (unsigned b : d0) bits0.push_back(b);
+    seq::dep_manager dm;
+
+    // empty tracker has no leaves
+    seq::dep_tracker d0 = dm.mk_empty();
+    vector<seq::dep_source, false> bits0;
+    dm.linearize(d0, bits0);
     SASSERT(bits0.empty());
 
-    // single bit set at position 5
-    seq::dep_tracker d1;
-    d1.insert(5);
-    unsigned_vector bits1;
-    for (unsigned b : d1) bits1.push_back(b);
+    // single leaf at eq-index 5
+    seq::dep_tracker d1 = dm.mk_leaf({seq::dep_source::kind::eq, 5});
+    vector<seq::dep_source, false> bits1;
+    dm.linearize(d1, bits1);
     SASSERT(bits1.size() == 1);
-    SASSERT(bits1[0] == 5);
+    SASSERT(bits1[0].index == 5);
+    SASSERT(bits1[0].m_kind == seq::dep_source::kind::eq);
 
-    // two bits merged
-    seq::dep_tracker d2;
-    d2.insert(3);
-    d2.insert(11);
-    unsigned_vector bits2;
-    for (unsigned b : d2) bits2.push_back(b);
+    // two leaves merged: eq-index 3 and mem-index 11
+    seq::dep_tracker d2 = dm.mk_join(
+        dm.mk_leaf({seq::dep_source::kind::eq, 3}),
+        dm.mk_leaf({seq::dep_source::kind::mem, 11}));
+    vector<seq::dep_source, false> bits2;
+    dm.linearize(d2, bits2);
     SASSERT(bits2.size() == 2);
-    SASSERT(bits2[0] == 3);
-    SASSERT(bits2[1] == 11);
+    bool has_eq3 = false, has_mem11 = false;
+    for (auto const& d : bits2) {
+        if (d.m_kind == seq::dep_source::kind::eq && d.index == 3) has_eq3 = true;
+        if (d.m_kind == seq::dep_source::kind::mem && d.index == 11) has_mem11 = true;
+    }
+    SASSERT(has_eq3);
+    SASSERT(has_mem11);
 
-    // test across word boundary (bit 31 and 32)
-    seq::dep_tracker d3;
-    d3.insert(31);
-    d3.insert(32);
-    unsigned_vector bits3;
-    for (unsigned b : d3) bits3.push_back(b);
+    // join with additional leaf
+    seq::dep_tracker d3 = dm.mk_join(
+        dm.mk_leaf({seq::dep_source::kind::eq, 31}),
+        dm.mk_leaf({seq::dep_source::kind::mem, 32}));
+    vector<seq::dep_source, false> bits3;
+    dm.linearize(d3, bits3);
     SASSERT(bits3.size() == 2);
-    SASSERT(bits3[0] == 31);
-    SASSERT(bits3[1] == 32);
+    bool has31 = false, has32 = false;
+    for (auto const& d : bits3) {
+        if (d.index == 31) has31 = true;
+        if (d.index == 32) has32 = true;
+    }
+    SASSERT(has31);
+    SASSERT(has32);
 }
 
 // test explain_conflict returns correct constraint indices
@@ -1648,7 +1655,7 @@ static void test_simplify_prefix_cancel() {
     euf::snode* aby = sg.mk_concat(a, sg.mk_concat(b, y));
 
     seq::nielsen_node* node = ng.mk_node();
-    seq::dep_tracker dep; dep.insert(0);
+    seq::dep_tracker dep = nullptr;
     node->add_str_eq(seq::str_eq(abx, aby, dep));
 
     auto sr = node->simplify_and_init();
@@ -1678,7 +1685,7 @@ static void test_simplify_suffix_cancel_rtl() {
     euf::snode* ya = sg.mk_concat(y, a);
 
     seq::nielsen_node* node = ng.mk_node();
-    seq::dep_tracker dep; dep.insert(0);
+    seq::dep_tracker dep = nullptr;
     node->add_str_eq(seq::str_eq(xa, ya, dep));
 
     auto sr = node->simplify_and_init();
@@ -1707,7 +1714,7 @@ static void test_simplify_symbol_clash() {
     euf::snode* by = sg.mk_concat(b, y);
 
     seq::nielsen_node* node = ng.mk_node();
-    seq::dep_tracker dep; dep.insert(0);
+    seq::dep_tracker dep = nullptr;
     node->add_str_eq(seq::str_eq(ax, by, dep));
 
     auto sr = node->simplify_and_init();
@@ -1733,7 +1740,7 @@ static void test_simplify_empty_propagation() {
 
     // ε = x·y → forces x=ε, y=ε → all trivial → satisfied
     seq::nielsen_node* node = ng.mk_node();
-    seq::dep_tracker dep; dep.insert(0);
+    seq::dep_tracker dep = nullptr;
     node->add_str_eq(seq::str_eq(e, xy, dep));
 
     auto sr = node->simplify_and_init();
@@ -1755,7 +1762,7 @@ static void test_simplify_empty_vs_char() {
 
     // ε = A → rhs has non-variable token → conflict
     seq::nielsen_node* node = ng.mk_node();
-    seq::dep_tracker dep; dep.insert(0);
+    seq::dep_tracker dep = nullptr;
     node->add_str_eq(seq::str_eq(e, a, dep));
 
     auto sr = node->simplify_and_init();
@@ -1781,7 +1788,7 @@ static void test_simplify_multi_pass_clash() {
     euf::snode* ac = sg.mk_concat(a, c);
 
     seq::nielsen_node* node = ng.mk_node();
-    seq::dep_tracker dep; dep.insert(0);
+    seq::dep_tracker dep = nullptr;
     node->add_str_eq(seq::str_eq(ab, ac, dep));
 
     auto sr = node->simplify_and_init();
@@ -1804,7 +1811,7 @@ static void test_simplify_trivial_removal() {
     euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort());
 
     seq::nielsen_node* node = ng.mk_node();
-    seq::dep_tracker dep; dep.insert(0);
+    seq::dep_tracker dep = nullptr;
     node->add_str_eq(seq::str_eq(e, e, dep));  // trivial
     node->add_str_eq(seq::str_eq(x, y, dep));  // non-trivial
 
@@ -1827,7 +1834,7 @@ static void test_simplify_all_trivial_satisfied() {
     euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort());
 
     seq::nielsen_node* node = ng.mk_node();
-    seq::dep_tracker dep; dep.insert(0);
+    seq::dep_tracker dep = nullptr;
     node->add_str_eq(seq::str_eq(x, x, dep));  // trivial: same pointer
     node->add_str_eq(seq::str_eq(e, e, dep));  // trivial: both empty
 
@@ -1854,7 +1861,7 @@ static void test_simplify_regex_infeasible() {
 
     // ε ∈ to_re("A") → non-nullable → conflict
     seq::nielsen_node* node = ng.mk_node();
-    seq::dep_tracker dep; dep.insert(0);
+    seq::dep_tracker dep = nullptr;
     node->add_str_mem(seq::str_mem(e, regex, e, 0, dep));
 
     auto sr = node->simplify_and_init();
@@ -1882,7 +1889,7 @@ static void test_simplify_nullable_removal() {
 
     // ε ∈ star(to_re("A")) → nullable → satisfied, mem removed
     seq::nielsen_node* node = ng.mk_node();
-    seq::dep_tracker dep; dep.insert(0);
+    seq::dep_tracker dep = nullptr;
     node->add_str_mem(seq::str_mem(e, regex, e, 0, dep));
 
     auto sr = node->simplify_and_init();
@@ -1910,7 +1917,7 @@ static void test_simplify_brzozowski_sat() {
 
     // "A" ∈ to_re("A") → derivative consumes 'A' → ε ∈ ε-regex → satisfied
     seq::nielsen_node* node = ng.mk_node();
-    seq::dep_tracker dep; dep.insert(0);
+    seq::dep_tracker dep = nullptr;
     node->add_str_mem(seq::str_mem(a, regex, e, 0, dep));
 
     auto sr = node->simplify_and_init();
@@ -1942,7 +1949,7 @@ static void test_simplify_brzozowski_rtl_suffix() {
 
     // x·"A" ∈ to_re("BA") → RTL consume trailing 'A' → x ∈ to_re("B")
     seq::nielsen_node* node = ng.mk_node();
-    seq::dep_tracker dep; dep.insert(0);
+    seq::dep_tracker dep = nullptr;
     node->add_str_mem(seq::str_mem(xa, regex, e, 0, dep));
 
     auto sr = node->simplify_and_init();
@@ -1972,7 +1979,7 @@ static void test_simplify_multiple_eqs() {
     euf::snode* e = sg.mk_empty_seq(seq.str.mk_string_sort());
 
     seq::nielsen_node* node = ng.mk_node();
-    seq::dep_tracker dep; dep.insert(0);
+    seq::dep_tracker dep = nullptr;
 
     // eq1: ε = ε (trivial → removed)
     node->add_str_eq(seq::str_eq(e, e, dep));
@@ -2409,11 +2416,13 @@ static void test_length_constraints_deps() {
 
     // all constraints should have dependency on eq 0
     for (auto const& c : constraints) {
-        SASSERT(!c.m_dep.empty());
-        unsigned_vector bits;
-        for (unsigned b : c.m_dep) bits.push_back(b);
-        SASSERT(bits.size() == 1);
-        SASSERT(bits[0] == 0);
+        SASSERT(c.m_dep != nullptr);
+        vector<seq::dep_source, false> vs;
+        ng.dep_mgr().linearize(c.m_dep, vs);
+        bool found = false;
+        for (auto const& d : vs)
+            if (d.m_kind == seq::dep_source::kind::eq && d.index == 0) found = true;
+        SASSERT(found);
     }
 
     std::cout << "  dependency tracking correct\n";
@@ -3253,9 +3262,8 @@ static void test_parikh_dep_tracking() {
     SASSERT(constraints.size() >= 2);
 
     // all Parikh constraints should have non-empty deps
-    for (auto const& c : constraints) {
-        SASSERT(!c.m_dep.empty());
-    }
+    for (auto const& c : constraints)
+        SASSERT(c.m_dep != nullptr);
     std::cout << "  all constraints have non-empty deps\n";
 }
 
@@ -3300,7 +3308,7 @@ static void test_add_lower_int_bound_basic() {
     ng.add_str_eq(x, x);  // create root node
 
     seq::nielsen_node* node = ng.root();
-    seq::dep_tracker dep;
+    seq::dep_tracker dep = nullptr;
 
     // initially no bounds
     SASSERT(node->var_lb(x) == 0);
@@ -3344,7 +3352,7 @@ static void test_add_upper_int_bound_basic() {
     ng.add_str_eq(x, x);
 
     seq::nielsen_node* node = ng.root();
-    seq::dep_tracker dep;
+    seq::dep_tracker dep = nullptr;
 
     SASSERT(node->var_ub(x) == UINT_MAX);
 
@@ -3385,7 +3393,7 @@ static void test_add_bound_lb_gt_ub_conflict() {
     ng.add_str_eq(x, x);
 
     seq::nielsen_node* node = ng.root();
-    seq::dep_tracker dep;
+    seq::dep_tracker dep = nullptr;
 
     // set ub=3 first
     node->add_upper_int_bound(x, 3, dep);
@@ -3415,7 +3423,7 @@ static void test_bounds_cloned() {
     ng.add_str_eq(x, y);
 
     seq::nielsen_node* parent = ng.root();
-    seq::dep_tracker dep;
+    seq::dep_tracker dep = nullptr;
 
     // set bounds on parent
     parent->add_lower_int_bound(x, 2, dep);
@@ -3454,7 +3462,7 @@ static void test_var_bound_watcher_single_var() {
     ng.add_str_eq(x, y);
 
     seq::nielsen_node* node = ng.root();
-    seq::dep_tracker dep;
+    seq::dep_tracker dep = nullptr;
 
     // set bounds: 3 <= len(x) <= 7
     node->add_lower_int_bound(x, 3, dep);
@@ -3491,7 +3499,7 @@ static void test_var_bound_watcher_conflict() {
     ng.add_str_eq(x, a);
 
     seq::nielsen_node* node = ng.root();
-    seq::dep_tracker dep;
+    seq::dep_tracker dep = nullptr;
 
     // set bounds: 3 <= len(x)  (so x must have at least 3 chars)
     node->add_lower_int_bound(x, 3, dep);
@@ -3625,7 +3633,7 @@ static void test_var_bound_watcher_multi_var() {
     ng.add_str_eq(x, y);
 
     seq::nielsen_node* node = ng.root();
-    seq::dep_tracker dep;
+    seq::dep_tracker dep = nullptr;
 
     // set upper bound: len(x) <= 5
     node->add_upper_int_bound(x, 5, dep);
diff --git a/src/test/seq_parikh.cpp b/src/test/seq_parikh.cpp
index 83bbc3da4..d8a7d0b6a 100644
--- a/src/test/seq_parikh.cpp
+++ b/src/test/seq_parikh.cpp
@@ -319,7 +319,8 @@ static void test_generate_constraints_ab_star() {
     euf::snode* x = sg.mk_var(symbol("x"));
     expr_ref re = mk_ab_star(m, seq);
     euf::snode* regex = sg.mk(re);
-    seq::dep_tracker dep; dep.insert(0);
+    seq::dep_manager dm;
+    seq::dep_tracker dep = dm.mk_leaf({seq::dep_source::kind::mem, 0});
     seq::str_mem mem(x, regex, nullptr, 0, dep);
 
     vector<seq::int_constraint> out;
@@ -364,7 +365,8 @@ static void test_generate_constraints_bounded_loop() {
     expr_ref ab = mk_to_re_ab(m, seq);
     expr_ref re(seq.re.mk_loop(ab, 1, 3), m);
     euf::snode* regex = sg.mk(re);
-    seq::dep_tracker dep; dep.insert(0);
+    seq::dep_manager dm;
+    seq::dep_tracker dep = dm.mk_leaf({seq::dep_source::kind::mem, 0});
     seq::str_mem mem(x, regex, nullptr, 0, dep);
 
     vector<seq::int_constraint> out;
@@ -400,7 +402,8 @@ static void test_generate_constraints_stride_one() {
     // full_seq: stride=1 → no modular constraint
     expr_ref re(seq.re.mk_full_seq(str_sort), m);
     euf::snode* regex = sg.mk(re);
-    seq::dep_tracker dep; dep.insert(0);
+    seq::dep_manager dm;
+    seq::dep_tracker dep = dm.mk_leaf({seq::dep_source::kind::mem, 0});
     seq::str_mem mem(x, regex, nullptr, 0, dep);
 
     vector<seq::int_constraint> out;
@@ -422,7 +425,8 @@ static void test_generate_constraints_fixed_length() {
     euf::snode* x = sg.mk_var(symbol("x"));
     expr_ref re = mk_to_re_ab(m, seq);  // fixed len 2
     euf::snode* regex = sg.mk(re);
-    seq::dep_tracker dep; dep.insert(0);
+    seq::dep_manager dm;
+    seq::dep_tracker dep = dm.mk_leaf({seq::dep_source::kind::mem, 0});
     seq::str_mem mem(x, regex, nullptr, 0, dep);
 
     vector<seq::int_constraint> out;
@@ -444,19 +448,24 @@ static void test_generate_constraints_dep_propagated() {
     euf::snode* x = sg.mk_var(symbol("x"));
     expr_ref re = mk_ab_star(m, seq);
     euf::snode* regex = sg.mk(re);
-    seq::dep_tracker dep; dep.insert(7);
+    seq::dep_manager dm;
+    seq::dep_tracker dep = dm.mk_leaf({seq::dep_source::kind::mem, 7});
     seq::str_mem mem(x, regex, nullptr, 0, dep);
 
     vector<seq::int_constraint> out;
     parikh.generate_parikh_constraints(mem, out);
 
-    // all generated constraints must carry bit 7 in their dependency
+    // all generated constraints must carry dep_source{mem,7} in their dependency
     for (auto const& ic : out) {
-        SASSERT(!ic.m_dep.empty());
-        seq::dep_tracker d7; d7.insert(7);
-        SASSERT(d7.subset_of(ic.m_dep));
+        SASSERT(ic.m_dep != nullptr);
+        vector<seq::dep_source, false> vs;
+        dm.linearize(ic.m_dep, vs);
+        bool found = false;
+        for (auto const& d : vs)
+            if (d.m_kind == seq::dep_source::kind::mem && d.index == 7) found = true;
+        SASSERT(found);
     }
-    std::cout << "  all constraints carry dep bit 7\n";
+    std::cout << "  all constraints carry dep {mem,7}\n";
 }
 
 // ---------------------------------------------------------------------------
@@ -565,7 +574,7 @@ static void test_check_conflict_valid_k_exists() {
     ng.add_str_mem(x, regex);
 
     // lb=3, ub=5: length 4 is achievable (k=2) → no conflict
-    seq::dep_tracker dep; dep.insert(0);
+    seq::dep_tracker dep = ng.dep_mgr().mk_leaf({seq::dep_source::kind::mem, 0});
     ng.root()->add_lower_int_bound(x, 3, dep);
     ng.root()->add_upper_int_bound(x, 5, dep);
 
@@ -593,7 +602,7 @@ static void test_check_conflict_no_valid_k() {
     ng.add_str_mem(x, regex);
 
     // lb=3, ub=3: only odd length 3 — never a multiple of 2 → conflict
-    seq::dep_tracker dep; dep.insert(0);
+    seq::dep_tracker dep = ng.dep_mgr().mk_leaf({seq::dep_source::kind::mem, 0});
     ng.root()->add_lower_int_bound(x, 3, dep);
     ng.root()->add_upper_int_bound(x, 3, dep);
 
@@ -621,7 +630,7 @@ static void test_check_conflict_abc_star() {
     ng.add_str_mem(x, regex);
 
     // lb=5, ub=5 → no valid k (5 is not a multiple of 3) → conflict
-    seq::dep_tracker dep; dep.insert(0);
+    seq::dep_tracker dep = ng.dep_mgr().mk_leaf({seq::dep_source::kind::mem, 0});
     ng.root()->add_lower_int_bound(x, 5, dep);
     ng.root()->add_upper_int_bound(x, 5, dep);
 
@@ -648,7 +657,7 @@ static void test_check_conflict_stride_one_never_conflicts() {
     euf::snode* regex = sg.mk(re);
     ng.add_str_mem(x, regex);
 
-    seq::dep_tracker dep; dep.insert(0);
+    seq::dep_tracker dep = ng.dep_mgr().mk_leaf({seq::dep_source::kind::mem, 0});
     ng.root()->add_lower_int_bound(x, 7, dep);
     ng.root()->add_upper_int_bound(x, 7, dep);