Refactor seq_derive: inline path pruning with ACI normalization

Replace simplify_ite_rec post-hoc pass with inline path pruning:
- push/pop API with lbool return (l_true=implied, l_undef=pushed, l_false=contradicts)
- apply_ite hoists ITE through union/inter/complement with path-aware pruning
- Path-aware caching for mk_union, mk_inter, mk_complement
- Incremental path expression maintenance for cache keys
- Complement always pushes through ITE for same-condition merge
- ACI normalization (flatten/sort/deduplicate) for union base case
- is_subset subsumption prevents unbounded union growth
- Prefix factoring (a·x ∪ a·y = a·(x ∪ y)) for loop derivatives
- seq_rewriter passed as reference to derive class
- Depth-limited single-ITE hoisting (path_stack.size() < 8)
- pred_implies with signed atoms avoids mk_not allocations
- extract_char_range properly checks m_ele identity

Results: 0 timeouts on regression suite (vs 2 on master).

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

src/ast/rewriter/seq_rewriter.h

@@ -128,6 +128,8 @@ class seq_rewriter {
         void insert(decl_kind op, expr* a, expr* b, expr* c, expr* r);
     };
 
+    friend class seq::derive;
+
     seq_util       m_util;
     arith_util     m_autil;
     bool_rewriter  m_br;
@@ -332,7 +334,7 @@ class seq_rewriter {
 
 public:
     seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
-        m_util(m), m_autil(m), m_br(m, p), m_derive(m), // m_re2aut(m), 
+        m_util(m), m_autil(m), m_br(m, p), m_derive(m, *this), // m_re2aut(m), 
         m_op_cache(m), m_es(m), 
         m_lhs(m), m_rhs(m), m_coalesce_chars(true) {
     }