[Tuner] Relax z3_solver version constraint (<4.15.8.0)

[bangtianliu]

Currently we pin z3_solver>=4.13.0.0,<4.15.8.0 due to a regression in 4.15.8 that causes the constraint solver to fail on group convolution operations, returning "canceled" status with 0 solutions instead of generating valid candidates.

Working versions: 4.13.0, 4.14.0, 4.15.0, 4.15.4
Broken version: 4.15.8

Action needed:
Monitor z3-solver releases and test newer versions (4.15.9+, 4.16.0+, etc.) to see if the regression is fixed, then relax the version constraint.

To test:

• Run the existing group conv test to verify it generates valid candidates:
  pytest amdsharktuner/tests/rocm/rocm_constraint_generator_test.py::test_generate_solutions_tile_and_fuse_group_conv -v

• Manually test with BOO tuning command:
  convfp16 -n 32 -c 512 -H 50 -W 50 -k 512 -y 3 -x 3 -p 1 -q 1 -u 1 -v 1 -l 1 -j 1 --in_layout NHWC --fil_layout NHWC --out_layout NHWC -m conv -g 32 -F 1 -t 1

Reference: PR #2825, #2826

[kuhar]

@bangtianliu I can see that 4.16 is out -- can you check if we can bump to it?