replace dep_tracker uint_set with scoped_dependency_manager<dep_source>

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

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_tracker dep = m_dep_mgr.mk_leaf({dep_source::kind::eq, m_num_input_eqs});
-        dep.insert(m_root->str_eqs().size());
         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_tracker dep = m_dep_mgr.mk_leaf({dep_source::kind::mem, m_num_input_mems});
-        dep.insert(m_root->str_eqs().size() + m_root->str_mems().size());
         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) {
+        vector<dep_source, false> vs;
-            if (b < m_num_input_eqs)
+        m_dep_mgr.linearize(deps, vs);
-                eq_indices.push_back(b);
+        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);
         }
     }
 

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
+       Z3 uses scoped_dependency_manager<dep_source> (an arena-based binary
-       purpose. The |=/subset_of/empty semantics are equivalent.
+       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
+    // source of a dependency: identifies an input constraint by kind and index.
-    // contributed to deriving a given constraint
+    // kind::eq means a string equality, kind::mem means a regex membership.
-    // mirrors ZIPT's DependencyTracker
+    // index is the 0-based position in the input eq or mem list respectively.
-    using dep_tracker = uint_set;
+    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
@@ -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
+        // explain a conflict: partition the dep_source leaves into str_eq indices
-        // (bits 0..num_eqs-1) and str_mem indices (bits num_eqs..num_eqs+num_mems-1).
+        // (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;
 

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();
+        vector<seq::dep_source, false> vs;
-        for (unsigned b : deps) {
+        m_nielsen.dep_mgr().linearize(deps, vs);
-            if (b < num_input_eqs) {
+        for (seq::dep_source const& d : vs) {
-                eq_source const& src = m_state.get_eq_source(b);
+            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 (d.index < m_nielsen_to_state_mem.size()) {
-                if (mem_idx < m_nielsen_to_state_mem.size()) {
+                    unsigned state_mem_idx = m_nielsen_to_state_mem[d.index];
-                    unsigned state_mem_idx = m_nielsen_to_state_mem[mem_idx];
                     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);
     }