Enable monadic regex solver by default (#10466)

## Summary
- set \smt.seq.regex_monadic\ to \	rue\ by default
- keep the existing option available for explicitly disabling the
monadic regex solver

## Testing
- regenerated and built the parameter helpers and Z3 shell
- confirmed \z3 -p\ reports \seq.regex_monadic (default: true)\`n- ran
the complete unit test suite

Copilot-Session: 2b211510-693f-4df8-9ebb-3db1e08f8683

src/params/smt_params_helper.pyg

@@ -142,7 +142,7 @@ def_module_params(module_name='smt',
                           ('core.validate', BOOL, False, '[internal] validate unsat core produced by SMT context. This option is intended for debugging'),
                           ('seq.split_w_len', BOOL, True, 'enable splitting guided by length constraints'),
                           ('seq.validate', BOOL, False, 'enable self-validation of theory axioms created by seq theory'),
-                          ('seq.regex_monadic', BOOL, False, 'use the monadic regular-expression end-game solver'),
+                          ('seq.regex_monadic', BOOL, True, 'use the monadic regular-expression end-game solver'),
                           ('seq.max_unfolding', UINT, 1000000000, 'maximal unfolding depth for checking string equations and regular expressions'),
                           ('seq.min_unfolding', UINT, 1, 'initial bound for strings whose lengths are bounded by iterative deepening. Set this to a higher value if there are only models with larger string lengths'),
                           ('theory_aware_branching', BOOL, False, 'Allow the context to use extra information from theory solvers regarding literal branching prioritization.'),