Optimize bitvector numeral creation in solvers

[filipeom]

• Bitwuzla: Now uses mk_bv_value_int or mk_bv_value_int64 when possible.
• Z3: Uses mk_numeral_int when possible.
• Dolmen (Alt-Ergo/Colibri2): Directly creates bitstrings from Z.t in of_z, avoiding a string roundtrip.
• Mappings: uses the more optimal of_z.

cc @redianthus. I think most of the times this should use the more optimized version?

[redianthus]

Great, thanks!
I'll try to do some benchmarks next week but this is looking really good and should improve things a lot. :D

I think this is actually exactly the kind of cases where Smtml can particularly shine compared to :

1. Going through a file.
2. Using the API by hand and not doing this kind of optimizations because they're hard to notice and people won't care in the first place and never fix them.

[filipeom]

I think this is actually exactly the kind of cases where Smtml can particularly shine compared to :

1. Going through a file.
2. Using the API by hand and not doing this kind of optimizations because they're hard to notice and people won't care in the first place and never fix them.

Exactly, I think this is another good argument for smtml 😃

Btw, I didn't use Z.to_bytes in this PR because it's an unreleased function. It's only available in 1.15: https://github.com/ocaml/Zarith/blob/386170fb0fd9fea4635214591e7ceea928d2cf5c/z.mli#L701-L719

I don't know if they're releasing it anytime soon

[redianthus]

I tried and it looks quite good! I don't see an issue anymore, so I think we can merge. :)