Merge pull request #8935 from Z3Prover/copilot/implement-int-bounds-var-bound-watcher

Implement IntBounds/VarBoundWatcher + Constraint.Shared for Nielsen graph arithmetic pruning

src/smt/seq/seq_nielsen.cpp

@@ -116,6 +116,8 @@ namespace seq {
         m_int_constraints.reset();
         m_char_diseqs.reset();
         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)
@@ -133,6 +135,11 @@ namespace seq {
         for (auto const& kv : parent.m_char_ranges) {
             m_char_ranges.insert(kv.m_key, kv.m_value.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);
     }
 
     void nielsen_node::apply_subst(euf::sgraph& sg, nielsen_subst const& s) {
@@ -151,6 +158,8 @@ namespace seq {
             mem.m_regex = sg.subst(mem.m_regex, s.m_var, s.m_replacement);
             mem.m_dep |= s.m_dep;
         }
+        // VarBoundWatcher: propagate bounds on s.m_var to variables in s.m_replacement
+        watch_var_bounds(s);
     }
 
     void nielsen_node::add_char_range(euf::snode* sym_char, char_set const& range) {
@@ -182,6 +191,185 @@ namespace seq {
         existing.push_back(other);
     }
 
+    // -----------------------------------------------
+    // nielsen_node: IntBounds methods
+    // mirrors ZIPT's AddLowerIntBound / AddHigherIntBound
+    // -----------------------------------------------
+
+    unsigned nielsen_node::var_lb(euf::snode* var) const {
+        if (!var) return 0;
+        unsigned v = 0;
+        m_var_lb.find(var->id(), v);
+        return v;
+    }
+
+    unsigned nielsen_node::var_ub(euf::snode* var) const {
+        if (!var) return UINT_MAX;
+        unsigned v = UINT_MAX;
+        m_var_ub.find(var->id(), v);
+        return v;
+    }
+
+    bool nielsen_node::add_lower_int_bound(euf::snode* var, unsigned lb, dep_tracker const& dep) {
+        if (!var || !var->is_var()) return false;
+        unsigned id = var->id();
+        // check against existing lower bound
+        unsigned cur_lb = 0;
+        m_var_lb.find(id, cur_lb);
+        if (lb <= cur_lb) return false;  // no tightening
+        m_var_lb.insert(id, lb);
+        // conflict if lb > current upper bound
+        unsigned cur_ub = UINT_MAX;
+        m_var_ub.find(id, cur_ub);
+        if (lb > cur_ub) {
+            m_is_general_conflict = true;
+            m_reason = backtrack_reason::arithmetic;
+            return true;
+        }
+        // add int_constraint: len(var) >= lb
+        ast_manager& m = m_graph->sg().get_manager();
+        seq_util& seq = m_graph->sg().get_seq_util();
+        arith_util arith(m);
+        expr_ref len_var(seq.str.mk_length(var->get_expr()), m);
+        expr_ref bound(arith.mk_int(lb), m);
+        m_int_constraints.push_back(int_constraint(len_var, bound, int_constraint_kind::ge, dep, m));
+        return true;
+    }
+
+    bool nielsen_node::add_upper_int_bound(euf::snode* var, unsigned ub, dep_tracker const& dep) {
+        if (!var || !var->is_var()) return false;
+        unsigned id = var->id();
+        // check against existing upper bound
+        unsigned cur_ub = UINT_MAX;
+        m_var_ub.find(id, cur_ub);
+        if (ub >= cur_ub) return false;  // no tightening
+        m_var_ub.insert(id, ub);
+        // conflict if current lower bound > ub
+        unsigned cur_lb = 0;
+        m_var_lb.find(id, cur_lb);
+        if (cur_lb > ub) {
+            m_is_general_conflict = true;
+            m_reason = backtrack_reason::arithmetic;
+            return true;
+        }
+        // add int_constraint: len(var) <= ub
+        ast_manager& m = m_graph->sg().get_manager();
+        seq_util& seq = m_graph->sg().get_seq_util();
+        arith_util arith(m);
+        expr_ref len_var(seq.str.mk_length(var->get_expr()), m);
+        expr_ref bound(arith.mk_int(ub), m);
+        m_int_constraints.push_back(int_constraint(len_var, bound, int_constraint_kind::le, dep, m));
+        return true;
+    }
+
+    // VarBoundWatcher: after applying substitution s, propagate bounds on s.m_var
+    // to variables in s.m_replacement.
+    // If s.m_var has bounds [lo, hi], and the replacement decomposes into
+    // const_len concrete chars plus a list of variable tokens, then:
+    //   - for a single variable y: lo-const_len <= len(y) <= hi-const_len
+    //   - for multiple variables: each gets an upper bound hi-const_len
+    // Mirrors ZIPT's VarBoundWatcher mechanism.
+    void nielsen_node::watch_var_bounds(nielsen_subst const& s) {
+        if (!s.m_var) return;
+        unsigned id = s.m_var->id();
+        unsigned lo = 0, hi = UINT_MAX;
+        m_var_lb.find(id, lo);
+        m_var_ub.find(id, hi);
+        if (lo == 0 && hi == UINT_MAX) return;  // no bounds to propagate
+
+        // decompose replacement into constant length + variable tokens
+        if (!s.m_replacement) return;
+        euf::snode_vector tokens;
+        s.m_replacement->collect_tokens(tokens);
+
+        unsigned const_len = 0;
+        euf::snode_vector var_tokens;
+        for (euf::snode* t : tokens) {
+            if (t->is_char() || t->is_unit()) {
+                ++const_len;
+            } else if (t->is_var()) {
+                var_tokens.push_back(t);
+            } else {
+                // power or unknown token: cannot propagate simply, abort
+                return;
+            }
+        }
+
+        if (var_tokens.empty()) {
+            // all concrete: check if const_len is within [lo, hi]
+            if (const_len < lo || (hi != UINT_MAX && const_len > hi)) {
+                m_is_general_conflict = true;
+                m_reason = backtrack_reason::arithmetic;
+            }
+            return;
+        }
+
+        if (var_tokens.size() == 1) {
+            euf::snode* y = var_tokens[0];
+            // lo <= const_len + len(y) => len(y) >= lo - const_len (if lo > const_len)
+            if (lo > const_len)
+                add_lower_int_bound(y, lo - const_len, s.m_dep);
+            // const_len + len(y) <= hi => len(y) <= hi - const_len
+            if (hi != UINT_MAX) {
+                if (const_len > hi) {
+                    m_is_general_conflict = true;
+                    m_reason = backtrack_reason::arithmetic;
+                } else {
+                    add_upper_int_bound(y, hi - const_len, s.m_dep);
+                }
+            }
+        } else {
+            // multiple variables: propagate upper bound to each
+            // (each variable contributes >= 0, so each <= hi - const_len)
+            if (hi != UINT_MAX) {
+                if (const_len > hi) {
+                    m_is_general_conflict = true;
+                    m_reason = backtrack_reason::arithmetic;
+                    return;
+                }
+                unsigned each_ub = hi - const_len;
+                for (euf::snode* y : var_tokens)
+                    add_upper_int_bound(y, each_ub, s.m_dep);
+            }
+        }
+    }
+
+    // Initialize per-variable Parikh bounds from this node's regex memberships.
+    // For each str_mem (str ∈ regex) with bounded regex length [min_len, max_len],
+    // calls add_lower/upper_int_bound for the primary string variable (if str is
+    // a single variable) or stores a bound on the length expression otherwise.
+    void nielsen_node::init_var_bounds_from_mems() {
+        for (str_mem const& mem : m_str_mem) {
+            if (!mem.m_str || !mem.m_regex) continue;
+            unsigned min_len = 0, max_len = UINT_MAX;
+            m_graph->compute_regex_length_interval(mem.m_regex, min_len, max_len);
+            if (min_len == 0 && max_len == UINT_MAX) continue;
+
+            // if str is a single variable, apply bounds directly
+            if (mem.m_str->is_var()) {
+                if (min_len > 0)
+                    add_lower_int_bound(mem.m_str, min_len, mem.m_dep);
+                if (max_len < UINT_MAX)
+                    add_upper_int_bound(mem.m_str, max_len, mem.m_dep);
+            } else {
+                // str is a concatenation or other term: add as general int_constraints
+                ast_manager& m = m_graph->sg().get_manager();
+                arith_util arith(m);
+                expr_ref len_str = m_graph->compute_length_expr(mem.m_str);
+                if (min_len > 0) {
+                    expr_ref bound(arith.mk_int(min_len), m);
+                    m_int_constraints.push_back(
+                        int_constraint(len_str, bound, int_constraint_kind::ge, mem.m_dep, m));
+                }
+                if (max_len < UINT_MAX) {
+                    expr_ref bound(arith.mk_int(max_len), m);
+                    m_int_constraints.push_back(
+                        int_constraint(len_str, bound, int_constraint_kind::le, mem.m_dep, m));
+                }
+            }
+        }
+    }
+
     void nielsen_node::apply_char_subst(euf::sgraph& sg, char_subst const& s) {
         if (!s.m_var) return;
 
@@ -318,6 +506,7 @@ namespace seq {
         m_fresh_cnt = 0;
         m_num_input_eqs = 0;
         m_num_input_mems = 0;
+        m_root_constraints_asserted = false;
     }
 
     std::ostream& nielsen_graph::display(std::ostream& out) const {
@@ -802,6 +991,10 @@ namespace seq {
         if (wi < m_str_mem.size())
             m_str_mem.shrink(wi);
 
+        // IntBounds initialization: derive per-variable Parikh length bounds from
+        // remaining regex memberships and add to m_int_constraints.
+        init_var_bounds_from_mems();
+
         if (is_satisfied())
             return simplify_result::satisfied;
 
@@ -839,6 +1032,22 @@ namespace seq {
     // nielsen_graph: search
     // -----------------------------------------------------------------------
 
+    void nielsen_graph::assert_root_constraints_to_solver() {
+        if (m_root_constraints_asserted) return;
+        m_root_constraints_asserted = true;
+        // Constraint.Shared: assert all root-level length/Parikh constraints
+        // to m_solver at the base level (no push/pop). These include:
+        //   - len(lhs) = len(rhs) for each non-trivial string equality
+        //   - len(str) >= min_len and len(str) <= max_len for each regex membership
+        //   - len(x) >= 0 for each variable appearing in the root constraints
+        // Making these visible to the solver before the DFS allows arithmetic
+        // pruning at every node, not just the root.
+        vector<length_constraint> constraints;
+        generate_length_constraints(constraints);
+        for (auto const& lc : constraints)
+            m_solver.assert_expr(lc.m_expr);
+    }
+
     nielsen_graph::search_result nielsen_graph::solve() {
         if (!m_root)
             return search_result::sat;
@@ -847,6 +1056,10 @@ namespace seq {
         m_sat_node = nullptr;
         m_sat_path.reset();
 
+        // Constraint.Shared: assert root-level length/Parikh constraints to the
+        // solver at the base level, so they are visible during all feasibility checks.
+        assert_root_constraints_to_solver();
+
         // Iterative deepening: increment by 1 on each failure.
         // m_max_search_depth == 0 means unlimited; otherwise stop when bound exceeds it.
         m_depth_bound = 3;

src/smt/seq/seq_nielsen.h

@@ -164,9 +164,10 @@ Abstract:
       has no ConstraintsIntEq or ConstraintsIntLe in nielsen_node.
     - IntBounds / VarBoundWatcher: per-variable integer interval bounds and the
       watcher mechanism that reruns bound propagation when a string variable is
-      substituted are not ported.
+      substituted — PORTED as nielsen_node::{add_lower_int_bound,
+      add_upper_int_bound, watch_var_bounds, init_var_bounds_from_mems}.
     - AddLowerIntBound() / AddHigherIntBound(): incremental interval tightening
-      with restart signaling is not ported.
+      — PORTED as the above add_lower/upper_int_bound methods.
 
     Character-level handling:
     - CharSubst: character-level variable substitution (symbolic char -> concrete
@@ -214,7 +215,10 @@ Abstract:
     - GetSignature(): the constraint-pair signature used for subsumption
       candidate matching is not ported.
     - Constraint.Shared: the flag indicating whether a constraint should be
-      forwarded to the outer solver is not ported.
+      forwarded to the outer solver — PORTED as
+      nielsen_graph::assert_root_constraints_to_solver(), called at the start
+      of solve() to make all root-level length/Parikh constraints immediately
+      visible to m_solver.
     - Interpretation: the model-extraction class mapping string and integer
       variables to concrete values is not ported.
     -----------------------------------------------------------------------
@@ -490,6 +494,12 @@ namespace seq {
         vector<str_mem>         m_str_mem;    // regex memberships
         vector<int_constraint>  m_int_constraints;  // integer equalities/inequalities (mirrors ZIPT's IntEq/IntLe)
 
+        // per-variable integer bounds for len(var). Mirrors ZIPT's IntBounds.
+        // key: snode id of the string variable.
+        // default lb = 0 (unrestricted); default ub = UINT_MAX (unrestricted).
+        u_map<unsigned>                m_var_lb;   // lower bound: lb <= len(var)
+        u_map<unsigned>                m_var_ub;   // upper bound: len(var) <= ub
+
         // character constraints (mirrors ZIPT's DisEqualities and CharRanges)
         // key: snode id of the s_unit symbolic character
         u_map<ptr_vector<euf::snode>>  m_char_diseqs;  // ?c != {?d, ?e, ...}
@@ -528,6 +538,28 @@ namespace seq {
         vector<int_constraint> const& int_constraints() const { return m_int_constraints; }
         vector<int_constraint>& int_constraints() { return m_int_constraints; }
 
+        // IntBounds: tighten the lower bound for len(var).
+        // Returns true if the bound was tightened (lb > current lower bound).
+        // When tightened without conflict, adds an int_constraint len(var) >= lb.
+        // When lb > current upper bound, sets arithmetic conflict (no constraint added)
+        // and still returns true (the bound value changed). Check is_general_conflict()
+        // separately to distinguish tightening-with-conflict from normal tightening.
+        // Mirrors ZIPT's AddLowerIntBound().
+        bool add_lower_int_bound(euf::snode* var, unsigned lb, dep_tracker const& dep);
+
+        // IntBounds: tighten the upper bound for len(var).
+        // Returns true if the bound was tightened (ub < current upper bound).
+        // When tightened without conflict, adds an int_constraint len(var) <= ub.
+        // When current lower bound > ub, sets arithmetic conflict (no constraint added)
+        // and still returns true (the bound value changed). Check is_general_conflict()
+        // separately to distinguish tightening-with-conflict from normal tightening.
+        // Mirrors ZIPT's AddHigherIntBound().
+        bool add_upper_int_bound(euf::snode* var, unsigned ub, dep_tracker const& dep);
+
+        // Query current bounds for a variable (default: 0 / UINT_MAX if not set).
+        unsigned var_lb(euf::snode* var) const;
+        unsigned var_ub(euf::snode* var) const;
+
         // character constraint access (mirrors ZIPT's DisEqualities / CharRanges)
         u_map<ptr_vector<euf::snode>> const& char_diseqs() const { return m_char_diseqs; }
         u_map<char_set> const& char_ranges() const { return m_char_ranges; }
@@ -603,6 +635,19 @@ namespace seq {
         // sets changed=true, and returns false.
         bool handle_empty_side(euf::sgraph& sg, euf::snode* non_empty_side,
                                dep_tracker const& dep, bool& changed);
+
+        // VarBoundWatcher: after applying substitution s, propagate the bounds
+        // of s.m_var to variables appearing in s.m_replacement.
+        // When var has bounds [lo, hi], derives bounds for variables in replacement
+        // using the known constant-length contribution of non-variable tokens.
+        // Mirrors ZIPT's VarBoundWatcher re-check mechanism.
+        void watch_var_bounds(nielsen_subst const& s);
+
+        // Initialize per-variable Parikh bounds from this node's regex memberships.
+        // For each str_mem constraint (str ∈ regex) where regex has length bounds
+        // [min_len, max_len], adds lower/upper bound constraints for len(str).
+        // Called from simplify_and_init to populate IntBounds at node creation.
+        void init_var_bounds_from_mems();
     };
 
     // search statistics collected during Nielsen graph solving
@@ -662,6 +707,10 @@ namespace seq {
         // -----------------------------------------------
         simple_solver&                m_solver;
 
+        // Constraint.Shared: guards re-assertion of root-level constraints.
+        // Set to true after assert_root_constraints_to_solver() is first called.
+        bool                          m_root_constraints_asserted = false;
+
     public:
         // Construct with a caller-supplied solver.  Ownership is NOT transferred;
         // the caller is responsible for keeping the solver alive.
@@ -754,6 +803,16 @@ namespace seq {
         // Also generates len(x) >= 0 for each variable appearing in the equations.
         void generate_length_constraints(vector<length_constraint>& constraints);
 
+        // build an arithmetic expression representing the length of an snode tree.
+        // concatenations are expanded to sums, chars to 1, empty to 0,
+        // variables to (str.len var_expr).
+        expr_ref compute_length_expr(euf::snode* n);
+
+        // compute Parikh length interval [min_len, max_len] for a regex snode.
+        // uses seq_util::rex min_length/max_length on the underlying expression.
+        // max_len == UINT_MAX means unbounded.
+        void compute_regex_length_interval(euf::snode* regex, unsigned& min_len, unsigned& max_len);
+
     private:
         search_result search_dfs(nielsen_node* node, unsigned depth, svector<nielsen_edge*>& cur_path);
 
@@ -860,20 +919,17 @@ namespace seq {
         // find a power token facing a variable head
         bool find_power_vs_var(nielsen_node* node, euf::snode*& power, euf::snode*& var_head, str_eq const*& eq_out) const;
 
-        // build an arithmetic expression representing the length of an snode tree.
-        // concatenations are expanded to sums, chars to 1, empty to 0,
-        // variables to (str.len var_expr).
-        expr_ref compute_length_expr(euf::snode* n);
-
-        // compute Parikh length interval [min_len, max_len] for a regex snode.
-        // uses seq_util::rex min_length/max_length on the underlying expression.
-        // max_len == UINT_MAX means unbounded.
-        void compute_regex_length_interval(euf::snode* regex, unsigned& min_len, unsigned& max_len);
-
         // -----------------------------------------------
         // Integer feasibility subsolver methods
         // -----------------------------------------------
 
+        // Constraint.Shared: assert all root-level length/Parikh constraints to
+        // m_solver at the base level (outside push/pop). Called once at the start
+        // of solve(). Makes derived constraints immediately visible to m_solver
+        // for arithmetic pruning at every DFS node, not just the root.
+        // Mirrors ZIPT's Constraint.Shared forwarding mechanism.
+        void assert_root_constraints_to_solver();
+
         // collect int_constraints along the path from root to the given node,
         // including constraints from edges and nodes.
         void collect_path_int_constraints(nielsen_node* node,

src/test/nseq_basic.cpp

@@ -21,6 +21,15 @@ Abstract:
 #include "smt/theory_nseq.h"
 #include <iostream>
 
+// Trivial solver that always returns sat and ignores all assertions.
+class nseq_basic_dummy_solver : public seq::simple_solver {
+public:
+    void push() override {}
+    void pop(unsigned) override {}
+    void assert_expr(expr*) override {}
+    lbool check() override { return l_true; }
+};
+
 // Test 1: instantiation of nielsen_graph compiles and doesn't crash
 static void test_nseq_instantiation() {
     std::cout << "test_nseq_instantiation\n";
@@ -28,7 +37,8 @@ static void test_nseq_instantiation() {
     reg_decl_plugins(m);
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
-    seq::nielsen_graph ng(sg);
+    nseq_basic_dummy_solver solver;
+    seq::nielsen_graph ng(sg, solver);
     SASSERT(ng.root() == nullptr);
     SASSERT(ng.num_nodes() == 0);
     std::cout << "  ok\n";
@@ -83,7 +93,8 @@ static void test_nseq_simplification() {
     reg_decl_plugins(m);
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
-    seq::nielsen_graph ng(sg);
+    nseq_basic_dummy_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     // Add a trivial equality: empty = empty
     euf::snode* empty1 = sg.mk_empty();
@@ -104,7 +115,8 @@ static void test_nseq_node_satisfied() {
     reg_decl_plugins(m);
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
-    seq::nielsen_graph ng(sg);
+    nseq_basic_dummy_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     seq::nielsen_node* node = ng.mk_node();
     // empty node has no constraints => satisfied
@@ -130,7 +142,8 @@ static void test_nseq_symbol_clash() {
     reg_decl_plugins(m);
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
-    seq::nielsen_graph ng(sg);
+    nseq_basic_dummy_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* a = sg.mk_char('a');
     euf::snode* b = sg.mk_char('b');
@@ -155,7 +168,8 @@ static void test_nseq_var_eq_self() {
     reg_decl_plugins(m);
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
-    seq::nielsen_graph ng(sg);
+    nseq_basic_dummy_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     ng.add_str_eq(x, x);
@@ -172,7 +186,8 @@ static void test_nseq_prefix_clash() {
     reg_decl_plugins(m);
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
-    seq::nielsen_graph ng(sg);
+    nseq_basic_dummy_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* a = sg.mk_char('a');
@@ -193,7 +208,8 @@ static void test_nseq_const_nielsen_solvable() {
     reg_decl_plugins(m);
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
-    seq::nielsen_graph ng(sg);
+    nseq_basic_dummy_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* x = sg.mk_var(symbol("x"));
     euf::snode* y = sg.mk_var(symbol("y"));
@@ -215,7 +231,8 @@ static void test_nseq_length_mismatch() {
     reg_decl_plugins(m);
     euf::egraph eg(m);
     euf::sgraph sg(m, eg);
-    seq::nielsen_graph ng(sg);
+    nseq_basic_dummy_solver solver;
+    seq::nielsen_graph ng(sg, solver);
 
     euf::snode* a = sg.mk_char('a');
     euf::snode* b = sg.mk_char('b');

src/test/nseq_zipt.cpp

@@ -29,6 +29,15 @@ Abstract:
 #include <functional>
 #include <chrono>
 
+// Trivial solver that always returns sat and ignores all assertions.
+class nseq_zipt_dummy_solver : public seq::simple_solver {
+public:
+    void push() override {}
+    void pop(unsigned) override {}
+    void assert_expr(expr*) override {}
+    lbool check() override { return l_true; }
+};
+
 // -----------------------------------------------------------------------
 // Trivial simple_solver stub: optimistically assumes integer constraints
 // are always feasible (returns l_true without actually checking).

src/test/seq_nielsen.cpp

@@ -27,7 +27,7 @@ public:
     dummy_simple_solver() : seq::simple_solver() {}
     void push() override {}
     void pop(unsigned n) override {}
-    void assert_expr(expr *constraint) override {}
+    void assert_expr(expr *e) override {}
     lbool check() override {
         return l_true;
     }
@@ -3133,6 +3133,390 @@ static void test_parikh_dep_tracking() {
     std::cout << "  all constraints have non-empty deps\n";
 }
 
+// -----------------------------------------------------------------------
+// IntBounds / VarBoundWatcher tests (Task: IntBounds/Constraint.Shared)
+// -----------------------------------------------------------------------
+
+// tracking solver: records assert_expr calls for inspection
+class tracking_solver : public seq::simple_solver {
+public:
+    vector<expr_ref> asserted;
+    ast_manager& m;
+    unsigned push_count = 0;
+    unsigned pop_count = 0;
+    lbool check_result = l_true;
+
+    tracking_solver(ast_manager& m) : m(m) {}
+    void push() override { ++push_count; }
+    void pop(unsigned n) override { pop_count += n; }
+    void assert_expr(expr* e) override { asserted.push_back(expr_ref(e, m)); }
+    lbool check() override { return check_result; }
+    void reset_tracking() {
+        asserted.reset();
+        push_count = 0;
+        pop_count = 0;
+    }
+};
+
+// test add_lower_int_bound: basic tightening adds int_constraint
+static void test_add_lower_int_bound_basic() {
+    std::cout << "test_add_lower_int_bound_basic\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::egraph eg(m);
+    euf::sgraph sg(m, eg);
+    seq_util seq(m);
+
+    euf::snode* x = sg.mk_var(symbol("x"));
+
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
+    ng.add_str_eq(x, x);  // create root node
+
+    seq::nielsen_node* node = ng.root();
+    seq::dep_tracker dep;
+
+    // initially no bounds
+    SASSERT(node->var_lb(x) == 0);
+    SASSERT(node->var_ub(x) == UINT_MAX);
+    SASSERT(node->int_constraints().empty());
+
+    // add lower bound lb=3: should tighten and add constraint
+    bool tightened = node->add_lower_int_bound(x, 3, dep);
+    SASSERT(tightened);
+    SASSERT(node->var_lb(x) == 3);
+    SASSERT(node->int_constraints().size() == 1);
+    SASSERT(node->int_constraints()[0].m_kind == seq::int_constraint_kind::ge);
+
+    // add weaker lb=2: no tightening
+    tightened = node->add_lower_int_bound(x, 2, dep);
+    SASSERT(!tightened);
+    SASSERT(node->var_lb(x) == 3);
+    SASSERT(node->int_constraints().size() == 1);
+
+    // add tighter lb=5: should tighten and add another constraint
+    tightened = node->add_lower_int_bound(x, 5, dep);
+    SASSERT(tightened);
+    SASSERT(node->var_lb(x) == 5);
+    SASSERT(node->int_constraints().size() == 2);
+
+    std::cout << "  ok\n";
+}
+
+// test add_upper_int_bound: basic tightening adds int_constraint
+static void test_add_upper_int_bound_basic() {
+    std::cout << "test_add_upper_int_bound_basic\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::egraph eg(m);
+    euf::sgraph sg(m, eg);
+
+    euf::snode* x = sg.mk_var(symbol("x"));
+
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
+    ng.add_str_eq(x, x);
+
+    seq::nielsen_node* node = ng.root();
+    seq::dep_tracker dep;
+
+    SASSERT(node->var_ub(x) == UINT_MAX);
+
+    // add upper bound ub=10: tightens
+    bool tightened = node->add_upper_int_bound(x, 10, dep);
+    SASSERT(tightened);
+    SASSERT(node->var_ub(x) == 10);
+    SASSERT(node->int_constraints().size() == 1);
+    SASSERT(node->int_constraints()[0].m_kind == seq::int_constraint_kind::le);
+
+    // add weaker ub=20: no tightening
+    tightened = node->add_upper_int_bound(x, 20, dep);
+    SASSERT(!tightened);
+    SASSERT(node->var_ub(x) == 10);
+    SASSERT(node->int_constraints().size() == 1);
+
+    // add tighter ub=5: tightens
+    tightened = node->add_upper_int_bound(x, 5, dep);
+    SASSERT(tightened);
+    SASSERT(node->var_ub(x) == 5);
+    SASSERT(node->int_constraints().size() == 2);
+
+    std::cout << "  ok\n";
+}
+
+// test add_lower_int_bound: conflict when lb > ub
+static void test_add_bound_lb_gt_ub_conflict() {
+    std::cout << "test_add_bound_lb_gt_ub_conflict\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::egraph eg(m);
+    euf::sgraph sg(m, eg);
+
+    euf::snode* x = sg.mk_var(symbol("x"));
+
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
+    ng.add_str_eq(x, x);
+
+    seq::nielsen_node* node = ng.root();
+    seq::dep_tracker dep;
+
+    // set ub=3 first
+    node->add_upper_int_bound(x, 3, dep);
+    SASSERT(!node->is_general_conflict());
+
+    // now set lb=5 > ub=3: should trigger conflict
+    node->add_lower_int_bound(x, 5, dep);
+    SASSERT(node->is_general_conflict());
+    SASSERT(node->reason() == seq::backtrack_reason::arithmetic);
+
+    std::cout << "  ok\n";
+}
+
+// test clone_from: child inherits parent bounds
+static void test_bounds_cloned() {
+    std::cout << "test_bounds_cloned\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::egraph eg(m);
+    euf::sgraph sg(m, eg);
+
+    euf::snode* x = sg.mk_var(symbol("x"));
+    euf::snode* y = sg.mk_var(symbol("y"));
+
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
+    ng.add_str_eq(x, y);
+
+    seq::nielsen_node* parent = ng.root();
+    seq::dep_tracker dep;
+
+    // set bounds on parent
+    parent->add_lower_int_bound(x, 2, dep);
+    parent->add_upper_int_bound(x, 7, dep);
+    parent->add_lower_int_bound(y, 1, dep);
+
+    // clone to child
+    seq::nielsen_node* child = ng.mk_child(parent);
+
+    // child should have same bounds
+    SASSERT(child->var_lb(x) == 2);
+    SASSERT(child->var_ub(x) == 7);
+    SASSERT(child->var_lb(y) == 1);
+    SASSERT(child->var_ub(y) == UINT_MAX);
+
+    // child's int_constraints should also be cloned (3 constraints: lb_x, ub_x, lb_y)
+    SASSERT(child->int_constraints().size() == parent->int_constraints().size());
+
+    std::cout << "  ok\n";
+}
+
+// test VarBoundWatcher: substitution x→a·y propagates bounds from x to y
+static void test_var_bound_watcher_single_var() {
+    std::cout << "test_var_bound_watcher_single_var\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::egraph eg(m);
+    euf::sgraph sg(m, eg);
+
+    euf::snode* x = sg.mk_var(symbol("x"));
+    euf::snode* y = sg.mk_var(symbol("y"));
+    euf::snode* a = sg.mk_char('a');
+
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
+    ng.add_str_eq(x, y);
+
+    seq::nielsen_node* node = ng.root();
+    seq::dep_tracker dep;
+
+    // set bounds: 3 <= len(x) <= 7
+    node->add_lower_int_bound(x, 3, dep);
+    node->add_upper_int_bound(x, 7, dep);
+    node->int_constraints().reset();  // clear for clean count
+
+    // apply substitution x → a·y
+    euf::snode* ay = sg.mk_concat(a, y);
+    seq::nielsen_subst s(x, ay, dep);
+    node->apply_subst(sg, s);
+
+    // VarBoundWatcher should propagate: 3 <= 1+len(y) <= 7
+    // => len(y) >= 2, len(y) <= 6
+    SASSERT(node->var_lb(y) == 2);
+    SASSERT(node->var_ub(y) == 6);
+
+    std::cout << "  ok\n";
+}
+
+// test VarBoundWatcher: substitution with all-concrete replacement detects conflict
+static void test_var_bound_watcher_conflict() {
+    std::cout << "test_var_bound_watcher_conflict\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::egraph eg(m);
+    euf::sgraph sg(m, eg);
+
+    euf::snode* x = sg.mk_var(symbol("x"));
+    euf::snode* a = sg.mk_char('a');
+    euf::snode* b = sg.mk_char('b');
+
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
+    ng.add_str_eq(x, a);
+
+    seq::nielsen_node* node = ng.root();
+    seq::dep_tracker dep;
+
+    // set bounds: 3 <= len(x)  (so x must have at least 3 chars)
+    node->add_lower_int_bound(x, 3, dep);
+    node->int_constraints().reset();
+
+    // apply substitution x → a·b (const_len=2 < lb=3)
+    euf::snode* ab = sg.mk_concat(a, b);
+    seq::nielsen_subst s(x, ab, dep);
+    node->apply_subst(sg, s);
+
+    // should detect conflict: len(x) >= 3 but replacement has len=2
+    SASSERT(node->is_general_conflict());
+    SASSERT(node->reason() == seq::backtrack_reason::arithmetic);
+
+    std::cout << "  ok\n";
+}
+
+// test init_var_bounds_from_mems: simplify_and_init adds Parikh bounds
+static void test_simplify_adds_parikh_bounds() {
+    std::cout << "test_simplify_adds_parikh_bounds\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::egraph eg(m);
+    euf::sgraph sg(m, eg);
+    seq_util seq(m);
+
+    euf::snode* x = sg.mk_var(symbol("x"));
+
+    // create regex: to_re("AB") — exactly 2 chars
+    expr_ref ch_a(seq.str.mk_char('A'), m);
+    expr_ref ch_b(seq.str.mk_char('B'), m);
+    expr_ref unit_a(seq.str.mk_unit(ch_a), m);
+    expr_ref unit_b(seq.str.mk_unit(ch_b), m);
+    expr_ref re_ab(seq.re.mk_concat(seq.re.mk_to_re(unit_a), seq.re.mk_to_re(unit_b)), m);
+    euf::snode* regex = sg.mk(re_ab);
+
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
+    ng.add_str_mem(x, regex);
+
+    seq::nielsen_node* node = ng.root();
+
+    // simplify_and_init should call init_var_bounds_from_mems
+    seq::simplify_result sr = node->simplify_and_init(ng);
+    (void)sr;
+
+    // x ∈ to_re("AB") has min_len=2, max_len=2
+    // so lb=2, ub=2 should be set on x
+    SASSERT(node->var_lb(x) == 2);
+    SASSERT(node->var_ub(x) == 2);
+
+    std::cout << "  ok\n";
+}
+
+// test assert_root_constraints_to_solver: root constraints are forwarded
+static void test_assert_root_constraints_to_solver() {
+    std::cout << "test_assert_root_constraints_to_solver\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::egraph eg(m);
+    euf::sgraph sg(m, eg);
+    seq_util seq(m);
+
+    euf::snode* x = sg.mk_var(symbol("x"));
+    euf::snode* a = sg.mk_char('a');
+    euf::snode* b = sg.mk_char('b');
+    euf::snode* ab = sg.mk_concat(a, b);
+
+    tracking_solver ts(m);
+    seq::nielsen_graph ng(sg, ts);
+    // equation: x = a·b → generates len(x) = 2 and len(x) >= 0
+    ng.add_str_eq(x, ab);
+
+    // solve() calls assert_root_constraints_to_solver() internally
+    ts.reset_tracking();
+    ng.solve();
+
+    // should have asserted at least: len(x) = 2, len(x) >= 0
+    SASSERT(ts.asserted.size() >= 2);
+    std::cout << "  asserted " << ts.asserted.size() << " root constraints to solver\n";
+    for (auto& e : ts.asserted)
+        std::cout << "    " << mk_pp(e, m) << "\n";
+
+    std::cout << "  ok\n";
+}
+
+// test assert_root_constraints_to_solver: called only once even across iterations
+static void test_assert_root_constraints_once() {
+    std::cout << "test_assert_root_constraints_once\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::egraph eg(m);
+    euf::sgraph sg(m, eg);
+
+    euf::snode* x = sg.mk_var(symbol("x"));
+    euf::snode* y = sg.mk_var(symbol("y"));
+
+    tracking_solver ts(m);
+    seq::nielsen_graph ng(sg, ts);
+    ng.add_str_eq(x, y);
+
+    // solve is called (iterative deepening runs multiple iterations)
+    ng.solve();
+    unsigned count_first = ts.asserted.size();
+
+    // after reset, assert count should be 0 then non-zero again
+    // (reset clears m_root_constraints_asserted)
+    // We can't call solve() again on the same graph without reset, but
+    // we can verify the count is stable between iterations by checking
+    // that the same constraints weren't added multiple times.
+    // The simplest check: count > 0 (constraints were asserted)
+    SASSERT(count_first > 0);  // x=y produces at least len(x)=len(y) and non-neg constraints
+    std::cout << "  asserted " << count_first << " constraints total during solve\n";
+    std::cout << "  ok\n";
+}
+
+// test VarBoundWatcher with multiple variables in replacement
+static void test_var_bound_watcher_multi_var() {
+    std::cout << "test_var_bound_watcher_multi_var\n";
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::egraph eg(m);
+    euf::sgraph sg(m, eg);
+
+    euf::snode* x = sg.mk_var(symbol("x"));
+    euf::snode* y = sg.mk_var(symbol("y"));
+    euf::snode* z = sg.mk_var(symbol("z"));
+
+    dummy_simple_solver solver;
+    seq::nielsen_graph ng(sg, solver);
+    ng.add_str_eq(x, y);
+
+    seq::nielsen_node* node = ng.root();
+    seq::dep_tracker dep;
+
+    // set upper bound: len(x) <= 5
+    node->add_upper_int_bound(x, 5, dep);
+    node->int_constraints().reset();
+
+    // apply substitution x → y·z (two vars, no constants)
+    euf::snode* yz = sg.mk_concat(y, z);
+    seq::nielsen_subst s(x, yz, dep);
+    node->apply_subst(sg, s);
+
+    // len(y·z) <= 5 → each of y, z gets ub=5
+    SASSERT(node->var_ub(y) == 5);
+    SASSERT(node->var_ub(z) == 5);
+
+    std::cout << "  ok\n";
+}
+
 void tst_seq_nielsen() {
     test_dep_tracker();
     test_str_eq();
@@ -3240,4 +3624,15 @@ void tst_seq_nielsen() {
     test_parikh_mixed_eq_mem();
     test_parikh_full_seq_no_bounds();
     test_parikh_dep_tracking();
+    // IntBounds / VarBoundWatcher / Constraint.Shared tests
+    test_add_lower_int_bound_basic();
+    test_add_upper_int_bound_basic();
+    test_add_bound_lb_gt_ub_conflict();
+    test_bounds_cloned();
+    test_var_bound_watcher_single_var();
+    test_var_bound_watcher_conflict();
+    test_simplify_adds_parikh_bounds();
+    test_assert_root_constraints_to_solver();
+    test_assert_root_constraints_once();
+    test_var_bound_watcher_multi_var();
 }