Port reverse normalization into derive class

Instead of treating reverse(r) as stuck (returning symbolic mk_derivative),
normalize it by pushing reverse inward through the regex structure, then
compute the derivative of the normalized result. Mirrors mk_re_reverse logic.

Handles: concat, union, intersection, diff, ite, opt, complement, star,
plus, loop, to_re (string literals, units, concats), and symmetric cases.

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

src/ast/rewriter/seq_derive.h

@@ -103,6 +103,9 @@ namespace seq {
         // Distribute concatenation through ITE/union in derivative
         expr_ref mk_deriv_concat(expr* d, expr* tail);
 
+        // Normalize reverse(r) by pushing reverse inward
+        expr_ref normalize_reverse(expr* r);
+
         // Simplify ITE conditions w.r.t. m_ele
         expr_ref simplify_ite(expr* d);
         expr_ref simplify_ite_rec(expr* cond, bool sign, expr* d);